diff -r 157c6663dedd -r 566f47250bd0 src/HOL/UNITY/Lift.ML
--- 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;