--- a/src/HOL/Wfrec.thy Sun Jul 31 19:09:21 2016 +0200
+++ b/src/HOL/Wfrec.thy Sun Jul 31 22:56:18 2016 +0200
@@ -7,20 +7,20 @@
section \<open>Well-Founded Recursion Combinator\<close>
theory Wfrec
-imports Wellfounded
+ imports Wellfounded
begin
-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
- wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
+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 wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
-definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" where
- "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
+definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
+ where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
-definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" 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)"
+definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool"
+ 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)"
-definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" where
- "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
+definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)"
+ where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
by (simp add: fun_eq_iff cut_def)
@@ -28,13 +28,17 @@
lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
by (simp add: cut_def)
-text\<open>Inductive characterization of wfrec combinator; for details see:
-John Harrison, "Inductive definitions: automation and application"\<close>
+text \<open>
+ Inductive characterization of \<open>wfrec\<close> combinator; for details see:
+ John Harrison, "Inductive definitions: automation and application".
+\<close>
lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
by (auto intro: the_equality[symmetric] theI)
-lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
+lemma wfrec_unique:
+ assumes "adm_wf R F" "wf R"
+ shows "\<exists>!y. wfrec_rel R F x y"
using \<open>wf R\<close>
proof induct
define f where "f y = (THE z. wfrec_rel R F y z)" for y
@@ -46,44 +50,46 @@
qed
lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
- by (auto simp add: adm_wf_def
- intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
+ by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
-apply (simp add: wfrec_def)
-apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
-apply (rule wfrec_rel.wfrecI)
-apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
-done
+ apply (simp add: wfrec_def)
+ apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
+ apply assumption
+ apply (rule wfrec_rel.wfrecI)
+ apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
+ done
-text\<open>* This form avoids giant explosions in proofs. NOTE USE OF ==\<close>
+text \<open>This form avoids giant explosions in proofs. NOTE USE OF \<open>\<equiv>\<close>.\<close>
lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
- by (auto intro: wfrec)
+ by (auto intro: wfrec)
subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
lemma wfrec_fixpoint:
- assumes WF: "wf R" and ADM: "adm_wf R F"
+ assumes wf: "wf R"
+ and adm: "adm_wf R F"
shows "wfrec R F = F (wfrec R F)"
proof (rule ext)
fix x
have "wfrec R F x = F (cut (wfrec R F) R x) x"
- using wfrec[of R F] WF by simp
+ using wfrec[of R F] wf by simp
also
- { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
- by (auto simp add: cut_apply)
- hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
- using ADM adm_wf_def[of R F] by auto }
+ have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y"
+ by (auto simp add: cut_apply)
+ then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
+ using adm adm_wf_def[of R F] by auto
finally show "wfrec R F x = F (wfrec R F) x" .
qed
+
subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
-definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
- "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
- \<comment>\<open>For @{const wfrec} declarations where the first n parameters
+definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
+ where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
+ \<comment> \<open>For @{const wfrec} declarations where the first n parameters
stay unchanged in the recursive call.\<close>
lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
@@ -92,12 +98,13 @@
lemma wf_same_fst:
assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
shows "wf (same_fst P R)"
-apply (simp cong del: imp_cong add: wf_def same_fst_def)
-apply (intro strip)
-apply (rename_tac a b)
-apply (case_tac "wf (R a)")
- apply (erule_tac a = b in wf_induct, blast)
-apply (blast intro: prem)
-done
+ apply (simp cong del: imp_cong add: wf_def same_fst_def)
+ apply (intro strip)
+ apply (rename_tac a b)
+ apply (case_tac "wf (R a)")
+ apply (erule_tac a = b in wf_induct)
+ apply blast
+ apply (blast intro: prem)
+ done
end