--- a/src/HOL/Ordinals_and_Cardinals/Wellfounded_More.thy Wed Sep 12 05:21:47 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Title: HOL/Ordinals_and_Cardinals/Wellfounded_More.thy
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-More on well-founded relations.
-*)
-
-header {* More on Well-Founded Relations *}
-
-theory Wellfounded_More
-imports Wellfounded_More_Base Order_Relation_More
-begin
-
-
-subsection {* Well-founded recursion via genuine fixpoints *}
-
-(*2*)lemma adm_wf_unique_fixpoint:
-fixes r :: "('a * 'a) set" and
- H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" and
- f :: "'a \<Rightarrow> 'b" and g :: "'a \<Rightarrow> 'b"
-assumes WF: "wf r" and ADM: "adm_wf r H" and fFP: "f = H f" and gFP: "g = H g"
-shows "f = g"
-proof-
- {fix x
- have "f x = g x"
- proof(rule wf_induct[of r "(\<lambda>x. f x = g x)"],
- auto simp add: WF)
- fix x assume "\<forall>y. (y, x) \<in> r \<longrightarrow> f y = g y"
- hence "H f x = H g x" using ADM adm_wf_def[of r H] by auto
- thus "f x = g x" using fFP and gFP by simp
- qed
- }
- thus ?thesis by (simp add: ext)
-qed
-
-(*2*)lemma wfrec_unique_fixpoint:
-fixes r :: "('a * 'a) set" and
- H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" and
- f :: "'a \<Rightarrow> 'b"
-assumes WF: "wf r" and ADM: "adm_wf r H" and
- fp: "f = H f"
-shows "f = wfrec r H"
-proof-
- have "H (wfrec r H) = wfrec r H"
- using assms wfrec_fixpoint[of r H] by simp
- thus ?thesis
- using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simp
-qed
-
-end