# Theory UNITY

Up to index of Isabelle/HOL/UNITY

theory UNITY
imports Main
begin

    (*  Title:      HOL/UNITY/UNITY
        ID:         $Id: UNITY.thy,v 1.23 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    The basic UNITY theory (revised version, based upon the "co" operator)

    From Misra, "A Logic for Concurrent Programming", 1994
    *)

    header {*The Basic UNITY Theory*}

    theory UNITY imports Main begin

    typedef (Program)
      'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
                       allowed :: ('a * 'a)set set). Id ∈ acts & Id: allowed}"
      by blast

    constdefs
      Acts :: "'a program => ('a * 'a)set set"
        "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"

      "constrains" :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
        "A co B == {F. ∀act ∈ Acts F. act``A ⊆ B}"

      unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
        "A unless B == (A-B) co (A ∪ B)"

      mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
                       => 'a program"
        "mk_program == %(init, acts, allowed).
                          Abs_Program (init, insert Id acts, insert Id allowed)"

      Init :: "'a program => 'a set"
        "Init F == (%(init, acts, allowed). init) (Rep_Program F)"

      AllowedActs :: "'a program => ('a * 'a)set set"
        "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"

      Allowed :: "'a program => 'a program set"
        "Allowed F == {G. Acts G ⊆ AllowedActs F}"

      stable     :: "'a set => 'a program set"
        "stable A == A co A"

      strongest_rhs :: "['a program, 'a set] => 'a set"
        "strongest_rhs F A == Inter {B. F ∈ A co B}"

      invariant :: "'a set => 'a program set"
        "invariant A == {F. Init F ⊆ A} ∩ stable A"

      increasing :: "['a => 'b::{order}] => 'a program set"
        --{*Polymorphic in both states and the meaning of @{text "≤"}*}
        "increasing f == \<Inter>z. stable {s. z ≤ f s}"

    text{*Perhaps equalities.ML shouldn't add this in the first place!*}
    declare image_Collect [simp del]

    subsubsection{*The abstract type of programs*}

    lemmas program_typedef =
         Rep_Program Rep_Program_inverse Abs_Program_inverse
         Program_def Init_def Acts_def AllowedActs_def mk_program_def

    lemma Id_in_Acts [iff]: "Id ∈ Acts F"
    apply (cut_tac x = F in Rep_Program)
    apply (auto simp add: program_typedef)
    done

    lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
    by (simp add: insert_absorb Id_in_Acts)

    lemma Acts_nonempty [simp]: "Acts F ≠ {}"
    by auto

    lemma Id_in_AllowedActs [iff]: "Id ∈ AllowedActs F"
    apply (cut_tac x = F in Rep_Program)
    apply (auto simp add: program_typedef)
    done

    lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
    by (simp add: insert_absorb Id_in_AllowedActs)

    subsubsection{*Inspectors for type "program"*}

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

    lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
    by (simp add: program_typedef)

    lemma AllowedActs_eq [simp]:
         "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
    by (simp add: program_typedef)

    subsubsection{*Equality for UNITY programs*}

    lemma surjective_mk_program [simp]:
         "mk_program (Init F, Acts F, AllowedActs F) = F"
    apply (cut_tac x = F in Rep_Program)
    apply (auto simp add: program_typedef)
    apply (drule_tac f = Abs_Program in arg_cong)+
    apply (simp add: program_typedef insert_absorb)
    done

    lemma program_equalityI:
         "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]
          ==> F = G"
    apply (rule_tac t = F in surjective_mk_program [THEN subst])
    apply (rule_tac t = G in surjective_mk_program [THEN subst], simp)
    done

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

    lemma program_equality_iff:
         "(F=G) =
          (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"
    by (blast intro: program_equalityI program_equalityE)

    subsubsection{*co*}

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

    lemma constrainsD:
        "[| F ∈ A co A'; act: Acts F;  (s,s'): act;  s ∈ A |] ==> s': A'"
    by (unfold constrains_def, blast)

    lemma constrains_empty [iff]: "F ∈ {} co B"
    by (unfold constrains_def, blast)

    lemma constrains_empty2 [iff]: "(F ∈ A co {}) = (A={})"
    by (unfold constrains_def, blast)

    lemma constrains_UNIV [iff]: "(F ∈ UNIV co B) = (B = UNIV)"
    by (unfold constrains_def, blast)

    lemma constrains_UNIV2 [iff]: "F ∈ A co UNIV"
    by (unfold constrains_def, blast)

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

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

    lemma constrains_weaken:
       "[| F ∈ A co A'; B ⊆ A; A'<=B' |] ==> F ∈ B co B'"
    by (unfold constrains_def, blast)

    subsubsection{*Union*}

    lemma constrains_Un:
        "[| F ∈ A co A'; F ∈ B co B' |] ==> F ∈ (A ∪ B) co (A' ∪ B')"
    by (unfold constrains_def, blast)

    lemma constrains_UN:
        "(!!i. i ∈ I ==> F ∈ (A i) co (A' i))
         ==> F ∈ (\<Union>i ∈ I. A i) co (\<Union>i ∈ I. A' i)"
    by (unfold constrains_def, blast)

    lemma constrains_Un_distrib: "(A ∪ B) co C = (A co C) ∩ (B co C)"
    by (unfold constrains_def, blast)

    lemma constrains_UN_distrib: "(\<Union>i ∈ I. A i) co B = (\<Inter>i ∈ I. A i co B)"
    by (unfold constrains_def, blast)

    lemma constrains_Int_distrib: "C co (A ∩ B) = (C co A) ∩ (C co B)"
    by (unfold constrains_def, blast)

    lemma constrains_INT_distrib: "A co (\<Inter>i ∈ I. B i) = (\<Inter>i ∈ I. A co B i)"
    by (unfold constrains_def, blast)

    subsubsection{*Intersection*}

    lemma constrains_Int:
        "[| F ∈ A co A'; F ∈ B co B' |] ==> F ∈ (A ∩ B) co (A' ∩ B')"
    by (unfold constrains_def, blast)

    lemma constrains_INT:
        "(!!i. i ∈ I ==> F ∈ (A i) co (A' i))
         ==> F ∈ (\<Inter>i ∈ I. A i) co (\<Inter>i ∈ I. A' i)"
    by (unfold constrains_def, blast)

    lemma constrains_imp_subset: "F ∈ A co A' ==> A ⊆ A'"
    by (unfold constrains_def, auto)

    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, blast)

    lemma constrains_cancel:
       "[| F ∈ A co (A' ∪ B); F ∈ B co B' |] ==> F ∈ A co (A' ∪ B')"
    by (unfold constrains_def, clarify, blast)

    subsubsection{*unless*}

    lemma unlessI: "F ∈ (A-B) co (A ∪ B) ==> F ∈ A unless B"
    by (unfold unless_def, assumption)

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

    subsubsection{*stable*}

    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 stable_UNIV [simp]: "stable UNIV = UNIV"
    by (unfold stable_def constrains_def, auto)

    subsubsection{*Union*}

    lemma stable_Un:
        "[| F ∈ stable A; F ∈ stable A' |] ==> F ∈ stable (A ∪ A')"

    apply (unfold stable_def)
    apply (blast intro: constrains_Un)
    done

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

    lemma stable_Union:
        "(!!A. A ∈ X ==> F ∈ stable A) ==> F ∈ stable (\<Union>X)"
    by (unfold stable_def constrains_def, blast)

    subsubsection{*Intersection*}

    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 ∈ stable (\<Inter>i ∈ I. A i)"
    apply (unfold stable_def)
    apply (blast intro: constrains_INT)
    done

    lemma stable_Inter:
        "(!!A. A ∈ X ==> F ∈ stable A) ==> F ∈ stable (\<Inter>X)"
    by (unfold stable_def constrains_def, blast)

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

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

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

    subsubsection{*invariant*}

    lemma invariantI: "[| Init F ⊆ A;  F ∈ stable A |] ==> F ∈ invariant A"
    by (simp add: invariant_def)

    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)"
    by (auto simp add: invariant_def stable_Int)

    subsubsection{*increasing*}

    lemma increasingD:
         "F ∈ increasing f ==> F ∈ stable {s. z ⊆ f s}"
    by (unfold increasing_def, blast)

    lemma increasing_constant [iff]: "F ∈ increasing (%s. c)"
    by (unfold increasing_def stable_def, auto)

    lemma mono_increasing_o:
         "mono g ==> increasing f ⊆ increasing (g o f)"
    apply (unfold increasing_def stable_def constrains_def, auto)
    apply (blast intro: monoD order_trans)
    done

    (*Holds by the theorem (Suc m ⊆ n) = (m < n) *)
    lemma strict_increasingD:
         "!!z::nat. F ∈ increasing f ==> F ∈ stable {s. z < f s}"
    by (simp add: increasing_def Suc_le_eq [symmetric])

    (** 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. **)

    lemma elimination:
        "[| ∀m ∈ M. F ∈ {s. s x = m} co (B m) |]
         ==> F ∈ {s. s x ∈ M} co (\<Union>m ∈ M. B m)"
    by (unfold constrains_def, blast)

    text{*As above, but for the trivial case of a one-variable state, in which the
      state is identified with its one variable.*}
    lemma elimination_sing:
        "(∀m ∈ M. F ∈ {m} co (B m)) ==> F ∈ M co (\<Union>m ∈ M. B m)"
    by (unfold constrains_def, blast)

    subsubsection{*Theoretical Results from Section 6*}

    lemma constrains_strongest_rhs:
        "F ∈ A co (strongest_rhs F A )"
    by (unfold constrains_def strongest_rhs_def, blast)

    lemma strongest_rhs_is_strongest:
        "F ∈ A co B ==> strongest_rhs F A ⊆ B"
    by (unfold constrains_def strongest_rhs_def, blast)

    subsubsection{*Ad-hoc set-theory rules*}

    lemma Un_Diff_Diff [simp]: "A ∪ B - (A - B) = B"
    by blast

    lemma Int_Union_Union: "Union(B) ∩ A = Union((%C. C ∩ A)`B)"
    by blast

    text{*Needed for WF reasoning in WFair.ML*}

    lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
    by blast

    lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
    by blast

    subsection{*Partial versus Total Transitions*}

    constdefs
      totalize_act :: "('a * 'a)set => ('a * 'a)set"
        "totalize_act act == act ∪ diag (-(Domain act))"

      totalize :: "'a program => 'a program"
        "totalize F == mk_program (Init F,
                                   totalize_act ` Acts F,
                                   AllowedActs F)"

      mk_total_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
                       => 'a program"
        "mk_total_program args == totalize (mk_program args)"

      all_total :: "'a program => bool"
        "all_total F == ∀act ∈ Acts F. Domain act = UNIV"

    lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
    by (blast intro: sym [THEN image_eqI])

    subsubsection{*Basic properties*}

    lemma totalize_act_Id [simp]: "totalize_act Id = Id"
    by (simp add: totalize_act_def)

    lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"
    by (auto simp add: totalize_act_def)

    lemma Init_totalize [simp]: "Init (totalize F) = Init F"
    by (unfold totalize_def, auto)

    lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)"
    by (simp add: totalize_def insert_Id_image_Acts)

    lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"
    by (simp add: totalize_def)

    lemma totalize_constrains_iff [simp]: "(totalize F ∈ A co B) = (F ∈ A co B)"
    by (simp add: totalize_def totalize_act_def constrains_def, blast)

    lemma totalize_stable_iff [simp]: "(totalize F ∈ stable A) = (F ∈ stable A)"
    by (simp add: stable_def)

    lemma totalize_invariant_iff [simp]:
         "(totalize F ∈ invariant A) = (F ∈ invariant A)"
    by (simp add: invariant_def)

    lemma all_total_totalize: "all_total (totalize F)"
    by (simp add: totalize_def all_total_def)

    lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"
    by (force simp add: totalize_act_def)

    lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)"
    apply (simp add: all_total_def totalize_def)
    apply (rule program_equalityI)
      apply (simp_all add: Domain_iff_totalize_act image_def)
    done

    lemma all_total_iff_totalize: "all_total F = (totalize F = F)"
    apply (rule iffI)
     apply (erule all_total_imp_totalize)
    apply (erule subst)
    apply (rule all_total_totalize)
    done

    lemma mk_total_program_constrains_iff [simp]:
         "(mk_total_program args ∈ A co B) = (mk_program args ∈ A co B)"
    by (simp add: mk_total_program_def)

    subsection{*Rules for Lazy Definition Expansion*}

    text{*They avoid expanding the full program, which is a large expression*}

    lemma def_prg_Init:
         "F == mk_total_program (init,acts,allowed) ==> Init F = init"
    by (simp add: mk_total_program_def)

    lemma def_prg_Acts:
         "F == mk_total_program (init,acts,allowed)
          ==> Acts F = insert Id (totalize_act ` acts)"
    by (simp add: mk_total_program_def)

    lemma def_prg_AllowedActs:
         "F == mk_total_program (init,acts,allowed)
          ==> AllowedActs F = insert Id allowed"
    by (simp add: mk_total_program_def)

    text{*An action is expanded if a pair of states is being tested against it*}
    lemma def_act_simp:
         "act == {(s,s'). P s s'} ==> ((s,s') ∈ act) = P s s'"
    by (simp add: mk_total_program_def)

    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 (simp add: mk_total_program_def)

    subsubsection{*Inspectors for type "program"*}

    lemma Init_total_eq [simp]:
         "Init (mk_total_program (init,acts,allowed)) = init"
    by (simp add: mk_total_program_def)

    lemma Acts_total_eq [simp]:
        "Acts(mk_total_program(init,acts,allowed)) = insert Id (totalize_act`acts)"
    by (simp add: mk_total_program_def)

    lemma AllowedActs_total_eq [simp]:
         "AllowedActs (mk_total_program (init,acts,allowed)) = insert Id allowed"
    by (auto simp add: mk_total_program_def)

    end

#### The abstract type of programs

lemmas program_typedef:

      Rep_Program x ∈ Program

      Abs_Program (Rep_Program x) = x

      y ∈ Program ==> Rep_Program (Abs_Program y) = y

      Program == {(init, acts, allowed). Id ∈ acts ∧ Id ∈ allowed}

      Init F == (%(init, acts, allowed). init) (Rep_Program F)

      Acts F == (%(init, acts, allowed). acts) (Rep_Program F)

      AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)

      mk_program ==
      %(init, acts, allowed). Abs_Program (init, insert Id acts, insert Id allowed)

