src/HOLCF/Bifinite.thy
 author huffman Mon May 11 08:28:09 2009 -0700 (2009-05-11) changeset 31095 b79d140f6d0b parent 31076 99fe356cbbc2 child 31113 15cf300a742f permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
 huffman@25903 ` 1` ```(* Title: HOLCF/Bifinite.thy ``` huffman@25903 ` 2` ``` Author: Brian Huffman ``` huffman@25903 ` 3` ```*) ``` huffman@25903 ` 4` huffman@25903 ` 5` ```header {* Bifinite domains and approximation *} ``` huffman@25903 ` 6` huffman@25903 ` 7` ```theory Bifinite ``` huffman@27402 ` 8` ```imports Deflation ``` huffman@25903 ` 9` ```begin ``` huffman@25903 ` 10` huffman@26407 ` 11` ```subsection {* Omega-profinite and bifinite domains *} ``` huffman@25903 ` 12` haftmann@29614 ` 13` ```class profinite = ``` huffman@26962 ` 14` ``` fixes approx :: "nat \ 'a \ 'a" ``` huffman@27310 ` 15` ``` assumes chain_approx [simp]: "chain approx" ``` huffman@26962 ` 16` ``` assumes lub_approx_app [simp]: "(\i. approx i\x) = x" ``` huffman@26962 ` 17` ``` assumes approx_idem: "approx i\(approx i\x) = approx i\x" ``` huffman@26962 ` 18` ``` assumes finite_fixes_approx: "finite {x. approx i\x = x}" ``` huffman@25903 ` 19` huffman@26962 ` 20` ```class bifinite = profinite + pcpo ``` huffman@25909 ` 21` huffman@31076 ` 22` ```lemma approx_below: "approx i\x \ x" ``` huffman@27402 ` 23` ```proof - ``` huffman@27402 ` 24` ``` have "chain (\i. approx i\x)" by simp ``` huffman@27402 ` 25` ``` hence "approx i\x \ (\i. approx i\x)" by (rule is_ub_thelub) ``` huffman@27402 ` 26` ``` thus "approx i\x \ x" by simp ``` huffman@27402 ` 27` ```qed ``` huffman@27402 ` 28` huffman@27402 ` 29` ```lemma finite_deflation_approx: "finite_deflation (approx i)" ``` huffman@27402 ` 30` ```proof ``` huffman@27402 ` 31` ``` fix x :: 'a ``` huffman@27402 ` 32` ``` show "approx i\(approx i\x) = approx i\x" ``` huffman@27402 ` 33` ``` by (rule approx_idem) ``` huffman@27402 ` 34` ``` show "approx i\x \ x" ``` huffman@31076 ` 35` ``` by (rule approx_below) ``` huffman@27402 ` 36` ``` show "finite {x. approx i\x = x}" ``` huffman@27402 ` 37` ``` by (rule finite_fixes_approx) ``` huffman@27402 ` 38` ```qed ``` huffman@27402 ` 39` wenzelm@30729 ` 40` ```interpretation approx: finite_deflation "approx i" ``` huffman@27402 ` 41` ```by (rule finite_deflation_approx) ``` huffman@27402 ` 42` ballarin@28234 ` 43` ```lemma (in deflation) deflation: "deflation d" .. ``` ballarin@28234 ` 44` huffman@27402 ` 45` ```lemma deflation_approx: "deflation (approx i)" ``` ballarin@28234 ` 46` ```by (rule approx.deflation) ``` huffman@25903 ` 47` huffman@27186 ` 48` ```lemma lub_approx [simp]: "(\i. approx i) = (\ x. x)" ``` huffman@25903 ` 49` ```by (rule ext_cfun, simp add: contlub_cfun_fun) ``` huffman@25903 ` 50` huffman@27309 ` 51` ```lemma approx_strict [simp]: "approx i\\ = \" ``` huffman@31076 ` 52` ```by (rule UU_I, rule approx_below) ``` huffman@25903 ` 53` huffman@25903 ` 54` ```lemma approx_approx1: ``` huffman@27186 ` 55` ``` "i \ j \ approx i\(approx j\x) = approx i\x" ``` huffman@31076 ` 56` ```apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx]) ``` huffman@25922 ` 57` ```apply (erule chain_mono [OF chain_approx]) ``` huffman@25903 ` 58` ```done ``` huffman@25903 ` 59` huffman@25903 ` 60` ```lemma approx_approx2: ``` huffman@27186 ` 61` ``` "j \ i \ approx i\(approx j\x) = approx j\x" ``` huffman@31076 ` 62` ```apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx]) ``` huffman@25922 ` 63` ```apply (erule chain_mono [OF chain_approx]) ``` huffman@25903 ` 64` ```done ``` huffman@25903 ` 65` huffman@25903 ` 66` ```lemma approx_approx [simp]: ``` huffman@27186 ` 67` ``` "approx i\(approx j\x) = approx (min i j)\x" ``` huffman@25903 ` 68` ```apply (rule_tac x=i and y=j in linorder_le_cases) ``` huffman@25903 ` 69` ```apply (simp add: approx_approx1 min_def) ``` huffman@25903 ` 70` ```apply (simp add: approx_approx2 min_def) ``` huffman@25903 ` 71` ```done ``` huffman@25903 ` 72` huffman@27402 ` 73` ```lemma finite_image_approx: "finite ((\x. approx n\x) ` A)" ``` huffman@27402 ` 74` ```by (rule approx.finite_image) ``` huffman@25903 ` 75` huffman@27402 ` 76` ```lemma finite_range_approx: "finite (range (\x. approx i\x))" ``` huffman@27402 ` 77` ```by (rule approx.finite_range) ``` huffman@27186 ` 78` huffman@27186 ` 79` ```lemma compact_approx [simp]: "compact (approx n\x)" ``` huffman@27402 ` 80` ```by (rule approx.compact) ``` huffman@25903 ` 81` huffman@27309 ` 82` ```lemma profinite_compact_eq_approx: "compact x \ \i. approx i\x = x" ``` huffman@27402 ` 83` ```by (rule admD2, simp_all) ``` huffman@25903 ` 84` huffman@27309 ` 85` ```lemma profinite_compact_iff: "compact x \ (\n. approx n\x = x)" ``` huffman@25903 ` 86` ``` apply (rule iffI) ``` huffman@27309 ` 87` ``` apply (erule profinite_compact_eq_approx) ``` huffman@25903 ` 88` ``` apply (erule exE) ``` huffman@25903 ` 89` ``` apply (erule subst) ``` huffman@25903 ` 90` ``` apply (rule compact_approx) ``` huffman@25903 ` 91` ```done ``` huffman@25903 ` 92` huffman@25903 ` 93` ```lemma approx_induct: ``` huffman@25903 ` 94` ``` assumes adm: "adm P" and P: "\n x. P (approx n\x)" ``` huffman@27186 ` 95` ``` shows "P x" ``` huffman@25903 ` 96` ```proof - ``` huffman@25903 ` 97` ``` have "P (\n. approx n\x)" ``` huffman@25903 ` 98` ``` by (rule admD [OF adm], simp, simp add: P) ``` huffman@25903 ` 99` ``` thus "P x" by simp ``` huffman@25903 ` 100` ```qed ``` huffman@25903 ` 101` huffman@31076 ` 102` ```lemma profinite_below_ext: "(\i. approx i\x \ approx i\y) \ x \ y" ``` huffman@25903 ` 103` ```apply (subgoal_tac "(\i. approx i\x) \ (\i. approx i\y)", simp) ``` huffman@25923 ` 104` ```apply (rule lub_mono, simp, simp, simp) ``` huffman@25903 ` 105` ```done ``` huffman@25903 ` 106` huffman@25903 ` 107` ```subsection {* Instance for continuous function space *} ``` huffman@25903 ` 108` huffman@27402 ` 109` ```lemma finite_range_cfun_lemma: ``` huffman@27402 ` 110` ``` assumes a: "finite (range (\x. a\x))" ``` huffman@27402 ` 111` ``` assumes b: "finite (range (\y. b\y))" ``` huffman@27402 ` 112` ``` shows "finite (range (\f. \ x. b\(f\(a\x))))" (is "finite (range ?h)") ``` huffman@27402 ` 113` ```proof (rule finite_imageD) ``` huffman@27402 ` 114` ``` let ?f = "\g. range (\x. (a\x, g\x))" ``` huffman@27402 ` 115` ``` show "finite (?f ` range ?h)" ``` huffman@27402 ` 116` ``` proof (rule finite_subset) ``` huffman@27402 ` 117` ``` let ?B = "Pow (range (\x. a\x) \ range (\y. b\y))" ``` huffman@27402 ` 118` ``` show "?f ` range ?h \ ?B" ``` huffman@27402 ` 119` ``` by clarsimp ``` huffman@27402 ` 120` ``` show "finite ?B" ``` huffman@27402 ` 121` ``` by (simp add: a b) ``` huffman@27402 ` 122` ``` qed ``` huffman@27402 ` 123` ``` show "inj_on ?f (range ?h)" ``` huffman@27402 ` 124` ``` proof (rule inj_onI, rule ext_cfun, clarsimp) ``` huffman@27402 ` 125` ``` fix x f g ``` huffman@27402 ` 126` ``` assume "range (\x. (a\x, b\(f\(a\x)))) = range (\x. (a\x, b\(g\(a\x))))" ``` huffman@27402 ` 127` ``` hence "range (\x. (a\x, b\(f\(a\x)))) \ range (\x. (a\x, b\(g\(a\x))))" ``` huffman@27402 ` 128` ``` by (rule equalityD1) ``` huffman@27402 ` 129` ``` hence "(a\x, b\(f\(a\x))) \ range (\x. (a\x, b\(g\(a\x))))" ``` huffman@27402 ` 130` ``` by (simp add: subset_eq) ``` huffman@27402 ` 131` ``` then obtain y where "(a\x, b\(f\(a\x))) = (a\y, b\(g\(a\y)))" ``` huffman@27402 ` 132` ``` by (rule rangeE) ``` huffman@27402 ` 133` ``` thus "b\(f\(a\x)) = b\(g\(a\x))" ``` huffman@27402 ` 134` ``` by clarsimp ``` huffman@27402 ` 135` ``` qed ``` huffman@27402 ` 136` ```qed ``` huffman@25903 ` 137` huffman@26962 ` 138` ```instantiation "->" :: (profinite, profinite) profinite ``` huffman@26962 ` 139` ```begin ``` huffman@25903 ` 140` huffman@26962 ` 141` ```definition ``` huffman@25903 ` 142` ``` approx_cfun_def: ``` huffman@26962 ` 143` ``` "approx = (\n. \ f x. approx n\(f\(approx n\x)))" ``` huffman@25903 ` 144` huffman@27402 ` 145` ```instance proof ``` huffman@27402 ` 146` ``` show "chain (approx :: nat \ ('a \ 'b) \ ('a \ 'b))" ``` huffman@27402 ` 147` ``` unfolding approx_cfun_def by simp ``` huffman@27402 ` 148` ```next ``` huffman@27402 ` 149` ``` fix x :: "'a \ 'b" ``` huffman@27402 ` 150` ``` show "(\i. approx i\x) = x" ``` huffman@27402 ` 151` ``` unfolding approx_cfun_def ``` huffman@27402 ` 152` ``` by (simp add: lub_distribs eta_cfun) ``` huffman@27402 ` 153` ```next ``` huffman@27402 ` 154` ``` fix i :: nat and x :: "'a \ 'b" ``` huffman@27402 ` 155` ``` show "approx i\(approx i\x) = approx i\x" ``` huffman@27402 ` 156` ``` unfolding approx_cfun_def by simp ``` huffman@27402 ` 157` ```next ``` huffman@27402 ` 158` ``` fix i :: nat ``` huffman@27402 ` 159` ``` show "finite {x::'a \ 'b. approx i\x = x}" ``` huffman@27402 ` 160` ``` apply (rule finite_range_imp_finite_fixes) ``` huffman@27402 ` 161` ``` apply (simp add: approx_cfun_def) ``` huffman@27402 ` 162` ``` apply (intro finite_range_cfun_lemma finite_range_approx) ``` huffman@27402 ` 163` ``` done ``` huffman@27402 ` 164` ```qed ``` huffman@25903 ` 165` huffman@26962 ` 166` ```end ``` huffman@26962 ` 167` huffman@26407 ` 168` ```instance "->" :: (profinite, bifinite) bifinite .. ``` huffman@25909 ` 169` huffman@25903 ` 170` ```lemma approx_cfun: "approx n\f\x = approx n\(f\(approx n\x))" ``` huffman@25903 ` 171` ```by (simp add: approx_cfun_def) ``` huffman@25903 ` 172` huffman@25903 ` 173` ```end ```