# Theory UNITY

Up to index of Isabelle/ZF/UNITY

theory UNITY
imports State
begin

    (*  Title:      ZF/UNITY/UNITY.thy
        ID:         $Id: UNITY.thy,v 1.7 2005/06/17 14:15:11 haftmann Exp $
        Author:     Sidi O Ehmety, Computer Laboratory
        Copyright   2001  University of Cambridge
    *)

    header {*The Basic UNITY Theory*}

    theory UNITY imports State begin

    text{*The basic UNITY theory (revised version, based upon the "co" operator)
    From Misra, "A Logic for Concurrent Programming", 1994.

    This ZF theory was ported from its HOL equivalent.*}

    consts
      "constrains" :: "[i, i] => i"  (infixl "co"     60)
      op_unless    :: "[i, i] => i"  (infixl "unless" 60)

    constdefs
       program  :: i
      "program == {<init, acts, allowed>:
                   Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)).
                   id(state) ∈ acts & id(state) ∈ allowed}"

      mk_program :: "[i,i,i]=>i"
      --{* The definition yields a program thanks to the coercions
           init ∩ state, acts ∩ Pow(state*state), etc. *}
      "mk_program(init, acts, allowed) ==
        <init ∩ state, cons(id(state), acts ∩ Pow(state*state)),
                  cons(id(state), allowed ∩ Pow(state*state))>"

      SKIP :: i
      "SKIP == mk_program(state, 0, Pow(state*state))"

      (* Coercion from anything to program *)
      programify :: "i=>i"
      "programify(F) == if F ∈ program then F else SKIP"

      RawInit :: "i=>i"
      "RawInit(F) == fst(F)"

      Init :: "i=>i"
      "Init(F) == RawInit(programify(F))"

      RawActs :: "i=>i"
      "RawActs(F) == cons(id(state), fst(snd(F)))"

      Acts :: "i=>i"
      "Acts(F) == RawActs(programify(F))"

      RawAllowedActs :: "i=>i"
      "RawAllowedActs(F) == cons(id(state), snd(snd(F)))"

      AllowedActs :: "i=>i"
      "AllowedActs(F) == RawAllowedActs(programify(F))"

      Allowed :: "i =>i"
      "Allowed(F) == {G ∈ program. Acts(G) ⊆ AllowedActs(F)}"

      initially :: "i=>i"
      "initially(A) == {F ∈ program. Init(F)⊆A}"

      stable     :: "i=>i"
       "stable(A) == A co A"

      strongest_rhs :: "[i, i] => i"
      "strongest_rhs(F, A) == Inter({B ∈ Pow(state). F ∈ A co B})"

      invariant :: "i => i"
      "invariant(A) == initially(A) ∩ stable(A)"

      (* meta-function composition *)
      metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65)
      "f comp g == %x. f(g(x))"

      pg_compl :: "i=>i"
      "pg_compl(X)== program - X"

    defs
      constrains_def:
         "A co B == {F ∈ program. (∀act ∈ Acts(F). act``A⊆B) & st_set(A)}"
        --{* the condition @{term "st_set(A)"} makes the definition slightly
             stronger than the HOL one *}

      unless_def:    "A unless B == (A - B) co (A Un B)"

    text{*SKIP*}
    lemma SKIP_in_program [iff,TC]: "SKIP ∈ program"
    by (force simp add: SKIP_def program_def mk_program_def)

    subsection{*The function @{term programify}, the coercion from anything to
     program*}

    lemma programify_program [simp]: "F ∈ program ==> programify(F)=F"
    by (force simp add: programify_def)

    lemma programify_in_program [iff,TC]: "programify(F) ∈ program"
    by (force simp add: programify_def)

    text{*Collapsing rules: to remove programify from expressions*}
    lemma programify_idem [simp]: "programify(programify(F))=programify(F)"
    by (force simp add: programify_def)

    lemma Init_programify [simp]: "Init(programify(F)) = Init(F)"
    by (simp add: Init_def)

    lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)"
    by (simp add: Acts_def)

    lemma AllowedActs_programify [simp]:
         "AllowedActs(programify(F)) = AllowedActs(F)"
    by (simp add: AllowedActs_def)

    subsection{*The Inspectors for Programs*}

    lemma id_in_RawActs: "F ∈ program ==>id(state) ∈ RawActs(F)"
    by (auto simp add: program_def RawActs_def)

    lemma id_in_Acts [iff,TC]: "id(state) ∈ Acts(F)"
    by (simp add: id_in_RawActs Acts_def)

    lemma id_in_RawAllowedActs: "F ∈ program ==>id(state) ∈ RawAllowedActs(F)"
    by (auto simp add: program_def RawAllowedActs_def)

    lemma id_in_AllowedActs [iff,TC]: "id(state) ∈ AllowedActs(F)"
    by (simp add: id_in_RawAllowedActs AllowedActs_def)

    lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)"
    by (simp add: cons_absorb)

    lemma cons_id_AllowedActs [simp]:
         "cons(id(state), AllowedActs(F)) = AllowedActs(F)"
    by (simp add: cons_absorb)

    subsection{*Types of the Inspectors*}

    lemma RawInit_type: "F ∈ program ==> RawInit(F)⊆state"
    by (auto simp add: program_def RawInit_def)

    lemma RawActs_type: "F ∈ program ==> RawActs(F)⊆Pow(state*state)"
    by (auto simp add: program_def RawActs_def)

    lemma RawAllowedActs_type:
         "F ∈ program ==> RawAllowedActs(F)⊆Pow(state*state)"
    by (auto simp add: program_def RawAllowedActs_def)

    lemma Init_type: "Init(F)⊆state"
    by (simp add: RawInit_type Init_def)

    lemmas InitD = Init_type [THEN subsetD, standard]

    lemma st_set_Init [iff]: "st_set(Init(F))"
    apply (unfold st_set_def)
    apply (rule Init_type)
    done

    lemma Acts_type: "Acts(F)⊆Pow(state*state)"
    by (simp add: RawActs_type Acts_def)

    lemma AllowedActs_type: "AllowedActs(F) ⊆ Pow(state*state)"
    by (simp add: RawAllowedActs_type AllowedActs_def)

    text{*Needed in Behaviors*}
    lemma ActsD: "[| act ∈ Acts(F); <s,s'> ∈ act |] ==> s ∈ state & s' ∈ state"
    by (blast dest: Acts_type [THEN subsetD])

    lemma AllowedActsD:
         "[| act ∈ AllowedActs(F); <s,s'> ∈ act |] ==> s ∈ state & s' ∈ state"
    by (blast dest: AllowedActs_type [THEN subsetD])

    subsection{*Simplification rules involving @{term state}, @{term Init},
      @{term Acts}, and @{term AllowedActs}*}

    text{*But are they really needed?*}

    lemma state_subset_is_Init_iff [iff]: "state ⊆ Init(F) <-> Init(F)=state"
    by (cut_tac F = F in Init_type, auto)

    lemma Pow_state_times_state_is_subset_Acts_iff [iff]:
         "Pow(state*state) ⊆ Acts(F) <-> Acts(F)=Pow(state*state)"
    by (cut_tac F = F in Acts_type, auto)

    lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]:
         "Pow(state*state) ⊆ AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)"
    by (cut_tac F = F in AllowedActs_type, auto)

    subsubsection{*Eliminating @{text "∩ state"} from expressions*}

    lemma Init_Int_state [simp]: "Init(F) ∩ state = Init(F)"
    by (cut_tac F = F in Init_type, blast)

    lemma state_Int_Init [simp]: "state ∩ Init(F) = Init(F)"
    by (cut_tac F = F in Init_type, blast)

    lemma Acts_Int_Pow_state_times_state [simp]:
         "Acts(F) ∩ Pow(state*state) = Acts(F)"
    by (cut_tac F = F in Acts_type, blast)

    lemma state_times_state_Int_Acts [simp]:
         "Pow(state*state) ∩ Acts(F) = Acts(F)"
    by (cut_tac F = F in Acts_type, blast)

    lemma AllowedActs_Int_Pow_state_times_state [simp]:
         "AllowedActs(F) ∩ Pow(state*state) = AllowedActs(F)"
    by (cut_tac F = F in AllowedActs_type, blast)

    lemma state_times_state_Int_AllowedActs [simp]:
         "Pow(state*state) ∩ AllowedActs(F) = AllowedActs(F)"
    by (cut_tac F = F in AllowedActs_type, blast)

    subsubsection{*The Operator @{term mk_program}*}

    lemma mk_program_in_program [iff,TC]:
         "mk_program(init, acts, allowed) ∈ program"
    by (auto simp add: mk_program_def program_def)

    lemma RawInit_eq [simp]:
         "RawInit(mk_program(init, acts, allowed)) = init ∩ state"
    by (auto simp add: mk_program_def RawInit_def)

    lemma RawActs_eq [simp]:
         "RawActs(mk_program(init, acts, allowed)) =
          cons(id(state), acts ∩ Pow(state*state))"
    by (auto simp add: mk_program_def RawActs_def)

    lemma RawAllowedActs_eq [simp]:
         "RawAllowedActs(mk_program(init, acts, allowed)) =
          cons(id(state), allowed ∩ Pow(state*state))"
    by (auto simp add: mk_program_def RawAllowedActs_def)

    lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init ∩ state"
    by (simp add: Init_def)

    lemma Acts_eq [simp]:
         "Acts(mk_program(init, acts, allowed)) =
          cons(id(state), acts  ∩ Pow(state*state))"
    by (simp add: Acts_def)

    lemma AllowedActs_eq [simp]:
         "AllowedActs(mk_program(init, acts, allowed))=
          cons(id(state), allowed ∩ Pow(state*state))"
    by (simp add: AllowedActs_def)

    text{*Init, Acts, and AlowedActs  of SKIP *}

    lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state"
    by (simp add: SKIP_def)

    lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)"
    by (force simp add: SKIP_def)

    lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}"
    by (force simp add: SKIP_def)

    lemma Init_SKIP [simp]: "Init(SKIP) = state"
    by (force simp add: SKIP_def)

    lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}"
    by (force simp add: SKIP_def)

    lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)"
    by (force simp add: SKIP_def)

    text{*Equality of UNITY programs*}

    lemma raw_surjective_mk_program:
         "F ∈ program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"
    apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def
                RawAllowedActs_def, blast+)
    done

    lemma surjective_mk_program [simp]:
      "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)"
    by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def)

    lemma program_equalityI:
        "[|Init(F) = Init(G); Acts(F) = Acts(G);
           AllowedActs(F) = AllowedActs(G); F ∈ program; G ∈ program |] ==> F = G"
    apply (subgoal_tac "programify(F) = programify(G)")
    apply simp
    apply (simp only: surjective_mk_program [symmetric])
    done

    lemma program_equalityE:
     "[|F = G;
        [|Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]
        ==> P |]
      ==> P"
    by force

    lemma program_equality_iff:
        "[| F ∈ program; G ∈ program |] ==>(F=G)  <->
         (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))"
    by (blast intro: program_equalityI program_equalityE)

    subsection{*These rules allow "lazy" definition expansion*}

    lemma def_prg_Init:
         "F == mk_program (init,acts,allowed) ==> Init(F) = init ∩ state"
    by auto

    lemma def_prg_Acts:
         "F == mk_program (init,acts,allowed)
          ==> Acts(F) = cons(id(state), acts ∩ Pow(state*state))"
    by auto

    lemma def_prg_AllowedActs:
         "F == mk_program (init,acts,allowed)
          ==> AllowedActs(F) = cons(id(state), allowed ∩ Pow(state*state))"
    by auto

    lemma def_prg_simps:
        "[| F == mk_program (init,acts,allowed) |]
         ==> Init(F) = init ∩ state &
             Acts(F) = cons(id(state), acts ∩ Pow(state*state)) &
             AllowedActs(F) = cons(id(state), allowed ∩ Pow(state*state))"
    by auto

    text{*An action is expanded only if a pair of states is being tested against it*}
    lemma def_act_simp:
         "[| act == {<s,s'> ∈ A*B. P(s, s')} |]
          ==> (<s,s'> ∈ act) <-> (<s,s'> ∈ A*B & P(s, s'))"
    by auto

    text{*A set is expanded only if an element is being tested against it*}
    lemma def_set_simp: "A == B ==> (x ∈ A) <-> (x ∈ B)"
    by auto

    subsection{*The Constrains Operator*}

    lemma constrains_type: "A co B ⊆ program"
    by (force simp add: constrains_def)

    lemma constrainsI:
        "[|(!!act s s'. [| act: Acts(F);  <s,s'> ∈ act; s ∈ A|] ==> s' ∈ A');
            F ∈ program; st_set(A) |]  ==> F ∈ A co A'"
    by (force simp add: constrains_def)

    lemma constrainsD:
       "F ∈ A co B ==> ∀act ∈ Acts(F). act``A⊆B"
    by (force simp add: constrains_def)

    lemma constrainsD2: "F ∈ A co B ==> F ∈ program & st_set(A)"
    by (force simp add: constrains_def)

    lemma constrains_empty [iff]: "F ∈ 0 co B <-> F ∈ program"
    by (force simp add: constrains_def st_set_def)

    lemma constrains_empty2 [iff]: "(F ∈ A co 0) <-> (A=0 & F ∈ program)"
    by (force simp add: constrains_def st_set_def)

    lemma constrains_state [iff]: "(F ∈ state co B) <-> (state⊆B & F ∈ program)"
    apply (cut_tac F = F in Acts_type)
    apply (force simp add: constrains_def st_set_def)
    done

    lemma constrains_state2 [iff]: "F ∈ A co state <-> (F ∈ program & st_set(A))"
    apply (cut_tac F = F in Acts_type)
    apply (force simp add: constrains_def st_set_def)
    done

    text{*monotonic in 2nd argument*}
    lemma constrains_weaken_R:
        "[| F ∈ A co A'; A'⊆B' |] ==> F ∈ A co B'"
    apply (unfold constrains_def, blast)
    done

    text{*anti-monotonic in 1st argument*}
    lemma constrains_weaken_L:
        "[| F ∈ A co A'; B⊆A |] ==> F ∈ B co A'"
    apply (unfold constrains_def st_set_def, blast)
    done

    lemma constrains_weaken:
       "[| F ∈ A co A'; B⊆A; A'⊆B' |] ==> F ∈ B co B'"
    apply (drule constrains_weaken_R)
    apply (drule_tac [2] constrains_weaken_L, blast+)
    done

    subsection{*Constrains and Union*}

    lemma constrains_Un:
        "[| F ∈ A co A'; F ∈ B co B' |] ==> F ∈ (A Un B) co (A' Un B')"
    by (auto simp add: constrains_def st_set_def, force)

    lemma constrains_UN:
         "[|!!i. i ∈ I ==> F ∈ A(i) co A'(i); F ∈ program |]
          ==> F ∈ (\<Union>i ∈ I. A(i)) co (\<Union>i ∈ I. A'(i))"
    by (force simp add: constrains_def st_set_def)

    lemma constrains_Un_distrib:
         "(A Un B) co C = (A co C) ∩ (B co C)"
    by (force simp add: constrains_def st_set_def)

    lemma constrains_UN_distrib:
       "i ∈ I ==> (\<Union>i ∈ I. A(i)) co B = (\<Inter>i ∈ I. A(i) co B)"
    by (force simp add: constrains_def st_set_def)

    subsection{*Constrains and Intersection*}

    lemma constrains_Int_distrib: "C co (A ∩ B) = (C co A) ∩ (C co B)"
    by (force simp add: constrains_def st_set_def)

    lemma constrains_INT_distrib:
         "x ∈ I ==> A co (\<Inter>i ∈ I. B(i)) = (\<Inter>i ∈ I. A co B(i))"
    by (force simp add: constrains_def st_set_def)

    lemma constrains_Int:
        "[| F ∈ A co A'; F ∈ B co B' |] ==> F ∈ (A ∩ B) co (A' ∩ B')"
    by (force simp add: constrains_def st_set_def)

    lemma constrains_INT [rule_format]:
         "[| ∀i ∈ I. F ∈ A(i) co A'(i); F ∈ program|]
          ==> F ∈ (\<Inter>i ∈ I. A(i)) co (\<Inter>i ∈ I. A'(i))"
    apply (case_tac "I=0")
     apply (simp add: Inter_def)
    apply (erule not_emptyE)
    apply (auto simp add: constrains_def st_set_def, blast)
    apply (drule bspec, assumption, force)
    done

    (* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *)
    lemma constrains_All:
    "[| ∀z. F:{s ∈ state. P(s, z)} co {s ∈ state. Q(s, z)}; F ∈ program |]==>
        F:{s ∈ state. ∀z. P(s, z)} co {s ∈ state. ∀z. Q(s, z)}"
    by (unfold constrains_def, blast)

    lemma constrains_imp_subset:
      "[| F ∈ A co A' |] ==> A ⊆ A'"
    by (unfold constrains_def st_set_def, force)

    text{*The reasoning is by subsets since "co" refers to single actions
      only.  So this rule isn't that useful.*}

    lemma constrains_trans: "[| F ∈ A co B; F ∈ B co C |] ==> F ∈ A co C"
    by (unfold constrains_def st_set_def, auto, blast)

    lemma constrains_cancel:
    "[| F ∈ A co (A' Un B); F ∈ B co B' |] ==> F ∈ A co (A' Un B')"
    apply (drule_tac A = B in constrains_imp_subset)
    apply (blast intro: constrains_weaken_R)
    done

    subsection{*The Unless Operator*}

    lemma unless_type: "A unless B ⊆ program"
    by (force simp add: unless_def constrains_def)

    lemma unlessI: "[| F ∈ (A-B) co (A Un B) |] ==> F ∈ A unless B"
    apply (unfold unless_def)
    apply (blast dest: constrainsD2)
    done

    lemma unlessD: "F :A unless B ==> F ∈ (A-B) co (A Un B)"
    by (unfold unless_def, auto)

    subsection{*The Operator @{term initially}*}

    lemma initially_type: "initially(A) ⊆ program"
    by (unfold initially_def, blast)

    lemma initiallyI: "[| F ∈ program; Init(F)⊆A |] ==> F ∈ initially(A)"
    by (unfold initially_def, blast)

    lemma initiallyD: "F ∈ initially(A) ==> Init(F)⊆A"
    by (unfold initially_def, blast)

    subsection{*The Operator @{term stable}*}

    lemma stable_type: "stable(A)⊆program"
    by (unfold stable_def constrains_def, blast)

    lemma stableI: "F ∈ A co A ==> F ∈ stable(A)"
    by (unfold stable_def, assumption)

    lemma stableD: "F ∈ stable(A) ==> F ∈ A co A"
    by (unfold stable_def, assumption)

    lemma stableD2: "F ∈ stable(A) ==> F ∈ program & st_set(A)"
    by (unfold stable_def constrains_def, auto)

    lemma stable_state [simp]: "stable(state) = program"
    by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD])

    lemma stable_unless: "stable(A)= A unless 0"
    by (auto simp add: unless_def stable_def)

    subsection{*Union and Intersection with @{term stable}*}

    lemma stable_Un:
        "[| F ∈ stable(A); F ∈ stable(A') |] ==> F ∈ stable(A Un A')"
    apply (unfold stable_def)
    apply (blast intro: constrains_Un)
    done

    lemma stable_UN:
         "[|!!i. i∈I ==> F ∈ stable(A(i)); F ∈ program |]
          ==> F ∈ stable (\<Union>i ∈ I. A(i))"
    apply (unfold stable_def)
    apply (blast intro: constrains_UN)
    done

    lemma stable_Int:
        "[| F ∈ stable(A);  F ∈ stable(A') |] ==> F ∈ stable (A ∩ A')"
    apply (unfold stable_def)
    apply (blast intro: constrains_Int)
    done

    lemma stable_INT:
         "[| !!i. i ∈ I ==> F ∈ stable(A(i)); F ∈ program |]
          ==> F ∈ stable (\<Inter>i ∈ I. A(i))"
    apply (unfold stable_def)
    apply (blast intro: constrains_INT)
    done

    lemma stable_All:
        "[|∀z. F ∈ stable({s ∈ state. P(s, z)}); F ∈ program|]
         ==> F ∈ stable({s ∈ state. ∀z. P(s, z)})"
    apply (unfold stable_def)
    apply (rule constrains_All, auto)
    done

    lemma stable_constrains_Un:
         "[| F ∈ stable(C); F ∈ A co (C Un A') |] ==> F ∈ (C Un A) co (C Un A')"
    apply (unfold stable_def constrains_def st_set_def, auto)
    apply (blast dest!: bspec)
    done

    lemma stable_constrains_Int:
         "[| F ∈ stable(C); F ∈  (C ∩ A) co A' |] ==> F ∈ (C ∩ A) co (C ∩ A')"
    by (unfold stable_def constrains_def st_set_def, blast)

    (* [| F ∈ stable(C); F  ∈ (C ∩ A) co A |] ==> F ∈ stable(C ∩ A) *)
    lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]

    subsection{*The Operator @{term invariant}*}

    lemma invariant_type: "invariant(A) ⊆ program"
    apply (unfold invariant_def)
    apply (blast dest: stable_type [THEN subsetD])
    done

    lemma invariantI: "[| Init(F)⊆A;  F ∈ stable(A) |] ==> F ∈ invariant(A)"
    apply (unfold invariant_def initially_def)
    apply (frule stable_type [THEN subsetD], auto)
    done

    lemma invariantD: "F ∈ invariant(A) ==> Init(F)⊆A & F ∈ stable(A)"
    by (unfold invariant_def initially_def, auto)

    lemma invariantD2: "F ∈ invariant(A) ==> F ∈ program & st_set(A)"
    apply (unfold invariant_def)
    apply (blast dest: stableD2)
    done

    text{*Could also say
          @{term "invariant(A) ∩ invariant(B) ⊆ invariant (A ∩ B)"}*}
    lemma invariant_Int:
      "[| F ∈ invariant(A);  F ∈ invariant(B) |] ==> F ∈ invariant(A ∩ B)"
    apply (unfold invariant_def initially_def)
    apply (simp add: stable_Int, blast)
    done

    subsection{*The Elimination Theorem*}

    (** The "free" m has become universally quantified!
     Should the premise be !!m instead of ∀m ? Would make it harder
     to use in forward proof. **)

    text{*The general case is easier to prove than the special case!*}
    lemma "elimination":
        "[| ∀m ∈ M. F ∈ {s ∈ A. x(s) = m} co B(m); F ∈ program  |]
         ==> F ∈ {s ∈ A. x(s) ∈ M} co (\<Union>m ∈ M. B(m))"
    by (auto simp add: constrains_def st_set_def, blast)

    text{*As above, but for the special case of A=state*}
    lemma elimination2:
         "[| ∀m ∈ M. F ∈ {s ∈ state. x(s) = m} co B(m); F ∈ program  |]
         ==> F:{s ∈ state. x(s) ∈ M} co (\<Union>m ∈ M. B(m))"
    by (rule UNITY.elimination, auto)

    subsection{*The Operator @{term strongest_rhs}*}

    lemma constrains_strongest_rhs:
        "[| F ∈ program; st_set(A) |] ==> F ∈ A co (strongest_rhs(F,A))"
    by (auto simp add: constrains_def strongest_rhs_def st_set_def
                  dest: Acts_type [THEN subsetD])

    lemma strongest_rhs_is_strongest:
         "[| F ∈ A co B; st_set(B) |] ==> strongest_rhs(F,A) ⊆ B"
    by (auto simp add: constrains_def strongest_rhs_def st_set_def)

    ML
    {*
    val constrains_def = thm "constrains_def";
    val stable_def = thm "stable_def";
    val invariant_def = thm "invariant_def";
    val unless_def = thm "unless_def";
    val initially_def = thm "initially_def";
    val SKIP_def = thm "SKIP_def";
    val Allowed_def = thm "Allowed_def";
    val programify_def = thm "programify_def";
    val metacomp_def = thm "metacomp_def";

    val id_in_Acts = thm "id_in_Acts";
    val id_in_RawAllowedActs = thm "id_in_RawAllowedActs";
    val id_in_AllowedActs = thm "id_in_AllowedActs";
    val cons_id_Acts = thm "cons_id_Acts";
    val cons_id_AllowedActs = thm "cons_id_AllowedActs";
    val Init_type = thm "Init_type";
    val st_set_Init = thm "st_set_Init";
    val Acts_type = thm "Acts_type";
    val AllowedActs_type = thm "AllowedActs_type";
    val ActsD = thm "ActsD";
    val AllowedActsD = thm "AllowedActsD";
    val mk_program_in_program = thm "mk_program_in_program";
    val Init_eq = thm "Init_eq";
    val Acts_eq = thm "Acts_eq";
    val AllowedActs_eq = thm "AllowedActs_eq";
    val Init_SKIP = thm "Init_SKIP";
    val Acts_SKIP = thm "Acts_SKIP";
    val AllowedActs_SKIP = thm "AllowedActs_SKIP";
    val raw_surjective_mk_program = thm "raw_surjective_mk_program";
    val surjective_mk_program = thm "surjective_mk_program";
    val program_equalityI = thm "program_equalityI";
    val program_equalityE = thm "program_equalityE";
    val program_equality_iff = thm "program_equality_iff";
    val def_prg_Init = thm "def_prg_Init";
    val def_prg_Acts = thm "def_prg_Acts";
    val def_prg_AllowedActs = thm "def_prg_AllowedActs";
    val def_prg_simps = thm "def_prg_simps";
    val def_act_simp = thm "def_act_simp";
    val def_set_simp = thm "def_set_simp";
    val constrains_type = thm "constrains_type";
    val constrainsI = thm "constrainsI";
    val constrainsD = thm "constrainsD";
    val constrainsD2 = thm "constrainsD2";
    val constrains_empty = thm "constrains_empty";
    val constrains_empty2 = thm "constrains_empty2";
    val constrains_state = thm "constrains_state";
    val constrains_state2 = thm "constrains_state2";
    val constrains_weaken_R = thm "constrains_weaken_R";
    val constrains_weaken_L = thm "constrains_weaken_L";
    val constrains_weaken = thm "constrains_weaken";
    val constrains_Un = thm "constrains_Un";
    val constrains_UN = thm "constrains_UN";
    val constrains_Un_distrib = thm "constrains_Un_distrib";
    val constrains_UN_distrib = thm "constrains_UN_distrib";
    val constrains_Int_distrib = thm "constrains_Int_distrib";
    val constrains_INT_distrib = thm "constrains_INT_distrib";
    val constrains_Int = thm "constrains_Int";
    val constrains_INT = thm "constrains_INT";
    val constrains_All = thm "constrains_All";
    val constrains_imp_subset = thm "constrains_imp_subset";
    val constrains_trans = thm "constrains_trans";
    val constrains_cancel = thm "constrains_cancel";
    val unless_type = thm "unless_type";
    val unlessI = thm "unlessI";
    val unlessD = thm "unlessD";
    val initially_type = thm "initially_type";
    val initiallyI = thm "initiallyI";
    val initiallyD = thm "initiallyD";
    val stable_type = thm "stable_type";
    val stableI = thm "stableI";
    val stableD = thm "stableD";
    val stableD2 = thm "stableD2";
    val stable_state = thm "stable_state";
    val stable_unless = thm "stable_unless";
    val stable_Un = thm "stable_Un";
    val stable_UN = thm "stable_UN";
    val stable_Int = thm "stable_Int";
    val stable_INT = thm "stable_INT";
    val stable_All = thm "stable_All";
    val stable_constrains_Un = thm "stable_constrains_Un";
    val stable_constrains_Int = thm "stable_constrains_Int";
    val invariant_type = thm "invariant_type";
    val invariantI = thm "invariantI";
    val invariantD = thm "invariantD";
    val invariantD2 = thm "invariantD2";
    val invariant_Int = thm "invariant_Int";
    val elimination = thm "elimination";
    val elimination2 = thm "elimination2";
    val constrains_strongest_rhs = thm "constrains_strongest_rhs";
    val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest";

    fun simp_of_act def = def RS def_act_simp;
    fun simp_of_set def = def RS def_set_simp;
    *}

    end

lemma SKIP_in_program:

      SKIP ∈ program

### The function @{term programify}, the coercion from anything to program

lemma programify_program:

      F ∈ program ==> programify(F) = F

lemma programify_in_program:

      programify(F) ∈ program

lemma programify_idem:

      programify(programify(F)) = programify(F)

lemma Init_programify:

      Init(programify(F)) = Init(F)

lemma Acts_programify:

      Acts(programify(F)) = Acts(F)

lemma AllowedActs_programify:

      AllowedActs(programify(F)) = AllowedActs(F)

### The Inspectors for Programs

lemma id_in_RawActs:

      F ∈ program ==> id(state) ∈ RawActs(F)

lemma id_in_Acts:

      id(state) ∈ Acts(F)

lemma id_in_RawAllowedActs:

      F ∈ program ==> id(state) ∈ RawAllowedActs(F)

lemma id_in_AllowedActs:

      id(state) ∈ AllowedActs(F)

lemma cons_id_Acts:

      cons(id(state), Acts(F)) = Acts(F)

lemma cons_id_AllowedActs:

      cons(id(state), AllowedActs(F)) = AllowedActs(F)

### Types of the Inspectors

lemma RawInit_type:

      F ∈ program ==> RawInit(F) ⊆ state

lemma RawActs_type:

      F ∈ program ==> RawActs(F) ⊆ Pow(state × state)

lemma RawAllowedActs_type:

      F ∈ program ==> RawAllowedActs(F) ⊆ Pow(state × state)

lemma Init_type:

      Init(F) ⊆ state

lemmas InitD:

      c ∈ Init(F) ==> c ∈ state

lemmas InitD:

      c ∈ Init(F) ==> c ∈ state

lemma st_set_Init:

      st_set(Init(F))

lemma Acts_type:

      Acts(F) ⊆ Pow(state × state)

lemma AllowedActs_type:

      AllowedActs(F) ⊆ Pow(state × state)

lemma ActsD:

      [| act ∈ Acts(F); ⟨s, s'⟩ ∈ act |] ==> s ∈ state ∧ s' ∈ state

lemma AllowedActsD:

      [| act ∈ AllowedActs(F); ⟨s, s'⟩ ∈ act |] ==> s ∈ state ∧ s' ∈ state

### Simplification rules involving @{term state}, @{term Init}, @{term Acts}, and @{term AllowedActs}

lemma state_subset_is_Init_iff:

      state ⊆ Init(F) <-> Init(F) = state

lemma Pow_state_times_state_is_subset_Acts_iff:

      Pow(state × state) ⊆ Acts(F) <-> Acts(F) = Pow(state × state)

lemma Pow_state_times_state_is_subset_AllowedActs_iff:

      Pow(state × state) ⊆ AllowedActs(F) <-> AllowedActs(F) = Pow(state × state)

#### Eliminating @{text "∩ state"} from expressions

lemma Init_Int_state:

      Init(F) ∩ state = Init(F)

lemma state_Int_Init:

      state ∩ Init(F) = Init(F)

lemma Acts_Int_Pow_state_times_state:

      Acts(F) ∩ Pow(state × state) = Acts(F)

lemma state_times_state_Int_Acts:

      Pow(state × state) ∩ Acts(F) = Acts(F)

lemma AllowedActs_Int_Pow_state_times_state:

      AllowedActs(F) ∩ Pow(state × state) = AllowedActs(F)

lemma state_times_state_Int_AllowedActs:

      Pow(state × state) ∩ AllowedActs(F) = AllowedActs(F)

#### The Operator @{term mk_program}

lemma mk_program_in_program:

      mk_program(init, acts, allowed) ∈ program

lemma RawInit_eq:

      RawInit(mk_program(init, acts, allowed)) = init ∩ state

lemma RawActs_eq:

      RawActs(mk_program(init, acts, allowed)) =
      cons(id(state), acts ∩ Pow(state × state))

lemma RawAllowedActs_eq:

      RawAllowedActs(mk_program(init, acts, allowed)) =
      cons(id(state), allowed ∩ Pow(state × state))

lemma Init_eq:

      Init(mk_program(init, acts, allowed)) = init ∩ state

lemma Acts_eq:

      Acts(mk_program(init, acts, allowed)) =
      cons(id(state), acts ∩ Pow(state × state))

lemma AllowedActs_eq:

      AllowedActs(mk_program(init, acts, allowed)) =
      cons(id(state), allowed ∩ Pow(state × state))

lemma RawInit_SKIP:

      RawInit(SKIP) = state

lemma RawAllowedActs_SKIP:

      RawAllowedActs(SKIP) = Pow(state × state)

lemma RawActs_SKIP:

      RawActs(SKIP) = {id(state)}

lemma Init_SKIP:

      Init(SKIP) = state

lemma Acts_SKIP:

      Acts(SKIP) = {id(state)}

lemma AllowedActs_SKIP:

      AllowedActs(SKIP) = Pow(state × state)

lemma raw_surjective_mk_program:

      F ∈ program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F)) = F

lemma surjective_mk_program:

      mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)

