src/HOL/Wfrec.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63572 c0cbfd2b5a45
child 69593 3dda49e08b9d
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     1 (*  Title:      HOL/Wfrec.thy
     2     Author:     Tobias Nipkow
     3     Author:     Lawrence C Paulson
     4     Author:     Konrad Slind
     5 *)
     6 
     7 section \<open>Well-Founded Recursion Combinator\<close>
     8 
     9 theory Wfrec
    10   imports Wellfounded
    11 begin
    12 
    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
    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)"
    15 
    16 definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
    17   where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
    18 
    19 definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool"
    20   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)"
    21 
    22 definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)"
    23   where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
    24 
    25 lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
    26   by (simp add: fun_eq_iff cut_def)
    27 
    28 lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
    29   by (simp add: cut_def)
    30 
    31 text \<open>
    32   Inductive characterization of \<open>wfrec\<close> combinator; for details see:
    33   John Harrison, "Inductive definitions: automation and application".
    34 \<close>
    35 
    36 lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
    37   by (auto intro: the_equality[symmetric] theI)
    38 
    39 lemma wfrec_unique:
    40   assumes "adm_wf R F" "wf R"
    41   shows "\<exists>!y. wfrec_rel R F x y"
    42   using \<open>wf R\<close>
    43 proof induct
    44   define f where "f y = (THE z. wfrec_rel R F y z)" for y
    45   case (less x)
    46   then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
    47     unfolding f_def by (rule theI_unique)
    48   with \<open>adm_wf R F\<close> show ?case
    49     by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
    50 qed
    51 
    52 lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
    53   by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
    54 
    55 lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
    56   apply (simp add: wfrec_def)
    57   apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
    58    apply assumption
    59   apply (rule wfrec_rel.wfrecI)
    60   apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    61   done
    62 
    63 
    64 text \<open>This form avoids giant explosions in proofs.  NOTE USE OF \<open>\<equiv>\<close>.\<close>
    65 lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
    66   by (auto intro: wfrec)
    67 
    68 
    69 subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
    70 
    71 lemma wfrec_fixpoint:
    72   assumes wf: "wf R"
    73     and adm: "adm_wf R F"
    74   shows "wfrec R F = F (wfrec R F)"
    75 proof (rule ext)
    76   fix x
    77   have "wfrec R F x = F (cut (wfrec R F) R x) x"
    78     using wfrec[of R F] wf by simp
    79   also
    80   have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y"
    81     by (auto simp add: cut_apply)
    82   then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
    83     using adm adm_wf_def[of R F] by auto
    84   finally show "wfrec R F x = F (wfrec R F) x" .
    85 qed
    86 
    87 
    88 subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
    89 
    90 definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
    91   where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
    92    \<comment> \<open>For @{const wfrec} declarations where the first n parameters
    93        stay unchanged in the recursive call.\<close>
    94 
    95 lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
    96   by (simp add: same_fst_def)
    97 
    98 lemma wf_same_fst:
    99   assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
   100   shows "wf (same_fst P R)"
   101   apply (simp cong del: imp_cong add: wf_def same_fst_def)
   102   apply (intro strip)
   103   apply (rename_tac a b)
   104   apply (case_tac "wf (R a)")
   105    apply (erule_tac a = b in wf_induct)
   106    apply blast
   107   apply (blast intro: prem)
   108   done
   109 
   110 end