# HG changeset patch
# User paulson
# Date 840446240 -7200
# Node ID 6d572f96fb765ac8f97a2505a9aeb3f04a3adab7
# Parent  f535276171d18cf648932cf2912935977774148e
Tidied some proofs, maybe using less_SucE

diff -r f535276171d1 -r 6d572f96fb76 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Mon Aug 19 11:15:44 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML	Mon Aug 19 11:17:20 1996 +0200
@@ -13,7 +13,7 @@
 by (etac hoare.induct 1);
     by(ALLGOALS Asm_simp_tac);
   by(fast_tac rel_cs 1);
- by(fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (rtac allI 1);
 by (rtac allI 1);
 by (rtac impI 1);
@@ -23,26 +23,24 @@
 by(rename_tac "s t" 1);
 by (rewtac Gamma_def);  
 by(eres_inst_tac [("x","s")] allE 1);
-by (safe_tac comp_cs);
+by (Step_tac 1);
   by(ALLGOALS Asm_full_simp_tac);
 qed "hoare_sound";
 
 goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
 by(Simp_tac 1);
 br ext 1;
-by(fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "swp_SKIP";
 
 goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
 by(Simp_tac 1);
-br ext 1;
-by(fast_tac HOL_cs 1);
 qed "swp_Ass";
 
 goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
 by(Simp_tac 1);
 br ext 1;
-by(fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed "swp_Semi";
 
 goalw Hoare.thy [swp_def]
@@ -50,7 +48,7 @@
 \                                    (~b s --> swp d Q s))";
 by(Simp_tac 1);
 br ext 1;
-by(fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed "swp_If";
 
 goalw Hoare.thy [swp_def]
@@ -62,38 +60,38 @@
 goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
 by(stac C_While_If 1);
 by(Asm_simp_tac 1);
-by(fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "swp_While_False";
 
 Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
 
+(*Not suitable for rewriting: LOOPS!*)
+goal Hoare.thy "swp (WHILE b DO c) Q s = \
+\                 (if b s then swp (c;WHILE b DO c) Q s else Q s)";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+qed "swp_While_if";
+
+
 Delsimps [C_while];
 
+AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
+
 goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
 by(com.induct_tac "c" 1);
 by(ALLGOALS Simp_tac);
-    by(fast_tac (HOL_cs addIs [hoare.skip]) 1);
-   by(fast_tac (HOL_cs addIs [hoare.ass]) 1);
-  by(fast_tac (HOL_cs addIs [hoare.semi]) 1);
- by(safe_tac (HOL_cs addSIs [hoare.If]));
-  br hoare.conseq 1;
-    by(fast_tac HOL_cs 2);
-   by(fast_tac HOL_cs 2);
-  by(fast_tac HOL_cs 1);
- br hoare.conseq 1;
-   by(fast_tac HOL_cs 2);
-  by(fast_tac HOL_cs 2);
- by(fast_tac HOL_cs 1);
+by (REPEAT_FIRST Fast_tac);
+by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
+by (Step_tac 1);
 br hoare.conseq 1;
   be thin_rl 1;
-  by(fast_tac HOL_cs 1);
+  by (Fast_tac 1);
  br hoare.While 1;
  br hoare.conseq 1;
    be thin_rl 3;
    br allI 3;
    br impI 3;
    ba 3;
-  by(fast_tac HOL_cs 2);
+  by (Fast_tac 2);
  by(safe_tac HOL_cs);
  by(rotate_tac ~1 1);
  by(Asm_full_simp_tac 1);
@@ -103,7 +101,7 @@
 
 goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
 br (swp_is_pre RSN (2,hoare.conseq)) 1;
- by(fast_tac HOL_cs 2);
+ by (Fast_tac 2);
 by(rewrite_goals_tac [hoare_valid_def,swp_def]);
-by(fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "hoare_relative_complete";
diff -r f535276171d1 -r 6d572f96fb76 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Mon Aug 19 11:15:44 1996 +0200
+++ b/src/HOL/Lambda/Eta.ML	Mon Aug 19 11:17:20 1996 +0200
@@ -12,6 +12,7 @@
 open Eta;
 
 Addsimps eta.intrs;
+Addsimps [imp_disj];
 
 val eta_cases = map (eta.mk_cases db.simps)
     ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
@@ -32,22 +33,21 @@
 
 goal Arith.thy "i < j --> pred i < j";
 by(nat_ind_tac "j" 1);
-by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq])));
+by(ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
 by(nat_ind_tac "j1" 1);
-by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
+by(ALLGOALS Asm_simp_tac);
 qed_spec_mp "less_imp_pred_less";
 
 goal Arith.thy "i<j --> ~ pred j < i";
 by(nat_ind_tac "j" 1);
-by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq])));
-by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1);
+by(ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
 qed_spec_mp "less_imp_not_pred_less";
 Addsimps [less_imp_not_pred_less];
 
 goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i";
 by(nat_ind_tac "j" 1);
-by(ALLGOALS(simp_tac(simpset_of "Nat")));
-by(simp_tac(simpset_of "Nat" addsimps [less_Suc_eq])1);
+by(ALLGOALS Simp_tac);
+by(simp_tac(!simpset addsimps [less_Suc_eq])1);
 by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
 qed_spec_mp "less_interval1";
 
@@ -80,7 +80,7 @@
 by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
 by (dtac Suc_mono 1);
 by(dtac less_interval1 1 THEN atac 1);
-by(asm_full_simp_tac (simpset_of "Nat" addsimps [eq_sym_conv]) 1);
+by(asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
 by(dtac less_trans_Suc 1 THEN atac 1);
 by(Asm_full_simp_tac 1);
 qed "free_subst";
diff -r f535276171d1 -r 6d572f96fb76 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Mon Aug 19 11:15:44 1996 +0200
+++ b/src/HOL/MiniML/W.ML	Mon Aug 19 11:17:20 1996 +0200
@@ -150,6 +150,8 @@
 qed_spec_mp "new_tv_W";
 
 
+AddSEs [less_SucE];
+
 goal thy
      "!n a s t m v. W e a n = Ok (s,t,m) -->            \
 \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
@@ -219,7 +221,7 @@
 (* case Var n *)
 by (strip_tac 1);
 by (simp_tac (!simpset addcongs [conj_cong] 
-    setloop (split_tac [expand_if])) 1);
+	      setloop (split_tac [expand_if])) 1);
 by (eresolve_tac has_type_casesE 1); 
 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
 by (res_inst_tac [("x","id_subst")] exI 1);