lemma program_equalityI:

      [| Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G);
         F ∈ program; G ∈ program |]
      ==> F = G

lemma program_equalityE:

      [| F = G;
         [| Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]
         ==> P |]
      ==> P

lemma program_equality_iff:

      [| F ∈ program; G ∈ program |]
      ==> F = G <->
          Init(F) = Init(G) ∧ Acts(F) = Acts(G) ∧ AllowedActs(F) = AllowedActs(G)

### These rules allow "lazy" definition expansion

lemma def_prg_Init:

      F == mk_program(init, acts, allowed) ==> Init(F) = init ∩ state

lemma def_prg_Acts:

      F == mk_program(init, acts, allowed)
      ==> Acts(F) = cons(id(state), acts ∩ Pow(state × state))

lemma def_prg_AllowedActs:

      F == mk_program(init, acts, allowed)
      ==> AllowedActs(F) = cons(id(state), allowed ∩ Pow(state × state))

lemma def_prg_simps:

      F == mk_program(init, acts, allowed)
      ==> Init(F) = init ∩ state ∧
          Acts(F) = cons(id(state), acts ∩ Pow(state × state)) ∧
          AllowedActs(F) = cons(id(state), allowed ∩ Pow(state × state))

lemma def_act_simp:

      act == {⟨s,s'⟩ ∈ A × B . P(s, s')}
      ==> ⟨s, s'⟩ ∈ act <-> ⟨s, s'⟩ ∈ A × B ∧ P(s, s')

lemma def_set_simp:

      A == B ==> x ∈ A <-> x ∈ B

### The Constrains Operator

lemma constrains_type:

      A co B ⊆ program

lemma constrainsI:

      [| !!act s s'. [| act ∈ Acts(F); ⟨s, s'⟩ ∈ act; s ∈ A |] ==> s' ∈ A';
         F ∈ program; st_set(A) |]
      ==> F ∈ A co A'

