(* 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
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
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
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)
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'
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)
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'
lemma unlessI:
F ∈ A - B co A ∪ B ==> F ∈ A unless B
lemma unlessD:
F ∈ A unless B ==> F ∈ A - B co A ∪ B
lemma stableI:
F ∈ A co A ==> F ∈ stable A
lemma stableD:
F ∈ stable A ==> F ∈ A co A
lemma stable_UNIV:
stable UNIV = UNIV
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)
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)
lemma invariantI:
[| Init F ⊆ A; F ∈ stable A |] ==> F ∈ invariant A
lemma invariant_Int:
[| F ∈ invariant A; F ∈ invariant B |] ==> F ∈ invariant (A ∩ B)
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)
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
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}
lemma insert_Id_image_Acts:
f Id = Id ==> insert Id (f ` Acts F) = f ` Acts F
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)
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)
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