src/HOL/Wfrec.thy
changeset 63572 c0cbfd2b5a45
parent 63040 eb4ddd18d635
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Wfrec.thy	Sun Jul 31 19:09:21 2016 +0200
     1.2 +++ b/src/HOL/Wfrec.thy	Sun Jul 31 22:56:18 2016 +0200
     1.3 @@ -7,20 +7,20 @@
     1.4  section \<open>Well-Founded Recursion Combinator\<close>
     1.5  
     1.6  theory Wfrec
     1.7 -imports Wellfounded
     1.8 +  imports Wellfounded
     1.9  begin
    1.10  
    1.11 -inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F where
    1.12 -  wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
    1.13 +inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F
    1.14 +  where wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
    1.15  
    1.16 -definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.17 -  "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
    1.18 +definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
    1.19 +  where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
    1.20  
    1.21 -definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" where
    1.22 -  "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)"
    1.23 +definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool"
    1.24 +  where "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)"
    1.25  
    1.26 -definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" where
    1.27 -  "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
    1.28 +definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)"
    1.29 +  where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
    1.30  
    1.31  lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
    1.32    by (simp add: fun_eq_iff cut_def)
    1.33 @@ -28,13 +28,17 @@
    1.34  lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
    1.35    by (simp add: cut_def)
    1.36  
    1.37 -text\<open>Inductive characterization of wfrec combinator; for details see:
    1.38 -John Harrison, "Inductive definitions: automation and application"\<close>
    1.39 +text \<open>
    1.40 +  Inductive characterization of \<open>wfrec\<close> combinator; for details see:
    1.41 +  John Harrison, "Inductive definitions: automation and application".
    1.42 +\<close>
    1.43  
    1.44  lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
    1.45    by (auto intro: the_equality[symmetric] theI)
    1.46  
    1.47 -lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
    1.48 +lemma wfrec_unique:
    1.49 +  assumes "adm_wf R F" "wf R"
    1.50 +  shows "\<exists>!y. wfrec_rel R F x y"
    1.51    using \<open>wf R\<close>
    1.52  proof induct
    1.53    define f where "f y = (THE z. wfrec_rel R F y z)" for y
    1.54 @@ -46,44 +50,46 @@
    1.55  qed
    1.56  
    1.57  lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
    1.58 -  by (auto simp add: adm_wf_def
    1.59 -           intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
    1.60 +  by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
    1.61  
    1.62  lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
    1.63 -apply (simp add: wfrec_def)
    1.64 -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
    1.65 -apply (rule wfrec_rel.wfrecI)
    1.66 -apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    1.67 -done
    1.68 +  apply (simp add: wfrec_def)
    1.69 +  apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
    1.70 +   apply assumption
    1.71 +  apply (rule wfrec_rel.wfrecI)
    1.72 +  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    1.73 +  done
    1.74  
    1.75  
    1.76 -text\<open>* This form avoids giant explosions in proofs.  NOTE USE OF ==\<close>
    1.77 +text \<open>This form avoids giant explosions in proofs.  NOTE USE OF \<open>\<equiv>\<close>.\<close>
    1.78  lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
    1.79 - by (auto intro: wfrec)
    1.80 +  by (auto intro: wfrec)
    1.81  
    1.82  
    1.83  subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
    1.84  
    1.85  lemma wfrec_fixpoint:
    1.86 -  assumes WF: "wf R" and ADM: "adm_wf R F"
    1.87 +  assumes wf: "wf R"
    1.88 +    and adm: "adm_wf R F"
    1.89    shows "wfrec R F = F (wfrec R F)"
    1.90  proof (rule ext)
    1.91    fix x
    1.92    have "wfrec R F x = F (cut (wfrec R F) R x) x"
    1.93 -    using wfrec[of R F] WF by simp
    1.94 +    using wfrec[of R F] wf by simp
    1.95    also
    1.96 -  { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
    1.97 -      by (auto simp add: cut_apply)
    1.98 -    hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
    1.99 -      using ADM adm_wf_def[of R F] by auto }
   1.100 +  have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y"
   1.101 +    by (auto simp add: cut_apply)
   1.102 +  then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
   1.103 +    using adm adm_wf_def[of R F] by auto
   1.104    finally show "wfrec R F x = F (wfrec R F) x" .
   1.105  qed
   1.106  
   1.107 +
   1.108  subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
   1.109  
   1.110 -definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
   1.111 -  "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
   1.112 -   \<comment>\<open>For @{const wfrec} declarations where the first n parameters
   1.113 +definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
   1.114 +  where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
   1.115 +   \<comment> \<open>For @{const wfrec} declarations where the first n parameters
   1.116         stay unchanged in the recursive call.\<close>
   1.117  
   1.118  lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
   1.119 @@ -92,12 +98,13 @@
   1.120  lemma wf_same_fst:
   1.121    assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
   1.122    shows "wf (same_fst P R)"
   1.123 -apply (simp cong del: imp_cong add: wf_def same_fst_def)
   1.124 -apply (intro strip)
   1.125 -apply (rename_tac a b)
   1.126 -apply (case_tac "wf (R a)")
   1.127 - apply (erule_tac a = b in wf_induct, blast)
   1.128 -apply (blast intro: prem)
   1.129 -done
   1.130 +  apply (simp cong del: imp_cong add: wf_def same_fst_def)
   1.131 +  apply (intro strip)
   1.132 +  apply (rename_tac a b)
   1.133 +  apply (case_tac "wf (R a)")
   1.134 +   apply (erule_tac a = b in wf_induct)
   1.135 +   apply blast
   1.136 +  apply (blast intro: prem)
   1.137 +  done
   1.138  
   1.139  end