src/HOL/Recdef.thy
changeset 26748 4d51ddd6aa5c
parent 23742 d6349ac8b153
child 29654 24e73987bfe2
     1.1 --- a/src/HOL/Recdef.thy	Thu Apr 24 16:53:04 2008 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Fri Apr 25 15:30:33 2008 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* TFL: recursive function definitions *}
     1.5  
     1.6  theory Recdef
     1.7 -imports Wellfounded_Relations FunDef
     1.8 +imports FunDef
     1.9  uses
    1.10    ("Tools/TFL/casesplit.ML")
    1.11    ("Tools/TFL/utils.ML")
    1.12 @@ -20,6 +20,30 @@
    1.13    ("Tools/recdef_package.ML")
    1.14  begin
    1.15  
    1.16 +text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
    1.17 +lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
    1.18 +apply auto
    1.19 +apply (blast intro: wfrec)
    1.20 +done
    1.21 +
    1.22 +
    1.23 +lemma tfl_wf_induct: "ALL R. wf R -->  
    1.24 +       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
    1.25 +apply clarify
    1.26 +apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
    1.27 +done
    1.28 +
    1.29 +lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
    1.30 +apply clarify
    1.31 +apply (rule cut_apply, assumption)
    1.32 +done
    1.33 +
    1.34 +lemma tfl_wfrec:
    1.35 +     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
    1.36 +apply clarify
    1.37 +apply (erule wfrec)
    1.38 +done
    1.39 +
    1.40  lemma tfl_eq_True: "(x = True) --> x"
    1.41    by blast
    1.42