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
```