lemmas program_typedef:

      Rep_Program x ∈ Program

      Abs_Program (Rep_Program x) = x

      y ∈ Program ==> Rep_Program (Abs_Program y) = y

      Program == {(init, acts, allowed). Id ∈ acts ∧ Id ∈ allowed}

      Init F == (%(init, acts, allowed). init) (Rep_Program F)

      Acts F == (%(init, acts, allowed). acts) (Rep_Program F)

      AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)

      mk_program ==
      %(init, acts, allowed). Abs_Program (init, insert Id acts, insert Id allowed)

lemma Id_in_Acts:

      Id ∈ Acts F

lemma insert_Id_Acts:

      insert Id (Acts F) = Acts F

lemma Acts_nonempty:

      Acts F ≠ {}

lemma Id_in_AllowedActs:

      Id ∈ AllowedActs F

lemma insert_Id_AllowedActs:

      insert Id (AllowedActs F) = AllowedActs F

#### Inspectors for type "program"

lemma Init_eq:

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

lemma Acts_eq:

      Acts (mk_program (init, acts, allowed)) = insert Id acts

lemma AllowedActs_eq:

      AllowedActs (mk_program (init, acts, allowed)) = insert Id allowed

#### Equality for UNITY programs

lemma surjective_mk_program:

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

