src/HOL/WF.ML
changeset 4821 bfbaea156f43
parent 4762 afebaa81f148
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/WF.ML	Wed Apr 22 14:04:35 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Wed Apr 22 14:06:05 1998 +0200
     1.3 @@ -213,31 +213,29 @@
     1.4  qed "is_the_recfun";
     1.5  
     1.6  val prems = goal WF.thy
     1.7 - "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
     1.8 -  by (cut_facts_tac prems 1);
     1.9 -  by (wf_ind_tac "a" prems 1);
    1.10 -  by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
    1.11 -                   is_the_recfun 1);
    1.12 -  by (rewtac is_recfun_def);
    1.13 -  by (stac cuts_eq 1);
    1.14 -  by (rtac allI 1);
    1.15 -  by (rtac impI 1);
    1.16 -  by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
    1.17 -  by (subgoal_tac
    1.18 + "!!r. [| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
    1.19 +by (wf_ind_tac "a" prems 1);
    1.20 +by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
    1.21 +                 is_the_recfun 1);
    1.22 +by (rewtac is_recfun_def);
    1.23 +by (stac cuts_eq 1);
    1.24 +by (Clarify_tac 1);
    1.25 +by (rtac (refl RSN (2,H_cong)) 1);
    1.26 +by (subgoal_tac
    1.27           "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1);
    1.28 -  by (etac allE 2);
    1.29 -  by (dtac impE 2);
    1.30 -  by (atac 2);
    1.31 + by (etac allE 2);
    1.32 + by (dtac impE 2);
    1.33 +   by (atac 2);
    1.34    by (atac 3);
    1.35 -  by (atac 2);
    1.36 -  by (etac ssubst 1);
    1.37 -  by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
    1.38 -  by (rtac allI 1);
    1.39 -  by (rtac impI 1);
    1.40 -  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
    1.41 -  by (res_inst_tac [("f1","H"),("x","ya")](arg_cong RS fun_cong) 1);
    1.42 -  by (fold_tac [is_recfun_def]);
    1.43 -  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
    1.44 + by (atac 2);
    1.45 +by (etac ssubst 1);
    1.46 +by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
    1.47 +by (Clarify_tac 1);
    1.48 +by (stac cut_apply 1);
    1.49 + by(fast_tac (claset() addDs [transD]) 1);
    1.50 +by (rtac (refl RSN (2,H_cong)) 1);
    1.51 +by (fold_tac [is_recfun_def]);
    1.52 +by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
    1.53  qed "unfold_the_recfun";
    1.54  
    1.55  val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;