src/HOL/Wellfounded.thy
 changeset 32462 c33faa289520 parent 32461 eee4fa79398f child 32463 3a0a65ca2261
```     1.1 --- a/src/HOL/Wellfounded.thy	Mon Aug 31 20:32:00 2009 +0200
1.2 +++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:44 2009 +0200
1.3 @@ -13,14 +13,6 @@
1.4
1.5  subsection {* Basic Definitions *}
1.6
1.7 -inductive
1.8 -  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
1.9 -  for R :: "('a * 'a) set"
1.10 -  and F :: "('a => 'b) => 'a => 'b"
1.11 -where
1.12 -  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
1.13 -            wfrec_rel R F x (F g x)"
1.14 -
1.15  constdefs
1.16    wf         :: "('a * 'a)set => bool"
1.17    "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
1.18 @@ -31,16 +23,6 @@
1.19    acyclic :: "('a*'a)set => bool"
1.20    "acyclic r == !x. (x,x) ~: r^+"
1.21
1.22 -  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
1.23 -  "cut f r x == (%y. if (y,x):r then f y else undefined)"
1.24 -
1.25 -  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
1.26 -  "adm_wf R F == ALL f g x.
1.27 -     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
1.28 -
1.29 -  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
1.30 -  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
1.31 -
1.32  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
1.33    "acyclicP r == acyclic {(x, y). r x y}"
1.34
1.35 @@ -425,46 +407,6 @@
1.36  by (blast intro: finite_acyclic_wf wf_acyclic)
1.37
1.38
1.39 -subsection{*Well-Founded Recursion*}
1.40 -
1.41 -text{*cut*}
1.42 -
1.43 -lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
1.44 -by (simp add: expand_fun_eq cut_def)
1.45 -
1.46 -lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
1.48 -
1.49 -text{*Inductive characterization of wfrec combinator; for details see:
1.50 -John Harrison, "Inductive definitions: automation and application"*}
1.51 -
1.52 -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
1.54 -apply (erule_tac a=x in wf_induct)
1.55 -apply (rule ex1I)
1.56 -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
1.57 -apply (fast dest!: theI')
1.58 -apply (erule wfrec_rel.cases, simp)
1.59 -apply (erule allE, erule allE, erule allE, erule mp)
1.60 -apply (fast intro: the_equality [symmetric])
1.61 -done
1.62 -
1.63 -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
1.65 -apply (intro strip)
1.66 -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
1.67 -apply (rule refl)
1.68 -done
1.69 -
1.70 -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"