@@ -236,7 +238,7 @@
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
 by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
-    setloop (split_tac [expand_bind]))) 1);
+			    setloop (split_tac [expand_bind]))) 1);
 
 (* case App e1 e2 *)
 by (strip_tac 1);
@@ -257,7 +259,7 @@
 by (safe_tac HOL_cs);
 by (fast_tac HOL_cs 1);
 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
-        conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
+			    conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
 
 by (subgoal_tac
   "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
@@ -272,11 +274,11 @@
 by (strip_tac 2);
 by (subgoal_tac "na ~=ma" 2);
 by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
-    new_tv_not_free_tv,new_tv_le]) 3);
+			    new_tv_not_free_tv,new_tv_le]) 3);
 by (case_tac "na:free_tv sa" 2);
 (* na ~: free_tv sa *)
 by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
-    setloop (split_tac [expand_if])) 3);
+		  setloop (split_tac [expand_if])) 3);
 (* na : free_tv sa *)
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 by (dtac eq_subst_tel_eq_free 2);
@@ -285,7 +287,7 @@
 by (case_tac "na:dom sa" 2);
 (* na ~: dom sa *)
 by (asm_full_simp_tac (!simpset addsimps [dom_def] 
-    setloop (split_tac [expand_if])) 3);
+		       setloop (split_tac [expand_if])) 3);
 (* na : dom sa *)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
@@ -295,9 +297,9 @@
 by (dtac new_tv_subst_tel 3);
 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
-    (!simpset addsimps [cod_def,free_tv_subst])) 3);
+	      (!simpset addsimps [cod_def,free_tv_subst])) 3);
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
-    setloop (split_tac [expand_if]))) 2);
+			    setloop (split_tac [expand_if]))) 2);
 
 by (Simp_tac 2);  
 by (rtac eq_free_eq_subst_te 2);