# HG changeset patch
# User paulson
# Date 875182398 -7200
# Node ID 56facaebf3e38fdf16ae04583444a2112b581790
# Parent  40856b593501652943d11c6498426b0e4e1bada1
Changed some proofs to use Clarify_tac

diff -r 40856b593501 -r 56facaebf3e3 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu Sep 25 12:10:07 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Thu Sep 25 12:13:18 1997 +0200
@@ -125,7 +125,7 @@
 goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
 by (cut_inst_tac [("evs","evs")] lemma 1);
 by (cut_inst_tac [("evs","evs'")] lemma 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (res_inst_tac [("x","N")] exI 1);
 by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
 by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
@@ -138,7 +138,7 @@
 by (cut_inst_tac [("evs","evs")] lemma 1);
 by (cut_inst_tac [("evs","evs'")] lemma 1);
 by (cut_inst_tac [("evs","evs''")] lemma 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (res_inst_tac [("x","N")] exI 1);
 by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
 by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
@@ -181,7 +181,7 @@
 by (etac exE 1);
 by (cut_inst_tac [("evs","evs''")] 
     (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (Full_simp_tac 1);
 by (fast_tac (!claset addSEs [allE]) 1);
 qed "Key_supply3";
diff -r 40856b593501 -r 56facaebf3e3 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Thu Sep 25 12:10:07 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 25 12:13:18 1997 +0200
@@ -190,7 +190,7 @@
 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
 by (etac yahalom.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by (ALLGOALS Clarify_tac);
 by (ex_strip_tac 2);
 by (Blast_tac 2);
 (*Remaining case: YM3*)
@@ -198,7 +198,7 @@
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message and handle this case by contradiction*)
 by (blast_tac (!claset addSEs spies_partsEs
-                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
+                       delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
 val lemma = result();
 
 goal thy 
@@ -301,11 +301,11 @@
 \                          Crypt (shrK B) {|Agent A, Key K|}|}     \
 \                       : set evs)";
 by (parts_induct_tac 1);
+by (ALLGOALS Clarify_tac);
 (*YM3 & Fake*)
 by (Blast_tac 2);
 by (Fake_parts_insert_tac 1);
 (*YM4*)
-by (Step_tac 1);
 (*A is uncompromised because NB is secure*)
 by (not_bad_tac "A" 1);
 (*A's certificate guarantees the existence of the Server message*)
@@ -515,8 +515,8 @@
 (*Fake*)
 by (spy_analz_tac 1);
 (** LEVEL 7: YM4 and Oops remain **)
+by (ALLGOALS Clarify_tac);
 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
-by (REPEAT (Safe_step_tac 1));
 by (not_bad_tac "Aa" 1);
 by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
 by (forward_tac [Says_Server_message_form] 3);
@@ -529,7 +529,6 @@
 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   covered by the quantified Oops assumption.*)
 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
-by (step_tac (!claset delrules [disjE, conjI]) 1);
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
 by (expand_case_tac "NB = NBa" 1);
 (*If NB=NBa then all other components of the Oops message agree*)
diff -r 40856b593501 -r 56facaebf3e3 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Sep 25 12:10:07 1997 +0200
+++ b/src/HOL/Finite.ML	Thu Sep 25 12:13:18 1997 +0200
@@ -131,20 +131,17 @@
 goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
 by (etac finite_induct 1);
  by (ALLGOALS Asm_simp_tac);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
- by (Step_tac 1);
+ by (Clarify_tac 1);
  by (rewtac inj_onto_def);
  by (Blast_tac 1);
 by (thin_tac "ALL A. ?PP(A)" 1);
 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (res_inst_tac [("x","xa")] bexI 1);
 by (ALLGOALS Asm_simp_tac);
-by (etac equalityE 1);
-by (rtac equalityI 1);
-by (Blast_tac 2);
-by (Best_tac 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
 val lemma = result();
 
 goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
@@ -318,7 +315,7 @@
 goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
 by (etac finite_induct 1);
 by (Simp_tac 1);
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (case_tac "x:B" 1);
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
  by (SELECT_GOAL(safe_tac (!claset))1);
@@ -409,8 +406,7 @@
 by (etac finite_induct 1);
 by (Simp_tac 1);
 by (Blast_tac 1);
-by (strip_tac 1);
-by (etac conjE 1);
+by (Clarify_tac 1);
 by (case_tac "x:A" 1);
 (*1*)
 by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
@@ -419,14 +415,13 @@
 by (hyp_subst_tac 1);
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
-by (dtac insert_lim 1);
-by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
 (*2*)
 by (rotate_tac ~1 1);
+by (eres_inst_tac [("P","?a<?b")] notE 1);
 by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
 by (case_tac "A=F" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "psubset_card" ;
 
 
@@ -438,16 +433,14 @@
 \          --> k dvd card(Union C)";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (strip_tac 1);
-by (REPEAT (etac conjE 1));
+by (Clarify_tac 1);
 by (stac card_Un_disjoint 1);
 by (ALLGOALS
     (asm_full_simp_tac (!simpset
 			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
-by (thin_tac "?PP-->?QQ" 1);
 by (thin_tac "!c:F. ?PP(c)" 1);
 by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (ball_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "dvd_partition";
diff -r 40856b593501 -r 56facaebf3e3 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Sep 25 12:10:07 1997 +0200
+++ b/src/HOL/List.ML	Thu Sep 25 12:13:18 1997 +0200
@@ -6,6 +6,8 @@
 List lemmas
 *)
 
+open List;
+
 goal thy "!x. xs ~= x#xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -128,7 +130,7 @@
 goal thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)";
 by (induct_tac "xs" 1);
 by (Simp_tac 1);
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1);
 by (Asm_full_simp_tac 1);
 by (Blast_tac 1);
@@ -560,7 +562,7 @@
 goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
 by (induct_tac "xs" 1);
  by (ALLGOALS Asm_simp_tac);
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (exhaust_tac "n" 1);
  by (Blast_tac 1);
 by (exhaust_tac "i" 1);
diff -r 40856b593501 -r 56facaebf3e3 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Thu Sep 25 12:10:07 1997 +0200
+++ b/src/HOL/WF.ML	Thu Sep 25 12:13:18 1997 +0200
@@ -16,7 +16,7 @@
  "[| r <= A Times A;  \
 \    !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
 \ ==>  wf(r)";
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (rtac allE 1);
 by (assume_tac 1);
 by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
@@ -51,7 +51,7 @@
 (*transitive closure of a wf relation is wf! *)
 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
 by (rewtac wf_def);
-by (strip_tac 1);
+by (Clarify_tac 1);
 (*must retain the universal formula for later use!*)
 by (rtac allE 1 THEN assume_tac 1);
 by (etac mp 1);
@@ -75,7 +75,7 @@
 
 goalw WF.thy [wf_def]
     "!!r. (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
 by (Blast_tac 1);
 val lemma2 = result();
@@ -243,7 +243,7 @@
 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
 by (stac cuts_eq 1);
 (*Applying the substitution: must keep the quantified assumption!!*)
-by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
+by (EVERY1 [Clarify_tac, rtac H_cong1, rtac allE, atac,
             etac (mp RS ssubst), atac]); 
 by (fold_tac [is_recfun_def]);
 by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
@@ -270,7 +270,7 @@
 by (rtac H_cong 1);    (*expose the equality of cuts*)
 by (rtac refl 2);
 by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (res_inst_tac [("r","r^+")] is_recfun_equal 1);
 by (atac 1);
 by (rtac trans_trancl 1);
@@ -313,22 +313,19 @@
 
 goal WF.thy
     "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
 by (assume_tac 1);
 by (Blast_tac 1);
 qed"tfl_wf_induct";
 
 goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)";
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (rtac cut_apply 1);
 by (assume_tac 1);
 qed"tfl_cut_apply";
 
 goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
-by (strip_tac 1);
-by (res_inst_tac [("r","R"), ("H","M"),
-                  ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (Clarify_tac 1);
+be wfrec 1;
 qed "tfl_wfrec";