src/HOL/BNF/BNF_Def.thy
 author traytel Thu Jul 25 12:25:07 2013 +0200 (2013-07-25) changeset 52730 6bf02eb4ddf7 parent 52719 480a3479fa47 child 52731 dacd47a0633f permissions -rw-r--r--
two useful relation theorems
 blanchet@49509 ` 1` ```(* Title: HOL/BNF/BNF_Def.thy ``` blanchet@48975 ` 2` ``` Author: Dmitriy Traytel, TU Muenchen ``` blanchet@48975 ` 3` ``` Copyright 2012 ``` blanchet@48975 ` 4` blanchet@48975 ` 5` ```Definition of bounded natural functors. ``` blanchet@48975 ` 6` ```*) ``` blanchet@48975 ` 7` blanchet@48975 ` 8` ```header {* Definition of Bounded Natural Functors *} ``` blanchet@48975 ` 9` blanchet@48975 ` 10` ```theory BNF_Def ``` blanchet@49282 ` 11` ```imports BNF_Util ``` blanchet@48975 ` 12` ```keywords ``` blanchet@49286 ` 13` ``` "print_bnfs" :: diag and ``` blanchet@51836 ` 14` ``` "bnf" :: thy_goal ``` blanchet@48975 ` 15` ```begin ``` blanchet@48975 ` 16` blanchet@49312 ` 17` ```lemma collect_o: "collect F o g = collect ((\f. f o g) ` F)" ``` blanchet@49312 ` 18` ```by (rule ext) (auto simp only: o_apply collect_def) ``` blanchet@49312 ` 19` blanchet@49312 ` 20` ```lemma converse_shift: ``` blanchet@49312 ` 21` ```"R1 \ R2 ^-1 \ R1 ^-1 \ R2" ``` blanchet@49312 ` 22` ```unfolding converse_def by auto ``` blanchet@49312 ` 23` traytel@51893 ` 24` ```lemma conversep_shift: ``` traytel@51893 ` 25` ```"R1 \ R2 ^--1 \ R1 ^--1 \ R2" ``` traytel@51893 ` 26` ```unfolding conversep.simps by auto ``` traytel@51893 ` 27` traytel@49495 ` 28` ```definition convol ("<_ , _>") where ``` traytel@49495 ` 29` ```" \ %a. (f a, g a)" ``` traytel@49495 ` 30` traytel@49495 ` 31` ```lemma fst_convol: ``` traytel@49495 ` 32` ```"fst o = f" ``` traytel@49495 ` 33` ```apply(rule ext) ``` traytel@49495 ` 34` ```unfolding convol_def by simp ``` traytel@49495 ` 35` traytel@49495 ` 36` ```lemma snd_convol: ``` traytel@49495 ` 37` ```"snd o = g" ``` traytel@49495 ` 38` ```apply(rule ext) ``` traytel@49495 ` 39` ```unfolding convol_def by simp ``` traytel@49495 ` 40` traytel@51893 ` 41` ```lemma convol_mem_GrpI: ``` traytel@51893 ` 42` ```"\g x = g' x; x \ A\ \ x \ (Collect (split (Grp A g)))" ``` traytel@51893 ` 43` ```unfolding convol_def Grp_def by auto ``` traytel@51893 ` 44` blanchet@49312 ` 45` ```definition csquare where ``` blanchet@49312 ` 46` ```"csquare A f1 f2 p1 p2 \ (\ a \ A. f1 (p1 a) = f2 (p2 a))" ``` blanchet@49312 ` 47` blanchet@49312 ` 48` ```(* The pullback of sets *) ``` blanchet@49312 ` 49` ```definition thePull where ``` blanchet@49312 ` 50` ```"thePull B1 B2 f1 f2 = {(b1,b2). b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2}" ``` blanchet@49312 ` 51` blanchet@49312 ` 52` ```lemma wpull_thePull: ``` blanchet@49312 ` 53` ```"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" ``` blanchet@49312 ` 54` ```unfolding wpull_def thePull_def by auto ``` blanchet@49312 ` 55` blanchet@49312 ` 56` ```lemma wppull_thePull: ``` blanchet@49312 ` 57` ```assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" ``` blanchet@49312 ` 58` ```shows ``` blanchet@49312 ` 59` ```"\ j. \ a' \ thePull B1 B2 f1 f2. ``` blanchet@49312 ` 60` ``` j a' \ A \ ``` blanchet@49312 ` 61` ``` e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" ``` blanchet@49312 ` 62` ```(is "\ j. \ a' \ ?A'. ?phi a' (j a')") ``` blanchet@49312 ` 63` ```proof(rule bchoice[of ?A' ?phi], default) ``` blanchet@49312 ` 64` ``` fix a' assume a': "a' \ ?A'" ``` blanchet@49312 ` 65` ``` hence "fst a' \ B1" unfolding thePull_def by auto ``` blanchet@49312 ` 66` ``` moreover ``` blanchet@49312 ` 67` ``` from a' have "snd a' \ B2" unfolding thePull_def by auto ``` blanchet@49312 ` 68` ``` moreover have "f1 (fst a') = f2 (snd a')" ``` blanchet@49312 ` 69` ``` using a' unfolding csquare_def thePull_def by auto ``` blanchet@49312 ` 70` ``` ultimately show "\ ja'. ?phi a' ja'" ``` blanchet@49325 ` 71` ``` using assms unfolding wppull_def by blast ``` blanchet@49312 ` 72` ```qed ``` blanchet@49312 ` 73` blanchet@49312 ` 74` ```lemma wpull_wppull: ``` blanchet@49312 ` 75` ```assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and ``` blanchet@49312 ` 76` ```1: "\ a' \ A'. j a' \ A \ e1 (p1 (j a')) = e1 (p1' a') \ e2 (p2 (j a')) = e2 (p2' a')" ``` blanchet@49312 ` 77` ```shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" ``` blanchet@49312 ` 78` ```unfolding wppull_def proof safe ``` blanchet@49312 ` 79` ``` fix b1 b2 ``` blanchet@49312 ` 80` ``` assume b1: "b1 \ B1" and b2: "b2 \ B2" and f: "f1 b1 = f2 b2" ``` blanchet@49312 ` 81` ``` then obtain a' where a': "a' \ A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" ``` blanchet@49312 ` 82` ``` using wp unfolding wpull_def by blast ``` blanchet@49312 ` 83` ``` show "\a\A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2" ``` blanchet@49325 ` 84` ``` apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto ``` blanchet@49312 ` 85` ```qed ``` blanchet@49312 ` 86` blanchet@49312 ` 87` ```lemma wppull_id: "\wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\ \ ``` blanchet@49312 ` 88` ``` wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2" ``` blanchet@49312 ` 89` ```by (erule wpull_wppull) auto ``` blanchet@49312 ` 90` traytel@51893 ` 91` ```lemma eq_alt: "op = = Grp UNIV id" ``` traytel@51893 ` 92` ```unfolding Grp_def by auto ``` traytel@51893 ` 93` traytel@51893 ` 94` ```lemma leq_conversepI: "R = op = \ R \ R^--1" ``` traytel@51893 ` 95` ``` by auto ``` traytel@51893 ` 96` traytel@51893 ` 97` ```lemma eq_OOI: "R = op = \ R = R OO R" ``` traytel@51893 ` 98` ``` by auto ``` traytel@51893 ` 99` traytel@51893 ` 100` ```lemma Grp_UNIV_id: "f = id \ (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f" ``` traytel@51893 ` 101` ```unfolding Grp_def by auto ``` traytel@51893 ` 102` traytel@51893 ` 103` ```lemma Grp_UNIV_idI: "x = y \ Grp UNIV id x y" ``` traytel@51893 ` 104` ```unfolding Grp_def by auto ``` traytel@51893 ` 105` traytel@51893 ` 106` ```lemma Grp_mono: "A \ B \ Grp A f \ Grp B f" ``` traytel@51893 ` 107` ```unfolding Grp_def by auto ``` traytel@51893 ` 108` traytel@51893 ` 109` ```lemma GrpI: "\f x = y; x \ A\ \ Grp A f x y" ``` traytel@51893 ` 110` ```unfolding Grp_def by auto ``` traytel@51893 ` 111` traytel@51893 ` 112` ```lemma GrpE: "Grp A f x y \ (\f x = y; x \ A\ \ R) \ R" ``` traytel@51893 ` 113` ```unfolding Grp_def by auto ``` traytel@51893 ` 114` traytel@51893 ` 115` ```lemma Collect_split_Grp_eqD: "z \ Collect (split (Grp A f)) \ (f \ fst) z = snd z" ``` traytel@51893 ` 116` ```unfolding Grp_def o_def by auto ``` traytel@51893 ` 117` traytel@51893 ` 118` ```lemma Collect_split_Grp_inD: "z \ Collect (split (Grp A f)) \ fst z \ A" ``` traytel@51893 ` 119` ```unfolding Grp_def o_def by auto ``` traytel@51893 ` 120` traytel@51893 ` 121` ```lemma wpull_Grp: ``` traytel@51893 ` 122` ```"wpull (Collect (split (Grp A f))) A (f ` A) f id fst snd" ``` traytel@51893 ` 123` ```unfolding wpull_def Grp_def by auto ``` traytel@51893 ` 124` traytel@51893 ` 125` ```definition "pick_middlep P Q a c = (SOME b. P a b \ Q b c)" ``` traytel@51893 ` 126` traytel@51893 ` 127` ```lemma pick_middlep: ``` traytel@51893 ` 128` ```"(P OO Q) a c \ P a (pick_middlep P Q a c) \ Q (pick_middlep P Q a c) c" ``` traytel@51893 ` 129` ```unfolding pick_middlep_def apply(rule someI_ex) by auto ``` blanchet@49312 ` 130` traytel@51893 ` 131` ```definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))" ``` traytel@51893 ` 132` ```definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))" ``` traytel@51893 ` 133` traytel@51893 ` 134` ```lemma fstOp_in: "ac \ Collect (split (P OO Q)) \ fstOp P Q ac \ Collect (split P)" ``` traytel@51893 ` 135` ```unfolding fstOp_def mem_Collect_eq ``` traytel@51893 ` 136` ```by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct1]) ``` blanchet@49312 ` 137` traytel@51893 ` 138` ```lemma fst_fstOp: "fst bc = (fst \ fstOp P Q) bc" ``` traytel@51893 ` 139` ```unfolding comp_def fstOp_def by simp ``` traytel@51893 ` 140` traytel@51893 ` 141` ```lemma snd_sndOp: "snd bc = (snd \ sndOp P Q) bc" ``` traytel@51893 ` 142` ```unfolding comp_def sndOp_def by simp ``` traytel@51893 ` 143` traytel@51893 ` 144` ```lemma sndOp_in: "ac \ Collect (split (P OO Q)) \ sndOp P Q ac \ Collect (split Q)" ``` traytel@51893 ` 145` ```unfolding sndOp_def mem_Collect_eq ``` traytel@51893 ` 146` ```by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2]) ``` traytel@51893 ` 147` traytel@51893 ` 148` ```lemma csquare_fstOp_sndOp: ``` traytel@51893 ` 149` ```"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" ``` traytel@51893 ` 150` ```unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp ``` traytel@51893 ` 151` traytel@51893 ` 152` ```lemma wppull_fstOp_sndOp: ``` traytel@51909 ` 153` ```shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) ``` traytel@51909 ` 154` ``` snd fst fst snd (fstOp P Q) (sndOp P Q)" ``` traytel@51893 ` 155` ```using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto ``` traytel@51893 ` 156` blanchet@49312 ` 157` ```lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" ``` blanchet@49312 ` 158` ```by (simp split: prod.split) ``` blanchet@49312 ` 159` blanchet@49312 ` 160` ```lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy" ``` blanchet@49312 ` 161` ```by (simp split: prod.split) ``` blanchet@49312 ` 162` traytel@51893 ` 163` ```lemma flip_pred: "A \ Collect (split (R ^--1)) \ (%(x, y). (y, x)) ` A \ Collect (split R)" ``` traytel@51893 ` 164` ```by auto ``` traytel@51893 ` 165` traytel@51893 ` 166` ```lemma Collect_split_mono: "A \ B \ Collect (split A) \ Collect (split B)" ``` traytel@51893 ` 167` ``` by auto ``` traytel@51893 ` 168` traytel@51916 ` 169` ```lemma Collect_split_mono_strong: ``` traytel@51916 ` 170` ``` "\\a\fst ` A. \b \ snd ` A. P a b \ Q a b; A \ Collect (split P)\ \ ``` traytel@51916 ` 171` ``` A \ Collect (split Q)" ``` traytel@51916 ` 172` ``` by fastforce ``` traytel@51916 ` 173` traytel@51917 ` 174` ```lemma predicate2_eqD: "A = B \ A a b \ B a b" ``` traytel@51893 ` 175` ```by metis ``` blanchet@49537 ` 176` traytel@52635 ` 177` ```lemma sum_case_o_inj: ``` traytel@52635 ` 178` ```"sum_case f g \ Inl = f" ``` traytel@52635 ` 179` ```"sum_case f g \ Inr = g" ``` traytel@52635 ` 180` ```by auto ``` traytel@52635 ` 181` traytel@52635 ` 182` ```lemma card_order_csum_cone_cexp_def: ``` traytel@52635 ` 183` ``` "card_order r \ ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \ {Inr ()})|" ``` traytel@52635 ` 184` ``` unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order) ``` traytel@52635 ` 185` traytel@52635 ` 186` ```lemma If_the_inv_into_in_Func: ``` traytel@52635 ` 187` ``` "\inj_on g C; C \ B \ {x}\ \ ``` traytel@52635 ` 188` ``` (\i. if i \ g ` C then the_inv_into C g i else x) \ Func UNIV (B \ {x})" ``` traytel@52635 ` 189` ```unfolding Func_def by (auto dest: the_inv_into_into) ``` traytel@52635 ` 190` traytel@52635 ` 191` ```lemma If_the_inv_into_f_f: ``` traytel@52635 ` 192` ``` "\i \ C; inj_on g C\ \ ``` traytel@52635 ` 193` ``` ((\i. if i \ g ` C then the_inv_into C g i else x) o g) i = id i" ``` traytel@52635 ` 194` ```unfolding Func_def by (auto elim: the_inv_into_f_f) ``` traytel@52635 ` 195` traytel@52719 ` 196` ```definition vimagep where ``` traytel@52719 ` 197` ``` "vimagep f g R = (\x y. R (f x) (g y))" ``` traytel@52719 ` 198` traytel@52719 ` 199` ```lemma vimagepI: "R (f x) (g y) \ vimagep f g R x y" ``` traytel@52719 ` 200` ``` unfolding vimagep_def by - ``` traytel@52719 ` 201` traytel@52719 ` 202` ```lemma vimagepD: "vimagep f g R x y \ R (f x) (g y)" ``` traytel@52719 ` 203` ``` unfolding vimagep_def by - ``` traytel@52719 ` 204` traytel@52719 ` 205` ```lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \ vimagep f g S)" ``` traytel@52719 ` 206` ``` unfolding fun_rel_def vimagep_def by auto ``` traytel@52719 ` 207` traytel@52719 ` 208` ```lemma convol_image_vimagep: " ` Collect (split (vimagep f g R)) \ Collect (split R)" ``` traytel@52719 ` 209` ``` unfolding vimagep_def convol_def by auto ``` traytel@52719 ` 210` blanchet@49309 ` 211` ```ML_file "Tools/bnf_def_tactics.ML" ``` blanchet@49537 ` 212` ```ML_file "Tools/bnf_def.ML" ``` blanchet@49309 ` 213` traytel@51893 ` 214` blanchet@48975 ` 215` ```end ```