src/HOL/Cardinals/Wellfounded_More.thy
 author blanchet Mon Jan 20 18:24:56 2014 +0100 (2014-01-20) changeset 55066 4e5ddf3162ac parent 55027 a74ea6d75571 child 58889 5b7a9633cfa8 permissions -rw-r--r--
tuning
 blanchet@49310 ` 1` ```(* Title: HOL/Cardinals/Wellfounded_More.thy ``` blanchet@48975 ` 2` ``` Author: Andrei Popescu, TU Muenchen ``` blanchet@48975 ` 3` ``` Copyright 2012 ``` blanchet@48975 ` 4` blanchet@48975 ` 5` ```More on well-founded relations. ``` blanchet@48975 ` 6` ```*) ``` blanchet@48975 ` 7` blanchet@48975 ` 8` ```header {* More on Well-Founded Relations *} ``` blanchet@48975 ` 9` blanchet@48975 ` 10` ```theory Wellfounded_More ``` blanchet@55027 ` 11` ```imports Wellfounded Order_Relation_More ``` blanchet@48975 ` 12` ```begin ``` blanchet@48975 ` 13` blanchet@48975 ` 14` ```subsection {* Well-founded recursion via genuine fixpoints *} ``` blanchet@48975 ` 15` blanchet@48975 ` 16` ```(*2*)lemma adm_wf_unique_fixpoint: ``` blanchet@48975 ` 17` ```fixes r :: "('a * 'a) set" and ``` blanchet@48975 ` 18` ``` H :: "('a \ 'b) \ 'a \ 'b" and ``` blanchet@48975 ` 19` ``` f :: "'a \ 'b" and g :: "'a \ 'b" ``` blanchet@48975 ` 20` ```assumes WF: "wf r" and ADM: "adm_wf r H" and fFP: "f = H f" and gFP: "g = H g" ``` blanchet@48975 ` 21` ```shows "f = g" ``` blanchet@48975 ` 22` ```proof- ``` blanchet@48975 ` 23` ``` {fix x ``` blanchet@48975 ` 24` ``` have "f x = g x" ``` blanchet@48975 ` 25` ``` proof(rule wf_induct[of r "(\x. f x = g x)"], ``` blanchet@48975 ` 26` ``` auto simp add: WF) ``` blanchet@48975 ` 27` ``` fix x assume "\y. (y, x) \ r \ f y = g y" ``` blanchet@48975 ` 28` ``` hence "H f x = H g x" using ADM adm_wf_def[of r H] by auto ``` blanchet@48975 ` 29` ``` thus "f x = g x" using fFP and gFP by simp ``` blanchet@48975 ` 30` ``` qed ``` blanchet@48975 ` 31` ``` } ``` blanchet@48975 ` 32` ``` thus ?thesis by (simp add: ext) ``` blanchet@48975 ` 33` ```qed ``` blanchet@48975 ` 34` blanchet@48975 ` 35` ```(*2*)lemma wfrec_unique_fixpoint: ``` blanchet@48975 ` 36` ```fixes r :: "('a * 'a) set" and ``` blanchet@48975 ` 37` ``` H :: "('a \ 'b) \ 'a \ 'b" and ``` blanchet@48975 ` 38` ``` f :: "'a \ 'b" ``` blanchet@48975 ` 39` ```assumes WF: "wf r" and ADM: "adm_wf r H" and ``` blanchet@48975 ` 40` ``` fp: "f = H f" ``` blanchet@48975 ` 41` ```shows "f = wfrec r H" ``` blanchet@48975 ` 42` ```proof- ``` blanchet@48975 ` 43` ``` have "H (wfrec r H) = wfrec r H" ``` blanchet@48975 ` 44` ``` using assms wfrec_fixpoint[of r H] by simp ``` blanchet@48975 ` 45` ``` thus ?thesis ``` blanchet@48975 ` 46` ``` using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simp ``` blanchet@48975 ` 47` ```qed ``` blanchet@48975 ` 48` blanchet@48975 ` 49` ```end ```