lemma program_equalityI:

      [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] ==> 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 = G) = (Init F = Init G ∧ Acts F = Acts G ∧ AllowedActs F = AllowedActs G)

#### co

lemma constrainsI:

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

lemma constrainsD:

      [| F ∈ A co A'; act ∈ Acts F; (s, s') ∈ act; s ∈ A |] ==> s' ∈ A'

lemma constrains_empty:

      F ∈ {} co B

lemma constrains_empty2:

      (F ∈ A co {}) = (A = {})

lemma constrains_UNIV:

      (F ∈ UNIV co B) = (B = UNIV)

lemma constrains_UNIV2:

      F ∈ A co UNIV

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'

#### 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 ∈ (UN i:I. A i) co (UN i:I. A' i)

lemma constrains_Un_distrib:

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

lemma constrains_UN_distrib:

      (UN i:I. A i) co B = (INT i:I. A i co B)

lemma constrains_Int_distrib:

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

lemma constrains_INT_distrib:

      A co (INT i:I. B i) = (INT i:I. A co B i)

#### Intersection

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 ∈ (INT i:I. A i) co (INT i:I. A' i)

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'

#### unless

lemma unlessI:

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

lemma unlessD:

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

#### stable

lemma stableI:

      F ∈ A co A ==> F ∈ stable A

lemma stableD:

      F ∈ stable A ==> F ∈ A co A

lemma stable_UNIV:

      stable UNIV = UNIV

#### Union

lemma stable_Un:

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

lemma stable_UN:

      (!!i. i ∈ I ==> F ∈ stable (A i)) ==> F ∈ stable (UN i:I. A i)

lemma stable_Union:

      (!!A. A ∈ X ==> F ∈ stable A) ==> F ∈ stable (Union X)

#### Intersection

lemma stable_Int:

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

lemma stable_INT:

      (!!i. i ∈ I ==> F ∈ stable (A i)) ==> F ∈ stable (INT i:I. A i)

lemma stable_Inter:

      (!!A. A ∈ X ==> F ∈ stable A) ==> F ∈ stable (Inter X)

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)

