blanchet@55059: (* Title: HOL/BNF_Def.thy blanchet@48975: Author: Dmitriy Traytel, TU Muenchen blanchet@57398: Author: Jasmin Blanchette, TU Muenchen blanchet@48975: Copyright 2012 blanchet@48975: blanchet@48975: Definition of bounded natural functors. blanchet@48975: *) blanchet@48975: blanchet@48975: header {* Definition of Bounded Natural Functors *} blanchet@48975: blanchet@48975: theory BNF_Def blanchet@57398: imports BNF_Cardinal_Arithmetic Fun_Def_Base blanchet@48975: keywords blanchet@49286: "print_bnfs" :: diag and blanchet@51836: "bnf" :: thy_goal blanchet@48975: begin blanchet@48975: blanchet@57398: definition blanchet@57398: rel_fun :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" blanchet@57398: where blanchet@57398: "rel_fun A B = (\f g. \x y. A x y \ B (f x) (g y))" blanchet@57398: blanchet@57398: lemma rel_funI [intro]: blanchet@57398: assumes "\x y. A x y \ B (f x) (g y)" blanchet@57398: shows "rel_fun A B f g" blanchet@57398: using assms by (simp add: rel_fun_def) blanchet@57398: blanchet@57398: lemma rel_funD: blanchet@57398: assumes "rel_fun A B f g" and "A x y" blanchet@57398: shows "B (f x) (g y)" blanchet@57398: using assms by (simp add: rel_fun_def) blanchet@57398: blanchet@57398: definition collect where blanchet@57398: "collect F x = (\f \ F. f x)" blanchet@57398: blanchet@57398: lemma fstI: "x = (y, z) \ fst x = y" blanchet@57398: by simp blanchet@57398: blanchet@57398: lemma sndI: "x = (y, z) \ snd x = z" blanchet@57398: by simp blanchet@57398: blanchet@57398: lemma bijI': "\\x y. (f x = f y) = (x = y); \y. \x. y = f x\ \ bij f" blanchet@57398: unfolding bij_def inj_on_def by auto blast blanchet@57398: blanchet@57398: (* Operator: *) blanchet@57398: definition "Gr A f = {(a, f a) | a. a \ A}" blanchet@57398: blanchet@57398: definition "Grp A f = (\a b. b = f a \ a \ A)" blanchet@57398: blanchet@57398: definition vimage2p where blanchet@57398: "vimage2p f g R = (\x y. R (f x) (g y))" blanchet@57398: blanchet@56635: lemma collect_comp: "collect F \ g = collect ((\f. f \ g) ` F)" blanchet@55066: by (rule ext) (auto simp only: comp_apply collect_def) traytel@51893: traytel@49495: definition convol ("<_ , _>") where traytel@49495: " \ %a. (f a, g a)" traytel@49495: traytel@49495: lemma fst_convol: blanchet@56635: "fst \ = f" traytel@49495: apply(rule ext) traytel@49495: unfolding convol_def by simp traytel@49495: traytel@49495: lemma snd_convol: blanchet@56635: "snd \ = g" traytel@49495: apply(rule ext) traytel@49495: unfolding convol_def by simp traytel@49495: traytel@51893: lemma convol_mem_GrpI: traytel@52986: "x \ A \ x \ (Collect (split (Grp A g)))" traytel@51893: unfolding convol_def Grp_def by auto traytel@51893: blanchet@49312: definition csquare where blanchet@49312: "csquare A f1 f2 p1 p2 \ (\ a \ A. f1 (p1 a) = f2 (p2 a))" blanchet@49312: traytel@51893: lemma eq_alt: "op = = Grp UNIV id" traytel@51893: unfolding Grp_def by auto traytel@51893: traytel@51893: lemma leq_conversepI: "R = op = \ R \ R^--1" traytel@51893: by auto traytel@51893: traytel@54841: lemma leq_OOI: "R = op = \ R \ R OO R" traytel@51893: by auto traytel@51893: traytel@53561: lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\x y. \z. z \ A \ f z = x \ g z = y)" traytel@53561: unfolding Grp_def by auto traytel@53561: traytel@51893: lemma Grp_UNIV_id: "f = id \ (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f" traytel@51893: unfolding Grp_def by auto traytel@51893: traytel@51893: lemma Grp_UNIV_idI: "x = y \ Grp UNIV id x y" traytel@51893: unfolding Grp_def by auto traytel@51893: traytel@51893: lemma Grp_mono: "A \ B \ Grp A f \ Grp B f" traytel@51893: unfolding Grp_def by auto traytel@51893: traytel@51893: lemma GrpI: "\f x = y; x \ A\ \ Grp A f x y" traytel@51893: unfolding Grp_def by auto traytel@51893: traytel@51893: lemma GrpE: "Grp A f x y \ (\f x = y; x \ A\ \ R) \ R" traytel@51893: unfolding Grp_def by auto traytel@51893: traytel@51893: lemma Collect_split_Grp_eqD: "z \ Collect (split (Grp A f)) \ (f \ fst) z = snd z" blanchet@55066: unfolding Grp_def comp_def by auto traytel@51893: traytel@51893: lemma Collect_split_Grp_inD: "z \ Collect (split (Grp A f)) \ fst z \ A" blanchet@55066: unfolding Grp_def comp_def by auto traytel@51893: traytel@51893: definition "pick_middlep P Q a c = (SOME b. P a b \ Q b c)" traytel@51893: traytel@51893: lemma pick_middlep: traytel@51893: "(P OO Q) a c \ P a (pick_middlep P Q a c) \ Q (pick_middlep P Q a c) c" traytel@51893: unfolding pick_middlep_def apply(rule someI_ex) by auto blanchet@49312: traytel@51893: definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))" traytel@51893: definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))" traytel@51893: traytel@51893: lemma fstOp_in: "ac \ Collect (split (P OO Q)) \ fstOp P Q ac \ Collect (split P)" traytel@51893: unfolding fstOp_def mem_Collect_eq blanchet@55642: by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1]) blanchet@49312: traytel@51893: lemma fst_fstOp: "fst bc = (fst \ fstOp P Q) bc" traytel@51893: unfolding comp_def fstOp_def by simp traytel@51893: traytel@51893: lemma snd_sndOp: "snd bc = (snd \ sndOp P Q) bc" traytel@51893: unfolding comp_def sndOp_def by simp traytel@51893: traytel@51893: lemma sndOp_in: "ac \ Collect (split (P OO Q)) \ sndOp P Q ac \ Collect (split Q)" traytel@51893: unfolding sndOp_def mem_Collect_eq blanchet@55642: by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2]) traytel@51893: traytel@51893: lemma csquare_fstOp_sndOp: traytel@51893: "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" traytel@51893: unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp traytel@51893: blanchet@56635: lemma snd_fst_flip: "snd xy = (fst \ (%(x, y). (y, x))) xy" blanchet@49312: by (simp split: prod.split) blanchet@49312: blanchet@56635: lemma fst_snd_flip: "fst xy = (snd \ (%(x, y). (y, x))) xy" blanchet@49312: by (simp split: prod.split) blanchet@49312: traytel@51893: lemma flip_pred: "A \ Collect (split (R ^--1)) \ (%(x, y). (y, x)) ` A \ Collect (split R)" traytel@51893: by auto traytel@51893: traytel@51893: lemma Collect_split_mono: "A \ B \ Collect (split A) \ Collect (split B)" traytel@51893: by auto traytel@51893: traytel@51916: lemma Collect_split_mono_strong: traytel@55163: "\X = fst ` A; Y = snd ` A; \a\X. \b \ Y. P a b \ Q a b; A \ Collect (split P)\ \ traytel@51916: A \ Collect (split Q)" traytel@51916: by fastforce traytel@51916: traytel@55163: traytel@51917: lemma predicate2_eqD: "A = B \ A a b \ B a b" traytel@55811: by simp blanchet@49537: blanchet@55414: lemma case_sum_o_inj: blanchet@55414: "case_sum f g \ Inl = f" blanchet@55414: "case_sum f g \ Inr = g" traytel@52635: by auto traytel@52635: traytel@52635: lemma card_order_csum_cone_cexp_def: traytel@52635: "card_order r \ ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \ {Inr ()})|" traytel@52635: unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order) traytel@52635: traytel@52635: lemma If_the_inv_into_in_Func: traytel@52635: "\inj_on g C; C \ B \ {x}\ \ traytel@52635: (\i. if i \ g ` C then the_inv_into C g i else x) \ Func UNIV (B \ {x})" traytel@52635: unfolding Func_def by (auto dest: the_inv_into_into) traytel@52635: traytel@52635: lemma If_the_inv_into_f_f: traytel@52635: "\i \ C; inj_on g C\ \ blanchet@56635: ((\i. if i \ g ` C then the_inv_into C g i else x) \ g) i = id i" traytel@52635: unfolding Func_def by (auto elim: the_inv_into_f_f) traytel@52635: blanchet@56635: lemma the_inv_f_o_f_id: "inj f \ (the_inv f \ f) z = id z" blanchet@56635: by (simp add: the_inv_f_f) blanchet@56635: traytel@52731: lemma vimage2pI: "R (f x) (g y) \ vimage2p f g R x y" traytel@52731: unfolding vimage2p_def by - traytel@52719: blanchet@55945: lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \ vimage2p f g S)" blanchet@55945: unfolding rel_fun_def vimage2p_def by auto traytel@52719: blanchet@56635: lemma convol_image_vimage2p: " fst, g \ snd> ` Collect (split (vimage2p f g R)) \ Collect (split R)" traytel@52731: unfolding vimage2p_def convol_def by auto traytel@52719: traytel@54961: lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\\" traytel@54961: unfolding vimage2p_def Grp_def by auto traytel@54961: blanchet@57398: ML_file "Tools/BNF/bnf_util.ML" blanchet@57398: ML_file "Tools/BNF/bnf_tactics.ML" blanchet@55062: ML_file "Tools/BNF/bnf_def_tactics.ML" blanchet@55062: ML_file "Tools/BNF/bnf_def.ML" blanchet@49309: blanchet@48975: end