--- a/src/HOL/Relation.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/Relation.thy Sat Feb 08 16:05:33 2003 +0100
@@ -86,6 +86,9 @@
subsection {* Diagonal: identity over a set *}
+lemma diag_empty [simp]: "diag {} = {}"
+ by (simp add: diag_def)
+
lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
by (simp add: diag_def)
@@ -318,6 +321,9 @@
lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B"
by blast
+lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
+ by blast
+
lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
--- a/src/HOL/UNITY/Comp.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy Sat Feb 08 16:05:33 2003 +0100
@@ -185,7 +185,7 @@
"[| F \<in> stable {s. P (v s) (w s)};
G \<in> preserves v; G \<in> preserves w |]
==> F Join G \<in> stable {s. P (v s) (w s)}"
-apply (simp)
+apply simp
apply (subgoal_tac "G \<in> preserves (funPair v w) ")
prefer 2 apply simp
apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
--- a/src/HOL/UNITY/Comp/Client.ML Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Client.ML Sat Feb 08 16:05:33 2003 +0100
@@ -14,7 +14,7 @@
\ (G : preserves rel & G : preserves ask & G : preserves tok &\
\ Client : Allowed G)";
by (auto_tac (claset(),
- simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));
+ simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed]));
qed "Client_ok_iff";
AddIffs [Client_ok_iff];
@@ -79,7 +79,8 @@
qed "Join_Always_rel_le_giv";
Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
-by (res_inst_tac [("act", "rel_act")] transientI 1);
+by (simp_tac (simpset() addsimps [Client_def, mk_total_program_def]) 1);
+by (res_inst_tac [("act", "rel_act")] totalize_transientI 1);
by (auto_tac (claset(),
simpset() addsimps [Domain_def, Client_def]));
by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
--- a/src/HOL/UNITY/Comp/Client.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Client.thy Sat Feb 08 16:05:33 2003 +0100
@@ -30,10 +30,10 @@
rel_act :: "('a state_d * 'a state_d) set"
"rel_act == {(s,s').
- EX nrel. nrel = size (rel s) &
- s' = s (| rel := rel s @ [giv s!nrel] |) &
- nrel < size (giv s) &
- ask s!nrel <= giv s!nrel}"
+ \\<exists>nrel. nrel = size (rel s) &
+ s' = s (| rel := rel s @ [giv s!nrel] |) &
+ nrel < size (giv s) &
+ ask s!nrel <= giv s!nrel}"
(** Choose a new token requirement **)
@@ -49,10 +49,11 @@
Client :: 'a state_d program
"Client ==
- mk_program ({s. tok s : atMost NbT &
- giv s = [] & ask s = [] & rel s = []},
- {rel_act, tok_act, ask_act},
- UN G: preserves rel Int preserves ask Int preserves tok.
+ mk_total_program
+ ({s. tok s : atMost NbT &
+ giv s = [] & ask s = [] & rel s = []},
+ {rel_act, tok_act, ask_act},
+ \\<Union>G \\<in> preserves rel Int preserves ask Int preserves tok.
Acts G)"
(*Maybe want a special theory section to declare such maps*)
--- a/src/HOL/UNITY/Comp/Counter.ML Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counter.ML Sat Feb 08 16:05:33 2003 +0100
@@ -11,11 +11,10 @@
Spriner LNCS 1586 (1999), pages 1215-1227.
*)
-Addsimps [Component_def RS def_prg_Init];
-Addsimps (map simp_of_act [a_def]);
+Addsimps [Component_def RS def_prg_Init, simp_of_act a_def];
(* Theorems about sum and sumj *)
-Goal "ALL n. I<n --> sum I (s(c n := x)) = sum I s";
+Goal "\\<forall>n. I<n --> sum I (s(c n := x)) = sum I s";
by (induct_tac "I" 1);
by Auto_tac;
qed_spec_mp "sum_upd_gt";
@@ -47,7 +46,7 @@
addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
qed "sumj_upd_C";
-Goal "ALL i. I<i--> (sumj I i s = sum I s)";
+Goal "\\<forall>i. I<i--> (sumj I i s = sum I s)";
by (induct_tac "I" 1);
by Auto_tac;
qed_spec_mp "sumj_sum_gt";
@@ -58,49 +57,49 @@
by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
qed "sumj_sum_eq";
-Goal "ALL i. i<I-->(sum I s = s (c i) + sumj I i s)";
+Goal "\\<forall>i. i<I-->(sum I s = s (c i) + sumj I i s)";
by (induct_tac "I" 1);
by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq]));
qed_spec_mp "sum_sumj";
(* Correctness proofs for Components *)
(* p2 and p3 proofs *)
-Goal "Component i : stable {s. s C = s (c i) + k}";
+Goal "Component i \\<in> stable {s. s C = s (c i) + k}";
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "p2";
-Goal "Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
+Goal "Component i \\<in> stable {s. \\<forall>v. v~=c i & v~=C --> s v = k v}";
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "p3";
Goal
-"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \
-\ Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \
-\ = (Component i: stable {s. s C = s (c i) + sumj I i s})";
+"(\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} \
+\ \\<inter> {s. \\<forall>v. v~=c i & v~=C --> s v = k v})) \
+\ = (Component i \\<in> stable {s. s C = s (c i) + sumj I i s})";
+by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1);
by (auto_tac (claset(), simpset()
- addsimps [constrains_def, stable_def,Component_def,
- sumj_upd_C, sumj_upd_ci]));
+ addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci]));
qed "p2_p3_lemma1";
Goal
-"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \
-\ {s. ALL v. v~=c i & v~=C --> s v = k v})";
+"\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} Int \
+\ {s. \\<forall>v. v~=c i & v~=C --> s v = k v})";
by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
qed "p2_p3_lemma2";
Goal
-"Component i: stable {s. s C = s (c i) + sumj I i s}";
+"Component i \\<in> stable {s. s C = s (c i) + sumj I i s}";
by (auto_tac (claset() addSIs [p2_p3_lemma2],
simpset() addsimps [p2_p3_lemma1 RS sym]));
qed "p2_p3";
(* Compositional Proof *)
-Goal "(ALL i. i < I --> s (c i) = 0) --> sum I s = 0";
+Goal "(\\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0";
by (induct_tac "I" 1);
by Auto_tac;
qed "sum_0'";
@@ -108,33 +107,7 @@
(* I could'nt be empty *)
Goalw [invariant_def]
-"!!I. 0<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
-by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
+"!!I. 0<I ==> (\\<Squnion>i \\<in> {i. i<I}. Component i) \\<in> invariant {s. s C = sum I s}";
+by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1);
by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
qed "safety";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/HOL/UNITY/Comp/Counter.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counter.thy Sat Feb 08 16:05:33 2003 +0100
@@ -37,6 +37,7 @@
Component :: "nat => state program"
"Component i ==
- mk_program({s. s C = 0 & s (c i) = 0}, {a i},
- UN G: preserves (%s. s (c i)). Acts G)"
+ mk_total_program({s. s C = 0 & s (c i) = 0}, {a i},
+ \\<Union>G \\<in> preserves (%s. s (c i)). Acts G)"
+
end
--- a/src/HOL/UNITY/Comp/Counterc.ML Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.ML Sat Feb 08 16:05:33 2003 +0100
@@ -12,11 +12,11 @@
*)
Addsimps [Component_def RS def_prg_Init,
-Component_def RS def_prg_AllowedActs];
-Addsimps (map simp_of_act [a_def]);
+ Component_def RS def_prg_AllowedActs,
+ simp_of_act a_def];
(* Theorems about sum and sumj *)
-Goal "ALL i. I<i--> (sum I s = sumj I i s)";
+Goal "\\<forall>i. I<i--> (sum I s = sumj I i s)";
by (induct_tac "I" 1);
by Auto_tac;
qed_spec_mp "sum_sumj_eq1";
@@ -26,18 +26,18 @@
by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1]));
qed_spec_mp "sum_sumj_eq2";
-Goal "(ALL i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
+Goal "(\\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
by (induct_tac "I" 1 THEN Auto_tac);
qed_spec_mp "sum_ext";
-Goal "(ALL j. j<I & j~=i --> c s' j = c s j) --> (sumj I i s' = sumj I i s)";
+Goal "(\\<forall>j. j<I & j~=i --> c s' j = c s j) --> (sumj I i s' = sumj I i s)";
by (induct_tac "I" 1);
by Safe_tac;
by (auto_tac (claset() addSIs [sum_ext], simpset()));
qed_spec_mp "sumj_ext";
-Goal "(ALL i. i<I --> c s i = 0) --> sum I s = 0";
+Goal "(\\<forall>i. i<I --> c s i = 0) --> sum I s = 0";
by (induct_tac "I" 1);
by Auto_tac;
qed "sum0";
@@ -46,22 +46,24 @@
(* Safety properties for Components *)
Goal "(Component i ok G) = \
-\ (G: preserves (%s. c s i) & Component i:Allowed G)";
+\ (G \\<in> preserves (%s. c s i) & Component i \\<in> Allowed G)";
by (auto_tac (claset(),
- simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed]));
+ simpset() addsimps [ok_iff_Allowed, Component_def RS def_total_prg_Allowed]));
qed "Component_ok_iff";
AddIffs [Component_ok_iff];
AddIffs [OK_iff_ok];
Addsimps [preserves_def];
-Goal "Component i: stable {s. C s = (c s) i + k}";
+Goal "Component i \\<in> stable {s. C s = (c s) i + k}";
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "p2";
-Goal "[| OK I Component; i:I |] \
-\ ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}";
+Goal "[| OK I Component; i\\<in>I |] \
+\ ==> Component i \\<in> stable {s. \\<forall>j\\<in>I. j~=i --> c s j = c k j}";
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (rewrite_goals_tac [Component_def, mk_total_program_def]);
by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1);
by (Blast_tac 1);
qed "p3";
@@ -69,22 +71,22 @@
Goal
"[| OK {i. i<I} Component; i<I |] ==> \
-\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \
-\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})";
+\ \\<forall>k. Component i \\<in> stable ({s. C s = c s i + sumj I i k} Int \
+\ {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j})";
by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
qed "p2_p3_lemma1";
-Goal "(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \
-\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})) \
-\ ==> (F:stable {s. C s = c s i + sumj I i s})";
+Goal "(\\<forall>k. F\\<in>stable ({s. C s = (c s) i + sumj I i k} Int \
+\ {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j})) \
+\ ==> (F\\<in>stable {s. C s = c s i + sumj I i s})";
by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1);
by (force_tac (claset() addSIs [sumj_ext], simpset()) 1);
qed "p2_p3_lemma2";
Goal "[| OK {i. i<I} Component; i<I |] \
-\ ==> Component i: stable {s. C s = c s i + sumj I i s}";
+\ ==> Component i \\<in> stable {s. C s = c s i + sumj I i s}";
by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1);
qed "p2_p3";
@@ -92,7 +94,7 @@
(* Compositional correctness *)
Goalw [invariant_def]
"[| 0<I; OK {i. i<I} Component |] \
-\ ==> (JN i:{i. i<I}. (Component i)) : invariant {s. C s = sum I s}";
+\ ==> (\\<Squnion>i\\<in>{i. i<I}. (Component i)) \\<in> invariant {s. C s = sum I s}";
by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3],
simpset()));
--- a/src/HOL/UNITY/Comp/Counterc.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.thy Sat Feb 08 16:05:33 2003 +0100
@@ -39,6 +39,7 @@
"a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
Component :: "nat => state program"
- "Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i},
- UN G: preserves (%s. (c s) i). Acts G)"
+ "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
+ {a i},
+ \\<Union>G \\<in> preserves (%s. (c s) i). Acts G)"
end
--- a/src/HOL/UNITY/Comp/Handshake.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Handshake.thy Sat Feb 08 16:05:33 2003 +0100
@@ -21,14 +21,14 @@
"cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
F :: "state program"
- "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
+ "F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
(*G's program*)
cmdG :: "(state*state) set"
"cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
G :: "state program"
- "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
+ "G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
(*the joint invariant*)
invFG :: "state set"
--- a/src/HOL/UNITY/Comp/Priority.ML Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Priority.ML Sat Feb 08 16:05:33 2003 +0100
@@ -77,7 +77,7 @@
(* property 13: universal *)
Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
-by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
by (constrains_tac 1);
by (Blast_tac 1);
qed "p13";
@@ -88,16 +88,15 @@
"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
by (Clarify_tac 1);
by (cut_inst_tac [("i", "j")] reach_lemma 1);
-by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
by (constrains_tac 1);
by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
qed "above_not_increase";
-Goal
-"system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
+Goal "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
by (cut_inst_tac [("i", "i")] above_not_increase 1);
-by (asm_full_simp_tac (simpset() addsimps
- [trancl_converse, constrains_def]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [trancl_converse, constrains_def]) 1);
by (Blast_tac 1);
qed "above_not_increase'";
@@ -106,7 +105,7 @@
(* p15: universal property: all Components well behave *)
Goal "ALL i. system: Highest i co Highest i Un Lowest i";
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
by (constrains_tac 1);
by Auto_tac;
qed "system_well_behaves";
@@ -147,9 +146,9 @@
(* propert 5: existential property *)
Goal "system: Highest i leadsTo Lowest i";
-by (asm_full_simp_tac (simpset() addsimps [system_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
by (ensures_tac "act i" 1);
-by (auto_tac (claset(), simpset() addsimps [Component_def]));
+by Auto_tac;
qed "Highest_leadsTo_Lowest";
(* a lowest i can never be in any abover set *)
--- a/src/HOL/UNITY/Comp/Priority.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/Priority.thy Sat Feb 08 16:05:33 2003 +0100
@@ -35,7 +35,7 @@
(* All components start with the same initial state *)
Component :: "vertex=>state program"
- "Component i == mk_program({init}, {act i}, UNIV)"
+ "Component i == mk_total_program({init}, {act i}, UNIV)"
(* Abbreviations *)
Highest :: "vertex=>state set"
--- a/src/HOL/UNITY/Comp/TimerArray.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Sat Feb 08 16:05:33 2003 +0100
@@ -18,7 +18,7 @@
"decr == UN n uu. {((Suc n, uu), (n,uu))}"
Timer :: "'a state program"
- "Timer == mk_program (UNIV, {decr}, UNIV)"
+ "Timer == mk_total_program (UNIV, {decr}, UNIV)"
declare Timer_def [THEN def_prg_Init, simp]
@@ -61,8 +61,8 @@
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)
+apply (unfold Timer_def mk_total_program_def, constrains)
+apply (rule_tac act = decr in totalize_transientI, auto)
done
end
--- a/src/HOL/UNITY/Constrains.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Constrains.thy Sat Feb 08 16:05:33 2003 +0100
@@ -55,7 +55,7 @@
subsection{*traces and reachable*}
lemma reachable_equiv_traces:
- "reachable F = {s. \<exists>evs. (s,evs): traces (Init F) (Acts F)}"
+ "reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}"
apply safe
apply (erule_tac [2] traces.induct)
apply (erule reachable.induct)
@@ -392,4 +392,35 @@
used by Always_Int_I) *)
lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
+
+subsection{*Totalize*}
+
+lemma reachable_imp_reachable_tot:
+ "s \<in> reachable F ==> s \<in> reachable (totalize F)"
+apply (erule reachable.induct)
+ apply (rule reachable.Init)
+ apply simp
+apply (rule_tac act = "totalize_act act" in reachable.Acts)
+apply (auto simp add: totalize_act_def)
+done
+
+lemma reachable_tot_imp_reachable:
+ "s \<in> reachable (totalize F) ==> s \<in> reachable F"
+apply (erule reachable.induct)
+ apply (rule reachable.Init, simp)
+apply (force simp add: totalize_act_def intro: reachable.Acts)
+done
+
+lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F"
+by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable)
+
+lemma totalize_Constrains_iff [simp]: "(totalize F \<in> A Co B) = (F \<in> A Co B)"
+by (simp add: Constrains_def)
+
+lemma totalize_Stable_iff [simp]: "(totalize F \<in> Stable A) = (F \<in> Stable A)"
+by (simp add: Stable_def)
+
+lemma totalize_Always_iff [simp]: "(totalize F \<in> Always A) = (F \<in> Always A)"
+by (simp add: Always_def)
+
end
--- a/src/HOL/UNITY/Detects.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Detects.thy Sat Feb 08 16:05:33 2003 +0100
@@ -21,7 +21,8 @@
(* Corollary from Sectiom 3.6.4 *)
-lemma Always_at_FP: "F \<in> A LeadsTo B ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
+lemma Always_at_FP:
+ "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
apply (rule LeadsTo_empty)
apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
@@ -36,8 +37,7 @@
apply (unfold Detects_def Int_def)
apply (simp (no_asm))
apply safe
-apply (rule_tac [2] LeadsTo_Trans)
-apply auto
+apply (rule_tac [2] LeadsTo_Trans, auto)
apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
apply (blast intro: Always_weaken)
apply (simp add: Always_Int_distrib)
@@ -49,9 +49,7 @@
done
lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
-apply (unfold Equality_def)
-apply blast
-done
+by (unfold Equality_def, blast)
(*Not quite antisymmetry: sets A and B agree in all reachable states *)
lemma Detects_antisym:
@@ -64,9 +62,9 @@
(* Theorem from Section 3.8 *)
lemma Detects_Always:
- "F \<in> A Detects B ==> F \<in> Always ((-(FP F)) \<union> (A <==> B))"
+ "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
apply (unfold Detects_def Equality_def)
-apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
+apply (simp add: Un_Int_distrib Always_Int_distrib)
apply (blast dest: Always_at_FP intro: Always_weaken)
done
@@ -75,7 +73,7 @@
lemma Detects_Imp_LeadstoEQ:
"F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
apply (unfold Detects_def Equality_def)
-apply (rule_tac B = "B" in LeadsTo_Diff)
+apply (rule_tac B = B in LeadsTo_Diff)
apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
apply (blast intro: Always_LeadsTo_weaken)
done
--- a/src/HOL/UNITY/ELT.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/ELT.thy Sat Feb 08 16:05:33 2003 +0100
@@ -281,22 +281,11 @@
"[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]
==> F : A leadsTo[CC] (B' Un A')"
apply (rule leadsETo_cancel1)
-prefer 2 apply assumption
-apply (simp_all (no_asm_simp))
+ prefer 2 apply assumption
+apply simp_all
done
-(** The impossibility law **)
-
-lemma leadsETo_empty_lemma: "F : A leadsTo[CC] B ==> B={} --> A={}"
-apply (erule leadsETo_induct)
-apply (simp_all (no_asm_simp))
-apply (unfold ensures_def constrains_def transient_def, blast)
-done
-
-lemma leadsETo_empty: "F : A leadsTo[CC] {} ==> A={}"
-by (blast intro!: leadsETo_empty_lemma [THEN mp])
-
(** PSP: Progress-Safety-Progress **)
@@ -367,23 +356,6 @@
apply (blast intro: constrains_Int [THEN constrains_weaken])+
done
-(*useful??*)
-lemma Join_leadsETo_stable_imp_leadsETo:
- "[| F Join G : (A leadsTo[CC] B); ALL C:CC. G : stable C |]
- ==> F: (A leadsTo[CC] B)"
-apply (erule leadsETo_induct)
-prefer 3 apply (blast intro: leadsETo_Union)
-prefer 2 apply (blast intro: leadsETo_Trans)
-apply (rule leadsETo_Basis)
-apply (case_tac "A <= B")
-apply (erule subset_imp_ensures)
-apply (auto intro: constrains_weaken simp add: stable_def ensures_def Join_transient)
-apply (erule_tac V = "?F : ?A co ?B" in thin_rl)+
-apply (erule transientE)
-apply (unfold constrains_def)
-apply (blast dest!: bspec)
-done
-
(**** Relationship with traditional "leadsTo", strong & weak ****)
(** strong **)
@@ -538,18 +510,6 @@
done
-
-(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
-lemma (in Extend)
- "[| G : preserves (v o f); project h C G : transient D;
- D : givenBy v |] ==> D={}"
-apply (rule stable_transient_empty)
- prefer 2 apply assumption
-(*If addIs then PROOF FAILED at depth 2*)
-apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)
-done
-
-
(*This version's stronger in the "ensures" precondition
BUT there's no ensures_weaken_L*)
lemma (in Extend) Join_project_ensures_strong:
@@ -563,20 +523,7 @@
apply (auto simp add: Int_Diff)
done
-(*Generalizes preserves_project_transient_empty*)
-lemma (in Extend) preserves_o_project_transient_empty:
- "[| G : preserves (v o f);
- project h C G : transient (C' Int D);
- project h C G : stable C'; D : givenBy v |]
- ==> C' Int D = {}"
-apply (rule stable_transient_empty)
-prefer 2 apply assumption
-(*Fragile proof. Was just a single blast call.
- If just "intro" then PROOF FAILED at depth 3*)
-apply (rule stable_Int)
- apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)+
-done
-
+(*NOT WORKING. MODIFY AS IN Project.thy
lemma (in Extend) pld_lemma:
"[| extend h F Join G : stable C;
F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;
@@ -596,7 +543,7 @@
prefer 2
apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
apply (rule Join_project_ensures_strong)
-apply (auto dest: preserves_o_project_transient_empty intro: project_stable_project_set simp add: Int_left_absorb)
+apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
done
@@ -652,6 +599,7 @@
apply (unfold extending_def)
apply (blast intro: project_LeadsETo_D)
done
+*)
(*** leadsETo in the precondition ***)
--- a/src/HOL/UNITY/Extend.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Extend.thy Sat Feb 08 16:05:33 2003 +0100
@@ -101,9 +101,6 @@
lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> B)"
by blast
-lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
-by (blast intro: sym [THEN image_eqI])
-
(*Possibly easier than reasoning about "inv h"*)
lemma good_mapI:
assumes surj_h: "surj h"
@@ -338,9 +335,9 @@
-subsection{*extend ****)
+subsection{*extend*}
-(*** Basic properties*}
+text{*Basic properties*}
lemma Init_extend [simp]:
"Init (extend h F) = extend_set h (Init F)"
@@ -453,6 +450,8 @@
lemma (in Extend) project_mono: "F \<le> G ==> project h C F \<le> project h C G"
by (simp add: component_eq_subset, blast)
+lemma (in Extend) all_total_extend: "all_total F ==> all_total (extend h F)"
+by (simp add: all_total_def Domain_extend_act)
subsection{*Safety: co, stable*}
@@ -611,10 +610,7 @@
lemma (in Extend) extend_transient_slice:
"extend h F \<in> transient A ==> F \<in> transient (slice A y)"
-apply (unfold transient_def, auto)
-apply (rule bexI, auto)
-apply (force simp add: extend_act_def)
-done
+by (unfold transient_def, auto)
(*Converse?*)
lemma (in Extend) extend_constrains_slice:
--- a/src/HOL/UNITY/FP.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/FP.thy Sat Feb 08 16:05:33 2003 +0100
@@ -56,4 +56,7 @@
lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
by (simp add: Diff_eq Compl_FP)
+lemma totalize_FP [simp]: "FP (totalize F) = FP F"
+by (simp add: FP_def)
+
end
--- a/src/HOL/UNITY/Follows.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Follows.thy Sat Feb 08 16:05:33 2003 +0100
@@ -62,16 +62,13 @@
subsection{*Destruction rules*}
lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
-apply (unfold Follows_def, blast)
-done
+by (unfold Follows_def, blast)
lemma Follows_Increasing2: "F \<in> f Fols g ==> F \<in> Increasing g"
-apply (unfold Follows_def, blast)
-done
+by (unfold Follows_def, blast)
lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<subseteq> g s}"
-apply (unfold Follows_def, blast)
-done
+by (unfold Follows_def, blast)
lemma Follows_LeadsTo:
"F \<in> f Fols g ==> F \<in> {s. k \<le> g s} LeadsTo {s. k \<le> f s}"
@@ -159,8 +156,7 @@
apply (rule LeadsTo_weaken)
apply (rule PSP_Stable)
apply (erule_tac x = "f s" in spec)
-apply (erule Stable_Int, assumption)
-apply blast+
+apply (erule Stable_Int, assumption, blast+)
done
lemma Follows_Un:
@@ -218,8 +214,7 @@
apply (rule LeadsTo_weaken)
apply (rule PSP_Stable)
apply (erule_tac x = "f s" in spec)
-apply (erule Stable_Int, assumption)
-apply blast
+apply (erule Stable_Int, assumption, blast)
apply (blast intro: union_le_mono order_trans)
done
--- a/src/HOL/UNITY/Guar.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy Sat Feb 08 16:05:33 2003 +0100
@@ -109,8 +109,7 @@
lemma ex_prop_equiv:
"ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
apply auto
-apply (unfold ex_prop_def component_of_def, safe)
-apply blast
+apply (unfold ex_prop_def component_of_def, safe, blast)
apply blast
apply (subst Join_commute)
apply (drule ok_sym, blast)
--- a/src/HOL/UNITY/Lift_prog.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Sat Feb 08 16:05:33 2003 +0100
@@ -47,7 +47,7 @@
apply (auto split add: nat_diff_split)
done
-(*** Injectiveness proof ***)
+subsection{*Injectiveness proof*}
lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
by (drule_tac x = i in fun_cong, simp)
@@ -80,7 +80,7 @@
apply (rule inj_onI, auto)
done
-(*** Surjectiveness proof ***)
+subsection{*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)
@@ -111,7 +111,11 @@
lemma sub_apply [simp]: "sub i f = f i"
by (simp add: sub_def)
-(*** lift_set ***)
+lemma all_total_lift: "all_total F ==> all_total (lift i F)"
+by (simp add: lift_def rename_def Extend.all_total_extend)
+
+
+subsection{*The Operator @{term lift_set}*}
lemma lift_set_empty [simp]: "lift_set i {} = {}"
by (unfold lift_set_def, auto)
@@ -133,9 +137,7 @@
done
lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
-apply (unfold lift_set_def)
-apply (simp add: image_Un)
-done
+by (simp add: lift_set_def image_Un)
lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
apply (unfold lift_set_def)
@@ -143,7 +145,7 @@
done
-(*** the lattice operations ***)
+subsection{*The Lattice Operations*}
lemma bij_lift [iff]: "bij (lift i)"
by (simp add: lift_def)
@@ -157,7 +159,7 @@
lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
by (simp add: lift_def)
-(*** Safety: co, stable, invariant ***)
+subsection{*Safety: constrains, stable, invariant*}
lemma lift_constrains:
"(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
@@ -169,29 +171,21 @@
lemma lift_invariant:
"(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
-apply (unfold lift_def lift_set_def)
-apply (simp add: rename_invariant)
-done
+by (simp add: lift_def lift_set_def rename_invariant)
lemma lift_Constrains:
"(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
-apply (unfold lift_def lift_set_def)
-apply (simp add: rename_Constrains)
-done
+by (simp add: lift_def lift_set_def rename_Constrains)
lemma lift_Stable:
"(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
-apply (unfold lift_def lift_set_def)
-apply (simp add: rename_Stable)
-done
+by (simp add: lift_def lift_set_def rename_Stable)
lemma lift_Always:
"(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
-apply (unfold lift_def lift_set_def)
-apply (simp add: rename_Always)
-done
+by (simp add: lift_def lift_set_def rename_Always)
-(*** Progress: transient, ensures ***)
+subsection{*Progress: transient, ensures*}
lemma lift_transient:
"(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
@@ -223,16 +217,12 @@
apply (simp add: o_def)
done
-lemma lift_guarantees_eq_lift_inv: "(lift i F \<in> X guarantees Y) =
+lemma lift_guarantees_eq_lift_inv:
+ "(lift i F \<in> X guarantees Y) =
(F \<in> (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*)
@@ -293,59 +283,9 @@
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)
- txt{*This simplification is VERY slow*}
-done
-
-lemma insert_map_eq_diff:
- "[| insert_map i s f = insert_map j t g; i\<noteq>j |]
- ==> \<exists>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\<noteq>j |]
- ==> \<exists>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
-
-lemma lift_transient_eq_disj:
- "F \<in> preserves snd
- ==> (lift i F \<in> transient (lift_set j (A <*> UNIV))) =
- (i=j & F \<in> 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, 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 Extend.intro,
- THEN Extend.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) =
+lemma lift_map_image_Times:
+ "lift_map i ` (A <*> UNIV) =
(\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
apply (auto intro!: bexI image_eqI simp add: lift_map_def)
apply (rule split_conv [symmetric])
@@ -368,7 +308,7 @@
done
-(*** Lemmas to handle function composition (o) more consistently ***)
+subsection{*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"
@@ -388,15 +328,18 @@
done
-(*** More lemmas about extend and project
- They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
+subsection{*More lemmas about extend and project*}
-lemma extend_act_extend_act: "extend_act h' (extend_act h act) =
+text{*They could be moved to theory Extend or Project*}
+
+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) =
+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)
@@ -407,7 +350,7 @@
by (simp add: extend_act_def project_act_def, blast)
-(*** OK and "lift" ***)
+subsection{*OK and "lift"*}
lemma act_in_UNION_preserves_fst:
"act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
--- a/src/HOL/UNITY/PPROD.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/PPROD.thy Sat Feb 08 16:05:33 2003 +0100
@@ -27,28 +27,20 @@
(*** Basic properties ***)
-lemma Init_PLam: "Init (PLam I F) = (\<Inter>i \<in> 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 Init_PLam [simp]: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
+by (simp add: PLam_def lift_def lift_set_def)
-lemma PLam_empty: "PLam {} F = SKIP"
-apply (simp (no_asm) add: PLam_def)
-done
+lemma PLam_empty [simp]: "PLam {} F = SKIP"
+by (simp add: PLam_def)
-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_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
+by (simp add: PLam_def lift_SKIP JN_constant)
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) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
-apply (simp (no_asm) add: PLam_def JN_component_iff)
-done
+by (simp add: PLam_def JN_component_iff)
lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
apply (unfold PLam_def)
@@ -59,87 +51,89 @@
(** Safety & Progress: but are they used anywhere? **)
-lemma PLam_constrains:
- "[| i \<in> I; \<forall>j. F j \<in> preserves snd |] ==>
- (PLam I F \<in> (lift_set i (A <*> UNIV)) co
- (lift_set i (B <*> UNIV))) =
- (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
-apply (simp (no_asm_simp) add: PLam_def JN_constrains)
+lemma PLam_constrains:
+ "[| i \<in> I; \<forall>j. F j \<in> preserves snd |]
+ ==> (PLam I F \<in> (lift_set i (A <*> UNIV)) co
+ (lift_set i (B <*> UNIV))) =
+ (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
+apply (simp add: PLam_def JN_constrains)
apply (subst insert_Diff [symmetric], assumption)
-apply (simp (no_asm_simp) add: lift_constrains)
+apply (simp add: lift_constrains)
apply (blast intro: constrains_imp_lift_constrains)
done
-lemma PLam_stable:
- "[| i \<in> I; \<forall>j. F j \<in> preserves snd |]
- ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
+lemma PLam_stable:
+ "[| i \<in> I; \<forall>j. F j \<in> preserves snd |]
+ ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
(F i \<in> stable (A <*> UNIV))"
-apply (simp (no_asm_simp) add: stable_def PLam_constrains)
-done
+by (simp add: stable_def PLam_constrains)
+
+lemma PLam_transient:
+ "i \<in> I ==>
+ PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
+by (simp add: JN_transient PLam_def)
-lemma PLam_transient:
- "i \<in> I ==>
- PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
-apply (simp (no_asm_simp) add: JN_transient PLam_def)
+text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
+lemma PLam_ensures:
+ "[| i \<in> I; F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
+ \<forall>j. F j \<in> preserves snd |]
+ ==> PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
+apply (simp add: ensures_def PLam_constrains PLam_transient
+ lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
+ Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
+apply (rule rev_bexI, assumption)
+apply (simp add: lift_transient)
done
-(*This holds because the F j cannot change (lift_set i)*)
-lemma PLam_ensures:
- "[| i \<in> I; F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
- \<forall>j. F j \<in> preserves snd |] ==>
- PLam I F \<in> 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 \<in> I;
- F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
- ((A <*> UNIV) \<union> (B <*> UNIV));
- F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
- \<forall>j. F j \<in> preserves snd |] ==>
- PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
+lemma PLam_leadsTo_Basis:
+ "[| i \<in> I;
+ F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
+ ((A <*> UNIV) \<union> (B <*> UNIV));
+ F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
+ \<forall>j. F j \<in> preserves snd |]
+ ==> PLam I F \<in> 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 \<in> invariant (A <*> UNIV); i \<in> I;
- \<forall>j. F j \<in> preserves snd |]
+lemma invariant_imp_PLam_invariant:
+ "[| F i \<in> invariant (A <*> UNIV); i \<in> I;
+ \<forall>j. F j \<in> preserves snd |]
==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
by (auto simp add: PLam_stable invariant_def)
lemma PLam_preserves_fst [simp]:
- "\<forall>j. F j \<in> preserves snd
- ==> (PLam I F \<in> preserves (v o sub j o fst)) =
+ "\<forall>j. F j \<in> preserves snd
+ ==> (PLam I F \<in> preserves (v o sub j o fst)) =
(if j \<in> I then F j \<in> preserves (v o fst) else True)"
-by (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
+by (simp add: PLam_def lift_preserves_sub)
lemma PLam_preserves_snd [simp,intro]:
"\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
-by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
+by (simp add: PLam_def lift_preserves_snd_I)
(*** guarantees properties ***)
-(*This rule looks unsatisfactory because it refers to "lift". One must use
+text{*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 \<in> I;
- OK I (%i. lift i (F i)) |]
+ no obvious way to alternative for the third premise.*}
+lemma guarantees_PLam_I:
+ "[| lift i (F i): X guarantees Y; i \<in> I;
+ OK I (%i. lift i (F i)) |]
==> (PLam I F) \<in> X guarantees Y"
apply (unfold PLam_def)
-apply (simp (no_asm_simp) add: guarantees_JN_I)
+apply (simp add: guarantees_JN_I)
done
lemma Allowed_PLam [simp]:
"Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
-by (simp (no_asm) add: PLam_def)
+by (simp add: PLam_def)
lemma PLam_preserves [simp]:
@@ -149,24 +143,24 @@
(**UNUSED
(*The f0 premise ensures that the product is well-defined.*)
- lemma PLam_invariant_imp_invariant:
- "[| PLam I F \<in> invariant (lift_set i A); i \<in> I;
+ lemma PLam_invariant_imp_invariant:
+ "[| PLam I F \<in> invariant (lift_set i A); i \<in> I;
f0: Init (PLam I F) |] ==> F i \<in> invariant A"
apply (auto simp add: invariant_def)
apply (drule_tac c = "f0 (i:=x) " in subsetD)
apply auto
done
- lemma PLam_invariant:
- "[| i \<in> I; f0: Init (PLam I F) |]
+ lemma PLam_invariant:
+ "[| i \<in> I; f0: Init (PLam I F) |]
==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> 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 \<in> I
+ lemma reachable_PLam:
+ "i \<in> I
==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
apply (auto simp add: invariant_def)
done
@@ -185,15 +179,15 @@
lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
by auto
- lemma reachable_PLam_subset1:
+ lemma reachable_PLam_subset1:
"reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
apply (force dest!: reachable_PLam)
done
(*simplify using reachable_lift??*)
lemma reachable_lift_Join_PLam [rule_format]:
- "[| i \<notin> I; A \<in> reachable (F i) |]
- ==> \<forall>f. f \<in> reachable (PLam I F)
+ "[| i \<notin> I; A \<in> reachable (F i) |]
+ ==> \<forall>f. f \<in> reachable (PLam I F)
--> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
apply (erule reachable.induct)
apply (ALLGOALS Clarify_tac)
@@ -222,16 +216,16 @@
(*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
+ lemma reachable_PLam_subset2:
+ "finite I
==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> 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 ==>
+ lemma reachable_PLam_eq:
+ "finite I ==>
reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
done
@@ -239,8 +233,8 @@
(** Co **)
- lemma Constrains_imp_PLam_Constrains:
- "[| F i \<in> A Co B; i \<in> I; finite I |]
+ lemma Constrains_imp_PLam_Constrains:
+ "[| F i \<in> A Co B; i \<in> I; finite I |]
==> PLam I F \<in> (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)
@@ -249,37 +243,37 @@
- lemma PLam_Constrains:
- "[| i \<in> I; finite I; f0: Init (PLam I F) |]
- ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =
+ lemma PLam_Constrains:
+ "[| i \<in> I; finite I; f0: Init (PLam I F) |]
+ ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =
(F i \<in> A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
done
- lemma PLam_Stable:
- "[| i \<in> I; finite I; f0: Init (PLam I F) |]
+ lemma PLam_Stable:
+ "[| i \<in> I; finite I; f0: Init (PLam I F) |]
==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
- apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
+ apply (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 \<in> I; finite I |]
- ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =
+ lemma const_PLam_Constrains:
+ "[| i \<in> I; finite I |]
+ ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =
(F \<in> A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
done
- lemma const_PLam_Stable:
- "[| i \<in> I; finite I |]
+ lemma const_PLam_Stable:
+ "[| i \<in> I; finite I |]
==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
- apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
+ apply (simp add: Stable_def const_PLam_Constrains)
done
- lemma const_PLam_Increasing:
- "[| i \<in> I; finite I |]
+ lemma const_PLam_Increasing:
+ "[| i \<in> I; finite I |]
==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
apply (unfold Increasing_def)
apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
--- a/src/HOL/UNITY/Project.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Project.thy Sat Feb 08 16:05:33 2003 +0100
@@ -16,20 +16,20 @@
projecting :: "['c program => 'c set, 'a*'b => 'c,
'a program, 'c program set, 'a program set] => bool"
"projecting C h F X' X ==
- ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
+ \<forall>G. extend h F Join G \<in> X' --> F Join project h (C G) G \<in> X"
extending :: "['c program => 'c set, 'a*'b => 'c, 'a program,
'c program set, 'a program set] => bool"
"extending C h F Y' Y ==
- ALL G. extend h F ok G --> F Join project h (C G) G : Y
- --> extend h F Join G : Y'"
+ \<forall>G. extend h F ok G --> F Join project h (C G) G \<in> Y
+ --> extend h F Join G \<in> Y'"
subset_closed :: "'a set set => bool"
- "subset_closed U == ALL A: U. Pow A <= U"
+ "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"
lemma (in Extend) project_extend_constrains_I:
- "F : A co B ==> project h C (extend h F) : A co B"
+ "F \<in> A co B ==> project h C (extend h F) \<in> A co B"
apply (auto simp add: extend_act_def project_act_def constrains_def)
done
@@ -38,8 +38,8 @@
(*used below to prove Join_project_ensures*)
lemma (in Extend) project_unless [rule_format]:
- "[| G : stable C; project h C G : A unless B |]
- ==> G : (C Int extend_set h A) unless (extend_set h B)"
+ "[| G \<in> stable C; project h C G \<in> A unless B |]
+ ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
apply (simp add: unless_def project_constrains)
apply (blast dest: stable_constrains_Int intro: constrains_weaken)
done
@@ -47,21 +47,21 @@
(*Generalizes project_constrains to the program F Join project h C G
useful with guarantees reasoning*)
lemma (in Extend) Join_project_constrains:
- "(F Join project h C G : A co B) =
- (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &
- F : A co B)"
+ "(F Join project h C G \<in> A co B) =
+ (extend h F Join G \<in> (C \<inter> extend_set h A) co (extend_set h B) &
+ F \<in> A co B)"
apply (simp (no_asm) add: project_constrains)
apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken]
dest: constrains_imp_subset)
done
(*The condition is required to prove the left-to-right direction
- could weaken it to G : (C Int extend_set h A) co C*)
+ could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
lemma (in Extend) Join_project_stable:
- "extend h F Join G : stable C
- ==> (F Join project h C G : stable A) =
- (extend h F Join G : stable (C Int extend_set h A) &
- F : stable A)"
+ "extend h F Join G \<in> stable C
+ ==> (F Join project h C G \<in> stable A) =
+ (extend h F Join G \<in> stable (C \<inter> extend_set h A) &
+ F \<in> stable A)"
apply (unfold stable_def)
apply (simp only: Join_project_constrains)
apply (blast intro: constrains_weaken dest: constrains_Int)
@@ -69,23 +69,23 @@
(*For using project_guarantees in particular cases*)
lemma (in Extend) project_constrains_I:
- "extend h F Join G : extend_set h A co extend_set h B
- ==> F Join project h C G : A co B"
+ "extend h F Join G \<in> extend_set h A co extend_set h B
+ ==> F Join project h C G \<in> A co B"
apply (simp add: project_constrains extend_constrains)
apply (blast intro: constrains_weaken dest: constrains_imp_subset)
done
lemma (in Extend) project_increasing_I:
- "extend h F Join G : increasing (func o f)
- ==> F Join project h C G : increasing func"
+ "extend h F Join G \<in> increasing (func o f)
+ ==> F Join project h C G \<in> increasing func"
apply (unfold increasing_def stable_def)
apply (simp del: Join_constrains
add: project_constrains_I extend_set_eq_Collect)
done
lemma (in Extend) Join_project_increasing:
- "(F Join project h UNIV G : increasing func) =
- (extend h F Join G : increasing (func o f))"
+ "(F Join project h UNIV G \<in> increasing func) =
+ (extend h F Join G \<in> increasing (func o f))"
apply (rule iffI)
apply (erule_tac [2] project_increasing_I)
apply (simp del: Join_stable
@@ -95,8 +95,8 @@
(*The UNIV argument is essential*)
lemma (in Extend) project_constrains_D:
- "F Join project h UNIV G : A co B
- ==> extend h F Join G : extend_set h A co extend_set h B"
+ "F Join project h UNIV G \<in> A co B
+ ==> extend h F Join G \<in> extend_set h A co extend_set h B"
by (simp add: project_constrains extend_constrains)
@@ -104,26 +104,26 @@
lemma projecting_Int:
"[| projecting C h F XA' XA; projecting C h F XB' XB |]
- ==> projecting C h F (XA' Int XB') (XA Int XB)"
+ ==> projecting C h F (XA' \<inter> XB') (XA \<inter> XB)"
by (unfold projecting_def, blast)
lemma projecting_Un:
"[| projecting C h F XA' XA; projecting C h F XB' XB |]
- ==> projecting C h F (XA' Un XB') (XA Un XB)"
+ ==> projecting C h F (XA' \<union> XB') (XA \<union> XB)"
by (unfold projecting_def, blast)
lemma projecting_INT:
- "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]
- ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"
+ "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]
+ ==> projecting C h F (\<Inter>i \<in> I. X' i) (\<Inter>i \<in> I. X i)"
by (unfold projecting_def, blast)
lemma projecting_UN:
- "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]
- ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"
+ "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]
+ ==> projecting C h F (\<Union>i \<in> I. X' i) (\<Union>i \<in> I. X i)"
by (unfold projecting_def, blast)
lemma projecting_weaken:
- "[| projecting C h F X' X; U'<=X'; X<=U |] ==> projecting C h F U' U"
+ "[| projecting C h F X' X; U'<=X'; X \<subseteq> U |] ==> projecting C h F U' U"
by (unfold projecting_def, auto)
lemma projecting_weaken_L:
@@ -132,26 +132,26 @@
lemma extending_Int:
"[| extending C h F YA' YA; extending C h F YB' YB |]
- ==> extending C h F (YA' Int YB') (YA Int YB)"
+ ==> extending C h F (YA' \<inter> YB') (YA \<inter> YB)"
by (unfold extending_def, blast)
lemma extending_Un:
"[| extending C h F YA' YA; extending C h F YB' YB |]
- ==> extending C h F (YA' Un YB') (YA Un YB)"
+ ==> extending C h F (YA' \<union> YB') (YA \<union> YB)"
by (unfold extending_def, blast)
lemma extending_INT:
- "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]
- ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)"
+ "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]
+ ==> extending C h F (\<Inter>i \<in> I. Y' i) (\<Inter>i \<in> I. Y i)"
by (unfold extending_def, blast)
lemma extending_UN:
- "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]
- ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)"
+ "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]
+ ==> extending C h F (\<Union>i \<in> I. Y' i) (\<Union>i \<in> I. Y i)"
by (unfold extending_def, blast)
lemma extending_weaken:
- "[| extending C h F Y' Y; Y'<=V'; V<=Y |] ==> extending C h F V' V"
+ "[| extending C h F Y' Y; Y'<=V'; V \<subseteq> Y |] ==> extending C h F V' V"
by (unfold extending_def, auto)
lemma extending_weaken_L:
@@ -204,9 +204,9 @@
(*In practice, C = reachable(...): the inclusion is equality*)
lemma (in Extend) reachable_imp_reachable_project:
- "[| reachable (extend h F Join G) <= C;
- z : reachable (extend h F Join G) |]
- ==> f z : reachable (F Join project h C G)"
+ "[| reachable (extend h F Join G) \<subseteq> C;
+ z \<in> reachable (extend h F Join G) |]
+ ==> f z \<in> reachable (F Join project h C G)"
apply (erule reachable.induct)
apply (force intro!: reachable.Init simp add: split_extended_all, auto)
apply (rule_tac act = x in reachable.Acts)
@@ -217,8 +217,8 @@
done
lemma (in Extend) project_Constrains_D:
- "F Join project h (reachable (extend h F Join G)) G : A Co B
- ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"
+ "F Join project h (reachable (extend h F Join G)) G \<in> A Co B
+ ==> extend h F Join G \<in> (extend_set h A) Co (extend_set h B)"
apply (unfold Constrains_def)
apply (simp del: Join_constrains
add: Join_project_constrains, clarify)
@@ -227,22 +227,22 @@
done
lemma (in Extend) project_Stable_D:
- "F Join project h (reachable (extend h F Join G)) G : Stable A
- ==> extend h F Join G : Stable (extend_set h A)"
+ "F Join project h (reachable (extend h F Join G)) G \<in> Stable A
+ ==> extend h F Join G \<in> Stable (extend_set h A)"
apply (unfold Stable_def)
apply (simp (no_asm_simp) add: project_Constrains_D)
done
lemma (in Extend) project_Always_D:
- "F Join project h (reachable (extend h F Join G)) G : Always A
- ==> extend h F Join G : Always (extend_set h A)"
+ "F Join project h (reachable (extend h F Join G)) G \<in> Always A
+ ==> extend h F Join G \<in> Always (extend_set h A)"
apply (unfold Always_def)
apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
done
lemma (in Extend) project_Increasing_D:
- "F Join project h (reachable (extend h F Join G)) G : Increasing func
- ==> extend h F Join G : Increasing (func o f)"
+ "F Join project h (reachable (extend h F Join G)) G \<in> Increasing func
+ ==> extend h F Join G \<in> Increasing (func o f)"
apply (unfold Increasing_def, auto)
apply (subst extend_set_eq_Collect [symmetric])
apply (simp (no_asm_simp) add: project_Stable_D)
@@ -253,9 +253,9 @@
(*In practice, C = reachable(...): the inclusion is equality*)
lemma (in Extend) reachable_project_imp_reachable:
- "[| C <= reachable(extend h F Join G);
- x : reachable (F Join project h C G) |]
- ==> EX y. h(x,y) : reachable (extend h F Join G)"
+ "[| C \<subseteq> reachable(extend h F Join G);
+ x \<in> reachable (F Join project h C G) |]
+ ==> \<exists>y. h(x,y) \<in> reachable (extend h F Join G)"
apply (erule reachable.induct)
apply (force intro: reachable.Init)
apply (auto simp add: project_act_def)
@@ -270,15 +270,15 @@
(*UNUSED*)
lemma (in Extend) reachable_extend_Join_subset:
- "reachable (extend h F Join G) <= C
- ==> reachable (extend h F Join G) <=
+ "reachable (extend h F Join G) \<subseteq> C
+ ==> reachable (extend h F Join G) \<subseteq>
extend_set h (reachable (F Join project h C G))"
apply (auto dest: reachable_imp_reachable_project)
done
lemma (in Extend) project_Constrains_I:
- "extend h F Join G : (extend_set h A) Co (extend_set h B)
- ==> F Join project h (reachable (extend h F Join G)) G : A Co B"
+ "extend h F Join G \<in> (extend_set h A) Co (extend_set h B)
+ ==> F Join project h (reachable (extend h F Join G)) G \<in> A Co B"
apply (unfold Constrains_def)
apply (simp del: Join_constrains
add: Join_project_constrains extend_set_Int_distrib)
@@ -291,43 +291,43 @@
done
lemma (in Extend) project_Stable_I:
- "extend h F Join G : Stable (extend_set h A)
- ==> F Join project h (reachable (extend h F Join G)) G : Stable A"
+ "extend h F Join G \<in> Stable (extend_set h A)
+ ==> F Join project h (reachable (extend h F Join G)) G \<in> Stable A"
apply (unfold Stable_def)
apply (simp (no_asm_simp) add: project_Constrains_I)
done
lemma (in Extend) project_Always_I:
- "extend h F Join G : Always (extend_set h A)
- ==> F Join project h (reachable (extend h F Join G)) G : Always A"
+ "extend h F Join G \<in> Always (extend_set h A)
+ ==> F Join project h (reachable (extend h F Join G)) G \<in> Always A"
apply (unfold Always_def)
apply (auto simp add: project_Stable_I)
apply (unfold extend_set_def, blast)
done
lemma (in Extend) project_Increasing_I:
- "extend h F Join G : Increasing (func o f)
- ==> F Join project h (reachable (extend h F Join G)) G : Increasing func"
+ "extend h F Join G \<in> Increasing (func o f)
+ ==> F Join project h (reachable (extend h F Join G)) G \<in> Increasing func"
apply (unfold Increasing_def, auto)
apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
done
lemma (in Extend) project_Constrains:
- "(F Join project h (reachable (extend h F Join G)) G : A Co B) =
- (extend h F Join G : (extend_set h A) Co (extend_set h B))"
+ "(F Join project h (reachable (extend h F Join G)) G \<in> A Co B) =
+ (extend h F Join G \<in> (extend_set h A) Co (extend_set h B))"
apply (blast intro: project_Constrains_I project_Constrains_D)
done
lemma (in Extend) project_Stable:
- "(F Join project h (reachable (extend h F Join G)) G : Stable A) =
- (extend h F Join G : Stable (extend_set h A))"
+ "(F Join project h (reachable (extend h F Join G)) G \<in> Stable A) =
+ (extend h F Join G \<in> Stable (extend_set h A))"
apply (unfold Stable_def)
apply (rule project_Constrains)
done
lemma (in Extend) project_Increasing:
- "(F Join project h (reachable (extend h F Join G)) G : Increasing func) =
- (extend h F Join G : Increasing (func o f))"
+ "(F Join project h (reachable (extend h F Join G)) G \<in> Increasing func) =
+ (extend h F Join G \<in> Increasing (func o f))"
apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
done
@@ -397,30 +397,24 @@
subsubsection{*transient*}
lemma (in Extend) transient_extend_set_imp_project_transient:
- "[| G : transient (C Int extend_set h A); G : stable C |]
- ==> project h C G : transient (project_set h C Int A)"
-
-apply (unfold transient_def)
-apply (auto simp add: Domain_project_act)
-apply (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A")
-prefer 2
+ "[| G \<in> transient (C \<inter> extend_set h A); G \<in> stable C |]
+ ==> project h C G \<in> transient (project_set h C \<inter> A)"
+apply (auto simp add: transient_def Domain_project_act)
+apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A")
+ prefer 2
apply (simp add: stable_def constrains_def, blast)
(*back to main goal*)
-apply (erule_tac V = "?AA <= -C Un ?BB" in thin_rl)
+apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl)
apply (drule bspec, assumption)
apply (simp add: extend_set_def project_act_def, blast)
done
(*converse might hold too?*)
lemma (in Extend) project_extend_transient_D:
- "project h C (extend h F) : transient (project_set h C Int D)
- ==> F : transient (project_set h C Int D)"
-apply (unfold transient_def)
-apply (auto simp add: Domain_project_act)
-apply (rule bexI)
-prefer 2 apply assumption
-apply auto
-apply (unfold extend_act_def, blast)
+ "project h C (extend h F) \<in> transient (project_set h C \<inter> D)
+ ==> F \<in> transient (project_set h C \<inter> D)"
+apply (simp add: transient_def Domain_project_act, safe)
+apply blast+
done
@@ -428,11 +422,12 @@
(*Used to prove project_leadsETo_I*)
lemma (in Extend) ensures_extend_set_imp_project_ensures:
- "[| extend h F : stable C; G : stable C;
- extend h F Join G : A ensures B; A-B = C Int extend_set h D |]
+ "[| extend h F \<in> stable C; G \<in> stable C;
+ extend h F Join G \<in> A ensures B; A-B = C \<inter> extend_set h D |]
==> F Join project h C G
- : (project_set h C Int project_set h A) ensures (project_set h B)"
-apply (simp add: ensures_def project_constrains Join_transient extend_transient, clarify)
+ \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
+apply (simp add: ensures_def project_constrains Join_transient extend_transient,
+ clarify)
apply (intro conjI)
(*first subgoal*)
apply (blast intro: extend_stable_project_set
@@ -457,19 +452,42 @@
[THEN project_extend_transient_D, THEN transient_strengthen])
done
+text{*Transferring a transient property upwards*}
+lemma (in Extend) project_transient_extend_set:
+ "project h C G \<in> transient (project_set h C \<inter> A - B)
+ ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
+apply (simp add: transient_def project_set_def extend_set_def project_act_def)
+apply (elim disjE bexE)
+ apply (rule_tac x=Id in bexI)
+ apply (blast intro!: rev_bexI )+
+done
+
+lemma (in Extend) project_unless2 [rule_format]:
+ "[| G \<in> stable C; project h C G \<in> (project_set h C \<inter> A) unless B |]
+ ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
+by (auto dest: stable_constrains_Int intro: constrains_weaken
+ simp add: unless_def project_constrains Diff_eq Int_assoc
+ Int_extend_set_lemma)
+
+
+lemma (in Extend) extend_unless:
+ "[|extend h F \<in> stable C; F \<in> A unless B|]
+ ==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B"
+apply (simp add: unless_def stable_def)
+apply (drule constrains_Int)
+apply (erule extend_constrains [THEN iffD2])
+apply (erule constrains_weaken, blast)
+apply blast
+done
+
(*Used to prove project_leadsETo_D*)
lemma (in Extend) Join_project_ensures [rule_format]:
- "[| project h C G ~: transient (A-B) | A<=B;
- extend h F Join G : stable C;
- F Join project h C G : A ensures B |]
- ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
-apply (erule disjE)
-prefer 2 apply (blast intro: subset_imp_ensures)
-apply (auto dest: extend_transient [THEN iffD2]
- intro: transient_strengthen project_set_I
- project_unless [THEN unlessD] unlessI
- project_extend_constrains_I
- simp add: ensures_def Join_transient)
+ "[| extend h F Join G \<in> stable C;
+ F Join project h C G \<in> A ensures B |]
+ ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
+apply (auto simp add: ensures_eq extend_unless project_unless)
+apply (blast intro: extend_transient [THEN iffD2] transient_strengthen)
+apply (blast intro: project_transient_extend_set transient_strengthen)
done
text{*Lemma useful for both STRONG and WEAK progress, but the transient
@@ -478,11 +496,10 @@
(*The strange induction formula allows induction over the leadsTo
assumption's non-atomic precondition*)
lemma (in Extend) PLD_lemma:
- "[| ALL D. project h C G : transient D --> D={};
- extend h F Join G : stable C;
- F Join project h C G : (project_set h C Int A) leadsTo B |]
- ==> extend h F Join G :
- C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"
+ "[| extend h F Join G \<in> stable C;
+ F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
+ ==> extend h F Join G \<in>
+ C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
apply (erule leadsTo_induct)
apply (blast intro: leadsTo_Basis Join_project_ensures)
apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
@@ -490,74 +507,28 @@
done
lemma (in Extend) project_leadsTo_D_lemma:
- "[| ALL D. project h C G : transient D --> D={};
- extend h F Join G : stable C;
- F Join project h C G : (project_set h C Int A) leadsTo B |]
- ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"
+ "[| extend h F Join G \<in> stable C;
+ F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
+ ==> extend h F Join G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
apply (rule PLD_lemma [THEN leadsTo_weaken])
apply (auto simp add: split_extended_all)
done
lemma (in Extend) Join_project_LeadsTo:
"[| C = (reachable (extend h F Join G));
- ALL D. project h C G : transient D --> D={};
- F Join project h C G : A LeadsTo B |]
- ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
+ F Join project h C G \<in> A LeadsTo B |]
+ ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
by (simp del: Join_stable add: LeadsTo_def project_leadsTo_D_lemma
project_set_reachable_extend_eq)
subsection{*Towards the theorem @{text project_Ensures_D}*}
-
-lemma (in Extend) act_subset_imp_project_act_subset:
- "act `` (C Int extend_set h A) <= B
- ==> project_act h (Restrict C act) `` (project_set h C Int A)
- <= project_set h B"
-apply (unfold project_set_def extend_set_def project_act_def, blast)
-done
-
-(*This trivial proof is the complementation part of transferring a transient
- property upwards. The hard part would be to
- show that G's action has a big enough domain.*)
-lemma (in Extend)
- "[| act: Acts G;
- (project_act h (Restrict C act))``
- (project_set h C Int A - B) <= -(project_set h C Int A - B) |]
- ==> act``(C Int extend_set h A - extend_set h B)
- <= -(C Int extend_set h A - extend_set h B)"
-by (auto simp add: project_set_def extend_set_def project_act_def)
-
-lemma (in Extend) stable_project_transient:
- "[| G : stable ((C Int extend_set h A) - (extend_set h B));
- project h C G : transient (project_set h C Int A - B) |]
- ==> (C Int extend_set h A) - extend_set h B = {}"
-apply (auto simp add: transient_def subset_Compl_self_eq Domain_project_act split_extended_all, blast)
-apply (auto simp add: stable_def constrains_def)
-apply (drule bspec, assumption)
-apply (auto simp add: Int_Diff extend_set_Diff_distrib [symmetric])
-apply (drule act_subset_imp_project_act_subset)
-apply (subgoal_tac "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}")
-apply (erule_tac V = "?r``?A <= ?B" in thin_rl)+
-apply (unfold project_set_def extend_set_def project_act_def)
-prefer 2 apply blast
-apply (rule ccontr)
-apply (drule subsetD, blast)
-apply (force simp add: split_extended_all)
-done
-
-lemma (in Extend) project_unless2 [rule_format]:
- "[| G : stable C; project h C G : (project_set h C Int A) unless B |]
- ==> G : (C Int extend_set h A) unless (extend_set h B)"
-by (auto dest: stable_constrains_Int intro: constrains_weaken
- simp add: unless_def project_constrains Diff_eq Int_assoc
- Int_extend_set_lemma)
-
lemma (in Extend) project_ensures_D_lemma:
- "[| G : stable ((C Int extend_set h A) - (extend_set h B));
- F Join project h C G : (project_set h C Int A) ensures B;
- extend h F Join G : stable C |]
- ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
+ "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));
+ F Join project h C G \<in> (project_set h C \<inter> A) ensures B;
+ extend h F Join G \<in> stable C |]
+ ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
(*unless*)
apply (auto intro!: project_unless2 [unfolded unless_def]
intro: project_extend_constrains_I
@@ -565,26 +536,24 @@
(*transient*)
(*A G-action cannot occur*)
prefer 2
- apply (force dest: stable_project_transient
- simp del: Diff_eq_empty_iff
- simp add: Diff_eq_empty_iff [symmetric])
+ apply (blast intro: project_transient_extend_set)
(*An F-action*)
apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
simp add: split_extended_all)
done
lemma (in Extend) project_ensures_D:
- "[| F Join project h UNIV G : A ensures B;
- G : stable (extend_set h A - extend_set h B) |]
- ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"
+ "[| F Join project h UNIV G \<in> A ensures B;
+ G \<in> stable (extend_set h A - extend_set h B) |]
+ ==> extend h F Join G \<in> (extend_set h A) ensures (extend_set h B)"
apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
done
lemma (in Extend) project_Ensures_D:
- "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B;
- G : stable (reachable (extend h F Join G) Int extend_set h A -
+ "[| F Join project h (reachable (extend h F Join G)) G \<in> A Ensures B;
+ G \<in> stable (reachable (extend h F Join G) \<inter> extend_set h A -
extend_set h B) |]
- ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)"
+ ==> extend h F Join G \<in> (extend_set h A) Ensures (extend_set h B)"
apply (unfold Ensures_def)
apply (rule project_ensures_D_lemma [THEN revcut_rl])
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
@@ -594,7 +563,7 @@
subsection{*Guarantees*}
lemma (in Extend) project_act_Restrict_subset_project_act:
- "project_act h (Restrict C act) <= project_act h act"
+ "project_act h (Restrict C act) \<subseteq> project_act h act"
apply (auto simp add: project_act_def)
done
@@ -616,24 +585,24 @@
Not clear that it has a converse [or that we want one!]*)
(*The raw version; 3rd premise could be weakened by adding the
- precondition extend h F Join G : X' *)
+ precondition extend h F Join G \<in> X' *)
lemma (in Extend) project_guarantees_raw:
- assumes xguary: "F : X guarantees Y"
+ assumes xguary: "F \<in> X guarantees Y"
and closed: "subset_closed (AllowedActs F)"
- and project: "!!G. extend h F Join G : X'
- ==> F Join project h (C G) G : X"
- and extend: "!!G. [| F Join project h (C G) G : Y |]
- ==> extend h F Join G : Y'"
- shows "extend h F : X' guarantees Y'"
+ and project: "!!G. extend h F Join G \<in> X'
+ ==> F Join project h (C G) G \<in> X"
+ and extend: "!!G. [| F Join project h (C G) G \<in> Y |]
+ ==> extend h F Join G \<in> Y'"
+ shows "extend h F \<in> X' guarantees Y'"
apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
apply (erule project)
done
lemma (in Extend) project_guarantees:
- "[| F : X guarantees Y; subset_closed (AllowedActs F);
+ "[| F \<in> X guarantees Y; subset_closed (AllowedActs F);
projecting C h F X' X; extending C h F Y' Y |]
- ==> extend h F : X' guarantees Y'"
+ ==> extend h F \<in> X' guarantees Y'"
apply (rule guaranteesI)
apply (auto simp add: guaranteesD projecting_def extending_def
subset_closed_ok_extend_imp_ok_project)
@@ -648,73 +617,58 @@
subsubsection{*Some could be deleted: the required versions are easy to prove*}
lemma (in Extend) extend_guar_increasing:
- "[| F : UNIV guarantees increasing func;
+ "[| F \<in> UNIV guarantees increasing func;
subset_closed (AllowedActs F) |]
- ==> extend h F : X' guarantees increasing (func o f)"
+ ==> extend h F \<in> X' guarantees increasing (func o f)"
apply (erule project_guarantees)
apply (rule_tac [3] extending_increasing)
apply (rule_tac [2] projecting_UNIV, auto)
done
lemma (in Extend) extend_guar_Increasing:
- "[| F : UNIV guarantees Increasing func;
+ "[| F \<in> UNIV guarantees Increasing func;
subset_closed (AllowedActs F) |]
- ==> extend h F : X' guarantees Increasing (func o f)"
+ ==> extend h F \<in> X' guarantees Increasing (func o f)"
apply (erule project_guarantees)
apply (rule_tac [3] extending_Increasing)
apply (rule_tac [2] projecting_UNIV, auto)
done
lemma (in Extend) extend_guar_Always:
- "[| F : Always A guarantees Always B;
+ "[| F \<in> Always A guarantees Always B;
subset_closed (AllowedActs F) |]
==> extend h F
- : Always(extend_set h A) guarantees Always(extend_set h B)"
+ \<in> Always(extend_set h A) guarantees Always(extend_set h B)"
apply (erule project_guarantees)
apply (rule_tac [3] extending_Always)
apply (rule_tac [2] projecting_Always, auto)
done
-lemma (in Extend) preserves_project_transient_empty:
- "[| G : preserves f; project h C G : transient D |] ==> D={}"
-apply (rule stable_transient_empty)
- prefer 2 apply assumption
-apply (blast intro: project_preserves_id_I
- preserves_id_subset_stable [THEN subsetD])
-done
-
-subsubsection{*Guarantees with a leadsTo postcondition
- ALL TOO WEAK because G can't affect F's variables at all**)
+subsubsection{*Guarantees with a leadsTo postcondition*}
lemma (in Extend) project_leadsTo_D:
- "[| F Join project h UNIV G : A leadsTo B;
- G : preserves f |]
- ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"
-apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken])
-apply (auto dest: preserves_project_transient_empty)
+ "F Join project h UNIV G \<in> A leadsTo B
+ ==> extend h F Join G \<in> (extend_set h A) leadsTo (extend_set h B)"
+apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
done
lemma (in Extend) project_LeadsTo_D:
- "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B;
- G : preserves f |]
- ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
-apply (rule refl [THEN Join_project_LeadsTo])
-apply (auto dest: preserves_project_transient_empty)
+ "F Join project h (reachable (extend h F Join G)) G \<in> A LeadsTo B
+ ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
+apply (rule refl [THEN Join_project_LeadsTo], auto)
done
lemma (in Extend) extending_leadsTo:
- "(ALL G. extend h F ok G --> G : preserves f)
- ==> extending (%G. UNIV) h F
- (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
+ "extending (%G. UNIV) h F
+ (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
apply (unfold extending_def)
apply (blast intro: project_leadsTo_D)
done
lemma (in Extend) extending_LeadsTo:
- "(ALL G. extend h F ok G --> G : preserves f)
- ==> extending (%G. reachable (extend h F Join G)) h F
- (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
+ "extending (%G. reachable (extend h F Join G)) h F
+ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
apply (unfold extending_def)
apply (blast intro: project_LeadsTo_D)
done
--- a/src/HOL/UNITY/Simple/Common.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy Sat Feb 08 16:05:33 2003 +0100
@@ -54,20 +54,27 @@
by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
(*This one is t := ftime t || t := gtime t*)
-lemma "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
+lemma "mk_total_program
+ (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
\<in> {m} co (maxfg m)"
-by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
+apply (simp add: mk_total_program_def)
+apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
+done
(*This one is t := max (ftime t) (gtime t)*)
-lemma "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
+lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
\<in> {m} co (maxfg m)"
-by (simp add: constrains_def maxfg_def max_def gasc)
+apply (simp add: mk_total_program_def)
+apply (simp add: constrains_def maxfg_def max_def gasc)
+done
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
-lemma "mk_program
+lemma "mk_total_program
(UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)
\<in> {m} co (maxfg m)"
-by (simp add: constrains_def maxfg_def max_def gasc)
+apply (simp add: mk_total_program_def)
+apply (simp add: constrains_def maxfg_def max_def gasc)
+done
(*It remans to prove that they satisfy CMT3': t does not decrease,
--- a/src/HOL/UNITY/Simple/Lift.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Simple/Lift.thy Sat Feb 08 16:05:33 2003 +0100
@@ -120,11 +120,12 @@
Lift :: "state program"
(*for the moment, we OMIT button_press*)
- "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
+ "Lift == mk_total_program
+ ({s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
- {request_act, open_act, close_act,
- req_up, req_down, move_up, move_down},
- UNIV)"
+ {request_act, open_act, close_act,
+ req_up, req_down, move_up, move_down},
+ UNIV)"
(** Invariants **)
@@ -196,7 +197,7 @@
lemma open_stop: "Lift \<in> Always open_stop"
apply (rule AlwaysI, force)
-apply (unfold Lift_def, constrains)
+apply (unfold Lift_def, constrains)
done
lemma stop_floor: "Lift \<in> Always stop_floor"
@@ -249,19 +250,22 @@
apply (unfold Lift_def, ensures_tac "open_act")
done (*lem_lift_1_5*)
+
+
+
lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo
- (Req n \<inter> opened - atFloor n)"
+ (Req n \<inter> opened - atFloor n)"
apply (cut_tac stop_floor)
apply (unfold Lift_def, ensures_tac "open_act")
done (*lem_lift_1_1*)
lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo
- (Req n \<inter> closed - (atFloor n - queueing))"
+ (Req n \<inter> closed - (atFloor n - queueing))"
apply (unfold Lift_def, ensures_tac "close_act")
done (*lem_lift_1_2*)
lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))
- LeadsTo (opened \<inter> atFloor n)"
+ LeadsTo (opened \<inter> atFloor n)"
apply (unfold Lift_def, ensures_tac "open_act")
done (*lem_lift_1_7*)
--- a/src/HOL/UNITY/Simple/Mutex.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Simple/Mutex.thy Sat Feb 08 16:05:33 2003 +0100
@@ -54,9 +54,10 @@
"V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
Mutex :: "state program"
- "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
- {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
- UNIV)"
+ "Mutex == mk_total_program
+ ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
+ {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
+ UNIV)"
(** The correct invariants **)
--- a/src/HOL/UNITY/Simple/NSP_Bad.ML Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.ML Sat Feb 08 16:05:33 2003 +0100
@@ -22,8 +22,7 @@
Here, it facilitates re-use of the Auth proofs.*)
AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]);
-
-Addsimps [Nprg_def RS def_prg_simps];
+Addsimps [Nprg_def RS def_prg_Init];
(*A "possibility property": there are traces that reach the end.
@@ -31,12 +30,13 @@
Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \
\ Says A B (Crypt (pubK B) (Nonce NB)) : set s";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (res_inst_tac [("act", "NS3")] reachable_Acts 2);
-by (res_inst_tac [("act", "NS2")] reachable_Acts 3);
-by (res_inst_tac [("act", "NS1")] reachable_Acts 4);
+by (res_inst_tac [("act", "totalize_act NS3")] reachable_Acts 2);
+by (res_inst_tac [("act", "totalize_act NS2")] reachable_Acts 3);
+by (res_inst_tac [("act", "totalize_act NS1")] reachable_Acts 4);
by (rtac reachable_Init 5);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
-by (REPEAT_FIRST (rtac exI ));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def, totalize_act_def])));
+ (*Now ignore the possibility of identity transitions*)
+by (REPEAT_FIRST (resolve_tac [disjI1, exI]));
by possibility_tac;
result();
@@ -54,12 +54,23 @@
by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset()));
*)
+val [prem] =
+Goal "(!!act s s'. [| act: {Id, Fake, NS1, NS2, NS3}; \
+\ (s,s') \\<in> act; s \\<in> A |] ==> s': A') \
+\ ==> Nprg \\<in> A co A'";
+by (asm_full_simp_tac (simpset() addsimps [Nprg_def, mk_total_program_def]) 1);
+by (rtac constrainsI 1);
+by (rtac prem 1);
+by Auto_tac;
+qed "ns_constrainsI";
+
+
fun ns_constrains_tac i =
SELECT_GOAL
(EVERY [REPEAT (etac Always_ConstrainsI 1),
REPEAT (resolve_tac [StableI, stableI,
constrains_imp_Constrains] 1),
- rtac constrainsI 1,
+ rtac ns_constrainsI 1,
Full_simp_tac 1,
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS (clarify_tac (claset() delrules [impI,impCE])),
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Sat Feb 08 16:05:33 2003 +0100
@@ -54,6 +54,6 @@
constdefs
Nprg :: state program
(*Initial trace is empty*)
- "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
+ "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
end
--- a/src/HOL/UNITY/Simple/Reach.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy Sat Feb 08 16:05:33 2003 +0100
@@ -24,7 +24,7 @@
"asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
Rprg :: "state program"
- "Rprg == mk_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
+ "Rprg == mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
reach_invariant :: "state set"
"reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
@@ -81,7 +81,8 @@
lemma lemma1:
"FP Rprg \<subseteq> fixedpoint"
-apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def, auto)
+apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
+apply (auto simp add: stable_def constrains_def)
apply (drule bspec, assumption)
apply (simp add: Image_singleton image_iff)
apply (drule fun_cong, auto)
@@ -89,8 +90,8 @@
lemma lemma2:
"fixedpoint \<subseteq> FP Rprg"
-apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def)
-apply (auto intro!: ext)
+apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
+apply (auto intro!: ext simp add: stable_def constrains_def)
done
lemma FP_fixedpoint: "FP Rprg = fixedpoint"
@@ -104,7 +105,8 @@
*)
lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
-apply (auto simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def)
+apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
+apply (auto simp add: Compl_FP UN_UN_flatten)
apply (rule fun_upd_idem, force)
apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
done
--- a/src/HOL/UNITY/SubstAx.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Sat Feb 08 16:05:33 2003 +0100
@@ -21,7 +21,7 @@
"op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
-(*Resembles the previous definition of LeadsTo*)
+text{*Resembles the previous definition of LeadsTo*}
lemma LeadsTo_eq_leadsTo:
"A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
apply (unfold LeadsTo_def)
@@ -76,7 +76,7 @@
lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
by (simp add: LeadsTo_def)
-(*Useful with cancellation, disjunction*)
+text{*Useful with cancellation, disjunction*}
lemma LeadsTo_Un_duplicate:
"F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
by (simp add: Un_ac)
@@ -91,14 +91,14 @@
apply (blast intro: LeadsTo_Union)
done
-(*Binary union introduction rule*)
+text{*Binary union introduction rule*}
lemma LeadsTo_Un:
"[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
apply (subst Un_eq_Union)
apply (blast intro: LeadsTo_Union)
done
-(*Lets us look at the starting state*)
+text{*Lets us look at the starting state*}
lemma single_LeadsTo_I:
"(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
@@ -182,8 +182,8 @@
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done
-(*Set difference: maybe combine with leadsTo_weaken_L??
- This is the most useful form of the "disjunction" rule*)
+text{*Set difference: maybe combine with leadsTo_weaken_L??
+ This is the most useful form of the "disjunction" rule*}
lemma LeadsTo_Diff:
"[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |]
==> F \<in> A LeadsTo C"
@@ -198,18 +198,18 @@
done
-(*Version with no index set*)
+text{*Version with no index set*}
lemma LeadsTo_UN_UN_noindex:
"(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
by (blast intro: LeadsTo_UN_UN)
-(*Version with no index set*)
+text{*Version with no index set*}
lemma all_LeadsTo_UN_UN:
"\<forall>i. F \<in> (A i) LeadsTo (A' i)
==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
by (blast intro: LeadsTo_UN_UN)
-(*Binary union version*)
+text{*Binary union version*}
lemma LeadsTo_Un_Un:
"[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]
==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
@@ -247,18 +247,18 @@
done
-(** The impossibility law **)
+text{*The impossibility law*}
-(*The set "A" may be non-empty, but it contains no reachable states*)
-lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)"
+text{*The set "A" may be non-empty, but it contains no reachable states*}
+lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)"
apply (simp add: LeadsTo_def Always_eq_includes_reachable)
apply (drule leadsTo_empty, auto)
done
-(** PSP: Progress-Safety-Progress **)
+subsection{*PSP: Progress-Safety-Progress*}
-(*Special case of PSP: Misra's "stable conjunction"*)
+text{*Special case of PSP: Misra's "stable conjunction"*}
lemma PSP_Stable:
"[| F \<in> A LeadsTo A'; F \<in> Stable B |]
==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
@@ -336,7 +336,7 @@
==> F \<in> A LeadsTo B"
by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
-(*Integer version. Could generalize from 0 to any lower bound*)
+text{*Integer version. Could generalize from 0 to any lower bound*}
lemma integ_0_le_induct:
"[| F \<in> Always {s. (0::int) \<le> f s};
!! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo
--- a/src/HOL/UNITY/UNITY.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/UNITY.thy Sat Feb 08 16:05:33 2003 +0100
@@ -50,12 +50,12 @@
invariant :: "'a set => 'a program set"
"invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
- (*Polymorphic in both states and the meaning of \<le> *)
increasing :: "['a => 'b::{order}] => 'a program set"
+ --{*Polymorphic in both states and the meaning of @{text "\<le>"}*}
"increasing f == \<Inter>z. stable {s. z \<le> f s}"
-(*Perhaps equalities.ML shouldn't add this in the first place!*)
+text{*Perhaps equalities.ML shouldn't add this in the first place!*}
declare image_Collect [simp del]
(*** The abstract type of programs ***)
@@ -83,14 +83,14 @@
(** Inspectors for type "program" **)
lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
-by (auto simp add: program_typedef)
+by (simp add: program_typedef)
lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
-by (auto simp add: program_typedef)
+by (simp add: program_typedef)
lemma AllowedActs_eq [simp]:
"AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
-by (auto simp add: program_typedef)
+by (simp add: program_typedef)
(** Equality for UNITY programs **)
@@ -121,38 +121,6 @@
by (blast intro: program_equalityI program_equalityE)
-(*** These rules allow "lazy" definition expansion
- They avoid expanding the full program, which is a large expression
-***)
-
-lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init"
-by auto
-
-lemma def_prg_Acts:
- "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"
-by auto
-
-lemma def_prg_AllowedActs:
- "F == mk_program (init,acts,allowed)
- ==> AllowedActs F = insert Id allowed"
-by auto
-
-(*The program is not expanded, but its Init and Acts are*)
-lemma def_prg_simps:
- "[| F == mk_program (init,acts,allowed) |]
- ==> Init F = init & Acts F = insert Id acts"
-by simp
-
-(*An action is expanded only if a pair of states is being tested against it*)
-lemma def_act_simp:
- "[| act == {(s,s'). P s s'} |] ==> ((s,s') \<in> act) = P s s'"
-by auto
-
-(*A set is expanded only if an element is being tested against it*)
-lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
-by auto
-
-
(*** co ***)
lemma constrainsI:
@@ -176,12 +144,12 @@
lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
by (unfold constrains_def, blast)
-(*monotonic in 2nd argument*)
+text{*monotonic in 2nd argument*}
lemma constrains_weaken_R:
"[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
by (unfold constrains_def, blast)
-(*anti-monotonic in 1st argument*)
+text{*anti-monotonic in 1st argument*}
lemma constrains_weaken_L:
"[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
by (unfold constrains_def, blast)
@@ -227,8 +195,8 @@
lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
by (unfold constrains_def, auto)
-(*The reasoning is by subsets since "co" refers to single actions
- only. So this rule isn't that useful.*)
+text{*The reasoning is by subsets since "co" refers to single actions
+ only. So this rule isn't that useful.*}
lemma constrains_trans:
"[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
by (unfold constrains_def, blast)
@@ -304,7 +272,7 @@
lemma invariantI: "[| Init F \<subseteq> A; F \<in> stable A |] ==> F \<in> invariant A"
by (simp add: invariant_def)
-(*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*)
+text{*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*}
lemma invariant_Int:
"[| F \<in> invariant A; F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
by (auto simp add: invariant_def stable_Int)
@@ -314,7 +282,6 @@
lemma increasingD:
"F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
-
by (unfold increasing_def, blast)
lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
@@ -341,8 +308,8 @@
==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
by (unfold constrains_def, blast)
-(*As above, but for the trivial case of a one-variable state, in which the
- state is identified with its one variable.*)
+text{*As above, but for the trivial case of a one-variable state, in which the
+ state is identified with its one variable.*}
lemma elimination_sing:
"(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
by (unfold constrains_def, blast)
@@ -376,4 +343,119 @@
lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
by blast
+
+subsection{*Partial versus Total Transitions*}
+
+constdefs
+ totalize_act :: "('a * 'a)set => ('a * 'a)set"
+ "totalize_act act == act \<union> diag (-(Domain act))"
+
+ totalize :: "'a program => 'a program"
+ "totalize F == mk_program (Init F,
+ totalize_act ` Acts F,
+ AllowedActs F)"
+
+ mk_total_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
+ => 'a program"
+ "mk_total_program args == totalize (mk_program args)"
+
+ all_total :: "'a program => bool"
+ "all_total F == \<forall>act \<in> Acts F. Domain act = UNIV"
+
+lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
+by (blast intro: sym [THEN image_eqI])
+
+
+text{*Basic properties*}
+
+lemma totalize_act_Id [simp]: "totalize_act Id = Id"
+by (simp add: totalize_act_def)
+
+lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"
+by (auto simp add: totalize_act_def)
+
+lemma Init_totalize [simp]: "Init (totalize F) = Init F"
+by (unfold totalize_def, auto)
+
+lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)"
+by (simp add: totalize_def insert_Id_image_Acts)
+
+lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"
+by (simp add: totalize_def)
+
+lemma totalize_constrains_iff [simp]: "(totalize F \<in> A co B) = (F \<in> A co B)"
+by (simp add: totalize_def totalize_act_def constrains_def, blast)
+
+lemma totalize_stable_iff [simp]: "(totalize F \<in> stable A) = (F \<in> stable A)"
+by (simp add: stable_def)
+
+lemma totalize_invariant_iff [simp]:
+ "(totalize F \<in> invariant A) = (F \<in> invariant A)"
+by (simp add: invariant_def)
+
+lemma all_total_totalize: "all_total (totalize F)"
+by (simp add: totalize_def all_total_def)
+
+lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"
+by (force simp add: totalize_act_def)
+
+lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)"
+apply (simp add: all_total_def totalize_def)
+apply (rule program_equalityI)
+ apply (simp_all add: Domain_iff_totalize_act image_def)
+done
+
+lemma all_total_iff_totalize: "all_total F = (totalize F = F)"
+apply (rule iffI)
+ apply (erule all_total_imp_totalize)
+apply (erule subst)
+apply (rule all_total_totalize)
+done
+
+lemma mk_total_program_constrains_iff [simp]:
+ "(mk_total_program args \<in> A co B) = (mk_program args \<in> A co B)"
+by (simp add: mk_total_program_def)
+
+
+subsection{*Rules for Lazy Definition Expansion*}
+
+text{*They avoid expanding the full program, which is a large expression*}
+
+lemma def_prg_Init:
+ "F == mk_total_program (init,acts,allowed) ==> Init F = init"
+by (simp add: mk_total_program_def)
+
+lemma def_prg_Acts:
+ "F == mk_total_program (init,acts,allowed)
+ ==> Acts F = insert Id (totalize_act ` acts)"
+by (simp add: mk_total_program_def)
+
+lemma def_prg_AllowedActs:
+ "F == mk_total_program (init,acts,allowed)
+ ==> AllowedActs F = insert Id allowed"
+by (simp add: mk_total_program_def)
+
+text{*An action is expanded if a pair of states is being tested against it*}
+lemma def_act_simp:
+ "act == {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
+by (simp add: mk_total_program_def)
+
+text{*A set is expanded only if an element is being tested against it*}
+lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
+by (simp add: mk_total_program_def)
+
+(** Inspectors for type "program" **)
+
+lemma Init_total_eq [simp]:
+ "Init (mk_total_program (init,acts,allowed)) = init"
+by (simp add: mk_total_program_def)
+
+lemma Acts_total_eq [simp]:
+ "Acts(mk_total_program(init,acts,allowed)) = insert Id (totalize_act`acts)"
+by (simp add: mk_total_program_def)
+
+lemma AllowedActs_total_eq [simp]:
+ "AllowedActs (mk_total_program (init,acts,allowed)) = insert Id allowed"
+by (auto simp add: mk_total_program_def)
+
end
--- a/src/HOL/UNITY/UNITY_tactics.ML Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Sat Feb 08 16:05:33 2003 +0100
@@ -72,6 +72,8 @@
(*UNITY*)
+val mk_total_program_def = thm "mk_total_program_def";
+val totalize_act_def = thm "totalize_act_def";
val constrains_def = thm "constrains_def";
val stable_def = thm "stable_def";
val invariant_def = thm "invariant_def";
@@ -91,7 +93,6 @@
val def_prg_Init = thm "def_prg_Init";
val def_prg_Acts = thm "def_prg_Acts";
val def_prg_AllowedActs = thm "def_prg_AllowedActs";
-val def_prg_simps = thm "def_prg_simps";
val def_act_simp = thm "def_act_simp";
val def_set_simp = thm "def_set_simp";
val constrainsI = thm "constrainsI";
@@ -140,13 +141,14 @@
val Int_Union_Union = thm "Int_Union_Union";
val Image_less_than = thm "Image_less_than";
val Image_inverse_less_than = thm "Image_inverse_less_than";
+val totalize_constrains_iff = thm "totalize_constrains_iff";
(*WFair*)
val stable_transient_empty = thm "stable_transient_empty";
val transient_strengthen = thm "transient_strengthen";
val transientI = thm "transientI";
+val totalize_transientI = thm "totalize_transientI";
val transientE = thm "transientE";
-val transient_UNIV = thm "transient_UNIV";
val transient_empty = thm "transient_empty";
val ensuresI = thm "ensuresI";
val ensuresD = thm "ensuresD";
@@ -415,12 +417,14 @@
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 def_total_prg_Allowed = thm "def_total_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";
+val totalize_JN = thm "totalize_JN";
(*Comp*)
val preserves_def = thm "preserves_def";
@@ -670,11 +674,6 @@
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";
@@ -751,14 +750,19 @@
(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I)
-(*proves "co" properties when the program is specified*)
+(*Proves "co" properties when the program is specified. Any use of invariants
+ (from weak constrains) must have been done already.*)
fun gen_constrains_tac(cs,ss) i =
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
+ (*reduce the fancy safety properties to "constrains"*)
REPEAT (etac Always_ConstrainsI 1
ORELSE
resolve_tac [StableI, stableI,
constrains_imp_Constrains] 1),
+ (*for safety, the totalize operator can be ignored*)
+ simp_tac (HOL_ss addsimps
+ [mk_total_program_def, totalize_constrains_iff]) 1,
rtac constrainsI 1,
full_simp_tac ss 1,
REPEAT (FIRSTGOAL (etac disjE)),
@@ -774,8 +778,9 @@
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,
+ simp_tac (ss addsimps [mk_total_program_def]) 2,
+ res_inst_tac [("act", sact)] totalize_transientI 2
+ ORELSE 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,
--- a/src/HOL/UNITY/Union.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Union.thy Sat Feb 08 16:05:33 2003 +0100
@@ -32,7 +32,7 @@
SKIP :: "'a program"
"SKIP == mk_program (UNIV, {}, UNIV)"
- (*Characterizes safety properties. Used with specifying AllowedActs*)
+ (*Characterizes safety properties. Used with specifying Allowed*)
safety_prop :: "'a program set => bool"
"safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
@@ -316,10 +316,10 @@
subsection{*the ok and OK relations*}
lemma ok_SKIP1 [iff]: "SKIP ok F"
-by (auto simp add: ok_def)
+by (simp add: ok_def)
lemma ok_SKIP2 [iff]: "F ok SKIP"
-by (auto simp add: ok_def)
+by (simp add: ok_def)
lemma ok_Join_commute:
"(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
@@ -332,7 +332,8 @@
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)
+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)
@@ -374,7 +375,7 @@
lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
by (auto simp add: OK_iff_ok ok_iff_Allowed)
-subsection{*@{text safety_prop}, for reasoning about
+subsection{*@{term safety_prop}, for reasoning about
given instances of "ok"*}
lemma safety_prop_Acts_iff:
@@ -389,11 +390,6 @@
"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 \<subseteq> B)"
by (simp add: safety_prop_def constrains_def, blast)
@@ -413,9 +409,35 @@
"(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
by (auto simp add: safety_prop_def, blast)
+lemma def_prg_Allowed:
+ "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]
+ ==> Allowed F = X"
+by (simp add: Allowed_eq)
+
+lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F"
+by (simp add: Allowed_def)
+
+lemma def_total_prg_Allowed:
+ "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]
+ ==> Allowed F = X"
+by (simp add: mk_total_program_def def_prg_Allowed)
+
lemma def_UNION_ok_iff:
"[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]
==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
by (auto simp add: ok_def safety_prop_Acts_iff)
+text{*The union of two total programs is total.*}
+lemma totalize_Join: "totalize F Join totalize G = totalize (F Join G)"
+by (simp add: program_equalityI totalize_def Join_def image_Un)
+
+lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F Join G)"
+by (simp add: all_total_def, blast)
+
+lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)"
+by (simp add: program_equalityI totalize_def JOIN_def image_UN)
+
+lemma all_total_JN: "(!!i. i\<in>I ==> all_total (F i)) ==> all_total(\<Squnion>i\<in>I. F i)"
+by (simp add: all_total_iff_totalize totalize_JN [symmetric])
+
end
--- a/src/HOL/UNITY/WFair.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/WFair.thy Sat Feb 08 16:05:33 2003 +0100
@@ -3,21 +3,44 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Weak Fairness versions of transient, ensures, leadsTo.
+Conditional Fairness versions of transient, ensures, leadsTo.
From Misra, "A Logic for Concurrent Programming", 1994
*)
-header{*Progress under Weak Fairness*}
+header{*Progress*}
theory WFair = UNITY:
+text{*The original version of this theory was based on weak fairness. (Thus,
+the entire UNITY development embodied this assumption, until February 2003.)
+Weak fairness states that if a command is enabled continuously, then it is
+eventually executed. Ernie Cohen suggested that I instead adopt unconditional
+fairness: every command is executed infinitely often.
+
+In fact, Misra's paper on "Progress" seems to be ambiguous about the correct
+interpretation, and says that the two forms of fairness are equivalent. They
+differ only on their treatment of partial transitions, which under
+unconditional fairness behave magically. That is because if there are partial
+transitions then there may be no fair executions, making all leads-to
+properties hold vacuously.
+
+Unconditional fairness has some great advantages. By distinguishing partial
+transitions from total ones that are the identity on part of their domain, it
+is more expressive. Also, by simplifying the definition of the transient
+property, it simplifies many proofs. A drawback is that some laws only hold
+under the assumption that all transitions are total. The best-known of these
+is the impossibility law for leads-to.
+*}
+
constdefs
- (*This definition specifies weak fairness. The rest of the theory
- is generic to all forms of fairness.*)
+ --{*This definition specifies conditional fairness. The rest of the theory
+ is generic to all forms of fairness. To get weak fairness, conjoin
+ the inclusion below with @{term "A \<subseteq> Domain act"}, which specifies
+ that the action is enabled over all of @{term A}.*}
transient :: "'a set => 'a program set"
- "transient A == {F. \<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A}"
+ "transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}"
ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60)
"A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
@@ -25,8 +48,8 @@
consts
- (*LEADS-TO constant for the inductive definition*)
leads :: "'a program => ('a set * 'a set) set"
+ --{*LEADS-TO constant for the inductive definition*}
inductive "leads F"
@@ -41,12 +64,12 @@
constdefs
- (*visible version of the LEADS-TO relation*)
leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60)
+ --{*visible version of the LEADS-TO relation*}
"A leadsTo B == {F. (A,B) \<in> leads F}"
- (*wlt F B is the largest set that leads to B*)
wlt :: "['a program, 'a set] => 'a set"
+ --{*predicate transformer: the largest set that leads to @{term B}*}
"wlt F B == Union {A. F \<in> A leadsTo B}"
syntax (xsymbols)
@@ -55,9 +78,17 @@
subsection{*transient*}
+lemma stable_transient:
+ "[| F \<in> stable A; F \<in> transient A |] ==> \<exists>act\<in>Acts F. A \<subseteq> - (Domain act)"
+apply (simp add: stable_def constrains_def transient_def, clarify)
+apply (rule rev_bexI, auto)
+done
+
lemma stable_transient_empty:
- "[| F \<in> stable A; F \<in> transient A |] ==> A = {}"
-by (unfold stable_def constrains_def transient_def, blast)
+ "[| F \<in> stable A; F \<in> transient A; all_total F |] ==> A = {}"
+apply (drule stable_transient, assumption)
+apply (simp add: all_total_def)
+done
lemma transient_strengthen:
"[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B"
@@ -66,22 +97,34 @@
done
lemma transientI:
- "[| act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |] ==> F \<in> transient A"
+ "[| act: Acts F; act``A \<subseteq> -A |] ==> F \<in> transient A"
by (unfold transient_def, blast)
lemma transientE:
"[| F \<in> transient A;
- !!act. [| act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |] ==> P |]
+ !!act. [| act: Acts F; act``A \<subseteq> -A |] ==> P |]
==> P"
by (unfold transient_def, blast)
-lemma transient_UNIV [simp]: "transient UNIV = {}"
-by (unfold transient_def, blast)
-
lemma transient_empty [simp]: "transient {} = UNIV"
by (unfold transient_def, auto)
+text{*This equation recovers the notion of weak fairness. A totalized
+ program satisfies a transient assertion just if the original program
+ contains a suitable action that is also enabled.*}
+lemma totalize_transient_iff:
+ "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
+apply (simp add: totalize_def totalize_act_def transient_def
+ Un_Image Un_subset_iff, safe)
+apply (blast intro!: rev_bexI)+
+done
+
+lemma totalize_transientI:
+ "[| act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |]
+ ==> totalize F \<in> transient A"
+by (simp add: totalize_transient_iff, blast)
+
subsection{*ensures*}
lemma ensuresI:
@@ -98,7 +141,7 @@
apply (blast intro: constrains_weaken transient_strengthen)
done
-(*The L-version (precondition strengthening) fails, but we have this*)
+text{*The L-version (precondition strengthening) fails, but we have this*}
lemma stable_ensures_Int:
"[| F \<in> stable C; F \<in> A ensures B |]
==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
@@ -134,7 +177,7 @@
lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
-(*Useful with cancellation, disjunction*)
+text{*Useful with cancellation, disjunction*}
lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
by (simp add: Un_ac)
@@ -142,7 +185,7 @@
"F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
by (simp add: Un_ac)
-(*The Union introduction rule as we should have liked to state it*)
+text{*The Union introduction rule as we should have liked to state it*}
lemma leadsTo_Union:
"(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
apply (unfold leadsTo_def)
@@ -162,7 +205,7 @@
apply (blast intro: leadsTo_Union)
done
-(*Binary union introduction rule*)
+text{*Binary union introduction rule*}
lemma leadsTo_Un:
"[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
apply (subst Un_eq_Union)
@@ -174,7 +217,7 @@
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
-(*The INDUCTION rule as we should have liked to state it*)
+text{*The INDUCTION rule as we should have liked to state it*}
lemma leadsTo_induct:
"[| F \<in> za leadsTo zb;
!!A B. F \<in> A ensures B ==> P A B;
@@ -203,16 +246,16 @@
(** Variant induction rule: on the preconditions for B **)
-(*Lemma is the weak version: can't see how to do it in one step*)
+text{*Lemma is the weak version: can't see how to do it in one step*}
lemma leadsTo_induct_pre_lemma:
"[| F \<in> za leadsTo zb;
P zb;
!!A B. [| F \<in> A ensures B; P B |] ==> P A;
!!S. \<forall>A \<in> S. P A ==> P (Union S)
|] ==> P za"
-(*by induction on this formula*)
+txt{*by induction on this formula*}
apply (subgoal_tac "P zb --> P za")
-(*now solve first subgoal: this formula is sufficient*)
+txt{*now solve first subgoal: this formula is sufficient*}
apply (blast intro: leadsTo_refl)
apply (erule leadsTo_induct)
apply (blast+)
@@ -240,7 +283,7 @@
"[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
by (blast intro: leadsTo_Trans subset_imp_leadsTo)
-(*Distributes over binary unions*)
+text{*Distributes over binary unions*}
lemma leadsTo_Un_distrib:
"F \<in> (A \<union> B) leadsTo C = (F \<in> A leadsTo C & F \<in> B leadsTo C)"
by (blast intro: leadsTo_Un leadsTo_weaken_L)
@@ -271,7 +314,7 @@
apply (blast intro: leadsTo_Union leadsTo_weaken_R)
done
-(*Binary union version*)
+text{*Binary union version*}
lemma leadsTo_Un_Un:
"[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]
==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
@@ -309,18 +352,17 @@
done
-
-(** The impossibility law **)
-
-lemma leadsTo_empty: "F \<in> A leadsTo {} ==> A={}"
+text{*The impossibility law*}
+lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
apply (erule leadsTo_induct_pre)
-apply (simp_all add: ensures_def constrains_def transient_def, blast)
+apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
+apply (drule bspec, assumption)+
+apply blast
done
+subsection{*PSP: Progress-Safety-Progress*}
-(** PSP: Progress-Safety-Progress **)
-
-(*Special case of PSP: Misra's "stable conjunction"*)
+text{*Special case of PSP: Misra's "stable conjunction"*}
lemma psp_stable:
"[| F \<in> A leadsTo A'; F \<in> stable B |]
==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
@@ -452,7 +494,7 @@
subsection{*wlt*}
-(*Misra's property W3*)
+text{*Misra's property W3*}
lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
apply (unfold wlt_def)
apply (blast intro!: leadsTo_Union)
@@ -463,17 +505,17 @@
apply (blast intro!: leadsTo_Union)
done
-(*Misra's property W2*)
+text{*Misra's property W2*}
lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
-(*Misra's property W4*)
+text{*Misra's property W4*}
lemma wlt_increasing: "B \<subseteq> wlt F B"
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
done
-(*Used in the Trans case below*)
+text{*Used in the Trans case below*}
lemma lemma1:
"[| B \<subseteq> A2;
F \<in> (A1 - B) co (A1 \<union> B);
@@ -481,18 +523,18 @@
==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
by (unfold constrains_def, clarify, blast)
-(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
+text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
lemma leadsTo_123:
"F \<in> A leadsTo A'
==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
apply (erule leadsTo_induct)
-(*Basis*)
-apply (blast dest: ensuresD)
-(*Trans*)
-apply clarify
-apply (rule_tac x = "Ba \<union> Bb" in exI)
-apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
-(*Union*)
+ txt{*Basis*}
+ apply (blast dest: ensuresD)
+ txt{*Trans*}
+ apply clarify
+ apply (rule_tac x = "Ba \<union> Bb" in exI)
+ apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
+txt{*Union*}
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
apply (auto intro: leadsTo_UN)
@@ -502,7 +544,7 @@
done
-(*Misra's property W5*)
+text{*Misra's property W5*}
lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
proof -
from wlt_leadsTo [of F B, THEN leadsTo_123]