Modifications due to improved simplifier.
authornipkow
Wed Apr 22 14:06:05 1998 +0200 (1998-04-22)
changeset 4821bfbaea156f43
parent 4820 8f6dbbd8d497
child 4822 2733e21814fe
Modifications due to improved simplifier.
src/HOL/NatDef.ML
src/HOL/WF.ML
     1.1 --- a/src/HOL/NatDef.ML	Wed Apr 22 14:04:35 1998 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Wed Apr 22 14:06:05 1998 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4  
     1.5  (* The unrolling rule for nat_rec *)
     1.6  goal thy
     1.7 -   "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
     1.8 +   "nat_rec c d = wfrec pred_nat (%f. nat_case c (%m. d m (f m)))";
     1.9    by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
    1.10  bind_thm("nat_rec_unfold", wf_pred_nat RS 
    1.11                              ((result() RS eq_reflection) RS def_wfrec));
     2.1 --- a/src/HOL/WF.ML	Wed Apr 22 14:04:35 1998 +0200
     2.2 +++ b/src/HOL/WF.ML	Wed Apr 22 14:06:05 1998 +0200
     2.3 @@ -213,31 +213,29 @@
     2.4  qed "is_the_recfun";
     2.5  
     2.6  val prems = goal WF.thy
     2.7 - "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
     2.8 -  by (cut_facts_tac prems 1);
     2.9 -  by (wf_ind_tac "a" prems 1);
    2.10 -  by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
    2.11 -                   is_the_recfun 1);
    2.12 -  by (rewtac is_recfun_def);
    2.13 -  by (stac cuts_eq 1);
    2.14 -  by (rtac allI 1);
    2.15 -  by (rtac impI 1);
    2.16 -  by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
    2.17 -  by (subgoal_tac
    2.18 + "!!r. [| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
    2.19 +by (wf_ind_tac "a" prems 1);
    2.20 +by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
    2.21 +                 is_the_recfun 1);
    2.22 +by (rewtac is_recfun_def);
    2.23 +by (stac cuts_eq 1);
    2.24 +by (Clarify_tac 1);
    2.25 +by (rtac (refl RSN (2,H_cong)) 1);
    2.26 +by (subgoal_tac
    2.27           "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1);
    2.28 -  by (etac allE 2);
    2.29 -  by (dtac impE 2);
    2.30 -  by (atac 2);
    2.31 + by (etac allE 2);
    2.32 + by (dtac impE 2);
    2.33 +   by (atac 2);
    2.34    by (atac 3);
    2.35 -  by (atac 2);
    2.36 -  by (etac ssubst 1);
    2.37 -  by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
    2.38 -  by (rtac allI 1);
    2.39 -  by (rtac impI 1);
    2.40 -  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
    2.41 -  by (res_inst_tac [("f1","H"),("x","ya")](arg_cong RS fun_cong) 1);
    2.42 -  by (fold_tac [is_recfun_def]);
    2.43 -  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
    2.44 + by (atac 2);
    2.45 +by (etac ssubst 1);
    2.46 +by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
    2.47 +by (Clarify_tac 1);
    2.48 +by (stac cut_apply 1);
    2.49 + by(fast_tac (claset() addDs [transD]) 1);
    2.50 +by (rtac (refl RSN (2,H_cong)) 1);
    2.51 +by (fold_tac [is_recfun_def]);
    2.52 +by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
    2.53  qed "unfold_the_recfun";
    2.54  
    2.55  val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;