--- a/src/ZF/IsaMakefile Wed Aug 08 14:16:42 2001 +0200
+++ b/src/ZF/IsaMakefile Wed Aug 08 14:33:10 2001 +0200
@@ -8,7 +8,9 @@
default: ZF
images: ZF
-test: ZF-IMP ZF-Coind ZF-AC ZF-Resid ZF-ex
+
+#Note: keep targets sorted
+test: ZF-AC ZF-Coind ZF-ex ZF-IMP ZF-Resid ZF-UNITY
all: images test
@@ -52,27 +54,6 @@
@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
-## ZF-IMP
-
-ZF-IMP: ZF $(LOG)/ZF-IMP.gz
-
-$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
- IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML
- @$(ISATOOL) usedir $(OUT)/ZF IMP
-
-
-## ZF-Coind
-
-ZF-Coind: ZF $(LOG)/ZF-Coind.gz
-
-$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
- Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \
- Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \
- Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \
- Coind/Values.thy
- @$(ISATOOL) usedir $(OUT)/ZF Coind
-
-
## ZF-AC
ZF-AC: ZF $(LOG)/ZF-AC.gz
@@ -91,17 +72,16 @@
@$(ISATOOL) usedir $(OUT)/ZF AC
-## ZF-Resid
+## ZF-Coind
-ZF-Resid: ZF $(LOG)/ZF-Resid.gz
+ZF-Coind: ZF $(LOG)/ZF-Coind.gz
-$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \
- Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
- Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
- Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
- Resid/Substitution.ML \
- Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
- @$(ISATOOL) usedir $(OUT)/ZF Resid
+$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
+ Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \
+ Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \
+ Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \
+ Coind/Values.thy
+ @$(ISATOOL) usedir $(OUT)/ZF Coind
## ZF-ex
@@ -122,9 +102,45 @@
@$(ISATOOL) usedir $(OUT)/ZF ex
+## ZF-IMP
+
+ZF-IMP: ZF $(LOG)/ZF-IMP.gz
+
+$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
+ IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML
+ @$(ISATOOL) usedir $(OUT)/ZF IMP
+
+
+## ZF-Resid
+
+ZF-Resid: ZF $(LOG)/ZF-Resid.gz
+
+$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \
+ Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
+ Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
+ Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
+ Resid/Substitution.ML \
+ Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
+ @$(ISATOOL) usedir $(OUT)/ZF Resid
+
+
+## ZF-UNITY
+
+ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz
+
+$(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \
+ UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
+ UNITY/FP.ML UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \
+ UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
+ UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
+ UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
+ UNITY/WFair.ML UNITY/WFair.thy
+ @$(ISATOOL) usedir $(OUT)/ZF UNITY
+
+
## clean
clean:
- @rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-IMP.gz \
- $(LOG)/ZF-Coind.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz \
- $(LOG)/ZF-ex.gz
+ @rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \
+ $(LOG)/ZF-ex.gz $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
+ $(LOG)/ZF-UNITY.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Comp.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,214 @@
+(* Title: ZF/UNITY/Comp.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 1998 University of Cambridge
+Composition
+From Chandy and Sanders, "Reasoning About Program Composition"
+
+Revised by Sidi Ehmety on January 2001
+
+*)
+
+(*** component and strict_component relations ***)
+
+Goalw [component_def]
+ "H component F | H component G ==> H component (F Join G)";
+by Auto_tac;
+by (res_inst_tac [("x", "Ga Join G")] exI 1);
+by (res_inst_tac [("x", "G Join F")] exI 2);
+by (auto_tac (claset(), simpset() addsimps Join_ac));
+qed "componentI";
+
+Goalw [component_def]
+ "G:program ==> (F component G) <-> \
+\ (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))";
+by Auto_tac;
+by (rtac exI 1);
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "component_eq_subset";
+
+
+Goalw [component_def]
+ "F:program ==> SKIP component F";
+by (res_inst_tac [("x", "F")] exI 1);
+by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
+qed "component_SKIP";
+
+
+Goalw [component_def]
+"F:program ==> F component F";
+by (res_inst_tac [("x", "F")] exI 1);
+by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1);
+qed "component_refl";
+
+Addsimps [component_SKIP, component_refl];
+
+Goal "F component SKIP ==> programify(F) = SKIP";
+by (rtac program_equalityI 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_eq_subset])));
+by (Blast_tac 1);
+qed "SKIP_minimal";
+
+
+Goalw [component_def] "F component (F Join G)";
+by (Blast_tac 1);
+qed "component_Join1";
+
+
+Goalw [component_def] "G component (F Join G)";
+by (simp_tac (simpset() addsimps [Join_commute]) 1);
+by (Blast_tac 1);
+qed "component_Join2";
+
+Goal "F component G ==> F Join G = G";
+by (auto_tac (claset(), simpset()
+ addsimps [component_def, Join_left_absorb]));
+qed "Join_absorb1";
+
+Goal "G component F ==> F Join G = F";
+by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
+qed "Join_absorb2";
+
+
+
+Goal "H:program ==> \
+\ (JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)";
+by (case_tac "I=0" 1);
+by (Force_tac 1);
+by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by Auto_tac;
+by (dres_inst_tac [("c", "xb"), ("A", "AllowedActs(H)")] subsetD 2);
+by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1));
+qed "JN_component_iff";
+
+
+Goalw [component_def] "i : I ==> F(i) component (JN i:I. (F(i)))";
+by (blast_tac (claset() addIs [JN_absorb]) 1);
+qed "component_JN";
+
+
+Goalw [component_def] "[| F component G; G component H |] ==> F component H";
+by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
+qed "component_trans";
+
+Goal "[| F:program; G:program |] ==> \
+\ (F component G & G component F) --> F = G";
+by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (Clarify_tac 1);
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "component_antisym";
+
+Goal "H:program ==> ((F Join G) component H) <-> (F component H & G component H)";
+by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (Blast_tac 1);
+qed "Join_component_iff";
+
+
+Goal "[| F component G; G:A co B; F:program |] ==> F : A co B";
+by (forward_tac [constrainsD2] 1);
+by (rotate_tac ~1 1);
+by (auto_tac (claset(),
+ simpset() addsimps [constrains_def, component_eq_subset]));
+qed "component_constrains";
+
+(*Used in Guar.thy to show that programs are partially ordered*)
+(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
+
+
+(*** preserves ***)
+
+val prems =
+Goalw [preserves_def]
+"ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)";
+by Auto_tac;
+by (blast_tac (claset() addDs [stableD2]) 1);
+bind_thm("preservesI", allI RS result());
+
+Goalw [preserves_def, stable_def, constrains_def]
+ "[| F:preserves(f); act : Acts(F); <s,t> : act |] ==> f(s) = f(t)";
+by (subgoal_tac "s:state & t:state" 1);
+by (blast_tac (claset() addSDs [ActsD]) 2);
+by Auto_tac;
+by (dres_inst_tac [("x", "f(s)")] spec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by Auto_tac;
+qed "preserves_imp_eq";
+
+Goalw [preserves_def]
+"(F Join G : preserves(v)) <-> \
+\ (programify(F) : preserves(v) & programify(G) : preserves(v))";
+by (auto_tac (claset(), simpset() addsimps [INT_iff]));
+qed "Join_preserves";
+
+
+Goal "(JOIN(I,F): preserves(v)) <-> (ALL i:I. programify(F(i)):preserves(v))";
+by (auto_tac (claset(), simpset() addsimps
+ [JN_stable, preserves_def, INT_iff]@state_simps));
+qed "JN_preserves";
+
+Goal "SKIP : preserves(v)";
+by (auto_tac (claset(), simpset()
+ addsimps [preserves_def, INT_iff]@state_simps));
+qed "SKIP_preserves";
+
+AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
+
+
+
+
+(** component_of **)
+
+(* component_of is stronger than component *)
+Goalw [component_def, component_of_def]
+"F component_of H ==> F component H";
+by (Blast_tac 1);
+qed "component_of_imp_component";
+
+
+
+(* component_of satisfies many of the <='s properties *)
+Goalw [component_of_def]
+"F:program ==> F component_of F";
+by (res_inst_tac [("x", "SKIP")] exI 1);
+by Auto_tac;
+qed "component_of_refl";
+
+
+
+Goalw [component_of_def]
+"F:program ==>SKIP component_of F";
+by Auto_tac;
+by (res_inst_tac [("x", "F")] exI 1);
+by Auto_tac;
+qed "component_of_SKIP";
+
+Addsimps [component_of_refl, component_of_SKIP];
+
+
+
+Goalw [component_of_def]
+"[| F component_of G; G component_of H |] ==> F component_of H";
+by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
+qed "component_of_trans";
+
+
+(** localize **)
+Goalw [localize_def]
+ "Init(localize(v,F)) = Init(F)";
+by (Simp_tac 1);
+qed "localize_Init_eq";
+
+
+Goalw [localize_def]
+ "Acts(localize(v,F)) = Acts(F)";
+by (Simp_tac 1);
+qed "localize_Acts_eq";
+
+Goalw [localize_def]
+ "AllowedActs(localize(v,F)) = AllowedActs(F Int (UN G:preserves(v). Acts(G)))";
+by Auto_tac;
+qed "localize_AllowedActs_eq";
+
+Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Comp.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,44 @@
+(* Title: ZF/UNITY/Comp.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Composition
+From Chandy and Sanders, "Reasoning About Program Composition",
+Technical Report 2000-003, University of Florida, 2000.
+
+Revised by Sidi Ehmety on January 2001
+
+Added: a strong form of the order relation over component and localize
+
+Theory ported from HOL.
+
+*)
+
+Comp = Union +
+
+constdefs
+
+ component :: [i, i] => o (infixl 65)
+ "F component H == (EX G. F Join G = H)"
+
+ strict_component :: [i, i] => o (infixl "strict'_component" 65)
+ "F strict_component H == F component H & F~=H"
+
+ (* A stronger form of the component relation *)
+ component_of :: "[i,i]=>o" (infixl "component'_of" 65)
+ "F component_of H == (EX G. F ok G & F Join G = H)"
+
+ strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65)
+ "F strict_component_of H == F component_of H & F~=H"
+
+ (* preserves any state function f, in particular a variable *)
+ preserves :: (i=>i)=>i
+ "preserves(f) == {F:program. ALL z. F: stable({s:state. f(s) = z})}"
+
+localize :: "[i=>i, i] => i"
+ "localize(f,F) == mk_program(Init(F), Acts(F),
+ AllowedActs(F Int (UN G:preserves(f). Acts(G))))"
+
+
+ end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Constrains.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,595 @@
+(* Title: ZF/UNITY/Constrains.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Safety relations: restricted to the set of reachable states.
+
+Proofs ported from HOL.
+*)
+
+(*** traces and reachable ***)
+
+Goalw [condition_def]
+ "reachable(F):condition";
+by (auto_tac (claset() addSDs [reachable.dom_subset RS subsetD]
+ addDs [InitD, ActsD], simpset()));
+qed "reachable_type";
+Addsimps [reachable_type];
+AddIs [reachable_type];
+
+Goal "x:reachable(F) ==> x:state";
+by (cut_inst_tac [("F", "F")] reachable_type 1);
+by (auto_tac (claset(), simpset() addsimps [condition_def]));
+qed "reachableD";
+
+Goal "F:program ==> \
+\ reachable(F) = {s:state. EX evs. <s,evs>: traces(Init(F), Acts(F))}";
+by (rtac equalityI 1);
+by Safe_tac;
+by (blast_tac (claset() addDs [reachableD]) 1);
+by (etac traces.induct 2);
+by (etac reachable.induct 1);
+by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
+qed "reachable_equiv_traces";
+
+Goal "Init(F) <= reachable(F)";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Init_into_reachable";
+
+Goal "[| F:program; G:program; \
+\ Acts(G) <= Acts(F) |] ==> G:stable(reachable(F))";
+by (blast_tac (claset()
+ addIs [stableI, constrainsI, reachable_type] @ reachable.intrs) 1);
+qed "stable_reachable";
+
+AddSIs [stable_reachable];
+Addsimps [stable_reachable];
+
+(*The set of all reachable states is an invariant...*)
+Goalw [invariant_def, initially_def]
+ "F:program ==> F:invariant(reachable(F))";
+by (blast_tac (claset() addIs [reachable_type]@reachable.intrs) 1);
+qed "invariant_reachable";
+
+(*...in fact the strongest invariant!*)
+Goal "F : invariant(A) ==> reachable(F) <= A";
+by (full_simp_tac
+ (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
+by (rtac subsetI 1);
+by (etac reachable.induct 1);
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "invariant_includes_reachable";
+
+(*** Co ***)
+
+(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
+val lemma = subset_refl RSN (3, rewrite_rule
+ [stable_def] stable_reachable RS constrains_Int);
+Goal "F:B co B' ==> F: (reachable(F) Int B) co (reachable(F) Int B')";
+by (blast_tac (claset() addSIs [lemma]
+ addDs [constrainsD2]) 1);
+qed "constrains_reachable_Int";
+
+(*Resembles the previous definition of Constrains*)
+Goalw [Constrains_def]
+ "A Co B = \
+\ {F:program. F : (reachable(F) Int A) co (reachable(F) Int B) & \
+\ A:condition & B:condition}";
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (subgoal_tac "reachable(x) Int B:condition" 2);
+by (blast_tac (claset() addDs [constrains_reachable_Int]
+ addIs [constrains_weaken]) 2);
+by (subgoal_tac "reachable(x) Int B:condition" 1);
+by (blast_tac (claset() addDs [constrains_reachable_Int]
+ addIs [constrains_weaken]) 1);
+by (REPEAT(blast_tac (claset() addIs [reachable_type]) 1));
+qed "Constrains_eq_constrains";
+
+Goalw [Constrains_def]
+ "F : A co A' ==> F : A Co A'";
+by (blast_tac (claset() addIs [constrains_weaken_L]
+ addDs [constrainsD2]) 1);
+qed "constrains_imp_Constrains";
+
+Goalw [stable_def, Stable_def]
+"F : stable(A) ==> F : Stable(A)";
+by (etac constrains_imp_Constrains 1);
+qed "stable_imp_Stable";
+
+
+val prems = Goal
+ "[|(!!act s s'. [| act: Acts(F); <s,s'>:act; s:A |] \
+\ ==> s':A'); F:program; A:condition; A':condition |] ==> F:A Co A'";
+by (rtac constrains_imp_Constrains 1);
+by (blast_tac (claset() addIs (constrainsI::prems)) 1);
+qed "ConstrainsI";
+
+Goalw [Constrains_def]
+ "F:A Co B ==> F:program & A:condition & B:condition";
+by (Blast_tac 1);
+qed "ConstrainsD";
+
+Goal "[| F:program; B:condition |] ==> F : 0 Co B";
+by (blast_tac (claset() addIs
+ [constrains_imp_Constrains, constrains_empty]) 1);
+qed "Constrains_empty";
+
+Goal "[| F:program; A:condition |] ==> F : A Co state";
+by (blast_tac (claset() addIs
+ [constrains_imp_Constrains, constrains_state2]) 1);
+qed "Constrains_state";
+Addsimps [Constrains_empty, Constrains_state];
+
+val Constrains_def2 = Constrains_eq_constrains RS eq_reflection;
+
+Goalw [Constrains_def2]
+ "[| F : A Co A'; A'<=B'; B':condition |] ==> F : A Co B'";
+by (Clarify_tac 1);
+by (blast_tac (claset()
+ addIs [reachable_type, constrains_weaken_R]) 1);
+qed "Constrains_weaken_R";
+
+
+Goalw [condition_def]
+ "[| A<=B; B:condition |] ==>A:condition";
+by (Blast_tac 1);
+qed "condition_subset_mono";
+
+
+Goalw [Constrains_def2]
+ "[| F : A Co A'; B<=A |] ==> F : B Co A'";
+by (Clarify_tac 1);
+by (forward_tac [condition_subset_mono] 1);
+by (assume_tac 1);
+by (blast_tac (claset()
+ addIs [reachable_type, constrains_weaken_L]) 1);
+qed "Constrains_weaken_L";
+
+Goalw [Constrains_def]
+ "[| F : A Co A'; B<=A; A'<=B'; B':condition |] ==> F : B Co B'";
+by (Clarify_tac 1);
+by (forward_tac [condition_subset_mono] 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [reachable_type, constrains_weaken]) 1);
+qed "Constrains_weaken";
+
+(** Union **)
+
+Goalw [Constrains_def2]
+ "[| F : A Co A'; F : B Co B' |] \
+\ ==> F : (A Un B) Co (A' Un B')";
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1);
+by (blast_tac (claset() addIs [constrains_Un]) 1);
+qed "Constrains_Un";
+
+Goalw [Constrains_def2]
+ "[| F:program; \
+\ ALL i:I. F : A(i) Co A'(i) |] \
+\ ==> F : (UN i:I. A(i)) Co (UN i:I. A'(i))";
+by (rtac CollectI 1);
+by Safe_tac;
+by (simp_tac (simpset() addsimps [Int_UN_distrib]) 1);
+by (blast_tac (claset() addIs [constrains_UN, CollectD2 RS conjunct1]) 1);
+by (rewrite_goals_tac [condition_def]);
+by (ALLGOALS(Blast_tac));
+qed "Constrains_UN";
+
+(** Intersection **)
+
+Goal "A Int (B Int C) = (A Int B) Int (A Int C)";
+by (Blast_tac 1);
+qed "Int_duplicate";
+
+Goalw [Constrains_def]
+ "[| F : A Co A'; F : B Co B' |] \
+\ ==> F : (A Int B) Co (A' Int B')";
+by (Step_tac 1);
+by (subgoal_tac "reachable(F) Int (A Int B) = \
+ \ (reachable(F) Int A) Int (reachable(F) Int B)" 1);
+by (Blast_tac 2);
+by (Asm_simp_tac 1);
+by (rtac constrains_Int 1);
+by (ALLGOALS(Asm_simp_tac));
+qed "Constrains_Int";
+
+Goal
+ "[| F:program; \
+\ ALL i:I. F: A(i) Co A'(i) |] \
+\ ==> F : (INT i:I. A(i)) Co (INT i:I. A'(i))";
+by (case_tac "I=0" 1);
+by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
+by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1);
+by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 2);
+by (Blast_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
+by (Step_tac 1);
+by (rtac constrains_INT 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (ALLGOALS(Blast_tac));
+qed "Constrains_INT";
+
+Goal "F : A Co A' ==> reachable(F) Int A <= A'";
+by (asm_full_simp_tac (simpset() addsimps
+ [Constrains_def, reachable_type]) 1);
+by (blast_tac (claset() addDs [constrains_imp_subset]) 1);
+qed "Constrains_imp_subset";
+
+Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C";
+by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
+qed "Constrains_trans";
+
+Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
+by (full_simp_tac (simpset()
+ addsimps [Constrains_eq_constrains, Int_Un_distrib2 RS sym]) 1);
+by (Step_tac 1);
+by (blast_tac (claset() addIs [constrains_cancel]) 1);
+qed "Constrains_cancel";
+
+(*** Stable ***)
+
+(*Useful because there's no Stable_weaken. [Tanja Vos]*)
+Goal "[| F: Stable(A); A = B |] ==> F : Stable(B)";
+by (Blast_tac 1);
+qed "Stable_eq";
+
+Goal "A:condition ==> F : Stable(A) <-> (F : stable(reachable(F) Int A))";
+by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains,
+ stable_def]) 1);
+by (blast_tac (claset() addDs [constrainsD2]) 1);
+qed "Stable_eq_stable";
+
+Goalw [Stable_def] "F : A Co A ==> F : Stable(A)";
+by (assume_tac 1);
+qed "StableI";
+
+Goalw [Stable_def] "F : Stable(A) ==> F : A Co A";
+by (assume_tac 1);
+qed "StableD";
+
+Goalw [Stable_def]
+ "[| F : Stable(A); F : Stable(A') |] ==> F : Stable(A Un A')";
+by (blast_tac (claset() addIs [Constrains_Un]) 1);
+qed "Stable_Un";
+
+Goalw [Stable_def]
+ "[| F : Stable(A); F : Stable(A') |] ==> F : Stable (A Int A')";
+by (blast_tac (claset() addIs [Constrains_Int]) 1);
+qed "Stable_Int";
+
+Goalw [Stable_def]
+ "[| F : Stable(C); F : A Co (C Un A') |] \
+\ ==> F : (C Un A) Co (C Un A')";
+by (subgoal_tac "C Un A' :condition & C Un A:condition" 1);
+by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1);
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+qed "Stable_Constrains_Un";
+
+
+Goalw [Stable_def]
+ "[| F : Stable(C); F : (C Int A) Co A' |] \
+\ ==> F : (C Int A) Co (C Int A')";
+by (blast_tac (claset() addDs [ConstrainsD]
+ addIs [Constrains_Int RS Constrains_weaken]) 1);
+qed "Stable_Constrains_Int";
+
+val [major, prem] = Goalw [Stable_def]
+ "[| F:program; \
+\ (!!i. i:I ==> F : Stable(A(i))) |]==> F : Stable (UN i:I. A(i))";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addIs [major, Constrains_UN, prem]) 1);
+qed "Stable_UN";
+
+val [major, prem] = Goalw [Stable_def]
+ "[| F:program; \
+\ (!!i. i:I ==> F:Stable(A(i))) |]==> F : Stable (INT i:I. A(i))";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addIs [major, Constrains_INT, prem]) 1);
+qed "Stable_INT";
+
+Goal "F:program ==>F : Stable (reachable(F))";
+by (asm_simp_tac (simpset()
+ addsimps [Stable_eq_stable, Int_absorb, subset_refl]) 1);
+qed "Stable_reachable";
+
+Goalw [Stable_def]
+"F:Stable(A) ==> F:program & A:condition";
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+qed "StableD2";
+
+(*** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of ALL m ? Would make it harder to use
+ in forward proof. ***)
+
+Goalw [condition_def]
+ "Collect(state,P):condition";
+by Auto_tac;
+qed "Collect_in_condition";
+AddIffs [Collect_in_condition];
+
+Goalw [Constrains_def]
+ "[| ALL m:M. F : {s:S. x(s) = m} Co B(m); F:program |] \
+\ ==> F : {s:S. x(s):M} Co (UN m:M. B(m))";
+by Safe_tac;
+by (res_inst_tac [("S1", "reachable(F) Int S")]
+ (elimination RS constrains_weaken_L) 1);
+by Auto_tac;
+by (rtac constrains_weaken_L 1);
+by (auto_tac (claset(), simpset() addsimps [condition_def]));
+qed "Elimination";
+
+(* As above, but for the special case of S=state *)
+
+Goal
+ "[| ALL m:M. F : {s:state. x(s) = m} Co B(m); F:program |] \
+\ ==> F : {s:state. x(s):M} Co (UN m:M. B(m))";
+by (blast_tac (claset() addIs [Elimination]) 1);
+qed "Elimination2";
+
+(** Unless **)
+
+Goalw [Unless_def]
+"F:A Unless B ==> F:program & A:condition & B:condition";
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+qed "UnlessD";
+
+(*** Specialized laws for handling Always ***)
+
+(** Natural deduction rules for "Always A" **)
+Goalw [Always_def, initially_def]
+ "Always(A) = initially(A) Int Stable(A)";
+by (blast_tac (claset() addDs [StableD2]) 1);
+qed "Always_eq";
+
+val Always_def2 = Always_eq RS eq_reflection;
+
+Goalw [Always_def]
+"[| Init(F)<=A; F : Stable(A) |] ==> F : Always(A)";
+by (asm_simp_tac (simpset() addsimps [StableD2]) 1);
+qed "AlwaysI";
+
+Goal "F : Always(A) ==> Init(F)<=A & F : Stable(A)";
+by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1);
+qed "AlwaysD";
+
+bind_thm ("AlwaysE", AlwaysD RS conjE);
+bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2);
+
+
+(*The set of all reachable states is Always*)
+Goal "F : Always(A) ==> reachable(F) <= A";
+by (full_simp_tac
+ (simpset() addsimps [Stable_def, Constrains_def, constrains_def,
+ Always_def]) 1);
+by (rtac subsetI 1);
+by (etac reachable.induct 1);
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "Always_includes_reachable";
+
+Goalw [Always_def2, invariant_def2, Stable_def, stable_def]
+ "F : invariant(A) ==> F : Always(A)";
+by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
+qed "invariant_imp_Always";
+
+bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);
+
+Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A) & A:condition}";
+by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def,
+ Constrains_eq_constrains, stable_def]) 1);
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (REPEAT(blast_tac (claset() addDs [constrainsD]
+ addIs reachable.intrs@[reachable_type]) 1));
+qed "Always_eq_invariant_reachable";
+
+(*the RHS is the traditional definition of the "always" operator*)
+Goal "Always(A) = {F:program. reachable(F) <= A & A:condition}";
+br equalityI 1;
+by (ALLGOALS(Clarify_tac));
+by (auto_tac (claset() addDs [invariant_includes_reachable],
+ simpset() addsimps [subset_Int_iff, invariant_reachable,
+ Always_eq_invariant_reachable]));
+qed "Always_eq_includes_reachable";
+
+Goalw [Always_def]
+"F:Always(A)==> F:program & A:condition";
+by (blast_tac (claset() addDs [StableD2]) 1);
+qed "AlwaysD2";
+
+Goal "Always(state) = program";
+br equalityI 1;
+by (ALLGOALS(Clarify_tac));
+by (blast_tac (claset() addDs [AlwaysD2]) 1);
+by (auto_tac (claset() addDs [reachableD],
+ simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_state_eq";
+Addsimps [Always_state_eq];
+
+Goal "[| state <= A; F:program; A:condition |] ==> F : Always(A)";
+by (auto_tac (claset(), simpset()
+ addsimps [Always_eq_includes_reachable]));
+by (auto_tac (claset() addSDs [reachableD],
+ simpset() addsimps [condition_def]));
+qed "state_AlwaysI";
+
+Goal "A:condition ==> Always(A) = (UN I: Pow(A). invariant(I))";
+by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (REPEAT(blast_tac (claset()
+ addIs [invariantI, impOfSubs Init_into_reachable,
+ impOfSubs invariant_includes_reachable]
+ addDs [invariantD2]) 1));
+qed "Always_eq_UN_invariant";
+
+Goal "[| F : Always(A); A <= B; B:condition |] ==> F : Always(B)";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_weaken";
+
+
+(*** "Co" rules involving Always ***)
+val Int_absorb2 = rewrite_rule [iff_def] subset_Int_iff RS conjunct1 RS mp;
+
+Goal "[| F:Always(INV); A:condition |] \
+ \ ==> (F:(INV Int A) Co A') <-> (F : A Co A')";
+by (asm_simp_tac
+ (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
+ Constrains_def, Int_assoc RS sym]) 1);
+by (blast_tac (claset() addDs [AlwaysD2]) 1);
+qed "Always_Constrains_pre";
+
+Goal "[| F : Always(INV); A':condition |] \
+\ ==> (F : A Co (INV Int A')) <->(F : A Co A')";
+by (asm_simp_tac
+ (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
+ Constrains_eq_constrains, Int_assoc RS sym]) 1);
+by (blast_tac (claset() addDs [AlwaysD2]) 1);
+qed "Always_Constrains_post";
+
+(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *)
+bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);
+
+(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *)
+bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
+
+(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
+Goal "[| F : Always(C); F : A Co A'; \
+\ C Int B <= A; C Int A' <= B'; B:condition; B':condition |] \
+\ ==> F : B Co B'";
+by (rtac Always_ConstrainsI 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (dtac Always_ConstrainsD 1);
+by (assume_tac 2);
+by (blast_tac (claset() addDs [ConstrainsD]) 1);
+by (blast_tac (claset() addIs [Constrains_weaken]) 1);
+qed "Always_Constrains_weaken";
+
+
+(** Conjoining Always properties **)
+
+Goal "[| A:condition; B:condition |] ==> \
+\ Always(A Int B) = Always(A) Int Always(B)";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_Int_distrib";
+
+(* the premise i:I is need since INT is formally not defined for I=0 *)
+Goal "[| i:I; ALL i:I. A(i):condition |] \
+\ ==>Always(INT i:I. A(i)) = (INT i:I. Always(A(i)))";
+by (rtac equalityI 1);
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_INT_distrib";
+
+
+Goal "[| F : Always(A); F : Always(B) |] ==> F : Always(A Int B)";
+by (asm_simp_tac (simpset() addsimps
+ [Always_Int_distrib,AlwaysD2]) 1);
+qed "Always_Int_I";
+
+(*Allows a kind of "implication introduction"*)
+Goal "F : Always(A) ==> (F : Always (state-A Un B)) <-> (F : Always(B))";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_Compl_Un_eq";
+
+(*Delete the nearest invariance assumption (which will be the second one
+ used by Always_Int_I) *)
+val Always_thin =
+ read_instantiate_sg (sign_of thy)
+ [("V", "?F : Always(?A)")] thin_rl;
+
+(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
+val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
+
+(*Combines a list of invariance THEOREMS into one.*)
+val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
+
+(*** Increasing ***)
+
+Goalw [Increasing_on_def]
+"[| F:Increasing_on(A, f, r); a:A |] ==> F: Stable({s:state. <a,f`s>:r})";
+by (Blast_tac 1);
+qed "Increasing_onD";
+
+Goalw [Increasing_on_def]
+"F:Increasing_on(A, f, r) ==> F:program & f:state->A & part_order(A,r)";
+by (auto_tac (claset(), simpset() addsimps [INT_iff]));
+qed "Increasing_onD2";
+
+Goalw [Increasing_on_def, Stable_def, Constrains_def, stable_def, constrains_def, part_order_def]
+ "!!f. g:mono_map(A,r,A,r) \
+\ ==> Increasing_on(A, f, r) <= Increasing_on(A, g O f, r)";
+by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1);
+by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def]));
+by (force_tac (claset() addSDs [bspec, ActsD], simpset()) 1);
+by (subgoal_tac "xd:state" 1);
+by (blast_tac (claset() addSDs [ActsD]) 2);
+by (subgoal_tac "f`xe:A & f`xd:A" 1);
+by (blast_tac (claset() addDs [apply_type]) 2);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (Asm_simp_tac 1);
+by (REPEAT(etac conjE 1));
+by (rotate_tac ~3 1);
+by (dres_inst_tac [("x", "xc")] bspec 1);
+by (Asm_simp_tac 1);
+by (dres_inst_tac [("c", "xd")] subsetD 1);
+by (rtac imageI 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1);
+by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (dres_inst_tac [("x", "f`xd")] bspec 2);
+by (ALLGOALS(Asm_simp_tac));
+by (dres_inst_tac [("b", "g`(f`xe)")] trans_onD 1);
+by Auto_tac;
+qed "mono_Increasing_on_comp";
+
+Goalw [increasing_on_def, Increasing_on_def]
+ "F : increasing_on(A, f,r) ==> F : Increasing_on(A, f,r)";
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
+by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
+qed "increasing_on_imp_Increasing_on";
+
+bind_thm("Increasing_on_constant", increasing_on_constant RS increasing_on_imp_Increasing_on);
+Addsimps [Increasing_on_constant];
+
+Goalw [Increasing_on_def, nat_order_def]
+ "[| F:Increasing_on(nat,f, nat_order); z:nat |] \
+\ ==> F: Stable({s:state. z < f`s})";
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
+by Safe_tac;
+by (dres_inst_tac [("x", "succ(z)")] bspec 1);
+by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq]));
+by (subgoal_tac "{x: state . f ` x : nat} = state" 1);
+by Auto_tac;
+qed "strict_Increasing_onD";
+
+(*To allow expansion of the program's definition when appropriate*)
+val program_defs_ref = ref ([] : thm list);
+
+(*proves "co" properties when the program is specified*)
+
+fun constrains_tac i =
+ SELECT_GOAL
+ (EVERY [REPEAT (Always_Int_tac 1),
+ REPEAT (etac Always_ConstrainsI 1
+ ORELSE
+ resolve_tac [StableI, stableI,
+ constrains_imp_Constrains] 1),
+ rtac constrainsI 1,
+ full_simp_tac (simpset() addsimps !program_defs_ref) 1,
+ ALLGOALS Clarify_tac,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS Clarify_tac,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS Clarify_tac,
+ ALLGOALS Asm_full_simp_tac,
+ ALLGOALS Clarify_tac]) i;
+
+(*For proving invariants*)
+fun always_tac i =
+ rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Constrains.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,75 @@
+(* Title: ZF/UNITY/Constrains.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Safety relations: restricted to the set of reachable states.
+
+Theory ported from HOL.
+*)
+
+Constrains = UNITY +
+consts traces :: "[i, i] => i"
+ (* Initial states and program => (final state, reversed trace to it)...
+ the domain might also be state*list(state) *)
+inductive
+ domains
+ "traces(init, acts)" <=
+ "(init Un (UN act:acts. field(act)))*list(UN act:acts. field(act))"
+ intrs
+ (*Initial trace is empty*)
+ Init "s: init ==> <s,[]> : traces(init,acts)"
+
+ Acts "[| act:acts; <s,evs> : traces(init,acts); <s,s'>: act |]
+ ==> <s', Cons(s,evs)> : traces(init, acts)"
+
+ type_intrs "list.intrs@[UnI1, UnI2, UN_I, fieldI2, fieldI1]"
+
+ consts reachable :: "i=>i"
+
+inductive
+ domains
+ "reachable(F)" <= "Init(F) Un (UN act:Acts(F). field(act))"
+ intrs
+ Init "s:Init(F) ==> s:reachable(F)"
+
+ Acts "[| act: Acts(F); s:reachable(F); <s,s'>: act |]
+ ==> s':reachable(F)"
+
+ type_intrs "[UnI1, UnI2, fieldI2, UN_I]"
+
+
+consts
+ Constrains :: "[i,i] => i" (infixl "Co" 60)
+ op_Unless :: "[i, i] => i" (infixl "Unless" 60)
+
+defs
+ Constrains_def
+ "A Co B == {F:program. F:(reachable(F) Int A) co B &
+ A:condition & B:condition}"
+
+ Unless_def
+ "A Unless B == (A-B) Co (A Un B)"
+
+constdefs
+ Stable :: "i => i"
+ "Stable(A) == A Co A"
+ (*Always is the weak form of "invariant"*)
+ Always :: "i => i"
+ "Always(A) == {F:program. Init(F) <= A} Int Stable(A)"
+
+ (*
+ The constant Increasing_on defines a weak form of the Charpentier's
+ increasing notion. It should not be confused with the ZF's
+ increasing constant which have a different meaning.
+ Increasing's parameters: a state function f,
+ a domain A and a order relation r over the domain A.
+ Should f be a meta function instead ?
+ *)
+ Increasing_on :: [i,i, i] => i ("Increasing[_]'(_,_')")
+ "Increasing[A](f, r) == {F:program. f:state->A &
+ part_order(A,r) &
+ F: (INT z:A. Stable({s:state. <z, f`s>:r}))}"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/FP.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,104 @@
+(* Title: HOL/UNITY/FP.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Fixed Point of a Program
+
+From Misra, "A Logic for Concurrent Programming", 1994
+
+Theory ported form HOL.
+*)
+
+
+Goalw [FP_Orig_def]
+ "FP_Orig(F):condition";
+by (Blast_tac 1);
+qed "FP_Orig_type";
+AddIffs [FP_Orig_type];
+AddTCs [FP_Orig_type];
+
+Goalw [FP_Orig_def, condition_def]
+ "x:FP_Orig(F) ==> x:state";
+by Auto_tac;
+qed "FP_OrigD";
+
+Goalw [FP_def, condition_def]
+ "FP(F):condition";
+by (Blast_tac 1);
+qed "FP_type";
+AddIffs [FP_type];
+AddTCs [FP_type];
+
+Goalw [FP_def, condition_def]
+ "x:FP(F) ==> x:state";
+by Auto_tac;
+qed "FP_D";
+
+Goal "Union(B) Int A = (UN C:B. C Int A)";
+by (Blast_tac 1);
+qed "Int_Union2";
+
+Goalw [FP_Orig_def, stable_def]
+"[| F:program; B:condition |] \
+\ ==> F:stable(FP_Orig(F) Int B)";
+by (stac Int_Union2 1);
+by (blast_tac (claset() addIs [constrains_UN]) 1);
+qed "stable_FP_Orig_Int";
+
+Goalw [FP_Orig_def, stable_def]
+ "[| ALL B:condition. F : stable (A Int B); A:condition |] \
+\ ==> A <= FP_Orig(F)";
+by (Blast_tac 1);
+bind_thm("FP_Orig_weakest", ballI RS result());
+
+Goal "A Int cons(a, B) = \
+ \ (if a : A then cons(a, cons(a, (A Int B))) else A Int B)";
+by Auto_tac;
+qed "Int_cons_right";
+
+
+Goal "[| F:program; B:condition |] ==> F : stable (FP(F) Int B)";
+by (subgoal_tac "FP(F) Int B = (UN x:B. FP(F) Int {x})" 1);
+by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [Int_cons_right]) 1);
+by (rewrite_goals_tac [FP_def, stable_def]);
+by (rtac constrains_UN 1);
+by (auto_tac (claset(), simpset() addsimps [cons_absorb]));
+qed "stable_FP_Int";
+
+
+Goal "F:program ==> FP(F) <= FP_Orig(F)";
+by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
+by Auto_tac;
+val lemma1 = result();
+
+
+Goalw [FP_Orig_def, FP_def]
+"F:program ==> FP_Orig(F) <= FP(F)";
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "{x}")] bspec 1);
+by (force_tac (claset(), simpset() addsimps [condition_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Int_cons_right]) 1);
+by (auto_tac (claset(), simpset() addsimps [cons_absorb]));
+by (force_tac (claset(), simpset() addsimps [condition_def]) 1);
+val lemma2 = result();
+
+
+Goal "F:program ==> FP(F) = FP_Orig(F)";
+by (rtac ([lemma1,lemma2] MRS equalityI) 1);
+by (ALLGOALS(assume_tac));
+qed "FP_equivalence";
+
+
+Goal "[| ALL B:condition. F : stable(A Int B); A:condition; F:program |] \
+\ ==> A <= FP(F)";
+by (asm_simp_tac (simpset() addsimps [FP_equivalence, FP_Orig_weakest]) 1);
+bind_thm("FP_weakest", result() RS ballI);
+
+Goalw [FP_def, stable_def, constrains_def, condition_def]
+ "[| F:program; A:condition |] ==> \
+\ A - FP(F) = (UN act: Acts(F). A -{s:state. act``{s} <= {s}})";
+by (Blast_tac 1);
+qed "Diff_FP";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/FP.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,22 @@
+(* Title: ZF/UNITY/FP.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Fixed Point of a Program
+
+From Misra, "A Logic for Concurrent Programming", 1994
+
+Theory ported from HOL.
+*)
+
+FP = UNITY +
+
+constdefs
+ FP_Orig :: i=>i
+ "FP_Orig(F) == Union({A:condition. ALL B:condition. F : stable(A Int B)})"
+
+ FP :: i=>i
+ "FP(F) == {s:state. F : stable({s})}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Guar.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,581 @@
+(* Title: ZF/UNITY/Guar.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Guarantees, etc.
+
+From Chandy and Sanders, "Reasoning About Program Composition"
+Revised by Sidi Ehmety on January 2001
+
+Proofs ported from HOL.
+*)
+
+
+Goal
+"F~:program ==> F Join G = programify(G)";
+by (rtac program_equalityI 1);
+by Auto_tac;
+by (auto_tac (claset(),
+ simpset() addsimps [Join_def, programify_def, SKIP_def,
+ Acts_def, Init_def, AllowedActs_def,
+ RawInit_eq, RawActs_eq, RawAllowedActs_eq,
+ Int_absorb, Int_assoc, Un_absorb]));
+by (forward_tac [Id_in_RawActs] 2);
+by (forward_tac [Id_in_RawAllowedActs] 3);
+by (dtac RawInit_type 1);
+by (dtac RawActs_type 2);
+by (dtac RawAllowedActs_type 3);
+by (auto_tac (claset(), simpset()
+ addsimps [condition_def, actionSet_def, cons_absorb]));
+qed "not_program_Join1";
+
+Goal
+"G~:program ==> F Join G = programify(F)";
+by (stac Join_commute 1);
+by (blast_tac (claset() addIs [not_program_Join1]) 1);
+qed "not_program_Join2";
+
+Goal "F~:program ==> F ok G";
+by (auto_tac (claset(),
+ simpset() addsimps [ok_def, programify_def, SKIP_def, mk_program_def,
+ Acts_def, Init_def, AllowedActs_def,
+ RawInit_def, RawActs_def, RawAllowedActs_def,
+ Int_absorb, Int_assoc, Un_absorb]));
+by (auto_tac (claset(), simpset()
+ addsimps [condition_def, actionSet_def, program_def, cons_absorb]));
+qed "not_program_ok1";
+
+Goal "G~:program ==> F ok G";
+by (rtac ok_sym 1);
+by (blast_tac (claset() addIs [not_program_ok1]) 1);
+qed "not_program_ok2";
+
+
+Goal "OK(cons(i, I), F) <-> \
+\ (i:I & OK(I, F)) | (i~:I & OK(I, F) & F(i) ok JOIN(I,F))";
+by (asm_full_simp_tac (simpset() addsimps [OK_iff_ok]) 1);
+(** Auto_tac proves the goal in one step, but take more time **)
+by Safe_tac;
+by (ALLGOALS(Clarify_tac));
+by (REPEAT(blast_tac (claset() addIs [ok_sym]) 10));
+by (REPEAT(Blast_tac 1));
+qed "OK_cons_iff";
+
+(*** existential properties ***)
+
+Goalw [ex_prop_def]
+ "GG:Fin(program) ==> (ex_prop(X) \
+\ --> GG Int X~=0 --> OK(GG, (%G. G)) -->(JN G:GG. G):X)";
+by (etac Fin_induct 1);
+by (ALLGOALS(asm_full_simp_tac
+ (simpset() addsimps [OK_cons_iff])));
+(* Auto_tac proves the goal in one step *)
+by Safe_tac;
+by (ALLGOALS(Asm_full_simp_tac));
+by (Fast_tac 1);
+qed_spec_mp "ex1";
+
+Goalw [ex_prop_def]
+ "X<=program ==> (ALL GG. GG:Fin(program) & GG Int X ~= 0\
+\ --> OK(GG,(%G. G)) -->(JN G:GG. G):X) --> ex_prop(X)";
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "{F,G}")] spec 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [OK_iff_ok])));
+by Safe_tac;
+by (auto_tac (claset() addIs [ok_sym], simpset()));
+qed "ex2";
+
+(*Chandy & Sanders take this as a definition*)
+
+Goal "X<=program ==> ex_prop(X) <-> \
+\ (ALL GG. GG:Fin(program) & GG Int X ~= 0 &\
+\ OK(GG,( %G. G)) --> (JN G:GG. G):X)";
+by (blast_tac (claset() addIs [ex1, ex2 RS mp]) 1);
+qed "ex_prop_finite";
+
+
+(*Their "equivalent definition" given at the end of section 3*)
+Goalw [ex_prop2_def]
+ "ex_prop(X) <-> ex_prop2(X)";
+by (Asm_full_simp_tac 1);
+by (rewrite_goals_tac
+ [ex_prop_def, component_of_def]);
+by Safe_tac;
+by (stac Join_commute 4);
+by (dtac ok_sym 4);
+by (case_tac "G:program" 1);
+by (dres_inst_tac [("x", "G")] bspec 5);
+by (dres_inst_tac [("x", "F")] bspec 4);
+by Safe_tac;
+by (force_tac (claset(),
+ simpset() addsimps [not_program_Join1]) 2);
+by (REPEAT(Force_tac 1));
+qed "ex_prop_equiv";
+
+(*** universal properties ***)
+
+Goalw [uv_prop_def]
+ "GG:Fin(program) ==> \
+\ (uv_prop(X)--> \
+\ GG <= X & OK(GG, (%G. G)) --> (JN G:GG. G):X)";
+by (etac Fin_induct 1);
+by (auto_tac (claset(), simpset() addsimps
+ [OK_cons_iff]));
+qed_spec_mp "uv1";
+
+Goalw [uv_prop_def]
+"X<=program ==> (ALL GG. GG:Fin(program) & GG <= X & OK(GG,(%G. G)) \
+\ --> (JN G:GG. G):X) --> uv_prop(X)";
+by Auto_tac;
+by (Clarify_tac 2);
+by (dres_inst_tac [("x", "{x,xa}")] spec 2);
+by (dres_inst_tac [("x", "0")] spec 1);
+by (auto_tac (claset() addDs [ok_sym],
+ simpset() addsimps [OK_iff_ok]));
+qed "uv2";
+
+(*Chandy & Sanders take this as a definition*)
+Goal
+"X<=program ==> \
+\ uv_prop(X) <-> (ALL GG. GG:Fin(program) & GG <= X &\
+\ OK(GG, %G. G) --> (JN G:GG. G): X)";
+by (REPEAT(blast_tac (claset() addIs [uv1,uv2 RS mp]) 1));
+qed "uv_prop_finite";
+
+(*** guarantees ***)
+(* The premise G:program is needed later *)
+val major::prems = Goal
+ "[| (!!G. [| F ok G; F Join G:X; G:program |] ==> F Join G : Y); F:program |] \
+\ ==> F : X guarantees Y";
+by (cut_facts_tac prems 1);
+by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
+by (blast_tac (claset() addIs [major]) 1);
+qed "guaranteesI";
+
+Goalw [guar_def, component_def]
+ "[| F : X guarantees Y; F ok G; F Join G:X; G:program |] \
+\ ==> F Join G : Y";
+by (Asm_full_simp_tac 1);
+qed "guaranteesD";
+
+(*This version of guaranteesD matches more easily in the conclusion
+ The major premise can no longer be F<=H since we need to reason about G*)
+
+Goalw [guar_def]
+ "[| F : X guarantees Y; F Join G = H; H : X; F ok G; G:program |] \
+\ ==> H : Y";
+by (Blast_tac 1);
+qed "component_guaranteesD";
+
+Goalw [guar_def]
+ "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
+by Auto_tac;
+qed "guarantees_weaken";
+
+Goalw [guar_def] "X <= Y \
+\ ==> X guarantees Y = program";
+by (Blast_tac 1);
+qed "subset_imp_guarantees_program";
+
+(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
+Goalw [guar_def] "[| X <= Y; F:program |] \
+\ ==> F : X guarantees Y";
+by (Blast_tac 1);
+qed "subset_imp_guarantees";
+
+(*Remark at end of section 4.1 *)
+Goalw [guar_def, component_of_def]
+"Y<=program ==>ex_prop(Y) --> (Y = (program guarantees Y))";
+by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
+(* Simplification tactics with ex_prop2_def loops *)
+by (rewrite_goals_tac [ex_prop2_def]);
+by (Clarify_tac 1);
+by (rtac equalityI 1);
+by Safe_tac;
+by (Blast_tac 1);
+by (dres_inst_tac [("x", "x")] bspec 1);
+by (dres_inst_tac [("x", "x")] bspec 3);
+by (dtac iff_sym 4);
+by (Blast_tac 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (etac iffE 2);
+by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
+by Safe_tac;
+by (REPEAT(Force_tac 1));
+qed "ex_prop_imp";
+
+Goalw [guar_def]
+ "(Y = program guarantees Y) ==> ex_prop(Y)";
+by (asm_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
+by (rewrite_goals_tac [ex_prop2_def]);
+by Safe_tac;
+by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
+by (dtac sym 2);
+by (ALLGOALS(etac equalityE));
+by (REPEAT(Force_tac 1));
+qed "guarantees_imp";
+
+Goal "Y<=program ==>(ex_prop(Y)) <-> (Y = program guarantees Y)";
+by (rtac iffI 1);
+by (rtac (ex_prop_imp RS mp) 1);
+by (rtac guarantees_imp 3);
+by (ALLGOALS(Asm_simp_tac));
+qed "ex_prop_equiv2";
+
+(** Distributive laws. Re-orient to perform miniscoping **)
+
+Goalw [guar_def]
+ "i:I ==>(UN i:I. X(i)) guarantees Y = (INT i:I. X(i) guarantees Y)";
+by (rtac equalityI 1);
+by Safe_tac;
+by (Force_tac 2);
+by (REPEAT(Blast_tac 1));
+qed "guarantees_UN_left";
+
+Goalw [guar_def]
+ "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
+by (rtac equalityI 1);
+by Safe_tac;
+by (REPEAT(Blast_tac 1));
+qed "guarantees_Un_left";
+
+Goalw [guar_def]
+ "i:I ==> X guarantees (INT i:I. Y(i)) = (INT i:I. X guarantees Y(i))";
+by (rtac equalityI 1);
+by Safe_tac;
+by (REPEAT(Blast_tac 1));
+qed "guarantees_INT_right";
+
+Goalw [guar_def]
+ "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
+by (Blast_tac 1);
+qed "guarantees_Int_right";
+
+Goal "[| F : Z guarantees X; F : Z guarantees Y |] \
+\ ==> F : Z guarantees (X Int Y)";
+by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
+qed "guarantees_Int_right_I";
+
+Goal "i:I==> (F : X guarantees (INT i:I. Y(i))) <-> \
+\ (ALL i:I. F : X guarantees Y(i))";
+by (asm_simp_tac (simpset() addsimps [guarantees_INT_right, INT_iff]) 1);
+by (Blast_tac 1);
+qed "guarantees_INT_right_iff";
+
+
+Goalw [guar_def] "(X guarantees Y) = (program guarantees ((program-X) Un Y))";
+by Auto_tac;
+qed "shunting";
+
+Goalw [guar_def] "(X guarantees Y) = (program - Y) guarantees (program -X)";
+by (Blast_tac 1);
+qed "contrapositive";
+
+(** The following two can be expressed using intersection and subset, which
+ is more faithful to the text but looks cryptic.
+**)
+
+Goalw [guar_def]
+ "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\
+\ ==> F : (V Int Y) guarantees Z";
+by (Blast_tac 1);
+qed "combining1";
+
+Goalw [guar_def]
+ "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\
+\ ==> F : V guarantees (X Un Z)";
+by (Blast_tac 1);
+qed "combining2";
+
+
+(** The following two follow Chandy-Sanders, but the use of object-quantifiers
+ does not suit Isabelle... **)
+
+(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
+Goalw [guar_def]
+ "[| ALL i:I. F : X guarantees Y(i); i:I |] \
+\ ==> F : X guarantees (INT i:I. Y(i))";
+by (Blast_tac 1);
+qed "all_guarantees";
+
+(*Premises should be [| F: X guarantees Y i; i: I |] *)
+Goalw [guar_def]
+ "EX i:I. F : X guarantees Y(i) ==> F : X guarantees (UN i:I. Y(i))";
+by (Blast_tac 1);
+qed "ex_guarantees";
+
+
+(*** Additional guarantees laws, by lcp ***)
+
+Goalw [guar_def]
+ "[| F: U guarantees V; G: X guarantees Y; F ok G |] \
+\ ==> F Join G: (U Int X) guarantees (V Int Y)";
+by (Simp_tac 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
+by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1);
+by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1);
+by (asm_simp_tac (simpset() addsimps Join_ac) 1);
+qed "guarantees_Join_Int";
+
+Goalw [guar_def]
+ "[| F: U guarantees V; G: X guarantees Y; F ok G |] \
+\ ==> F Join G: (U Un X) guarantees (V Un Y)";
+by (Simp_tac 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
+by (subgoal_tac "F Join G Join x = G Join (F Join x)" 1);
+by (rotate_tac 4 1);
+by (dres_inst_tac [("x", "F Join x")] bspec 1);
+by (Simp_tac 1);
+by (force_tac (claset(), simpset() addsimps [ok_commute]) 1);
+by (asm_simp_tac (simpset() addsimps Join_ac) 1);
+qed "guarantees_Join_Un";
+
+Goalw [guar_def]
+ "[| ALL i:I. F(i) : X(i) guarantees Y(i); OK(I,F); i:I |] \
+\ ==> (JN i:I. F(i)) : (INT i:I. X(i)) guarantees (INT i:I. Y(i))";
+by Safe_tac;
+by (Blast_tac 2);
+by (dres_inst_tac [("x", "xa")] bspec 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [INT_iff])));
+by Safe_tac;
+by (rotate_tac ~1 1);
+by (dres_inst_tac [("x", "(JN x:(I-{xa}). F(x)) Join G")] bspec 1);
+by (auto_tac
+ (claset() addIs [OK_imp_ok],
+ simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
+qed "guarantees_JN_INT";
+
+Goalw [guar_def]
+ "[| ALL i:I. F(i) : X(i) guarantees Y(i); OK(I,F) |] \
+\ ==> JOIN(I,F) : (UN i:I. X(i)) guarantees (UN i:I. Y(i))";
+by Auto_tac;
+by (dres_inst_tac [("x", "xa")] bspec 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by Safe_tac;
+by (rotate_tac ~1 1);
+by (dres_inst_tac [("x", "JOIN(I-{xa}, F) Join x")] bspec 1);
+by (auto_tac
+ (claset() addIs [OK_imp_ok],
+ simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
+qed "guarantees_JN_UN";
+
+(*** guarantees laws for breaking down the program, by lcp ***)
+
+Goalw [guar_def]
+ "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y";
+by (Simp_tac 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
+qed "guarantees_Join_I1";
+
+Goal "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y";
+by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute,
+ inst "G" "G" ok_commute]) 1);
+by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
+qed "guarantees_Join_I2";
+
+Goalw [guar_def]
+ "[| i:I; F(i): X guarantees Y; OK(I,F) |] \
+\ ==> (JN i:I. F(i)) : X guarantees Y";
+by Safe_tac;
+by (dres_inst_tac [("x", "JOIN(I-{i},F) Join G")] bspec 1);
+by (Simp_tac 1);
+by (auto_tac (claset() addIs [OK_imp_ok],
+ simpset() addsimps [JN_Join_diff, Join_assoc RS sym]));
+qed "guarantees_JN_I";
+
+(*** well-definedness ***)
+
+Goalw [welldef_def] "F Join G: welldef ==> programify(F): welldef";
+by Auto_tac;
+qed "Join_welldef_D1";
+
+Goalw [welldef_def] "F Join G: welldef ==> programify(G): welldef";
+by Auto_tac;
+qed "Join_welldef_D2";
+
+(*** refinement ***)
+
+Goalw [refines_def] "F refines F wrt X";
+by (Blast_tac 1);
+qed "refines_refl";
+
+(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
+
+Goalw [guar_def, component_of_def]
+"(F:X guarantees Y) <-> \
+\ F:program & (ALL H:program. H:X --> (F component_of H --> H:Y))";
+by Safe_tac;
+by (REPEAT(Force_tac 1));
+qed "guarantees_equiv";
+
+Goalw [wg_def] "!!X. [| F:(X guarantees Y); X <= program |] ==> X <= wg(F,Y)";
+by Auto_tac;
+qed "wg_weakest";
+
+Goalw [wg_def, guar_def]
+"F:program ==> F:wg(F,Y) guarantees Y";
+by (Blast_tac 1);
+qed "wg_guarantees";
+
+Goalw [wg_def]
+ "[| F:program; H:program |] ==> \
+\ (H: wg(F,X)) <-> H:program & (F component_of H --> H:X)";
+by (simp_tac (simpset() addsimps [guarantees_equiv]) 1);
+by (rtac iffI 1);
+by Safe_tac;
+by (res_inst_tac [("x", "{H}")] bexI 3);
+by (res_inst_tac [("x", "{H}")] bexI 2);
+by (REPEAT(Blast_tac 1));
+qed "wg_equiv";
+
+Goal
+"[| F component_of H; F:program; H:program |] ==> \
+\ H:wg(F,X) <-> H:X";
+by (asm_full_simp_tac (simpset() addsimps [wg_equiv]) 1);
+qed "component_of_wg";
+
+Goal
+"ALL FF:Fin(program). FF Int X ~= 0 --> OK(FF, %F. F) \
+\ --> (ALL F:FF. ((JN F:FF. F): wg(F,X)) <-> ((JN F:FF. F):X))";
+by (Clarify_tac 1);
+by (subgoal_tac "F component_of (JN F:FF. F)" 1);
+by (dres_inst_tac [("X", "X")] component_of_wg 1);
+by (force_tac (claset() addSDs [Fin.dom_subset RS subsetD RS PowD],
+ simpset()) 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_def])));
+by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);
+by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym],
+ simpset() addsimps [OK_iff_ok]));
+qed "wg_finite";
+
+
+(* "!!FF. [| FF:Fin(program); FF Int X ~=0; OK(FF, %F. F); G:FF |]
+ ==> JOIN(FF, %F. F):wg(G, X) <-> JOIN(FF, %F. F):X" *)
+val wg_finite2 = wg_finite RS bspec RS mp RS mp RS bspec;
+
+
+Goal "[| ex_prop(X); F:program |] ==> (F:X) <-> (ALL H:program. H : wg(F,X))";
+by (asm_full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1);
+by (rewrite_goals_tac [ex_prop2_def]);
+by (Blast_tac 1);
+qed "wg_ex_prop";
+
+(** From Charpentier and Chandy "Theorems About Composition" **)
+(* Proposition 2 *)
+Goalw [wx_def] "wx(X)<=X";
+by Auto_tac;
+qed "wx_subset";
+
+Goalw [wx_def] "wx(X)<=program";
+by Auto_tac;
+qed "wx_into_program";
+
+Goal
+"ex_prop(wx(X))";
+by (full_simp_tac (simpset()
+ addsimps [ex_prop_def, wx_def]) 1);
+by Safe_tac;
+by (ALLGOALS(res_inst_tac [("x", "xb")] bexI));
+by (REPEAT(Force_tac 1));
+qed "wx_ex_prop";
+
+Goalw [wx_def]
+"ALL Z. Z<=program --> Z<= X --> ex_prop(Z) --> Z <= wx(X)";
+by Auto_tac;
+qed "wx_weakest";
+
+(* Proposition 6 *)
+Goalw [ex_prop_def]
+ "ex_prop({F:program. ALL G:program. F ok G --> F Join G:X})";
+by Safe_tac;
+by (dres_inst_tac [("x", "G Join Ga")] bspec 1);
+by (Simp_tac 1);
+by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1);
+by (dres_inst_tac [("x", "F Join Ga")] bspec 1);
+by (Simp_tac 1);
+by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1);
+by Safe_tac;
+by (asm_simp_tac (simpset() addsimps [ok_commute]) 1);
+by (subgoal_tac "F Join G = G Join F" 1);
+by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1);
+by (simp_tac (simpset() addsimps [Join_commute]) 1);
+qed "wx'_ex_prop";
+
+(* Equivalence with the other definition of wx *)
+
+Goalw [wx_def]
+ "wx(X) = {F:program. ALL G:program. F ok G --> (F Join G):X}";
+by (rtac equalityI 1);
+by Safe_tac;
+by (Blast_tac 1);
+by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
+by (dres_inst_tac [("x", "x")] bspec 1);
+by (dres_inst_tac [("x", "G")] bspec 2);
+by (forw_inst_tac [("c", "x Join G")] subsetD 3);
+by Safe_tac;
+by (Blast_tac 1);
+by (Blast_tac 1);
+by (res_inst_tac [("B", "{F:program. ALL G:program. F ok G --> F Join G:X}")]
+ UnionI 1);
+by Safe_tac;
+by (rtac wx'_ex_prop 2);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x", "SKIP")] bspec 1);
+by Auto_tac;
+qed "wx_equiv";
+
+(* Propositions 7 to 11 are all about this second definition of wx. And
+ by equivalence between the two definition, they are the same as the ones proved *)
+
+
+(* Proposition 12 *)
+(* Main result of the paper *)
+Goalw [guar_def]
+ "(X guarantees Y) = wx((program-X) Un Y)";
+by (simp_tac (simpset() addsimps [wx_equiv]) 1);
+by Auto_tac;
+qed "guarantees_wx_eq";
+
+(* {* Corollary, but this result has already been proved elsewhere *}
+ "ex_prop(X guarantees Y)";
+ by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
+ qed "guarantees_ex_prop";
+*)
+
+(* Rules given in section 7 of Chandy and Sander's
+ Reasoning About Program composition paper *)
+
+Goal "[| Init(F) <= A; F:program |] \
+\ ==> F:(stable(A)) guarantees (Always(A))";
+by (rtac guaranteesI 1);
+by (assume_tac 2);
+by (simp_tac (simpset() addsimps [Join_commute]) 1);
+by (rtac stable_Join_Always1 1);
+by (ALLGOALS(asm_full_simp_tac (simpset()
+ addsimps [invariant_def, Join_stable])));
+by (auto_tac (claset(), simpset() addsimps [programify_def]));
+qed "stable_guarantees_Always";
+
+(* To be moved to WFair.ML *)
+Goal "[| F:A co A Un B; F:transient(A) |] ==> F:A leadsTo B";
+by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
+by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
+by (rtac (ensuresI RS leadsTo_Basis) 3);
+by (ALLGOALS(Blast_tac));
+qed "leadsTo_Basis'";
+
+Goal "[| F:transient(A); B:condition |] \
+\ ==> F: (A co A Un B) guarantees (A leadsTo (B-A))";
+by (rtac guaranteesI 1);
+by (rtac leadsTo_Basis' 1);
+by (dtac constrains_weaken_R 1);
+by (assume_tac 3);
+by (blast_tac (claset() addIs [Join_transient_I1]) 3);
+by (REPEAT(blast_tac (claset() addDs [transientD]) 1));
+qed "constrains_guarantees_leadsTo";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Guar.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,72 @@
+(* Title: ZF/UNITY/Guar.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Guarantees, etc.
+
+From Chandy and Sanders, "Reasoning About Program Composition",
+Technical Report 2000-003, University of Florida, 2000.
+
+Revised by Sidi Ehmety on January 2001
+
+Added: Compatibility, weakest guarantees, etc.
+
+and Weakest existential property,
+from Charpentier and Chandy "Theorems about Composition",
+Fifth International Conference on Mathematics of Program, 2000.
+
+Theory ported from HOL.
+*)
+Guar = Comp +
+constdefs
+
+ (*Existential and Universal properties. I formalize the two-program
+ case, proving equivalence with Chandy and Sanders's n-ary definitions*)
+
+ ex_prop :: i =>o
+ "ex_prop(X) == ALL F:program. ALL G:program.
+ F ok G --> F:X | G:X --> (F Join G):X"
+
+ (* Equivalent definition of ex_prop given at the end of section 3*)
+ ex_prop2 :: i =>o
+ "ex_prop2(X) == ALL G:program. (G:X <-> (ALL H:program. (G component_of H) --> H:X))"
+
+ strict_ex_prop :: i => o
+ "strict_ex_prop(X) == ALL F:program. ALL G:program.
+ F ok G --> (F:X | G: X) <-> (F Join G : X)"
+
+
+ uv_prop :: i => o
+ "uv_prop(X) == SKIP:X & (ALL F:program. ALL G:program.
+ F ok G --> F:X & G:X --> (F Join G):X)"
+
+ strict_uv_prop :: i => o
+ "strict_uv_prop(X) == SKIP:X &
+ (ALL F:program. ALL G:program. F ok G -->(F:X & G:X) <-> (F Join G:X))"
+
+ guar :: [i, i] => i (infixl "guarantees" 55)
+ (*higher than membership, lower than Co*)
+ "X guarantees Y == {F:program. ALL G:program. F ok G --> F Join G : X --> F Join G:Y}"
+
+ (* Weakest guarantees *)
+ wg :: [i,i] => i
+ "wg(F,Y) == Union({X:Pow(program). F:(X guarantees Y)})"
+
+ (* Weakest existential property stronger than X *)
+ wx :: "i =>i"
+ "wx(X) == Union({Y:Pow(program). Y<=X & ex_prop(Y)})"
+
+ (*Ill-defined programs can arise through "Join"*)
+ welldef :: i
+ "welldef == {F:program. Init(F) ~= 0}"
+
+ refines :: [i, i, i] => o ("(3_ refines _ wrt _)" [10,10,10] 10)
+ "G refines F wrt X ==
+ ALL H:program. (F ok H & G ok H & F Join H:welldef Int X)
+ --> (G Join H:welldef Int X)"
+
+ iso_refines :: [i,i, i] => o ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
+ "G iso_refines F wrt X == F:welldef Int X --> G:welldef Int X"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Mutex.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,269 @@
+(* Title: ZF/UNITY/Mutex.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+
+*)
+
+(** Variables' types **)
+
+AddIffs [p_type, u_type, v_type, m_type, n_type];
+
+Goal "!!s. s:state ==> s`u:bool";
+by (dres_inst_tac [("a", "u"), ("A", "variable")]
+ apply_type 1);
+by (auto_tac (claset(), simpset() addsimps [u_type]));
+qed "u_apply_type";
+
+Goal "!!s. s:state ==> s`v:bool";
+by (dres_inst_tac [("a", "v"), ("A", "variable")]
+ apply_type 1);
+by (auto_tac (claset(), simpset() addsimps [v_type]));
+qed "v_apply_type";
+
+
+Goal "!!s. s:state ==> s`p:bool";
+by (dres_inst_tac [("a", "p"), ("A", "variable")]
+ apply_type 1);
+by (auto_tac (claset(), simpset() addsimps [p_type]));
+qed "p_apply_type";
+
+Goal "!!s. s:state ==> s`m:int";
+by (dres_inst_tac [("a", "m"), ("A", "variable")]
+ apply_type 1);
+by (auto_tac (claset(), simpset() addsimps [m_type]));
+qed "m_apply_type";
+
+Goal "!!s. s:state ==> s`n:int";
+by (dres_inst_tac [("a", "n"), ("A", "variable")]
+ apply_type 1);
+by (auto_tac (claset(), simpset() addsimps [n_type]));
+qed "n_apply_type";
+
+Addsimps [p_apply_type, u_apply_type, v_apply_type, m_apply_type, n_apply_type];
+
+
+(** Mutex is a program **)
+
+Goalw [Mutex_def]
+"Mutex:program";
+by Auto_tac;
+qed "Mutex_in_program";
+AddIffs [Mutex_in_program];
+
+Addsimps [Mutex_def RS def_prg_Init];
+program_defs_ref := [Mutex_def];
+
+Addsimps (map simp_of_act
+ [U0_def, U1_def, U2_def, U3_def, U4_def,
+ V0_def, V1_def, V2_def, V3_def, V4_def]);
+
+Addsimps (map simp_of_set [U0_def, U1_def, U2_def, U3_def, U4_def,
+ V0_def, V1_def, V2_def, V3_def, V4_def]);
+
+Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
+
+Addsimps [condition_def, actionSet_def];
+
+
+Addsimps variable.intrs;
+AddIs variable.intrs;
+
+(** In case one wants to be sure that the initial state is not empty **)
+Goal "some(u:=0,v:=0, m:= #0,n:= #0):Init(Mutex)";
+by Auto_tac;
+by (REPEAT(rtac update_type2 1));
+by (auto_tac (claset(), simpset() addsimps [lam_type]));
+qed "Mutex_Init_not_empty";
+
+Goal "Mutex : Always(IU)";
+by (always_tac 1);
+by Auto_tac;
+qed "IU";
+
+Goal "Mutex : Always(IV)";
+by (always_tac 1);
+by Auto_tac;
+qed "IV";
+
+
+(*The safety property: mutual exclusion*)
+Goal "Mutex : Always({s:state. ~(s`m = #3 & s`n = #3)})";
+by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
+by Auto_tac;
+qed "mutual_exclusion";
+
+(*The bad invariant FAILS in V1*)
+
+Goal "[| x$<#1; #3 $<= x |] ==> P";
+by (dres_inst_tac [("j", "#1"), ("k", "#3")] zless_zle_trans 1);
+by (dres_inst_tac [("j", "x")] zle_zless_trans 2);
+by Auto_tac;
+qed "less_lemma";
+
+Goal "Mutex : Always(bad_IU)";
+by (always_tac 1);
+by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless]));
+by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def]));
+by (subgoal_tac "#1 $<= #3" 1);
+by (dres_inst_tac [("x", "#1"), ("y", "#3")] zle_trans 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
+by Auto_tac;
+(*Resulting state: n=1, p=false, m=4, u=false.
+ Execution of V1 (the command of process v guarded by n=1) sets p:=true,
+ violating the invariant!*)
+(*Check that subgoals remain: proof failed.*)
+getgoal 1;
+
+
+(*** Progress for U ***)
+
+Goalw [Unless_def]
+"Mutex : {s:state. s`m=#2} Unless {s:state. s`m=#3}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "U_F0";
+
+Goal "Mutex : {s:state. s`m=#1} LeadsTo {s:state. s`p = s`v & s`m = #2}";
+by (ensures_tac "U1" 1);
+by Auto_tac;
+qed "U_F1";
+
+Goal "Mutex : {s:state. s`p =0 & s`m = #2} LeadsTo {s:state. s`m = #3}";
+by (cut_facts_tac [IU] 1);
+by (ensures_tac "U2" 1);
+by Auto_tac;
+qed "U_F2";
+
+Goal "Mutex : {s:state. s`m = #3} LeadsTo {s:state. s`p=1}";
+by (res_inst_tac [("B", "{s:state. s`m = #4}")] LeadsTo_Trans 1);
+by (ensures_tac "U4" 2);
+by (ensures_tac "U3" 1);
+by Auto_tac;
+qed "U_F3";
+
+
+Goal "Mutex : {s:state. s`m = #2} LeadsTo {s:state. s`p=1}";
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
+ MRS LeadsTo_Diff) 1);
+by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
+by Auto_tac;
+by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def]));
+val U_lemma2 = result();
+
+Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`p =1}";
+by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
+by Auto_tac;
+val U_lemma1 = result();
+
+Goal "i:int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)";
+by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [neq_iff_zless]));
+by (dres_inst_tac [("j", "#3"), ("i", "i")] zle_zless_trans 4);
+by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 2);
+by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 1);
+by Auto_tac;
+by (rtac zle_anti_sym 1);
+by (ALLGOALS(asm_simp_tac (simpset()
+ addsimps [zless_add1_iff_zle RS iff_sym])));
+qed "eq_123";
+
+
+Goal "Mutex : {s:state. #1 $<= s`m & s`m $<= #3} LeadsTo {s:state. s`p=1}";
+by (simp_tac (simpset() addsimps [m_apply_type RS eq_123, Collect_disj_eq,
+ LeadsTo_Un_distrib,
+ U_lemma1, U_lemma2, U_F3] ) 1);
+val U_lemma123 = result();
+
+
+(*Misra's F4*)
+Goal "Mutex : {s:state. s`u = 1} LeadsTo {s:state. s`p=1}";
+by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
+by Auto_tac;
+qed "u_Leadsto_p";
+
+
+(*** Progress for V ***)
+
+Goalw [Unless_def]
+"Mutex : {s:state. s`n=#2} Unless {s:state. s`n=#3}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "V_F0";
+
+Goal "Mutex : {s:state. s`n=#1} LeadsTo {s:state. s`p = not(s`u) & s`n = #2}";
+by (ensures_tac "V1" 1);
+by (auto_tac (claset() addIs [not_type], simpset()));
+qed "V_F1";
+
+Goal "Mutex : {s:state. s`p=1 & s`n = #2} LeadsTo {s:state. s`n = #3}";
+by (cut_facts_tac [IV] 1);
+by (ensures_tac "V2" 1);
+by Auto_tac;
+qed "V_F2";
+
+Goal "Mutex : {s:state. s`n = #3} LeadsTo {s:state. s`p=0}";
+by (res_inst_tac [("B", "{s:state. s`n = #4}")] LeadsTo_Trans 1);
+by (ensures_tac "V4" 2);
+by (ensures_tac "V3" 1);
+by Auto_tac;
+qed "V_F3";
+
+
+Goal "Mutex : {s:state. s`n = #2} LeadsTo {s:state. s`p=0}";
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
+ MRS LeadsTo_Diff) 1);
+by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
+by Auto_tac;
+by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def]));
+val V_lemma2 = result();
+
+Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`p = 0}";
+by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
+by Auto_tac;
+val V_lemma1 = result();
+
+Goal "Mutex : {s:state. #1 $<= s`n & s`n $<= #3} LeadsTo {s:state. s`p = 0}";
+by (simp_tac (simpset() addsimps
+ [n_apply_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
+ V_lemma1, V_lemma2, V_F3] ) 1);
+val V_lemma123 = result();
+
+
+(*Misra's F4*)
+Goal "Mutex : {s:state. s`v = 1} LeadsTo {s:state. s`p = 0}";
+by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
+by Auto_tac;
+qed "v_Leadsto_not_p";
+
+(** Absence of starvation **)
+
+(*Misra's F6*)
+Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`m = #3}";
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac U_F2 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
+by (stac Un_commute 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
+by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
+by Auto_tac;
+by (auto_tac (claset() addSDs [v_apply_type], simpset() addsimps [bool_def]));
+qed "m1_Leadsto_3";
+
+
+(*The same for V*)
+Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`n = #3}";
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac V_F2 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
+by (stac Un_commute 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
+by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
+by Auto_tac;
+by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def]));
+qed "n1_Leadsto_3";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Mutex.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,86 @@
+(* Title: ZF/UNITY/Mutex.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+
+Variables' types are introduced globally so that type verification of
+UNITY programs/specifications reduce to the usual ZF typechecking.
+An ill-tyed expression will reduce to the empty set.
+*)
+
+Mutex = SubstAx +
+consts
+ p, m, n, u, v :: i
+
+translations
+ "p" == "Var([])"
+ "m" == "Var([0])"
+ "n" == "Var([1])"
+ "u" == "Var([1,0])"
+ "v" == "Var([1,1])"
+
+rules (** Type declarations **)
+ p_type "type_of(p)=bool"
+ m_type "type_of(m)=int"
+ n_type "type_of(n)=int"
+ u_type "type_of(u)=bool"
+ v_type "type_of(v)=bool"
+
+constdefs
+ (** The program for process U **)
+ U0 :: i
+ "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"
+
+ U1 :: i
+ "U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) & s`m = #1}"
+
+ U2 :: i
+ "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"
+
+ U3 :: i
+ "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"
+
+ U4 :: i
+ "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
+
+
+ (** The program for process V **)
+
+ V0 :: i
+ "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
+
+ V1 :: i
+ "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"
+
+ V2 :: i
+ "V2 == {<s,t>:state*state. t = s(n:=#3) & s`p=1 & s`n = #2}"
+
+ V3 :: i
+ "V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}"
+
+ V4 :: i
+ "V4 == {<s,t>:state*state. t = s (p:=0, n:=#0) & s`n = #4}"
+
+ Mutex :: i
+ "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
+ {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, action)"
+
+ (** The correct invariants **)
+
+ IU :: i
+ "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))
+ & (s`m = #3 --> s`p=0)}"
+
+ IV :: i
+ "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))
+ & (s`n = #3 --> s`p=1)}"
+
+ (** The faulty invariant (for U alone) **)
+
+ bad_IU :: i
+ "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m $<= #3))&
+ (#3 $<= s`m & s`m $<= #4 --> s`p=0)}"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/ROOT.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,13 @@
+(* Title: ZF/UNITY/ROOT
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Root file for ZF/UNITY proofs.
+*)
+
+(*Basic meta-theory*)
+time_use_thy "Guar";
+
+(*Simple examples: no composition*)
+time_use_thy"Mutex";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/State.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,210 @@
+(* Title: HOL/UNITY/State.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Formalizes UNITY-program states.
+*)
+
+AddIffs [some_in_state];
+
+
+Goal "!!A. state<=A ==> EX x. x:A";
+by (res_inst_tac [("x", "some")] exI 1);
+by Auto_tac;
+qed "state_subset_not_empty";
+
+(** condition **)
+Goalw [condition_def]
+ "A:condition ==>A<=state";
+by (Blast_tac 1);
+qed "conditionD";
+
+Goalw [condition_def]
+ "A<=state ==> A:condition";
+by (Blast_tac 1);
+qed "conditionI";
+
+(** actionSet **)
+Goalw [actionSet_def]
+"acts:actionSet ==> acts<=action";
+by (Blast_tac 1);
+qed "actionSetD";
+
+Goalw [actionSet_def]
+"acts<=action ==>acts:actionSet";
+by (Blast_tac 1);
+qed "actionSetI";
+
+(** Identity **)
+Goalw [condition_def, Identity_def]
+"A:condition ==> Id``A = A";
+by (Blast_tac 1);
+qed "Id_image";
+
+Goalw [Identity_def]
+"A<=state ==> Id``A = A";
+by (Blast_tac 1);
+qed "Id_image2";
+
+Addsimps [Id_image, Id_image2];
+
+Goalw [Identity_def]
+ "Id:action";
+by (Blast_tac 1);
+qed "Id_in_action";
+AddIffs [Id_in_action];
+AddTCs [Id_in_action];
+
+Goalw [Identity_def]
+ "(x:Id) <-> (EX c:state. x=<c,c>)";
+by (Blast_tac 1);
+qed "Id_member_simp";
+Addsimps [Id_member_simp];
+
+Goalw [Identity_def]
+"Id``0 = 0";
+by (Blast_tac 1);
+qed "Id_0";
+Addsimps [Id_0];
+
+
+Goalw [Identity_def]
+"Id``state = state";
+by (Blast_tac 1);
+qed "Id_image_state";
+Addsimps [Id_image_state];
+
+Goalw [condition_def]
+"0:condition";
+by (Blast_tac 1);
+qed "condition_0";
+
+Goalw [condition_def]
+"state:condition";
+by (Blast_tac 1);
+qed "condition_state";
+
+Goalw [actionSet_def]
+"0:actionSet";
+by Auto_tac;
+qed "actionSet_0";
+
+Goalw [actionSet_def]
+"action:actionSet";
+by Auto_tac;
+qed "actionSet_Prod";
+
+AddIffs [condition_0, condition_state, actionSet_0, actionSet_Prod];
+AddTCs [condition_0, condition_state, actionSet_0, actionSet_Prod];
+
+(** Simplification rules for condition **)
+
+
+(** Union and Un **)
+
+Goalw [condition_def]
+ "A Un B:condition <-> A:condition & B:condition";
+by (Blast_tac 1);
+qed "condition_Un";
+
+Goalw [condition_def]
+ "Union(S):condition <-> (ALL A:S. A:condition)";
+by (Blast_tac 1);
+qed "condition_Union";
+
+AddIffs [condition_Un, condition_Union];
+AddIs [condition_Un RS iffD2, condition_Union RS iffD2];
+
+(** Intersection **)
+
+Goalw [condition_def]
+ "[| A:condition; B:condition |] ==> A Int B: condition";
+by (Blast_tac 1);
+qed "condition_IntI";
+
+Goalw [condition_def, Inter_def]
+ "(ALL A:S. A:condition) ==> Inter(S): condition";
+by (Blast_tac 1);
+bind_thm("condition_InterI", ballI RS result());
+
+AddIs [condition_IntI, condition_InterI];
+Addsimps [condition_IntI, condition_InterI];
+
+Goalw [condition_def]
+"A:condition ==> A - B :condition";
+by (Blast_tac 1);
+qed "condition_DiffI";
+AddIs [condition_DiffI];
+Addsimps [condition_DiffI];
+
+
+(** Needed in WFair.thy **)
+Goalw [condition_def]
+"S:Pow(condition) ==> Union(S):condition";
+by (Blast_tac 1);
+qed "Union_in_conditionI";
+
+(** Simplification rules **)
+
+Goalw [condition_def]
+ "{s:state. P(s)}:condition";
+by Auto_tac;
+qed "Collect_in_condition";
+
+Goal "{s:state. P(s)}:Pow(state)";
+by Auto_tac;
+qed "Collect_condition2";
+
+Goal "{s:state. P(s)}<=state";
+by Auto_tac;
+qed "Collect_condition3";
+
+Goal "{s:state. P(s)} Int state = {s:state. P(s)}";
+by Auto_tac;
+qed "Collect_Int_state";
+
+Goal "state Int {s:state. P(s)} = {s:state. P(s)}";
+by Auto_tac;
+qed "Collect_Int_state2";
+
+val state_simps = [Collect_in_condition, Collect_condition2,
+Collect_condition3, Collect_Int_state, Collect_Int_state2];
+
+
+(* actionSet *)
+
+Goalw [actionSet_def]
+ "(A Un B):actionSet <-> (A:actionSet&B:actionSet)";
+by Auto_tac;
+qed "actionSet_Un";
+
+Goalw [actionSet_def]
+ "(UN i:I. A(i)):actionSet <-> (ALL i:I. A(i):actionSet)";
+by Auto_tac;
+qed "actionSet_UN";
+
+AddIffs [actionSet_Un, actionSet_UN];
+AddIs [actionSet_Un RS iffD2, actionSet_UN RS iffD2];
+
+Goalw [actionSet_def]
+"[| A:actionSet; B:actionSet |] ==> (A Int B):actionSet";
+by Auto_tac;
+qed "actionSet_Int";
+
+Goalw [actionSet_def]
+"(ALL i:I. A(i):actionSet) ==> (INT i:I. A(i)):actionSet";
+by (auto_tac (claset(), simpset() addsimps [Inter_def]));
+qed "actionSet_INT";
+
+Addsimps [actionSet_INT];
+AddIs [actionSet_INT];
+Addsimps [Inter_0];
+
+Goalw [condition_def]
+ "(PROD x:variable. type_of(x)):condition";
+by Auto_tac;
+qed "PROD_condition";
+
+Addsimps [PROD_condition];
+AddIs [PROD_condition];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/State.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,60 @@
+(* Title: HOL/UNITY/State.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Formalizes UNITY-program states using dependent types:
+ - variables are typed.
+ - the state space is uniform, common to all defined programs.
+ - variables can be quantified over.
+
+*)
+
+State = UNITYMisc +
+
+consts
+ variable :: i
+
+(**
+ Variables are better represented using integers, but at the moment
+ there is a problem with integer translations like "uu" == "Var(#0)", which
+ are needed to give names to variables.
+ So for the time being we are using lists of naturals to index variables.
+ **)
+
+datatype variable = Var("i:list(nat)")
+ type_intrs "[list_nat_into_univ]"
+
+consts
+ state, action, some ::i
+ type_of :: i=>i
+
+translations
+ (* The state space is a dependent type *)
+ "state" == "Pi(variable, type_of)"
+
+ (* Commands are relations over states *)
+ "action" == "Pow(state*state)"
+
+rules
+ (** We might have defined the state space in a such way that it is already
+ not empty by formation: for example "state==PROD x:variable. type_of(x) Un {0}"
+ which contains the function (lam x:variable. 0) is a possible choice.
+ However, we prefer the following way for simpler proofs by avoiding
+ case splitting resulting from type_of(x) Un {0}. **)
+
+ some_in_state "some:state"
+
+constdefs
+ (* State conditions/predicates are sets of states *)
+ condition :: i
+ "condition == Pow(state)"
+
+ actionSet :: i
+ "actionSet == Pow(action)"
+
+consts
+ Id :: i
+translations
+ "Id" == "Identity(state)"
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/SubstAx.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,486 @@
+(* Title: ZF/UNITY/SubstAx.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+LeadsTo relation, restricted to the set of reachable states.
+
+*)
+
+
+(*Resembles the previous definition of LeadsTo*)
+
+Goalw [LeadsTo_def]
+ "A LeadsTo B = \
+\ {F:program. F : (reachable(F) Int A) leadsTo (reachable(F) Int B) & \
+\ A:condition & B:condition}";
+by (blast_tac (claset() addDs [psp_stable2, leadsToD, constrainsD2]
+ addIs [leadsTo_weaken]) 1);
+qed "LeadsTo_eq_leadsTo";
+
+Goalw [LeadsTo_def]
+"F: A LeadsTo B ==> F:program & A:condition & B:condition";
+by (Blast_tac 1);
+qed "LeadsToD";
+
+(*** Specialized laws for handling invariants ***)
+
+(** Conjoining an Always property **)
+Goal "[| F : Always(INV); A:condition |] ==> \
+\ (F : (INV Int A) LeadsTo A') <-> (F : A LeadsTo A')";
+by (asm_full_simp_tac
+ (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
+ Int_absorb2, Int_assoc RS sym, leadsToD]) 1);
+qed "Always_LeadsTo_pre";
+
+Goal "[| F : Always(INV); A':condition |] \
+ \ ==> (F : A LeadsTo (INV Int A')) <-> (F : A LeadsTo A')";
+by (asm_full_simp_tac
+ (simpset() addsimps [LeadsTo_eq_leadsTo, Always_eq_includes_reachable,
+ Int_absorb2, Int_assoc RS sym,leadsToD]) 1);
+qed "Always_LeadsTo_post";
+
+(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
+Goal "[| F:Always(C); F : (C Int A) LeadsTo A'; A:condition |] \
+\ ==> F: A LeadsTo A'";
+by (blast_tac (claset() addIs [Always_LeadsTo_pre RS iffD1]) 1);
+qed "Always_LeadsToI";
+
+(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
+Goal
+"[| F : Always(C); F : A LeadsTo A'; A':condition |] \
+\ ==> F : A LeadsTo (C Int A')";
+by (blast_tac (claset() addIs [Always_LeadsTo_post RS iffD2]) 1);
+qed "Always_LeadsToD";
+
+(*** Introduction rules: Basis, Trans, Union ***)
+
+Goal "F : A leadsTo B ==> F : A LeadsTo B";
+by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
+by (blast_tac (claset() addIs [leadsTo_weaken_L]
+ addDs [leadsToD]) 1);
+qed "leadsTo_imp_LeadsTo";
+
+Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C";
+by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
+qed "LeadsTo_Trans";
+
+Goalw [LeadsTo_def]
+ "[| ALL A:S. F : A LeadsTo B; F:program; B:condition |] \
+\ ==> F : Union(S) LeadsTo B";
+by Auto_tac;
+by (stac Int_Union_Union2 1);
+by (blast_tac (claset() addIs [leadsTo_UN]) 1);
+bind_thm("LeadsTo_Union", ballI RS result());
+
+
+(*** Derived rules ***)
+
+Goalw [LeadsTo_def]
+"[| F:program; A:condition |] ==>F : A LeadsTo state";
+by (blast_tac (claset() addIs [leadsTo_state]) 1);
+qed "LeadsTo_state";
+Addsimps [LeadsTo_state];
+
+(*Useful with cancellation, disjunction*)
+Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "LeadsTo_Un_duplicate";
+
+Goal "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "LeadsTo_Un_duplicate2";
+
+Goal "[| ALL i:I. F : A(i) LeadsTo B; F:program; B:condition |] \
+\ ==> F : (UN i:I. A(i)) LeadsTo B";
+by (simp_tac (simpset() addsimps [Int_Union_Union]) 1);
+by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
+bind_thm("LeadsTo_UN", ballI RS result());
+
+(*Binary union introduction rule*)
+Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C";
+by (stac Un_eq_Union 1);
+by (blast_tac (claset() addIs [LeadsTo_Union]
+ addDs [LeadsToD]) 1);
+qed "LeadsTo_Un";
+
+(*Lets us look at the starting state*)
+Goal "[| ALL s:A. F : {s} LeadsTo B; F:program; B:condition |]\
+\ ==> F : A LeadsTo B";
+by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1);
+by (REPEAT(Blast_tac 1));
+bind_thm("single_LeadsTo_I", ballI RS result());
+
+Goal "[| A <= B; B:condition; F:program |] ==> F : A LeadsTo B";
+by (subgoal_tac "A:condition" 1);
+by (force_tac (claset(),
+ simpset() addsimps [condition_def]) 2);
+by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+qed "subset_imp_LeadsTo";
+
+bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
+Addsimps [empty_LeadsTo];
+
+Goal "[| F : A LeadsTo A'; A' <= B'; B':condition |] ==> F : A LeadsTo B'";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
+by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
+qed_spec_mp "LeadsTo_weaken_R";
+
+
+Goal "[| F : A LeadsTo A'; B <= A |] \
+\ ==> F : B LeadsTo A'";
+by (subgoal_tac "B:condition" 1);
+by (force_tac (claset() addSDs [LeadsToD],
+ simpset() addsimps [condition_def]) 2);
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
+by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
+qed_spec_mp "LeadsTo_weaken_L";
+
+Goal "[| F : A LeadsTo A'; \
+\ B <= A; A' <= B'; B':condition |] \
+\ ==> F : B LeadsTo B'";
+by (blast_tac (claset() addIs [LeadsTo_weaken_R,
+ LeadsTo_weaken_L, LeadsTo_Trans]) 1);
+qed "LeadsTo_weaken";
+
+Goal "[| F : Always(C); F : A LeadsTo A'; \
+\ C Int B <= A; C Int A' <= B'; B:condition; B':condition |] \
+\ ==> F : B LeadsTo B'";
+by (blast_tac (claset()
+ addDs [AlwaysD2, LeadsToD, Always_LeadsToI]
+ addIs [LeadsTo_weaken, Always_LeadsToD]) 1);
+qed "Always_LeadsTo_weaken";
+
+(** Two theorems for "proof lattices" **)
+
+Goal "F : A LeadsTo B ==> F:(A Un B) LeadsTo B";
+by (blast_tac (claset()
+ addIs [LeadsTo_Un, subset_imp_LeadsTo]
+ addDs [LeadsToD]) 1);
+qed "LeadsTo_Un_post";
+
+Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \
+\ ==> F : (A Un B) LeadsTo C";
+by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
+ LeadsTo_weaken_L, LeadsTo_Trans]
+ addDs [LeadsToD]) 1);
+qed "LeadsTo_Trans_Un";
+
+
+(** Distributive laws **)
+
+Goal "(F : (A Un B) LeadsTo C) <-> (F : A LeadsTo C & F : B LeadsTo C)";
+by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
+qed "LeadsTo_Un_distrib";
+
+Goal "[| F:program; B:condition |] ==> \
+\ (F : (UN i:I. A(i)) LeadsTo B) <-> (ALL i : I. F : A(i) LeadsTo B)";
+by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
+qed "LeadsTo_UN_distrib";
+
+Goal "[| F:program; B:condition |] ==> \
+\ (F : Union(S) LeadsTo B) <-> (ALL A : S. F : A LeadsTo B)";
+by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
+qed "LeadsTo_Union_distrib";
+
+(** More rules using the premise "Always INV" **)
+
+Goal "F : A Ensures B ==> F : A LeadsTo B";
+by (asm_full_simp_tac
+ (simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1);
+qed "LeadsTo_Basis";
+
+Goal "[| F : (A-B) Co (A Un B); F : transient (A-B) |] \
+\ ==> F : A Ensures B";
+by (asm_full_simp_tac
+ (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
+by (blast_tac (claset() addIs [ensuresI, constrains_weaken,
+ transient_strengthen]
+ addDs [constrainsD2]) 1);
+qed "EnsuresI";
+
+Goal "[| F : Always(INV); \
+\ F : (INV Int (A-A')) Co (A Un A'); \
+\ F : transient (INV Int (A-A')) |] \
+\ ==> F : A LeadsTo A'";
+by (rtac Always_LeadsToI 1);
+by (assume_tac 1);
+by (blast_tac (claset() addDs [ConstrainsD]) 2);
+by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
+ Always_ConstrainsD RS Constrains_weaken,
+ transient_strengthen]
+ addDs [AlwaysD2, ConstrainsD]) 1);
+qed "Always_LeadsTo_Basis";
+
+(*Set difference: maybe combine with leadsTo_weaken_L??
+ This is the most useful form of the "disjunction" rule*)
+Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C; \
+\ A:condition; B:condition |] \
+\ ==> F : A LeadsTo C";
+by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]
+ addDs [LeadsToD]) 1);
+qed "LeadsTo_Diff";
+
+
+Goal "[| ALL i:I. F: A(i) LeadsTo A'(i); F:program |] \
+\ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))";
+by (rtac LeadsTo_Union 1);
+by (ALLGOALS(Clarify_tac));
+by (blast_tac (claset() addDs [LeadsToD]) 2);
+by (blast_tac (claset() addIs [LeadsTo_weaken_R]
+ addDs [LeadsToD]) 1);
+bind_thm ("LeadsTo_UN_UN", ballI RS result());
+
+
+(*Version with no index set*)
+Goal "[| ALL i. F: A(i) LeadsTo A'(i); F:program |] \
+\ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))";
+by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
+qed "all_LeadsTo_UN_UN";
+
+bind_thm ("LeadsTo_UN_UN_noindex", allI RS all_LeadsTo_UN_UN);
+
+(*Binary union version*)
+Goal "[| F : A LeadsTo A'; F : B LeadsTo B' |] \
+\ ==> F : (A Un B) LeadsTo (A' Un B')";
+by (blast_tac (claset()
+ addIs [LeadsTo_Un, LeadsTo_weaken_R]
+ addDs [LeadsToD]) 1);
+qed "LeadsTo_Un_Un";
+
+(** The cancellation law **)
+
+Goal "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |] \
+\ ==> F : A LeadsTo (A' Un B')";
+by (blast_tac (claset() addIs [LeadsTo_Un_Un,
+ subset_imp_LeadsTo, LeadsTo_Trans]
+ addDs [LeadsToD]) 1);
+qed "LeadsTo_cancel2";
+
+Goal "A Un (B - A) = A Un B";
+by Auto_tac;
+qed "Un_Diff";
+
+Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] \
+\ ==> F : A LeadsTo (A' Un B')";
+by (rtac LeadsTo_cancel2 1);
+by (assume_tac 2);
+by (asm_simp_tac (simpset() addsimps [Un_Diff]) 1);
+qed "LeadsTo_cancel_Diff2";
+
+Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] \
+\ ==> F : A LeadsTo (B' Un A')";
+by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
+by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
+qed "LeadsTo_cancel1";
+
+
+Goal "(B - A) Un A = B Un A";
+by Auto_tac;
+qed "Diff_Un2";
+
+Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] \
+\ ==> F : A LeadsTo (B' Un A')";
+by (rtac LeadsTo_cancel1 1);
+by (assume_tac 2);
+by (asm_simp_tac (simpset() addsimps [Diff_Un2]) 1);
+qed "LeadsTo_cancel_Diff1";
+
+
+(** The impossibility law **)
+
+(*The set "A" may be non-empty, but it contains no reachable states*)
+Goal "F : A LeadsTo 0 ==> F : Always (state -A)";
+by (full_simp_tac (simpset()
+ addsimps [LeadsTo_def,Always_eq_includes_reachable]) 1);
+by (Clarify_tac 1);
+by (forward_tac [reachableD] 1);
+by (auto_tac (claset() addSDs [leadsTo_empty],
+ simpset() addsimps [condition_def]));
+qed "LeadsTo_empty";
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction"*)
+Goal "[| F : A LeadsTo A'; F : Stable(B) |] \
+\ ==> F : (A Int B) LeadsTo (A' Int B)";
+by (forward_tac [StableD2] 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1);
+by (Clarify_tac 1);
+by (dtac psp_stable 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps (Int_absorb::Int_ac)) 1);
+qed "PSP_Stable";
+
+Goal "[| F : A LeadsTo A'; F : Stable(B) |] \
+\ ==> F : (B Int A) LeadsTo (B Int A')";
+by (asm_simp_tac (simpset() addsimps PSP_Stable::Int_ac) 1);
+qed "PSP_Stable2";
+
+Goal "[| F : A LeadsTo A'; F : B Co B' |] \
+\ ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))";
+by (full_simp_tac
+ (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
+by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
+qed "PSP";
+
+Goal "[| F : A LeadsTo A'; F : B Co B' |] \
+\ ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))";
+by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
+qed "PSP2";
+
+
+Goal
+"[| F : A LeadsTo A'; F : B Unless B' |] \
+\ ==> F : (A Int B) LeadsTo ((A' Int B) Un B')";
+by (forward_tac [LeadsToD] 1);
+by (forward_tac [UnlessD] 1);
+by (rewrite_goals_tac [Unless_def]);
+by (dtac PSP 1);
+by (assume_tac 1);
+by (blast_tac (claset()
+ addIs [LeadsTo_Diff,
+ LeadsTo_weaken, subset_imp_LeadsTo]) 1);
+qed "PSP_Unless";
+
+(*** Induction rules ***)
+
+(** Meta or object quantifier ????? **)
+Goal "[| wf(r); \
+\ ALL m:I. F : (A Int f-``{m}) LeadsTo \
+\ ((A Int f-``(converse(r) `` {m})) Un B); \
+\ field(r)<=I; A<=f-``I; F:program; A:condition; B:condition |] \
+\ ==> F : A LeadsTo B";
+by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
+by Safe_tac;
+by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1);
+by (ALLGOALS(Clarify_tac));
+by (dres_inst_tac [("x", "m")] bspec 4);
+by Safe_tac;
+by (res_inst_tac [("A'",
+ "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")]
+ leadsTo_weaken_R 4);
+by (asm_simp_tac (simpset() addsimps [Int_assoc]) 4);
+by (asm_simp_tac (simpset() addsimps [Int_assoc]) 5);
+by (REPEAT(Blast_tac 1));
+qed "LeadsTo_wf_induct";
+
+
+
+Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``lessThan(m,nat)) Un B); \
+\ A<=f-``nat; F:program; A:condition; B:condition |] \
+\ ==> F : A LeadsTo B";
+by (res_inst_tac [("A1", "nat"), ("I", "nat")] (wf_less_than RS LeadsTo_wf_induct) 1);
+by (ALLGOALS(asm_full_simp_tac
+ (simpset() addsimps [nat_less_than_field])));
+by (Clarify_tac 1);
+by (ALLGOALS(asm_full_simp_tac
+ (simpset() addsimps [rewrite_rule [vimage_def] Image_inverse_less_than])));
+qed "LessThan_induct";
+
+
+(******
+ To be ported ??? I am not sure.
+
+ integ_0_le_induct
+ LessThan_bounded_induct
+ GreaterThan_bounded_induct
+
+*****)
+
+(*** Completion: Binary and General Finite versions ***)
+
+Goal "[| F : A LeadsTo (A' Un C); F : A' Co (A' Un C); \
+\ F : B LeadsTo (B' Un C); F : B' Co (B' Un C) |] \
+\ ==> F : (A Int B) LeadsTo ((A' Int B') Un C)";
+by (full_simp_tac
+ (simpset() addsimps [LeadsTo_eq_leadsTo, Constrains_eq_constrains,
+ Int_Un_distrib2 RS sym]) 1);
+by Safe_tac;
+by (REPEAT(Blast_tac 2));
+by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
+qed "Completion";
+
+
+Goal "[| I:Fin(X);F:program; C:condition |] \
+\ ==> (ALL i:I. F : (A(i)) LeadsTo (A'(i) Un C)) --> \
+\ (ALL i:I. F : (A'(i)) Co (A'(i) Un C)) --> \
+\ F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)";
+by (etac Fin_induct 1);
+by Auto_tac;
+by (case_tac "y=0" 1);
+by Auto_tac;
+by (etac not_emptyE 1);
+by (subgoal_tac "Inter(cons(A(x), RepFun(y, A)))= A(x) Int Inter(RepFun(y,A)) &\
+ \ Inter(cons(A'(x), RepFun(y, A')))= A'(x) Int Inter(RepFun(y,A'))" 1);
+by (Blast_tac 2);
+by (Asm_simp_tac 1);
+by (rtac Completion 1);
+by (subgoal_tac "Inter(RepFun(y, A')) Un C = (INT x:RepFun(y, A'). x Un C)" 4);
+by (Blast_tac 5);
+by (Asm_simp_tac 4);
+by (rtac Constrains_INT 4);
+by (REPEAT(Blast_tac 1));
+val lemma = result();
+
+
+val prems = Goal
+ "[| I:Fin(X); !!i. i:I ==> F : A(i) LeadsTo (A'(i) Un C); \
+\ !!i. i:I ==> F : A'(i) Co (A'(i) Un C); \
+\ F:program; C:condition |] \
+\ ==> F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)";
+by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
+qed "Finite_completion";
+
+Goalw [Stable_def]
+ "[| F : A LeadsTo A'; F : Stable(A'); \
+\ F : B LeadsTo B'; F : Stable(B') |] \
+\ ==> F : (A Int B) LeadsTo (A' Int B')";
+by (res_inst_tac [("C1", "0")] (Completion RS LeadsTo_weaken_R) 1);
+by (REPEAT(blast_tac (claset() addDs [LeadsToD,ConstrainsD]) 5));
+by (ALLGOALS(Asm_full_simp_tac));
+qed "Stable_completion";
+
+
+val prems = Goalw [Stable_def]
+ "[| I:Fin(X); \
+\ ALL i:I. F : A(i) LeadsTo A'(i); \
+\ ALL i:I. F: Stable(A'(i)); F:program |] \
+\ ==> F : (INT i:I. A(i)) LeadsTo (INT i:I. A'(i))";
+by (subgoal_tac "(INT i:I. A'(i)):condition" 1);
+by (blast_tac (claset() addDs [LeadsToD,ConstrainsD]) 2);
+by (res_inst_tac [("C1", "0")] (Finite_completion RS LeadsTo_weaken_R) 1);
+by (assume_tac 7);
+by (ALLGOALS(Asm_full_simp_tac));
+by (ALLGOALS (Blast_tac));
+qed "Finite_stable_completion";
+
+
+(*proves "ensures/leadsTo" properties when the program is specified*)
+fun ensures_tac sact =
+ SELECT_GOAL
+ (EVERY [REPEAT (Always_Int_tac 1),
+ etac Always_LeadsTo_Basis 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
+ EnsuresI, ensuresI] 1),
+ (*now there are two subgoals: co & transient*)
+ simp_tac (simpset() addsimps !program_defs_ref) 2,
+ res_inst_tac [("act", sact)] transientI 2,
+ (*simplify the command's domain*)
+ simp_tac (simpset() addsimps [domain_def]) 3,
+ (* proving the domain part *)
+ Clarify_tac 3, dtac swap 3, Force_tac 4,
+ rtac ReplaceI 3, Force_tac 3, Force_tac 4,
+ Asm_full_simp_tac 3, rtac conjI 3, Simp_tac 4,
+ REPEAT (rtac update_type2 3),
+ constrains_tac 1,
+ ALLGOALS Clarify_tac,
+ ALLGOALS (asm_full_simp_tac
+ (simpset() addsimps [condition_def])),
+ ALLGOALS Clarify_tac]);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/SubstAx.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,25 @@
+(* Title: ZF/UNITY/SubstAx.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Weak LeadsTo relation (restricted to the set of reachable states)
+
+Theory ported from HOL.
+*)
+
+SubstAx = WFair + Constrains +
+
+constdefs
+ Ensures :: "[i,i] => i" (infixl 60)
+ "A Ensures B == {F:program. F : (reachable(F) Int A) ensures B &
+ A:condition & B:condition}"
+
+ LeadsTo :: "[i, i] => i" (infixl 60)
+ "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo B &
+ A:condition & B:condition}"
+
+syntax (xsymbols)
+ "op LeadsTo" :: "[i, i] => i" (infixl " \\<longmapsto>w " 60)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/UNITY.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,792 @@
+(* Title: ZF/UNITY/UNITY.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+The basic UNITY theory (revised version, based upon the "co" operator)
+From Misra, "A Logic for Concurrent Programming", 1994
+
+Proofs ported from HOL
+*)
+
+(** SKIP **)
+Goal "SKIP:program";
+by (auto_tac (claset(), simpset() addsimps
+ [SKIP_def, program_def, mk_program_def, actionSet_def, cons_absorb]));
+qed "SKIP_type";
+AddIffs [SKIP_type];
+AddTCs [SKIP_type];
+
+(** programify: coersion from anything to program **)
+
+Goalw [programify_def]
+"F:program ==> programify(F)=F";
+by Auto_tac;
+qed "programify_program";
+Addsimps [programify_program];
+
+Goalw [programify_def]
+"programify(F):program";
+by Auto_tac;
+qed "programify_in_program";
+AddIffs [programify_in_program];
+AddTCs [programify_in_program];
+
+(** Collapsing rules: to remove programify from expressions **)
+Goalw [programify_def]
+"programify(programify(F))=programify(F)";
+by Auto_tac;
+qed "programify_idem";
+Addsimps [programify_idem];
+
+Goal
+"Init(programify(F)) = Init(F)";
+by (simp_tac (simpset() addsimps [Init_def]) 1);
+qed "Init_programify";
+
+Goal
+"Acts(programify(F)) = Acts(F)";
+by (simp_tac (simpset() addsimps [Acts_def]) 1);
+qed "Acts_programify";
+
+Goal
+"AllowedActs(programify(F)) = AllowedActs(F)";
+by (simp_tac (simpset() addsimps [AllowedActs_def]) 1);
+qed "AllowedActs_programify";
+
+Addsimps [Init_programify,Acts_programify,AllowedActs_programify];
+
+(** program inspectors **)
+
+Goal "F:program ==>Id:RawActs(F)";
+by (auto_tac (claset(), simpset()
+ addsimps [program_def, RawActs_def]));
+qed "Id_in_RawActs";
+
+Goal "Id:Acts(F)";
+by (simp_tac (simpset()
+ addsimps [Id_in_RawActs, Acts_def]) 1);
+qed "Id_in_Acts";
+
+Goal "F:program ==>Id:RawAllowedActs(F)";
+by (auto_tac (claset(), simpset()
+ addsimps [program_def, RawAllowedActs_def]));
+qed "Id_in_RawAllowedActs";
+
+Goal "Id:AllowedActs(F)";
+by (simp_tac (simpset()
+ addsimps [Id_in_RawAllowedActs, AllowedActs_def]) 1);
+qed "Id_in_AllowedActs";
+
+AddIffs [Id_in_Acts, Id_in_AllowedActs];
+AddTCs [Id_in_Acts, Id_in_AllowedActs];
+
+Goal "cons(Id, Acts(F)) = Acts(F)";
+by (simp_tac (simpset() addsimps [cons_absorb]) 1);
+qed "cons_Id_Acts";
+
+Goal "cons(Id, AllowedActs(F)) = AllowedActs(F)";
+by (simp_tac (simpset() addsimps [cons_absorb]) 1);
+qed "cons_Id_AllowedActs";
+
+Addsimps [cons_Id_Acts, cons_Id_AllowedActs];
+
+(** inspectors's types **)
+Goal
+"F:program ==> RawInit(F):condition";
+by (auto_tac (claset(), simpset()
+ addsimps [program_def, RawInit_def]));
+qed "RawInit_type";
+
+Goal "Init(F):condition";
+by (simp_tac (simpset()
+ addsimps [RawInit_type, Init_def]) 1);
+qed "Init_type";
+
+Goal
+"F:program ==> RawActs(F):actionSet";
+by (auto_tac (claset(), simpset()
+ addsimps [program_def, RawActs_def, actionSet_def]));
+qed "RawActs_type";
+
+Goal
+"Acts(F):actionSet";
+by (simp_tac (simpset()
+ addsimps [RawActs_type, Acts_def]) 1);
+qed "Acts_type";
+
+Goal
+"F:program ==> RawAllowedActs(F):actionSet";
+by (auto_tac (claset(), simpset()
+ addsimps [program_def, RawAllowedActs_def, actionSet_def]));
+qed "RawAllowedActs_type";
+
+Goal
+"AllowedActs(F): actionSet";
+by (simp_tac (simpset()
+ addsimps [RawAllowedActs_type, AllowedActs_def]) 1);
+qed "AllowedActs_type";
+
+AddIffs [Init_type, Acts_type, AllowedActs_type];
+AddTCs [Init_type, Acts_type, AllowedActs_type];
+
+Goal "x:Init(F) ==> x:state";
+by (cut_inst_tac [("F", "F")] Init_type 1);
+by (auto_tac (claset(), simpset() addsimps [condition_def]));
+qed "InitD";
+
+Goal "act:Acts(F) ==> act<=state*state";
+by (cut_inst_tac [("F", "F")] Acts_type 1);
+by (rewrite_goals_tac [actionSet_def]);
+by Auto_tac;
+qed "ActsD";
+
+
+Goal "act:AllowedActs(F) ==> act<=state*state";
+by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
+by (rewrite_goals_tac [actionSet_def]);
+by Auto_tac;
+qed "AllowedActsD";
+
+(** More simplification rules involving state
+ and Init, Acts, and AllowedActs **)
+
+Goal "state <= Init(F) <-> Init(F)=state";
+by (cut_inst_tac [("F", "F")] Init_type 1);
+by (auto_tac (claset(),
+ simpset() addsimps [condition_def]));
+qed "Init_state_eq";
+
+Goal "action <= Acts(F) <-> Acts(F)=action";
+by (cut_inst_tac [("F", "F")] Acts_type 1);
+by (auto_tac (claset(),
+ simpset() addsimps [actionSet_def]));
+qed "Acts_action_eq";
+
+Goal "action <= AllowedActs(F) <-> AllowedActs(F)=action";
+by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
+by (auto_tac (claset(),
+ simpset() addsimps [actionSet_def]));
+qed "AllowedActs_action_eq";
+
+(** Eliminating `Int state' from expressions **)
+Goal
+"Init(F) Int state = Init(F)";
+by (cut_inst_tac [("F", "F")] Init_type 1);
+by (auto_tac (claset(),
+ simpset() addsimps [condition_def]));
+qed "Init_Int_state";
+
+Goal
+"state Int Init(F) = Init(F)";
+by (stac (Int_commute) 1);
+by (simp_tac (simpset()
+ addsimps [Init_Int_state]) 1);
+qed "Init_Int_state2";
+
+Goal
+"Acts(F) Int action = Acts(F)";
+by (cut_inst_tac [("F", "F")] Acts_type 1);
+by (auto_tac (claset(),
+ simpset() addsimps [actionSet_def]));
+qed "Acts_Int_action";
+
+Goal
+"action Int Acts(F) = Acts(F)";
+by (simp_tac (simpset() addsimps
+ [Int_commute, Acts_Int_action]) 1);
+qed "Acts_Int_action2";
+
+Goal
+"AllowedActs(F) Int action = AllowedActs(F)";
+by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
+by (auto_tac (claset(),
+ simpset() addsimps [actionSet_def]));
+qed "AllowedActs_Int_action";
+
+Goal
+"action Int AllowedActs(F) = AllowedActs(F)";
+by (simp_tac (simpset() addsimps
+ [Int_commute, AllowedActs_Int_action]) 1);
+qed "AllowedActs_Int_action2";
+
+Addsimps
+[Init_state_eq, Acts_action_eq, AllowedActs_action_eq,
+ Init_Int_state, Init_Int_state2, Acts_Int_action, Acts_Int_action2,
+ AllowedActs_Int_action,AllowedActs_Int_action2];
+
+(** mk_program **)
+
+Goal "mk_program(init, acts, allowed):program";
+by (auto_tac (claset(), simpset()
+ addsimps [program_def, mk_program_def, condition_def, actionSet_def]));
+qed "mk_program_type";
+AddIffs [mk_program_type];
+AddTCs [mk_program_type];
+
+Goal "RawInit(mk_program(init, acts, allowed)) = init Int state";
+by (auto_tac (claset(), simpset()
+ addsimps [RawInit_def, mk_program_def]));
+qed "RawInit_eq";
+
+Goal "Init(mk_program(init, acts, allowed)) = init Int state";
+by (auto_tac (claset(), simpset()
+ addsimps [Init_def, RawInit_eq]));
+qed "Init_eq";
+Addsimps [Init_eq];
+
+Goalw [RawActs_def]
+"RawActs(mk_program(init, acts, allowed)) \
+\ = cons(Id, acts Int Pow(state*state))";
+by (auto_tac (claset(), simpset()
+ addsimps [mk_program_def]));
+qed "RawActs_eq";
+
+Goalw [Acts_def]
+"Acts(mk_program(init, acts, allowed)) \
+ \ = cons(Id, acts Int Pow(state*state))";
+by (auto_tac (claset(),
+ simpset() addsimps [RawActs_eq]));
+qed "Acts_eq";
+Addsimps [Acts_eq];
+
+Goalw [RawAllowedActs_def]
+"RawAllowedActs(mk_program(init, acts, allowed)) \
+\ = cons(Id, allowed Int action)";
+by (auto_tac (claset(),
+ simpset() addsimps [mk_program_def]));
+qed "RawAllowedActs_eq";
+
+Goalw [AllowedActs_def]
+"AllowedActs(mk_program(init, acts, allowed)) \
+\ = cons(Id, allowed Int action)";
+by (auto_tac (claset(),
+ simpset() addsimps [RawAllowedActs_eq]));
+qed "AllowedActs_eq";
+Addsimps [AllowedActs_eq];
+
+
+(**Init, Acts, and AlowedActs of SKIP **)
+
+Goal "RawInit(SKIP) = state";
+by (auto_tac (claset(), simpset()
+ addsimps [SKIP_def, RawInit_eq]));
+qed "RawInit_SKIP";
+
+Goal "Init(SKIP) = state";
+by (simp_tac (simpset()
+ addsimps [Init_def, RawInit_SKIP]) 1);
+qed "Init_SKIP";
+Addsimps [Init_SKIP];
+
+Goal "RawActs(SKIP) = {Id}";
+by (auto_tac (claset(), simpset()
+ addsimps [SKIP_def, RawActs_eq]));
+qed "RawActs_SKIP";
+
+
+Goal "Acts(SKIP) = {Id}";
+by (simp_tac (simpset()
+ addsimps [Acts_def, RawActs_SKIP]) 1);
+qed "Acts_SKIP";
+Addsimps [Acts_SKIP];
+
+Goal "RawAllowedActs(SKIP) = action";
+by (auto_tac (claset(), simpset()
+ addsimps [SKIP_def, RawAllowedActs_eq]));
+qed "RawAllowedActs_SKIP";
+
+Goal "AllowedActs(SKIP) = action";
+by (simp_tac (simpset()
+ addsimps [AllowedActs_def, RawAllowedActs_SKIP]) 1);
+qed "AllowedActs_SKIP";
+Addsimps [AllowedActs_SKIP];
+
+(** Equality for UNITY programs **)
+
+Goal
+"F:program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F";
+by (auto_tac (claset(), simpset() addsimps
+ [program_def, mk_program_def, RawInit_def,
+ RawActs_def, RawAllowedActs_def, actionSet_def, condition_def]));
+by (REPEAT(Blast_tac 1));
+qed "raw_surjective_mk_program";
+
+Goal
+ "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)";
+by (auto_tac (claset(), simpset() addsimps
+ [Init_def, Acts_def, AllowedActs_def,
+ raw_surjective_mk_program]));
+qed "surjective_mk_program";
+
+
+Goal "[|Init(F) = Init(G); Acts(F) = Acts(G); \
+\ AllowedActs(F) = AllowedActs(G); F:program; G:program |] ==> F = G";
+by (stac (programify_program RS sym) 1);
+by (rtac sym 2);
+by (stac (programify_program RS sym) 2);
+by (stac (surjective_mk_program RS sym) 3);
+by (stac (surjective_mk_program RS sym) 3);
+by (ALLGOALS(Asm_simp_tac));
+qed "program_equalityI";
+
+val [major,minor] =
+Goal "[| F = G; \
+\ [| Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]\
+\ ==> P |] ==> P";
+by (rtac minor 1);
+by (auto_tac (claset(), simpset() addsimps [major]));
+qed "program_equalityE";
+
+
+Goal "[| F:program; G:program |] ==>(F=G) <-> \
+\ (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))";
+by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
+qed "program_equality_iff";
+
+Addsimps [surjective_mk_program];
+
+(*** These rules allow "lazy" definition expansion
+
+...skipping 1 line
+
+***)
+
+Goal "F == mk_program (init,acts,allowed) ==> Init(F) = init Int state";
+by Auto_tac;
+qed "def_prg_Init";
+
+
+Goal "F == mk_program (init,acts,allowed) ==> Acts(F) = cons(Id, acts Int action)";
+by Auto_tac;
+qed "def_prg_Acts";
+
+
+Goal "F == mk_program (init,acts,allowed) ==> \
+\ AllowedActs(F) = cons(Id, allowed Int action)";
+by Auto_tac;
+qed "def_prg_AllowedActs";
+
+
+val [rew] = goal thy
+ "[| F == mk_program (init,acts,allowed) |] \
+\ ==> Init(F) = init Int state & Acts(F) = cons(Id, acts Int action)";
+by (rewtac rew);
+by Auto_tac;
+qed "def_prg_simps";
+
+
+(*An action is expanded only if a pair of states is being tested against it*)
+Goal "[| act == {<s,s'>:A*B. P(s, s')} |] ==> \
+\ (<s,s'>:act) <-> (<s,s'>:A*B & P(s, s'))";
+by Auto_tac;
+qed "def_act_simp";
+
+fun simp_of_act def = def RS def_act_simp;
+
+(*A set is expanded only if an element is being tested against it*)
+Goal "A == B ==> (x : A) <-> (x : B)";
+by Auto_tac;
+qed "def_set_simp";
+
+fun simp_of_set def = def RS def_set_simp;
+
+(*** co ***)
+
+val prems = Goalw [constrains_def]
+ "[|(!!act s s'. [| act: Acts(F); <s,s'>:act; s:A|] ==> s':A'); \
+ \ F:program; A:condition; A':condition |] ==> F:A co A'";
+by (blast_tac(claset() addIs prems) 1);
+qed "constrainsI";
+
+Goalw [constrains_def]
+ "F:A co B ==> ALL act:Acts(F). act``A<=B";
+by (Blast_tac 1);
+qed "constrainsD";
+
+Goalw [constrains_def]
+ "F:A co B ==> F:program & A:condition & B:condition";
+by (Blast_tac 1);
+qed "constrainsD2";
+
+Goalw [constrains_def]
+ "[| F:program; B:condition |] ==> F : 0 co B";
+by (Blast_tac 1);
+qed "constrains_empty";
+
+Goalw [constrains_def]
+ "[| F:program; A:condition |] ==>(F : A co 0) <-> (A=0)";
+by (auto_tac (claset() addSDs [bspec],
+ simpset() addsimps [condition_def]));
+qed "constrains_empty2";
+
+Goalw [constrains_def]
+"[| F:program; B:condition |] ==> (F: state co B) <-> (B = state)";
+by (auto_tac (claset() addSDs [bspec] addDs [ActsD],
+ simpset() addsimps [condition_def]));
+qed "constrains_state";
+
+
+Goalw [constrains_def]
+ "[| F:program; A:condition |] ==> F : A co state";
+by (auto_tac (claset() addDs [ActsD], simpset()));
+qed "constrains_state2";
+
+Addsimps [constrains_empty, constrains_empty2,
+ constrains_state, constrains_state2];
+
+(*monotonic in 2nd argument*)
+Goalw [constrains_def]
+ "[| F:A co A'; A'<=B'; B':condition |] ==> F : A co B'";
+by (Blast_tac 1);
+qed "constrains_weaken_R";
+
+(*anti-monotonic in 1st argument*)
+Goalw [constrains_def, condition_def]
+ "[| F : A co A'; B<=A |] ==> F : B co A'";
+by (Blast_tac 1);
+qed "constrains_weaken_L";
+
+Goal
+ "[| F : A co A'; B<=A; A'<=B'; B':condition |] ==> F : B co B'";
+by (dtac constrains_weaken_R 1);
+by (dtac constrains_weaken_L 3);
+by (REPEAT(Blast_tac 1));
+qed "constrains_weaken";
+
+(** Union **)
+
+Goalw [constrains_def]
+ "[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')";
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
+qed "constrains_Un";
+
+Goalw [constrains_def]
+ "[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')";
+by Auto_tac;
+by (asm_full_simp_tac
+ (simpset() addsimps [condition_def]) 1);
+by (Blast_tac 1);
+qed "constrains_Un";
+
+Goalw [constrains_def]
+ "[| ALL i:I. F:A(i) co A'(i); F:program |] ==> \
+\ F:(UN i:I. A(i)) co (UN i:I. A'(i))";
+by (Clarify_tac 1);
+by (Blast_tac 1);
+bind_thm ("constrains_UN", ballI RS result());
+
+
+Goalw [constrains_def]
+ "(A Un B) co C = (A co C) Int (B co C)";
+by (rtac equalityI 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (ALLGOALS(Blast_tac));
+qed "constrains_Un_distrib";
+
+
+Goalw [constrains_def]
+ "i:I ==> (UN i:I. A(i)) co B = (INT i:I. A(i) co B)";
+by (rtac equalityI 1);
+by Safe_tac;
+by (ALLGOALS(Asm_full_simp_tac));
+by (ALLGOALS(Blast_tac));
+qed "constrains_UN_distrib";
+
+Goalw [constrains_def]
+ "[| A:condition; B:condition |] \
+\ ==> C co (A Int B) = (C co A) Int (C co B)";
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(Blast_tac));
+qed "constrains_Int_distrib";
+
+Goalw [constrains_def] "[| i:I; ALL i:I. B(i):condition |] ==> \
+\ A co (INT i:I. B(i)) = (INT i:I. A co B(i))";
+by (rtac equalityI 1);
+by Safe_tac;
+by (ALLGOALS(Blast_tac));
+qed "constrains_INT_distrib";
+
+(** Intersection **)
+
+Goalw [constrains_def]
+ "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')";
+by (Clarify_tac 1);
+by (Blast_tac 1);
+qed "constrains_Int";
+
+Goalw [constrains_def]
+ "[| ALL i:I. F : A(i) co A'(i); F:program |] \
+\ ==> F : (INT i:I. A(i)) co (INT i:I. A'(i))";
+by (case_tac "I=0" 1);
+by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
+by (etac not_emptyE 1);
+by Safe_tac;
+by (dres_inst_tac [("x", "xd")] bspec 1);
+by (ALLGOALS(Blast_tac));
+bind_thm ("constrains_INT", ballI RS result());
+
+
+(* This rule simulates the HOL's one for (INT z. A i) co (INT z. B i) *)
+
+Goalw [constrains_def, condition_def]
+ "[| ALL z. F: {s:state. P(s, z)} co {s:state. Q(s, z)}; F:program |] ==> \
+\ F: {s:state. ALL z. P(s, z)} co {s:state. ALL z. Q(s, z)}";
+by (auto_tac (claset() addSDs [bspec] addDs [ActsD],
+ simpset() addsimps [condition_def]));
+by (Blast_tac 1);
+bind_thm ("constrains_All", allI RS result());
+
+Goalw [constrains_def]
+ "F : A co A' ==> A <= A'";
+by (auto_tac (claset() addSDs [bspec], simpset()));
+qed "constrains_imp_subset";
+
+(*The reasoning is by subsets since "co" refers to single actions
+ only. So this rule isn't that useful.*)
+
+Goalw [constrains_def]
+ "[| F : A co B; F : B co C |] ==> F : A co C";
+by Auto_tac;
+by (dres_inst_tac [("x", "x")] bspec 1);
+by (dres_inst_tac [("x", "Id")] bspec 2);
+by (auto_tac (claset() addDs [ActsD],
+ simpset() addsimps [condition_def]));
+qed "constrains_trans";
+
+Goalw [constrains_def]
+ "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')";
+by Auto_tac;
+by (dres_inst_tac [("x", "Id")] bspec 1);
+by (dres_inst_tac [("x", "x")] bspec 2);
+by (auto_tac (claset(), simpset() addsimps [condition_def]));
+qed "constrains_cancel";
+
+(*** unless ***)
+
+Goalw [unless_def] "F : (A-B) co (A Un B) ==> F : A unless B";
+by (assume_tac 1);
+qed "unlessI";
+
+Goalw [unless_def] "F :A unless B ==> F : (A-B) co (A Un B)";
+by (assume_tac 1);
+qed "unlessD";
+
+Goalw [unless_def, constrains_def]
+ "F: A unless B ==> F:program & A:condition & B:condition";
+by Auto_tac;
+qed "unlessD2";
+
+(*** initially ***)
+
+Goalw [initially_def]
+"[| Init(F)<=A; F:program; A:condition |] ==> F:initially(A)";
+by (Blast_tac 1);
+qed "initiallyI";
+
+Goalw [initially_def]
+"F:initially(A) ==> Init(F)<=A";
+by (Blast_tac 1);
+qed "initiallyD";
+
+Goalw [initially_def]
+"F:initially(A) ==> F:program & A:condition";
+by (Blast_tac 1);
+qed "initiallyD2";
+
+(*** stable ***)
+
+Goalw [stable_def]
+ "F : A co A ==> F : stable(A)";
+by (assume_tac 1);
+qed "stableI";
+
+Goalw [stable_def] "F : stable(A) ==> F : A co A";
+by (assume_tac 1);
+qed "stableD";
+
+Goalw [stable_def, constrains_def]
+ "F:stable(A)==> F:program & A:condition";
+by (Blast_tac 1);
+qed "stableD2";
+
+Goalw [stable_def, constrains_def]
+ "stable(state) = program";
+by (auto_tac (claset() addDs [ActsD], simpset()));
+qed "stable_state";
+Addsimps [stable_state];
+
+(** Union **)
+
+Goalw [stable_def]
+ "[| F : stable(A); F : stable(A') |] ==> F : stable(A Un A')";
+by (blast_tac (claset() addIs [constrains_Un]) 1);
+qed "stable_Un";
+
+val [major, minor] = Goalw [stable_def]
+ "[| (!!i. i:I ==> F : stable(A(i))); F:program |] ==> F:stable (UN i:I. A(i))";
+by (cut_facts_tac [minor] 1);
+by (blast_tac (claset() addIs [constrains_UN, major]) 1);
+qed "stable_UN";
+
+Goalw [stable_def]
+ "[| F : stable(A); F : stable(A') |] ==> F : stable (A Int A')";
+by (blast_tac (claset() addIs [constrains_Int]) 1);
+qed "stable_Int";
+
+val [major, minor] = Goalw [stable_def]
+ "[| (!!i. i:I ==> F : stable(A(i))); F:program |] \
+\ ==> F : stable (INT i:I. A(i))";
+by (cut_facts_tac [minor] 1);
+by (blast_tac (claset() addIs [constrains_INT, major]) 1);
+qed "stable_INT";
+
+Goalw [stable_def]
+ "[| ALL z. F: stable({s:state. P(s, z)}); F:program |] ==> \
+\ F: stable({s:state. ALL z. P(s, z)})";
+by (rtac constrains_All 1);
+by Auto_tac;
+bind_thm("stable_All", allI RS result());
+
+
+Goalw [stable_def, constrains_def]
+ "[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')";
+by (Clarify_tac 1);
+by (Blast_tac 1);
+qed "stable_constrains_Un";
+
+
+Goalw [stable_def, constrains_def]
+ "[| F : stable(C); F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')";
+by (Clarify_tac 1);
+by (Blast_tac 1);
+qed "stable_constrains_Int";
+
+(*[| F : stable(C); F : (C Int A) co A |] ==> F : stable (C Int A) *)
+bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
+
+(** invariant **)
+
+Goalw [invariant_def, initially_def]
+"invariant(A) = initially(A) Int stable(A)";
+by (blast_tac (claset() addDs [stableD2]) 1);
+qed "invariant_eq";
+
+val invariant_def2 = invariant_eq RS eq_reflection;
+
+Goalw [invariant_def]
+ "[| Init(F)<=A; F:stable(A) |] ==> F : invariant(A)";
+by (blast_tac (claset() addDs [stableD2]) 1);
+qed "invariantI";
+
+Goalw [invariant_def]
+"F:invariant(A) ==> Init(F)<=A & F:stable(A)";
+by Auto_tac;
+qed "invariantD";
+
+Goalw [invariant_def]
+ "F:invariant(A) ==> F:program & A:condition";
+by (blast_tac (claset() addDs [stableD2]) 1);
+qed "invariantD2";
+
+(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
+Goalw [invariant_def]
+ "[| F : invariant(A); F : invariant(B) |] ==> F : invariant(A Int B)";
+by (asm_full_simp_tac (simpset() addsimps [stable_Int]) 1);
+by (Blast_tac 1);
+qed "invariant_Int";
+
+(** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of ALL m ? Would make it harder to use
+ in forward proof. **)
+
+Goalw [constrains_def]
+ "[| ALL m:M. F : {s:S. x(s) = m} co B(m); F:program |] \
+\ ==> F:{s:S. x(s):M} co (UN m:M. B(m))";
+by Safe_tac;
+by (Blast_tac 1);
+by (auto_tac (claset(), simpset() addsimps [condition_def]));
+qed "elimination";
+
+(* As above, but for the special case of S=state *)
+Goal "[| ALL m:M. F : {s:state. x(s) = m} co B(m); F:program |] \
+\ ==> F:{s:state. x(s):M} co (UN m:M. B(m))";
+by (rtac elimination 1);
+by (ALLGOALS(Clarify_tac));
+qed "eliminiation2";
+
+
+Goalw [constrains_def, strongest_rhs_def]
+ "[| F:program; A:condition |] ==>F : A co (strongest_rhs(F,A))";
+by (auto_tac (claset() addDs [ActsD], simpset()));
+qed "constrains_strongest_rhs";
+
+Goalw [constrains_def, strongest_rhs_def]
+ "F : A co B ==> strongest_rhs(F,A) <=B";
+by Safe_tac;
+by (dtac InterD 1);
+by (auto_tac (claset(),
+ simpset() addsimps [condition_def]));
+qed "strongest_rhs_is_strongest";
+
+(*** increasing ***)
+Goalw [increasing_on_def]
+ "[| F:increasing[A](f, r); z:A |] ==> F:stable({s:state. <z, f`s>:r})";
+by (Blast_tac 1);
+qed "increasing_onD";
+
+Goalw [increasing_on_def]
+"F:increasing[A](f, r) ==> F:program & f:state->A & part_order(A,r)";
+by (auto_tac (claset(), simpset() addsimps [INT_iff]));
+qed "increasing_onD2";
+
+Goalw [increasing_on_def, stable_def]
+"[| part_order(A,r); c:A; F:program |] ==> F : increasing[A](lam s:state. c, r)";
+by (auto_tac (claset(), simpset() addsimps [INT_iff]));
+by (force_tac (claset() addSDs [bspec, ActsD],
+ simpset() addsimps [constrains_def, condition_def]) 1);
+qed "increasing_on_constant";
+Addsimps [increasing_on_constant];
+
+Goalw [increasing_on_def, stable_def, constrains_def, part_order_def]
+ "!!f. g:mono_map(A,r,A,r) \
+\ ==> increasing[A](f, r) <= increasing[A](g O f, r)";
+by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1);
+by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def]));
+by (force_tac (claset() addSDs [bspec, ActsD], simpset()) 1);
+by (subgoal_tac "xd:state" 1);
+by (force_tac (claset() addSDs [ActsD], simpset()) 2);
+by (subgoal_tac "f`xe:A & f`xd:A" 1);
+by (blast_tac (claset() addDs [apply_type]) 2);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (Asm_simp_tac 1);
+by (REPEAT(etac conjE 1));
+by (rotate_tac ~2 1);
+by (dres_inst_tac [("x", "xc")] bspec 1);
+by (Asm_simp_tac 1);
+by (dres_inst_tac [("c", "xd")] subsetD 1);
+by (rtac imageI 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1);
+by (dres_inst_tac [("x", "f`xe")] bspec 1);
+by (dres_inst_tac [("x", "f`xd")] bspec 2);
+by (ALLGOALS(Asm_simp_tac));
+by (dres_inst_tac [("b", "g`(f`xe)")] trans_onD 1);
+by Auto_tac;
+qed "mono_increasing_on_comp";
+
+(*Holds by the theorem (succ(m) le n) = (m < n) *)
+Goalw [increasing_on_def, nat_order_def]
+ "[| F:increasing[nat](f, nat_order); z:nat |] \
+\ ==> F: stable({s:state. z < f`s})";
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
+by Safe_tac;
+by (dres_inst_tac [("x", "succ(z)")] bspec 1);
+by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq]));
+by (subgoal_tac "{x: state . f ` x : nat} = state" 1);
+by Auto_tac;
+qed "strict_increasing_onD";
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/UNITY.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,98 @@
+(* Title: ZF/UNITY/UNITY.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+The basic UNITY theory (revised version, based upon the "co" operator)
+From Misra, "A Logic for Concurrent Programming", 1994
+
+Theory ported from HOL.
+*)
+
+UNITY = State + UNITYMisc +
+consts
+ constrains :: "[i, i] => i" (infixl "co" 60)
+ op_unless :: "[i, i] => i" (infixl "unless" 60)
+
+constdefs
+ program :: i
+ "program == {<init, acts, allowed>:condition*actionSet*actionSet.
+ Id:acts & Id:allowed}"
+
+ mk_program :: [i,i,i]=>i
+ "mk_program(init, acts, allowed) ==
+ <init Int state, cons(Id, acts Int action), cons(Id, allowed Int action)>"
+
+ SKIP :: i
+ "SKIP == mk_program(state, 0, action)"
+
+ (** 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, fst(snd(F)))"
+
+ Acts :: i=>i
+ "Acts(F) == RawActs(programify(F))"
+
+ RawAllowedActs :: i=>i
+ "RawAllowedActs(F) == cons(Id, snd(snd(F)))"
+
+ AllowedActs :: i=>i
+ "AllowedActs(F) == RawAllowedActs(programify(F))"
+
+
+ Allowed :: i =>i
+ "Allowed(F) == {G:program. Acts(G) <= AllowedActs(F)}"
+
+ (* initially property, used by some UNITY authors *)
+ initially :: i => i
+ "initially(A) == {F:program. Init(F)<= A & A:condition}"
+
+ 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) == {F:program. Init(F)<=A} Int stable(A)"
+
+ part_order :: [i, i] => o
+ "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
+
+ nat_order :: i
+ "nat_order == {<i,j>:nat*nat. i le j}"
+
+ (*
+ The constant increasing_on defines the Charpentier's increasing notion.
+ It should not be confused with the ZF's increasing constant
+ which have a different meaning.
+ Increasing_on's parameters: a state function f, a domain A and
+ a order relation r over the domain A
+ Should f be a meta function instead ?
+ *)
+ increasing_on :: [i,i, i] => i ("increasing[_]'(_,_')")
+ "increasing[A](f, r) ==
+ {F:program. f:state->A & part_order(A,r) & F:
+ (INT z:A. stable({s:state. <z, f`s>:r}))}"
+
+defs
+ (* The typing requirements `A:condition & B:condition'
+ make the definition stronger than the original ones in HOL. *)
+
+ constrains_def "A co B ==
+ {F:program. (ALL act:Acts(F). act``A <= B)
+ & A:condition & B:condition}"
+
+ unless_def "A unless B == (A - B) co (A Un B)"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/UNITYMisc.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,215 @@
+(* Title: HOL/UNITY/UNITYMisc.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Some miscellaneous and add-hoc set theory concepts.
+
+*)
+
+Goalw [measure_def, less_than_def]
+ "less_than(A) = {<x,y>:A*A. x<y}";
+by Auto_tac;
+qed "less_than_equals";
+
+Goalw [less_than_def] "wf(less_than(A))";
+by (rtac wf_measure 1);
+qed "wf_less_than";
+
+Goalw [less_than_def, measure_def]
+ "less_than(A)<= A*A";
+by Auto_tac;
+qed "less_than_subset";
+
+Goalw [less_than_def, measure_def]
+"<x,y>:less_than(A) <-> (x:A & y:A & x<y)";
+by Auto_tac;
+qed "less_than_iff";
+
+Goalw [lessThan_def]
+"i:lessThan(k,A) <-> i:A & i<k";
+by Auto_tac;
+qed "lessThan_iff";
+
+Goalw [greaterThan_def]
+"i:greaterThan(k,A) <-> i:A & k<i";
+by Auto_tac;
+qed "greaterThan_iff";
+
+
+
+(** Needed for WF reasoning in WFair.ML **)
+
+Goal "k:A ==>less_than(A)``{k} = greaterThan(k, A)";
+by (rtac equalityI 1);
+by (auto_tac (claset(), simpset() addsimps
+ [less_than_iff,greaterThan_iff]));
+qed "Image_less_than";
+
+Goal "k:A ==> less_than(A)-`` {k} = lessThan(k, A)";
+by (rtac equalityI 1);
+by (auto_tac (claset(), simpset() addsimps
+ [less_than_iff,lessThan_iff]));
+qed "Image_inverse_less_than";
+
+Addsimps [Image_less_than, Image_inverse_less_than];
+
+
+(** Ad-hoc set-theory rules **)
+
+Goal "(C Int A) Un (C Int B) = C Int (A Un B)";
+by (Blast_tac 1);
+qed "Int_Un_distrib2";
+
+Goal "C Int (A - B) = (C Int A) - (C Int B)";
+by (Blast_tac 1);
+qed "Diff_Int_distrib";
+
+Goal "(A - B) Int C = (A Int C) - (B Int C)";
+by (Blast_tac 1);
+qed "Diff_Int_distrib2";
+
+Goal "A Un (A Un B) = A Un B";
+by (Blast_tac 1);
+qed "double_Un";
+
+Goal "A Un (B Un C) = B Un (A Un C)";
+by (Blast_tac 1);
+qed "Un_assoc2";
+
+
+val Un_ac = [Un_assoc, double_Un, Un_commute, Un_assoc2, Un_absorb];
+
+Goal "A Un B = Union({A, B})";
+by (Blast_tac 1);
+qed "Un_eq_Union";
+
+Goal "(UN x:A. {x}) = A";
+by (Blast_tac 1);
+qed "UN_singleton";
+
+
+Goal "Union(B) Int A = (UN b:B. b Int A)";
+by Auto_tac;
+qed "Int_Union_Union";
+
+Goal "A Int Union(B) = (UN b:B. A Int b)";
+by Auto_tac;
+qed "Int_Union_Union2";
+
+(** Intersection **)
+Goal "A Int (A Int B) = A Int B";
+by (Blast_tac 1);
+qed "double_Int";
+
+Goal "A Int (B Int C) = B Int (A Int C)";
+by (Blast_tac 1);
+qed "Int_assoc2";
+
+val Int_ac = [Int_assoc, double_Int, Int_commute, Int_assoc2];
+
+Goal "A Int B = 0 ==> A - B = A";
+by (Blast_tac 1);
+qed "Diff_triv";
+
+Goal "A Int B - C = A Int (B - C)";
+by (Blast_tac 1);
+qed "Int_Diff";
+
+Goal "f -``B = (UN y:B. f-``{y})";
+by (Blast_tac 1);
+qed "vimage_eq_UN";
+
+Goal "A Un B - (A - B) = B";
+by (Blast_tac 1);
+qed "Un_Diff_Diff";
+AddIffs [Un_Diff_Diff];
+
+(*** INT simps ***)
+
+Goal
+"i:I ==> (INT i:I. A(i)) Un B = (INT i:I. A(i) Un B)";
+by Auto_tac;
+qed "INT_Un_distrib";
+
+Goal
+ "!!C. c: C ==> (INT x:C. cons(a, B(x))) = cons(a, (INT x:C. B(x)))";
+by Auto_tac;
+qed "INT_cons";
+
+Goal
+"i:I ==> (INT i:I. A(i)) Int B = (INT i:I. A(i) Int B)";
+by Auto_tac;
+qed "INT_Int_distrib2";
+
+Goal
+"i:I ==> B Int (INT i:I. A(i)) = (INT i:I. B Int A(i))";
+by Auto_tac;
+qed "Int_INT_distrib";
+
+val INT_simps = [Un_INT_distrib, Un_INT_distrib2,
+ INT_constant, INT_Int_distrib, Diff_INT,
+ INT_Un_distrib,INT_cons, INT_Int_distrib2, Int_INT_distrib, Inter_0];
+
+
+(*** UN ***)
+Goal
+"!!C. c: C ==> cons(a, (UN x:C. B(x))) = (UN x:C. cons(a, B(x)))";
+by Auto_tac;
+qed "UN_cons";
+
+Goal
+ "!!C. c: C ==> B Un (UN x:C. A(x)) = (UN x:C. B Un A(x))";
+by Auto_tac;
+qed "Un_UN_distrib";
+
+Goal
+"!!C. c: C ==> (UN x:C. B(x)) Un A = (UN x:C. B(x) Un A)";
+by Auto_tac;
+qed "UN_Un_distrib2";
+
+Goal "(UN x:C. B(x)) Int A = (UN x:C. B(x) Int A)";
+by Auto_tac;
+qed "UN_Int_distrib";
+
+val UN_simps = [UN_cons, Un_UN_distrib, UN_Un_distrib2, UN_Un_distrib, UN_Int_distrib, UN_0];
+
+(** Needed in State theory for the current definition of variables
+where they are indexed by lists **)
+
+Goal "i:list(nat) ==> i:univ(0)";
+by (dres_inst_tac [("B", "0")] list_into_univ 1);
+by (blast_tac (claset() addIs [nat_into_univ]) 1);
+by (assume_tac 1);
+qed "list_nat_into_univ";
+
+(** To be moved to Update theory **)
+
+Goalw [update_def]
+ "[| f:Pi(A,B); x:A; y:B(x) |] ==> f(x:=y):Pi(A, B)";
+by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb,
+ apply_funtype, lam_type]) 1);
+qed "update_type2";
+
+(** Simplication rules for Collect; To be moved elsewhere **)
+Goal "{x:A. P(x)} Int A = {x:A. P(x)}";
+by Auto_tac;
+qed "Collect_Int2";
+
+Goal "A Int {x:A. P(x)} = {x:A. P(x)}";
+by Auto_tac;
+qed "Collect_Int3";
+
+AddIffs [Collect_Int2, Collect_Int3];
+
+
+Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
+by Auto_tac;
+qed "Collect_disj_eq";
+
+Goal "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)";
+by Auto_tac;
+qed "Collect_conj_eq";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/UNITYMisc.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,25 @@
+(* Title: HOL/UNITY/UNITYMisc.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Some miscellaneous and add-hoc set theory concepts.
+*)
+
+
+
+UNITYMisc = Main +
+constdefs
+ less_than :: i=>i
+ "less_than(A) == measure(A, %x. x)"
+
+ lessThan :: [i, i] => i
+ "lessThan(u,A) == {x:A. x<u}"
+
+ greaterThan :: [i,i]=> i
+ "greaterThan(u,A) == {x:A. u<x}"
+
+ (* Identity relation over a domain A *)
+ Identity :: i=>i
+ "Identity(A) == {p:A*A. EX x. p=<x,x>}"
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Union.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,649 @@
+(* Title: ZF/UNITY/Union.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Unions of programs
+
+From Misra's Chapter 5: Asynchronous Compositions of Programs
+
+Proofs ported from HOL.
+
+*)
+
+(** SKIP **)
+
+Goal "reachable(SKIP) = state";
+by (force_tac (claset() addEs [reachable.induct]
+ addIs reachable.intrs, simpset()) 1);
+qed "reachable_SKIP";
+
+Addsimps [reachable_SKIP];
+
+(* Elimination programify from ok and Join *)
+
+Goal "programify(F) ok G <-> F ok G";
+by (simp_tac (simpset() addsimps [ok_def]) 1);
+qed "ok_programify_left";
+
+Goal "F ok programify(G) <-> F ok G";
+by (simp_tac (simpset() addsimps [ok_def]) 1);
+qed "ok_programify_right";
+
+Goal "programify(F) Join G = F Join G";
+by (simp_tac (simpset() addsimps [Join_def]) 1);
+qed "Join_programify_left";
+
+Goal "F Join programify(G) = F Join G";
+by (simp_tac (simpset() addsimps [Join_def]) 1);
+qed "Join_programify_right";
+
+Addsimps [ok_programify_left, ok_programify_right,
+ Join_programify_left, Join_programify_right];
+
+(** SKIP and safety properties **)
+
+Goalw [constrains_def]
+"[| A:condition; B:condition |] ==> (SKIP: A co B) <-> (A<=B)";
+by Auto_tac;
+qed "SKIP_in_constrains_iff";
+Addsimps [SKIP_in_constrains_iff];
+
+
+Goalw [Constrains_def]
+"[| A:condition; B:condition |] ==> (SKIP : A Co B)<-> (A<=B)";
+by (Asm_simp_tac 1);
+by (auto_tac (claset(),
+ simpset() addsimps [condition_def]));
+qed "SKIP_in_Constrains_iff";
+Addsimps [SKIP_in_Constrains_iff];
+
+Goal "A:condition ==>SKIP : stable(A)";
+by (auto_tac (claset(),
+ simpset() addsimps [stable_def]));
+qed "SKIP_in_stable";
+Addsimps [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable];
+
+
+(** Join and JOIN types **)
+
+Goalw [Join_def]
+ "F Join G : program";
+by Auto_tac;
+qed "Join_in_program";
+AddIffs [Join_in_program];
+AddTCs [Join_in_program];
+
+Goalw [JOIN_def]
+"JOIN(I,F):program";
+by Auto_tac;
+qed "JOIN_in_program";
+AddIffs [JOIN_in_program];
+AddTCs [JOIN_in_program];
+
+(* Init, Acts, and AllowedActs of Join and JOIN *)
+Goal "Init(F Join G) = Init(F) Int Init(G)";
+by (simp_tac (simpset()
+ addsimps [Int_assoc, Join_def]) 1);
+qed "Init_Join";
+
+Goal "Acts(F Join G) = Acts(F) Un Acts(G)";
+by (simp_tac (simpset()
+ addsimps [Int_Un_distrib,cons_absorb,Join_def]) 1);
+qed "Acts_Join";
+
+Goal "AllowedActs(F Join G) = \
+\ AllowedActs(F) Int AllowedActs(G)";
+by (simp_tac (simpset()
+ addsimps [Int_assoc,cons_absorb,Join_def]) 1);
+qed "AllowedActs_Join";
+Addsimps [Init_Join, Acts_Join, AllowedActs_Join];
+
+
+(** Join's algebraic laws **)
+
+Goal "F Join G = G Join F";
+by (simp_tac (simpset() addsimps
+ [Join_def, Un_commute, Int_commute]) 1);
+qed "Join_commute";
+
+
+Goal "A Join (B Join C) = B Join (A Join C)";
+by (asm_simp_tac (simpset() addsimps
+ Un_ac@Int_ac@[Join_def,Int_Un_distrib, cons_absorb]) 1);
+qed "Join_left_commute";
+
+
+Goal "(F Join G) Join H = F Join (G Join H)";
+by (asm_simp_tac (simpset() addsimps
+ Un_ac@[Join_def, cons_absorb, Int_assoc, Int_Un_distrib]) 1);
+qed "Join_assoc";
+
+Goalw [Join_def, SKIP_def]
+ "SKIP Join F = programify(F)";
+by (simp_tac (simpset() addsimps [Int_absorb, cons_absorb,cons_eq]) 1);
+qed "Join_SKIP_left";
+
+Goal "F Join SKIP = programify(F)";
+by (stac Join_commute 1);
+by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1);
+qed "Join_SKIP_right";
+
+
+Addsimps [Join_SKIP_left, Join_SKIP_right];
+
+
+Goal "F Join F = programify(F)";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "Join_absorb";
+
+Addsimps [Join_absorb];
+
+Goal "F Join (F Join G) = F Join G";
+by (asm_simp_tac (simpset() addsimps [Join_assoc RS sym]) 1);
+qed "Join_left_absorb";
+
+
+(*Join is an AC-operator*)
+val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute];
+
+(** Eliminating programify in JN and OK expressions **)
+
+Goal "OK(I, %x. programify(F(x))) <-> OK(I, F)";
+by (simp_tac (simpset() addsimps [OK_def]) 1);
+qed "OK_programify";
+
+Goal "JOIN(I, %x. programify(F(x))) = JOIN(I, F)";
+by (simp_tac (simpset() addsimps [JOIN_def]) 1);
+qed "JN_programify";
+
+Addsimps [OK_programify, JN_programify];
+
+(* JN *)
+
+Goalw [JOIN_def]
+"JOIN(0, F) = SKIP";
+by Auto_tac;
+qed "JN_empty";
+Addsimps [JN_empty];
+AddSEs [not_emptyE];
+Addsimps [Inter_0];
+
+Goal
+ "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (auto_tac (claset(), simpset()
+ addsimps [JOIN_def,INT_Int_distrib2]));
+qed "Init_JN";
+
+Goal
+"Acts(JOIN(I,F)) = cons(Id, UN i:I. Acts(F(i)))";
+by (auto_tac (claset(),
+ simpset() addsimps [JOIN_def, UN_Int_distrib]));
+qed "Acts_JN";
+
+Goal
+"AllowedActs(JN i:I. F(i)) = (if I=0 then action else (INT i:I. AllowedActs(F(i))))";
+by (auto_tac (claset(), simpset()
+ addsimps [JOIN_def, INT_cons RS sym, INT_Int_distrib2]));
+qed "AllowedActs_JN";
+
+Addsimps [Init_JN, Acts_JN, AllowedActs_JN];
+
+
+Goal "(JN i:cons(a,I). F(i)) = F(a) Join (JN i:I. F(i))";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "JN_cons";
+Addsimps[JN_cons];
+
+
+val prems = Goalw [JOIN_def]
+ "[| I=J; !!i. i:J ==> F(i) = G(i) |] ==> \
+\ (JN i:I. F(i)) = (JN i:J. G(i))";
+by (asm_simp_tac (simpset() addsimps prems) 1);
+qed "JN_cong";
+
+Addcongs [JN_cong];
+
+
+(*** JN laws ***)
+Goal "k:I ==>F(k) Join (JN i:I. F(i)) = (JN i:I. F(i))";
+by (stac (JN_cons RS sym) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [cons_absorb]));
+qed "JN_absorb";
+
+Goalw [Inter_def] "[| i:I; j:J |] ==> \
+\ (INT i:I Un J. A(i)) = ((INT i:I. A(i)) Int (INT j:J. A(j)))";
+by Auto_tac;
+by (Blast_tac 1);
+qed "INT_Un";
+
+Goal "(JN i: I Un J. F(i)) = ((JN i: I. F(i)) Join (JN i:J. F(i)))";
+by (rtac program_equalityI 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by Safe_tac;
+by (ALLGOALS(asm_full_simp_tac (simpset()
+ addsimps [Int_absorb, INT_Int_distrib2,
+ Int_INT_distrib, UN_cons, INT_cons])));
+by (ALLGOALS(Clarify_tac));
+by (REPEAT(Blast_tac 1));
+qed "JN_Un";
+
+Goal "(JN i:I. c) = (if I=0 then SKIP else programify(c))";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "JN_constant";
+
+Goal
+"(JN i:I. F(i) Join G(i)) = (JN i:I. F(i)) Join (JN i:I. G(i))";
+by (rtac program_equalityI 1);
+by (ALLGOALS(simp_tac (simpset() addsimps [Int_absorb])));
+by Safe_tac;
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps
+ [INT_Int_distrib, Int_absorb])));
+by (Force_tac 1);
+qed "JN_Join_distrib";
+
+Goal
+"(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))";
+by (asm_simp_tac (simpset()
+ addsimps [JN_Join_distrib, JN_constant]) 1);
+qed "JN_Join_miniscope";
+
+(*Used to prove guarantees_JN_I*)
+
+Goal "i:I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "JN_Join_diff";
+
+(*** 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.*)
+
+Goalw [constrains_def, JOIN_def]
+ "i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)";
+by Auto_tac;
+by (blast_tac (claset() addDs [ActsD]) 1);
+qed "JN_constrains";
+
+Goal "(F Join G : A co B) <-> \
+\ (programify(F):A co B & programify(G):A co B)";
+by (auto_tac
+ (claset(), simpset() addsimps [constrains_def]));
+qed "Join_constrains";
+
+Goal "(F Join G : A unless B) <-> \
+\ (programify(F) : A unless B & programify(G):A unless B)";
+by (asm_simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
+qed "Join_unless";
+
+Addsimps [Join_constrains, Join_unless];
+
+(*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
+*)
+
+Goal "[| F : A co A'; G:B co B' |] \
+\ ==> F Join G : (A Int B) co (A' Un B')";
+by (subgoal_tac "A:condition&A':condition & B: condition& \
+ \ B': condition & F:program & G:program" 1);
+by (blast_tac (claset() addDs [constrainsD2]) 2);
+by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "Join_constrains_weaken";
+
+(*If I=0, it degenerates to SKIP : UNIV co 0, which is false.*)
+Goal "[| ALL i:I. F(i) : A(i) co A'(i); i: I |] \
+\ ==> (JN i:I. F(i)) : (INT i:I. A(i)) co (UN i:I. A'(i))";
+by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
+by (Clarify_tac 1);
+by (subgoal_tac "(ALL i:I. F(i):program & A(i):condition)&\
+ \ (Union(RepFun(I, A')):condition)&\
+ \ (Inter(RepFun(I, A)):condition)" 1);
+by (blast_tac (claset() addDs [constrainsD2]) 2);
+by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "JN_constrains_weaken";
+
+
+Goal "A:condition ==> (JN i:I. F(i)) : stable(A) <-> \
+\ (ALL i:I. programify(F(i)):stable(A))";
+by (asm_simp_tac
+ (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
+by Auto_tac;
+by (blast_tac (claset() addDs [ActsD]) 1);
+qed "JN_stable";
+
+
+Goal "[| ALL i:I. F(i) : invariant(A); i : I |] \
+\ ==> (JN i:I. F(i)) : invariant(A)";
+by (subgoal_tac "A:condition" 1);
+by (blast_tac (claset() addDs [invariantD2]) 2);
+by (asm_full_simp_tac (simpset() addsimps [invariant_def, JN_stable]) 1);
+by (Blast_tac 1);
+bind_thm ("invariant_JN_I", ballI RS result());
+Goal " (F Join G : stable(A)) <-> \
+\ (programify(F) : stable(A) & programify(G): stable(A))";
+by (asm_simp_tac (simpset() addsimps [stable_def]) 1);
+qed "Join_stable";
+
+
+(* TO BE DONE: stable_increasing *)
+
+Addsimps [Join_stable];
+
+Goal "[| F : invariant(A); G : invariant(A) |] \
+\ ==> F Join G : invariant(A)";
+by (subgoal_tac "F:program&G:program" 1);
+by (blast_tac (claset() addDs [invariantD2]) 2);
+by (full_simp_tac (simpset() addsimps [invariant_def]) 1);
+by (auto_tac (claset() addIs [Join_in_program], simpset()));
+qed "invariant_JoinI";
+
+
+(* Fails if I=0 because INT i:0. A(i) = 0 *)
+Goal "i:I ==> FP(JN i:I. F(i)) = (INT i:I. FP (programify(F(i))))";
+by (asm_simp_tac (simpset() addsimps [FP_def, Inter_def]) 1);
+by (rtac equalityI 1);
+by Safe_tac;
+by (ALLGOALS(subgoal_tac "{x}:condition"));
+by (rotate_tac ~1 3);
+by (rotate_tac ~1 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable])));
+by (rewrite_goals_tac [condition_def]);
+by (REPEAT(Blast_tac 1));
+qed "FP_JN";
+
+(*** Progress: transient, ensures ***)
+
+Goal "i:I==>(JN i:I. F(i)) : transient(A) <-> \
+\ (EX i:I. programify(F(i)) : transient(A))";
+by (auto_tac (claset(),
+ simpset() addsimps [transient_def, JOIN_def]));
+by (auto_tac (claset(), simpset() addsimps
+ [condition_def,UN_Int_distrib, INT_Int_distrib]));
+qed "JN_transient";
+
+Goal "F Join G : transient(A) <-> \
+\ (programify(F) : transient(A) | programify(G):transient(A))";
+by (auto_tac (claset(),
+ simpset() addsimps [transient_def,
+ Join_def, Int_Un_distrib]));
+qed "Join_transient";
+
+Addsimps [Join_transient];
+
+
+Goal "F : transient(A) ==> F Join G : transient(A)";
+by (asm_full_simp_tac (simpset()
+ addsimps [Join_transient, transientD]) 1);
+qed "Join_transient_I1";
+
+
+Goal "G : transient(A) ==> F Join G : transient(A)";
+by (asm_full_simp_tac (simpset()
+ addsimps [Join_transient, transientD]) 1);
+qed "Join_transient_I2";
+
+(*If I=0 it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
+Goal "i : I ==> \
+\ (JN i:I. F(i)) : A ensures B <-> \
+\ ((ALL i:I. programify(F(i)) : (A-B) co (A Un B)) & \
+\ (EX i:I. programify(F(i)) : A ensures B))";
+by (auto_tac (claset(),
+ simpset() addsimps [ensures_def, JN_constrains, JN_transient]));
+qed "JN_ensures";
+
+
+Goalw [ensures_def]
+ "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)))";
+by (auto_tac (claset(), simpset() addsimps [Join_transient]));
+qed "Join_ensures";
+
+
+
+Goalw [stable_def, constrains_def, Join_def]
+ "[| F : stable(A); G : A co A' |] \
+\ ==> F Join G : A co A'";
+by Auto_tac;
+by (rewrite_goals_tac [condition_def]);
+by Auto_tac;
+by (blast_tac (claset() addDs [ActsD]) 3);
+by (dres_inst_tac [("x", "Id")] bspec 1);
+by (dres_inst_tac [("x", "Id")] bspec 2);
+by (dres_inst_tac [("x", "x")] bspec 4);
+by (dres_inst_tac [("x", "Id")] bspec 5);
+by Auto_tac;
+qed "stable_Join_constrains";
+
+(*Premise for G cannot use Always because F: Stable A is
+ weaker than G : stable A *)
+Goal "[| F : stable(A); G : invariant(A) |] ==> F Join G : Always(A)";
+by (subgoal_tac "A:condition & F:program" 1);
+by (blast_tac (claset() addDs [stableD2]) 2);
+by (asm_full_simp_tac (simpset() addsimps [Always_def, invariant_def,
+ Stable_eq_stable]) 1);
+by (force_tac(claset() addIs [stable_Int], simpset()) 1);
+qed "stable_Join_Always1";
+
+
+
+(*As above, but exchanging the roles of F and G*)
+Goal "[| F : invariant(A); G : stable(A) |] ==> F Join G : Always(A)";
+by (stac Join_commute 1);
+by (blast_tac (claset() addIs [stable_Join_Always1]) 1);
+qed "stable_Join_Always2";
+
+
+
+Goal "[| F : stable(A); G : A ensures B |] ==> F Join G : A ensures B";
+by (subgoal_tac "F:program&G:program&A:condition&B:condition" 1);
+by (blast_tac (claset() addDs [stableD2, ensuresD2]) 2);
+by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1);
+by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
+by (etac constrains_weaken 1);
+by Auto_tac;
+qed "stable_Join_ensures1";
+
+
+(*As above, but exchanging the roles of F and G*)
+Goal "[| F : A ensures B; G : stable(A) |] ==> F Join G : A ensures B";
+by (stac Join_commute 1);
+by (blast_tac (claset() addIs [stable_Join_ensures1]) 1);
+qed "stable_Join_ensures2";
+
+
+(*** the ok and OK relations ***)
+
+Goal "SKIP ok F";
+by (auto_tac (claset() addDs [ActsD],
+ simpset() addsimps [ok_def]));
+qed "ok_SKIP1";
+
+Goal "F ok SKIP";
+by (auto_tac (claset() addDs [ActsD],
+ simpset() addsimps [ok_def]));
+qed "ok_SKIP2";
+
+AddIffs [ok_SKIP1, ok_SKIP2];
+
+Goal "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_commute";
+
+Goal "(F ok G) <->(G ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_commute";
+
+bind_thm ("ok_sym", ok_commute RS iffD1);
+
+Goal "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)";
+by (asm_full_simp_tac
+ (simpset() addsimps [ok_def, Join_def, OK_def,
+ Int_assoc, cons_absorb, Int_Un_distrib, Ball_def]) 1);
+by (rtac iffI 1);
+by Safe_tac;
+by (REPEAT(Force_tac 1));
+qed "ok_iff_OK";
+
+Goal "F ok (G Join H) <-> (F ok G & F ok H)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_iff1";
+
+
+Goal "(G Join H) ok F <-> (G ok F & H ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_iff2";
+AddIffs [ok_Join_iff1, ok_Join_iff2];
+
+(*useful? Not with the previous two around*)
+Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_commute_I";
+
+Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (blast_tac (claset() addDs [ActsD]) 1);
+by (REPEAT(Force_tac 1));
+qed "ok_JN_iff1";
+
+
+Goal "JOIN(I,G) ok F <-> (ALL i:I. G(i) ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (blast_tac (claset() addDs [ActsD]) 1);
+qed "ok_JN_iff2";
+AddIffs [ok_JN_iff1, ok_JN_iff2];
+
+Goal "OK(I,F) <-> (ALL i: I. ALL j: I-{i}. F(i) ok (F(j)))";
+by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def]));
+qed "OK_iff_ok";
+
+
+Goal "[| OK(I,F); i: I; j: I; i~=j|] ==> F(i) ok F(j)";
+by (auto_tac (claset(), simpset() addsimps [OK_iff_ok]));
+qed "OK_imp_ok";
+
+
+(*** Allowed ***)
+
+Goal "Allowed(SKIP) = program";
+by (auto_tac (claset() addDs [ActsD],
+ simpset() addsimps [Allowed_def]));
+qed "Allowed_SKIP";
+
+Goal "Allowed(F Join G) = \
+\ Allowed(programify(F)) Int Allowed(programify(G))";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
+qed "Allowed_Join";
+
+Goal "i:I ==> \
+\ Allowed(JOIN(I,F)) = (INT i:I. Allowed(programify(F(i))))";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
+br equalityI 1;
+by Auto_tac;
+qed "Allowed_JN";
+
+Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
+
+Goal
+"F ok G <-> (programify(F):Allowed(programify(G)) & \
+\ programify(G):Allowed(programify(F)))";
+by (asm_simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
+qed "ok_iff_Allowed";
+
+
+Goal "OK(I,F) <-> \
+\ (ALL i: I. ALL j: I-{i}. programify(F(i)) : Allowed(programify(F(j))))";
+by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed]));
+qed "OK_iff_Allowed";
+
+(*** safety_prop, for reasoning about given instances of "ok" ***)
+
+Goal "safety_prop(X) ==> (Acts(G) <= cons(Id, (UN F:X. Acts(F)))) <-> (programify(G):X)";
+by (full_simp_tac( simpset() addsimps [safety_prop_def]) 1);
+by (Clarify_tac 1);
+by (case_tac "G:program" 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (Blast_tac 1);
+by Safe_tac;
+by (Force_tac 2);
+by (force_tac (claset(), simpset()
+ addsimps [programify_def]) 1);
+qed "safety_prop_Acts_iff";
+
+Goal "X:property ==> \
+\ (safety_prop(X) --> \
+\ ((UN G:X. Acts(G)) <= AllowedActs(F)) <-> (X <= Allowed(programify(F))))";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def,
+ safety_prop_Acts_iff RS iff_sym, property_def]));
+qed "safety_prop_AllowedActs_iff_Allowed";
+
+
+Goal "X:property ==> \
+\ safety_prop(X) --> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X";
+by (asm_full_simp_tac (simpset() addsimps [Allowed_def,
+ UN_Int_distrib,safety_prop_Acts_iff, property_def]) 1);
+by Auto_tac;
+qed "Allowed_eq";
+
+Goal "[| F == mk_program (init, acts, UN F:X. Acts(F)); X:property; safety_prop(X) |] \
+\ ==> Allowed(F) = X";
+by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1);
+qed "def_prg_Allowed";
+
+(*For safety_prop to hold, the property must be satisfiable!*)
+Goal "B:condition ==> safety_prop(A co B) <-> (A <= B)";
+by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1);
+by Auto_tac;
+by (Blast_tac 2);
+by (force_tac (claset(), simpset() addsimps [condition_def]) 1);
+qed "safety_prop_constrains";
+Addsimps [safety_prop_constrains];
+
+
+
+Goal "A:condition ==>safety_prop(stable(A))";
+by (asm_simp_tac (simpset() addsimps [stable_def]) 1);
+qed "safety_prop_stable";
+Addsimps [safety_prop_stable];
+
+Goal "[| X:property; Y:property |] ==> \
+\ safety_prop(X) --> safety_prop(Y) --> safety_prop(X Int Y)";
+by (asm_full_simp_tac (simpset()
+ addsimps [safety_prop_def, property_def]) 1);
+by Safe_tac;
+by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"),
+ ("C", "Union(RepFun(Y, Acts))")] subset_trans 2);
+by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"),
+ ("C", "Union(RepFun(X, Acts))")] subset_trans 1);
+by (REPEAT(Blast_tac 1));
+qed "safety_prop_Int";
+Addsimps [safety_prop_Int];
+
+(* If I=0 the conclusion becomes safety_prop(0) which is false *)
+Goal "[| ALL i:I. X(i):property; i:I |] ==> \
+\ (ALL i:I. safety_prop(X(i))) --> safety_prop(INT i:I. X(i))";
+by (asm_full_simp_tac (simpset() addsimps [safety_prop_def, property_def]) 1);
+by Safe_tac;
+by (dres_inst_tac [("B", "Union(RepFun(Inter(RepFun(I, X)), Acts))"),
+ ("C", "Union(RepFun(X(xb), Acts))")] subset_trans 3);
+by (REPEAT(Blast_tac 1));
+bind_thm ("safety_prop_Inter", ballI RS result());
+
+Goal "[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X); X:property |] \
+\ ==> F ok G <-> (programify(G):X & acts Int action <= AllowedActs(G))";
+by (auto_tac (claset(),
+ simpset() addsimps [ok_def, safety_prop_Acts_iff, UN_Int_distrib, property_def]));
+qed "def_UNION_ok_iff";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Union.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,59 @@
+(* Title: ZF/UNITY/Union.thy
+ ID: $Id$
+ 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..
+
+*)
+
+Union = SubstAx + FP +
+
+constdefs
+
+ (*FIXME: conjoin Init(F) Int Init(G) ~= 0 *)
+ ok :: [i, i] => o (infixl 65)
+ "F ok G == Acts(F) <= AllowedActs(G) &
+ Acts(G) <= AllowedActs(F)"
+
+ (*FIXME: conjoin (INT i:I. Init(F(i))) ~= 0 *)
+ OK :: [i, i=>i] => o
+ "OK(I,F) == (ALL i:I. ALL 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(INT i:I. Init(F(i)), UN i:I. Acts(F(i)),
+ INT i:I. AllowedActs(F(i)))"
+
+ Join :: [i, i] => i (infixl 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) == SKIP:X &
+ (ALL G:program. Acts(G) <= (UN F:X. Acts(F)) --> G:X)"
+
+ property :: i
+ "property == Pow(program)"
+
+
+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 ("\\<bottom>")
+ "op Join" :: [i, i] => i (infixl "\\<squnion>" 65)
+ "@JOIN1" :: [pttrns, i] => i ("(3\\<Squnion> _./ _)" 10)
+ "@JOIN" :: [pttrn, i, i] => i ("(3\\<Squnion> _:_./ _)" 10)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/WFair.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,776 @@
+(* Title: HOL/UNITY/WFair.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Weak Fairness versions of transient, ensures, leadsTo.
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+(*** transient ***)
+
+Goalw [transient_def]
+"F:transient(A) ==> F:program & A:condition";
+by Auto_tac;
+qed "transientD";
+
+Goalw [stable_def, constrains_def, transient_def]
+ "[| F : stable(A); F : transient(A) |] ==> A = 0";
+by Auto_tac;
+by (Blast_tac 1);
+qed "stable_transient_empty";
+
+Goalw [transient_def]
+ "[| F : transient(A); B<=A |] ==> F : transient(B)";
+by Safe_tac;
+by (res_inst_tac [("x", "act")] bexI 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (Blast_tac 1);
+by (auto_tac (claset(),
+ simpset() addsimps [condition_def]));
+qed "transient_strengthen";
+
+Goalw [transient_def]
+"[| act:Acts(F); A <= domain(act); act``A <= state-A; \
+\ F:program; A:condition |] ==> F : transient(A)";
+by (Blast_tac 1);
+qed "transientI";
+
+val major::prems =
+Goalw [transient_def]
+ "[| F:transient(A); \
+\ !!act. [| act:Acts(F); A <= domain(act); act``A <= state-A |] ==> P |] \
+\ ==> P";
+by (rtac (major RS CollectE) 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "transientE";
+
+Goalw [transient_def] "transient(state) = 0";
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by (dtac ActsD 1);
+by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1);
+by (blast_tac (claset() addSDs [state_subset_not_empty]) 1);
+qed "transient_state";
+
+Goalw [transient_def] "transient(0) = program";
+by (rtac equalityI 1);
+by Safe_tac;
+by (subgoal_tac "Id:Acts(x)" 1);
+by (Asm_simp_tac 2);
+by (res_inst_tac [("x", "Id")] bexI 1);
+by (ALLGOALS(Blast_tac));
+qed "transient_empty";
+
+Addsimps [transient_empty, transient_state];
+
+(*** ensures ***)
+
+Goalw [ensures_def]
+ "[| F : (A-B) co (A Un B); F : transient(A-B) |] \
+\ ==> F : A ensures B";
+by (Blast_tac 1);
+qed "ensuresI";
+
+(** From Misra's notes, Progress chapter, exercise number 4 **)
+Goal "[| F:A co A Un B; F: transient(A) |] ==> F: A ensures B";
+by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
+by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
+by (auto_tac (claset(), simpset() addsimps [ensures_def]));
+qed "ensuresI2";
+
+
+Goalw [ensures_def]
+ "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)";
+by (Blast_tac 1);
+qed "ensuresD";
+
+Goalw [ensures_def, constrains_def]
+ "F : A ensures B ==> F:program & A:condition & B:condition";
+by Auto_tac;
+qed "ensuresD2";
+
+Goalw [ensures_def]
+ "[| F : A ensures A'; A'<=B'; B':condition |] ==> F : A ensures B'";
+by (Clarify_tac 1);
+by (blast_tac (claset()
+ addIs [transient_strengthen, constrains_weaken]
+ addDs [constrainsD2]) 1);
+qed "ensures_weaken_R";
+
+(*The L-version (precondition strengthening) fails, but we have this*)
+Goalw [ensures_def]
+ "[| F : stable(C); F : A ensures B |] \
+\ ==> F : (C Int A) ensures (C Int B)";
+by (asm_full_simp_tac (simpset() addsimps [ensures_def,
+ Int_Un_distrib2,
+ Diff_Int_distrib RS sym]) 1);
+by (Clarify_tac 1);
+by (blast_tac (claset()
+ addIs [transient_strengthen,
+ stable_constrains_Int, constrains_weaken]
+ addDs [constrainsD2]) 1);
+qed "stable_ensures_Int";
+
+Goal "[| F : stable(A); F : transient(C); \
+\ A <= B Un C; B:condition|] ==> F : A ensures B";
+by (asm_full_simp_tac (simpset()
+ addsimps [ensures_def, stable_def]) 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [transient_strengthen,
+ constrains_weaken]
+ addDs [constrainsD2]) 1);
+qed "stable_transient_ensures";
+
+Goal "(A ensures B) = (A unless B) Int transient (A-B)";
+by (simp_tac (simpset()
+ addsimps [ensures_def, unless_def]) 1);
+qed "ensures_eq";
+
+(*** leadsTo ***)
+
+val leads_lhs_subset = leads.dom_subset RS subsetD RS SigmaD1;
+val leads_rhs_subset = leads.dom_subset RS subsetD RS SigmaD2;
+
+Goalw [leadsTo_def]
+ "F: A leadsTo B ==> F:program & A:condition & B:condition";
+by (blast_tac (claset() addDs [leads_lhs_subset,
+ leads_rhs_subset]) 1);
+qed "leadsToD";
+
+Goalw [leadsTo_def]
+ "F : A ensures B ==> F : A leadsTo B";
+by (blast_tac (claset() addDs [ensuresD2]
+ addIs [leads.Basis]) 1);
+qed "leadsTo_Basis";
+
+AddIs [leadsTo_Basis];
+Addsimps [leadsTo_Basis];
+
+Goalw [leadsTo_def]
+ "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C";
+by (blast_tac (claset() addIs [leads.Trans]) 1);
+qed "leadsTo_Trans";
+
+(* To be move to State.thy *)
+
+Goalw [condition_def]
+ "A:condition ==> state<=A <-> A=state";
+by Auto_tac;
+qed "state_upper";
+Addsimps [state_upper];
+
+
+Goalw [transient_def]
+ "F : transient(A) ==> F : A leadsTo (state - A )";
+by (rtac (ensuresI RS leadsTo_Basis) 1);
+by (ALLGOALS(Clarify_tac));
+by (blast_tac (claset() addIs [transientI]) 2);
+by (rtac constrains_weaken 1);
+by Auto_tac;
+qed "transient_imp_leadsTo";
+
+(*Useful with cancellation, disjunction*)
+
+Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "leadsTo_Un_duplicate";
+
+Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "leadsTo_Un_duplicate2";
+
+(*The Union introduction rule as we should have liked to state it*)
+Goalw [leadsTo_def]
+ "[| ALL A:S. F : A leadsTo B; F:program; B:condition |]\
+\ ==> F : Union(S) leadsTo B";
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [leads.Union]
+ addDs [leads_lhs_subset]) 1);
+bind_thm ("leadsTo_Union", ballI RS result());
+
+Goalw [leadsTo_def]
+ "[| ALL A:S. F: (A Int C) leadsTo B; F:program; B:condition |] \
+ \ ==> F : (Union(S) Int C) leadsTo B";
+by (Clarify_tac 1);
+by (simp_tac (simpset() addsimps [Int_Union_Union]) 1);
+by (blast_tac (claset() addIs [leads.Union]
+ addDs [leads_lhs_subset, leads_rhs_subset]) 1);
+bind_thm ("leadsTo_Union_Int", ballI RS result());
+
+Goalw [leadsTo_def]
+"[| ALL i:I. F : (A(i)) leadsTo B; F:program; B:condition |] \
+\ ==> F:(UN i:I. A(i)) leadsTo B";
+by (Clarify_tac 1);
+by (simp_tac (simpset() addsimps [Int_Union_Union]) 1);
+by (blast_tac (claset() addIs [leads.Union]
+ addDs [leads_lhs_subset, leads_rhs_subset]) 1);
+bind_thm ("leadsTo_UN", ballI RS result());
+
+(*Binary union introduction rule*)
+Goal "[| F: A leadsTo C; F: B leadsTo C |] ==> F : (A Un B) leadsTo C";
+by (stac Un_eq_Union 1);
+by (blast_tac (claset() addIs [leadsTo_Union]
+ addDs [leadsToD]) 1);
+qed "leadsTo_Un";
+
+
+Goal "[| ALL x:A. F:{x} leadsTo B; \
+\ F:program; B:condition |] ==> F : A leadsTo B";
+by (res_inst_tac [("b", "A")] (UN_singleton RS subst) 1);
+by (blast_tac (claset() addIs [leadsTo_UN]) 1);
+bind_thm("single_leadsTo_I", ballI RS result());
+
+
+(*The INDUCTION rule as we should have liked to state it*)
+val major::prems = Goalw [leadsTo_def]
+ "[| F: za leadsTo zb; \
+\ !!A B. F : A ensures B ==> P(A, B); \
+\ !!A B C. [| F: A leadsTo B; P(A, B); \
+\ F: B leadsTo C; P(B, C) |] \
+\ ==> P(A, C); \
+\ !!B S. [| ALL A:S. F:A leadsTo B & P(A, B); B:condition |] \
+\ ==> P(Union(S), B) \
+\ |] ==> P(za, zb)";
+by (cut_facts_tac [major] 1);
+by (rtac (major RS CollectD2 RS leads.induct) 1);
+by (auto_tac (claset() addIs prems, simpset()));
+qed "leadsTo_induct";
+
+Goal
+"[| A<=B; F:program; B:condition |] \
+\ ==> F : A ensures B";
+by (rewrite_goals_tac [ensures_def, constrains_def,
+ transient_def, condition_def]);
+by (Clarify_tac 1);
+by Safe_tac;
+by (res_inst_tac [("x", "Id")] bexI 5);
+by (REPEAT(blast_tac (claset() addDs [Id_in_Acts]) 1));
+qed "subset_imp_ensures";
+
+bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis);
+bind_thm ("leadsTo_refl", subset_refl RS subset_imp_leadsTo);
+
+bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
+
+Addsimps [empty_leadsTo];
+
+Goalw [condition_def]
+ "[| F:program; A:condition |] ==> F: A leadsTo state";
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+qed "leadsTo_state";
+Addsimps [leadsTo_state];
+
+(* A nicer induction rule; without ensures *)
+val [major,impl,basis,trans,unionp] = Goal
+ "[| F: za leadsTo zb; \
+\ !!A B. [| A<=B; B:condition |] ==> P(A, B); \
+\ !!A B. [| F:A co A Un B; F:transient(A) |] ==> P(A, B); \
+\ !!A B C. [| F: A leadsTo B; P(A, B); \
+\ F: B leadsTo C; P(B, C) |] \
+\ ==> P(A, C); \
+\ !!B S. [| ALL A:S. F:A leadsTo B & P(A, B); B:condition |] \
+\ ==> P(Union(S), B) \
+\ |] ==> P(za, zb)";
+by (cut_facts_tac [major] 1);
+by (etac leadsTo_induct 1);
+by (auto_tac (claset() addIs [trans,unionp], simpset()));
+by (rewrite_goal_tac [ensures_def] 1);
+by Auto_tac;
+by (forward_tac [constrainsD2] 1);
+by (dres_inst_tac [("B'", "(A-B) Un B")] constrains_weaken_R 1);
+by Auto_tac;
+by (forward_tac [ensuresI2 RS leadsTo_Basis] 1);
+by (dtac basis 2);
+by (subgoal_tac "A Int B <= B " 3);
+by Auto_tac;
+by (dtac impl 1);
+by Auto_tac;
+by (res_inst_tac [("a", "Union({A - B, A Int B})"), ("P", "%x. P(x, ?u)")] subst 1);
+by (rtac unionp 2);
+by (auto_tac (claset() addIs [subset_imp_leadsTo], simpset()));
+qed "leadsTo_induct2";
+
+
+
+(** Variant induction rule: on the preconditions for B **)
+(*Lemma is the weak version: can't see how to do it in one step*)
+val major::prems = Goal
+ "[| F : za leadsTo zb; \
+\ P(zb); \
+\ !!A B. [| F : A ensures B; P(B) |] ==> P(A); \
+\ !!S. [| ALL A:S. P(A) |] ==> P(Union(S)) \
+\ |] ==> P(za)";
+(*by induction on this formula*)
+by (subgoal_tac "P(zb) --> P(za)" 1);
+(*now solve first subgoal: this formula is sufficient*)
+by (blast_tac (claset() addIs leadsTo_refl::prems) 1);
+by (rtac (major RS leadsTo_induct) 1);
+by (REPEAT (blast_tac (claset() addIs prems) 1));
+qed "lemma";
+
+
+val [major, cond, ensuresp, unionp] = Goal
+ "[| F : za leadsTo zb; \
+\ P(zb); \
+\ !!A B. [| F : A ensures B; F : B leadsTo zb; P(B) |] ==> P(A); \
+\ !!S. ALL A:S. F : A leadsTo zb & P(A) ==> P(Union(S)) \
+\ |] ==> P(za)";
+by (cut_facts_tac [major] 1);
+by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1);
+by (etac conjunct2 1);
+by (rtac (major RS lemma) 1);
+by (blast_tac (claset() addDs [leadsToD]
+ addIs [leadsTo_Union,unionp]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans,ensuresp]) 2);
+by (blast_tac (claset() addIs [conjI,leadsTo_refl,cond]
+ addDs [leadsToD]) 1);
+qed "leadsTo_induct_pre";
+
+
+Goal
+"[| F : A leadsTo A'; A'<=B'; B':condition |]\
+\ ==> F : A leadsTo B'";
+by (blast_tac (claset() addIs [subset_imp_leadsTo,
+ leadsTo_Trans]
+ addDs [leadsToD]) 1);
+qed "leadsTo_weaken_R";
+
+
+Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
+by (blast_tac (claset()
+ addIs [leadsTo_Trans, subset_imp_leadsTo]
+ addDs [leadsToD]) 1);
+qed_spec_mp "leadsTo_weaken_L";
+
+(*Distributes over binary unions*)
+Goal "F:(A Un B) leadsTo C <-> (F:A leadsTo C & F : B leadsTo C)";
+by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
+qed "leadsTo_Un_distrib";
+
+Goal "[| F:program; B:condition |] \
+\==> F : (UN i:I. A(i)) leadsTo B <-> (ALL i : I. F : (A(i)) leadsTo B)";
+by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
+qed "leadsTo_UN_distrib";
+
+Goal "[| F:program; B:condition |] \
+\==> F : (Union(S)) leadsTo B <-> (ALL A:S. F : A leadsTo B)";
+by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
+qed "leadsTo_Union_distrib";
+
+Goal
+"[| F : A leadsTo A'; B<=A; A'<=B'; B':condition |] \
+\ ==> F : B leadsTo B'";
+by (subgoal_tac "B:condition & A':condition" 1);
+by (force_tac (claset() addSDs [leadsToD],
+ simpset() addsimps [condition_def]) 2);
+by (blast_tac (claset()
+ addIs [leadsTo_weaken_R, leadsTo_weaken_L, leadsTo_Trans]) 1);
+qed "leadsTo_weaken";
+
+(*Set difference: maybe combine with leadsTo_weaken_L?*)
+Goal "[| F : (A-B) leadsTo C; F : B leadsTo C|] ==> F : A leadsTo C";
+by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]
+ addDs [leadsToD]) 1);
+qed "leadsTo_Diff";
+
+
+Goal "[| ALL i:I. F : (A(i)) leadsTo (A'(i)); F:program |] \
+\ ==> F:(UN i:I. A(i)) leadsTo (UN i:I. A'(i))";
+by (rtac leadsTo_Union 1);
+by (ALLGOALS(Clarify_tac));
+by (REPEAT(blast_tac (claset()
+ addIs [leadsTo_weaken_R] addDs [leadsToD]) 1));
+qed "leadsTo_UN_UN";
+
+(*Binary union version*)
+Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
+\ ==> F : (A Un B) leadsTo (A' Un B')";
+by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]
+ addDs [leadsToD]) 1);
+qed "leadsTo_Un_Un";
+
+
+(** The cancellation law **)
+
+Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \
+\ ==> F : A leadsTo (A' Un B')";
+by (blast_tac (claset()
+ addIs [leadsTo_Trans, leadsTo_Un_Un, leadsTo_refl]
+ addDs [leadsToD]) 1);
+qed "leadsTo_cancel2";
+
+Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \
+\ ==> F : A leadsTo (A' Un B')";
+by (rtac leadsTo_cancel2 1);
+by (assume_tac 2);
+by (blast_tac (claset() addIs [leadsTo_weaken_R]
+ addDs [leadsToD]) 1);
+qed "leadsTo_cancel_Diff2";
+
+
+Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \
+\ ==> F : A leadsTo (B' Un A')";
+by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
+by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
+qed "leadsTo_cancel1";
+
+Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \
+\ ==> F : A leadsTo (B' Un A')";
+by (rtac leadsTo_cancel1 1);
+by (assume_tac 2);
+by (blast_tac (claset()
+ addIs [leadsTo_weaken_R]
+ addDs [leadsToD]) 1);
+qed "leadsTo_cancel_Diff1";
+
+(** The impossibility law **)
+
+Goal
+ "F : A leadsTo 0 ==> A=0";
+by (etac leadsTo_induct_pre 1);
+by (rewrite_goals_tac
+ [ensures_def, constrains_def, transient_def]);
+by Auto_tac;
+by (auto_tac (claset() addSDs [Acts_type],
+ simpset() addsimps
+ [actionSet_def, condition_def]));
+by (blast_tac (claset() addSDs [bspec]) 1);
+qed "leadsTo_empty";
+
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction"*)
+Goalw [stable_def]
+ "[| F : A leadsTo A'; F : stable(B) |] ==> \
+\ F:(A Int B) leadsTo (A' Int B)";
+by (etac leadsTo_induct 1);
+by (rtac leadsTo_Union_Int 3);
+by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
+by (rtac leadsTo_Basis 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [ensures_def, Diff_Int_distrib RS sym,
+ Diff_Int_distrib2 RS sym, Int_Un_distrib RS sym]) 1);
+by (REPEAT(blast_tac (claset()
+ addIs [transient_strengthen,constrains_Int]
+ addDs [constrainsD2]) 1));
+qed "psp_stable";
+
+
+Goal
+ "[| F : A leadsTo A'; F : stable(B) |] \
+\ ==> F : (B Int A) leadsTo (B Int A')";
+by (asm_simp_tac (simpset()
+ addsimps psp_stable::Int_ac) 1);
+qed "psp_stable2";
+
+
+Goalw [ensures_def, constrains_def]
+ "[| F : A ensures A'; F : B co B' |] \
+\ ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))";
+(*speeds up the proof*)
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [transient_strengthen]) 1);
+qed "psp_ensures";
+
+Goal "[| F : A leadsTo A'; F : B co B' |] \
+\ ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))";
+by (subgoal_tac "F:program & A:condition & \
+ \ A':condition & B:condition & B':condition" 1);
+by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2);
+by (etac leadsTo_induct 1);
+by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
+(*Transitivity case has a delicate argument involving "cancellation"*)
+by (rtac leadsTo_Un_duplicate2 2);
+by (etac leadsTo_cancel_Diff1 2);
+by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
+by (blast_tac (claset() addIs [leadsTo_weaken_L]
+ addDs [constrains_imp_subset]) 2);
+(*Basis case*)
+by (blast_tac (claset() addIs [psp_ensures]) 1);
+qed "psp";
+
+
+Goal "[| F : A leadsTo A'; F : B co B' |] \
+\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))";
+by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
+qed "psp2";
+
+
+
+Goalw [unless_def]
+ "[| F : A leadsTo A'; F : B unless B' |] \
+\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')";
+by (subgoal_tac "F:program & A:condition & A':condition &\
+ \ B:condition & B':condition" 1);
+by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2);
+by (dtac psp 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+qed "psp_unless";
+
+(*** Proving the induction rules ***)
+(** The most general rule: r is any wf relation; f is any variant function **)
+Goal "[| wf(r); \
+\ m:I; \
+\ field(r)<=I; \
+\ F:program; B:condition;\
+\ ALL m:I. F : (A Int f-``{m}) leadsTo \
+\ ((A Int f-``(converse(r)``{m})) Un B) |] \
+\ ==> F : (A Int f-``{m}) leadsTo B";
+by (eres_inst_tac [("a","m")] wf_induct2 1);
+by (ALLGOALS(Asm_simp_tac));
+by (subgoal_tac "F : (A Int (f-``(converse(r)``{x}))) leadsTo B" 1);
+by (stac vimage_eq_UN 2);
+by (asm_simp_tac (simpset() addsimps [Int_UN_distrib]) 2);
+by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
+by (case_tac "converse(r)``{x}=0" 1);
+by (auto_tac (claset() addSEs [not_emptyE] addSIs [leadsTo_UN], simpset()));
+qed "lemma1";
+
+(** Meta or object quantifier ? **)
+Goal "[| wf(r); \
+\ field(r)<=I; \
+\ A<=f-``I;\
+\ F:program; A:condition; B:condition; \
+\ ALL m:I. F : (A Int f-``{m}) leadsTo \
+\ ((A Int f-``(converse(r)``{m})) Un B) |] \
+\ ==> F : A leadsTo B";
+by (res_inst_tac [("b", "A")] subst 1);
+by (res_inst_tac [("I", "I")] leadsTo_UN 2);
+by (REPEAT (assume_tac 2));
+by (Clarify_tac 2);
+by (eres_inst_tac [("I", "I")] lemma1 2);
+by (REPEAT (assume_tac 2));
+by (rtac equalityI 1);
+by Safe_tac;
+by (thin_tac "field(r)<=I" 1);
+by (dres_inst_tac [("c", "x")] subsetD 1);
+by Safe_tac;
+by (res_inst_tac [("b", "x")] UN_I 1);
+by Auto_tac;
+qed "leadsTo_wf_induct";
+
+Goalw [field_def] "field(less_than(nat)) = nat";
+by (simp_tac (simpset() addsimps [less_than_equals]) 1);
+by (rtac equalityI 1);
+by (force_tac (claset() addSEs [rangeE], simpset()) 1);
+by (Clarify_tac 1);
+by (thin_tac "x~:range(?y)" 1);
+by (etac nat_induct 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [domain_def])));
+by (res_inst_tac [("x", "<succ(xa),succ(succ(xa))>")] ReplaceI 2);
+by (res_inst_tac [("x", "<0,1>")] ReplaceI 1);
+by (REPEAT(force_tac (claset() addIs [splitI], simpset()) 1));
+qed "nat_less_than_field";
+
+(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
+Goal
+ "[| A<=f-``nat;\
+\ F:program; A:condition; B:condition; \
+\ ALL m:nat. F:(A Int f-``{m}) leadsTo ((A Int f-``lessThan(m,nat)) Un B) |] \
+\ ==> F : A leadsTo B";
+by (res_inst_tac [("A1", "nat")]
+ (wf_less_than RS leadsTo_wf_induct) 1);
+by (Clarify_tac 6);
+by (ALLGOALS(asm_full_simp_tac
+ (simpset() addsimps [nat_less_than_field])));
+by (Clarify_tac 1);
+by (ALLGOALS(asm_full_simp_tac
+ (simpset() addsimps [rewrite_rule [vimage_def] Image_inverse_less_than])));
+qed "lessThan_induct";
+
+
+(*** wlt ****)
+
+(*Misra's property W3*)
+Goalw [wlt_def]
+"[| F:program; B:condition |] ==> F:wlt(F, B) leadsTo B";
+by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
+qed "wlt_leadsTo";
+
+Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt(F, B)";
+by (blast_tac (claset() addSIs [leadsTo_Union]
+ addDs [leadsToD]) 1);
+qed "leadsTo_subset";
+
+(*Misra's property W2*)
+Goal "[| F:program; B:condition |] ==> \
+\ F : A leadsTo B <-> (A <= wlt(F,B))";
+by (blast_tac (claset()
+ addSIs [leadsTo_subset, wlt_leadsTo RS leadsTo_weaken_L]) 1);
+qed "leadsTo_eq_subset_wlt";
+
+(*Misra's property W4*)
+Goal "[| F:program; B:condition |] ==> B <= wlt(F,B)";
+by (asm_simp_tac (simpset()
+ addsimps [leadsTo_eq_subset_wlt RS iff_sym,
+ subset_imp_leadsTo]) 1);
+qed "wlt_increasing";
+
+(*Used in the Trans case below*)
+Goalw [constrains_def]
+ "[| B <= A2; \
+\ F : (A1 - B) co (A1 Un B); \
+\ F : (A2 - C) co (A2 Un C) |] \
+\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
+by (Clarify_tac 1);
+by (Blast_tac 1);
+qed "lemma1";
+
+
+
+(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
+(* slightly different from the HOL one: B here is bounded *)
+Goal "F : A leadsTo A' \
+\ ==> EX B:condition. A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')";
+by (forward_tac [leadsToD] 1);
+by (etac leadsTo_induct 1);
+(*Basis*)
+by (blast_tac (claset() addDs [ensuresD, constrainsD2]) 1);
+(*Trans*)
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "Ba Un Bb")] bexI 1);
+by (blast_tac (claset() addIs [lemma1,leadsTo_Un_Un, leadsTo_cancel1,
+ leadsTo_Un_duplicate]) 1);
+by (Blast_tac 1);
+(*Union*)
+by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1]) 1);
+by (subgoal_tac "EX y. y:Pi(S, %A. {Ba:condition. A<=Ba & \
+ \ F:Ba leadsTo B & F:Ba - B co Ba Un B})" 1);
+by (rtac AC_ball_Pi 2);
+by (Clarify_tac 2);
+by (rotate_tac 3 2);
+by (blast_tac (claset() addSDs [bspec]) 2);
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "UN A:S. y`A")] bexI 1);
+by Safe_tac;
+by (res_inst_tac [("I1", "S")] (constrains_UN RS constrains_weaken) 3);
+by (rtac leadsTo_Union 2);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [condition_def]) 7);
+by (asm_full_simp_tac (simpset() addsimps [condition_def]) 6);
+by (REPEAT(blast_tac (claset() addDs [apply_type]) 1));
+qed "leadsTo_123";
+
+
+(*Misra's property W5*)
+Goal "[| F:program; B:condition |] ==>F : (wlt(F, B) - B) co (wlt(F,B))";
+by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "Ba = wlt(F,B)" 1);
+by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [wlt_increasing RS (subset_Un_iff2 RS iffD1)]) 1);
+qed "wlt_constrains_wlt";
+
+Goalw [wlt_def, condition_def]
+ "wlt(F,B):condition";
+by Auto_tac;
+qed "wlt_in_condition";
+
+(*** Completion: Binary and General Finite versions ***)
+
+Goal "[| W = wlt(F, (B' Un C)); \
+\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \
+\ F : B leadsTo (B' Un C); F : B' co (B' Un C) |] \
+\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)";
+by (subgoal_tac "W:condition" 1);
+by (blast_tac (claset() addIs [wlt_in_condition]) 2);
+by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
+by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt]
+ MRS constrains_Un RS constrains_weaken]
+ addDs [leadsToD, constrainsD2]) 2);
+by (subgoal_tac "F : (W-C) co W" 1);
+by (subgoals_tac ["F:program", "(B' Un C):condition"] 2);
+by (rotate_tac ~2 2);
+by (asm_full_simp_tac
+ (simpset() addsimps
+ [wlt_increasing RS (subset_Un_iff2 RS iffD1), Un_assoc]) 2);
+by (REPEAT(blast_tac (claset() addDs [leadsToD, constrainsD]) 2));
+by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
+by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]
+ addDs [leadsToD, constrainsD2]) 2);
+(** LEVEL 6 **)
+by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
+by (subgoal_tac "A' Int W Un C:condition & A' Int B' Un C:condition" 2);
+by (rtac leadsTo_Un_duplicate2 2);
+by (blast_tac (claset()
+ addIs [leadsTo_Un_Un, wlt_leadsTo RS
+ psp2 RS leadsTo_weaken,leadsTo_refl]
+ addDs [leadsToD, constrainsD]) 2);
+by (thin_tac "W=wlt(F, B' Un C)" 2);
+by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2);
+by (dtac leadsTo_Diff 1);
+by (blast_tac (claset() addIs [subset_imp_leadsTo]
+ addDs [leadsToD, constrainsD2]) 1);
+by (subgoal_tac "A Int B <= A Int W" 1);
+by (blast_tac (claset() addSDs [leadsTo_subset]
+ addSIs [subset_refl RS Int_mono]) 2);
+(** To speed the proof **)
+by (subgoal_tac "A Int B :condition & A \
+ \ Int W :condition & A' Int B' Un C:condition" 1);
+by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]
+ addDs [leadsToD, constrainsD2]) 1);
+by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 1);
+bind_thm("completion", refl RS result());
+
+Goal "[| I:Fin(X); F:program; C:condition |] ==> \
+\(ALL i:I. F : (A(i)) leadsTo (A'(i) Un C)) --> \
+\ (ALL i:I. F : (A'(i)) co (A'(i) Un C)) --> \
+\ F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)";
+by (etac Fin_induct 1);
+by Auto_tac;
+by (case_tac "y=0" 1);
+by Auto_tac;
+by (etac not_emptyE 1);
+by (subgoal_tac "Inter(cons(A(x), RepFun(y, A)))= A(x) Int Inter(RepFun(y,A)) & \
+ \ Inter(cons(A'(x), RepFun(y, A')))= A'(x) Int Inter(RepFun(y,A'))" 1);
+by (Blast_tac 2);
+by (Asm_simp_tac 1);
+by (rtac completion 1);
+by (subgoal_tac "Inter(RepFun(y, A')) Un C = (INT x:RepFun(y, A'). x Un C)" 4);
+by (Blast_tac 5);
+by (Asm_simp_tac 4);
+by (rtac constrains_INT 4);
+by (REPEAT(Blast_tac 1));
+qed "lemma";
+
+val prems = Goal
+ "[| I:Fin(X); \
+\ !!i. i:I ==> F : A(i) leadsTo (A'(i) Un C); \
+\ !!i. i:I ==> F : A'(i) co (A'(i) Un C); F:program; C:condition |] \
+\ ==> F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)";
+by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
+qed "finite_completion";
+
+Goalw [stable_def]
+ "[| F : A leadsTo A'; F : stable(A'); \
+\ F : B leadsTo B'; F : stable(B') |] \
+\ ==> F : (A Int B) leadsTo (A' Int B')";
+by (res_inst_tac [("C1", "0")] (completion RS leadsTo_weaken_R) 1);
+by (REPEAT(blast_tac (claset() addDs [leadsToD, constrainsD2]) 5));
+by (ALLGOALS(Asm_full_simp_tac));
+qed "stable_completion";
+
+
+val prems = Goalw [stable_def]
+ "[| I:Fin(X); \
+\ ALL i:I. F : A(i) leadsTo A'(i); \
+\ ALL i:I. F: stable(A'(i)); F:program |] \
+\ ==> F : (INT i:I. A(i)) leadsTo (INT i:I. A'(i))";
+by (subgoal_tac "(INT i:I. A'(i)):condition" 1);
+by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2);
+by (res_inst_tac [("C1", "0")] (finite_completion RS leadsTo_weaken_R) 1);
+by (assume_tac 7);
+by (ALLGOALS(Asm_full_simp_tac));
+by (ALLGOALS (Blast_tac));
+qed "finite_stable_completion";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/WFair.thy Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,57 @@
+(* Title: HOL/UNITY/WFair.thy
+ ID: $Id$
+ Author: Sidi Ehmety, Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Weak Fairness versions of transient, ensures, leadsTo.
+
+From Misra, "A Logic for Concurrent Programming", 1994
+
+Theory ported from HOL.
+*)
+
+WFair = UNITY +
+constdefs
+
+ (*This definition specifies weak fairness. The rest of the theory
+ is generic to all forms of fairness.*)
+ transient :: "i=>i"
+ "transient(A) =={F:program. (EX act: Acts(F).
+ A<= domain(act) & act``A <= state-A) & A:condition}"
+
+ ensures :: "[i,i] => i" (infixl 60)
+ "A ensures B == ((A-B) co (A Un B)) Int transient(A-B)"
+
+consts
+
+ (*LEADS-TO constant for the inductive definition*)
+ leads :: "i=>i"
+
+inductive (* All typing conidition `A:condition' will desapear
+ in the dervied rules *)
+ domains
+ "leads(F)" <= "condition*condition"
+ intrs
+ Basis "[| F:A ensures B; A:condition; B:condition |] ==> <A,B>:leads(F)"
+ Trans "[| <A,B> : leads(F); <B,C> : leads(F) |] ==> <A,C>:leads(F)"
+ Union "[| S:Pow({A:S. <A, B>:leads(F)});
+ B:condition; S:Pow(condition) |] ==>
+ <Union(S),B>:leads(F)"
+
+ monos Pow_mono
+ type_intrs "[UnionI, Union_in_conditionI, PowI]"
+
+constdefs
+
+ (*visible version of the LEADS-TO relation*)
+ leadsTo :: "[i, i] => i" (infixl 60)
+ "A leadsTo B == {F:program. <A,B>:leads(F)}"
+
+ (*wlt F B is the largest set that leads to B*)
+ wlt :: "[i, i] => i"
+ "wlt(F, B) == Union({A:condition. F: A leadsTo B})"
+
+syntax (xsymbols)
+ "op leadsTo" :: "[i, i] => i" (infixl "\\<longmapsto>" 60)
+
+end