--- a/src/HOL/UNITY/Common.ML Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Tue Sep 29 15:58:47 1998 +0200
@@ -69,7 +69,7 @@
Goal "[| ALL m. Constrains prg {m} (maxfg m); \
\ ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
-\ n: common; id: Acts prg |] \
+\ n: common |] \
\ ==> LeadsTo prg (atMost n) common";
by (rtac LeadsTo_weaken_R 1);
by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
@@ -82,7 +82,7 @@
(*The "ALL m: -common" form echoes CMT6.*)
Goal "[| ALL m. Constrains prg {m} (maxfg m); \
\ ALL m: -common. LeadsTo prg {m} (greaterThan m); \
-\ n: common; id: Acts prg |] \
+\ n: common |] \
\ ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
by (rtac lemma 1);
by (ALLGOALS Asm_simp_tac);
--- a/src/HOL/UNITY/Constrains.ML Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML Tue Sep 29 15:58:47 1998 +0200
@@ -89,14 +89,14 @@
qed "ball_Constrains_INT";
Goalw [Constrains_def]
- "[| Constrains prg A A'; id: Acts prg |] ==> reachable prg Int A <= A'";
+ "Constrains prg A A' ==> reachable prg Int A <= A'";
by (dtac constrains_imp_subset 1);
-by (assume_tac 1);
-by (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]) 1);
+by (ALLGOALS
+ (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
qed "Constrains_imp_subset";
Goalw [Constrains_def]
- "[| id: Acts prg; Constrains prg A B; Constrains prg B C |] \
+ "[| Constrains prg A B; Constrains prg B C |] \
\ ==> Constrains prg A C";
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";
@@ -167,7 +167,7 @@
qed "Elimination_sing";
Goalw [Constrains_def, constrains_def]
- "[| Constrains prg A (A' Un B); Constrains prg B B'; id: Acts prg |] \
+ "[| Constrains prg A (A' Un B); Constrains prg B B' |] \
\ ==> Constrains prg A (A' Un B')";
by (Blast_tac 1);
qed "Constrains_cancel";
--- a/src/HOL/UNITY/Handshake.ML Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML Tue Sep 29 15:58:47 1998 +0200
@@ -20,11 +20,6 @@
Addsimps [simp_of_set invFG_def];
-Goalw [Join_def] "id : Acts (Join prgF prgG) ";
-by (Simp_tac 1);
-qed "id_in_Acts";
-AddIffs [id_in_Acts];
-
Goal "Invariant (Join prgF prgG) invFG";
by (rtac InvariantI 1);
by (Force_tac 1);
@@ -59,6 +54,5 @@
by (rtac lemma2_2 2);
by (rtac LeadsTo_Trans 1);
by (rtac lemma2_2 2);
-by (rtac (lemma2_1) 1);
-by Auto_tac;
+by (rtac lemma2_1 1);
qed "progress";
--- a/src/HOL/UNITY/Handshake.thy Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Handshake.thy Tue Sep 29 15:58:47 1998 +0200
@@ -22,7 +22,7 @@
prgF :: "state program"
"prgF == (|Init = {s. NF s = 0 & BB s},
- Acts = {id, cmdF}|)"
+ Acts0 = {cmdF}|)"
(*G's program*)
cmdG :: "(state*state) set"
@@ -30,7 +30,7 @@
prgG :: "state program"
"prgG == (|Init = {s. NG s = 0 & BB s},
- Acts = {id, cmdG}|)"
+ Acts0 = {cmdG}|)"
(*the joint invariant*)
invFG :: "state set"
--- a/src/HOL/UNITY/Lift.thy Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy Tue Sep 29 15:58:47 1998 +0200
@@ -118,8 +118,8 @@
(*for the moment, we OMIT button_press*)
"Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
- Acts = {id, request_act, open_act, close_act,
- req_up, req_down, move_up, move_down}|)"
+ Acts0 = {request_act, open_act, close_act,
+ req_up, req_down, move_up, move_down}|)"
(** Invariants **)
--- a/src/HOL/UNITY/Mutex.thy Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy Tue Sep 29 15:58:47 1998 +0200
@@ -63,9 +63,8 @@
Mprg :: state program
"Mprg == (|Init = {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0},
- Acts = {id,
- cmd0U, cmd1U, cmd2U, cmd3U, cmd4U,
- cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
+ Acts0 = {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U,
+ cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
(** The correct invariants **)
--- a/src/HOL/UNITY/NSP_Bad.thy Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.thy Tue Sep 29 15:58:47 1998 +0200
@@ -55,6 +55,6 @@
Nprg :: state program
(*Initial trace is empty*)
"Nprg == (|Init = {[]},
- Acts = {id, Fake, NS1, NS2, NS3}|)"
+ Acts0 = {Fake, NS1, NS2, NS3}|)"
end
--- a/src/HOL/UNITY/Reach.thy Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy Tue Sep 29 15:58:47 1998 +0200
@@ -25,7 +25,7 @@
Rprg :: state program
"Rprg == (|Init = {%v. v=init},
- Acts = insert id (UN (u,v): edges. {asgt u v})|)"
+ Acts0 = (UN (u,v): edges. {asgt u v})|)"
reach_invariant :: state set
"reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
--- a/src/HOL/UNITY/SubstAx.ML Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Tue Sep 29 15:58:47 1998 +0200
@@ -65,7 +65,7 @@
(*** Derived rules ***)
-Goal "id: Acts prg ==> LeadsTo prg A UNIV";
+Goal "LeadsTo prg A UNIV";
by (asm_simp_tac (simpset() addsimps [LeadsTo_def,
Int_lower1 RS subset_imp_leadsTo]) 1);
qed "LeadsTo_UNIV";
@@ -92,7 +92,7 @@
by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
qed "LeadsTo_Un";
-Goal "[| A <= B; id: Acts prg |] ==> LeadsTo prg A B";
+Goal "[| A <= B |] ==> LeadsTo prg A B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "subset_imp_LeadsTo";
@@ -105,20 +105,20 @@
by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
qed_spec_mp "LeadsTo_weaken_R";
-Goal "[| LeadsTo prg A A'; B <= A; id: Acts prg |] \
+Goal "[| LeadsTo prg A A'; B <= A |] \
\ ==> LeadsTo prg B A'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
qed_spec_mp "LeadsTo_weaken_L";
-Goal "[| LeadsTo prg A A'; id: Acts prg; \
+Goal "[| LeadsTo prg A A'; \
\ B <= A; A' <= B' |] \
\ ==> LeadsTo prg B B'";
by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
-Goal "[| reachable prg <= C; LeadsTo prg A A'; id: Acts prg; \
+Goal "[| reachable prg <= C; LeadsTo prg A A'; \
\ C Int B <= A; C Int A' <= B' |] \
\ ==> LeadsTo prg B B'";
by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
@@ -127,11 +127,11 @@
(** Two theorems for "proof lattices" **)
-Goal "[| id: Acts prg; LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
+Goal "[| LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
qed "LeadsTo_Un_post";
-Goal "[| id: Acts prg; LeadsTo prg A B; LeadsTo prg B C |] \
+Goal "[| LeadsTo prg A B; LeadsTo prg B C |] \
\ ==> LeadsTo prg (A Un B) C";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
LeadsTo_weaken_L, LeadsTo_Trans]) 1);
@@ -140,21 +140,15 @@
(** Distributive laws **)
-Goal "id: Acts prg ==> \
-\ LeadsTo prg (A Un B) C = \
-\ (LeadsTo prg A C & LeadsTo prg B C)";
+Goal "LeadsTo prg (A Un B) C = (LeadsTo prg A C & LeadsTo prg B C)";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Un_distrib";
-Goal "id: Acts prg ==> \
-\ LeadsTo prg (UN i:I. A i) B = \
-\ (ALL i : I. LeadsTo prg (A i) B)";
+Goal "LeadsTo prg (UN i:I. A i) B = (ALL i : I. LeadsTo prg (A i) B)";
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
qed "LeadsTo_UN_distrib";
-Goal "id: Acts prg ==> \
-\ LeadsTo prg (Union S) B = \
-\ (ALL A : S. LeadsTo prg A B)";
+Goal "LeadsTo prg (Union S) B = (ALL A : S. LeadsTo prg A B)";
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Union_distrib";
@@ -181,7 +175,7 @@
qed "Invariant_LeadsTo_Basis";
Goal "[| Invariant prg INV; \
-\ LeadsTo prg A A'; id: Acts prg; \
+\ LeadsTo prg A A'; \
\ INV Int B <= A; INV Int A' <= B' |] \
\ ==> LeadsTo prg B B'";
by (rtac Invariant_LeadsToI 1);
@@ -194,7 +188,7 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
-Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C; id: Acts prg |] \
+Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C |] \
\ ==> LeadsTo prg A C";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";
@@ -236,27 +230,26 @@
(** The cancellation law **)
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B'; \
-\ id: Acts prg |] \
+Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B' |] \
\ ==> LeadsTo prg A (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un_Un,
subset_imp_LeadsTo, LeadsTo_Trans]) 1);
qed "LeadsTo_cancel2";
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B' |] \
\ ==> LeadsTo prg A (A' Un B')";
by (rtac LeadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "LeadsTo_cancel_Diff2";
-Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B' |] \
\ ==> LeadsTo prg A (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
qed "LeadsTo_cancel1";
-Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B' |] \
\ ==> LeadsTo prg A (B' Un A')";
by (rtac LeadsTo_cancel1 1);
by (assume_tac 2);
@@ -291,24 +284,23 @@
qed "PSP_stable2";
Goalw [LeadsTo_def, Constrains_def]
- "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
+ "[| LeadsTo prg A A'; Constrains prg B B' |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
qed "PSP";
-Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A A'; Constrains prg B B' |] \
\ ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
qed "PSP2";
Goalw [Unless_def]
- "[| LeadsTo prg A A'; Unless prg B B'; id: Acts prg |] \
+ "[| LeadsTo prg A A'; Unless prg B B' |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
by (dtac PSP 1);
by (assume_tac 1);
by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken,
- subset_imp_LeadsTo]) 2);
-by (assume_tac 1);
+ subset_imp_LeadsTo]) 1);
qed "PSP_Unless";
@@ -317,20 +309,18 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
\ ALL m. LeadsTo prg (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: Acts prg |] \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
\ ==> LeadsTo prg A B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_wf_induct 1);
-by (assume_tac 2);
+by (Simp_tac 2);
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
qed "LeadsTo_wf_induct";
Goal "[| wf r; \
\ ALL m:I. LeadsTo prg (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: Acts prg |] \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
\ ==> LeadsTo prg A ((A - (f-``I)) Un B)";
by (etac LeadsTo_wf_induct 1);
by Safe_tac;
@@ -341,45 +331,37 @@
Goal "[| ALL m. LeadsTo prg (A Int f-``{m}) \
-\ ((A Int f-``(lessThan m)) Un B); \
-\ id: Acts prg |] \
+\ ((A Int f-``(lessThan m)) Un B) |] \
\ ==> LeadsTo prg A B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
-by (assume_tac 2);
by (Asm_simp_tac 1);
qed "LessThan_induct";
(*Integer version. Could generalize from #0 to any lower bound*)
-val [reach, prem, id] =
+val [reach, prem] =
Goal "[| reachable prg <= {s. #0 <= f s}; \
\ !! z. LeadsTo prg (A Int {s. f s = z}) \
-\ ((A Int {s. f s < z}) Un B); \
-\ id: Acts prg |] \
+\ ((A Int {s. f s < z}) Un B) |] \
\ ==> LeadsTo prg A B";
by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
by (simp_tac (simpset() addsimps [vimage_def]) 1);
br ([reach, prem] MRS reachable_LeadsTo_weaken) 1;
-by (auto_tac (claset(),
- simpset() addsimps [id, nat_eq_iff, nat_less_iff]));
+by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
qed "integ_0_le_induct";
Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m}) \
-\ ((A Int f-``(lessThan m)) Un B); \
-\ id: Acts prg |] \
+\ ((A Int f-``(lessThan m)) Un B) |] \
\ ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)";
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
by (rtac (wf_less_than RS Bounded_induct) 1);
-by (assume_tac 2);
by (Asm_simp_tac 1);
qed "LessThan_bounded_induct";
Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m}) \
-\ ((A Int f-``(greaterThan m)) Un B); \
-\ id: Acts prg |] \
+\ ((A Int f-``(greaterThan m)) Un B) |] \
\ ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
(wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
-by (assume_tac 2);
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
by (Clarify_tac 1);
by (case_tac "m<l" 1);
@@ -391,14 +373,14 @@
(*** Completion: Binary and General Finite versions ***)
Goal "[| LeadsTo prg A A'; Stable prg A'; \
-\ LeadsTo prg B B'; Stable prg B'; id: Acts prg |] \
+\ LeadsTo prg B B'; Stable prg B' |] \
\ ==> LeadsTo prg (A Int B) (A' Int B')";
by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
qed "Stable_completion";
-Goal "[| finite I; id: Acts prg |] \
+Goal "finite I \
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i)) --> \
\ (ALL i:I. Stable prg (A' i)) --> \
\ LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
@@ -409,8 +391,7 @@
Goal "[| LeadsTo prg A (A' Un C); Constrains prg A' (A' Un C); \
-\ LeadsTo prg B (B' Un C); Constrains prg B' (B' Un C); \
-\ id: Acts prg |] \
+\ LeadsTo prg B (B' Un C); Constrains prg B' (B' Un C) |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
Int_Un_distrib]) 1);
@@ -418,7 +399,7 @@
qed "Completion";
-Goal "[| finite I; id: Acts prg |] \
+Goal "[| finite I |] \
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) --> \
\ (ALL i:I. Constrains prg (A' i) (A' i Un C)) --> \
\ LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
--- a/src/HOL/UNITY/Traces.ML Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Tue Sep 29 15:58:47 1998 +0200
@@ -9,6 +9,13 @@
*)
+Goal "id: Acts prg";
+by (simp_tac (simpset() addsimps [Acts_def]) 1);
+qed "id_in_Acts";
+AddIffs [id_in_Acts];
+
+
+
Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
by Safe_tac;
by (etac traces.induct 2);
@@ -20,11 +27,12 @@
by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
qed "stable_reachable";
-Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)";
+Goalw [Acts_def]
+ "(act : Acts(|Init=init, Acts0=acts|)) = (act=id | act : acts)";
by Auto_tac;
qed "Acts_eq";
-Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)";
+Goal "(s : Init(|Init=init, Acts0=acts|)) = (s:init)";
by Auto_tac;
qed "Init_eq";
@@ -34,8 +42,8 @@
(*** These three rules allow "lazy" definition expansion ***)
val [rew] = goal thy
- "[| prg == (|Init=init, Acts=acts|) |] \
-\ ==> Init prg = init & Acts prg = acts";
+ "[| prg == (|Init=init, Acts0=acts|) |] \
+\ ==> Init prg = init & Acts prg = insert id acts";
by (rewtac rew);
by Auto_tac;
qed "def_prg_simps";
--- a/src/HOL/UNITY/Traces.thy Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy Tue Sep 29 15:58:47 1998 +0200
@@ -25,8 +25,13 @@
record 'a program =
- Init :: 'a set
- Acts :: "('a * 'a)set set"
+ Init :: 'a set
+ Acts0 :: "('a * 'a)set set"
+
+
+constdefs
+ Acts :: "'a program => ('a * 'a)set set"
+ "Acts prg == insert id (Acts0 prg)"
consts reachable :: "'a program => 'a set"
--- a/src/HOL/UNITY/Union.ML Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Tue Sep 29 15:58:47 1998 +0200
@@ -14,19 +14,27 @@
qed "Init_Join";
Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
-by (simp_tac (simpset() addsimps [Join_def]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Acts_def, Join_def]));
qed "Acts_Join";
Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
by (simp_tac (simpset() addsimps [JOIN_def]) 1);
qed "Init_JN";
-Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))";
-by (simp_tac (simpset() addsimps [JOIN_def]) 1);
+Goal "Acts (JN i:I. prg i) = insert id (UN i:I. Acts (prg i))";
+by (auto_tac (claset(),
+ simpset() addsimps [Acts_def, JOIN_def]));
qed "Acts_JN";
Addsimps [Init_Join, Init_JN];
+Goal "(JN x:insert a A. B x) = Join (B a) (JN x:A. B x)";
+by (simp_tac (simpset() addsimps [Acts_def, JOIN_def, Join_def]) 1);
+qed "JN_insert";
+Addsimps[JN_insert];
+
+
(** Theoretical issues **)
Goal "Join prgF prgG = Join prgG prgF";
@@ -34,7 +42,7 @@
qed "Join_commute";
Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
-by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1);
+by (simp_tac (simpset() addsimps Un_ac@[Join_def, Acts_def, Int_assoc]) 1);
qed "Join_assoc";
@@ -50,13 +58,20 @@
*)
-(**NOT PROVABLE because no "surjective pairing" for records
-Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
-by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
-qed "Join_Null";
-*)
+
+
(**NOT PROVABLE because no "surjective pairing" for records
+Goalw [Join_def, SKIP_def] "Join prgF SKIP = prgF";
+by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
+qed "Join_SKIP";
+
+ In order to prove Join_SKIP, we possibly need
+ "Acts0 = ... - {id}" in JOIN_def and Join_def. But then Join_absorb only
+ holds if id ~: Acts0(prg). Or else we need to change 'a program to
+ an abstract type! Then equality could be made to ignore Acts0.
+
+NOT PROVABLE because no "surjective pairing" for records
Goalw [Join_def] "Join prgF prgF = prgF";
by Auto_tac;
qed "Join_absorb";
@@ -64,10 +79,19 @@
+Goal "(JN G:{}. G) = SKIP";
+by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1);
+qed "JN_empty";
+Addsimps [JN_empty];
+
+
+
+
(*** Safety: constrains, stable, FP ***)
Goalw [constrains_def, JOIN_def]
- "constrains (Acts (JN i:I. prg i)) A B = \
+ "I ~= {} ==> \
+\ constrains (Acts (JN i:I. prg i)) A B = \
\ (ALL i:I. constrains (Acts (prg i)) A B)";
by Auto_tac;
qed "constrains_JN";
@@ -80,10 +104,11 @@
qed "Constrains_JN";
**)
-Goalw [constrains_def, Join_def]
- "constrains (Acts (Join prgF prgG)) A B = \
-\ (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
-by (simp_tac (simpset() addsimps [ball_Un]) 1);
+Goal "constrains (Acts (Join prgF prgG)) A B = \
+\ (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
+by (auto_tac
+ (claset(),
+ simpset() addsimps [constrains_def, Join_def, Acts_def, ball_Un]));
qed "constrains_Join";
Goal "[| constrains (Acts prgF) A A'; constrains (Acts prgG) B B' |] \
@@ -92,9 +117,9 @@
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "constrains_Join_weaken";
-Goalw [stable_def]
- "stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
-by (simp_tac (simpset() addsimps [constrains_JN]) 1);
+Goal "I ~= {} ==> \
+\ stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
+by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
qed "stable_JN";
Goal "stable (Acts (Join prgF prgG)) A = \
@@ -102,30 +127,32 @@
by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
qed "stable_Join";
-Goalw [FP_def] "FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
-by (simp_tac (simpset() addsimps [stable_JN, INTER_def]) 1);
+Goal "I ~= {} ==> FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
+by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
qed "FP_JN";
(*** Progress: transient, ensures ***)
-Goalw [transient_def, JOIN_def]
- "transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
-by (Simp_tac 1);
+Goal "I ~= {} ==> \
+\ transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
+by (auto_tac (claset(),
+ simpset() addsimps [transient_def, JOIN_def]));
qed "transient_JN";
-Goalw [transient_def, Join_def]
- "transient (Acts (Join prgF prgG)) A = \
-\ (transient (Acts prgF) A | transient (Acts prgG) A)";
-by (simp_tac (simpset() addsimps [bex_Un]) 1);
+Goal "transient (Acts (Join prgF prgG)) A = \
+\ (transient (Acts prgF) A | transient (Acts prgG) A)";
+by (auto_tac (claset(),
+ simpset() addsimps [bex_Un, Acts_def, transient_def,
+ Join_def]));
qed "transient_Join";
-Goalw [ensures_def]
- "ensures (Acts (JN i:I. prg i)) A B = \
-\ ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
-\ (EX i:I. ensures (Acts (prg i)) A B))";
+Goal "I ~= {} ==> \
+\ ensures (Acts (JN i:I. prg i)) A B = \
+\ ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
+\ (EX i:I. ensures (Acts (prg i)) A B))";
by (auto_tac (claset(),
- simpset() addsimps [constrains_JN, transient_JN]));
+ simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
qed "ensures_JN";
Goalw [ensures_def]
@@ -146,7 +173,7 @@
(*Premises cannot use Invariant because Stable prgF A is weaker than
stable (Acts prgG) A *)
-Goal "[| stable (Acts prgF) A; Init prgG <= A; stable (Acts prgG) A |] \
+Goal "[| stable (Acts prgF) A; Init prgG <= A; stable (Acts prgG) A |] \
\ ==> Invariant (Join prgF prgG) A";
by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
stable_Join]) 1);
--- a/src/HOL/UNITY/Union.thy Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Union.thy Tue Sep 29 15:58:47 1998 +0200
@@ -12,15 +12,15 @@
constdefs
JOIN :: ['a set, 'a => 'b program] => 'b program
- "JOIN I prg == (|Init = INT i:I. Init (prg i),
- Acts = UN i:I. Acts (prg i)|)"
+ "JOIN I prg == (|Init = INT i:I. Init (prg i),
+ Acts0 = UN i:I. Acts (prg i)|)"
Join :: ['a program, 'a program] => 'a program
- "Join prgF prgG == (|Init = Init prgF Int Init prgG,
- Acts = Acts prgF Un Acts prgG|)"
+ "Join prgF prgG == (|Init = Init prgF Int Init prgG,
+ Acts0 = Acts prgF Un Acts prgG|)"
- Null :: 'a program
- "Null == (|Init = UNIV, Acts = {id}|)"
+ SKIP :: 'a program
+ "SKIP == (|Init = UNIV, Acts0 = {}|)"
syntax
"@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)