src/HOL/Wfrec.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 61799 4cf66f21b764 child 63040 eb4ddd18d635 permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
```     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 where
```
```    14   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" where
```
```    17   "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" where
```
```    20   "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)" where
```
```    23   "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>Inductive characterization of wfrec combinator; for details see:
```
```    32 John Harrison, "Inductive definitions: automation and application"\<close>
```
```    33
```
```    34 lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
```
```    35   by (auto intro: the_equality[symmetric] theI)
```
```    36
```
```    37 lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
```
```    38   using \<open>wf R\<close>
```
```    39 proof induct
```
```    40   def f \<equiv> "\<lambda>y. THE z. wfrec_rel R F y z"
```
```    41   case (less x)
```
```    42   then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
```
```    43     unfolding f_def by (rule theI_unique)
```
```    44   with \<open>adm_wf R F\<close> show ?case
```
```    45     by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
```
```    46 qed
```
```    47
```
```    48 lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
```
```    49   by (auto simp add: adm_wf_def
```
```    50            intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
```
```    51
```
```    52 lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
```
```    53 apply (simp add: wfrec_def)
```
```    54 apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
```
```    55 apply (rule wfrec_rel.wfrecI)
```
```    56 apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
```
```    57 done
```
```    58
```
```    59
```
```    60 text\<open>* This form avoids giant explosions in proofs.  NOTE USE OF ==\<close>
```
```    61 lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
```
```    62  by (auto intro: wfrec)
```
```    63
```
```    64
```
```    65 subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
```
```    66
```
```    67 lemma wfrec_fixpoint:
```
```    68   assumes WF: "wf R" and ADM: "adm_wf R F"
```
```    69   shows "wfrec R F = F (wfrec R F)"
```
```    70 proof (rule ext)
```
```    71   fix x
```
```    72   have "wfrec R F x = F (cut (wfrec R F) R x) x"
```
```    73     using wfrec[of R F] WF by simp
```
```    74   also
```
```    75   { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
```
```    76       by (auto simp add: cut_apply)
```
```    77     hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
```
```    78       using ADM adm_wf_def[of R F] by auto }
```
```    79   finally show "wfrec R F x = F (wfrec R F) x" .
```
```    80 qed
```
```    81
```
```    82 subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
```
```    83
```
```    84 definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
```
```    85   "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
```
```    86    \<comment>\<open>For @{const wfrec} declarations where the first n parameters
```
```    87        stay unchanged in the recursive call.\<close>
```
```    88
```
```    89 lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
```
```    90   by (simp add: same_fst_def)
```
```    91
```
```    92 lemma wf_same_fst:
```
```    93   assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
```
```    94   shows "wf (same_fst P R)"
```
```    95 apply (simp cong del: imp_cong add: wf_def same_fst_def)
```
```    96 apply (intro strip)
```
```    97 apply (rename_tac a b)
```
```    98 apply (case_tac "wf (R a)")
```
```    99  apply (erule_tac a = b in wf_induct, blast)
```
```   100 apply (blast intro: prem)
```
```   101 done
```
```   102
```
```   103 end
```