moved wfrec to Recdef.thy
authorkrauss
Mon Aug 31 20:34:44 2009 +0200 (2009-08-31)
changeset 32462c33faa289520
parent 32461 eee4fa79398f
child 32463 3a0a65ca2261
moved wfrec to Recdef.thy
src/HOL/Recdef.thy
src/HOL/Tools/TFL/rules.ML
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Recdef.thy	Mon Aug 31 20:32:00 2009 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Mon Aug 31 20:34:44 2009 +0200
     1.3 @@ -19,6 +19,65 @@
     1.4    ("Tools/recdef.ML")
     1.5  begin
     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 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    1.17 +  "cut f r x == (%y. if (y,x):r then f y else undefined)"
    1.18 +
    1.19 +  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
    1.20 +  "adm_wf R F == ALL f g x.
    1.21 +     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    1.22 +
    1.23 +  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    1.24 +  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    1.25 +
    1.26 +subsection{*Well-Founded Recursion*}
    1.27 +
    1.28 +text{*cut*}
    1.29 +
    1.30 +lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
    1.31 +by (simp add: expand_fun_eq cut_def)
    1.32 +
    1.33 +lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
    1.34 +by (simp add: cut_def)
    1.35 +
    1.36 +text{*Inductive characterization of wfrec combinator; for details see:
    1.37 +John Harrison, "Inductive definitions: automation and application"*}
    1.38 +
    1.39 +lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
    1.40 +apply (simp add: adm_wf_def)
    1.41 +apply (erule_tac a=x in wf_induct)
    1.42 +apply (rule ex1I)
    1.43 +apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
    1.44 +apply (fast dest!: theI')
    1.45 +apply (erule wfrec_rel.cases, simp)
    1.46 +apply (erule allE, erule allE, erule allE, erule mp)
    1.47 +apply (fast intro: the_equality [symmetric])
    1.48 +done
    1.49 +
    1.50 +lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
    1.51 +apply (simp add: adm_wf_def)
    1.52 +apply (intro strip)
    1.53 +apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
    1.54 +apply (rule refl)
    1.55 +done
    1.56 +
    1.57 +lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
    1.58 +apply (simp add: wfrec_def)
    1.59 +apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
    1.60 +apply (rule wfrec_rel.wfrecI)
    1.61 +apply (intro strip)
    1.62 +apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    1.63 +done
    1.64 +
    1.65 +
    1.66  text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
    1.67  lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
    1.68  apply auto
     2.1 --- a/src/HOL/Tools/TFL/rules.ML	Mon Aug 31 20:32:00 2009 +0200
     2.2 +++ b/src/HOL/Tools/TFL/rules.ML	Mon Aug 31 20:34:44 2009 +0200
     2.3 @@ -456,7 +456,7 @@
     2.4  fun is_cong thm =
     2.5    case (Thm.prop_of thm)
     2.6       of (Const("==>",_)$(Const("Trueprop",_)$ _) $
     2.7 -         (Const("==",_) $ (Const (@{const_name "Wellfounded.cut"},_) $ f $ R $ a $ x) $ _)) => false
     2.8 +         (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
     2.9        | _ => true;
    2.10  
    2.11  
    2.12 @@ -659,7 +659,7 @@
    2.13    end;
    2.14  
    2.15  fun restricted t = isSome (S.find_term
    2.16 -                            (fn (Const(@{const_name "Wellfounded.cut"},_)) =>true | _ => false)
    2.17 +                            (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
    2.18                              t)
    2.19  
    2.20  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
     3.1 --- a/src/HOL/Wellfounded.thy	Mon Aug 31 20:32:00 2009 +0200
     3.2 +++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:44 2009 +0200
     3.3 @@ -13,14 +13,6 @@
     3.4  
     3.5  subsection {* Basic Definitions *}
     3.6  
     3.7 -inductive
     3.8 -  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
     3.9 -  for R :: "('a * 'a) set"
    3.10 -  and F :: "('a => 'b) => 'a => 'b"
    3.11 -where
    3.12 -  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
    3.13 -            wfrec_rel R F x (F g x)"
    3.14 -
    3.15  constdefs
    3.16    wf         :: "('a * 'a)set => bool"
    3.17    "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
    3.18 @@ -31,16 +23,6 @@
    3.19    acyclic :: "('a*'a)set => bool"
    3.20    "acyclic r == !x. (x,x) ~: r^+"
    3.21  
    3.22 -  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    3.23 -  "cut f r x == (%y. if (y,x):r then f y else undefined)"
    3.24 -
    3.25 -  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
    3.26 -  "adm_wf R F == ALL f g x.
    3.27 -     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    3.28 -
    3.29 -  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    3.30 -  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    3.31 -
    3.32  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
    3.33    "acyclicP r == acyclic {(x, y). r x y}"
    3.34  
    3.35 @@ -425,46 +407,6 @@
    3.36  by (blast intro: finite_acyclic_wf wf_acyclic)
    3.37  
    3.38  
    3.39 -subsection{*Well-Founded Recursion*}
    3.40 -
    3.41 -text{*cut*}
    3.42 -
    3.43 -lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
    3.44 -by (simp add: expand_fun_eq cut_def)
    3.45 -
    3.46 -lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
    3.47 -by (simp add: cut_def)
    3.48 -
    3.49 -text{*Inductive characterization of wfrec combinator; for details see:  
    3.50 -John Harrison, "Inductive definitions: automation and application"*}
    3.51 -
    3.52 -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
    3.53 -apply (simp add: adm_wf_def)
    3.54 -apply (erule_tac a=x in wf_induct) 
    3.55 -apply (rule ex1I)
    3.56 -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
    3.57 -apply (fast dest!: theI')
    3.58 -apply (erule wfrec_rel.cases, simp)
    3.59 -apply (erule allE, erule allE, erule allE, erule mp)
    3.60 -apply (fast intro: the_equality [symmetric])
    3.61 -done
    3.62 -
    3.63 -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
    3.64 -apply (simp add: adm_wf_def)
    3.65 -apply (intro strip)
    3.66 -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
    3.67 -apply (rule refl)
    3.68 -done
    3.69 -
    3.70 -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
    3.71 -apply (simp add: wfrec_def)
    3.72 -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
    3.73 -apply (rule wfrec_rel.wfrecI)
    3.74 -apply (intro strip)
    3.75 -apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    3.76 -done
    3.77 -
    3.78 -
    3.79  subsection {* @{typ nat} is well-founded *}
    3.80  
    3.81  lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"