#### invariant

lemma invariantI:

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

lemma invariant_Int:

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

#### increasing

lemma increasingD:

      F ∈ increasing f ==> F ∈ stable {s. z ⊆ f s}

lemma increasing_constant:

      F ∈ increasing (%s. c)

lemma mono_increasing_o:

      mono g ==> increasing f ⊆ increasing (g o f)

lemma strict_increasingD:

      F ∈ increasing f ==> F ∈ stable {s. z < f s}

lemma elimination:

      ∀m∈M. F ∈ {s. s x = m} co B m ==> F ∈ {s. s x ∈ M} co (UN m:M. B m)

lemma elimination_sing:

      ∀m∈M. F ∈ {m} co B m ==> F ∈ M co (UN m:M. B m)

#### Theoretical Results from Section 6

lemma constrains_strongest_rhs:

      F ∈ A co strongest_rhs F A

lemma strongest_rhs_is_strongest:

      F ∈ A co B ==> strongest_rhs F A ⊆ B

#### Ad-hoc set-theory rules

lemma Un_Diff_Diff:

      A ∪ B - (A - B) = B

lemma Int_Union_Union:

      Union B ∩ A = Union ((%C. C ∩ A) ` B)

lemma Image_less_than:

      less_than `` {k} = {k<..}

lemma Image_inverse_less_than:

      less_than^-1 `` {k} = {..<k}

### Partial versus Total Transitions

lemma insert_Id_image_Acts:

      f Id = Id ==> insert Id (f ` Acts F) = f ` Acts F

#### Basic properties

lemma totalize_act_Id:

      totalize_act Id = Id

lemma Domain_totalize_act:

      Domain (totalize_act act) = UNIV

lemma Init_totalize:

      Init (totalize F) = Init F

lemma Acts_totalize:

      Acts (totalize F) = totalize_act ` Acts F

