
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Wfrec.thy
--- a/src/HOL/Wfrec.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Wfrec.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -10,86 +10,88 @@
 imports Wellfounded
 begin
 
-inductive
-  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
-  for R :: "('a * 'a) set"
-  and F :: "('a => 'b) => 'a => 'b"
-where
-  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
-            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 => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
-  "cut f r x == (%y. if (y,x):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 * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
-  "adm_wf R F == ALL f g x.
-     (ALL z. (z, x) : R --> f z = g z) --> 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 * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
-  "wfrec R F == %x. THE y. wfrec_rel R (%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)
 
-lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: fun_eq_iff cut_def)
-
-lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
-by (simp add: cut_def)
+lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
+  by (simp add: cut_def)
 
 text{*Inductive characterization of wfrec combinator; for details see:
 John Harrison, "Inductive definitions: automation and application"*}
 
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
-apply (simp add: adm_wf_def)
-apply (erule_tac a=x in wf_induct)
-apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
-apply (fast dest!: theI')
-apply (erule wfrec_rel.cases, simp)
-apply (erule allE, erule allE, erule allE, erule mp)
-apply (blast intro: the_equality [symmetric])
-done
+lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
+  by (auto intro: the_equality[symmetric] theI)
 
-lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
-apply (simp add: adm_wf_def)
-apply (intro strip)
-apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
-apply (rule refl)
-done
+lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
+  using `wf R`
+proof induct
+  def f \<equiv> "\<lambda>y. THE z. wfrec_rel R F y z"
+  case (less x)
+  then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
+    unfolding f_def by (rule theI_unique)
+  with `adm_wf R F` show ?case
+    by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
+qed
 
-lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
+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])
+
+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 (intro strip)
 apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
 done
 
 
 text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
-lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
-apply auto
-apply (blast intro: wfrec)
-done
+lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
+ by (auto intro: wfrec)
+
+
+subsubsection {* Well-founded recursion via genuine fixpoints *}
 
+lemma wfrec_fixpoint:
+  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
+  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 }
+  finally show "wfrec R F x = F (wfrec R F) x" .
+qed
 
 subsection {* Wellfoundedness of @{text same_fst} *}
 
-definition
- same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
-where
-    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
-   --{*For @{text rec_def} 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}"
+   --{*For @{const wfrec} declarations where the first n parameters
        stay unchanged in the recursive call. *}
 
-lemma same_fstI [intro!]:
-     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
-by (simp add: same_fst_def)
+lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
+  by (simp add: same_fst_def)
 
 lemma wf_same_fst:
-  assumes prem: "(!!x. P x ==> wf(R x))"
-  shows "wf(same_fst P R)"
+  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)




