|
1 (* Title: HOL/Cardinals/Wellfounded_More.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 More on well-founded relations. |
|
6 *) |
|
7 |
|
8 header {* More on Well-Founded Relations *} |
|
9 |
|
10 theory Wellfounded_More |
|
11 imports Wellfounded_More_Base Order_Relation_More |
|
12 begin |
|
13 |
|
14 |
|
15 subsection {* Well-founded recursion via genuine fixpoints *} |
|
16 |
|
17 (*2*)lemma adm_wf_unique_fixpoint: |
|
18 fixes r :: "('a * 'a) set" and |
|
19 H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" and |
|
20 f :: "'a \<Rightarrow> 'b" and g :: "'a \<Rightarrow> 'b" |
|
21 assumes WF: "wf r" and ADM: "adm_wf r H" and fFP: "f = H f" and gFP: "g = H g" |
|
22 shows "f = g" |
|
23 proof- |
|
24 {fix x |
|
25 have "f x = g x" |
|
26 proof(rule wf_induct[of r "(\<lambda>x. f x = g x)"], |
|
27 auto simp add: WF) |
|
28 fix x assume "\<forall>y. (y, x) \<in> r \<longrightarrow> f y = g y" |
|
29 hence "H f x = H g x" using ADM adm_wf_def[of r H] by auto |
|
30 thus "f x = g x" using fFP and gFP by simp |
|
31 qed |
|
32 } |
|
33 thus ?thesis by (simp add: ext) |
|
34 qed |
|
35 |
|
36 (*2*)lemma wfrec_unique_fixpoint: |
|
37 fixes r :: "('a * 'a) set" and |
|
38 H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" and |
|
39 f :: "'a \<Rightarrow> 'b" |
|
40 assumes WF: "wf r" and ADM: "adm_wf r H" and |
|
41 fp: "f = H f" |
|
42 shows "f = wfrec r H" |
|
43 proof- |
|
44 have "H (wfrec r H) = wfrec r H" |
|
45 using assms wfrec_fixpoint[of r H] by simp |
|
46 thus ?thesis |
|
47 using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simp |
|
48 qed |
|
49 |
|
50 end |