(* Title: ZF/UNITY/Union.thy ID: $Id: Union.thy,v 1.8 2005/06/17 14:15:11 haftmann Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge Unions of programs Partly from Misra's Chapter 5: Asynchronous Compositions of Programs Theory ported form HOL.. *) theory Union imports SubstAx FP begin constdefs (*FIXME: conjoin Init(F) Int Init(G) \ 0 *) ok :: "[i, i] => o" (infixl "ok" 65) "F ok G == Acts(F) \ AllowedActs(G) & Acts(G) \ AllowedActs(F)" (*FIXME: conjoin (\i \ I. Init(F(i))) \ 0 *) OK :: "[i, i=>i] => o" "OK(I,F) == (\i \ I. \j \ I-{i}. Acts(F(i)) \ AllowedActs(F(j)))" JOIN :: "[i, i=>i] => i" "JOIN(I,F) == if I = 0 then SKIP else mk_program(\i \ I. Init(F(i)), \i \ I. Acts(F(i)), \i \ I. AllowedActs(F(i)))" Join :: "[i, i] => i" (infixl "Join" 65) "F Join G == mk_program (Init(F) Int Init(G), Acts(F) Un Acts(G), AllowedActs(F) Int AllowedActs(G))" (*Characterizes safety properties. Used with specifying AllowedActs*) safety_prop :: "i => o" "safety_prop(X) == X\program & SKIP \ X & (\G \ program. Acts(G) \ (\F \ X. Acts(F)) --> G \ X)" syntax "@JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10) "@JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10) translations "JN x:A. B" == "JOIN(A, (%x. B))" "JN x y. B" == "JN x. JN y. B" "JN x. B" == "JOIN(state,(%x. B))" syntax (symbols) SKIP :: i ("\") Join :: "[i, i] => i" (infixl "\" 65) "@JOIN1" :: "[pttrns, i] => i" ("(3\ _./ _)" 10) "@JOIN" :: "[pttrn, i, i] => i" ("(3\ _ \ _./ _)" 10) subsection{*SKIP*} lemma reachable_SKIP [simp]: "reachable(SKIP) = state" by (force elim: reachable.induct intro: reachable.intros) text{*Elimination programify from ok and Join*} lemma ok_programify_left [iff]: "programify(F) ok G <-> F ok G" by (simp add: ok_def) lemma ok_programify_right [iff]: "F ok programify(G) <-> F ok G" by (simp add: ok_def) lemma Join_programify_left [simp]: "programify(F) Join G = F Join G" by (simp add: Join_def) lemma Join_programify_right [simp]: "F Join programify(G) = F Join G" by (simp add: Join_def) subsection{*SKIP and safety properties*} lemma SKIP_in_constrains_iff [iff]: "(SKIP \ A co B) <-> (A\B & st_set(A))" by (unfold constrains_def st_set_def, auto) lemma SKIP_in_Constrains_iff [iff]: "(SKIP \ A Co B)<-> (state Int A\B)" by (unfold Constrains_def, auto) lemma SKIP_in_stable [iff]: "SKIP \ stable(A) <-> st_set(A)" by (auto simp add: stable_def) lemma SKIP_in_Stable [iff]: "SKIP \ Stable(A)" by (unfold Stable_def, auto) subsection{*Join and JOIN types*} lemma Join_in_program [iff,TC]: "F Join G \ program" by (unfold Join_def, auto) lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \ program" by (unfold JOIN_def, auto) subsection{*Init, Acts, and AllowedActs of Join and JOIN*} lemma Init_Join [simp]: "Init(F Join G) = Init(F) Int Init(G)" by (simp add: Int_assoc Join_def) lemma Acts_Join [simp]: "Acts(F Join G) = Acts(F) Un Acts(G)" by (simp add: Int_Un_distrib2 cons_absorb Join_def) lemma AllowedActs_Join [simp]: "AllowedActs(F Join G) = AllowedActs(F) Int AllowedActs(G)" apply (simp add: Int_assoc cons_absorb Join_def) done subsection{*Join's algebraic laws*} lemma Join_commute: "F Join G = G Join F" by (simp add: Join_def Un_commute Int_commute) lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)" apply (simp add: Join_def Int_Un_distrib2 cons_absorb) apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb) done lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)" by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2) subsection{*Needed below*} lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)" by auto lemma Join_SKIP_left [simp]: "SKIP Join F = programify(F)" apply (unfold Join_def SKIP_def) apply (auto simp add: Int_absorb cons_eq) done lemma Join_SKIP_right [simp]: "F Join SKIP = programify(F)" apply (subst Join_commute) apply (simp add: Join_SKIP_left) done lemma Join_absorb [simp]: "F Join F = programify(F)" by (rule program_equalityI, auto) lemma Join_left_absorb: "F Join (F Join G) = F Join G" by (simp add: Join_assoc [symmetric]) subsection{*Join is an AC-operator*} lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute subsection{*Eliminating programify form JN and OK expressions*} lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) <-> OK(I, F)" by (simp add: OK_def) lemma JN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)" by (simp add: JOIN_def) subsection{*JN*} lemma JN_empty [simp]: "JOIN(0, F) = SKIP" by (unfold JOIN_def, auto) lemma Init_JN [simp]: "Init(\i \ I. F(i)) = (if I=0 then state else (\i \ I. Init(F(i))))" by (simp add: JOIN_def INT_extend_simps del: INT_simps) lemma Acts_JN [simp]: "Acts(JOIN(I,F)) = cons(id(state), \i \ I. Acts(F(i)))" apply (unfold JOIN_def) apply (auto simp del: INT_simps UN_simps) apply (rule equalityI) apply (auto dest: Acts_type [THEN subsetD]) done lemma AllowedActs_JN [simp]: "AllowedActs(\i \ I. F(i)) = (if I=0 then Pow(state*state) else (\i \ I. AllowedActs(F(i))))" apply (unfold JOIN_def, auto) apply (rule equalityI) apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD]) done lemma JN_cons [simp]: "(\i \ cons(a,I). F(i)) = F(a) Join (\i \ I. F(i))" by (rule program_equalityI, auto) lemma JN_cong [cong]: "[| I=J; !!i. i \ J ==> F(i) = G(i) |] ==> (\i \ I. F(i)) = (\i \ J. G(i))" by (simp add: JOIN_def) subsection{*JN laws*} lemma JN_absorb: "k \ I ==>F(k) Join (\i \ I. F(i)) = (\i \ I. F(i))" apply (subst JN_cons [symmetric]) apply (auto simp add: cons_absorb) done lemma JN_Un: "(\i \ I Un J. F(i)) = ((\i \ I. F(i)) Join (\i \ J. F(i)))" apply (rule program_equalityI) apply (simp_all add: UN_Un INT_Un) apply (simp_all del: INT_simps add: INT_extend_simps, blast) done lemma JN_constant: "(\i \ I. c) = (if I=0 then SKIP else programify(c))" by (rule program_equalityI, auto) lemma JN_Join_distrib: "(\i \ I. F(i) Join G(i)) = (\i \ I. F(i)) Join (\i \ I. G(i))" apply (rule program_equalityI) apply (simp_all add: INT_Int_distrib, blast) done lemma JN_Join_miniscope: "(\i \ I. F(i) Join G) = ((\i \ I. F(i) Join G))" by (simp add: JN_Join_distrib JN_constant) text{*Used to prove guarantees_JN_I*} lemma JN_Join_diff: "i \ I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)" apply (rule program_equalityI) apply (auto elim!: not_emptyE) done subsection{*Safety: co, stable, FP*} (*Fails if I=0 because it collapses to SKIP \ A co B, i.e. to A\B. So an alternative precondition is A\B, but most proofs using this rule require I to be nonempty for other reasons anyway.*) lemma JN_constrains: "i \ I==>(\i \ I. F(i)) \ A co B <-> (\i \ I. programify(F(i)) \ A co B)" apply (unfold constrains_def JOIN_def st_set_def, auto) prefer 2 apply blast apply (rename_tac j act y z) apply (cut_tac F = "F (j) " in Acts_type) apply (drule_tac x = act in bspec, auto) done lemma Join_constrains [iff]: "(F Join G \ A co B) <-> (programify(F) \ A co B & programify(G) \ A co B)" by (auto simp add: constrains_def) lemma Join_unless [iff]: "(F Join G \ A unless B) <-> (programify(F) \ A unless B & programify(G) \ A unless B)" by (simp add: Join_constrains unless_def) (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. reachable (F Join G) could be much bigger than reachable F, reachable G *) lemma Join_constrains_weaken: "[| F \ A co A'; G \ B co B' |] ==> F Join G \ (A Int B) co (A' Un B')" apply (subgoal_tac "st_set (A) & st_set (B) & F \ program & G \ program") prefer 2 apply (blast dest: constrainsD2, simp) apply (blast intro: constrains_weaken) done (*If I=0, it degenerates to SKIP \ state co 0, which is false.*) lemma JN_constrains_weaken: assumes major: "(!!i. i \ I ==> F(i) \ A(i) co A'(i))" and minor: "i \ I" shows "(\i \ I. F(i)) \ (\i \ I. A(i)) co (\i \ I. A'(i))" apply (cut_tac minor) apply (simp (no_asm_simp) add: JN_constrains) apply clarify apply (rename_tac "j") apply (frule_tac i = j in major) apply (frule constrainsD2, simp) apply (blast intro: constrains_weaken) done lemma JN_stable: "(\i \ I. F(i)) \ stable(A) <-> ((\i \ I. programify(F(i)) \ stable(A)) & st_set(A))" apply (auto simp add: stable_def constrains_def JOIN_def) apply (cut_tac F = "F (i) " in Acts_type) apply (drule_tac x = act in bspec, auto) done lemma initially_JN_I: assumes major: "(!!i. i \ I ==>F(i) \ initially(A))" and minor: "i \ I" shows "(\i \ I. F(i)) \ initially(A)" apply (cut_tac minor) apply (auto elim!: not_emptyE simp add: Inter_iff initially_def) apply (frule_tac i = x in major) apply (auto simp add: initially_def) done lemma invariant_JN_I: assumes major: "(!!i. i \ I ==> F(i) \ invariant(A))" and minor: "i \ I" shows "(\i \ I. F(i)) \ invariant(A)" apply (cut_tac minor) apply (auto intro!: initially_JN_I dest: major simp add: invariant_def JN_stable) apply (erule_tac V = "i \ I" in thin_rl) apply (frule major) apply (drule_tac [2] major) apply (auto simp add: invariant_def) apply (frule stableD2, force)+ done lemma Join_stable [iff]: " (F Join G \ stable(A)) <-> (programify(F) \ stable(A) & programify(G) \ stable(A))" by (simp add: stable_def) lemma initially_JoinI [intro!]: "[| F \ initially(A); G \ initially(A) |] ==> F Join G \ initially(A)" by (unfold initially_def, auto) lemma invariant_JoinI: "[| F \ invariant(A); G \ invariant(A) |] ==> F Join G \ invariant(A)" apply (subgoal_tac "F \ program&G \ program") prefer 2 apply (blast dest: invariantD2) apply (simp add: invariant_def) apply (auto intro: Join_in_program) done (* Fails if I=0 because \i \ 0. A(i) = 0 *) lemma FP_JN: "i \ I ==> FP(\i \ I. F(i)) = (\i \ I. FP (programify(F(i))))" by (auto simp add: FP_def Inter_def st_set_def JN_stable) subsection{*Progress: transient, ensures*} lemma JN_transient: "i \ I ==> (\i \ I. F(i)) \ transient(A) <-> (\i \ I. programify(F(i)) \ transient(A))" apply (auto simp add: transient_def JOIN_def) apply (unfold st_set_def) apply (drule_tac [2] x = act in bspec) apply (auto dest: Acts_type [THEN subsetD]) done lemma Join_transient [iff]: "F Join G \ transient(A) <-> (programify(F) \ transient(A) | programify(G) \ transient(A))" apply (auto simp add: transient_def Join_def Int_Un_distrib2) done lemma Join_transient_I1: "F \ transient(A) ==> F Join G \ transient(A)" by (simp add: Join_transient transientD2) lemma Join_transient_I2: "G \ transient(A) ==> F Join G \ transient(A)" by (simp add: Join_transient transientD2) (*If I=0 it degenerates to (SKIP \ A ensures B) = False, i.e. to ~(A\B) *) lemma JN_ensures: "i \ I ==> (\i \ I. F(i)) \ A ensures B <-> ((\i \ I. programify(F(i)) \ (A-B) co (A Un B)) & (\i \ I. programify(F(i)) \ A ensures B))" by (auto simp add: ensures_def JN_constrains JN_transient) lemma Join_ensures: "F Join G \ A ensures B <-> (programify(F) \ (A-B) co (A Un B) & programify(G) \ (A-B) co (A Un B) & (programify(F) \ transient (A-B) | programify(G) \ transient (A-B)))" apply (unfold ensures_def) apply (auto simp add: Join_transient) done lemma stable_Join_constrains: "[| F \ stable(A); G \ A co A' |] ==> F Join G \ A co A'" apply (unfold stable_def constrains_def Join_def st_set_def) apply (cut_tac F = F in Acts_type) apply (cut_tac F = G in Acts_type, force) done (*Premise for G cannot use Always because F \ Stable A is weaker than G \ stable A *) lemma stable_Join_Always1: "[| F \ stable(A); G \ invariant(A) |] ==> F Join G \ Always(A)" apply (subgoal_tac "F \ program & G \ program & st_set (A) ") prefer 2 apply (blast dest: invariantD2 stableD2) apply (simp add: Always_def invariant_def initially_def Stable_eq_stable) apply (force intro: stable_Int) done (*As above, but exchanging the roles of F and G*) lemma stable_Join_Always2: "[| F \ invariant(A); G \ stable(A) |] ==> F Join G \ Always(A)" apply (subst Join_commute) apply (blast intro: stable_Join_Always1) done lemma stable_Join_ensures1: "[| F \ stable(A); G \ A ensures B |] ==> F Join G \ A ensures B" apply (subgoal_tac "F \ program & G \ program & st_set (A) ") prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD]) apply (simp (no_asm_simp) add: Join_ensures) apply (simp add: stable_def ensures_def) apply (erule constrains_weaken, auto) done (*As above, but exchanging the roles of F and G*) lemma stable_Join_ensures2: "[| F \ A ensures B; G \ stable(A) |] ==> F Join G \ A ensures B" apply (subst Join_commute) apply (blast intro: stable_Join_ensures1) done subsection{*The ok and OK relations*} lemma ok_SKIP1 [iff]: "SKIP ok F" by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) lemma ok_SKIP2 [iff]: "F ok SKIP" by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) lemma ok_Join_commute: "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))" by (auto simp add: ok_def) lemma ok_commute: "(F ok G) <->(G ok F)" by (auto simp add: ok_def) lemmas ok_sym = ok_commute [THEN iffD1, standard] lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)" by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb Int_Un_distrib2 Ball_def, safe, force+) lemma ok_Join_iff1 [iff]: "F ok (G Join H) <-> (F ok G & F ok H)" by (auto simp add: ok_def) lemma ok_Join_iff2 [iff]: "(G Join H) ok F <-> (G ok F & H ok F)" by (auto simp add: ok_def) (*useful? Not with the previous two around*) lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)" by (auto simp add: ok_def) lemma ok_JN_iff1 [iff]: "F ok JOIN(I,G) <-> (\i \ I. F ok G(i))" by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def) lemma ok_JN_iff2 [iff]: "JOIN(I,G) ok F <-> (\i \ I. G(i) ok F)" apply (auto elim!: not_emptyE simp add: ok_def) apply (blast dest: Acts_type [THEN subsetD]) done lemma OK_iff_ok: "OK(I,F) <-> (\i \ I. \j \ I-{i}. F(i) ok (F(j)))" by (auto simp add: ok_def OK_def) lemma OK_imp_ok: "[| OK(I,F); i \ I; j \ I; i\j|] ==> F(i) ok F(j)" by (auto simp add: OK_iff_ok) lemma OK_0 [iff]: "OK(0,F)" by (simp add: OK_def) lemma OK_cons_iff: "OK(cons(i, I), F) <-> (i \ I & OK(I, F)) | (i\I & OK(I, F) & F(i) ok JOIN(I,F))" apply (simp add: OK_iff_ok) apply (blast intro: ok_sym) done subsection{*Allowed*} lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program" by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def) lemma Allowed_Join [simp]: "Allowed(F Join G) = Allowed(programify(F)) Int Allowed(programify(G))" apply (auto simp add: Allowed_def) done lemma Allowed_JN [simp]: "i \ I ==> Allowed(JOIN(I,F)) = (\i \ I. Allowed(programify(F(i))))" apply (auto simp add: Allowed_def, blast) done lemma ok_iff_Allowed: "F ok G <-> (programify(F) \ Allowed(programify(G)) & programify(G) \ Allowed(programify(F)))" by (simp add: ok_def Allowed_def) lemma OK_iff_Allowed: "OK(I,F) <-> (\i \ I. \j \ I-{i}. programify(F(i)) \ Allowed(programify(F(j))))" apply (auto simp add: OK_iff_ok ok_iff_Allowed) done subsection{*safety_prop, for reasoning about given instances of "ok"*} lemma safety_prop_Acts_iff: "safety_prop(X) ==> (Acts(G) \ cons(id(state), (\F \ X. Acts(F)))) <-> (programify(G) \ X)" apply (simp (no_asm_use) add: safety_prop_def) apply clarify apply (case_tac "G \ program", simp_all, blast, safe) prefer 2 apply force apply (force simp add: programify_def) done lemma safety_prop_AllowedActs_iff_Allowed: "safety_prop(X) ==> (\G \ X. Acts(G)) \ AllowedActs(F) <-> (X \ Allowed(programify(F)))" apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym] safety_prop_def, blast) done lemma Allowed_eq: "safety_prop(X) ==> Allowed(mk_program(init, acts, \F \ X. Acts(F))) = X" apply (subgoal_tac "cons (id (state), Union (RepFun (X, Acts)) Int Pow (state * state)) = Union (RepFun (X, Acts))") apply (rule_tac [2] equalityI) apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto) apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+ done lemma def_prg_Allowed: "[| F == mk_program (init, acts, \F \ X. Acts(F)); safety_prop(X) |] ==> Allowed(F) = X" by (simp add: Allowed_eq) (*For safety_prop to hold, the property must be satisfiable!*) lemma safety_prop_constrains [iff]: "safety_prop(A co B) <-> (A \ B & st_set(A))" by (simp add: safety_prop_def constrains_def st_set_def, blast) (* To be used with resolution *) lemma safety_prop_constrainsI [iff]: "[| A\B; st_set(A) |] ==>safety_prop(A co B)" by auto lemma safety_prop_stable [iff]: "safety_prop(stable(A)) <-> st_set(A)" by (simp add: stable_def) lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))" by auto lemma safety_prop_Int [simp]: "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)" apply (simp add: safety_prop_def, safe, blast) apply (drule_tac [2] B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (Y, Acts))" in subset_trans) apply (drule_tac B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (X, Acts))" in subset_trans) apply blast+ done (* If I=0 the conclusion becomes safety_prop(0) which is false *) lemma safety_prop_Inter: assumes major: "(!!i. i \ I ==>safety_prop(X(i)))" and minor: "i \ I" shows "safety_prop(\i \ I. X(i))" apply (simp add: safety_prop_def) apply (cut_tac minor, safe) apply (simp (no_asm_use) add: Inter_iff) apply clarify apply (frule major) apply (drule_tac [2] i = xa in major) apply (frule_tac [4] i = xa in major) apply (auto simp add: safety_prop_def) apply (drule_tac B = "Union (RepFun (Inter (RepFun (I, X)), Acts))" and C = "Union (RepFun (X (xa), Acts))" in subset_trans) apply blast+ done lemma def_UNION_ok_iff: "[| F == mk_program(init,acts, \G \ X. Acts(G)); safety_prop(X) |] ==> F ok G <-> (programify(G) \ X & acts Int Pow(state*state) \ AllowedActs(G))" apply (unfold ok_def) apply (drule_tac G = G in safety_prop_Acts_iff) apply (cut_tac F = G in AllowedActs_type) apply (cut_tac F = G in Acts_type, auto) done ML {* val safety_prop_def = thm "safety_prop_def"; val reachable_SKIP = thm "reachable_SKIP"; val ok_programify_left = thm "ok_programify_left"; val ok_programify_right = thm "ok_programify_right"; val Join_programify_left = thm "Join_programify_left"; val Join_programify_right = thm "Join_programify_right"; val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff"; val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff"; val SKIP_in_stable = thm "SKIP_in_stable"; val SKIP_in_Stable = thm "SKIP_in_Stable"; val Join_in_program = thm "Join_in_program"; val JOIN_in_program = thm "JOIN_in_program"; val Init_Join = thm "Init_Join"; val Acts_Join = thm "Acts_Join"; val AllowedActs_Join = thm "AllowedActs_Join"; val Join_commute = thm "Join_commute"; val Join_left_commute = thm "Join_left_commute"; val Join_assoc = thm "Join_assoc"; val cons_id = thm "cons_id"; val Join_SKIP_left = thm "Join_SKIP_left"; val Join_SKIP_right = thm "Join_SKIP_right"; val Join_absorb = thm "Join_absorb"; val Join_left_absorb = thm "Join_left_absorb"; val OK_programify = thm "OK_programify"; val JN_programify = thm "JN_programify"; val JN_empty = thm "JN_empty"; val Init_JN = thm "Init_JN"; val Acts_JN = thm "Acts_JN"; val AllowedActs_JN = thm "AllowedActs_JN"; val JN_cons = thm "JN_cons"; val JN_cong = thm "JN_cong"; val JN_absorb = thm "JN_absorb"; val JN_Un = thm "JN_Un"; val JN_constant = thm "JN_constant"; val JN_Join_distrib = thm "JN_Join_distrib"; val JN_Join_miniscope = thm "JN_Join_miniscope"; val JN_Join_diff = thm "JN_Join_diff"; val JN_constrains = thm "JN_constrains"; val Join_constrains = thm "Join_constrains"; val Join_unless = thm "Join_unless"; val Join_constrains_weaken = thm "Join_constrains_weaken"; val JN_constrains_weaken = thm "JN_constrains_weaken"; val JN_stable = thm "JN_stable"; val initially_JN_I = thm "initially_JN_I"; val invariant_JN_I = thm "invariant_JN_I"; val Join_stable = thm "Join_stable"; val initially_JoinI = thm "initially_JoinI"; val invariant_JoinI = thm "invariant_JoinI"; val FP_JN = thm "FP_JN"; val JN_transient = thm "JN_transient"; val Join_transient = thm "Join_transient"; val Join_transient_I1 = thm "Join_transient_I1"; val Join_transient_I2 = thm "Join_transient_I2"; val JN_ensures = thm "JN_ensures"; val Join_ensures = thm "Join_ensures"; val stable_Join_constrains = thm "stable_Join_constrains"; val stable_Join_Always1 = thm "stable_Join_Always1"; val stable_Join_Always2 = thm "stable_Join_Always2"; val stable_Join_ensures1 = thm "stable_Join_ensures1"; val stable_Join_ensures2 = thm "stable_Join_ensures2"; val ok_SKIP1 = thm "ok_SKIP1"; val ok_SKIP2 = thm "ok_SKIP2"; val ok_Join_commute = thm "ok_Join_commute"; val ok_commute = thm "ok_commute"; val ok_sym = thm "ok_sym"; val ok_iff_OK = thm "ok_iff_OK"; val ok_Join_iff1 = thm "ok_Join_iff1"; val ok_Join_iff2 = thm "ok_Join_iff2"; val ok_Join_commute_I = thm "ok_Join_commute_I"; val ok_JN_iff1 = thm "ok_JN_iff1"; val ok_JN_iff2 = thm "ok_JN_iff2"; val OK_iff_ok = thm "OK_iff_ok"; val OK_imp_ok = thm "OK_imp_ok"; val Allowed_SKIP = thm "Allowed_SKIP"; val Allowed_Join = thm "Allowed_Join"; val Allowed_JN = thm "Allowed_JN"; val ok_iff_Allowed = thm "ok_iff_Allowed"; val OK_iff_Allowed = thm "OK_iff_Allowed"; val safety_prop_Acts_iff = thm "safety_prop_Acts_iff"; val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed"; val Allowed_eq = thm "Allowed_eq"; val def_prg_Allowed = thm "def_prg_Allowed"; val safety_prop_constrains = thm "safety_prop_constrains"; val safety_prop_constrainsI = thm "safety_prop_constrainsI"; val safety_prop_stable = thm "safety_prop_stable"; val safety_prop_stableI = thm "safety_prop_stableI"; val safety_prop_Int = thm "safety_prop_Int"; val safety_prop_Inter = thm "safety_prop_Inter"; val def_UNION_ok_iff = thm "def_UNION_ok_iff"; val Join_ac = thms "Join_ac"; *} end