lemma constrainsD:

      F ∈ A co B ==> ∀act∈Acts(F). act `` A ⊆ B

lemma constrainsD2:

      F ∈ A co B ==> F ∈ program ∧ st_set(A)

lemma constrains_empty:

      F ∈ 0 co B <-> F ∈ program

lemma constrains_empty2:

      F ∈ A co 0 <-> A = 0 ∧ F ∈ program

lemma constrains_state:

      F ∈ state co B <-> state ⊆ B ∧ F ∈ program

lemma constrains_state2:

      F ∈ A co state <-> F ∈ program ∧ st_set(A)

lemma constrains_weaken_R:

      [| F ∈ A co A'; A' ⊆ B' |] ==> F ∈ A co B'

lemma constrains_weaken_L:

      [| F ∈ A co A'; B ⊆ A |] ==> F ∈ B co A'

lemma constrains_weaken:

      [| F ∈ A co A'; B ⊆ A; A' ⊆ B' |] ==> F ∈ B co B'

### Constrains and Union

lemma constrains_Un:

      [| F ∈ A co A'; F ∈ B co B' |] ==> F ∈ A ∪ B co A' ∪ B'

lemma constrains_UN:

      [| !!i. i ∈ I ==> F ∈ A(i) co A'(i); F ∈ program |]
      ==> F ∈ (\<Union>i∈I. A(i)) co (\<Union>i∈I. A'(i))

lemma constrains_Un_distrib:

      A ∪ B co C = (A co C) ∩ (B co C)

lemma constrains_UN_distrib:

      i ∈ I ==> (\<Union>i∈I. A(i)) co B = (\<Inter>i∈I. A(i) co B)

### Constrains and Intersection

lemma constrains_Int_distrib:

      C co A ∩ B = (C co A) ∩ (C co B)

lemma constrains_INT_distrib:

      x ∈ I ==> A co (\<Inter>i∈I. B(i)) = (\<Inter>i∈I. A co B(i))

lemma constrains_Int:

      [| F ∈ A co A'; F ∈ B co B' |] ==> F ∈ A ∩ B co A' ∩ B'

lemma constrains_INT:

      [| !!i. i ∈ I ==> F ∈ A(i) co A'(i); F ∈ program |]
      ==> F ∈ (\<Inter>i∈I. A(i)) co (\<Inter>i∈I. A'(i))

lemma constrains_All:

      [| ∀z. F ∈ {s ∈ state . P(s, z)} co {s ∈ state . Q(s, z)}; F ∈ program |]
      ==> F ∈ {s ∈ state . ∀z. P(s, z)} co {s ∈ state . ∀z. Q(s, z)}

lemma constrains_imp_subset:

      F ∈ A co A' ==> A ⊆ A'

lemma constrains_trans:

      [| F ∈ A co B; F ∈ B co C |] ==> F ∈ A co C

lemma constrains_cancel:

      [| F ∈ A co A' ∪ B; F ∈ B co B' |] ==> F ∈ A co A' ∪ B'

### The Unless Operator

lemma unless_type:

      A unless B ⊆ program

lemma unlessI:

      F ∈ A - B co A ∪ B ==> F ∈ A unless B

lemma unlessD:

      F ∈ A unless B ==> F ∈ A - B co A ∪ B

### The Operator @{term initially}

lemma initially_type:

      initially(A) ⊆ program

lemma initiallyI:

      [| F ∈ program; Init(F) ⊆ A |] ==> F ∈ initially(A)

lemma initiallyD:

      F ∈ initially(A) ==> Init(F) ⊆ A

### The Operator @{term stable}

lemma stable_type:

      stable(A) ⊆ program

lemma stableI:

      F ∈ A co A ==> F ∈ stable(A)

lemma stableD:

      F ∈ stable(A) ==> F ∈ A co A

lemma stableD2:

      F ∈ stable(A) ==> F ∈ program ∧ st_set(A)

lemma stable_state:

      stable(state) = program

lemma stable_unless:

      stable(A) = A unless 0

### Union and Intersection with @{term stable}

lemma stable_Un:

      [| F ∈ stable(A); F ∈ stable(A') |] ==> F ∈ stable(A ∪ A')

lemma stable_UN:

      [| !!i. i ∈ I ==> F ∈ stable(A(i)); F ∈ program |]
      ==> F ∈ stable(\<Union>i∈I. A(i))

lemma stable_Int:

      [| F ∈ stable(A); F ∈ stable(A') |] ==> F ∈ stable(A ∩ A')

lemma stable_INT:

      [| !!i. i ∈ I ==> F ∈ stable(A(i)); F ∈ program |]
      ==> F ∈ stable(\<Inter>i∈I. A(i))

lemma stable_All:

      [| ∀z. F ∈ stable({s ∈ state . P(s, z)}); F ∈ program |]
      ==> F ∈ stable({s ∈ state . ∀z. P(s, z)})

lemma stable_constrains_Un:

      [| F ∈ stable(C); F ∈ A co C ∪ A' |] ==> F ∈ C ∪ A co C ∪ A'

lemma stable_constrains_Int:

      [| F ∈ stable(C); F ∈ C ∩ A co A' |] ==> F ∈ C ∩ A co C ∩ A'

lemmas stable_constrains_stable:

      [| F ∈ stable(C); F ∈ C ∩ A co A |] ==> F ∈ stable(C ∩ A)

lemmas stable_constrains_stable:

      [| F ∈ stable(C); F ∈ C ∩ A co A |] ==> F ∈ stable(C ∩ A)

### The Operator @{term invariant}

lemma invariant_type:

      invariant(A) ⊆ program

lemma invariantI:

      [| Init(F) ⊆ A; F ∈ stable(A) |] ==> F ∈ invariant(A)

lemma invariantD:

      F ∈ invariant(A) ==> Init(F) ⊆ A ∧ F ∈ stable(A)

lemma invariantD2:

      F ∈ invariant(A) ==> F ∈ program ∧ st_set(A)

lemma invariant_Int:

      [| F ∈ invariant(A); F ∈ invariant(B) |] ==> F ∈ invariant(A ∩ B)

### The Elimination Theorem

lemma elimination:

      [| ∀m∈M. F ∈ {s ∈ A . x(s) = m} co B(m); F ∈ program |]
      ==> F ∈ {s ∈ A . x(s) ∈ M} co (\<Union>m∈M. B(m))

lemma elimination2:

      [| ∀m∈M. F ∈ {s ∈ state . x(s) = m} co B(m); F ∈ program |]
      ==> F ∈ {s ∈ state . x(s) ∈ M} co (\<Union>m∈M. B(m))

### The Operator @{term strongest_rhs}

lemma constrains_strongest_rhs:

      [| F ∈ program; st_set(A) |] ==> F ∈ A co strongest_rhs(F, A)

lemma strongest_rhs_is_strongest:

      [| F ∈ A co B; st_set(B) |] ==> strongest_rhs(F, A) ⊆ B