--- a/src/HOL/IsaMakefile Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/IsaMakefile Wed Jan 29 16:34:51 2003 +0100
@@ -382,13 +382,13 @@
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
- UNITY/Comp.ML UNITY/Comp.thy UNITY/Detects.thy UNITY/ELT.thy \
+ UNITY/Comp.thy UNITY/Detects.thy UNITY/ELT.thy \
UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \
UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
- UNITY/Guar.ML UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \
+ UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \
UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \
UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML \
- UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \
+ UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \
UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \
UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy \
--- a/src/HOL/UNITY/Comp.ML Wed Jan 29 16:29:38 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,263 +0,0 @@
-(* Title: HOL/UNITY/Comp.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Composition
-From Chandy and Sanders, "Reasoning About Program Composition"
-
-Revised by Sidi Ehmety on January 2001
-
-*)
-(*** component <= ***)
-Goalw [component_def]
- "H <= F | H <= G ==> H <= (F Join G)";
-by Auto_tac;
-by (res_inst_tac [("x", "G Join Ga")] 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]
- "(F <= G) = \
-\ (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)";
-by (force_tac (claset() addSIs [exI, program_equalityI],
- simpset()) 1);
-qed "component_eq_subset";
-
-Goalw [component_def] "SKIP <= F";
-by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
-qed "component_SKIP";
-
-Goalw [component_def] "F <= (F :: 'a program)";
-by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
-qed "component_refl";
-
-AddIffs [component_SKIP, component_refl];
-
-Goal "F <= SKIP ==> F = SKIP";
-by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [component_eq_subset]));
-qed "SKIP_minimal";
-
-Goalw [component_def] "F <= (F Join G)";
-by (Blast_tac 1);
-qed "component_Join1";
-
-Goalw [component_def] "G <= (F Join G)";
-by (simp_tac (simpset() addsimps [Join_commute]) 1);
-by (Blast_tac 1);
-qed "component_Join2";
-
-Goal "F<=G ==> F Join G = G";
-by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb]));
-qed "Join_absorb1";
-
-Goal "G<=F ==> F Join G = F";
-by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
-qed "Join_absorb2";
-
-Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
-by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by (Blast_tac 1);
-qed "JN_component_iff";
-
-Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
-by (blast_tac (claset() addIs [JN_absorb]) 1);
-qed "component_JN";
-
-Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)";
-by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
-qed "component_trans";
-
-Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)";
-by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by (blast_tac (claset() addSIs [program_equalityI]) 1);
-qed "component_antisym";
-
-Goal "((F Join G) <= H) = (F <= H & G <= H)";
-by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by (Blast_tac 1);
-qed "Join_component_iff";
-
-Goal "[| F <= G; G : A co B |] ==> F : A co B";
-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] "(!!z. F : stable {s. v s = z}) ==> F : preserves v";
-by (blast_tac (claset() addIs prems) 1);
-qed "preservesI";
-
-Goalw [preserves_def, stable_def, constrains_def]
- "[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'";
-by (Force_tac 1);
-qed "preserves_imp_eq";
-
-Goalw [preserves_def]
- "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
-by Auto_tac;
-qed "Join_preserves";
-
-Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)";
-by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1);
-by (Blast_tac 1);
-qed "JN_preserves";
-
-Goal "SKIP : preserves v";
-by (auto_tac (claset(), simpset() addsimps [preserves_def]));
-qed "SKIP_preserves";
-
-AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
-
-Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
-by (Simp_tac 1);
-qed "funPair_apply";
-Addsimps [funPair_apply];
-
-Goal "preserves (funPair v w) = preserves v Int preserves w";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, stable_def, constrains_def]));
-by (Blast_tac 1);
-qed "preserves_funPair";
-
-(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
-AddIffs [preserves_funPair RS eqset_imp_iff];
-
-
-Goal "(funPair f g) o h = funPair (f o h) (g o h)";
-by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
-qed "funPair_o_distrib";
-
-Goal "fst o (funPair f g) = f";
-by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
-qed "fst_o_funPair";
-
-Goal "snd o (funPair f g) = g";
-by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
-qed "snd_o_funPair";
-Addsimps [fst_o_funPair, snd_o_funPair];
-
-Goal "preserves v <= preserves (w o v)";
-by (force_tac (claset(),
- simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
-qed "subset_preserves_o";
-
-Goal "preserves v <= stable {s. P (v s)}";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, stable_def, constrains_def]));
-by (rename_tac "s' s" 1);
-by (subgoal_tac "v s = v s'" 1);
-by (ALLGOALS Force_tac);
-qed "preserves_subset_stable";
-
-Goal "preserves v <= increasing v";
-by (auto_tac (claset(),
- simpset() addsimps [impOfSubs preserves_subset_stable,
- increasing_def]));
-qed "preserves_subset_increasing";
-
-Goal "preserves id <= stable A";
-by (force_tac (claset(),
- simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
-qed "preserves_id_subset_stable";
-
-
-(** For use with def_UNION_ok_iff **)
-
-Goal "safety_prop (preserves v)";
-by (auto_tac (claset() addIs [safety_prop_INTER1],
- simpset() addsimps [preserves_def]));
-qed "safety_prop_preserves";
-AddIffs [safety_prop_preserves];
-
-
-(** Some lemmas used only in Client.ML **)
-
-Goal "[| F : stable {s. P (v s) (w s)}; \
-\ G : preserves v; G : preserves w |] \
-\ ==> F Join G : stable {s. P (v s) (w s)}";
-by (Asm_simp_tac 1);
-by (subgoal_tac "G: preserves (funPair v w)" 1);
-by (Asm_simp_tac 2);
-by (dres_inst_tac [("P1", "split ?Q")]
- (impOfSubs preserves_subset_stable) 1);
-by Auto_tac;
-qed "stable_localTo_stable2";
-
-Goal "[| F : stable {s. v s <= w s}; G : preserves v; \
-\ F Join G : Increasing w |] \
-\ ==> F Join G : Stable {s. v s <= w s}";
-by (auto_tac (claset(),
- simpset() addsimps [stable_def, Stable_def, Increasing_def,
- Constrains_def, all_conj_distrib]));
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-(*The G case remains*)
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, stable_def, constrains_def]));
-by (case_tac "act: Acts F" 1);
-by (Blast_tac 1);
-(*We have a G-action, so delete assumptions about F-actions*)
-by (thin_tac "ALL act:Acts F. ?P act" 1);
-by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
-by (subgoal_tac "v x = v xa" 1);
-by (Blast_tac 2);
-by Auto_tac;
-by (etac order_trans 1);
-by (Blast_tac 1);
-qed "Increasing_preserves_Stable";
-
-(** component_of **)
-
-(* component_of is stronger than <= *)
-Goalw [component_def, component_of_def]
-"F component_of H ==> F <= H";
-by (Blast_tac 1);
-qed "component_of_imp_component";
-
-
-(* component_of satisfies many of the <='s properties *)
-Goalw [component_of_def]
-"F component_of F";
-by (res_inst_tac [("x", "SKIP")] exI 1);
-by Auto_tac;
-qed "component_of_refl";
-
-Goalw [component_of_def]
-"SKIP component_of F";
-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";
-
-bind_thm ("strict_component_of_eq", strict_component_of_def RS meta_eq_to_obj_eq);
-
-(** 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];
--- a/src/HOL/UNITY/Comp.thy Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy Wed Jan 29 16:34:51 2003 +0100
@@ -13,14 +13,13 @@
*)
-Comp = Union +
+theory Comp = Union:
-instance
- program :: (type) ord
+instance program :: (type) ord ..
defs
- component_def "F <= H == EX G. F Join G = H"
- strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)"
+ component_def: "F <= H == EX G. F Join G = H"
+ strict_component_def: "(F < (H::'a program)) == (F <= H & F ~= H)"
constdefs
@@ -28,7 +27,7 @@
(infixl "component'_of" 50)
"F component_of H == EX G. F ok G & F Join G = H"
- strict_component_of :: "'a program\\<Rightarrow>'a program=> bool"
+ strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
(infixl "strict'_component'_of" 50)
"F strict_component_of H == F component_of H & F~=H"
@@ -41,4 +40,222 @@
funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
"funPair f g == %x. (f x, g x)"
+
+
+(*** component <= ***)
+lemma componentI:
+ "H <= F | H <= G ==> H <= (F Join G)"
+apply (unfold component_def, auto)
+apply (rule_tac x = "G Join Ga" in exI)
+apply (rule_tac [2] x = "G Join F" in exI)
+apply (auto simp add: Join_ac)
+done
+
+lemma component_eq_subset:
+ "(F <= G) =
+ (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"
+apply (unfold component_def)
+apply (force intro!: exI program_equalityI)
+done
+
+lemma component_SKIP [iff]: "SKIP <= F"
+apply (unfold component_def)
+apply (force intro: Join_SKIP_left)
+done
+
+lemma component_refl [iff]: "F <= (F :: 'a program)"
+apply (unfold component_def)
+apply (blast intro: Join_SKIP_right)
+done
+
+lemma SKIP_minimal: "F <= SKIP ==> F = SKIP"
+by (auto intro!: program_equalityI simp add: component_eq_subset)
+
+lemma component_Join1: "F <= (F Join G)"
+by (unfold component_def, blast)
+
+lemma component_Join2: "G <= (F Join G)"
+apply (unfold component_def)
+apply (simp (no_asm) add: Join_commute)
+apply blast
+done
+
+lemma Join_absorb1: "F<=G ==> F Join G = G"
+by (auto simp add: component_def Join_left_absorb)
+
+lemma Join_absorb2: "G<=F ==> F Join G = F"
+by (auto simp add: Join_ac component_def)
+
+lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
+apply (simp (no_asm) add: component_eq_subset)
+apply blast
+done
+
+lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
+apply (unfold component_def)
+apply (blast intro: JN_absorb)
+done
+
+lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"
+apply (unfold component_def)
+apply (blast intro: Join_assoc [symmetric])
+done
+
+lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)"
+apply (simp (no_asm_use) add: component_eq_subset)
+apply (blast intro!: program_equalityI)
+done
+
+lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
+apply (simp (no_asm) add: component_eq_subset)
+apply blast
+done
+
+lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
+by (auto simp add: constrains_def component_eq_subset)
+
+(*Used in Guar.thy to show that programs are partially ordered*)
+lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
+
+
+(*** preserves ***)
+
+lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
+by (unfold preserves_def, blast)
+
+lemma preserves_imp_eq:
+ "[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'"
+apply (unfold preserves_def stable_def constrains_def, force)
+done
+
+lemma Join_preserves [iff]:
+ "(F Join G : preserves v) = (F : preserves v & G : preserves v)"
+apply (unfold preserves_def, auto)
+done
+
+lemma JN_preserves [iff]:
+ "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
+apply (simp (no_asm) add: JN_stable preserves_def)
+apply blast
+done
+
+lemma SKIP_preserves [iff]: "SKIP : preserves v"
+by (auto simp add: preserves_def)
+
+lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
+by (simp add: funPair_def)
+
+lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w"
+by (auto simp add: preserves_def stable_def constrains_def, blast)
+
+(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
+declare preserves_funPair [THEN eqset_imp_iff, iff]
+
+
+lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)"
+apply (simp (no_asm) add: funPair_def o_def)
+done
+
+lemma fst_o_funPair [simp]: "fst o (funPair f g) = f"
+apply (simp (no_asm) add: funPair_def o_def)
+done
+
+lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
+apply (simp (no_asm) add: funPair_def o_def)
+done
+
+lemma subset_preserves_o: "preserves v <= preserves (w o v)"
+by (force simp add: preserves_def stable_def constrains_def)
+
+lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}"
+apply (auto simp add: preserves_def stable_def constrains_def)
+apply (rename_tac s' s)
+apply (subgoal_tac "v s = v s'")
+apply (force+)
+done
+
+lemma preserves_subset_increasing: "preserves v <= increasing v"
+by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)
+
+lemma preserves_id_subset_stable: "preserves id <= stable A"
+by (force simp add: preserves_def stable_def constrains_def)
+
+
+(** For use with def_UNION_ok_iff **)
+
+lemma safety_prop_preserves [iff]: "safety_prop (preserves v)"
+by (auto intro: safety_prop_INTER1 simp add: preserves_def)
+
+
+(** Some lemmas used only in Client.ML **)
+
+lemma stable_localTo_stable2:
+ "[| F : stable {s. P (v s) (w s)};
+ G : preserves v; G : preserves w |]
+ ==> F Join G : stable {s. P (v s) (w s)}"
+apply (simp (no_asm_simp))
+apply (subgoal_tac "G: preserves (funPair v w) ")
+ prefer 2 apply simp
+apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
+done
+
+lemma Increasing_preserves_Stable:
+ "[| F : stable {s. v s <= w s}; G : preserves v;
+ F Join G : Increasing w |]
+ ==> F Join G : Stable {s. v s <= w s}"
+apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
+apply (blast intro: constrains_weaken)
+(*The G case remains*)
+apply (auto simp add: preserves_def stable_def constrains_def)
+apply (case_tac "act: Acts F", blast)
+(*We have a G-action, so delete assumptions about F-actions*)
+apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl)
+apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl)
+apply (subgoal_tac "v x = v xa")
+prefer 2 apply blast
+apply auto
+apply (erule order_trans, blast)
+done
+
+(** component_of **)
+
+(* component_of is stronger than <= *)
+lemma component_of_imp_component: "F component_of H ==> F <= H"
+by (unfold component_def component_of_def, blast)
+
+
+(* component_of satisfies many of the <='s properties *)
+lemma component_of_refl [simp]: "F component_of F"
+apply (unfold component_of_def)
+apply (rule_tac x = SKIP in exI, auto)
+done
+
+lemma component_of_SKIP [simp]: "SKIP component_of F"
+by (unfold component_of_def, auto)
+
+lemma component_of_trans:
+ "[| F component_of G; G component_of H |] ==> F component_of H"
+apply (unfold component_of_def)
+apply (blast intro: Join_assoc [symmetric])
+done
+
+lemmas strict_component_of_eq =
+ strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
+
+(** localize **)
+lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
+apply (unfold localize_def)
+apply (simp (no_asm))
+done
+
+lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
+apply (unfold localize_def)
+apply (simp (no_asm))
+done
+
+lemma localize_AllowedActs_eq [simp]:
+ "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
+apply (unfold localize_def, auto)
+done
+
end
--- a/src/HOL/UNITY/Comp/Counter.thy Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counter.thy Wed Jan 29 16:34:51 2003 +0100
@@ -11,7 +11,8 @@
Spriner LNCS 1586 (1999), pages 1215-1227.
*)
-Counter = Comp +
+Counter = UNITY_Main +
+
(* Variables are names *)
datatype name = C | c nat
types state = name=>int
--- a/src/HOL/UNITY/Comp/Counterc.thy Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.thy Wed Jan 29 16:34:51 2003 +0100
@@ -11,7 +11,8 @@
Spriner LNCS 1586 (1999), pages 1215-1227.
*)
-Counterc = Comp +
+Counterc = UNITY_Main +
+
types state
arities state :: type
--- a/src/HOL/UNITY/Guar.ML Wed Jan 29 16:29:38 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,520 +0,0 @@
-(* Title: HOL/UNITY/Guar.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Guarantees, etc.
-
-From Chandy and Sanders, "Reasoning About Program Composition"
-Revised by Sidi Ehmety on January 2001
-*)
-
-Goal "(OK (insert i I) F) = (if i:I then OK I F else OK I F & (F i ok JOIN I F))";
-by (auto_tac (claset() addIs [ok_sym],
- simpset() addsimps [OK_iff_ok]));
-qed "OK_insert_iff";
-
-
-
-(*** existential properties ***)
-Goalw [ex_prop_def]
- "[| ex_prop X; finite GG |] ==> \
-\ GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X";
-by (etac finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps [OK_insert_iff,Int_insert_left]));
-qed_spec_mp "ex1";
-
-
-Goalw [ex_prop_def]
- "ALL GG. finite GG & GG Int X ~= {} --> 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 (auto_tac (claset() addDs [ok_sym],
- simpset() addsimps [OK_iff_ok]));
-qed "ex2";
-
-
-(*Chandy & Sanders take this as a definition*)
-Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)";
-by (blast_tac (claset() addIs [ex1,ex2]) 1);
-qed "ex_prop_finite";
-
-
-(*Their "equivalent definition" given at the end of section 3*)
-Goal
- "ex_prop X = (ALL G. G:X = (ALL H. (G component_of H) --> H: X))";
-by Auto_tac;
-by (rewrite_goals_tac
- [ex_prop_def, component_of_def]);
-by Safe_tac;
-by (stac Join_commute 3);
-by (dtac ok_sym 3);
-by (REPEAT(Blast_tac 1));
-qed "ex_prop_equiv";
-
-
-(*** universal properties ***)
-Goalw [uv_prop_def]
- "[| uv_prop X; finite GG |] ==> \
-\ GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X";
-by (etac finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps
- [Int_insert_left, OK_insert_iff]));
-qed_spec_mp "uv1";
-
-Goalw [uv_prop_def]
- "ALL GG. finite GG & GG <= X & OK GG (%G. G)-->(JN G:GG. G):X ==> uv_prop X";
-by (rtac conjI 1);
-by (Clarify_tac 2);
-by (dres_inst_tac [("x", "{F,G}")] spec 2);
-by (dres_inst_tac [("x", "{}")] spec 1);
-by (auto_tac (claset() addDs [ok_sym], simpset() addsimps [OK_iff_ok]));
-qed "uv2";
-
-(*Chandy & Sanders take this as a definition*)
-Goal "uv_prop X = (ALL GG. finite GG & GG <= X & OK GG (%G. G)--> (JN G:GG. G): X)";
-by (blast_tac (claset() addIs [uv1,uv2]) 1);
-qed "uv_prop_finite";
-
-(*** guarantees ***)
-
-val prems = Goal
- "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) \
-\ ==> F : X guarantees Y";
-by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "guaranteesI";
-
-Goalw [guar_def, component_def]
- "[| F : X guarantees Y; F ok G; F Join G : X |] \
-\ ==> F Join G : Y";
-by (Blast_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 |] \
-\ ==> 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 (Blast_tac 1);
-qed "guarantees_weaken";
-
-Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
-by (Blast_tac 1);
-qed "subset_imp_guarantees_UNIV";
-
-(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
-by (Blast_tac 1);
-qed "subset_imp_guarantees";
-
-(*Remark at end of section 4.1 *)
-
-Goalw [guar_def] "ex_prop Y ==> (Y = UNIV guarantees Y)";
-by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
-by Safe_tac;
-by (dres_inst_tac [("x", "x")] spec 1);
-by (dres_inst_tac [("x", "x")] spec 2);
-by (dtac sym 2);
-by (ALLGOALS(etac iffE));
-by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
-by (REPEAT(Blast_tac 1));
-qed "ex_prop_imp";
-
-Goalw [guar_def] "(Y = UNIV guarantees Y) ==> ex_prop(Y)";
-by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
-by Safe_tac;
-by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
-by (dtac sym 2);
-by (ALLGOALS(etac equalityE));
-by (REPEAT(Blast_tac 1));
-qed "guarantees_imp";
-
-Goal "(ex_prop Y) = (Y = UNIV guarantees Y)";
-by (rtac iffI 1);
-by (rtac ex_prop_imp 1);
-by (rtac guarantees_imp 2);
-by (ALLGOALS(Asm_simp_tac));
-qed "ex_prop_equiv2";
-
-
-(** Distributive laws. Re-orient to perform miniscoping **)
-
-Goalw [guar_def]
- "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
-by (Blast_tac 1);
-qed "guarantees_UN_left";
-
-Goalw [guar_def]
- "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
-by (Blast_tac 1);
-qed "guarantees_Un_left";
-
-Goalw [guar_def]
- "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
-by (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 "(F : X guarantees (INTER I Y)) = \
-\ (ALL i:I. F : X guarantees (Y i))";
-by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
-qed "guarantees_INT_right_iff";
-
-Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
-by (Blast_tac 1);
-qed "shunting";
-
-Goalw [guar_def] "(X guarantees Y) = -Y guarantees -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) ==> 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 Ga = G Join (F Join Ga)" 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 Ga = G Join (F Join Ga)" 1);
-by (asm_full_simp_tac (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 |] \
-\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
-by Auto_tac;
-by (ball_tac 1);
-by (rename_tac "i" 1);
-by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 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) : (UNION I X) guarantees (UNION I Y)";
-by Auto_tac;
-by (ball_tac 1);
-by (rename_tac "i" 1);
-by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 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 (Clarify_tac 1);
-by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
-by (auto_tac (claset() addIs [OK_imp_ok],
- simpset() addsimps [JN_Join_diff, JN_Join_diff, Join_assoc RS sym]));
-qed "guarantees_JN_I";
-
-
-(*** well-definedness ***)
-
-Goalw [welldef_def] "F Join G: welldef ==> F: welldef";
-by Auto_tac;
-qed "Join_welldef_D1";
-
-Goalw [welldef_def] "F Join G: welldef ==> 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";
-
-(* Goalw [refines_def]
- "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X";
-by Auto_tac;
-qed "refines_trans"; *)
-
-
-
-Goalw [strict_ex_prop_def]
- "strict_ex_prop X \
-\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) \
-\ = (F:X --> G:X)";
-by Auto_tac;
-qed "strict_ex_refine_lemma";
-
-Goalw [strict_ex_prop_def]
- "strict_ex_prop X \
-\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
-\ (F: welldef Int X --> G:X)";
-by Safe_tac;
-by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
-by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
-qed "strict_ex_refine_lemma_v";
-
-Goal "[| strict_ex_prop X; \
-\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
-\ ==> (G refines F wrt X) = (G iso_refines F wrt X)";
-by (res_inst_tac [("x","SKIP")] allE 1
- THEN assume_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [refines_def, iso_refines_def,
- strict_ex_refine_lemma_v]) 1);
-qed "ex_refinement_thm";
-
-
-Goalw [strict_uv_prop_def]
- "strict_uv_prop X \
-\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
-by (Blast_tac 1);
-qed "strict_uv_refine_lemma";
-
-Goalw [strict_uv_prop_def]
- "strict_uv_prop X \
-\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
-\ (F: welldef Int X --> G:X)";
-by Safe_tac;
-by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
-by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2],
- simpset()));
-qed "strict_uv_refine_lemma_v";
-
-Goal "[| strict_uv_prop X; \
-\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
-\ ==> (G refines F wrt X) = (G iso_refines F wrt X)";
-by (res_inst_tac [("x","SKIP")] allE 1
- THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
- strict_uv_refine_lemma_v]) 1);
-qed "uv_refinement_thm";
-
-(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
-Goalw [guar_def, component_of_def]
-"(F:X guarantees Y) = (ALL H. H:X \\<longrightarrow> (F component_of H \\<longrightarrow> H:Y))";
-by Auto_tac;
-qed "guarantees_equiv";
-
-Goalw [wg_def] "!!X. F:(X guarantees Y) ==> X <= (wg F Y)";
-by Auto_tac;
-qed "wg_weakest";
-
-Goalw [wg_def, guar_def] "F:((wg F Y) guarantees Y)";
-by (Blast_tac 1);
-qed "wg_guarantees";
-
-Goalw [wg_def]
- "(H: wg F X) = (F component_of H --> H:X)";
-by (simp_tac (simpset() addsimps [guarantees_equiv]) 1);
-by (rtac iffI 1);
-by (res_inst_tac [("x", "{H}")] exI 2);
-by (REPEAT(Blast_tac 1));
-qed "wg_equiv";
-
-
-Goal
-"F component_of H ==> (H:wg F X) = (H:X)";
-by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1);
-qed "component_of_wg";
-
-
-Goal
-"ALL FF. finite FF & FF Int X ~= {} --> 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 (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [component_of_def]) 1);
-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";
-
-Goal "ex_prop X ==> (F:X) = (ALL H. H : wg F X)";
-by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1);
-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]
-"ex_prop (wx X)";
-by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
-by Safe_tac;
-by (Blast_tac 1);
-by Auto_tac;
-qed "wx_ex_prop";
-
-Goalw [wx_def]
-"ALL Z. Z<= X --> ex_prop Z --> Z <= wx X";
-by Auto_tac;
-qed "wx_weakest";
-
-
-(* Proposition 6 *)
-Goalw [ex_prop_def]
- "ex_prop({F. ALL G. F ok G --> F Join G:X})";
-by Safe_tac;
-by (dres_inst_tac [("x", "G Join Ga")] spec 1);
-by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1);
-by (dres_inst_tac [("x", "F Join Ga")] spec 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. ALL G. F ok G --> (F Join G):X}";
-by Safe_tac;
-by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
-by (dres_inst_tac [("x", "x")] spec 1);
-by (dres_inst_tac [("x", "G")] spec 1);
-by (forw_inst_tac [("c", "x Join G")] subsetD 1);
-by Safe_tac;
-by (Simp_tac 1);
-by (res_inst_tac [("x", "{F. ALL G. F ok G --> F Join G:X}")] exI 1);
-by Safe_tac;
-by (rtac wx'_ex_prop 2);
-by (rotate_tac 1 1);
-by (dres_inst_tac [("x", "SKIP")] spec 1);
-by Auto_tac;
-qed "wx_equiv";
-
-
-(* Propositions 7 to 11 are about this second definition of wx. And
- they are the same as the ones proved for the first definition of wx by equivalence *)
-
-(* Proposition 12 *)
-(* Main result of the paper *)
-Goalw [guar_def]
- "(X guarantees Y) = wx(-X Un Y)";
-by (simp_tac (simpset() addsimps [wx_equiv]) 1);
-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:(stable A) guarantees (Always A)";
-by (rtac guaranteesI 1);
-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])));
-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 ==> 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 2);
-by (Blast_tac 1);
-by (blast_tac (claset() addIs [Join_transient_I1]) 1);
-qed "constrains_guarantees_leadsTo";
-
-
-
-
-
-
-
--- a/src/HOL/UNITY/Guar.thy Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy Wed Jan 29 16:34:51 2003 +0100
@@ -18,36 +18,39 @@
*)
-Guar = Comp +
+theory Guar = Comp:
instance program :: (type) order
- (component_refl, component_trans, component_antisym,
- program_less_le)
+ by (intro_classes,
+ (assumption | rule component_refl component_trans component_antisym
+ program_less_le)+)
+
constdefs
(*Existential and Universal properties. I formalize the two-program
case, proving equivalence with Chandy and Sanders's n-ary definitions*)
- ex_prop :: 'a program set => bool
- "ex_prop X == ALL F G. F ok G -->F:X | G: X --> (F Join G) : X"
+ ex_prop :: "'a program set => bool"
+ "ex_prop X == \<forall>F G. F ok G -->F:X | G: X --> (F Join G) : X"
- strict_ex_prop :: 'a program set => bool
- "strict_ex_prop X == ALL F G. F ok G --> (F:X | G: X) = (F Join G : X)"
+ strict_ex_prop :: "'a program set => bool"
+ "strict_ex_prop X == \<forall>F G. F ok G --> (F:X | G: X) = (F Join G : X)"
- uv_prop :: 'a program set => bool
- "uv_prop X == SKIP : X & (ALL F G. F ok G --> F:X & G: X --> (F Join G) : X)"
+ uv_prop :: "'a program set => bool"
+ "uv_prop X == SKIP : X & (\<forall>F G. F ok G --> F:X & G: X --> (F Join G) : X)"
- strict_uv_prop :: 'a program set => bool
- "strict_uv_prop X == SKIP : X & (ALL F G. F ok G -->(F:X & G: X) = (F Join G : X))"
+ strict_uv_prop :: "'a program set => bool"
+ "strict_uv_prop X ==
+ SKIP : X & (\<forall>F G. F ok G --> (F:X & G: X) = (F Join G : X))"
- guar :: ['a program set, 'a program set] => 'a program set
+ guar :: "['a program set, 'a program set] => 'a program set"
(infixl "guarantees" 55) (*higher than membership, lower than Co*)
- "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}"
+ "X guarantees Y == {F. \<forall>G. F ok G --> F Join G : X --> F Join G : Y}"
(* Weakest guarantees *)
- wg :: ['a program, 'a program set] => 'a program set
+ wg :: "['a program, 'a program set] => 'a program set"
"wg F Y == Union({X. F:X guarantees Y})"
(* Weakest existential property stronger than X *)
@@ -55,17 +58,484 @@
"wx X == Union({Y. Y<=X & ex_prop Y})"
(*Ill-defined programs can arise through "Join"*)
- welldef :: 'a program set
+ welldef :: "'a program set"
"welldef == {F. Init F ~= {}}"
- refines :: ['a program, 'a program, 'a program set] => bool
+ refines :: "['a program, 'a program, 'a program set] => bool"
("(3_ refines _ wrt _)" [10,10,10] 10)
"G refines F wrt X ==
- ALL H. (F ok H & G ok H & F Join H:welldef Int X) --> (G Join H:welldef Int X)"
+ \<forall>H. (F ok H & G ok H & F Join H : welldef Int X) -->
+ (G Join H : welldef Int X)"
- iso_refines :: ['a program, 'a program, 'a program set] => bool
+ iso_refines :: "['a program, 'a program, 'a program set] => bool"
("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
"G iso_refines F wrt X ==
F : welldef Int X --> G : welldef Int X"
+
+lemma OK_insert_iff:
+ "(OK (insert i I) F) =
+ (if i:I then OK I F else OK I F & (F i ok JOIN I F))"
+by (auto intro: ok_sym simp add: OK_iff_ok)
+
+
+(*** existential properties ***)
+lemma ex1 [rule_format (no_asm)]:
+ "[| ex_prop X; finite GG |] ==>
+ GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
+apply (unfold ex_prop_def)
+apply (erule finite_induct)
+apply (auto simp add: OK_insert_iff Int_insert_left)
+done
+
+
+lemma ex2:
+ "\<forall>GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X
+ ==> ex_prop X"
+apply (unfold ex_prop_def, clarify)
+apply (drule_tac x = "{F,G}" in spec)
+apply (auto dest: ok_sym simp add: OK_iff_ok)
+done
+
+
+(*Chandy & Sanders take this as a definition*)
+lemma ex_prop_finite:
+ "ex_prop X =
+ (\<forall>GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"
+by (blast intro: ex1 ex2)
+
+
+(*Their "equivalent definition" given at the end of section 3*)
+lemma ex_prop_equiv:
+ "ex_prop X = (\<forall>G. G:X = (\<forall>H. (G component_of H) --> H: X))"
+apply auto
+apply (unfold ex_prop_def component_of_def, safe)
+apply blast
+apply blast
+apply (subst Join_commute)
+apply (drule ok_sym, blast)
+done
+
+
+(*** universal properties ***)
+lemma uv1 [rule_format]:
+ "[| uv_prop X; finite GG |]
+ ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"
+apply (unfold uv_prop_def)
+apply (erule finite_induct)
+apply (auto simp add: Int_insert_left OK_insert_iff)
+done
+
+lemma uv2:
+ "\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X
+ ==> uv_prop X"
+apply (unfold uv_prop_def)
+apply (rule conjI)
+ apply (drule_tac x = "{}" in spec)
+ prefer 2
+ apply clarify
+ apply (drule_tac x = "{F,G}" in spec)
+apply (auto dest: ok_sym simp add: OK_iff_ok)
+done
+
+(*Chandy & Sanders take this as a definition*)
+lemma uv_prop_finite:
+ "uv_prop X =
+ (\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)"
+by (blast intro: uv1 uv2)
+
+(*** guarantees ***)
+
+lemma guaranteesI:
+ "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y)
+ ==> F : X guarantees Y"
+by (simp add: guar_def component_def)
+
+lemma guaranteesD:
+ "[| F : X guarantees Y; F ok G; F Join G : X |]
+ ==> F Join G : Y"
+by (unfold guar_def component_def, blast)
+
+(*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*)
+lemma component_guaranteesD:
+ "[| F : X guarantees Y; F Join G = H; H : X; F ok G |]
+ ==> H : Y"
+by (unfold guar_def, blast)
+
+lemma guarantees_weaken:
+ "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"
+by (unfold guar_def, blast)
+
+lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV"
+by (unfold guar_def, blast)
+
+(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
+lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y"
+by (unfold guar_def, blast)
+
+(*Remark at end of section 4.1 *)
+
+lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)"
+apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
+apply safe
+ apply (drule_tac x = x in spec)
+ apply (drule_tac [2] x = x in spec)
+ apply (drule_tac [2] sym)
+apply (auto simp add: component_of_def)
+done
+
+lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
+apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
+apply safe
+apply (auto simp add: component_of_def dest: sym)
+done
+
+lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)"
+apply (rule iffI)
+apply (rule ex_prop_imp)
+apply (auto simp add: guarantees_imp)
+done
+
+
+(** Distributive laws. Re-orient to perform miniscoping **)
+
+lemma guarantees_UN_left:
+ "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"
+by (unfold guar_def, blast)
+
+lemma guarantees_Un_left:
+ "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
+by (unfold guar_def, blast)
+
+lemma guarantees_INT_right:
+ "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"
+by (unfold guar_def, blast)
+
+lemma guarantees_Int_right:
+ "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
+by (unfold guar_def, blast)
+
+lemma guarantees_Int_right_I:
+ "[| F : Z guarantees X; F : Z guarantees Y |]
+ ==> F : Z guarantees (X Int Y)"
+by (simp add: guarantees_Int_right)
+
+lemma guarantees_INT_right_iff:
+ "(F : X guarantees (INTER I Y)) = (\<forall>i\<in>I. F : X guarantees (Y i))"
+by (simp add: guarantees_INT_right)
+
+lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))"
+by (unfold guar_def, blast)
+
+lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
+by (unfold guar_def, blast)
+
+(** The following two can be expressed using intersection and subset, which
+ is more faithful to the text but looks cryptic.
+**)
+
+lemma combining1:
+ "[| F : V guarantees X; F : (X Int Y) guarantees Z |]
+ ==> F : (V Int Y) guarantees Z"
+
+by (unfold guar_def, blast)
+
+lemma combining2:
+ "[| F : V guarantees (X Un Y); F : Y guarantees Z |]
+ ==> F : V guarantees (X Un Z)"
+by (unfold guar_def, blast)
+
+(** 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) *)
+lemma all_guarantees:
+ "\<forall>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"
+by (unfold guar_def, blast)
+
+(*Premises should be [| F: X guarantees Y i; i: I |] *)
+lemma ex_guarantees:
+ "\<exists>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"
+by (unfold guar_def, blast)
+
+
+(*** Additional guarantees laws, by lcp ***)
+
+lemma guarantees_Join_Int:
+ "[| F: U guarantees V; G: X guarantees Y; F ok G |]
+ ==> F Join G: (U Int X) guarantees (V Int Y)"
+apply (unfold guar_def)
+apply (simp (no_asm))
+apply safe
+apply (simp add: Join_assoc)
+apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (simp add: ok_commute)
+apply (simp (no_asm_simp) add: Join_ac)
+done
+
+lemma guarantees_Join_Un:
+ "[| F: U guarantees V; G: X guarantees Y; F ok G |]
+ ==> F Join G: (U Un X) guarantees (V Un Y)"
+apply (unfold guar_def)
+apply (simp (no_asm))
+apply safe
+apply (simp add: Join_assoc)
+apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (simp add: ok_commute)
+apply (simp (no_asm_simp) add: Join_ac)
+done
+
+lemma guarantees_JN_INT:
+ "[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |]
+ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"
+apply (unfold guar_def, auto)
+apply (drule bspec, assumption)
+apply (rename_tac "i")
+apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (auto intro: OK_imp_ok
+ simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
+done
+
+lemma guarantees_JN_UN:
+ "[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |]
+ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"
+apply (unfold guar_def, auto)
+apply (drule bspec, assumption)
+apply (rename_tac "i")
+apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (auto intro: OK_imp_ok
+ simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
+done
+
+
+(*** guarantees laws for breaking down the program, by lcp ***)
+
+lemma guarantees_Join_I1:
+ "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"
+apply (unfold guar_def)
+apply (simp (no_asm))
+apply safe
+apply (simp add: Join_assoc)
+done
+
+lemma guarantees_Join_I2:
+ "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"
+apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
+apply (blast intro: guarantees_Join_I1)
+done
+
+lemma guarantees_JN_I:
+ "[| i : I; F i: X guarantees Y; OK I F |]
+ ==> (JN i:I. (F i)) : X guarantees Y"
+apply (unfold guar_def, clarify)
+apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
+done
+
+
+(*** well-definedness ***)
+
+lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef"
+by (unfold welldef_def, auto)
+
+lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef"
+by (unfold welldef_def, auto)
+
+(*** refinement ***)
+
+lemma refines_refl: "F refines F wrt X"
+by (unfold refines_def, blast)
+
+
+(* Goalw [refines_def]
+ "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"
+by Auto_tac
+qed "refines_trans"; *)
+
+
+
+lemma strict_ex_refine_lemma:
+ "strict_ex_prop X
+ ==> (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X)
+ = (F:X --> G:X)"
+by (unfold strict_ex_prop_def, auto)
+
+lemma strict_ex_refine_lemma_v:
+ "strict_ex_prop X
+ ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =
+ (F: welldef Int X --> G:X)"
+apply (unfold strict_ex_prop_def, safe)
+apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
+apply (auto dest: Join_welldef_D1 Join_welldef_D2)
+done
+
+lemma ex_refinement_thm:
+ "[| strict_ex_prop X;
+ \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |]
+ ==> (G refines F wrt X) = (G iso_refines F wrt X)"
+apply (rule_tac x = SKIP in allE, assumption)
+apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
+done
+
+
+lemma strict_uv_refine_lemma:
+ "strict_uv_prop X ==>
+ (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)"
+by (unfold strict_uv_prop_def, blast)
+
+lemma strict_uv_refine_lemma_v:
+ "strict_uv_prop X
+ ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =
+ (F: welldef Int X --> G:X)"
+apply (unfold strict_uv_prop_def, safe)
+apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
+apply (auto dest: Join_welldef_D1 Join_welldef_D2)
+done
+
+lemma uv_refinement_thm:
+ "[| strict_uv_prop X;
+ \<forall>H. F ok H & G ok H & F Join H : welldef Int X -->
+ G Join H : welldef |]
+ ==> (G refines F wrt X) = (G iso_refines F wrt X)"
+apply (rule_tac x = SKIP in allE, assumption)
+apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
+done
+
+(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
+lemma guarantees_equiv:
+ "(F:X guarantees Y) = (\<forall>H. H:X \<longrightarrow> (F component_of H \<longrightarrow> H:Y))"
+by (unfold guar_def component_of_def, auto)
+
+lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"
+by (unfold wg_def, auto)
+
+lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
+by (unfold wg_def guar_def, blast)
+
+lemma wg_equiv:
+ "(H: wg F X) = (F component_of H --> H:X)"
+apply (unfold wg_def)
+apply (simp (no_asm) add: guarantees_equiv)
+apply (rule iffI)
+apply (rule_tac [2] x = "{H}" in exI)
+apply (blast+)
+done
+
+
+lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)"
+by (simp add: wg_equiv)
+
+lemma wg_finite:
+ "\<forall>FF. finite FF & FF Int X ~= {} --> OK FF (%F. F)
+ --> (\<forall>F\<in>FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"
+apply clarify
+apply (subgoal_tac "F component_of (JN F:FF. F) ")
+apply (drule_tac X = X in component_of_wg, simp)
+apply (simp add: component_of_def)
+apply (rule_tac x = "JN F: (FF-{F}) . F" in exI)
+apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
+done
+
+lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\<forall>H. H : wg F X)"
+apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
+apply blast
+done
+
+(** From Charpentier and Chandy "Theorems About Composition" **)
+(* Proposition 2 *)
+lemma wx_subset: "(wx X)<=X"
+by (unfold wx_def, auto)
+
+lemma wx_ex_prop: "ex_prop (wx X)"
+apply (unfold wx_def)
+apply (simp (no_asm) add: ex_prop_equiv)
+apply safe
+apply blast
+apply auto
+done
+
+lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z <= wx X"
+by (unfold wx_def, auto)
+
+(* Proposition 6 *)
+lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G:X})"
+apply (unfold ex_prop_def, safe)
+apply (drule_tac x = "G Join Ga" in spec)
+apply (force simp add: ok_Join_iff1 Join_assoc)
+apply (drule_tac x = "F Join Ga" in spec)
+apply (simp (no_asm_use) add: ok_Join_iff1)
+apply safe
+apply (simp (no_asm_simp) add: ok_commute)
+apply (subgoal_tac "F Join G = G Join F")
+apply (simp (no_asm_simp) add: Join_assoc)
+apply (simp (no_asm) add: Join_commute)
+done
+
+(* Equivalence with the other definition of wx *)
+
+lemma wx_equiv:
+ "wx X = {F. \<forall>G. F ok G --> (F Join G):X}"
+
+apply (unfold wx_def, safe)
+apply (simp (no_asm_use) add: ex_prop_def)
+apply (drule_tac x = x in spec)
+apply (drule_tac x = G in spec)
+apply (frule_tac c = "x Join G" in subsetD, safe)
+apply (simp (no_asm))
+apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G:X}" in exI, safe)
+apply (rule_tac [2] wx'_ex_prop)
+apply (rotate_tac 1)
+apply (drule_tac x = SKIP in spec, auto)
+done
+
+
+(* Propositions 7 to 11 are about this second definition of wx. And
+ they are the same as the ones proved for the first definition of wx by equivalence *)
+
+(* Proposition 12 *)
+(* Main result of the paper *)
+lemma guarantees_wx_eq:
+ "(X guarantees Y) = wx(-X Un Y)"
+apply (unfold guar_def)
+apply (simp (no_asm) add: wx_equiv)
+done
+
+(* {* 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 *)
+
+lemma stable_guarantees_Always:
+ "Init F <= A ==> F:(stable A) guarantees (Always A)"
+apply (rule guaranteesI)
+apply (simp (no_asm) add: Join_commute)
+apply (rule stable_Join_Always1)
+apply (simp_all add: invariant_def Join_stable)
+done
+
+(* To be moved to WFair.ML *)
+lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"
+apply (drule_tac B = "A-B" in constrains_weaken_L)
+apply (drule_tac [2] B = "A-B" in transient_strengthen)
+apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
+apply (blast+)
+done
+
+
+
+lemma constrains_guarantees_leadsTo:
+ "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
+apply (rule guaranteesI)
+apply (rule leadsTo_Basis')
+apply (drule constrains_weaken_R)
+prefer 2 apply assumption
+apply blast
+apply (blast intro: Join_transient_I1)
+done
+
end
--- a/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 16:34:51 2003 +0100
@@ -6,6 +6,193 @@
Specialized UNITY tactics, and ML bindings of theorems
*)
+(*Union*)
+val Init_SKIP = thm "Init_SKIP";
+val Acts_SKIP = thm "Acts_SKIP";
+val AllowedActs_SKIP = thm "AllowedActs_SKIP";
+val reachable_SKIP = thm "reachable_SKIP";
+val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff";
+val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff";
+val SKIP_in_stable = thm "SKIP_in_stable";
+val Init_Join = thm "Init_Join";
+val Acts_Join = thm "Acts_Join";
+val AllowedActs_Join = thm "AllowedActs_Join";
+val JN_empty = thm "JN_empty";
+val JN_insert = thm "JN_insert";
+val Init_JN = thm "Init_JN";
+val Acts_JN = thm "Acts_JN";
+val AllowedActs_JN = thm "AllowedActs_JN";
+val JN_cong = thm "JN_cong";
+val Join_commute = thm "Join_commute";
+val Join_assoc = thm "Join_assoc";
+val Join_left_commute = thm "Join_left_commute";
+val Join_SKIP_left = thm "Join_SKIP_left";
+val Join_SKIP_right = thm "Join_SKIP_right";
+val Join_absorb = thm "Join_absorb";
+val Join_left_absorb = thm "Join_left_absorb";
+val Join_ac = thms "Join_ac";
+val JN_absorb = thm "JN_absorb";
+val JN_Un = thm "JN_Un";
+val JN_constant = thm "JN_constant";
+val JN_Join_distrib = thm "JN_Join_distrib";
+val JN_Join_miniscope = thm "JN_Join_miniscope";
+val JN_Join_diff = thm "JN_Join_diff";
+val JN_constrains = thm "JN_constrains";
+val Join_constrains = thm "Join_constrains";
+val Join_unless = thm "Join_unless";
+val Join_constrains_weaken = thm "Join_constrains_weaken";
+val JN_constrains_weaken = thm "JN_constrains_weaken";
+val JN_stable = thm "JN_stable";
+val invariant_JN_I = thm "invariant_JN_I";
+val Join_stable = thm "Join_stable";
+val Join_increasing = thm "Join_increasing";
+val invariant_JoinI = thm "invariant_JoinI";
+val FP_JN = thm "FP_JN";
+val JN_transient = thm "JN_transient";
+val Join_transient = thm "Join_transient";
+val Join_transient_I1 = thm "Join_transient_I1";
+val Join_transient_I2 = thm "Join_transient_I2";
+val JN_ensures = thm "JN_ensures";
+val Join_ensures = thm "Join_ensures";
+val stable_Join_constrains = thm "stable_Join_constrains";
+val stable_Join_Always1 = thm "stable_Join_Always1";
+val stable_Join_Always2 = thm "stable_Join_Always2";
+val stable_Join_ensures1 = thm "stable_Join_ensures1";
+val stable_Join_ensures2 = thm "stable_Join_ensures2";
+val ok_SKIP1 = thm "ok_SKIP1";
+val ok_SKIP2 = thm "ok_SKIP2";
+val ok_Join_commute = thm "ok_Join_commute";
+val ok_commute = thm "ok_commute";
+val ok_sym = thm "ok_sym";
+val ok_iff_OK = thm "ok_iff_OK";
+val ok_Join_iff1 = thm "ok_Join_iff1";
+val ok_Join_iff2 = thm "ok_Join_iff2";
+val ok_Join_commute_I = thm "ok_Join_commute_I";
+val ok_JN_iff1 = thm "ok_JN_iff1";
+val ok_JN_iff2 = thm "ok_JN_iff2";
+val OK_iff_ok = thm "OK_iff_ok";
+val OK_imp_ok = thm "OK_imp_ok";
+val Allowed_SKIP = thm "Allowed_SKIP";
+val Allowed_Join = thm "Allowed_Join";
+val Allowed_JN = thm "Allowed_JN";
+val ok_iff_Allowed = thm "ok_iff_Allowed";
+val OK_iff_Allowed = thm "OK_iff_Allowed";
+val safety_prop_Acts_iff = thm "safety_prop_Acts_iff";
+val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
+val Allowed_eq = thm "Allowed_eq";
+val def_prg_Allowed = thm "def_prg_Allowed";
+val safety_prop_constrains = thm "safety_prop_constrains";
+val safety_prop_stable = thm "safety_prop_stable";
+val safety_prop_Int = thm "safety_prop_Int";
+val safety_prop_INTER1 = thm "safety_prop_INTER1";
+val safety_prop_INTER = thm "safety_prop_INTER";
+val def_UNION_ok_iff = thm "def_UNION_ok_iff";
+
+(*Comp*)
+val preserves_def = thm "preserves_def";
+val funPair_def = thm "funPair_def";
+val componentI = thm "componentI";
+val component_eq_subset = thm "component_eq_subset";
+val component_SKIP = thm "component_SKIP";
+val component_refl = thm "component_refl";
+val SKIP_minimal = thm "SKIP_minimal";
+val component_Join1 = thm "component_Join1";
+val component_Join2 = thm "component_Join2";
+val Join_absorb1 = thm "Join_absorb1";
+val Join_absorb2 = thm "Join_absorb2";
+val JN_component_iff = thm "JN_component_iff";
+val component_JN = thm "component_JN";
+val component_trans = thm "component_trans";
+val component_antisym = thm "component_antisym";
+val Join_component_iff = thm "Join_component_iff";
+val component_constrains = thm "component_constrains";
+val program_less_le = thm "program_less_le";
+val preservesI = thm "preservesI";
+val preserves_imp_eq = thm "preserves_imp_eq";
+val Join_preserves = thm "Join_preserves";
+val JN_preserves = thm "JN_preserves";
+val SKIP_preserves = thm "SKIP_preserves";
+val funPair_apply = thm "funPair_apply";
+val preserves_funPair = thm "preserves_funPair";
+val funPair_o_distrib = thm "funPair_o_distrib";
+val fst_o_funPair = thm "fst_o_funPair";
+val snd_o_funPair = thm "snd_o_funPair";
+val subset_preserves_o = thm "subset_preserves_o";
+val preserves_subset_stable = thm "preserves_subset_stable";
+val preserves_subset_increasing = thm "preserves_subset_increasing";
+val preserves_id_subset_stable = thm "preserves_id_subset_stable";
+val safety_prop_preserves = thm "safety_prop_preserves";
+val stable_localTo_stable2 = thm "stable_localTo_stable2";
+val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
+val component_of_imp_component = thm "component_of_imp_component";
+val component_of_refl = thm "component_of_refl";
+val component_of_SKIP = thm "component_of_SKIP";
+val component_of_trans = thm "component_of_trans";
+val strict_component_of_eq = thm "strict_component_of_eq";
+val localize_Init_eq = thm "localize_Init_eq";
+val localize_Acts_eq = thm "localize_Acts_eq";
+val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
+
+(*Guar*)
+val guar_def = thm "guar_def";
+val OK_insert_iff = thm "OK_insert_iff";
+val ex1 = thm "ex1";
+val ex2 = thm "ex2";
+val ex_prop_finite = thm "ex_prop_finite";
+val ex_prop_equiv = thm "ex_prop_equiv";
+val uv1 = thm "uv1";
+val uv2 = thm "uv2";
+val uv_prop_finite = thm "uv_prop_finite";
+val guaranteesI = thm "guaranteesI";
+val guaranteesD = thm "guaranteesD";
+val component_guaranteesD = thm "component_guaranteesD";
+val guarantees_weaken = thm "guarantees_weaken";
+val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV";
+val subset_imp_guarantees = thm "subset_imp_guarantees";
+val ex_prop_imp = thm "ex_prop_imp";
+val guarantees_imp = thm "guarantees_imp";
+val ex_prop_equiv2 = thm "ex_prop_equiv2";
+val guarantees_UN_left = thm "guarantees_UN_left";
+val guarantees_Un_left = thm "guarantees_Un_left";
+val guarantees_INT_right = thm "guarantees_INT_right";
+val guarantees_Int_right = thm "guarantees_Int_right";
+val guarantees_Int_right_I = thm "guarantees_Int_right_I";
+val guarantees_INT_right_iff = thm "guarantees_INT_right_iff";
+val shunting = thm "shunting";
+val contrapositive = thm "contrapositive";
+val combining1 = thm "combining1";
+val combining2 = thm "combining2";
+val all_guarantees = thm "all_guarantees";
+val ex_guarantees = thm "ex_guarantees";
+val guarantees_Join_Int = thm "guarantees_Join_Int";
+val guarantees_Join_Un = thm "guarantees_Join_Un";
+val guarantees_JN_INT = thm "guarantees_JN_INT";
+val guarantees_JN_UN = thm "guarantees_JN_UN";
+val guarantees_Join_I1 = thm "guarantees_Join_I1";
+val guarantees_Join_I2 = thm "guarantees_Join_I2";
+val guarantees_JN_I = thm "guarantees_JN_I";
+val Join_welldef_D1 = thm "Join_welldef_D1";
+val Join_welldef_D2 = thm "Join_welldef_D2";
+val refines_refl = thm "refines_refl";
+val ex_refinement_thm = thm "ex_refinement_thm";
+val uv_refinement_thm = thm "uv_refinement_thm";
+val guarantees_equiv = thm "guarantees_equiv";
+val wg_weakest = thm "wg_weakest";
+val wg_guarantees = thm "wg_guarantees";
+val wg_equiv = thm "wg_equiv";
+val component_of_wg = thm "component_of_wg";
+val wg_finite = thm "wg_finite";
+val wg_ex_prop = thm "wg_ex_prop";
+val wx_subset = thm "wx_subset";
+val wx_ex_prop = thm "wx_ex_prop";
+val wx_weakest = thm "wx_weakest";
+val wx'_ex_prop = thm "wx'_ex_prop";
+val wx_equiv = thm "wx_equiv";
+val guarantees_wx_eq = thm "guarantees_wx_eq";
+val stable_guarantees_Always = thm "stable_guarantees_Always";
+val leadsTo_Basis = thm "leadsTo_Basis";
+val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo";
+
(*Extend*)
val Restrict_iff = thm "Restrict_iff";
val Restrict_UNIV = thm "Restrict_UNIV";
--- a/src/HOL/UNITY/Union.ML Wed Jan 29 16:29:38 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,471 +0,0 @@
-(* Title: HOL/UNITY/Union.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Unions of programs
-
-From Misra's Chapter 5: Asynchronous Compositions of Programs
-*)
-
-
-(** SKIP **)
-
-Goal "Init SKIP = UNIV";
-by (simp_tac (simpset() addsimps [SKIP_def]) 1);
-qed "Init_SKIP";
-
-Goal "Acts SKIP = {Id}";
-by (simp_tac (simpset() addsimps [SKIP_def]) 1);
-qed "Acts_SKIP";
-
-Goal "AllowedActs SKIP = UNIV";
-by (auto_tac (claset(), simpset() addsimps [SKIP_def]));
-qed "AllowedActs_SKIP";
-
-Addsimps [Init_SKIP, Acts_SKIP, AllowedActs_SKIP];
-
-Goal "reachable SKIP = UNIV";
-by (force_tac (claset() addEs [reachable.induct]
- addIs reachable.intrs, simpset()) 1);
-qed "reachable_SKIP";
-
-Addsimps [reachable_SKIP];
-
-(** SKIP and safety properties **)
-
-Goalw [constrains_def] "(SKIP : A co B) = (A<=B)";
-by Auto_tac;
-qed "SKIP_in_constrains_iff";
-AddIffs [SKIP_in_constrains_iff];
-
-Goalw [Constrains_def] "(SKIP : A Co B) = (A<=B)";
-by Auto_tac;
-qed "SKIP_in_Constrains_iff";
-AddIffs [SKIP_in_Constrains_iff];
-
-Goalw [stable_def] "SKIP : stable A";
-by Auto_tac;
-qed "SKIP_in_stable";
-AddIffs [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable];
-
-
-(** Join **)
-
-Goal "Init (F Join G) = Init F Int Init G";
-by (simp_tac (simpset() addsimps [Join_def]) 1);
-qed "Init_Join";
-
-Goal "Acts (F Join G) = Acts F Un Acts G";
-by (auto_tac (claset(), simpset() addsimps [Join_def]));
-qed "Acts_Join";
-
-Goal "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G";
-by (auto_tac (claset(), simpset() addsimps [Join_def]));
-qed "AllowedActs_Join";
-
-Addsimps [Init_Join, Acts_Join, AllowedActs_Join];
-
-
-(** JN **)
-
-Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP";
-by Auto_tac;
-qed "JN_empty";
-Addsimps [JN_empty];
-
-Goal "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)";
-by (rtac program_equalityI 1);
-by (auto_tac (claset(), simpset() addsimps [JOIN_def, Join_def]));
-qed "JN_insert";
-Addsimps[JN_empty, JN_insert];
-
-Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))";
-by (simp_tac (simpset() addsimps [JOIN_def]) 1);
-qed "Init_JN";
-
-Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))";
-by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
-qed "Acts_JN";
-
-Goal "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))";
-by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
-qed "AllowedActs_JN";
-
-Addsimps [Init_JN, Acts_JN, AllowedActs_JN];
-
-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];
-
-
-(** 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 "(F Join G) Join H = F Join (G Join H)";
-by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1);
-qed "Join_assoc";
-
-Goal "A Join (B Join C) = B Join (A Join C)";
-by(rtac ([Join_assoc,Join_commute] MRS
- read_instantiate[("f","op Join")](thm"mk_left_commute")) 1);
-qed "Join_left_commute";
-
-
-Goalw [Join_def, SKIP_def] "SKIP Join F = F";
-by (rtac program_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
-qed "Join_SKIP_left";
-
-Goalw [Join_def, SKIP_def] "F Join SKIP = F";
-by (rtac program_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
-qed "Join_SKIP_right";
-
-Addsimps [Join_SKIP_left, Join_SKIP_right];
-
-Goalw [Join_def] "F Join F = F";
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "Join_absorb";
-
-Addsimps [Join_absorb];
-
-Goalw [Join_def] "F Join (F Join G) = F Join G";
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "Join_left_absorb";
-
-(*Join is an AC-operator*)
-val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute];
-
-
-(*** JN laws ***)
-
-(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
-Goal "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)";
-by (auto_tac (claset() addSIs [program_equalityI], simpset()));
-qed "JN_absorb";
-
-Goal "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))";
-by (auto_tac (claset() addSIs [program_equalityI], simpset()));
-qed "JN_Un";
-
-Goal "(JN i:I. c) = (if I={} then SKIP else 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 (auto_tac (claset() addSIs [program_equalityI], simpset()));
-qed "JN_Join_distrib";
-
-Goal "i : I ==> (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);
-by Auto_tac;
-qed "JN_Join_miniscope";
-
-(*Used to prove guarantees_JN_I*)
-Goalw [JOIN_def, Join_def] "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={} 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. F i : A co B)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "JN_constrains";
-
-Goal "(F Join G : A co B) = (F : A co B & G : A co B)";
-by (auto_tac
- (claset(),
- simpset() addsimps [constrains_def, Join_def]));
-qed "Join_constrains";
-
-Goal "(F Join G : A unless B) = (F : A unless B & G : A unless B)";
-by (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 (Simp_tac 1);
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "Join_constrains_weaken";
-
-(*If I={}, it degenerates to SKIP : UNIV co {}, 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 (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "JN_constrains_weaken";
-
-Goal "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
-by (asm_simp_tac
- (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
-qed "JN_stable";
-
-Goal "[| ALL i:I. F i : invariant A; i : I |] \
-\ ==> (JN i:I. F i) : invariant A";
-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) = \
-\ (F : stable A & G : stable A)";
-by (simp_tac (simpset() addsimps [stable_def]) 1);
-qed "Join_stable";
-
-Goal "(F Join G : increasing f) = \
-\ (F : increasing f & G : increasing f)";
-by (simp_tac (simpset() addsimps [increasing_def, Join_stable]) 1);
-by (Blast_tac 1);
-qed "Join_increasing";
-
-Addsimps [Join_stable, Join_increasing];
-
-Goal "[| F : invariant A; G : invariant A |] \
-\ ==> F Join G : invariant A";
-by (full_simp_tac (simpset() addsimps [invariant_def]) 1);
-by (Blast_tac 1);
-qed "invariant_JoinI";
-
-Goal "FP (JN i:I. F i) = (INT i:I. FP (F i))";
-by (asm_simp_tac (simpset() addsimps [FP_def, JN_stable, INTER_def]) 1);
-qed "FP_JN";
-
-
-(*** Progress: transient, ensures ***)
-
-Goal "i : I ==> \
-\ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
-by (auto_tac (claset(),
- simpset() addsimps [transient_def, JOIN_def]));
-qed "JN_transient";
-
-Goal "F Join G : transient A = \
-\ (F : transient A | G : transient A)";
-by (auto_tac (claset(),
- simpset() addsimps [bex_Un, transient_def,
- Join_def]));
-qed "Join_transient";
-
-Addsimps [Join_transient];
-
-Goal "F : transient A ==> F Join G : transient A";
-by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
-qed "Join_transient_I1";
-
-Goal "G : transient A ==> F Join G : transient A";
-by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
-qed "Join_transient_I2";
-
-(*If I={} 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. F i : (A-B) co (A Un B)) & (EX i:I. 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 = \
-\ (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & \
-\ (F : transient (A-B) | 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 (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
-by (Blast_tac 1);
-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 (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 (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(), simpset() addsimps [ok_def]));
-qed "ok_SKIP1";
-
-Goal "F ok SKIP";
-by (auto_tac (claset(), 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::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
-by (asm_full_simp_tac
- (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def,
- OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);
-by (Blast_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]));
-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]));
-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 = UNIV";
-by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
-qed "Allowed_SKIP";
-
-Goal "Allowed (F Join G) = Allowed F Int Allowed G";
-by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
-qed "Allowed_Join";
-
-Goal "Allowed (JOIN I F) = (INT i:I. Allowed (F i))";
-by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
-qed "Allowed_JN";
-
-Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
-
-Goal "F ok G = (F : Allowed G & G : Allowed F)";
-by (simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
-qed "ok_iff_Allowed";
-
-Goal "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(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 <= insert Id (UNION X Acts)) = (G : X)";
-by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
-qed "safety_prop_Acts_iff";
-
-Goal "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)";
-by (auto_tac (claset(),
- simpset() addsimps [Allowed_def, safety_prop_Acts_iff RS sym]));
-qed "safety_prop_AllowedActs_iff_Allowed";
-
-Goal "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X";
-by (asm_simp_tac (simpset() addsimps [Allowed_def, safety_prop_Acts_iff]) 1);
-qed "Allowed_eq";
-
-Goal "[| F == mk_program (init, acts, UNION X Acts) ; 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 "safety_prop (A co B) = (A <= B)";
-by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1);
-by (Blast_tac 1);
-qed "safety_prop_constrains";
-AddIffs [safety_prop_constrains];
-
-Goal "safety_prop (stable A)";
-by (simp_tac (simpset() addsimps [stable_def]) 1);
-qed "safety_prop_stable";
-AddIffs [safety_prop_stable];
-
-Goal "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)";
-by (full_simp_tac (simpset() addsimps [safety_prop_def]) 1);
-by (Blast_tac 1);
-qed "safety_prop_Int";
-Addsimps [safety_prop_Int];
-
-Goal "(ALL i. safety_prop (X i)) ==> safety_prop (INT i. X i)";
-by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
-by (Blast_tac 1);
-bind_thm ("safety_prop_INTER1", allI RS result());
-Addsimps [safety_prop_INTER1];
-
-Goal "(ALL i:I. safety_prop (X i)) ==> safety_prop (INT i:I. X i)";
-by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
-by (Blast_tac 1);
-bind_thm ("safety_prop_INTER", ballI RS result());
-Addsimps [safety_prop_INTER];
-
-Goal "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] \
-\ ==> F ok G = (G : X & acts <= AllowedActs G)";
-by (auto_tac (claset(), simpset() addsimps [ok_def, safety_prop_Acts_iff]));
-qed "def_UNION_ok_iff";
--- a/src/HOL/UNITY/Union.thy Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/UNITY/Union.thy Wed Jan 29 16:34:51 2003 +0100
@@ -8,28 +8,28 @@
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
*)
-Union = SubstAx + FP +
+theory Union = SubstAx + FP:
constdefs
(*FIXME: conjoin Init F Int Init G ~= {} *)
- ok :: ['a program, 'a program] => bool (infixl 65)
+ ok :: "['a program, 'a program] => bool" (infixl "ok" 65)
"F ok G == Acts F <= AllowedActs G &
Acts G <= AllowedActs F"
(*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *)
- OK :: ['a set, 'a => 'b program] => bool
+ OK :: "['a set, 'a => 'b program] => bool"
"OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
- JOIN :: ['a set, 'a => 'b program] => 'b program
+ JOIN :: "['a set, 'a => 'b program] => 'b program"
"JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
INT i:I. AllowedActs (F i))"
- Join :: ['a program, 'a program] => 'a program (infixl 65)
+ Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65)
"F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
AllowedActs F Int AllowedActs G)"
- SKIP :: 'a program
+ SKIP :: "'a program"
"SKIP == mk_program (UNIV, {}, UNIV)"
(*Characterizes safety properties. Used with specifying AllowedActs*)
@@ -37,8 +37,8 @@
"safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
syntax
- "@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10)
- "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)
+ "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
+ "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
translations
"JN x:A. B" == "JOIN A (%x. B)"
@@ -46,9 +46,375 @@
"JN x. B" == "JOIN UNIV (%x. B)"
syntax (xsymbols)
- SKIP :: 'a program ("\\<bottom>")
- "op Join" :: ['a program, 'a program] => 'a program (infixl "\\<squnion>" 65)
- "@JOIN1" :: [pttrns, 'b set] => 'b set ("(3\\<Squnion> _./ _)" 10)
- "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Squnion> _:_./ _)" 10)
+ SKIP :: "'a program" ("\<bottom>")
+ "op Join" :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
+ "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
+ "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _:_./ _)" 10)
+
+
+(** SKIP **)
+
+lemma Init_SKIP [simp]: "Init SKIP = UNIV"
+by (simp add: SKIP_def)
+
+lemma Acts_SKIP [simp]: "Acts SKIP = {Id}"
+by (simp add: SKIP_def)
+
+lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV"
+by (auto simp add: SKIP_def)
+
+lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
+by (force elim: reachable.induct intro: reachable.intros)
+
+(** SKIP and safety properties **)
+
+lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
+by (unfold constrains_def, auto)
+
+lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)"
+by (unfold Constrains_def, auto)
+
+lemma SKIP_in_stable [iff]: "SKIP : stable A"
+by (unfold stable_def, auto)
+
+declare SKIP_in_stable [THEN stable_imp_Stable, iff]
+
+
+(** Join **)
+
+lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
+by (simp add: Join_def)
+
+lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G"
+by (auto simp add: Join_def)
+
+lemma AllowedActs_Join [simp]:
+ "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G"
+by (auto simp add: Join_def)
+
+
+(** JN **)
+
+lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
+by (unfold JOIN_def SKIP_def, auto)
+
+lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)"
+apply (rule program_equalityI)
+apply (auto simp add: JOIN_def Join_def)
+done
+
+lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))"
+by (simp add: JOIN_def)
+
+lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"
+by (auto simp add: JOIN_def)
+
+lemma AllowedActs_JN [simp]:
+ "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))"
+by (auto simp add: JOIN_def)
+
+
+lemma JN_cong [cong]:
+ "[| I=J; !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)"
+by (simp add: JOIN_def)
+
+
+(** Algebraic laws **)
+
+lemma Join_commute: "F Join G = G Join F"
+by (simp add: Join_def Un_commute Int_commute)
+
+lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
+by (simp add: Un_ac Join_def Int_assoc insert_absorb)
+
+lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
+by (simp add: Un_ac Int_ac Join_def insert_absorb)
+
+lemma Join_SKIP_left [simp]: "SKIP Join F = F"
+apply (unfold Join_def SKIP_def)
+apply (rule program_equalityI)
+apply (simp_all (no_asm) add: insert_absorb)
+done
+
+lemma Join_SKIP_right [simp]: "F Join SKIP = F"
+apply (unfold Join_def SKIP_def)
+apply (rule program_equalityI)
+apply (simp_all (no_asm) add: insert_absorb)
+done
+
+lemma Join_absorb [simp]: "F Join F = F"
+apply (unfold Join_def)
+apply (rule program_equalityI, auto)
+done
+
+lemma Join_left_absorb: "F Join (F Join G) = F Join G"
+apply (unfold Join_def)
+apply (rule program_equalityI, auto)
+done
+
+(*Join is an AC-operator*)
+lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
+
+
+(*** JN laws ***)
+
+(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
+lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
+by (auto intro!: program_equalityI)
+
+lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"
+by (auto intro!: program_equalityI)
+
+lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)"
+by (rule program_equalityI, auto)
+
+lemma JN_Join_distrib:
+ "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)"
+by (auto intro!: program_equalityI)
+
+lemma JN_Join_miniscope:
+ "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"
+by (auto simp add: JN_Join_distrib JN_constant)
+
+(*Used to prove guarantees_JN_I*)
+lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F"
+apply (unfold JOIN_def Join_def)
+apply (rule program_equalityI, auto)
+done
+
+
+(*** Safety: co, stable, FP ***)
+
+(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an
+ alternative precondition is A<=B, but most proofs using this rule require
+ I to be nonempty for other reasons anyway.*)
+lemma JN_constrains:
+ "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)"
+by (simp add: constrains_def JOIN_def, blast)
+
+lemma Join_constrains [simp]:
+ "(F Join G : A co B) = (F : A co B & G : A co B)"
+by (auto simp add: constrains_def Join_def)
+
+lemma Join_unless [simp]:
+ "(F Join G : A unless B) = (F : A unless B & G : A unless B)"
+by (simp add: Join_constrains unless_def)
+
+(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
+ reachable (F Join G) could be much bigger than reachable F, reachable G
+*)
+
+
+lemma Join_constrains_weaken:
+ "[| F : A co A'; G : B co B' |]
+ ==> F Join G : (A Int B) co (A' Un B')"
+by (simp, blast intro: constrains_weaken)
+
+(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
+lemma JN_constrains_weaken:
+ "[| 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)"
+apply (simp (no_asm_simp) add: JN_constrains)
+apply (blast intro: constrains_weaken)
+done
+
+lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"
+by (simp add: stable_def constrains_def JOIN_def)
+
+lemma invariant_JN_I:
+ "[| !!i. i:I ==> F i : invariant A; i : I |]
+ ==> (JN i:I. F i) : invariant A"
+by (simp add: invariant_def JN_stable, blast)
+
+lemma Join_stable [simp]:
+ "(F Join G : stable A) =
+ (F : stable A & G : stable A)"
+by (simp add: stable_def)
+
+lemma Join_increasing [simp]:
+ "(F Join G : increasing f) =
+ (F : increasing f & G : increasing f)"
+by (simp add: increasing_def Join_stable, blast)
+
+lemma invariant_JoinI:
+ "[| F : invariant A; G : invariant A |]
+ ==> F Join G : invariant A"
+by (simp add: invariant_def, blast)
+
+lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))"
+by (simp add: FP_def JN_stable INTER_def)
+
+
+(*** Progress: transient, ensures ***)
+
+lemma JN_transient:
+ "i : I ==>
+ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"
+by (auto simp add: transient_def JOIN_def)
+
+lemma Join_transient [simp]:
+ "F Join G : transient A =
+ (F : transient A | G : transient A)"
+by (auto simp add: bex_Un transient_def Join_def)
+
+lemma Join_transient_I1: "F : transient A ==> F Join G : transient A"
+by (simp add: Join_transient)
+
+lemma Join_transient_I2: "G : transient A ==> F Join G : transient A"
+by (simp add: Join_transient)
+
+(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
+lemma JN_ensures:
+ "i : I ==>
+ (JN i:I. F i) : A ensures B =
+ ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))"
+by (auto simp add: ensures_def JN_constrains JN_transient)
+
+lemma Join_ensures:
+ "F Join G : A ensures B =
+ (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) &
+ (F : transient (A-B) | G : transient (A-B)))"
+by (auto simp add: ensures_def Join_transient)
+
+lemma stable_Join_constrains:
+ "[| F : stable A; G : A co A' |]
+ ==> F Join G : A co A'"
+apply (unfold stable_def constrains_def Join_def)
+apply (simp add: ball_Un, blast)
+done
+
+(*Premise for G cannot use Always because F: Stable A is weaker than
+ G : stable A *)
+lemma stable_Join_Always1:
+ "[| F : stable A; G : invariant A |] ==> F Join G : Always A"
+apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
+apply (force intro: stable_Int)
+done
+
+(*As above, but exchanging the roles of F and G*)
+lemma stable_Join_Always2:
+ "[| F : invariant A; G : stable A |] ==> F Join G : Always A"
+apply (subst Join_commute)
+apply (blast intro: stable_Join_Always1)
+done
+
+lemma stable_Join_ensures1:
+ "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B"
+apply (simp (no_asm_simp) add: Join_ensures)
+apply (simp add: stable_def ensures_def)
+apply (erule constrains_weaken, auto)
+done
+
+(*As above, but exchanging the roles of F and G*)
+lemma stable_Join_ensures2:
+ "[| F : A ensures B; G : stable A |] ==> F Join G : A ensures B"
+apply (subst Join_commute)
+apply (blast intro: stable_Join_ensures1)
+done
+
+
+(*** the ok and OK relations ***)
+
+lemma ok_SKIP1 [iff]: "SKIP ok F"
+by (auto simp add: ok_def)
+
+lemma ok_SKIP2 [iff]: "F ok SKIP"
+by (auto simp add: ok_def)
+
+lemma ok_Join_commute:
+ "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
+by (auto simp add: ok_def)
+
+lemma ok_commute: "(F ok G) = (G ok F)"
+by (auto simp add: ok_def)
+
+lemmas ok_sym = ok_commute [THEN iffD1, standard]
+
+lemma ok_iff_OK:
+ "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"
+by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast)
+
+lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)"
+by (auto simp add: ok_def)
+
+lemma ok_Join_iff2 [iff]: "(G Join H) ok F = (G ok F & H ok F)"
+by (auto simp add: ok_def)
+
+(*useful? Not with the previous two around*)
+lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
+by (auto simp add: ok_def)
+
+lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)"
+by (auto simp add: ok_def)
+
+lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (ALL i:I. G i ok F)"
+by (auto simp add: ok_def)
+
+lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"
+by (auto simp add: ok_def OK_def)
+
+lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"
+by (auto simp add: OK_iff_ok)
+
+
+(*** Allowed ***)
+
+lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
+by (auto simp add: Allowed_def)
+
+lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G"
+by (auto simp add: Allowed_def)
+
+lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))"
+by (auto simp add: Allowed_def)
+
+lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)"
+by (simp add: ok_def Allowed_def)
+
+lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
+by (auto simp add: OK_iff_ok ok_iff_Allowed)
+
+(*** safety_prop, for reasoning about given instances of "ok" ***)
+
+lemma safety_prop_Acts_iff:
+ "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
+by (auto simp add: safety_prop_def)
+
+lemma safety_prop_AllowedActs_iff_Allowed:
+ "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)"
+by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
+
+lemma Allowed_eq:
+ "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
+by (simp add: Allowed_def safety_prop_Acts_iff)
+
+lemma def_prg_Allowed:
+ "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]
+ ==> Allowed F = X"
+by (simp add: Allowed_eq)
+
+(*For safety_prop to hold, the property must be satisfiable!*)
+lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)"
+by (simp add: safety_prop_def constrains_def, blast)
+
+lemma safety_prop_stable [iff]: "safety_prop (stable A)"
+by (simp add: stable_def)
+
+lemma safety_prop_Int [simp]:
+ "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)"
+by (simp add: safety_prop_def, blast)
+
+lemma safety_prop_INTER1 [simp]:
+ "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)"
+by (auto simp add: safety_prop_def, blast)
+
+lemma safety_prop_INTER [simp]:
+ "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)"
+by (auto simp add: safety_prop_def, blast)
+
+lemma def_UNION_ok_iff:
+ "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]
+ ==> F ok G = (G : X & acts <= AllowedActs G)"
+by (auto simp add: ok_def safety_prop_Acts_iff)
end