# HG changeset patch # User traytel # Date 1373185440 -7200 # Node ID d2ad6eae514fdcc94b17dd6e01acbce311e7b5d3 # Parent 0c4b140cff00533c475908e2ad52435ca4065e2f Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type) diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/BNF/Basic_BNFs.thy --- a/src/HOL/BNF/Basic_BNFs.thy Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/BNF/Basic_BNFs.thy Sun Jul 07 10:24:00 2013 +0200 @@ -317,7 +317,7 @@ lemma card_of_bounded_range: "|{f :: 'd \ 'a. range f \ B}| \o |Func (UNIV :: 'd set) B|" (is "|?LHS| \o |?RHS|") proof - - let ?f = "\f. %x. if f x \ B then Some (f x) else None" + let ?f = "\f. %x. if f x \ B then f x else undefined" have "inj_on ?f ?LHS" unfolding inj_on_def proof (unfold fun_eq_iff, safe) fix g :: "'d \ 'a" and f :: "'d \ 'a" and x diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Sun Jul 07 10:24:00 2013 +0200 @@ -129,7 +129,7 @@ apply (rule ordLeq_transitive) apply (rule card_of_list_in) apply (rule ordLeq_transitive) - apply (erule card_of_Pfunc_Pow_Func) + apply (erule card_of_Pfunc_Pow_Func_option) apply (rule ordIso_ordLeq_trans) apply (rule Times_cprod) apply (rule cprod_cinfinite_bound) @@ -145,6 +145,8 @@ apply (rule Card_order_ctwo) apply (rule natLeq_Card_order) apply (rule ordIso_ordLeq_trans) + apply (rule card_of_Func_option_Func) + apply (rule ordIso_ordLeq_trans) apply (rule card_of_Func) apply (rule ordIso_ordLeq_trans) apply (rule cexp_cong2) diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Jul 07 10:24:00 2013 +0200 @@ -2443,7 +2443,7 @@ val timer = time (timer "map functions for the new codatatypes"); - val bd = mk_ccexp sbd sbd; + val bd = mk_cexp sbd sbd; val timer = time (timer "bounds for the new codatatypes"); @@ -2694,7 +2694,7 @@ (fn {context = ctxt, prems = _} => mk_in_bd_tac ctxt (nth isNode_hsets (i - 1)) isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets - sbd_Cnotzero sbd_Card_order mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm)) + mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm)) ks isNode_hset_thmss carT_defs card_of_carT_thms mor_image'_thms Rep_inverses (transpose mor_hset_thmss); diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Jul 07 10:24:00 2013 +0200 @@ -58,7 +58,7 @@ val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_in_bd_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> - thm -> thm -> thm -> thm -> thm -> thm -> tactic + thm -> thm -> thm -> thm -> tactic val mk_incl_lsbis_tac: int -> int -> thm -> tactic val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_length_Lev'_tac: thm -> tactic @@ -480,8 +480,7 @@ rtac sbd_Cinfinite, if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum}, rtac @{thm Cnotzero_clists}, - rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Func_Ffunc}, - rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp}, + rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp}, rtac ctrans, rtac @{thm cexp_mono}, rtac @{thm ordLeq_ordIso_trans}, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @@ -530,7 +529,7 @@ rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2, rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans), rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE}, - hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp), + hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Func_def} RS equalityD2 RS set_mp), rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1, CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY' [rtac (mk_UnIN n i), dtac (def RS iffD1), @@ -1324,10 +1323,10 @@ EVERY' (map rtac [ordIso_ordLeq_trans, @{thm card_of_ordIso_subst}, hset_def, ctrans, @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat}, @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite, - ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1; + @{thm infinite_ordLeq_cexp}, sbd_Cinfinite]) 1; fun mk_in_bd_tac ctxt isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets - sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg = + mor_Rep coalgT mor_T_final tcoalg = let val n = length isNode_hsets; val in_hin_tac = rtac CollectI THEN' @@ -1339,9 +1338,7 @@ EVERY' [rtac (Thm.permute_prems 0 1 @{thm ordLeq_transitive}), rtac ctrans, rtac @{thm card_of_image}, rtac ordIso_ordLeq_trans, rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans, - rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero}, - rtac @{thm cexp_ordLeq_ccexp}, rtac @{thm Card_order_csum}, - rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order, + rtac @{thm card_of_image}, rtac card_of_carT, rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym, rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE, @@ -1363,10 +1360,10 @@ end; fun mk_bd_card_order_tac sbd_card_order = - EVERY' (map rtac [@{thm card_order_ccexp}, sbd_card_order, sbd_card_order]) 1; + EVERY' (map rtac [@{thm card_order_cexp}, sbd_card_order, sbd_card_order]) 1; fun mk_bd_cinfinite_tac sbd_Cinfinite = - EVERY' (map rtac [@{thm cinfinite_ccexp}, @{thm ctwo_ordLeq_Cinfinite}, + EVERY' (map rtac [@{thm cinfinite_cexp}, @{thm ctwo_ordLeq_Cinfinite}, sbd_Cinfinite, sbd_Cinfinite]) 1; fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq = diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Sun Jul 07 10:24:00 2013 +0200 @@ -76,7 +76,6 @@ val mk_predT: typ list -> typ val mk_pred1T: typ -> typ val mk_pred2T: typ -> typ -> typ - val mk_optionT: typ -> typ val mk_relT: typ * typ -> typ val dest_relT: typ -> typ * typ val dest_pred2T: typ -> typ * typ @@ -100,7 +99,6 @@ val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term val mk_card_of: term -> term val mk_card_order: term -> term - val mk_ccexp: term -> term -> term val mk_cexp: term -> term -> term val mk_cinfinite: term -> term val mk_collect: term list -> typ -> term @@ -400,12 +398,10 @@ fun mk_predT Ts = Ts ---> HOLogic.boolT; fun mk_pred1T T = mk_predT [T]; fun mk_pred2T T U = mk_predT [T, U]; -fun mk_optionT T = Type (@{type_name option}, [T]); val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; val dest_pred2T = apsnd Term.domain_type o Term.dest_funT; fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]); -fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT; (** Constants **) @@ -576,8 +572,7 @@ val mk_csum = mk_card_binop @{const_name csum} mk_sumT; val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT; -val mk_cexp = mk_card_binop @{const_name cexp} mk_partial_funT; -val mk_ccexp = mk_card_binop @{const_name ccexp} mk_partial_funT; +val mk_cexp = mk_card_binop @{const_name cexp} (op --> o swap); val ctwo = @{term ctwo}; fun mk_collect xs defT = diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/Cardinals/Cardinal_Arithmetic.thy --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Sun Jul 07 10:24:00 2013 +0200 @@ -369,19 +369,12 @@ definition cexp (infixr "^c" 90) where "r1 ^c r2 \ |Func (Field r2) (Field r1)|" -definition ccexp (infixr "^^c" 90) where - "r1 ^^c r2 \ |Pfunc (Field r2) (Field r1)|" - -lemma cexp_ordLeq_ccexp: "r1 ^c r2 \o r1 ^^c r2" -unfolding cexp_def ccexp_def by (rule card_of_mono1) (rule Func_Pfunc) - -lemma card_order_ccexp: +lemma card_order_cexp: assumes "card_order r1" "card_order r2" - shows "card_order (r1 ^^c r2)" + shows "card_order (r1 ^c r2)" proof - have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto - thus ?thesis unfolding ccexp_def Pfunc_def - by (auto simp: card_of_card_order_on split: option.split) + thus ?thesis unfolding cexp_def Func_def by (simp add: card_of_card_order_on) qed lemma Card_order_cexp: "Card_order (r1 ^c r2)" @@ -393,11 +386,12 @@ shows "p1 ^c p2 \o r1 ^c r2" proof(cases "Field p1 = {}") case True - hence "|Field (p1 ^c p2)| \o cone" - unfolding czero_def cone_def cexp_def Field_card_of + hence "|Field |Func (Field p2) (Field p1)|| \o cone" + unfolding cone_def Field_card_of by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty) (metis Func_is_emp card_of_empty ex_in_conv) - hence "p1 ^c p2 \o cone" by (simp add: Field_card_of cexp_def) + hence "|Func (Field p2) (Field p1)| \o cone" by (simp add: Field_card_of cexp_def) + hence "p1 ^c p2 \o cone" unfolding cexp_def . thus ?thesis proof (cases "Field p2 = {}") case True @@ -406,7 +400,7 @@ thus ?thesis using `p1 ^c p2 \o cone` ordLeq_transitive by auto next case False with True have "|Field (p1 ^c p2)| =o czero" - unfolding card_of_ordIso_czero_iff_empty cexp_def Func_is_emp Field_card_of by blast + unfolding card_of_ordIso_czero_iff_empty cexp_def Field_card_of Func_def by auto thus ?thesis unfolding cexp_def card_of_ordIso_czero_iff_empty Field_card_of by (simp add: card_of_empty) qed @@ -490,7 +484,7 @@ have "r ^c cone =o |Field r|" unfolding cexp_def cone_def Field_card_of Func_empty card_of_ordIso[symmetric] bij_betw_def Func_def inj_on_def image_def - by (rule exI[of _ "\f. case f () of Some a \ a"]) auto + by (rule exI[of _ "\f. f ()"]) auto also have "|Field r| =o r" by (rule card_of_Field_ordIso[OF assms]) finally show ?thesis . qed @@ -624,9 +618,6 @@ lemma cinfinite_cexp: "\ctwo \o q; Cinfinite r\ \ cinfinite (q ^c r)" by (metis assms cinfinite_mono ordLeq_cexp2) -lemma cinfinite_ccexp: "\ctwo \o q; Cinfinite r\ \ cinfinite (q ^^c r)" -by (rule cinfinite_mono[OF cexp_ordLeq_ccexp cinfinite_cexp]) - lemma Cinfinite_cexp: "\ctwo \o q; Cinfinite r\ \ Cinfinite (q ^c r)" by (simp add: cinfinite_cexp Card_order_cexp) @@ -754,7 +745,7 @@ "r1 *c r2 \o (r1 +c r2) ^c ctwo" unfolding cprod_def csum_def cexp_def ctwo_def Field_card_of proof - - let ?f = "\(a, b). %x. if x then Some (Inl a) else Some (Inr b)" + let ?f = "\(a, b). %x. if x then Inl a else Inr b" have "inj_on ?f (Field r1 \ Field r2)" (is "inj_on _ ?LHS") by (auto simp: inj_on_def fun_eq_iff split: bool.split) moreover diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/Cardinals/Cardinal_Order_Relation.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Sun Jul 07 10:24:00 2013 +0200 @@ -75,7 +75,6 @@ card_of_Plus_ordLeq_infinite_Field[simp] curr_in[intro, simp] Func_empty[simp] - Func_map_empty[simp] Func_is_emp[simp] @@ -1045,18 +1044,103 @@ using ordLeq_card_Bpow[OF rc r] by (metis A card_of_ordLeq_infinite) +definition Func_option where + "Func_option A B \ + {f. (\ a. f a \ None \ a \ A) \ (\ a \ A. case f a of Some b \ b \ B |None \ True)}" + +lemma card_of_Func_option_Func: +"|Func_option A B| =o |Func A B|" +proof (rule ordIso_symmetric, unfold card_of_ordIso[symmetric], intro exI) + let ?F = "\ f a. if a \ A then Some (f a) else None" + show "bij_betw ?F (Func A B) (Func_option A B)" + unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI) + fix f g assume f: "f \ Func A B" and g: "g \ Func A B" and eq: "?F f = ?F g" + show "f = g" + proof(rule ext) + fix a + show "f a = g a" + proof(cases "a \ A") + case True + have "Some (f a) = ?F f a" using True by auto + also have "... = ?F g a" using eq unfolding fun_eq_iff by(rule allE) + also have "... = Some (g a)" using True by auto + finally have "Some (f a) = Some (g a)" . + thus ?thesis by simp + qed(insert f g, unfold Func_def, auto) + qed + next + show "?F ` Func A B = Func_option A B" + proof safe + fix f assume f: "f \ Func_option A B" + def g \ "\ a. case f a of Some b \ b | None \ undefined" + have "g \ Func A B" + using f unfolding g_def Func_def Func_option_def by force+ + moreover have "f = ?F g" + proof(rule ext) + fix a show "f a = ?F g a" + using f unfolding Func_option_def g_def by (cases "a \ A") force+ + qed + ultimately show "f \ ?F ` (Func A B)" by blast + qed(unfold Func_def Func_option_def, auto) + qed +qed + +(* partial-function space: *) +definition Pfunc where +"Pfunc A B \ + {f. (\a. f a \ None \ a \ A) \ + (\a. case f a of None \ True | Some b \ b \ B)}" + +lemma Func_Pfunc: +"Func_option A B \ Pfunc A B" +unfolding Func_option_def Pfunc_def by auto + +lemma Pfunc_Func_option: +"Pfunc A B = (\ A' \ Pow A. Func_option A' B)" +proof safe + fix f assume f: "f \ Pfunc A B" + show "f \ (\A'\Pow A. Func_option A' B)" + proof (intro UN_I) + let ?A' = "{a. f a \ None}" + show "?A' \ Pow A" using f unfolding Pow_def Pfunc_def by auto + show "f \ Func_option ?A' B" using f unfolding Func_option_def Pfunc_def by auto + qed +next + fix f A' assume "f \ Func_option A' B" and "A' \ A" + thus "f \ Pfunc A B" unfolding Func_option_def Pfunc_def by auto +qed + +lemma card_of_Func_option_mono: +fixes A1 A2 :: "'a set" and B :: "'b set" +assumes A12: "A1 \ A2" and B: "B \ {}" +shows "|Func_option A1 B| \o |Func_option A2 B|" +by (metis card_of_Func_mono[OF A12 B] card_of_Func_option_Func + ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric) + +lemma card_of_Pfunc_Pow_Func_option: +assumes "B \ {}" +shows "|Pfunc A B| \o |Pow A <*> Func_option A B|" +proof- + have "|Pfunc A B| =o |\ A' \ Pow A. Func_option A' B|" (is "_ =o ?K") + unfolding Pfunc_Func_option by(rule card_of_refl) + also have "?K \o |Sigma (Pow A) (\ A'. Func_option A' B)|" using card_of_UNION_Sigma . + also have "|Sigma (Pow A) (\ A'. Func_option A' B)| \o |Pow A <*> Func_option A B|" + apply(rule card_of_Sigma_mono1) using card_of_Func_option_mono[OF _ assms] by auto + finally show ?thesis . +qed + lemma Bpow_ordLeq_Func_Field: assumes rc: "Card_order r" and r: "Field r \ {}" and A: "infinite A" shows "|Bpow r A| \o |Func (Field r) A|" proof- - let ?F = "\ f. {x | x a. f a = Some x}" + let ?F = "\ f. {x | x a. f a = x \ a \ Field r}" {fix X assume "X \ Bpow r A - {{}}" hence XA: "X \ A" and "|X| \o r" and X: "X \ {}" unfolding Bpow_def by auto hence "|X| \o |Field r|" by (metis Field_card_of card_of_mono2) then obtain F where 1: "X = F ` (Field r)" using card_of_ordLeq2[OF X] by metis - def f \ "\ i. if i \ Field r then Some (F i) else None" + def f \ "\ i. if i \ Field r then F i else undefined" have "\ f \ Func (Field r) A. X = ?F f" apply (intro bexI[of _ f]) using 1 XA unfolding Func_def f_def by auto } @@ -1075,7 +1159,7 @@ lemma Func_emp2[simp]: "A \ {} \ Func A {} = {}" by auto lemma empty_in_Func[simp]: -"B \ {} \ empty \ Func {} B" +"B \ {} \ (\x. undefined) \ Func {} B" unfolding Func_def by auto lemma Func_mono[simp]: diff -r 0c4b140cff00 -r d2ad6eae514f src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy --- a/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy Fri Jul 05 18:10:07 2013 +0200 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy Sun Jul 07 10:24:00 2013 +0200 @@ -2206,20 +2206,19 @@ (* function space *) definition Func where -"Func A B \ - {f. (\ a. f a \ None \ a \ A) \ (\ a \ A. case f a of Some b \ b \ B |None \ True)}" +"Func A B = {f . (\ a \ A. f a \ B) \ (\ a. a \ A \ f a = undefined)}" lemma Func_empty: -"Func {} B = {empty}" +"Func {} B = {\x. undefined}" unfolding Func_def by auto lemma Func_elim: assumes "g \ Func A B" and "a \ A" -shows "\ b. b \ B \ g a = Some b" -using assms unfolding Func_def by (cases "g a") force+ +shows "\ b. b \ B \ g a = b" +using assms unfolding Func_def by (cases "g a = undefined") auto definition curr where -"curr A f \ \ a. if a \ A then Some (\ b. f (a,b)) else None" +"curr A f \ \ a. if a \ A then \b. f (a,b) else undefined" lemma curr_in: assumes f: "f \ Func (A <*> B) C" @@ -2236,14 +2235,11 @@ fix a b show "f1 (a, b) = f2 (a, b)" proof (cases "(a,b) \ A <*> B") case False - thus ?thesis using assms unfolding Func_def - apply(cases "f1 (a,b)") apply(cases "f2 (a,b)", simp, blast) - apply(cases "f2 (a,b)") by auto + thus ?thesis using assms unfolding Func_def by auto next case True hence a: "a \ A" and b: "b \ B" by auto thus ?thesis - using c unfolding curr_def fun_eq_iff - apply(elim allE[of _ a]) apply simp unfolding fun_eq_iff by auto + using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp qed qed qed @@ -2252,45 +2248,22 @@ assumes "g \ Func A (Func B C)" shows "\ f \ Func (A <*> B) C. curr A f = g" proof - let ?f = "\ ab. case g (fst ab) of None \ None | Some g1 \ g1 (snd ab)" + let ?f = "\ ab. if fst ab \ A \ snd ab \ B then g (fst ab) (snd ab) else undefined" show "curr A ?f = g" proof (rule ext) fix a show "curr A ?f a = g a" proof (cases "a \ A") case False - hence "g a = None" using assms unfolding Func_def by auto + hence "g a = undefined" using assms unfolding Func_def by auto thus ?thesis unfolding curr_def using False by simp next case True - obtain g1 where "g1 \ Func B C" and "g a = Some g1" + obtain g1 where "g1 \ Func B C" and "g a = g1" using assms using Func_elim[OF assms True] by blast - thus ?thesis using True unfolding curr_def by auto + thus ?thesis using True unfolding Func_def curr_def by auto qed qed - show "?f \ Func (A <*> B) C" - unfolding Func_def mem_Collect_eq proof(intro conjI allI ballI) - fix ab show "?f ab \ None \ ab \ A \ B" - proof(cases "g (fst ab)") - case None - hence "fst ab \ A" using assms unfolding Func_def by force - thus ?thesis using None by auto - next - case (Some g1) - hence fst: "fst ab \ A" and g1: "g1 \ Func B C" - using assms unfolding Func_def[of A] by force+ - hence "?f ab \ None \ g1 (snd ab) \ None" using Some by auto - also have "... \ snd ab \ B" using g1 unfolding Func_def by auto - also have "... \ ab \ A \ B" using fst by (cases ab, auto) - finally show ?thesis . - qed - next - fix ab assume ab: "ab \ A \ B" - hence "fst ab \ A" and "snd ab \ B" by(cases ab, auto) - then obtain g1 where "g1 \ Func B C" and "g (fst ab) = Some g1" - using assms using Func_elim[OF assms] by blast - thus "case ?f ab of Some c \ c \ C |None \ True" - unfolding Func_def by auto - qed + show "?f \ Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto qed lemma bij_betw_curr: @@ -2304,42 +2277,19 @@ using bij_betw_curr by blast definition Func_map where -"Func_map B2 f1 f2 g b2 \ - if b2 \ B2 then case g (f2 b2) of None \ None | Some a1 \ Some (f1 a1) - else None" +"Func_map B2 f1 f2 g b2 \ if b2 \ B2 then f1 (g (f2 b2)) else undefined" lemma Func_map: assumes g: "g \ Func A2 A1" and f1: "f1 ` A1 \ B1" and f2: "f2 ` B2 \ A2" shows "Func_map B2 f1 f2 g \ Func B2 B1" -unfolding Func_def mem_Collect_eq proof(intro conjI allI ballI) - fix b2 show "Func_map B2 f1 f2 g b2 \ None \ b2 \ B2" - proof(cases "b2 \ B2") - case True - hence "f2 b2 \ A2" using f2 by auto - then obtain a1 where "g (f2 b2) = Some a1" and "a1 \ A1" - using g unfolding Func_def by(cases "g (f2 b2)", fastforce+) - thus ?thesis unfolding Func_map_def using True by auto - qed(unfold Func_map_def, auto) -next - fix b2 assume b2: "b2 \ B2" - hence "f2 b2 \ A2" using f2 by auto - then obtain a1 where "g (f2 b2) = Some a1" and "a1 \ A1" - using g unfolding Func_def by(cases "g (f2 b2)", fastforce+) - thus "case Func_map B2 f1 f2 g b2 of None \ True | Some b1 \ b1 \ B1" - unfolding Func_map_def using b2 f1 by auto -qed - -lemma Func_map_empty: -"Func_map B2 f1 f2 empty = empty" -unfolding Func_map_def[abs_def] by (rule ext, auto) +using assms unfolding Func_def Func_map_def mem_Collect_eq by auto lemma Func_non_emp: assumes "B \ {}" shows "Func A B \ {}" proof- obtain b where b: "b \ B" using assms by auto - hence "(\ a. if a \ A then Some b else None) \ Func A B" - unfolding Func_def by auto + hence "(\ a. if a \ A then b else undefined) \ Func A B" unfolding Func_def by auto thus ?thesis by blast qed @@ -2355,7 +2305,7 @@ moreover {fix f assume "f \ Func A B" moreover obtain a where "a \ A" using R by blast - ultimately obtain b where "b \ B" unfolding Func_def by(cases "f a", force+) + ultimately obtain b where "b \ B" unfolding Func_def by(cases "f a = undefined", force+) with R have False by auto } thus ?L by blast @@ -2367,100 +2317,66 @@ shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1" proof(cases "B2 = {}") case True - thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_empty) + thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def) next case False note B2 = False show ?thesis -proof safe - fix h assume h: "h \ Func B2 B1" - def j1 \ "inv_into A1 f1" - have "\ a2 \ f2 ` B2. \ b2. b2 \ B2 \ f2 b2 = a2" by blast - then obtain k where k: "\ a2 \ f2 ` B2. k a2 \ B2 \ f2 (k a2) = a2" by metis - {fix b2 assume b2: "b2 \ B2" - hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto - moreover have "k (f2 b2) \ B2" using b2 A2(2) k by auto - ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast - } note kk = this - obtain b22 where b22: "b22 \ B2" using B2 by auto - def j2 \ "\ a2. if a2 \ f2 ` B2 then k a2 else b22" - have j2A2: "j2 ` A2 \ B2" unfolding j2_def using k b22 by auto - have j2: "\ b2. b2 \ B2 \ j2 (f2 b2) = b2" - using kk unfolding j2_def by auto - def g \ "Func_map A2 j1 j2 h" - have "Func_map B2 f1 f2 g = h" - proof (rule ext) - fix b2 show "Func_map B2 f1 f2 g b2 = h b2" - proof(cases "b2 \ B2") - case True - show ?thesis - proof (cases "h b2") - case (Some b1) - hence b1: "b1 \ f1 ` A1" using True h unfolding B1 Func_def by auto + proof safe + fix h assume h: "h \ Func B2 B1" + def j1 \ "inv_into A1 f1" + have "\ a2 \ f2 ` B2. \ b2. b2 \ B2 \ f2 b2 = a2" by blast + then obtain k where k: "\ a2 \ f2 ` B2. k a2 \ B2 \ f2 (k a2) = a2" by metis + {fix b2 assume b2: "b2 \ B2" + hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto + moreover have "k (f2 b2) \ B2" using b2 A2(2) k by auto + ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast + } note kk = this + obtain b22 where b22: "b22 \ B2" using B2 by auto + def j2 \ "\ a2. if a2 \ f2 ` B2 then k a2 else b22" + have j2A2: "j2 ` A2 \ B2" unfolding j2_def using k b22 by auto + have j2: "\ b2. b2 \ B2 \ j2 (f2 b2) = b2" + using kk unfolding j2_def by auto + def g \ "Func_map A2 j1 j2 h" + have "Func_map B2 f1 f2 g = h" + proof (rule ext) + fix b2 show "Func_map B2 f1 f2 g b2 = h b2" + proof(cases "b2 \ B2") + case True show ?thesis - using Some True A2 f_inv_into_f[OF b1] - unfolding g_def Func_map_def j1_def j2[OF True] by auto - qed(insert A2 True j2[OF True], unfold g_def Func_map_def, auto) - qed(insert h, unfold Func_def Func_map_def, auto) - qed - moreover have "g \ Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) - using inv_into_into j2A2 B1 A2 inv_into_into - unfolding j1_def image_def by fast+ - ultimately show "h \ Func_map B2 f1 f2 ` Func A2 A1" - unfolding Func_map_def[abs_def] unfolding image_def by auto -qed(insert B1 Func_map[OF _ _ A2(2)], auto) -qed - -(* partial-function space: *) -definition Pfunc where -"Pfunc A B \ - {f. (\a. f a \ None \ a \ A) \ - (\a. case f a of None \ True | Some b \ b \ B)}" - -lemma Func_Pfunc: -"Func A B \ Pfunc A B" -unfolding Func_def Pfunc_def by auto - -lemma Pfunc_Func: -"Pfunc A B = (\ A' \ Pow A. Func A' B)" -proof safe - fix f assume f: "f \ Pfunc A B" - show "f \ (\A'\Pow A. Func A' B)" - proof (intro UN_I) - let ?A' = "{a. f a \ None}" - show "?A' \ Pow A" using f unfolding Pow_def Pfunc_def by auto - show "f \ Func ?A' B" using f unfolding Func_def Pfunc_def by auto - qed -next - fix f A' assume "f \ Func A' B" and "A' \ A" - thus "f \ Pfunc A B" unfolding Func_def Pfunc_def by auto + proof (cases "h b2 = undefined") + case True + hence b1: "h b2 \ f1 ` A1" using h `b2 \ B2` unfolding B1 Func_def by auto + show ?thesis using A2 f_inv_into_f[OF b1] + unfolding True g_def Func_map_def j1_def j2[OF `b2 \ B2`] by auto + qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def, + auto intro: f_inv_into_f) + qed(insert h, unfold Func_def Func_map_def, auto) + qed + moreover have "g \ Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) + using inv_into_into j2A2 B1 A2 inv_into_into + unfolding j1_def image_def by fast+ + ultimately show "h \ Func_map B2 f1 f2 ` Func A2 A1" + unfolding Func_map_def[abs_def] unfolding image_def by auto + qed(insert B1 Func_map[OF _ _ A2(2)], auto) qed lemma card_of_Pow_Func: "|Pow A| =o |Func A (UNIV::bool set)|" proof- - def F \ "\ A' a. if a \ A then (if a \ A' then Some True else Some False) - else None" + def F \ "\ A' a. if a \ A then (if a \ A' then True else False) + else undefined" have "bij_betw F (Pow A) (Func A (UNIV::bool set))" unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI) - fix A1 A2 assume A1: "A1 \ Pow A" and A2: "A2 \ Pow A" and eq: "F A1 = F A2" - show "A1 = A2" - proof- - {fix a - have "a \ A1 \ F A1 a = Some True" using A1 unfolding F_def Pow_def by auto - also have "... \ F A2 a = Some True" unfolding eq .. - also have "... \ a \ A2" using A2 unfolding F_def Pow_def by auto - finally have "a \ A1 \ a \ A2" . - } - thus ?thesis by auto - qed + fix A1 A2 assume "A1 \ Pow A" "A2 \ Pow A" "F A1 = F A2" + thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm) next show "F ` Pow A = Func A UNIV" proof safe fix f assume f: "f \ Func A (UNIV::bool set)" show "f \ F ` Pow A" unfolding image_def mem_Collect_eq proof(intro bexI) - let ?A1 = "{a \ A. f a = Some True}" + let ?A1 = "{a \ A. f a = True}" show "f = F ?A1" unfolding F_def apply(rule ext) - using f unfolding Func_def mem_Collect_eq by (auto,force) + using f unfolding Func_def mem_Collect_eq by auto qed auto qed(unfold Func_def mem_Collect_eq F_def, auto) qed @@ -2473,8 +2389,8 @@ shows "|Func A1 B| \o |Func A2 B|" proof- obtain bb where bb: "bb \ B" using B by auto - def F \ "\ (f1::'a \ 'b option) a. if a \ A2 then (if a \ A1 then f1 a else Some bb) - else None" + def F \ "\ (f1::'a \ 'b) a. if a \ A2 then (if a \ A1 then f1 a else bb) + else undefined" show ?thesis unfolding card_of_ordLeq[symmetric] proof(intro exI[of _ F] conjI) show "inj_on F (Func A1 B)" unfolding inj_on_def proof safe fix f g assume f: "f \ Func A1 B" and g: "g \ Func A1 B" and eq: "F f = F g" @@ -2491,27 +2407,13 @@ qed(insert bb, unfold Func_def F_def, force) qed -lemma card_of_Pfunc_Pow_Func: -assumes "B \ {}" -shows "|Pfunc A B| \o |Pow A <*> Func A B|" -proof- - have "|Pfunc A B| =o |\ A' \ Pow A. Func A' B|" (is "_ =o ?K") - unfolding Pfunc_Func by(rule card_of_refl) - also have "?K \o |Sigma (Pow A) (\ A'. Func A' B)|" using card_of_UNION_Sigma . - also have "|Sigma (Pow A) (\ A'. Func A' B)| \o |Pow A <*> Func A B|" - apply(rule card_of_Sigma_mono1) using card_of_Func_mono[OF _ assms] by auto - finally show ?thesis . -qed - lemma ordLeq_Func: assumes "{b1,b2} \ B" "b1 \ b2" shows "|A| \o |Func A B|" unfolding card_of_ordLeq[symmetric] proof(intro exI conjI) - let ?F = "\ aa a. if a \ A then (if a = aa then Some b1 else Some b2) - else None" + let ?F = "\ aa a. if a \ A then (if a = aa then b1 else b2) else undefined" show "inj_on ?F A" using assms unfolding inj_on_def fun_eq_iff by auto - show "?F ` A \ Func A B" using assms unfolding Func_def apply auto - by (metis option.simps(3)) + show "?F ` A \ Func A B" using assms unfolding Func_def by auto qed lemma infinite_Func: @@ -2519,58 +2421,17 @@ shows "infinite (Func A B)" using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite) -(* alternative function space avoiding the option type, with undefined instead of None *) -definition Ffunc where -"Ffunc A B = {f . (\ a \ A. f a \ B) \ (\ a. a \ A \ f a = undefined)}" - -lemma card_of_Func_Ffunc: -"|Ffunc A B| =o |Func A B|" -unfolding card_of_ordIso[symmetric] proof - let ?F = "\ f a. if a \ A then Some (f a) else None" - show "bij_betw ?F (Ffunc A B) (Func A B)" - unfolding bij_betw_def unfolding inj_on_def proof(intro conjI ballI impI) - fix f g assume f: "f \ Ffunc A B" and g: "g \ Ffunc A B" and eq: "?F f = ?F g" - show "f = g" - proof(rule ext) - fix a - show "f a = g a" - proof(cases "a \ A") - case True - have "Some (f a) = ?F f a" using True by auto - also have "... = ?F g a" using eq unfolding fun_eq_iff by(rule allE) - also have "... = Some (g a)" using True by auto - finally have "Some (f a) = Some (g a)" . - thus ?thesis by simp - qed(insert f g, unfold Ffunc_def, auto) - qed - next - show "?F ` Ffunc A B = Func A B" - proof safe - fix f assume f: "f \ Func A B" - def g \ "\ a. case f a of Some b \ b | None \ undefined" - have "g \ Ffunc A B" - using f unfolding g_def Func_def Ffunc_def by force+ - moreover have "f = ?F g" - proof(rule ext) - fix a show "f a = ?F g a" - using f unfolding Func_def g_def by (cases "a \ A") force+ - qed - ultimately show "f \ ?F ` (Ffunc A B)" by blast - qed(unfold Ffunc_def Func_def, auto) - qed -qed - lemma card_of_Func_UNIV: "|Func (UNIV::'a set) (B::'b set)| =o |{f::'a \ 'b. range f \ B}|" apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI) - let ?F = "\ f (a::'a). Some ((f a)::'b)" + let ?F = "\ f (a::'a). ((f a)::'b)" show "bij_betw ?F {f. range f \ B} (Func UNIV B)" unfolding bij_betw_def inj_on_def proof safe - fix h :: "'a \ 'b option" assume h: "h \ Func UNIV B" - hence "\ a. \ b. h a = Some b" unfolding Func_def by auto - then obtain f where f: "\ a. h a = Some (f a)" by metis + fix h :: "'a \ 'b" assume h: "h \ Func UNIV B" + hence "\ a. \ b. h a = b" unfolding Func_def by auto + then obtain f where f: "\ a. h a = f a" by metis hence "range f \ B" using h unfolding Func_def by auto - thus "h \ (\f a. Some (f a)) ` {f. range f \ B}" using f unfolding image_def by auto + thus "h \ (\f a. f a) ` {f. range f \ B}" using f unfolding image_def by auto qed(unfold Func_def fun_eq_iff, auto) qed