lemma AllowedActs_totalize:

      AllowedActs (totalize F) = AllowedActs F

lemma totalize_constrains_iff:

      (totalize F ∈ A co B) = (F ∈ A co B)

lemma totalize_stable_iff:

      (totalize F ∈ stable A) = (F ∈ stable A)

lemma totalize_invariant_iff:

      (totalize F ∈ invariant A) = (F ∈ invariant A)

lemma all_total_totalize:

      all_total (totalize F)

lemma Domain_iff_totalize_act:

      (Domain act = UNIV) = (totalize_act act = act)

lemma all_total_imp_totalize:

      all_total F ==> totalize F = F

lemma all_total_iff_totalize:

      all_total F = (totalize F = F)

lemma mk_total_program_constrains_iff:

      (mk_total_program args ∈ A co B) = (mk_program args ∈ A co B)

### Rules for Lazy Definition Expansion

lemma def_prg_Init:

      F == mk_total_program (init, acts, allowed) ==> Init F = init

lemma def_prg_Acts:

      F == mk_total_program (init, acts, allowed)
      ==> Acts F = insert Id (totalize_act ` acts)

lemma def_prg_AllowedActs:

      F == mk_total_program (init, acts, allowed)
      ==> AllowedActs F = insert Id allowed

lemma def_act_simp:

      act == {(s, s'). P s s'} ==> ((s, s') ∈ act) = P s s'

lemma def_set_simp:

      A == B ==> (x ∈ A) = (x ∈ B)

#### Inspectors for type "program"

lemma Init_total_eq:

      Init (mk_total_program (init, acts, allowed)) = init

lemma Acts_total_eq:

      Acts (mk_total_program (init, acts, allowed)) = insert Id (totalize_act ` acts)

lemma AllowedActs_total_eq:

      AllowedActs (mk_total_program (init, acts, allowed)) = insert Id allowed