# HG changeset patch # User paulson # Date 997273990 -7200 # Node ID 697dcaaf478ff06cadf2dab76031024506e01754 # Parent 0f57375aafce9b2dd18f90d1587648c889d04044 new ZF/UNITY theory diff -r 0f57375aafce -r 697dcaaf478f src/ZF/IsaMakefile --- 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 diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Comp.ML --- /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); : 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]; diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Comp.thy --- /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 diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Constrains.ML --- /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. : 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); :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. :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; diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Constrains.thy --- /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 ==> : traces(init,acts)" + + Acts "[| act:acts; : traces(init,acts); : act |] + ==> : 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); : 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. :r}))}" + +end + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/FP.ML --- /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"; + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/FP.thy --- /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 diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Guar.ML --- /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"; + + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Guar.thy --- /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 diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Mutex.ML --- /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"; diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Mutex.thy --- /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 == {:state*state. t = s(u:=1, m:=#1) & s`m = #0}" + + U1 :: i + "U1 == {:state*state. t = s(p:= s`v, m:=#2) & s`m = #1}" + + U2 :: i + "U2 == {:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}" + + U3 :: i + "U3 == {:state*state. t=s(u:=0, m:=#4) & s`m = #3}" + + U4 :: i + "U4 == {:state*state. t = s(p:=1, m:=#0) & s`m = #4}" + + + (** The program for process V **) + + V0 :: i + "V0 == {:state*state. t = s (v:=1, n:=#1) & s`n = #0}" + + V1 :: i + "V1 == {:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}" + + V2 :: i + "V2 == {:state*state. t = s(n:=#3) & s`p=1 & s`n = #2}" + + V3 :: i + "V3 == {:state*state. t = s (v:=0, n:=#4) & s`n = #3}" + + V4 :: i + "V4 == {: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 diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/ROOT.ML --- /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"; diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/State.ML --- /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=)"; +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]; diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/State.thy --- /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 diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/SubstAx.ML --- /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]); + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/SubstAx.thy --- /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 " \\w " 60) + +end diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/UNITY.ML --- /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 == {:A*B. P(s, s')} |] ==> \ +\ (:act) <-> (: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); :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. :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 diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/UNITY.thy --- /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 == {:condition*actionSet*actionSet. + Id:acts & Id:allowed}" + + mk_program :: [i,i,i]=>i + "mk_program(init, acts, allowed) == + " + + 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 == {: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. :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 + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/UNITYMisc.ML --- /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) = {:A*A. x:less_than(A) <-> (x:A & y:A & x i:A & i i:A & kless_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"; + + + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/UNITYMisc.thy --- /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 i + "greaterThan(u,A) == {x:A. ui + "Identity(A) == {p:A*A. EX x. p=}" +end \ No newline at end of file diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Union.ML --- /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"; + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/Union.thy --- /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 ("\\") + "op Join" :: [i, i] => i (infixl "\\" 65) + "@JOIN1" :: [pttrns, i] => i ("(3\\ _./ _)" 10) + "@JOIN" :: [pttrn, i, i] => i ("(3\\ _:_./ _)" 10) + +end diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/WFair.ML --- /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", "")] 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"; + diff -r 0f57375aafce -r 697dcaaf478f src/ZF/UNITY/WFair.thy --- /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 |] ==> :leads(F)" + Trans "[| : leads(F); : leads(F) |] ==> :leads(F)" + Union "[| S:Pow({A:S. :leads(F)}); + B:condition; S:Pow(condition) |] ==> + :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. :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 "\\" 60) + +end