# HG changeset patch
# User nipkow
# Date 893246765 -7200
# Node ID bfbaea156f43cf1157ddd567adf76e502dd449b2
# Parent  8f6dbbd8d497e0c165f227c7dd670dcaba136472
Modifications due to improved simplifier.

diff -r 8f6dbbd8d497 -r bfbaea156f43 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Apr 22 14:04:35 1998 +0200
+++ b/src/HOL/NatDef.ML	Wed Apr 22 14:06:05 1998 +0200
@@ -157,7 +157,7 @@
 
 (* The unrolling rule for nat_rec *)
 goal thy
-   "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
+   "nat_rec c d = wfrec pred_nat (%f. nat_case c (%m. d m (f m)))";
   by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
 bind_thm("nat_rec_unfold", wf_pred_nat RS 
                             ((result() RS eq_reflection) RS def_wfrec));
diff -r 8f6dbbd8d497 -r bfbaea156f43 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed Apr 22 14:04:35 1998 +0200
+++ b/src/HOL/WF.ML	Wed Apr 22 14:06:05 1998 +0200
@@ -213,31 +213,29 @@
 qed "is_the_recfun";
 
 val prems = goal WF.thy
- "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
-  by (cut_facts_tac prems 1);
-  by (wf_ind_tac "a" prems 1);
-  by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
-                   is_the_recfun 1);
-  by (rewtac is_recfun_def);
-  by (stac cuts_eq 1);
-  by (rtac allI 1);
-  by (rtac impI 1);
-  by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
-  by (subgoal_tac
+ "!!r. [| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
+by (wf_ind_tac "a" prems 1);
+by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
+                 is_the_recfun 1);
+by (rewtac is_recfun_def);
+by (stac cuts_eq 1);
+by (Clarify_tac 1);
+by (rtac (refl RSN (2,H_cong)) 1);
+by (subgoal_tac
          "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1);
-  by (etac allE 2);
-  by (dtac impE 2);
-  by (atac 2);
+ by (etac allE 2);
+ by (dtac impE 2);
+   by (atac 2);
   by (atac 3);
-  by (atac 2);
-  by (etac ssubst 1);
-  by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
-  by (rtac allI 1);
-  by (rtac impI 1);
-  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
-  by (res_inst_tac [("f1","H"),("x","ya")](arg_cong RS fun_cong) 1);
-  by (fold_tac [is_recfun_def]);
-  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
+ by (atac 2);
+by (etac ssubst 1);
+by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
+by (Clarify_tac 1);
+by (stac cut_apply 1);
+ by(fast_tac (claset() addDs [transD]) 1);
+by (rtac (refl RSN (2,H_cong)) 1);
+by (fold_tac [is_recfun_def]);
+by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
 qed "unfold_the_recfun";
 
 val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;