--- a/src/HOL/UNITY/Handshake.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Handshake.thy Thu Oct 01 18:28:18 1998 +0200
@@ -21,16 +21,14 @@
"cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
prgF :: "state program"
- "prgF == (|Init = {s. NF s = 0 & BB s},
- Acts0 = {cmdF}|)"
+ "prgF == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
(*G's program*)
cmdG :: "(state*state) set"
"cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
prgG :: "state program"
- "prgG == (|Init = {s. NG s = 0 & BB s},
- Acts0 = {cmdG}|)"
+ "prgG == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
(*the joint invariant*)
invFG :: "state set"
--- a/src/HOL/UNITY/LessThan.ML Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML Thu Oct 01 18:28:18 1998 +0200
@@ -87,7 +87,7 @@
Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
-by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (simp_tac (simpset() addsimps [order_le_less]) 1);
by (Blast_tac 1);
qed "atLeast_Suc";
@@ -119,7 +119,7 @@
Addsimps [atMost_0];
Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
-by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1);
+by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
by (Blast_tac 1);
qed "atMost_Suc";
--- a/src/HOL/UNITY/Lift.ML Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Oct 01 18:28:18 1998 +0200
@@ -6,27 +6,6 @@
The Lift-Control Example
*)
-
-Addsimps [integ_of_Pls RS sym];
-(*AND ALSO int 1 = #1 ??*)
-
-
-(**INTDEF.ML**)
-Goal "(int m) + (int n + z) = int (m + n) + z";
-by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1);
-qed "zadd_int_left";
-
-
-(**INT.ML**)
-
-
-(**BIN.ML**)
-
- Goal "#0 <= int m";
- by (simp_tac (simpset_of Bin.thy addsimps [integ_of_Pls]) 1);
- qed "zero_zle_int";
- AddIffs [zero_zle_int];
-
Goal "~ z < w ==> (z < w + #1) = (z = w)";
by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
qed "not_zless_zless1_eq";
@@ -49,16 +28,16 @@
(** Rules to move "metric n s" out of the assumptions, for case splitting **)
val mov_metric1 = read_instantiate_sg (sign_of thy)
- [("P", "?x < metric ?n ?s")] rev_mp;
+ [("P", "?x < metric ?n ?s")] rev_mp;
val mov_metric2 = read_instantiate_sg (sign_of thy)
- [("P", "?x = metric ?n ?s")] rev_mp;
+ [("P", "?x = metric ?n ?s")] rev_mp;
val mov_metric3 = read_instantiate_sg (sign_of thy)
- [("P", "~ (?x < metric ?n ?s)")] rev_mp;
+ [("P", "~ (?x < metric ?n ?s)")] rev_mp;
val mov_metric4 = read_instantiate_sg (sign_of thy)
- [("P", "(?x <= metric ?n ?s)")] rev_mp;
+ [("P", "(?x <= metric ?n ?s)")] rev_mp;
(*The order in which they are applied seems to be critical...*)
val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
@@ -267,7 +246,7 @@
(** LEVEL 6 **)
by (ALLGOALS (asm_simp_tac (simpset() addsimps
[zle_def] @ metric_simps @ zcompare_rls)));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps int_0::zadd_ac)));
qed "E_thm12b";
(*lift_4*)
@@ -308,7 +287,8 @@
by Auto_tac;
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
+ (asm_simp_tac (simpset() addsimps [int_0, zle_def] @
+ metric_simps @ zcompare_rls)));
(** LEVEL 5 **)
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
by (etac exE 1);
--- a/src/HOL/UNITY/Lift.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy Thu Oct 01 18:28:18 1998 +0200
@@ -116,10 +116,10 @@
Lprg :: state program
(*for the moment, we OMIT button_press*)
- "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
+ "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
- Acts0 = {request_act, open_act, close_act,
- req_up, req_down, move_up, move_down}|)"
+ {request_act, open_act, close_act,
+ req_up, req_down, move_up, move_down})"
(** Invariants **)
--- a/src/HOL/UNITY/Mutex.ML Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Thu Oct 01 18:28:18 1998 +0200
@@ -37,7 +37,7 @@
(*The safety property: mutual exclusion*)
-Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}";
+Goal "(reachable Mprg) Int {s. MM s = #3 & NN s = #3} = {}";
by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
by Auto_tac;
qed "mutual_exclusion";
@@ -47,8 +47,15 @@
Goal "Invariant Mprg bad_invariantU";
by (rtac InvariantI 1);
by (constrains_tac 2);
-by (auto_tac (claset() addSEs [le_SucE], simpset()));
-by (Asm_full_simp_tac 1);
+by (Force_tac 1);
+(*Needs a decision procedure to simplify the resulting state*)
+by (auto_tac (claset(),
+ simpset_of Int.thy addsimps
+ [zadd_int, integ_of_Pls, integ_of_Min,
+ integ_of_BIT, le_int_Suc_eq]));
+by (dtac zle_trans 1 THEN assume_tac 1);
+by (full_simp_tac (simpset_of Int.thy) 1);
+by (asm_full_simp_tac (simpset() addsimps int_simps) 1);
(*Resulting state: n=1, p=false, m=4, u=false.
Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
violating the invariant!*)
@@ -56,43 +63,53 @@
getgoal 1;
+Goal "(#1 <= m & m <= #3) = (m = #1 | m = #2 | m = #3)";
+by (auto_tac (claset(),
+ simpset_of Int.thy addsimps
+ [zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min,
+ integ_of_BIT]));
+by (exhaust_tac "na" 1);
+by (exhaust_tac "nat" 2);
+by (exhaust_tac "n" 3);
+auto();
+qed "eq_123";
+
+
(*** Progress for U ***)
-Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
+Goalw [Unless_def] "Unless Mprg {s. MM s=#2} {s. MM s=#3}";
by (constrains_tac 1);
qed "U_F0";
-Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
+Goal "LeadsTo Mprg {s. MM s=#1} {s. PP s = VV s & MM s = #2}";
by (ensures_tac "cmd1U" 1);
qed "U_F1";
-Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
+Goal "LeadsTo Mprg {s. ~ PP s & MM s = #2} {s. MM s = #3}";
by (cut_facts_tac [invariantU] 1);
by (ensures_tac "cmd2U" 1);
qed "U_F2";
-Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}";
-by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1);
+Goal "LeadsTo Mprg {s. MM s = #3} {s. PP s}";
+by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1);
by (ensures_tac "cmd4U" 2);
by (ensures_tac "cmd3U" 1);
qed "U_F3";
-Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
+Goal "LeadsTo Mprg {s. MM s = #2} {s. PP s}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
val U_lemma2 = result();
-Goal "LeadsTo Mprg {s. MM s = 1} {s. PP s}";
+Goal "LeadsTo Mprg {s. MM s = #1} {s. PP s}";
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
val U_lemma1 = result();
-Goal "LeadsTo Mprg {s. 1 <= MM s & MM s <= 3} {s. PP s}";
-by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
- addcongs [rev_conj_cong]) 1);
-by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
+Goal "LeadsTo Mprg {s. #1 <= MM s & MM s <= #3} {s. PP s}";
+by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
U_lemma1, U_lemma2, U_F3] ) 1);
val U_lemma123 = result();
@@ -106,41 +123,39 @@
(*** Progress for V ***)
-Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
+Goalw [Unless_def] "Unless Mprg {s. NN s=#2} {s. NN s=#3}";
by (constrains_tac 1);
qed "V_F0";
-Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
+Goal "LeadsTo Mprg {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}";
by (ensures_tac "cmd1V" 1);
qed "V_F1";
-Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
+Goal "LeadsTo Mprg {s. PP s & NN s = #2} {s. NN s = #3}";
by (cut_facts_tac [invariantV] 1);
by (ensures_tac "cmd2V" 1);
qed "V_F2";
-Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}";
-by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1);
+Goal "LeadsTo Mprg {s. NN s = #3} {s. ~ PP s}";
+by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1);
by (ensures_tac "cmd4V" 2);
by (ensures_tac "cmd3V" 1);
qed "V_F3";
-Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
+Goal "LeadsTo Mprg {s. NN s = #2} {s. ~ PP s}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
val V_lemma2 = result();
-Goal "LeadsTo Mprg {s. NN s = 1} {s. ~ PP s}";
+Goal "LeadsTo Mprg {s. NN s = #1} {s. ~ PP s}";
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
val V_lemma1 = result();
-Goal "LeadsTo Mprg {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}";
-by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
- addcongs [rev_conj_cong]) 1);
-by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
+Goal "LeadsTo Mprg {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}";
+by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
V_lemma1, V_lemma2, V_F3] ) 1);
val V_lemma123 = result();
@@ -155,7 +170,7 @@
(** Absence of starvation **)
(*Misra's F6*)
-Goal "LeadsTo Mprg {s. MM s = 1} {s. MM s = 3}";
+Goal "LeadsTo Mprg {s. MM s = #1} {s. MM s = #3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac U_F2 2);
@@ -169,7 +184,7 @@
(*The same for V*)
-Goal "LeadsTo Mprg {s. NN s = 1} {s. NN s = 3}";
+Goal "LeadsTo Mprg {s. NN s = #1} {s. NN s = #3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac V_F2 2);
--- a/src/HOL/UNITY/Mutex.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy Thu Oct 01 18:28:18 1998 +0200
@@ -8,20 +8,10 @@
Mutex = SubstAx +
-(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
-syntax
- "3" :: nat ("3")
- "4" :: nat ("4")
-
-translations
- "3" == "Suc 2"
- "4" == "Suc 3"
-
-
record state =
PP :: bool
- MM :: nat
- NN :: nat
+ MM :: int
+ NN :: int
UU :: bool
VV :: bool
@@ -30,57 +20,57 @@
(** The program for process U **)
cmd0U :: "(state*state) set"
- "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}"
+ "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=#1|) & MM s = #0}"
cmd1U :: "(state*state) set"
- "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}"
+ "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=#2|) & MM s = #1}"
cmd2U :: "(state*state) set"
- "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}"
+ "cmd2U == {(s,s'). s' = s (|MM:=#3|) & ~ PP s & MM s = #2}"
cmd3U :: "(state*state) set"
- "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}"
+ "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=#4|) & MM s = #3}"
cmd4U :: "(state*state) set"
- "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}"
+ "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=#0|) & MM s = #4}"
(** The program for process V **)
cmd0V :: "(state*state) set"
- "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}"
+ "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=#1|) & NN s = #0}"
cmd1V :: "(state*state) set"
- "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}"
+ "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=#2|) & NN s = #1}"
cmd2V :: "(state*state) set"
- "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}"
+ "cmd2V == {(s,s'). s' = s (|NN:=#3|) & PP s & NN s = #2}"
cmd3V :: "(state*state) set"
- "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}"
+ "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=#4|) & NN s = #3}"
cmd4V :: "(state*state) set"
- "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}"
+ "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}"
Mprg :: state program
- "Mprg == (|Init = {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0},
- Acts0 = {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U,
- cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
+ "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0},
+ {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U,
+ cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})"
(** The correct invariants **)
invariantU :: "state set"
- "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
- (MM s = 3 --> ~ PP s)}"
+ "invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) &
+ (MM s = #3 --> ~ PP s)}"
invariantV :: "state set"
- "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) &
- (NN s = 3 --> PP s)}"
+ "invariantV == {s. (VV s = (#1 <= NN s & NN s <= #3)) &
+ (NN s = #3 --> PP s)}"
(** The faulty invariant (for U alone) **)
bad_invariantU :: "state set"
- "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
- (3 <= MM s & MM s <= 4 --> ~ PP s)}"
+ "bad_invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) &
+ (#3 <= MM s & MM s <= #4 --> ~ PP s)}"
end
--- a/src/HOL/UNITY/NSP_Bad.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.thy Thu Oct 01 18:28:18 1998 +0200
@@ -54,7 +54,6 @@
constdefs
Nprg :: state program
(*Initial trace is empty*)
- "Nprg == (|Init = {[]},
- Acts0 = {Fake, NS1, NS2, NS3}|)"
+ "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})"
end
--- a/src/HOL/UNITY/Reach.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy Thu Oct 01 18:28:18 1998 +0200
@@ -24,8 +24,7 @@
"asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
Rprg :: state program
- "Rprg == (|Init = {%v. v=init},
- Acts0 = (UN (u,v): edges. {asgt u v})|)"
+ "Rprg == mk_program ({%v. v=init}, 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/Token.ML Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Token.ML Thu Oct 01 18:28:18 1998 +0200
@@ -54,7 +54,7 @@
by (auto_tac (claset(),
simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
-by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI,
+by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, less_imp_le,
diff_add_assoc]) 2);
by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
--- a/src/HOL/UNITY/Traces.ML Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Thu Oct 01 18:28:18 1998 +0200
@@ -9,40 +9,44 @@
*)
+
+(*** The abstract type of programs ***)
+
+val rep_ss = simpset() addsimps
+ [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program,
+ Rep_Program_inverse, Abs_Program_inverse];
+
+
Goal "id: Acts prg";
-by (simp_tac (simpset() addsimps [Acts_def]) 1);
+by (cut_inst_tac [("x", "prg")] Rep_Program 1);
+by (auto_tac (claset(), rep_ss));
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);
-by (etac reachable.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
-qed "reachable_equiv_traces";
+Goal "Init (mk_program (init,acts)) = init";
+by (auto_tac (claset(), rep_ss));
+qed "Init_eq";
-Goal "acts <= Acts prg ==> stable acts (reachable prg)";
-by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
-qed "stable_reachable";
-
-Goalw [Acts_def]
- "(act : Acts(|Init=init, Acts0=acts|)) = (act=id | act : acts)";
-by Auto_tac;
+Goal "Acts (mk_program (init,acts)) = insert id acts";
+by (auto_tac (claset(), rep_ss));
qed "Acts_eq";
-Goal "(s : Init(|Init=init, Acts0=acts|)) = (s:init)";
-by Auto_tac;
-qed "Init_eq";
+Addsimps [Acts_eq, Init_eq];
+
-AddIffs [Acts_eq, Init_eq];
+Goal "[| Init prg = Init prg'; Acts prg = Acts prg' |] ==> prg = prg'";
+by (cut_inst_tac [("p", "Rep_Program prg")] surjective_pairing 1);
+by (auto_tac (claset(), rep_ss));
+by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1);
+by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1);
+qed "program_equalityI";
(*** These three rules allow "lazy" definition expansion ***)
val [rew] = goal thy
- "[| prg == (|Init=init, Acts0=acts|) |] \
+ "[| prg == mk_program (init,acts) |] \
\ ==> Init prg = init & Acts prg = insert id acts";
by (rewtac rew);
by Auto_tac;
@@ -64,3 +68,16 @@
fun simp_of_set def = def RS def_set_simp;
+
+(*** traces and reachable ***)
+
+Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
+by Safe_tac;
+by (etac traces.induct 2);
+by (etac reachable.induct 1);
+by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
+qed "reachable_equiv_traces";
+
+Goal "acts <= Acts prg ==> stable acts (reachable prg)";
+by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
+qed "stable_reachable";
--- a/src/HOL/UNITY/Traces.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy Thu Oct 01 18:28:18 1998 +0200
@@ -24,14 +24,18 @@
==> (s', s#evs) : traces Init Acts"
-record 'a program =
- Init :: 'a set
- Acts0 :: "('a * 'a)set set"
-
+typedef (Program)
+ 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). id:acts}"
constdefs
+ mk_program :: "('a set * ('a * 'a)set set) => 'a program"
+ "mk_program == %(init, acts). Abs_Program (init, insert id acts)"
+
+ Init :: "'a program => 'a set"
+ "Init prg == fst (Rep_Program prg)"
+
Acts :: "'a program => ('a * 'a)set set"
- "Acts prg == insert id (Acts0 prg)"
+ "Acts prg == snd (Rep_Program prg)"
consts reachable :: "'a program => 'a set"
--- a/src/HOL/UNITY/Union.ML Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Thu Oct 01 18:28:18 1998 +0200
@@ -14,8 +14,7 @@
qed "Init_Join";
Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
-by (auto_tac (claset(),
- simpset() addsimps [Acts_def, Join_def]));
+by (auto_tac (claset(), simpset() addsimps [Join_def]));
qed "Acts_Join";
Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
@@ -23,14 +22,14 @@
qed "Init_JN";
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]));
+by (auto_tac (claset(), simpset() addsimps [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);
+br program_equalityI 1;
+by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
qed "JN_insert";
Addsimps[JN_insert];
@@ -42,41 +41,18 @@
qed "Join_commute";
Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
-by (simp_tac (simpset() addsimps Un_ac@[Join_def, Acts_def, Int_assoc]) 1);
+by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
qed "Join_assoc";
-
-
-(*
-val field_defs = thms"program.field_defs";
-val dest_defs = thms"program.dest_defs";
-val dest_convs = thms"program.dest_convs";
-
-val update_defs = thms"program.update_defs";
-val make_defs = thms"program.make_defs";
-val update_convs = thms"program.update_convs";
-val simps = thms"program.simps";
-*)
-
-
-
-
-
-(**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);
+br program_equalityI 1;
+by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
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";
+br program_equalityI 1;
by Auto_tac;
qed "Join_absorb";
-*)
-
Goal "(JN G:{}. G) = SKIP";
@@ -93,7 +69,8 @@
"I ~= {} ==> \
\ constrains (Acts (JN i:I. prg i)) A B = \
\ (ALL i:I. constrains (Acts (prg i)) A B)";
-by Auto_tac;
+by (Simp_tac 1);
+by (Blast_tac 1);
qed "constrains_JN";
(**FAILS, I think; see 5.4.1, Substitution Axiom.
@@ -108,7 +85,7 @@
\ (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
by (auto_tac
(claset(),
- simpset() addsimps [constrains_def, Join_def, Acts_def, ball_Un]));
+ simpset() addsimps [constrains_def, Join_def, ball_Un]));
qed "constrains_Join";
Goal "[| constrains (Acts prgF) A A'; constrains (Acts prgG) B B' |] \
@@ -143,7 +120,7 @@
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,
+ simpset() addsimps [bex_Un, transient_def,
Join_def]));
qed "transient_Join";
--- a/src/HOL/UNITY/Union.thy Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Union.thy Thu Oct 01 18:28:18 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),
- Acts0 = UN i:I. Acts (prg i)|)"
+ "JOIN I prg == mk_program (INT i:I. Init (prg i),
+ UN i:I. Acts (prg i))"
Join :: ['a program, 'a program] => 'a program
- "Join prgF prgG == (|Init = Init prgF Int Init prgG,
- Acts0 = Acts prgF Un Acts prgG|)"
+ "Join prgF prgG == mk_program (Init prgF Int Init prgG,
+ Acts prgF Un Acts prgG)"
SKIP :: 'a program
- "SKIP == (|Init = UNIV, Acts0 = {}|)"
+ "SKIP == mk_program (UNIV, {})"
syntax
"@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)