# HG changeset patch
# User paulson
# Date 904725433 -7200
# Node ID 771a68a468ccb97c778d935b931a33cb43bc7b8e
# Parent  c57c87628bb4e10f4ab8028e913d8953b7de7a9b
modified proofs for new constrains_tac and ensures_tac

diff -r c57c87628bb4 -r 771a68a468cc src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Wed Sep 02 10:36:49 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Wed Sep 02 10:37:13 1998 +0200
@@ -97,18 +97,19 @@
 by (rtac InvariantI 1);
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
+by Safe_tac;
 by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
 by (auto_tac (claset(),
 	      simpset() addsimps [gr_implies_gr0 RS le_pred_eq]));
 qed "moving_down";
 
-
 Goal "Invariant Lprg bounded";
 by (rtac InvariantI 1);
 br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2;
 bw Lprg_def;
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 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]));
 by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]));
@@ -133,6 +134,7 @@
 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";
 
 (*lem_lift_1_1*)
@@ -140,12 +142,14 @@
 \                  (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";
 
 (*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";
 
 
@@ -153,6 +157,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";
 
 
@@ -187,6 +192,7 @@
 br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
 by (ensures_tac defs "req_down" 2);
 by (ensures_tac defs "req_up" 1);
+by Auto_tac;
 qed "lift_2";
 
 
@@ -210,6 +216,7 @@
 \       (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;
 (*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);
@@ -236,6 +243,7 @@
 \       (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 (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*)
@@ -271,6 +279,8 @@
 \                      (moving Int Req n Int (metric n -`` lessThan N))";
 by (cut_facts_tac [bounded] 1);
 by (ensures_tac defs "req_up" 1);
+by Auto_tac;
+by (ALLGOALS (eres_inst_tac [("P", "?x < metric n s")] notE));
 by (REPEAT_FIRST (etac rev_mp'));
 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
 by (auto_tac (claset() addIs [diff_Suc_less_diff], 
@@ -302,6 +312,8 @@
 \                  (moving Int Req n Int (metric n -`` lessThan N))";
 by (cut_facts_tac [bounded] 1);
 by (ensures_tac defs "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 (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
@@ -357,7 +369,7 @@
 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);
-auto();
+by Auto_tac;
 qed "metric_eq_0D";
 
 AddDs [metric_eq_0D];
@@ -368,6 +380,7 @@
 \                  (stopped Int atFloor n)";
 by (cut_facts_tac [bounded] 1);
 by (ensures_tac defs "request_act" 1);
+by Auto_tac;
 qed "E_thm11";
 
 (*lem_lift_3_5*)
@@ -375,7 +388,7 @@
 \       (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 (asm_simp_tac (simpset() addsimps metric_simps) 1);
+by (auto_tac (claset(), simpset() addsimps metric_simps));
 qed "E_thm13";
 
 (*lem_lift_3_6*)
@@ -385,7 +398,7 @@
 \       (opened Int Req n Int (metric n -`` {N}))";
 by (ensures_tac defs "open_act" 1);
 by (REPEAT_FIRST (etac rev_mp'));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+by (auto_tac (claset(), simpset() addsimps metric_simps));
 qed "E_thm14";
 
 (*lem_lift_3_7*)
@@ -393,7 +406,7 @@
 \       (opened Int Req n Int (metric n -`` {N}))  \
 \       (closed Int Req n Int (metric n -`` {N}))";
 by (ensures_tac defs "close_act" 1);
-by (asm_simp_tac (simpset() addsimps metric_simps) 1);
+by (auto_tac (claset(), simpset() addsimps metric_simps));
 qed "E_thm15";
 
 
diff -r c57c87628bb4 -r 771a68a468cc src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Wed Sep 02 10:36:49 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Wed Sep 02 10:37:13 1998 +0200
@@ -56,6 +56,7 @@
 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 (Asm_full_simp_tac 1);
 (*Resulting state: n=1, p=false, m=4, u=false.  
@@ -73,18 +74,21 @@
 
 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;
 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;
 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;
 qed "U_F3";
 
 Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
@@ -122,17 +126,20 @@
 
 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;
 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;
 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;
 qed "V_F3";
 
 Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
diff -r c57c87628bb4 -r 771a68a468cc src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Wed Sep 02 10:36:49 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Wed Sep 02 10:37:13 1998 +0200
@@ -122,8 +122,11 @@
 by (rtac LeadsTo_UN 1);
 by Auto_tac;
 by (ensures_tac [Rprg_def, asgt_def] "asgt a b" 1);
-by (cut_facts_tac [metric_le RS le_imp_less_or_eq] 1);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
+bd (metric_le RS le_anti_sym) 1;
+by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
+	      simpset()));
 qed "LeadsTo_Diff_fixedpoint";
 
 Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";