A new approach, using simp_of_act and simp_of_set to activate definitions when
necessary
--- a/src/HOL/UNITY/Constrains.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML Thu Sep 03 16:40:02 1998 +0200
@@ -252,19 +252,15 @@
val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
-(** main_def defines the main program as a set;
- cmd_defs defines the separate commands
-**)
-
(*proves "constrains" properties when the program is specified*)
-fun constrains_tac (main_def::cmd_defs) =
+val constrains_tac =
SELECT_GOAL
(EVERY [REPEAT (resolve_tac [StableI, stableI,
constrains_imp_Constrains] 1),
rtac constrainsI 1,
- full_simp_tac (simpset() addsimps [main_def]) 1,
+ Full_simp_tac 1,
REPEAT_FIRST (etac disjE),
ALLGOALS Clarify_tac,
- ALLGOALS (asm_full_simp_tac (simpset() addsimps cmd_defs))]);
+ ALLGOALS Asm_full_simp_tac]);
--- a/src/HOL/UNITY/Handshake.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML Thu Sep 03 16:40:02 1998 +0200
@@ -11,38 +11,41 @@
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper "split_all_tac";
+Addsimps [prgF_def RS def_prg_simps];
+Addsimps [prgG_def RS def_prg_simps];
+Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
+
(*Simplification for records*)
Addsimps (thms"state.update_defs");
-Addsimps [invFG_def];
+Addsimps [simp_of_set invFG_def];
-Goalw [prgF_def, Join_def] "id : Acts (Join prgF prgG) ";
+Goalw [Join_def] "id : Acts (Join prgF prgG) ";
by (Simp_tac 1);
qed "id_in_Acts";
AddIffs [id_in_Acts];
-
-Goalw [prgF_def, prgG_def] "Invariant (Join prgF prgG) invFG";
+Goal "Invariant (Join prgF prgG) invFG";
by (rtac InvariantI 1);
by (Force_tac 1);
by (rtac (constrains_imp_Constrains RS StableI) 1);
by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
-by (constrains_tac [prgG_def,cmdG_def] 2);
+by (constrains_tac 2);
by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
-by (constrains_tac [prgF_def,cmdF_def] 1);
+by (constrains_tac 1);
qed "invFG";
Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \
\ ({s. NF s = k} Int {s. BB s})";
by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
-by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
-by (constrains_tac [prgF_def,cmdF_def] 1);
+by (ensures_tac "cmdG" 2);
+by (constrains_tac 1);
qed "lemma2_1";
Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
-by (constrains_tac [prgG_def,cmdG_def] 2);
-by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
+by (constrains_tac 2);
+by (ensures_tac "cmdF" 1);
qed "lemma2_2";
--- a/src/HOL/UNITY/Lift.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Sep 03 16:40:02 1998 +0200
@@ -7,20 +7,38 @@
*)
-(*To move 0 < metric n s out of the assumptions for case splitting*)
-val rev_mp' = read_instantiate_sg (sign_of thy)
- [("P", "0 < metric ?n ?s")] rev_mp;
+(*split_all_tac causes a big blow-up*)
+claset_ref() := claset() delSWrapper "split_all_tac";
+
+
+(** 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;
+
+val mov_metric2 = read_instantiate_sg (sign_of thy)
+ [("P", "?x = metric ?n ?s")] rev_mp;
+
+val mov_metric3 = read_instantiate_sg (sign_of thy)
+ [("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];
+
val Suc_lessD_contra = Suc_lessD COMP rev_contrapos;
val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra;
+Addsimps [Lprg_def RS def_prg_simps];
+
+Addsimps (map simp_of_act
+ [request_act_def, open_act_def, close_act_def,
+ req_up_def, req_down_def, move_up_def, move_down_def,
+ button_press_def]);
+
val always_defs = [above_def, below_def, queueing_def,
goingup_def, goingdown_def, ready_def];
-val cmd_defs = [Lprg_def,
- request_act_def, open_act_def, close_act_def,
- req_up_def, req_down_def, move_up_def, move_down_def,
- button_press_def];
+Addsimps (map simp_of_set always_defs);
Goalw [Lprg_def] "id : Acts Lprg";
by (Simp_tac 1);
@@ -40,9 +58,13 @@
less_not_refl2, less_not_refl3];
+(*Hoping to be faster than
+ asm_simp_tac (simpset() addsimps metric_simps
+ but sometimes it's slower*)
+val metric_simp_tac =
+ asm_simp_tac (simpset() addsimps [metric_def, vimage_def]) THEN'
+ asm_simp_tac (simpset() addsimps metric_simps);
-(*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "split_all_tac";
(*Simplification for records*)
Addsimps (thms"state.update_defs");
@@ -65,38 +87,37 @@
by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
qed "less_imp_le_pred";
-Goalw [Lprg_def] "Invariant Lprg open_stop";
+Goal "Invariant Lprg open_stop";
by (rtac InvariantI 1);
by (Force_tac 1);
-by (constrains_tac (cmd_defs@always_defs) 1);
+by (constrains_tac 1);
qed "open_stop";
-Goalw [Lprg_def] "Invariant Lprg stop_floor";
+Goal "Invariant Lprg stop_floor";
by (rtac InvariantI 1);
by (Force_tac 1);
-by (constrains_tac (cmd_defs@always_defs) 1);
+by (constrains_tac 1);
qed "stop_floor";
(*This one needs open_stop, which was proved above*)
Goal "Invariant Lprg open_move";
by (rtac InvariantI 1);
-br (open_stop RS Invariant_ConstrainsI RS StableI) 2;
-bw Lprg_def;
+by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
by (Force_tac 1);
-by (constrains_tac (cmd_defs@always_defs) 1);
+by (constrains_tac 1);
qed "open_move";
-Goalw [Lprg_def] "Invariant Lprg moving_up";
+Goal "Invariant Lprg moving_up";
by (rtac InvariantI 1);
by (Force_tac 1);
-by (constrains_tac (cmd_defs@always_defs) 1);
+by (constrains_tac 1);
by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
qed "moving_up";
-Goalw [Lprg_def] "Invariant Lprg moving_down";
+Goal "Invariant Lprg moving_down";
by (rtac InvariantI 1);
by (Force_tac 1);
-by (constrains_tac (cmd_defs@always_defs) 1);
+by (constrains_tac 1);
by Safe_tac;
by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
by (auto_tac (claset(),
@@ -105,10 +126,9 @@
Goal "Invariant Lprg bounded";
by (rtac InvariantI 1);
-br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2;
-bw Lprg_def;
+by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
by (Force_tac 1);
-by (constrains_tac (cmd_defs@always_defs) 1);
+by (constrains_tac 1);
by Safe_tac;
by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le]));
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
@@ -123,42 +143,33 @@
val abbrev_defs = [moving_def, stopped_def,
opened_def, closed_def, atFloor_def, Req_def];
-val defs = cmd_defs@always_defs@abbrev_defs;
+Addsimps (map simp_of_set abbrev_defs);
(** The HUG'93 paper mistakenly omits the Req n from these! **)
(** Lift_1 **)
-(*lem_lift_1_5*)
Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
by (cut_facts_tac [stop_floor] 1);
-by (ensures_tac defs "open_act" 1);
-by Auto_tac;
-qed "E_thm01";
+by (ensures_tac "open_act" 1);
+qed "E_thm01"; (*lem_lift_1_5*)
-(*lem_lift_1_1*)
Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
\ (Req n Int opened - atFloor n)";
by (cut_facts_tac [stop_floor] 1);
-by (ensures_tac defs "open_act" 1);
-by Auto_tac;
-qed "E_thm02";
+by (ensures_tac "open_act" 1);
+qed "E_thm02"; (*lem_lift_1_1*)
-(*lem_lift_1_2*)
Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
\ (Req n Int closed - (atFloor n - queueing))";
-by (ensures_tac defs "close_act" 1);
-by Auto_tac;
-qed "E_thm03";
+by (ensures_tac "close_act" 1);
+qed "E_thm03"; (*lem_lift_1_2*)
-
-(*lem_lift_1_7*)
Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
\ (opened Int atFloor n)";
-by (ensures_tac defs "open_act" 1);
-by Auto_tac;
-qed "E_thm04";
+by (ensures_tac "open_act" 1);
+qed "E_thm04"; (*lem_lift_1_7*)
(** Lift 2. Statements of thm05a and thm05b were wrong! **)
@@ -182,16 +193,16 @@
Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
\ ((closed Int goingup Int Req n) Un \
\ (closed Int goingdown Int Req n))";
-br subset_imp_LeadsTo 1;
-by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
+by (rtac subset_imp_LeadsTo 1);
+by (auto_tac (claset() addSEs [nat_neqE], simpset()));
qed "E_thm05c";
(*lift_2*)
Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
\ (moving Int Req n)";
-br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
-by (ensures_tac defs "req_down" 2);
-by (ensures_tac defs "req_up" 1);
+by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
+by (ensures_tac "req_down" 2);
+by (ensures_tac "req_up" 1);
by Auto_tac;
qed "lift_2";
@@ -212,18 +223,16 @@
Goal "0 < N ==> \
\ LeadsTo Lprg \
\ (moving Int Req n Int (metric n -`` {N}) Int \
-\ {s. floor s ~: req s} Int {s. up s}) \
+\ {s. floor s ~: req s} Int {s. up s}) \
\ (moving Int Req n Int (metric n -`` lessThan N))";
by (cut_facts_tac [moving_up] 1);
-by (ensures_tac defs "move_up" 1);
-by Auto_tac;
+by (ensures_tac "move_up" 1);
+by Safe_tac;
(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
-be (leI RS le_anti_sym RS sym) 1;
-by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
-by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
-by (REPEAT_FIRST (etac rev_mp'));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
-by (distinct_tac 1);
+by (etac (leI RS le_anti_sym RS sym) 1);
+by (REPEAT_FIRST (eresolve_tac mov_metrics));
+by (REPEAT_FIRST distinct_tac);
+by (ALLGOALS metric_simp_tac);
by (auto_tac
(claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)]
addIs [diff_Suc_less_diff],
@@ -242,16 +251,14 @@
\ {s. floor s ~: req s} - {s. up s}) \
\ (moving Int Req n Int (metric n -`` lessThan N))";
by (cut_facts_tac [moving_down] 1);
-by (ensures_tac defs "move_down" 1);
-by Auto_tac;
+by (ensures_tac "move_down" 1);
+by Safe_tac;
by (ALLGOALS distinct_tac);
by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
-be (leI RS le_anti_sym RS sym) 1;
-by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
-by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
-by (REPEAT_FIRST (etac rev_mp'));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+by (etac (leI RS le_anti_sym RS sym) 1);
+by (REPEAT_FIRST (eresolve_tac mov_metrics));
+by (ALLGOALS metric_simp_tac);
by (auto_tac
(claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
addIs [diff_le_Suc_diff, diff_less_Suc_diff],
@@ -263,7 +270,7 @@
Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n -`` {N}) Int \
\ {s. floor s ~: req s}) \
\ (moving Int Req n Int (metric n -`` lessThan N))";
-br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
+by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (etac E_thm12b 4);
by (etac E_thm12a 3);
by (rtac id_in_Acts 2);
@@ -278,11 +285,11 @@
\ ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \
\ (moving Int Req n Int (metric n -`` lessThan N))";
by (cut_facts_tac [bounded] 1);
-by (ensures_tac defs "req_up" 1);
+by (ensures_tac "req_up" 1);
by Auto_tac;
-by (ALLGOALS (eres_inst_tac [("P", "?x < metric n s")] notE));
-by (REPEAT_FIRST (etac rev_mp'));
+by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+ (*faster than metric_simp_tac or than using just metric_def*)
by (auto_tac (claset() addIs [diff_Suc_less_diff],
simpset() addsimps [arith1, arith2]));
qed "E_thm16a";
@@ -311,12 +318,12 @@
\ LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \
\ (moving Int Req n Int (metric n -`` lessThan N))";
by (cut_facts_tac [bounded] 1);
-by (ensures_tac defs "req_down" 1);
+by (ensures_tac "req_down" 1);
by Auto_tac;
-by (ALLGOALS (eres_inst_tac [("P", "?x < metric n s")] notE));
by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
-by (REPEAT_FIRST (etac rev_mp'));
+by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+ (*faster and better than metric_simp_tac *)
by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff],
simpset() addsimps [trans_le_add1, arith3, arith4]));
qed "E_thm16b";
@@ -346,19 +353,20 @@
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
i.e. the trivial disjunction, leading to an asymmetrical proof.*)
Goal "0<N ==> Req n Int (metric n -``{N}) <= goingup Un goingdown";
-by (asm_simp_tac (simpset() addsimps (defs@metric_simps)) 1);
-by (Blast_tac 1);
+by (asm_simp_tac
+ (simpset() addsimps (always_defs@abbrev_defs@[metric_def,vimage_def])) 1);
+by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm16c";
(*lift_5*)
Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N})) \
\ (moving Int Req n Int (metric n -`` lessThan N))";
-br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
+by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (etac E_thm16b 4);
by (etac E_thm16a 3);
by (rtac id_in_Acts 2);
-bd E_thm16c 1;
+by (dtac E_thm16c 1);
by (Blast_tac 1);
qed "lift_5";
@@ -367,9 +375,10 @@
(*lemma used to prove lem_lift_3_1*)
Goal "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n";
-be rev_mp 1;
-by (asm_simp_tac (simpset() addsimps metric_simps) 1);
-by Auto_tac;
+by (etac rev_mp 1);
+ (*MUCH faster than metric_simps*)
+by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
+by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "metric_eq_0D";
AddDs [metric_eq_0D];
@@ -379,7 +388,7 @@
Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0})) \
\ (stopped Int atFloor n)";
by (cut_facts_tac [bounded] 1);
-by (ensures_tac defs "request_act" 1);
+by (ensures_tac "request_act" 1);
by Auto_tac;
qed "E_thm11";
@@ -387,7 +396,7 @@
Goal "LeadsTo Lprg \
\ (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
\ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})";
-by (ensures_tac defs "request_act" 1);
+by (ensures_tac "request_act" 1);
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm13";
@@ -396,8 +405,8 @@
\ LeadsTo Lprg \
\ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
\ (opened Int Req n Int (metric n -`` {N}))";
-by (ensures_tac defs "open_act" 1);
-by (REPEAT_FIRST (etac rev_mp'));
+by (ensures_tac "open_act" 1);
+by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm14";
@@ -405,7 +414,7 @@
Goal "LeadsTo Lprg \
\ (opened Int Req n Int (metric n -`` {N})) \
\ (closed Int Req n Int (metric n -`` {N}))";
-by (ensures_tac defs "close_act" 1);
+by (ensures_tac "close_act" 1);
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm15";
@@ -423,36 +432,35 @@
Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
-br (allI RS LessThan_induct) 1;
+by (rtac (allI RS LessThan_induct) 1);
by (exhaust_tac "m" 1);
-auto();
-br E_thm11 1;
-br ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1;
-br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
-br lift_3_Req 4;
-br lift_4 3;
-auto();
+by Auto_tac;
+by (rtac E_thm11 1);
+by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
+by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
+by (rtac lift_3_Req 4);
+by (rtac lift_4 3);
+by Auto_tac;
qed "lift_3";
Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
-br LeadsTo_Trans 1;
-br (E_thm04 RS LeadsTo_Un) 2;
-br LeadsTo_Un_post' 2;
-br (E_thm01 RS LeadsTo_Trans_Un') 2;
-br (lift_3 RS LeadsTo_Trans_Un') 2;
-br (lift_2 RS LeadsTo_Trans_Un') 2;
-br (E_thm03 RS LeadsTo_Trans_Un') 2;
-br E_thm02 2;
-br (open_move RS Invariant_LeadsToI) 1;
-br (open_stop RS Invariant_LeadsToI) 1;
-br subset_imp_LeadsTo 1;
+by (rtac LeadsTo_Trans 1);
+by (rtac (E_thm04 RS LeadsTo_Un) 2);
+by (rtac LeadsTo_Un_post' 2);
+by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
+by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
+by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
+by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2);
+by (rtac E_thm02 2);
+by (rtac (open_move RS Invariant_LeadsToI) 1);
+by (rtac (open_stop RS Invariant_LeadsToI) 1);
+by (rtac subset_imp_LeadsTo 1);
by (rtac id_in_Acts 2);
-bws defs;
by (Clarify_tac 1);
(*stops simplification from looping*)
by (Full_simp_tac 1);
-by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
+by (Blast_tac 1);
qed "lift_1";
Close_locale;
--- a/src/HOL/UNITY/Lift.thy Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy Thu Sep 03 16:40:02 1998 +0200
@@ -4,8 +4,6 @@
Copyright 1998 University of Cambridge
The Lift-Control Example
-
-
*)
Lift = SubstAx +
--- a/src/HOL/UNITY/Mutex.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Thu Sep 03 16:40:02 1998 +0200
@@ -9,35 +9,27 @@
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper "split_all_tac";
-val cmd_defs = [Mprg_def,
- cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def,
- cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def];
+Addsimps [Mprg_def RS def_prg_simps];
-Goalw [Mprg_def] "id : Acts Mprg";
-by (Simp_tac 1);
-qed "id_in_Acts";
-AddIffs [id_in_Acts];
+Addsimps (map simp_of_act
+ [cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def,
+ cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def]);
+Addsimps (map simp_of_set
+ [invariantU_def, invariantV_def, bad_invariantU_def]);
(*Simplification for records*)
-val select_defs = thms"state.select_defs"
-and update_defs = thms"state.update_defs"
-and dest_defs = thms"state.dest_defs";
-
-Addsimps update_defs;
+Addsimps (thms"state.update_defs");
-Addsimps [invariantU_def, invariantV_def];
-
-
-Goalw [Mprg_def] "Invariant Mprg invariantU";
+Goal "Invariant Mprg invariantU";
by (rtac InvariantI 1);
-by (constrains_tac cmd_defs 2);
+by (constrains_tac 2);
by Auto_tac;
qed "invariantU";
-Goalw [Mprg_def] "Invariant Mprg invariantV";
+Goal "Invariant Mprg invariantV";
by (rtac InvariantI 1);
-by (constrains_tac cmd_defs 2);
+by (constrains_tac 2);
by Auto_tac;
qed "invariantV";
@@ -52,12 +44,10 @@
(*The bad invariant FAILS in cmd1V*)
-Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU";
+Goal "Invariant Mprg bad_invariantU";
by (rtac InvariantI 1);
-by (Force_tac 1);
-by (constrains_tac cmd_defs 1);
-by Auto_tac;
-by (safe_tac (claset() addSEs [le_SucE]));
+by (constrains_tac 2);
+by (auto_tac (claset() addSEs [le_SucE], simpset()));
by (Asm_full_simp_tac 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,
@@ -69,26 +59,22 @@
(*** Progress for U ***)
Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
-by (constrains_tac cmd_defs 1);
+by (constrains_tac 1);
qed "U_F0";
Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
-by (ensures_tac cmd_defs "cmd1U" 1);
-by Auto_tac;
+by (ensures_tac "cmd1U" 1);
qed "U_F1";
Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
by (cut_facts_tac [invariantU] 1);
-by (rewtac Mprg_def);
-by (ensures_tac cmd_defs "cmd2U" 1);
-by Auto_tac;
+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);
-by (ensures_tac cmd_defs "cmd4U" 2);
-by (ensures_tac cmd_defs "cmd3U" 1);
-by Auto_tac;
+by (ensures_tac "cmd4U" 2);
+by (ensures_tac "cmd3U" 1);
qed "U_F3";
Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
@@ -121,25 +107,22 @@
Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
-by (constrains_tac cmd_defs 1);
+by (constrains_tac 1);
qed "V_F0";
Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
-by (ensures_tac cmd_defs "cmd1V" 1);
-by Auto_tac;
+by (ensures_tac "cmd1V" 1);
qed "V_F1";
Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
by (cut_facts_tac [invariantV] 1);
-by (ensures_tac cmd_defs "cmd2V" 1);
-by Auto_tac;
+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);
-by (ensures_tac cmd_defs "cmd4V" 2);
-by (ensures_tac cmd_defs "cmd3V" 1);
-by Auto_tac;
+by (ensures_tac "cmd4V" 2);
+by (ensures_tac "cmd3V" 1);
qed "V_F3";
Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
--- a/src/HOL/UNITY/Reach.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Thu Sep 03 16:40:02 1998 +0200
@@ -19,22 +19,19 @@
AddSEs [ifE];
-val cmd_defs = [Rprg_def, asgt_def, fun_upd_def];
+Addsimps [Rprg_def RS def_prg_simps];
-Goalw [Rprg_def] "id : (Acts Rprg)";
-by (Simp_tac 1);
-qed "id_in_Acts";
-AddIffs [id_in_Acts];
+Addsimps [simp_of_act asgt_def];
(*All vertex sets are finite*)
AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
-Addsimps [reach_invariant_def];
+Addsimps [simp_of_set reach_invariant_def];
-Goalw [Rprg_def] "Invariant Rprg reach_invariant";
+Goal "Invariant Rprg reach_invariant";
by (rtac InvariantI 1);
by Auto_tac; (*for the initial state; proof of stability remains*)
-by (constrains_tac [Rprg_def, asgt_def] 1);
+by (constrains_tac 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
qed "reach_invariant";
@@ -42,28 +39,27 @@
(*** Fixedpoint ***)
(*If it reaches a fixedpoint, it has found a solution*)
-Goalw [fixedpoint_def, reach_invariant_def]
- "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
+Goalw [fixedpoint_def]
+ "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
by (rtac equalityI 1);
+by (auto_tac (claset() addSIs [ext], simpset()));
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
-by (auto_tac (claset() addSIs [ext], simpset()));
by (etac rtrancl_induct 1);
by Auto_tac;
qed "fixedpoint_invariant_correct";
-Goalw (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
- "FP (Acts Rprg) <= fixedpoint";
+Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
+ "FP (Acts Rprg) <= fixedpoint";
by Auto_tac;
-by (dtac bspec 1);
-by (Blast_tac 1);
+by (dtac bspec 1 THEN Blast_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
by (dtac fun_cong 1);
by Auto_tac;
val lemma1 = result();
-Goalw (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
- "fixedpoint <= FP (Acts Rprg)";
-by (auto_tac (claset() addIs [ext], simpset()));
+Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
+ "fixedpoint <= FP (Acts Rprg)";
+by (auto_tac (claset() addSIs [ext], simpset()));
val lemma2 = result();
Goal "FP (Acts Rprg) = fixedpoint";
@@ -79,9 +75,8 @@
Goal "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
by (simp_tac (simpset() addsimps
- ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym,
- Rprg_def, asgt_def])) 1);
-by Safe_tac;
+ ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1);
+by Auto_tac;
by (rtac fun_upd_idem 1);
by (Blast_tac 1);
by (Full_simp_tac 1);
@@ -121,7 +116,7 @@
by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
by (rtac LeadsTo_UN 1);
by Auto_tac;
-by (ensures_tac [Rprg_def, asgt_def] "asgt a b" 1);
+by (ensures_tac "asgt a b" 1);
by (Blast_tac 2);
by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
bd (metric_le RS le_anti_sym) 1;
@@ -130,8 +125,9 @@
qed "LeadsTo_Diff_fixedpoint";
Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
-by (rtac (LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R RS LeadsTo_Diff) 1);
-by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
+by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
+ subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
+by Auto_tac;
qed "LeadsTo_Un_fixedpoint";
--- a/src/HOL/UNITY/Reach.thy Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy Thu Sep 03 16:40:02 1998 +0200
@@ -34,7 +34,7 @@
"fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
metric :: state => nat
- "metric == (%s. card {v. ~ s v})"
+ "metric s == card {v. ~ s v}"
rules
--- a/src/HOL/UNITY/SubstAx.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Thu Sep 03 16:40:02 1998 +0200
@@ -401,12 +401,8 @@
qed "Finite_completion";
-(** main_def defines the main program as a set;
- cmd_defs defines the separate commands
-**)
-
(*proves "ensures/leadsTo" properties when the program is specified*)
-fun ensures_tac (main_def::cmd_defs) sact =
+fun ensures_tac sact =
SELECT_GOAL
(EVERY [REPEAT (Invariant_Int_tac 1),
etac Invariant_LeadsTo_Basis 1
@@ -414,11 +410,8 @@
REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
res_inst_tac [("act", sact)] transient_mem 2,
(*simplify the command's domain*)
- simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
- (*INSIST that the command belongs to the program*)
- force_tac (claset(), simpset() addsimps [main_def]) 2,
- constrains_tac (main_def::cmd_defs) 1,
- rewrite_goals_tac cmd_defs,
+ simp_tac (simpset() addsimps [Domain_def]) 3,
+ constrains_tac 1,
ALLGOALS Clarify_tac,
ALLGOALS Asm_full_simp_tac]);
--- a/src/HOL/UNITY/Traces.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Thu Sep 03 16:40:02 1998 +0200
@@ -12,7 +12,7 @@
Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
by Safe_tac;
by (etac traces.induct 2);
-be reachable.induct 1;
+by (etac reachable.induct 1);
by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
qed "reachable_equiv_traces";
@@ -21,11 +21,38 @@
qed "stable_reachable";
Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)";
-auto();
+by Auto_tac;
qed "Acts_eq";
Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)";
-auto();
+by Auto_tac;
qed "Init_eq";
AddIffs [Acts_eq, Init_eq];
+
+
+(*** These three rules allow "lazy" definition expansion ***)
+
+val [rew] = goal thy
+ "[| prg == (|Init=init, Acts=acts|) |] \
+\ ==> Init prg = init & Acts prg = acts";
+by (rewtac rew);
+by Auto_tac;
+qed "def_prg_simps";
+
+val [rew] = goal thy
+ "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
+by (rewtac rew);
+by Auto_tac;
+qed "def_act_simp";
+
+fun simp_of_act def = def RS def_act_simp;
+
+val [rew] = goal thy
+ "[| A == B |] ==> (x : A) = (x : B)";
+by (rewtac rew);
+by Auto_tac;
+qed "def_set_simp";
+
+fun simp_of_set def = def RS def_set_simp;
+
--- a/src/HOL/UNITY/Union.ML Wed Sep 02 16:52:06 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Thu Sep 03 16:40:02 1998 +0200
@@ -6,9 +6,6 @@
Unions of programs
From Misra's Chapter 5: Asynchronous Compositions of Programs
-
-NOT CLEAR WHETHER ALL THESE FORMS ARE NEEDED:
- Maybe Join instead of Un, and JOIN for UNION
*)