--- a/src/HOL/UNITY/Comp/AllocBase.thy Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Jan 24 18:13:59 2003 +0100
@@ -6,7 +6,7 @@
Common declarations for Chandy and Charpentier's Allocator
*)
-AllocBase = Rename + Follows +
+AllocBase = UNITY_Main +
consts
NbT :: nat (*Number of tokens in system*)
--- a/src/HOL/UNITY/Comp/Handshake.ML Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(* Title: HOL/UNITY/Handshake
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Handshake Protocol
-
-From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
-*)
-
-Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
-program_defs_ref := [F_def, G_def];
-
-Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
-Addsimps [simp_of_set invFG_def];
-
-
-Goal "(F Join G) : Always invFG";
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (rtac (constrains_imp_Constrains RS StableI) 1);
-by Auto_tac;
-by (constrains_tac 2);
-by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
-by (constrains_tac 1);
-qed "invFG";
-
-Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
-\ ({s. NF s = k} Int {s. BB s})";
-by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
-by (ensures_tac "cmdG" 2);
-by (constrains_tac 1);
-qed "lemma2_1";
-
-Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
-by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
-by (constrains_tac 2);
-by (ensures_tac "cmdF" 1);
-qed "lemma2_2";
-
-Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}";
-by (rtac LeadsTo_weaken_R 1);
-by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
- GreaterThan_bounded_induct 1);
-(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
-by (auto_tac (claset() addSIs [lemma2_1, lemma2_2]
- addIs[LeadsTo_Trans, LeadsTo_Diff],
- simpset() addsimps [vimage_def]));
-qed "progress";
--- a/src/HOL/UNITY/Comp/Handshake.thy Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Comp/Handshake.thy Fri Jan 24 18:13:59 2003 +0100
@@ -8,7 +8,7 @@
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
*)
-Handshake = Union +
+theory Handshake = UNITY_Main:
record state =
BB :: bool
@@ -34,4 +34,46 @@
invFG :: "state set"
"invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
+
+declare F_def [THEN def_prg_Init, simp]
+ G_def [THEN def_prg_Init, simp]
+
+ cmdF_def [THEN def_act_simp, simp]
+ cmdG_def [THEN def_act_simp, simp]
+
+ invFG_def [THEN def_set_simp, simp]
+
+
+lemma invFG: "(F Join G) : Always invFG"
+apply (rule AlwaysI)
+apply force
+apply (rule constrains_imp_Constrains [THEN StableI])
+apply auto
+ apply (unfold F_def, constrains)
+apply (unfold G_def, constrains)
+done
+
+lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo
+ ({s. NF s = k} Int {s. BB s})"
+apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
+ apply (unfold F_def, constrains)
+apply (unfold G_def, ensures_tac "cmdG")
+done
+
+lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo
+ {s. k < NF s}"
+apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
+ apply (unfold F_def, ensures_tac "cmdF")
+apply (unfold G_def, constrains)
+done
+
+lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
+apply (rule LeadsTo_weaken_R)
+apply (rule_tac f = "NF" and l = "Suc m" and B = "{}"
+ in GreaterThan_bounded_induct)
+(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
+apply (auto intro!: lemma2_1 lemma2_2
+ intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
+done
+
end
--- a/src/HOL/UNITY/Comp/TimerArray.ML Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: HOL/UNITY/TimerArray.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-A trivial example of reasoning about an array of processes
-*)
-
-Addsimps [Timer_def RS def_prg_Init];
-program_defs_ref := [Timer_def];
-
-Addsimps [count_def, decr_def];
-
-(*Demonstrates induction, but not used in the following proof*)
-Goal "Timer : UNIV leadsTo {s. count s = 0}";
-by (res_inst_tac [("f", "count")] lessThan_induct 1);
-by (Simp_tac 1);
-by (case_tac "m" 1);
-by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
-by (ensures_tac "decr" 1);
-qed "Timer_leadsTo_zero";
-
-Goal "Timer : preserves snd";
-by (rtac preservesI 1);
-by (constrains_tac 1);
-qed "Timer_preserves_snd";
-AddIffs [Timer_preserves_snd];
-
-Addsimps [PLam_stable];
-
-Goal "finite I \
-\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
-by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")]
- (finite_stable_completion RS leadsTo_weaken) 1);
-by Auto_tac;
-(*Safety property, already reduced to the single Timer case*)
-by (constrains_tac 2);
-(*Progress property for the array of Timers*)
-by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
-by (case_tac "m" 1);
-(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
-by (auto_tac (claset() addIs [subset_imp_leadsTo],
- simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
- lift_set_Un_distrib RS sym,
- Times_Un_distrib1 RS sym,
- Times_Diff_distrib1 RS sym]));
-by (rename_tac "n" 1);
-by (rtac PLam_leadsTo_Basis 1);
-by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
-by (constrains_tac 1);
-by (res_inst_tac [("act", "decr")] transientI 1);
-by (auto_tac (claset(), simpset() addsimps [Timer_def]));
-qed "TimerArray_leadsTo_zero";
--- a/src/HOL/UNITY/Comp/TimerArray.thy Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Fri Jan 24 18:13:59 2003 +0100
@@ -6,7 +6,7 @@
A trivial example of reasoning about an array of processes
*)
-TimerArray = PPROD +
+theory TimerArray = UNITY_Main:
types 'a state = "nat * 'a" (*second component allows new variables*)
@@ -17,7 +17,52 @@
decr :: "('a state * 'a state) set"
"decr == UN n uu. {((Suc n, uu), (n,uu))}"
- Timer :: 'a state program
+ Timer :: "'a state program"
"Timer == mk_program (UNIV, {decr}, UNIV)"
+
+declare Timer_def [THEN def_prg_Init, simp]
+
+declare count_def [simp] decr_def [simp]
+
+(*Demonstrates induction, but not used in the following proof*)
+lemma Timer_leadsTo_zero: "Timer : UNIV leadsTo {s. count s = 0}"
+apply (rule_tac f = count in lessThan_induct, simp)
+apply (case_tac "m")
+ apply (force intro!: subset_imp_leadsTo)
+apply (unfold Timer_def, ensures_tac "decr")
+done
+
+lemma Timer_preserves_snd [iff]: "Timer : preserves snd"
+apply (rule preservesI)
+apply (unfold Timer_def, constrains)
+done
+
+
+declare PLam_stable [simp]
+
+lemma TimerArray_leadsTo_zero:
+ "finite I
+ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
+apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)"
+ in finite_stable_completion [THEN leadsTo_weaken])
+apply auto
+(*Safety property, already reduced to the single Timer case*)
+ prefer 2
+ apply (simp add: Timer_def, constrains)
+(*Progress property for the array of Timers*)
+apply (rule_tac f = "sub i o fst" in lessThan_induct)
+apply (case_tac "m")
+(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
+apply (auto intro: subset_imp_leadsTo
+ simp add: insert_absorb
+ lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric]
+ Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
+apply (rename_tac "n")
+apply (rule PLam_leadsTo_Basis)
+apply (auto simp add: lessThan_Suc [symmetric])
+apply (unfold Timer_def, constrains)
+apply (rule_tac act = decr in transientI, auto)
+done
+
end
--- a/src/HOL/UNITY/Lift_prog.ML Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,487 +0,0 @@
-(* Title: HOL/UNITY/Lift_prog.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Arrays of processes.
-*)
-
-Addsimps [insert_map_def, delete_map_def];
-
-Goal "delete_map i (insert_map i x f) = f";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "insert_map_inverse";
-
-Goal "(insert_map i x (delete_map i g)) = g(i:=x)";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "insert_map_delete_map_eq";
-
-(*** Injectiveness proof ***)
-
-Goal "(insert_map i x f) = (insert_map i y g) ==> x=y";
-by (dres_inst_tac [("x","i")] fun_cong 1);
-by (Full_simp_tac 1);
-qed "insert_map_inject1";
-
-Goal "(insert_map i x f) = (insert_map i y g) ==> f=g";
-by (dres_inst_tac [("f", "delete_map i")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [insert_map_inverse]) 1);
-qed "insert_map_inject2";
-
-Goal "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g";
-by (blast_tac (claset() addDs [insert_map_inject1, insert_map_inject2]) 1);
-bind_thm ("insert_map_inject", result() RS conjE);
-AddSEs [insert_map_inject];
-
-(*The general case: we don't assume i=i'*)
-Goalw [lift_map_def]
- "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) \
-\ = (uu = uu' & insert_map i s f = insert_map i' s' f')";
-by Auto_tac;
-qed "lift_map_eq_iff";
-AddIffs [lift_map_eq_iff];
-
-Goalw [lift_map_def, drop_map_def] "!!s. drop_map i (lift_map i s) = s";
-by (force_tac (claset() addIs [insert_map_inverse], simpset()) 1);
-qed "drop_map_lift_map_eq";
-Addsimps [drop_map_lift_map_eq];
-
-Goalw [lift_map_def] "inj (lift_map i)";
-by (rtac injI 1);
-by Auto_tac;
-qed "inj_lift_map";
-
-(*** Surjectiveness proof ***)
-
-Goalw [lift_map_def, drop_map_def] "!!s. lift_map i (drop_map i s) = s";
-by (force_tac (claset(), simpset() addsimps [insert_map_delete_map_eq]) 1);
-qed "lift_map_drop_map_eq";
-Addsimps [lift_map_drop_map_eq];
-
-Goal "(drop_map i s) = (drop_map i s') ==> s=s'";
-by (dres_inst_tac [("f", "lift_map i")] arg_cong 1);
-by (Full_simp_tac 1);
-qed "drop_map_inject";
-AddSDs [drop_map_inject];
-
-Goal "surj (lift_map i)";
-by (rtac surjI 1);
-by (rtac lift_map_drop_map_eq 1);
-qed "surj_lift_map";
-
-Goal "bij (lift_map i)";
-by (simp_tac (simpset() addsimps [bij_def, inj_lift_map, surj_lift_map]) 1);
-qed "bij_lift_map";
-AddIffs [bij_lift_map];
-
-Goal "inv (lift_map i) = drop_map i";
-by (rtac inv_equality 1);
-by Auto_tac;
-qed "inv_lift_map_eq";
-Addsimps [inv_lift_map_eq];
-
-Goal "inv (drop_map i) = lift_map i";
-by (rtac inv_equality 1);
-by Auto_tac;
-qed "inv_drop_map_eq";
-Addsimps [inv_drop_map_eq];
-
-Goal "bij (drop_map i)";
-by (simp_tac (simpset() delsimps [inv_lift_map_eq]
- addsimps [inv_lift_map_eq RS sym, bij_imp_bij_inv]) 1);
-qed "bij_drop_map";
-AddIffs [bij_drop_map];
-
-(*sub's main property!*)
-Goal "sub i f = f i";
-by (simp_tac (simpset() addsimps [sub_def]) 1);
-qed "sub_apply";
-Addsimps [sub_apply];
-
-(*** lift_set ***)
-
-Goalw [lift_set_def] "lift_set i {} = {}";
-by Auto_tac;
-qed "lift_set_empty";
-Addsimps [lift_set_empty];
-
-Goalw [lift_set_def] "(lift_map i x : lift_set i A) = (x : A)";
-by (rtac (inj_lift_map RS inj_image_mem_iff) 1);
-qed "lift_set_iff";
-
-(*Do we really need both this one and its predecessor?*)
-Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)";
-by (asm_simp_tac (simpset() addsimps [lift_set_def,
- mem_rename_set_iff, drop_map_def]) 1);
-qed "lift_set_iff2";
-AddIffs [lift_set_iff2];
-
-Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B";
-by (etac image_mono 1);
-qed "lift_set_mono";
-
-Goalw [lift_set_def] "lift_set i (A Un B) = lift_set i A Un lift_set i B";
-by (asm_simp_tac (simpset() addsimps [image_Un]) 1);
-qed "lift_set_Un_distrib";
-
-Goalw [lift_set_def] "lift_set i (A-B) = lift_set i A - lift_set i B";
-by (rtac (inj_lift_map RS image_set_diff) 1);
-qed "lift_set_Diff_distrib";
-
-
-(*** the lattice operations ***)
-
-Goal "bij (lift i)";
-by (simp_tac (simpset() addsimps [lift_def]) 1);
-qed "bij_lift";
-AddIffs [bij_lift];
-
-Goalw [lift_def] "lift i SKIP = SKIP";
-by (Asm_simp_tac 1);
-qed "lift_SKIP";
-Addsimps [lift_SKIP];
-
-Goalw [lift_def] "lift i (F Join G) = lift i F Join lift i G";
-by (Asm_simp_tac 1);
-qed "lift_Join";
-Addsimps [lift_Join];
-
-Goalw [lift_def] "lift j (JOIN I F) = (JN i:I. lift j (F i))";
-by (Asm_simp_tac 1);
-qed "lift_JN";
-Addsimps [lift_JN];
-
-(*** Safety: co, stable, invariant ***)
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)";
-by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
-qed "lift_constrains";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : stable (lift_set i A)) = (F : stable A)";
-by (asm_simp_tac (simpset() addsimps [rename_stable]) 1);
-qed "lift_stable";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : invariant (lift_set i A)) = (F : invariant A)";
-by (asm_simp_tac (simpset() addsimps [rename_invariant]) 1);
-qed "lift_invariant";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)";
-by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
-qed "lift_Constrains";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : Stable (lift_set i A)) = (F : Stable A)";
-by (asm_simp_tac (simpset() addsimps [rename_Stable]) 1);
-qed "lift_Stable";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : Always (lift_set i A)) = (F : Always A)";
-by (asm_simp_tac (simpset() addsimps [rename_Always]) 1);
-qed "lift_Always";
-
-(*** Progress: transient, ensures ***)
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : transient (lift_set i A)) = (F : transient A)";
-by (asm_simp_tac (simpset() addsimps [rename_transient]) 1);
-qed "lift_transient";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : (lift_set i A) ensures (lift_set i B)) = \
-\ (F : A ensures B)";
-by (asm_simp_tac (simpset() addsimps [rename_ensures]) 1);
-qed "lift_ensures";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : (lift_set i A) leadsTo (lift_set i B)) = \
-\ (F : A leadsTo B)";
-by (asm_simp_tac (simpset() addsimps [rename_leadsTo]) 1);
-qed "lift_leadsTo";
-
-Goalw [lift_def, lift_set_def]
- "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) = \
-\ (F : A LeadsTo B)";
-by (asm_simp_tac (simpset() addsimps [rename_LeadsTo]) 1);
-qed "lift_LeadsTo";
-
-
-(** guarantees **)
-
-Goalw [lift_def]
- "(lift i F : (lift i ` X) guarantees (lift i ` Y)) = \
-\ (F : X guarantees Y)";
-by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [o_def]) 1);
-qed "lift_lift_guarantees_eq";
-
-Goal "(lift i F : X guarantees Y) = \
-\ (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))";
-by (asm_simp_tac
- (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
- lift_def]) 1);
-qed "lift_guarantees_eq_lift_inv";
-
-
-(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj,
- which is used only in TimerArray and perhaps isn't even essential
- there!
-***)
-
-(*To preserve snd means that the second component is there just to allow
- guarantees properties to be stated. Converse fails, for lift i F can
- change function components other than i*)
-Goal "F : preserves snd ==> lift i F : preserves snd";
-by (dres_inst_tac [("w1", "snd")] (impOfSubs subset_preserves_o) 1);
-by (asm_simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
-by (full_simp_tac (simpset() addsimps [lift_map_def, o_def, split_def]) 1);
-qed "lift_preserves_snd_I";
-
-Goal "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)";
-by (dres_inst_tac [("f", "insert_map i (g i)")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [insert_map_delete_map_eq]) 1);
-by (etac exI 1);
-bind_thm ("delete_map_eqE", result() RS exE);
-AddSEs [delete_map_eqE];
-
-Goal "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i";
-by (Force_tac 1);
-qed "delete_map_neq_apply";
-
-(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
-
-Goal "(f o fst) -` A = (f-`A) <*> UNIV";
-by Auto_tac;
-qed "vimage_o_fst_eq";
-
-Goal "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)";
-by Auto_tac;
-qed "vimage_sub_eq_lift_set";
-
-Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
-
-Goalw [extend_act_def]
- "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) = \
-\ ((drop_map i s, drop_map i s') : act)";
-by Auto_tac;
-by (rtac bexI 1);
-by Auto_tac;
-qed "mem_lift_act_iff";
-AddIffs [mem_lift_act_iff];
-
-Goal "[| F : preserves snd; i~=j |] \
-\ ==> lift j F : stable (lift_set i (A <*> UNIV))";
-by (auto_tac (claset(),
- simpset() addsimps [lift_def, lift_set_def,
- stable_def, constrains_def, rename_def,
- extend_def, mem_rename_set_iff]));
-by (auto_tac (claset() addSDs [preserves_imp_eq],
- simpset() addsimps [lift_map_def, drop_map_def]));
-by (dres_inst_tac [("x", "i")] fun_cong 1);
-by Auto_tac;
-qed "preserves_snd_lift_stable";
-
-(*If i~=j then lift j F does nothing to lift_set i, and the
- premise ensures A<=B.*)
-Goal "[| F i : (A <*> UNIV) co (B <*> UNIV); \
-\ F j : preserves snd |] \
-\ ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))";
-by (case_tac "i=j" 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def,
- rename_constrains]) 1);
-by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1);
-by (assume_tac 1);
-by (etac (constrains_imp_subset RS lift_set_mono) 1);
-qed "constrains_imp_lift_constrains";
-
-(** Lemmas for the transient theorem **)
-
-Goal "(insert_map i t f)(i := s) = insert_map i s f";
-by (rtac ext 1);
-by Auto_tac;
-qed "insert_map_upd_same";
-
-Goal "(insert_map j t f)(i := s) = \
-\ (if i=j then insert_map i s f \
-\ else if i<j then insert_map j t (f(i:=s)) \
-\ else insert_map j t (f(i - Suc 0 := s)))";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-by (ALLGOALS arith_tac);
-qed "insert_map_upd";
-
-Goal "[| insert_map i s f = insert_map j t g; i~=j |] \
-\ ==> EX g'. insert_map i s' f = insert_map j t g'";
-by (stac (insert_map_upd_same RS sym) 1);
-by (etac ssubst 1);
-by (asm_simp_tac (HOL_ss addsimps [insert_map_upd]) 1);
-by (Blast_tac 1);
-qed "insert_map_eq_diff";
-
-Goalw [lift_map_def]
- "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i~=j |] \
-\ ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))";
-by Auto_tac;
-by (blast_tac (claset() addDs [insert_map_eq_diff]) 1);
-qed "lift_map_eq_diff";
-
-Goal "F : preserves snd \
-\ ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \
-\ (i=j & F : transient (A <*> UNIV) | A={})";
-by (case_tac "i=j" 1);
-by (auto_tac (claset(), simpset() addsimps [lift_transient]));
-by (auto_tac (claset(),
- simpset() addsimps [lift_set_def, lift_def, transient_def,
- rename_def, extend_def, Domain_extend_act]));
-by (dtac subsetD 1);
-by (Blast_tac 1);
-by Auto_tac;
-by (rename_tac "s f uu s' f' uu'" 1);
-by (subgoal_tac "f'=f & uu'=uu" 1);
-by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
-by Auto_tac;
-by (dtac sym 1);
-by (dtac subsetD 1);
-by (rtac ImageI 1);
-by (etac
- (bij_lift_map RS good_map_bij RS export (mem_extend_act_iff RS iffD2)) 1);
-by (Force_tac 1);
-by (etac (lift_map_eq_diff RS exE) 1);
-by Auto_tac;
-qed "lift_transient_eq_disj";
-
-(*USELESS??*)
-Goal "lift_map i ` (A <*> UNIV) = \
-\ (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
-by (auto_tac (claset() addSIs [bexI, image_eqI],
- simpset() addsimps [lift_map_def]));
-by (rtac (split_conv RS sym) 1);
-qed "lift_map_image_Times";
-
-Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))";
-by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
-qed "lift_preserves_eq";
-
-(*A useful rewrite. If o, sub have been rewritten out already then can also
- use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*)
-Goal "F : preserves snd \
-\ ==> lift i F : preserves (v o sub j o fst) = \
-\ (if i=j then F : preserves (v o fst) else True)";
-by (dtac (impOfSubs subset_preserves_o) 1);
-by (full_simp_tac (simpset() addsimps [lift_preserves_eq, o_def,
- drop_map_lift_map_eq]) 1);
-by (asm_simp_tac (simpset() delcongs [if_weak_cong]
- addsimps [lift_map_def,
- eq_commute, split_def, o_def]) 1);
-by Auto_tac;
-qed "lift_preserves_sub";
-
-
-(*** Lemmas to handle function composition (o) more consistently ***)
-
-(*Lets us prove one version of a theorem and store others*)
-Goal "f o g = h ==> f' o f o g = f' o h";
-by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1);
-qed "o_equiv_assoc";
-
-Goal "f o g = h ==> ALL x. f(g x) = h x";
-by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1);
-qed "o_equiv_apply";
-
-fun make_o_equivs th =
- [th,
- th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
- th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
-
-Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
-
-Goal "sub i o fst o lift_map i = fst";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def, sub_def]));
-qed "fst_o_lift_map";
-
-Goal "snd o lift_map i = snd o snd";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def]));
-qed "snd_o_lift_map";
-
-Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
-
-
-(*** More lemmas about extend and project
- They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
-
-Goal "extend_act h' (extend_act h act) = \
-\ extend_act (%(x,(y,y')). h'(h(x,y),y')) act";
-by (auto_tac (claset() addSEs [rev_bexI],
- simpset() addsimps [extend_act_def]));
-by (ALLGOALS Blast_tac);
-qed "extend_act_extend_act";
-
-Goal "project_act h (project_act h' act) = \
-\ project_act (%(x,(y,y')). h'(h(x,y),y')) act";
-by (auto_tac (claset() addSEs [rev_bexI],
- simpset() addsimps [project_act_def]));
-qed "project_act_project_act";
-
-Goal "project_act h (extend_act h' act) = \
-\ {(x,x'). EX s s' y y' z. (s,s') : act & \
-\ h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}";
-by (simp_tac (simpset() addsimps [extend_act_def, project_act_def]) 1);
-by (Blast_tac 1);
-qed "project_act_extend_act";
-
-
-(*** OK and "lift" ***)
-
-Goal "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts";
-by (res_inst_tac [("a","mk_program(UNIV,{act},UNIV)")] UN_I 1);
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def,stable_def,constrains_def]));
-qed "act_in_UNION_preserves_fst";
-
-Goal "[| ALL i:I. F i : preserves snd; \
-\ ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] \
-\ ==> OK I (%i. lift i (F i))";
-by (auto_tac (claset(),
- simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend]));
-by (simp_tac (
- simpset() addsimps [export AllowedActs_extend,project_act_extend_act]) 1);
-by (rename_tac "act" 1);
-by (subgoal_tac
- "{(x, x'). EX s f u s' f' u'. \
-\ ((s, f, u), s', f', u') : act & \
-\ lift_map j x = lift_map i (s, f, u) & \
-\ lift_map j x' = lift_map i (s', f', u')} \
-\ <= {(x,x'). fst x = fst x'}" 1);
-by (blast_tac (claset() addIs [act_in_UNION_preserves_fst]) 1);
-by (Clarify_tac 1);
-by (REPEAT (dres_inst_tac [("x","j")] fun_cong 1) );
-by (dres_inst_tac [("x","i")] bspec 1);
-by (assume_tac 1);
-by (ftac preserves_imp_eq 1);
-by Auto_tac;
-qed "UNION_OK_lift_I";
-
-Goal "[| ALL i:I. F i : preserves snd; \
-\ ALL i:I. preserves fst <= Allowed (F i) |] \
-\ ==> OK I (%i. lift i (F i))";
-by (asm_full_simp_tac
- (simpset() addsimps [safety_prop_AllowedActs_iff_Allowed,
- UNION_OK_lift_I]) 1);
-qed "OK_lift_I";
-
-Goal "Allowed (lift i F) = lift i ` (Allowed F)";
-by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1);
-qed "Allowed_lift";
-Addsimps [Allowed_lift];
-
-Goal "lift i ` preserves v = preserves (v o drop_map i)";
-by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def,
- inv_lift_map_eq]) 1);
-qed "lift_image_preserves";
--- a/src/HOL/UNITY/Lift_prog.thy Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Fri Jan 24 18:13:59 2003 +0100
@@ -3,10 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
-lift_prog, etc: replication of components
+lift_prog, etc: replication of components and arrays of processes.
*)
-Lift_prog = Rename +
+theory Lift_prog = Rename:
constdefs
@@ -31,9 +31,458 @@
"lift i == rename (lift_map i)"
(*simplifies the expression of specifications*)
- constdefs
- sub :: ['a, 'a=>'b] => 'b
- "sub == %i f. f i"
+ sub :: "['a, 'a=>'b] => 'b"
+ "sub == %i f. f i"
+
+
+declare insert_map_def [simp] delete_map_def [simp]
+
+lemma insert_map_inverse: "delete_map i (insert_map i x f) = f"
+apply (rule ext)
+apply (simp (no_asm))
+done
+
+lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
+apply (rule ext)
+apply (auto split add: nat_diff_split)
+done
+
+(*** Injectiveness proof ***)
+
+lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
+apply (drule_tac x = i in fun_cong)
+apply (simp (no_asm_use))
+done
+
+lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g"
+apply (drule_tac f = "delete_map i" in arg_cong)
+apply (simp (no_asm_use) add: insert_map_inverse)
+done
+
+lemma insert_map_inject':
+ "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g"
+by (blast dest: insert_map_inject1 insert_map_inject2)
+
+lemmas insert_map_inject = insert_map_inject' [THEN conjE, elim!]
+
+(*The general case: we don't assume i=i'*)
+lemma lift_map_eq_iff [iff]:
+ "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu')))
+ = (uu = uu' & insert_map i s f = insert_map i' s' f')"
+apply (unfold lift_map_def, auto)
+done
+
+(*The !!s allows the automatic splitting of the bound variable*)
+lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s"
+apply (unfold lift_map_def drop_map_def)
+apply (force intro: insert_map_inverse)
+done
+
+lemma inj_lift_map: "inj (lift_map i)"
+apply (unfold lift_map_def)
+apply (rule inj_onI, auto)
+done
+
+(*** Surjectiveness proof ***)
+
+lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
+apply (unfold lift_map_def drop_map_def)
+apply (force simp add: insert_map_delete_map_eq)
+done
+
+lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'"
+apply (drule_tac f = "lift_map i" in arg_cong)
+apply (simp (no_asm_use))
+done
+
+lemma surj_lift_map: "surj (lift_map i)"
+apply (rule surjI)
+apply (rule lift_map_drop_map_eq)
+done
+
+lemma bij_lift_map [iff]: "bij (lift_map i)"
+apply (simp (no_asm) add: bij_def inj_lift_map surj_lift_map)
+done
+
+lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i"
+by (rule inv_equality, auto)
+
+lemma inv_drop_map_eq [simp]: "inv (drop_map i) = lift_map i"
+by (rule inv_equality, auto)
+
+lemma bij_drop_map [iff]: "bij (drop_map i)"
+by (simp del: inv_lift_map_eq add: inv_lift_map_eq [symmetric] bij_imp_bij_inv)
+
+(*sub's main property!*)
+lemma sub_apply [simp]: "sub i f = f i"
+apply (simp (no_asm) add: sub_def)
+done
+
+(*** lift_set ***)
+
+lemma lift_set_empty [simp]: "lift_set i {} = {}"
+by (unfold lift_set_def, auto)
+
+lemma lift_set_iff: "(lift_map i x : lift_set i A) = (x : A)"
+apply (unfold lift_set_def)
+apply (rule inj_lift_map [THEN inj_image_mem_iff])
+done
+
+(*Do we really need both this one and its predecessor?*)
+lemma lift_set_iff2 [iff]:
+ "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"
+by (simp (no_asm_simp) add: lift_set_def mem_rename_set_iff drop_map_def)
+
+
+lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B"
+apply (unfold lift_set_def)
+apply (erule image_mono)
+done
+
+lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B"
+apply (unfold lift_set_def)
+apply (simp (no_asm_simp) add: image_Un)
+done
+
+lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
+apply (unfold lift_set_def)
+apply (rule inj_lift_map [THEN image_set_diff])
+done
+
+
+(*** the lattice operations ***)
+
+lemma bij_lift [iff]: "bij (lift i)"
+apply (simp (no_asm) add: lift_def)
+done
+
+lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
+apply (unfold lift_def)
+apply (simp (no_asm_simp))
+done
+
+lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
+apply (unfold lift_def)
+apply (simp (no_asm_simp))
+done
+
+lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))"
+apply (unfold lift_def)
+apply (simp (no_asm_simp))
+done
+
+(*** Safety: co, stable, invariant ***)
+
+lemma lift_constrains:
+ "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_constrains)
+done
+
+lemma lift_stable:
+ "(lift i F : stable (lift_set i A)) = (F : stable A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_stable)
+done
+
+lemma lift_invariant:
+ "(lift i F : invariant (lift_set i A)) = (F : invariant A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_invariant)
+done
+
+lemma lift_Constrains:
+ "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_Constrains)
+done
+
+lemma lift_Stable:
+ "(lift i F : Stable (lift_set i A)) = (F : Stable A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_Stable)
+done
+
+lemma lift_Always:
+ "(lift i F : Always (lift_set i A)) = (F : Always A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_Always)
+done
+
+(*** Progress: transient, ensures ***)
+
+lemma lift_transient:
+ "(lift i F : transient (lift_set i A)) = (F : transient A)"
+
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_transient)
+done
+
+lemma lift_ensures:
+ "(lift i F : (lift_set i A) ensures (lift_set i B)) =
+ (F : A ensures B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_ensures)
+done
+
+lemma lift_leadsTo:
+ "(lift i F : (lift_set i A) leadsTo (lift_set i B)) =
+ (F : A leadsTo B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_leadsTo)
+done
+
+lemma lift_LeadsTo:
+ "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =
+ (F : A LeadsTo B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_LeadsTo)
+done
+
+
+(** guarantees **)
+
+lemma lift_lift_guarantees_eq:
+ "(lift i F : (lift i ` X) guarantees (lift i ` Y)) =
+ (F : X guarantees Y)"
+
+apply (unfold lift_def)
+apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
+apply (simp (no_asm_simp) add: o_def)
+done
+
+lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) =
+ (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
+by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
+(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj,
+ which is used only in TimerArray and perhaps isn't even essential
+ there!
+***)
+
+(*To preserve snd means that the second component is there just to allow
+ guarantees properties to be stated. Converse fails, for lift i F can
+ change function components other than i*)
+lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd"
+apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
+apply (simp (no_asm_simp) add: lift_def rename_preserves)
+apply (simp (no_asm_use) add: lift_map_def o_def split_def)
+done
+
+lemma delete_map_eqE':
+ "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"
+apply (drule_tac f = "insert_map i (g i) " in arg_cong)
+apply (simp (no_asm_use) add: insert_map_delete_map_eq)
+apply (erule exI)
+done
+
+lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]
+
+lemma delete_map_neq_apply:
+ "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i"
+by force
+
+(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
+
+lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
+by auto
+
+lemma vimage_sub_eq_lift_set [simp]:
+ "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
+by auto
+
+lemma mem_lift_act_iff [iff]:
+ "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) =
+ ((drop_map i s, drop_map i s') : act)"
+apply (unfold extend_act_def, auto)
+apply (rule bexI, auto)
+done
+
+lemma preserves_snd_lift_stable:
+ "[| F : preserves snd; i~=j |]
+ ==> lift j F : stable (lift_set i (A <*> UNIV))"
+apply (auto simp add: lift_def lift_set_def stable_def constrains_def rename_def extend_def mem_rename_set_iff)
+apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
+apply (drule_tac x = i in fun_cong, auto)
+done
+
+(*If i~=j then lift j F does nothing to lift_set i, and the
+ premise ensures A<=B.*)
+lemma constrains_imp_lift_constrains:
+ "[| F i : (A <*> UNIV) co (B <*> UNIV);
+ F j : preserves snd |]
+ ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
+apply (case_tac "i=j")
+apply (simp add: lift_def lift_set_def rename_constrains)
+apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], assumption)
+apply (erule constrains_imp_subset [THEN lift_set_mono])
+done
+
+(** Lemmas for the transient theorem **)
+
+lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f"
+by (rule ext, auto)
+
+lemma insert_map_upd:
+ "(insert_map j t f)(i := s) =
+ (if i=j then insert_map i s f
+ else if i<j then insert_map j t (f(i:=s))
+ else insert_map j t (f(i - Suc 0 := s)))"
+apply (rule ext)
+apply (simp split add: nat_diff_split)
+done
+
+lemma insert_map_eq_diff:
+ "[| insert_map i s f = insert_map j t g; i~=j |]
+ ==> EX g'. insert_map i s' f = insert_map j t g'"
+apply (subst insert_map_upd_same [symmetric])
+apply (erule ssubst)
+apply (simp only: insert_map_upd if_False split: split_if, blast)
+done
+
+lemma lift_map_eq_diff:
+ "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i~=j |]
+ ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
+apply (unfold lift_map_def, auto)
+apply (blast dest: insert_map_eq_diff)
+done
+
+
+ML
+{*
+bind_thm ("export_mem_extend_act_iff", export mem_extend_act_iff)
+*}
+
+
+lemma lift_transient_eq_disj:
+ "F : preserves snd
+ ==> (lift i F : transient (lift_set j (A <*> UNIV))) =
+ (i=j & F : transient (A <*> UNIV) | A={})"
+apply (case_tac "i=j")
+apply (auto simp add: lift_transient)
+apply (auto simp add: lift_set_def lift_def transient_def rename_def extend_def Domain_extend_act)
+apply (drule subsetD, blast)
+apply auto
+apply (rename_tac s f uu s' f' uu')
+apply (subgoal_tac "f'=f & uu'=uu")
+ prefer 2 apply (force dest!: preserves_imp_eq, auto)
+apply (drule sym)
+apply (drule subsetD)
+apply (rule ImageI)
+apply (erule bij_lift_map [THEN good_map_bij,
+ THEN export_mem_extend_act_iff [THEN iffD2]], force)
+apply (erule lift_map_eq_diff [THEN exE], auto)
+done
+
+(*USELESS??*)
+lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) =
+ (UN s:A. UN f. {insert_map i s f}) <*> UNIV"
+apply (auto intro!: bexI image_eqI simp add: lift_map_def)
+apply (rule split_conv [symmetric])
+done
+
+lemma lift_preserves_eq:
+ "(lift i F : preserves v) = (F : preserves (v o lift_map i))"
+by (simp add: lift_def rename_preserves)
+
+(*A useful rewrite. If o, sub have been rewritten out already then can also
+ use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*)
+lemma lift_preserves_sub:
+ "F : preserves snd
+ ==> lift i F : preserves (v o sub j o fst) =
+ (if i=j then F : preserves (v o fst) else True)"
+apply (drule subset_preserves_o [THEN subsetD])
+apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
+apply (simp cong del: if_weak_cong add: lift_map_def eq_commute split_def o_def, auto)
+done
+
+
+(*** Lemmas to handle function composition (o) more consistently ***)
+
+(*Lets us prove one version of a theorem and store others*)
+lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
+by (simp add: expand_fun_eq o_def)
+
+lemma o_equiv_apply: "f o g = h ==> ALL x. f(g x) = h x"
+by (simp add: expand_fun_eq o_def)
+
+lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
+apply (rule ext)
+apply (auto simp add: o_def lift_map_def sub_def)
+done
+
+lemma snd_o_lift_map: "snd o lift_map i = snd o snd"
+apply (rule ext)
+apply (auto simp add: o_def lift_map_def)
+done
+
+
+(*** More lemmas about extend and project
+ They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
+
+lemma extend_act_extend_act: "extend_act h' (extend_act h act) =
+ extend_act (%(x,(y,y')). h'(h(x,y),y')) act"
+apply (auto elim!: rev_bexI simp add: extend_act_def, blast)
+done
+
+lemma project_act_project_act: "project_act h (project_act h' act) =
+ project_act (%(x,(y,y')). h'(h(x,y),y')) act"
+by (auto elim!: rev_bexI simp add: project_act_def)
+
+lemma project_act_extend_act:
+ "project_act h (extend_act h' act) =
+ {(x,x'). EX s s' y y' z. (s,s') : act &
+ h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
+by (simp add: extend_act_def project_act_def, blast)
+
+
+(*** OK and "lift" ***)
+
+lemma act_in_UNION_preserves_fst:
+ "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts"
+apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
+apply (auto simp add: preserves_def stable_def constrains_def)
+done
+
+
+ML
+{*
+bind_thm ("export_Acts_extend", export Acts_extend);
+bind_thm ("export_AllowedActs_extend", export AllowedActs_extend)
+*}
+
+lemma UNION_OK_lift_I:
+ "[| ALL i:I. F i : preserves snd;
+ ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]
+ ==> OK I (%i. lift i (F i))"
+apply (auto simp add: OK_def lift_def rename_def export_Acts_extend)
+apply (simp (no_asm) add: export_AllowedActs_extend project_act_extend_act)
+apply (rename_tac "act")
+apply (subgoal_tac
+ "{(x, x'). \<exists>s f u s' f' u'.
+ ((s, f, u), s', f', u') : act &
+ lift_map j x = lift_map i (s, f, u) &
+ lift_map j x' = lift_map i (s', f', u') }
+ <= { (x,x') . fst x = fst x'}")
+apply (blast intro: act_in_UNION_preserves_fst, clarify)
+apply (drule_tac x = j in fun_cong)+
+apply (drule_tac x = i in bspec, assumption)
+apply (frule preserves_imp_eq, auto)
+done
+
+lemma OK_lift_I:
+ "[| ALL i:I. F i : preserves snd;
+ ALL i:I. preserves fst <= Allowed (F i) |]
+ ==> OK I (%i. lift i (F i))"
+by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
+
+
+lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
+by (simp add: lift_def Allowed_rename)
+
+lemma lift_image_preserves: "lift i ` preserves v = preserves (v o drop_map i)"
+apply (simp (no_asm) add: rename_image_preserves lift_def inv_lift_map_eq)
+done
+
end
--- a/src/HOL/UNITY/PPROD.ML Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,281 +0,0 @@
-(* Title: HOL/UNITY/PPROD.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Abstraction over replicated components (PLam)
-General products of programs (Pi operation)
-
-Some dead wood here!
-*)
-
-(*** Basic properties ***)
-
-Goal "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
-by (simp_tac (simpset() addsimps [PLam_def, lift_def, lift_set_def]) 1);
-qed "Init_PLam";
-
-Addsimps [Init_PLam];
-
-Goal "PLam {} F = SKIP";
-by (simp_tac (simpset() addsimps [PLam_def]) 1);
-qed "PLam_empty";
-
-Goal "(plam i: I. SKIP) = SKIP";
-by (simp_tac (simpset() addsimps [PLam_def,lift_SKIP,JN_constant]) 1);
-qed "PLam_SKIP";
-
-Addsimps [PLam_SKIP, PLam_empty];
-
-Goalw [PLam_def] "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)";
-by Auto_tac;
-qed "PLam_insert";
-
-Goal "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)";
-by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1);
-qed "PLam_component_iff";
-
-Goalw [PLam_def] "i : I ==> lift i (F i) <= (PLam I F)";
-(*blast_tac doesn't use HO unification*)
-by (fast_tac (claset() addIs [component_JN]) 1);
-qed "component_PLam";
-
-
-(** Safety & Progress: but are they used anywhere? **)
-
-Goal "[| i : I; ALL j. F j : preserves snd |] ==> \
-\ (PLam I F : (lift_set i (A <*> UNIV)) co \
-\ (lift_set i (B <*> UNIV))) = \
-\ (F i : (A <*> UNIV) co (B <*> UNIV))";
-by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
-by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [lift_constrains]) 1);
-by (blast_tac (claset() addIs [constrains_imp_lift_constrains]) 1);
-qed "PLam_constrains";
-
-Goal "[| i : I; ALL j. F j : preserves snd |] \
-\ ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = \
-\ (F i : stable (A <*> UNIV))";
-by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
-qed "PLam_stable";
-
-Goal "i : I ==> \
-\ PLam I F : transient A = (EX i:I. lift i (F i) : transient A)";
-by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
-qed "PLam_transient";
-
-(*This holds because the F j cannot change (lift_set i)*)
-Goal "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV); \
-\ ALL j. F j : preserves snd |] ==> \
-\ PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)";
-by (auto_tac (claset(),
- simpset() addsimps [ensures_def, PLam_constrains, PLam_transient,
- lift_transient_eq_disj,
- lift_set_Un_distrib RS sym,
- lift_set_Diff_distrib RS sym,
- Times_Un_distrib1 RS sym,
- Times_Diff_distrib1 RS sym]));
-qed "PLam_ensures";
-
-Goal "[| i : I; \
-\ F i : ((A <*> UNIV) - (B <*> UNIV)) co \
-\ ((A <*> UNIV) Un (B <*> UNIV)); \
-\ F i : transient ((A <*> UNIV) - (B <*> UNIV)); \
-\ ALL j. F j : preserves snd |] ==> \
-\ PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)";
-by (rtac (PLam_ensures RS leadsTo_Basis) 1);
-by (rtac ensuresI 2);
-by (ALLGOALS assume_tac);
-qed "PLam_leadsTo_Basis";
-
-
-(** invariant **)
-
-Goal "[| F i : invariant (A <*> UNIV); i : I; \
-\ ALL j. F j : preserves snd |] \
-\ ==> PLam I F : invariant (lift_set i (A <*> UNIV))";
-by (auto_tac (claset(),
- simpset() addsimps [PLam_stable, invariant_def]));
-qed "invariant_imp_PLam_invariant";
-
-
-Goal "ALL j. F j : preserves snd \
-\ ==> (PLam I F : preserves (v o sub j o fst)) = \
-\ (if j: I then F j : preserves (v o fst) else True)";
-by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1);
-qed "PLam_preserves_fst";
-Addsimps [PLam_preserves_fst];
-
-Goal "ALL j. F j : preserves snd ==> PLam I F : preserves snd";
-by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_snd_I]) 1);
-qed "PLam_preserves_snd";
-Addsimps [PLam_preserves_snd];
-AddIs [PLam_preserves_snd];
-
-
-(*** guarantees properties ***)
-
-(*This rule looks unsatisfactory because it refers to "lift". One must use
- lift_guarantees_eq_lift_inv to rewrite the first subgoal and
- something like lift_preserves_sub to rewrite the third. However there's
- no obvious way to alternative for the third premise.*)
-Goalw [PLam_def]
- "[| lift i (F i): X guarantees Y; i : I; \
-\ OK I (%i. lift i (F i)) |] \
-\ ==> (PLam I F) : X guarantees Y";
-by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
-qed "guarantees_PLam_I";
-
-Goal "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))";
-by (simp_tac (simpset() addsimps [PLam_def]) 1);
-qed "Allowed_PLam";
-Addsimps [Allowed_PLam];
-
-Goal "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))";
-by (simp_tac (simpset() addsimps [PLam_def, lift_def, rename_preserves]) 1);
-qed "PLam_preserves";
-Addsimps [PLam_preserves];
-
-(**UNUSED
- (*The f0 premise ensures that the product is well-defined.*)
- Goal "[| PLam I F : invariant (lift_set i A); i : I; \
- \ f0: Init (PLam I F) |] ==> F i : invariant A";
- by (auto_tac (claset(),
- simpset() addsimps [invariant_def]));
- by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
- by Auto_tac;
- qed "PLam_invariant_imp_invariant";
-
- Goal "[| i : I; f0: Init (PLam I F) |] \
- \ ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)";
- by (blast_tac (claset() addIs [invariant_imp_PLam_invariant,
- PLam_invariant_imp_invariant]) 1);
- qed "PLam_invariant";
-
- (*The f0 premise isn't needed if F is a constant program because then
- we get an initial state by replicating that of F*)
- Goal "i : I \
- \ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
- by (auto_tac (claset(),
- simpset() addsimps [invariant_def]));
- qed "const_PLam_invariant";
-**)
-
-
-(**UNUSED
- (** Reachability **)
-
- Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)";
- by (etac reachable.induct 1);
- by (auto_tac (claset() addIs reachable.intrs, simpset()));
- qed "reachable_PLam";
-
- (*Result to justify a re-organization of this file*)
- Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
- by Auto_tac;
- result();
-
- Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
- by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
- qed "reachable_PLam_subset1";
-
- (*simplify using reachable_lift??*)
- Goal "[| i ~: I; A : reachable (F i) |] \
- \ ==> ALL f. f : reachable (PLam I F) \
- \ --> f(i:=A) : reachable (lift i (F i) Join PLam I F)";
- by (etac reachable.induct 1);
- by (ALLGOALS Clarify_tac);
- by (etac reachable.induct 1);
- (*Init, Init case*)
- by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
- (*Init of F, action of PLam F case*)
- by (res_inst_tac [("act","act")] reachable.Acts 1);
- by (Force_tac 1);
- by (assume_tac 1);
- by (force_tac (claset() addIs [ext], simpset()) 1);
- (*induction over the 2nd "reachable" assumption*)
- by (eres_inst_tac [("xa","f")] reachable.induct 1);
- (*Init of PLam F, action of F case*)
- by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1);
- by (Force_tac 1);
- by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
- by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
- (*last case: an action of PLam I F*)
- by (res_inst_tac [("act","acta")] reachable.Acts 1);
- by (Force_tac 1);
- by (assume_tac 1);
- by (force_tac (claset() addIs [ext], simpset()) 1);
- qed_spec_mp "reachable_lift_Join_PLam";
-
-
- (*The index set must be finite: otherwise infinitely many copies of F can
- perform actions, and PLam can never catch up in finite time.*)
- Goal "finite I \
- \ ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)";
- by (etac finite_induct 1);
- by (Simp_tac 1);
- by (force_tac (claset() addDs [reachable_lift_Join_PLam],
- simpset() addsimps [PLam_insert]) 1);
- qed "reachable_PLam_subset2";
-
- Goal "finite I ==> \
- \ reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))";
- by (REPEAT_FIRST (ares_tac [equalityI,
- reachable_PLam_subset1,
- reachable_PLam_subset2]));
- qed "reachable_PLam_eq";
-
-
- (** Co **)
-
- Goal "[| F i : A Co B; i: I; finite I |] \
- \ ==> PLam I F : (lift_set i A) Co (lift_set i B)";
- by (auto_tac
- (claset(),
- simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
- reachable_PLam_eq]));
- by (auto_tac (claset(),
- simpset() addsimps [constrains_def, PLam_def]));
- by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
- qed "Constrains_imp_PLam_Constrains";
-
-
-
- Goal "[| i: I; finite I; f0: Init (PLam I F) |] \
- \ ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = \
- \ (F i : A Co B)";
- by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains,
- PLam_Constrains_imp_Constrains]) 1);
- qed "PLam_Constrains";
-
- Goal "[| i: I; finite I; f0: Init (PLam I F) |] \
- \ ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)";
- by (asm_simp_tac (simpset() delsimps [Init_PLam]
- addsimps [Stable_def, PLam_Constrains]) 1);
- qed "PLam_Stable";
-
-
- (** const_PLam (no dependence on i) doesn't require the f0 premise **)
-
- Goal "[| i: I; finite I |] \
- \ ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = \
- \ (F : A Co B)";
- by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains,
- const_PLam_Constrains_imp_Constrains]) 1);
- qed "const_PLam_Constrains";
-
- Goal "[| i: I; finite I |] \
- \ ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
- by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1);
- qed "const_PLam_Stable";
-
- Goalw [Increasing_def]
- "[| i: I; finite I |] \
- \ ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
- by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
- by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
- by (asm_full_simp_tac
- (simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
- qed "const_PLam_Increasing";
-**)
-
--- a/src/HOL/UNITY/PPROD.thy Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/PPROD.thy Fri Jan 24 18:13:59 2003 +0100
@@ -5,9 +5,11 @@
Abstraction over replicated components (PLam)
General products of programs (Pi operation)
+
+Some dead wood here!
*)
-PPROD = Lift_prog +
+theory PPROD = Lift_prog:
constdefs
@@ -16,9 +18,258 @@
"PLam I F == JN i:I. lift i (F i)"
syntax
- "@PLam" :: [pttrn, nat set, 'b set] => (nat => 'b) set ("(3plam _:_./ _)" 10)
+ "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
+ ("(3plam _:_./ _)" 10)
translations
"plam x:A. B" == "PLam A (%x. B)"
+
+(*** Basic properties ***)
+
+lemma Init_PLam: "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"
+apply (simp (no_asm) add: PLam_def lift_def lift_set_def)
+done
+
+declare Init_PLam [simp]
+
+lemma PLam_empty: "PLam {} F = SKIP"
+apply (simp (no_asm) add: PLam_def)
+done
+
+lemma PLam_SKIP: "(plam i: I. SKIP) = SKIP"
+apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant)
+done
+
+declare PLam_SKIP [simp] PLam_empty [simp]
+
+lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
+by (unfold PLam_def, auto)
+
+lemma PLam_component_iff: "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)"
+apply (simp (no_asm) add: PLam_def JN_component_iff)
+done
+
+lemma component_PLam: "i : I ==> lift i (F i) <= (PLam I F)"
+apply (unfold PLam_def)
+(*blast_tac doesn't use HO unification*)
+apply (fast intro: component_JN)
+done
+
+
+(** Safety & Progress: but are they used anywhere? **)
+
+lemma PLam_constrains: "[| i : I; ALL j. F j : preserves snd |] ==>
+ (PLam I F : (lift_set i (A <*> UNIV)) co
+ (lift_set i (B <*> UNIV))) =
+ (F i : (A <*> UNIV) co (B <*> UNIV))"
+apply (simp (no_asm_simp) add: PLam_def JN_constrains)
+apply (subst insert_Diff [symmetric], assumption)
+apply (simp (no_asm_simp) add: lift_constrains)
+apply (blast intro: constrains_imp_lift_constrains)
+done
+
+lemma PLam_stable: "[| i : I; ALL j. F j : preserves snd |]
+ ==> (PLam I F : stable (lift_set i (A <*> UNIV))) =
+ (F i : stable (A <*> UNIV))"
+apply (simp (no_asm_simp) add: stable_def PLam_constrains)
+done
+
+lemma PLam_transient: "i : I ==>
+ PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"
+apply (simp (no_asm_simp) add: JN_transient PLam_def)
+done
+
+(*This holds because the F j cannot change (lift_set i)*)
+lemma PLam_ensures: "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV);
+ ALL j. F j : preserves snd |] ==>
+ PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
+apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
+done
+
+lemma PLam_leadsTo_Basis: "[| i : I;
+ F i : ((A <*> UNIV) - (B <*> UNIV)) co
+ ((A <*> UNIV) Un (B <*> UNIV));
+ F i : transient ((A <*> UNIV) - (B <*> UNIV));
+ ALL j. F j : preserves snd |] ==>
+ PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
+by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
+
+
+
+(** invariant **)
+
+lemma invariant_imp_PLam_invariant: "[| F i : invariant (A <*> UNIV); i : I;
+ ALL j. F j : preserves snd |]
+ ==> PLam I F : invariant (lift_set i (A <*> UNIV))"
+by (auto simp add: PLam_stable invariant_def)
+
+
+lemma PLam_preserves_fst [simp]:
+ "ALL j. F j : preserves snd
+ ==> (PLam I F : preserves (v o sub j o fst)) =
+ (if j: I then F j : preserves (v o fst) else True)"
+by (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
+
+lemma PLam_preserves_snd [simp,intro]:
+ "ALL j. F j : preserves snd ==> PLam I F : preserves snd"
+by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
+
+
+
+(*** guarantees properties ***)
+
+(*This rule looks unsatisfactory because it refers to "lift". One must use
+ lift_guarantees_eq_lift_inv to rewrite the first subgoal and
+ something like lift_preserves_sub to rewrite the third. However there's
+ no obvious way to alternative for the third premise.*)
+lemma guarantees_PLam_I:
+ "[| lift i (F i): X guarantees Y; i : I;
+ OK I (%i. lift i (F i)) |]
+ ==> (PLam I F) : X guarantees Y"
+apply (unfold PLam_def)
+apply (simp (no_asm_simp) add: guarantees_JN_I)
+done
+
+lemma Allowed_PLam [simp]:
+ "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))"
+by (simp (no_asm) add: PLam_def)
+
+
+lemma PLam_preserves [simp]:
+ "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))"
+by (simp (no_asm) add: PLam_def lift_def rename_preserves)
+
+
+(**UNUSED
+ (*The f0 premise ensures that the product is well-defined.*)
+ lemma PLam_invariant_imp_invariant: "[| PLam I F : invariant (lift_set i A); i : I;
+ f0: Init (PLam I F) |] ==> F i : invariant A"
+ apply (auto simp add: invariant_def)
+ apply (drule_tac c = "f0 (i:=x) " in subsetD)
+ apply auto
+ done
+
+ lemma PLam_invariant: "[| i : I; f0: Init (PLam I F) |]
+ ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"
+ apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
+ done
+
+ (*The f0 premise isn't needed if F is a constant program because then
+ we get an initial state by replicating that of F*)
+ lemma reachable_PLam: "i : I
+ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"
+ apply (auto simp add: invariant_def)
+ done
+**)
+
+
+(**UNUSED
+ (** Reachability **)
+
+ Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)"
+ apply (erule reachable.induct)
+ apply (auto intro: reachable.intrs)
+ done
+
+ (*Result to justify a re-organization of this file*)
+ lemma ??unknown??: "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
+ apply auto
+ result()
+
+ lemma reachable_PLam_subset1: "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
+ apply (force dest!: reachable_PLam)
+ done
+
+ (*simplify using reachable_lift??*)
+ lemma reachable_lift_Join_PLam [rule_format (no_asm)]: "[| i ~: I; A : reachable (F i) |]
+ ==> ALL f. f : reachable (PLam I F)
+ --> f(i:=A) : reachable (lift i (F i) Join PLam I F)"
+ apply (erule reachable.induct)
+ apply (ALLGOALS Clarify_tac)
+ apply (erule reachable.induct)
+ (*Init, Init case*)
+ apply (force intro: reachable.intrs)
+ (*Init of F, action of PLam F case*)
+ apply (rule_tac act = act in reachable.Acts)
+ apply force
+ apply assumption
+ apply (force intro: ext)
+ (*induction over the 2nd "reachable" assumption*)
+ apply (erule_tac xa = f in reachable.induct)
+ (*Init of PLam F, action of F case*)
+ apply (rule_tac act = "lift_act i act" in reachable.Acts)
+ apply force
+ apply (force intro: reachable.Init)
+ apply (force intro: ext simp add: lift_act_def)
+ (*last case: an action of PLam I F*)
+ apply (rule_tac act = acta in reachable.Acts)
+ apply force
+ apply assumption
+ apply (force intro: ext)
+ done
+
+
+ (*The index set must be finite: otherwise infinitely many copies of F can
+ perform actions, and PLam can never catch up in finite time.*)
+ lemma reachable_PLam_subset2: "finite I
+ ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"
+ apply (erule finite_induct)
+ apply (simp (no_asm))
+ apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
+ done
+
+ lemma reachable_PLam_eq: "finite I ==>
+ reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"
+ apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
+ done
+
+
+ (** Co **)
+
+ lemma Constrains_imp_PLam_Constrains: "[| F i : A Co B; i: I; finite I |]
+ ==> PLam I F : (lift_set i A) Co (lift_set i B)"
+ apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
+ apply (auto simp add: constrains_def PLam_def)
+ apply (REPEAT (blast intro: reachable.intrs))
+ done
+
+
+
+ lemma PLam_Constrains: "[| i: I; finite I; f0: Init (PLam I F) |]
+ ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =
+ (F i : A Co B)"
+ apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
+ done
+
+ lemma PLam_Stable: "[| i: I; finite I; f0: Init (PLam I F) |]
+ ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"
+ apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
+ done
+
+
+ (** const_PLam (no dependence on i) doesn't require the f0 premise **)
+
+ lemma const_PLam_Constrains: "[| i: I; finite I |]
+ ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =
+ (F : A Co B)"
+ apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
+ done
+
+ lemma const_PLam_Stable: "[| i: I; finite I |]
+ ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"
+ apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
+ done
+
+ lemma const_PLam_Increasing:
+ "[| i: I; finite I |]
+ ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"
+ apply (unfold Increasing_def)
+ apply (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}")
+ apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
+ apply (simp add: finite_lessThan const_PLam_Stable)
+ done
+**)
+
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY_Main.thy Fri Jan 24 18:13:59 2003 +0100
@@ -0,0 +1,27 @@
+(* Title: HOL/UNITY/UNITY_Main.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2003 University of Cambridge
+
+Inclusive UNITY theory
+*)
+
+theory UNITY_Main = Detects + PPROD + Follows
+files "UNITY_tactics.ML":
+
+method_setup constrains = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_constrains_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1)) *}
+ "for proving safety properties"
+
+method_setup ensures_tac = {*
+ fn args => fn ctxt =>
+ Method.goal_args' (Scan.lift Args.name)
+ (gen_ensures_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt))
+ args ctxt *}
+ "for proving progress properties"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Jan 24 18:13:59 2003 +0100
@@ -0,0 +1,145 @@
+(* Title: HOL/UNITY/UNITY_tactics.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2003 University of Cambridge
+
+Specialized UNITY tactics, and ML bindings of theorems
+*)
+
+
+(*Lift_prog*)
+val sub_def = thm "sub_def";
+val lift_map_def = thm "lift_map_def";
+val drop_map_def = thm "drop_map_def";
+val insert_map_inverse = thm "insert_map_inverse";
+val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
+val insert_map_inject1 = thm "insert_map_inject1";
+val insert_map_inject2 = thm "insert_map_inject2";
+val insert_map_inject = thm "insert_map_inject";
+val insert_map_inject = thm "insert_map_inject";
+val lift_map_eq_iff = thm "lift_map_eq_iff";
+val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
+val inj_lift_map = thm "inj_lift_map";
+val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
+val drop_map_inject = thm "drop_map_inject";
+val surj_lift_map = thm "surj_lift_map";
+val bij_lift_map = thm "bij_lift_map";
+val inv_lift_map_eq = thm "inv_lift_map_eq";
+val inv_drop_map_eq = thm "inv_drop_map_eq";
+val bij_drop_map = thm "bij_drop_map";
+val sub_apply = thm "sub_apply";
+val lift_set_empty = thm "lift_set_empty";
+val lift_set_iff = thm "lift_set_iff";
+val lift_set_iff2 = thm "lift_set_iff2";
+val lift_set_mono = thm "lift_set_mono";
+val lift_set_Un_distrib = thm "lift_set_Un_distrib";
+val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
+val bij_lift = thm "bij_lift";
+val lift_SKIP = thm "lift_SKIP";
+val lift_Join = thm "lift_Join";
+val lift_JN = thm "lift_JN";
+val lift_constrains = thm "lift_constrains";
+val lift_stable = thm "lift_stable";
+val lift_invariant = thm "lift_invariant";
+val lift_Constrains = thm "lift_Constrains";
+val lift_Stable = thm "lift_Stable";
+val lift_Always = thm "lift_Always";
+val lift_transient = thm "lift_transient";
+val lift_ensures = thm "lift_ensures";
+val lift_leadsTo = thm "lift_leadsTo";
+val lift_LeadsTo = thm "lift_LeadsTo";
+val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
+val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
+val lift_preserves_snd_I = thm "lift_preserves_snd_I";
+val delete_map_eqE = thm "delete_map_eqE";
+val delete_map_eqE = thm "delete_map_eqE";
+val delete_map_neq_apply = thm "delete_map_neq_apply";
+val vimage_o_fst_eq = thm "vimage_o_fst_eq";
+val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
+val mem_lift_act_iff = thm "mem_lift_act_iff";
+val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
+val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
+val insert_map_upd_same = thm "insert_map_upd_same";
+val insert_map_upd = thm "insert_map_upd";
+val insert_map_eq_diff = thm "insert_map_eq_diff";
+val lift_map_eq_diff = thm "lift_map_eq_diff";
+val lift_transient_eq_disj = thm "lift_transient_eq_disj";
+val lift_map_image_Times = thm "lift_map_image_Times";
+val lift_preserves_eq = thm "lift_preserves_eq";
+val lift_preserves_sub = thm "lift_preserves_sub";
+val o_equiv_assoc = thm "o_equiv_assoc";
+val o_equiv_apply = thm "o_equiv_apply";
+val fst_o_lift_map = thm "fst_o_lift_map";
+val snd_o_lift_map = thm "snd_o_lift_map";
+val extend_act_extend_act = thm "extend_act_extend_act";
+val project_act_project_act = thm "project_act_project_act";
+val project_act_extend_act = thm "project_act_extend_act";
+val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
+val UNION_OK_lift_I = thm "UNION_OK_lift_I";
+val OK_lift_I = thm "OK_lift_I";
+val Allowed_lift = thm "Allowed_lift";
+val lift_image_preserves = thm "lift_image_preserves";
+
+
+(*PPROD*)
+val Init_PLam = thm "Init_PLam";
+val PLam_empty = thm "PLam_empty";
+val PLam_SKIP = thm "PLam_SKIP";
+val PLam_insert = thm "PLam_insert";
+val PLam_component_iff = thm "PLam_component_iff";
+val component_PLam = thm "component_PLam";
+val PLam_constrains = thm "PLam_constrains";
+val PLam_stable = thm "PLam_stable";
+val PLam_transient = thm "PLam_transient";
+val PLam_ensures = thm "PLam_ensures";
+val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
+val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
+val PLam_preserves_fst = thm "PLam_preserves_fst";
+val PLam_preserves_snd = thm "PLam_preserves_snd";
+val guarantees_PLam_I = thm "guarantees_PLam_I";
+val Allowed_PLam = thm "Allowed_PLam";
+val PLam_preserves = thm "PLam_preserves";
+
+
+(*proves "co" properties when the program is specified*)
+fun gen_constrains_tac(cs,ss) 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 ss 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac cs),
+ ALLGOALS (asm_lr_simp_tac ss)]) i;
+
+(*proves "ensures/leadsTo" properties when the program is specified*)
+fun gen_ensures_tac(cs,ss) 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 ss 2,
+ res_inst_tac [("act", sact)] transientI 2,
+ (*simplify the command's domain*)
+ simp_tac (ss addsimps [Domain_def]) 3,
+ gen_constrains_tac (cs,ss) 1,
+ ALLGOALS (clarify_tac cs),
+ ALLGOALS (asm_lr_simp_tac ss)]);
+
+
+(*Composition equivalences, from Lift_prog*)
+
+fun make_o_equivs th =
+ [th,
+ th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
+ th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
+
+Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
+
+Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);