Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
--- 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 \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
proof -
- let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None"
+ let ?f = "\<lambda>f. %x. if f x \<in> B then f x else undefined"
have "inj_on ?f ?LHS" unfolding inj_on_def
proof (unfold fun_eq_iff, safe)
fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
--- 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)
--- 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);
--- 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 =
--- 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 =
--- 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 \<equiv> |Func (Field r2) (Field r1)|"
-definition ccexp (infixr "^^c" 90) where
- "r1 ^^c r2 \<equiv> |Pfunc (Field r2) (Field r1)|"
-
-lemma cexp_ordLeq_ccexp: "r1 ^c r2 \<le>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 \<le>o r1 ^c r2"
proof(cases "Field p1 = {}")
case True
- hence "|Field (p1 ^c p2)| \<le>o cone"
- unfolding czero_def cone_def cexp_def Field_card_of
+ hence "|Field |Func (Field p2) (Field p1)|| \<le>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 \<le>o cone" by (simp add: Field_card_of cexp_def)
+ hence "|Func (Field p2) (Field p1)| \<le>o cone" by (simp add: Field_card_of cexp_def)
+ hence "p1 ^c p2 \<le>o cone" unfolding cexp_def .
thus ?thesis
proof (cases "Field p2 = {}")
case True
@@ -406,7 +400,7 @@
thus ?thesis using `p1 ^c p2 \<le>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 _ "\<lambda>f. case f () of Some a \<Rightarrow> a"]) auto
+ by (rule exI[of _ "\<lambda>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: "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> cinfinite (q ^c r)"
by (metis assms cinfinite_mono ordLeq_cexp2)
-lemma cinfinite_ccexp: "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> cinfinite (q ^^c r)"
-by (rule cinfinite_mono[OF cexp_ordLeq_ccexp cinfinite_cexp])
-
lemma Cinfinite_cexp:
"\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> Cinfinite (q ^c r)"
by (simp add: cinfinite_cexp Card_order_cexp)
@@ -754,7 +745,7 @@
"r1 *c r2 \<le>o (r1 +c r2) ^c ctwo"
unfolding cprod_def csum_def cexp_def ctwo_def Field_card_of
proof -
- let ?f = "\<lambda>(a, b). %x. if x then Some (Inl a) else Some (Inr b)"
+ let ?f = "\<lambda>(a, b). %x. if x then Inl a else Inr b"
have "inj_on ?f (Field r1 \<times> Field r2)" (is "inj_on _ ?LHS")
by (auto simp: inj_on_def fun_eq_iff split: bool.split)
moreover
--- 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 \<equiv>
+ {f. (\<forall> a. f a \<noteq> None \<longleftrightarrow> a \<in> A) \<and> (\<forall> a \<in> A. case f a of Some b \<Rightarrow> b \<in> B |None \<Rightarrow> 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 = "\<lambda> f a. if a \<in> 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 \<in> Func A B" and g: "g \<in> 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 \<in> 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 \<in> Func_option A B"
+ def g \<equiv> "\<lambda> a. case f a of Some b \<Rightarrow> b | None \<Rightarrow> undefined"
+ have "g \<in> 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 \<in> A") force+
+ qed
+ ultimately show "f \<in> ?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 \<equiv>
+ {f. (\<forall>a. f a \<noteq> None \<longrightarrow> a \<in> A) \<and>
+ (\<forall>a. case f a of None \<Rightarrow> True | Some b \<Rightarrow> b \<in> B)}"
+
+lemma Func_Pfunc:
+"Func_option A B \<subseteq> Pfunc A B"
+unfolding Func_option_def Pfunc_def by auto
+
+lemma Pfunc_Func_option:
+"Pfunc A B = (\<Union> A' \<in> Pow A. Func_option A' B)"
+proof safe
+ fix f assume f: "f \<in> Pfunc A B"
+ show "f \<in> (\<Union>A'\<in>Pow A. Func_option A' B)"
+ proof (intro UN_I)
+ let ?A' = "{a. f a \<noteq> None}"
+ show "?A' \<in> Pow A" using f unfolding Pow_def Pfunc_def by auto
+ show "f \<in> Func_option ?A' B" using f unfolding Func_option_def Pfunc_def by auto
+ qed
+next
+ fix f A' assume "f \<in> Func_option A' B" and "A' \<subseteq> A"
+ thus "f \<in> 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 \<subseteq> A2" and B: "B \<noteq> {}"
+shows "|Func_option A1 B| \<le>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 \<noteq> {}"
+shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
+proof-
+ have "|Pfunc A B| =o |\<Union> A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
+ unfolding Pfunc_Func_option by(rule card_of_refl)
+ also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
+ also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>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 \<noteq> {}" and A: "infinite A"
shows "|Bpow r A| \<le>o |Func (Field r) A|"
proof-
- let ?F = "\<lambda> f. {x | x a. f a = Some x}"
+ let ?F = "\<lambda> f. {x | x a. f a = x \<and> a \<in> Field r}"
{fix X assume "X \<in> Bpow r A - {{}}"
hence XA: "X \<subseteq> A" and "|X| \<le>o r"
and X: "X \<noteq> {}" unfolding Bpow_def by auto
hence "|X| \<le>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 \<equiv> "\<lambda> i. if i \<in> Field r then Some (F i) else None"
+ def f \<equiv> "\<lambda> i. if i \<in> Field r then F i else undefined"
have "\<exists> f \<in> 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 \<noteq> {} \<Longrightarrow> Func A {} = {}" by auto
lemma empty_in_Func[simp]:
-"B \<noteq> {} \<Longrightarrow> empty \<in> Func {} B"
+"B \<noteq> {} \<Longrightarrow> (\<lambda>x. undefined) \<in> Func {} B"
unfolding Func_def by auto
lemma Func_mono[simp]:
--- 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 \<equiv>
- {f. (\<forall> a. f a \<noteq> None \<longleftrightarrow> a \<in> A) \<and> (\<forall> a \<in> A. case f a of Some b \<Rightarrow> b \<in> B |None \<Rightarrow> True)}"
+"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
lemma Func_empty:
-"Func {} B = {empty}"
+"Func {} B = {\<lambda>x. undefined}"
unfolding Func_def by auto
lemma Func_elim:
assumes "g \<in> Func A B" and "a \<in> A"
-shows "\<exists> b. b \<in> B \<and> g a = Some b"
-using assms unfolding Func_def by (cases "g a") force+
+shows "\<exists> b. b \<in> B \<and> g a = b"
+using assms unfolding Func_def by (cases "g a = undefined") auto
definition curr where
-"curr A f \<equiv> \<lambda> a. if a \<in> A then Some (\<lambda> b. f (a,b)) else None"
+"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
lemma curr_in:
assumes f: "f \<in> Func (A <*> B) C"
@@ -2236,14 +2235,11 @@
fix a b show "f1 (a, b) = f2 (a, b)"
proof (cases "(a,b) \<in> 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 \<in> A" and b: "b \<in> 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 \<in> Func A (Func B C)"
shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
proof
- let ?f = "\<lambda> ab. case g (fst ab) of None \<Rightarrow> None | Some g1 \<Rightarrow> g1 (snd ab)"
+ let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> 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 \<in> 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 \<in> Func B C" and "g a = Some g1"
+ obtain g1 where "g1 \<in> 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 \<in> Func (A <*> B) C"
- unfolding Func_def mem_Collect_eq proof(intro conjI allI ballI)
- fix ab show "?f ab \<noteq> None \<longleftrightarrow> ab \<in> A \<times> B"
- proof(cases "g (fst ab)")
- case None
- hence "fst ab \<notin> A" using assms unfolding Func_def by force
- thus ?thesis using None by auto
- next
- case (Some g1)
- hence fst: "fst ab \<in> A" and g1: "g1 \<in> Func B C"
- using assms unfolding Func_def[of A] by force+
- hence "?f ab \<noteq> None \<longleftrightarrow> g1 (snd ab) \<noteq> None" using Some by auto
- also have "... \<longleftrightarrow> snd ab \<in> B" using g1 unfolding Func_def by auto
- also have "... \<longleftrightarrow> ab \<in> A \<times> B" using fst by (cases ab, auto)
- finally show ?thesis .
- qed
- next
- fix ab assume ab: "ab \<in> A \<times> B"
- hence "fst ab \<in> A" and "snd ab \<in> B" by(cases ab, auto)
- then obtain g1 where "g1 \<in> 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 \<Rightarrow> c \<in> C |None \<Rightarrow> True"
- unfolding Func_def by auto
- qed
+ show "?f \<in> 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 \<equiv>
- if b2 \<in> B2 then case g (f2 b2) of None \<Rightarrow> None | Some a1 \<Rightarrow> Some (f1 a1)
- else None"
+"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
lemma Func_map:
assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
-unfolding Func_def mem_Collect_eq proof(intro conjI allI ballI)
- fix b2 show "Func_map B2 f1 f2 g b2 \<noteq> None \<longleftrightarrow> b2 \<in> B2"
- proof(cases "b2 \<in> B2")
- case True
- hence "f2 b2 \<in> A2" using f2 by auto
- then obtain a1 where "g (f2 b2) = Some a1" and "a1 \<in> 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 \<in> B2"
- hence "f2 b2 \<in> A2" using f2 by auto
- then obtain a1 where "g (f2 b2) = Some a1" and "a1 \<in> A1"
- using g unfolding Func_def by(cases "g (f2 b2)", fastforce+)
- thus "case Func_map B2 f1 f2 g b2 of None \<Rightarrow> True | Some b1 \<Rightarrow> b1 \<in> 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 \<noteq> {}"
shows "Func A B \<noteq> {}"
proof-
obtain b where b: "b \<in> B" using assms by auto
- hence "(\<lambda> a. if a \<in> A then Some b else None) \<in> Func A B"
- unfolding Func_def by auto
+ hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
thus ?thesis by blast
qed
@@ -2355,7 +2305,7 @@
moreover
{fix f assume "f \<in> Func A B"
moreover obtain a where "a \<in> A" using R by blast
- ultimately obtain b where "b \<in> B" unfolding Func_def by(cases "f a", force+)
+ ultimately obtain b where "b \<in> 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 \<in> Func B2 B1"
- def j1 \<equiv> "inv_into A1 f1"
- have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
- then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
- {fix b2 assume b2: "b2 \<in> B2"
- hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
- moreover have "k (f2 b2) \<in> 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 \<in> B2" using B2 by auto
- def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
- have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
- have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
- using kk unfolding j2_def by auto
- def g \<equiv> "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 \<in> B2")
- case True
- show ?thesis
- proof (cases "h b2")
- case (Some b1)
- hence b1: "b1 \<in> f1 ` A1" using True h unfolding B1 Func_def by auto
+ proof safe
+ fix h assume h: "h \<in> Func B2 B1"
+ def j1 \<equiv> "inv_into A1 f1"
+ have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
+ then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
+ {fix b2 assume b2: "b2 \<in> B2"
+ hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
+ moreover have "k (f2 b2) \<in> 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 \<in> B2" using B2 by auto
+ def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
+ have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
+ have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
+ using kk unfolding j2_def by auto
+ def g \<equiv> "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 \<in> 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 \<in> 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 \<in> 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 \<equiv>
- {f. (\<forall>a. f a \<noteq> None \<longrightarrow> a \<in> A) \<and>
- (\<forall>a. case f a of None \<Rightarrow> True | Some b \<Rightarrow> b \<in> B)}"
-
-lemma Func_Pfunc:
-"Func A B \<subseteq> Pfunc A B"
-unfolding Func_def Pfunc_def by auto
-
-lemma Pfunc_Func:
-"Pfunc A B = (\<Union> A' \<in> Pow A. Func A' B)"
-proof safe
- fix f assume f: "f \<in> Pfunc A B"
- show "f \<in> (\<Union>A'\<in>Pow A. Func A' B)"
- proof (intro UN_I)
- let ?A' = "{a. f a \<noteq> None}"
- show "?A' \<in> Pow A" using f unfolding Pow_def Pfunc_def by auto
- show "f \<in> Func ?A' B" using f unfolding Func_def Pfunc_def by auto
- qed
-next
- fix f A' assume "f \<in> Func A' B" and "A' \<subseteq> A"
- thus "f \<in> Pfunc A B" unfolding Func_def Pfunc_def by auto
+ proof (cases "h b2 = undefined")
+ case True
+ hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then Some True else Some False)
- else None"
+ def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> 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 \<in> Pow A" and A2: "A2 \<in> Pow A" and eq: "F A1 = F A2"
- show "A1 = A2"
- proof-
- {fix a
- have "a \<in> A1 \<longleftrightarrow> F A1 a = Some True" using A1 unfolding F_def Pow_def by auto
- also have "... \<longleftrightarrow> F A2 a = Some True" unfolding eq ..
- also have "... \<longleftrightarrow> a \<in> A2" using A2 unfolding F_def Pow_def by auto
- finally have "a \<in> A1 \<longleftrightarrow> a \<in> A2" .
- }
- thus ?thesis by auto
- qed
+ fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> 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 \<in> Func A (UNIV::bool set)"
show "f \<in> F ` Pow A" unfolding image_def mem_Collect_eq proof(intro bexI)
- let ?A1 = "{a \<in> A. f a = Some True}"
+ let ?A1 = "{a \<in> 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| \<le>o |Func A2 B|"
proof-
obtain bb where bb: "bb \<in> B" using B by auto
- def F \<equiv> "\<lambda> (f1::'a \<Rightarrow> 'b option) a. if a \<in> A2 then (if a \<in> A1 then f1 a else Some bb)
- else None"
+ def F \<equiv> "\<lambda> (f1::'a \<Rightarrow> 'b) a. if a \<in> A2 then (if a \<in> 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 \<in> Func A1 B" and g: "g \<in> 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 \<noteq> {}"
-shows "|Pfunc A B| \<le>o |Pow A <*> Func A B|"
-proof-
- have "|Pfunc A B| =o |\<Union> A' \<in> Pow A. Func A' B|" (is "_ =o ?K")
- unfolding Pfunc_Func by(rule card_of_refl)
- also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func A' B)|" using card_of_UNION_Sigma .
- also have "|Sigma (Pow A) (\<lambda> A'. Func A' B)| \<le>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} \<subseteq> B" "b1 \<noteq> b2"
shows "|A| \<le>o |Func A B|"
unfolding card_of_ordLeq[symmetric] proof(intro exI conjI)
- let ?F = "\<lambda> aa a. if a \<in> A then (if a = aa then Some b1 else Some b2)
- else None"
+ let ?F = "\<lambda> aa a. if a \<in> 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 \<subseteq> Func A B" using assms unfolding Func_def apply auto
- by (metis option.simps(3))
+ show "?F ` A \<subseteq> 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 . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
-
-lemma card_of_Func_Ffunc:
-"|Ffunc A B| =o |Func A B|"
-unfolding card_of_ordIso[symmetric] proof
- let ?F = "\<lambda> f a. if a \<in> 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 \<in> Ffunc A B" and g: "g \<in> 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 \<in> 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 \<in> Func A B"
- def g \<equiv> "\<lambda> a. case f a of Some b \<Rightarrow> b | None \<Rightarrow> undefined"
- have "g \<in> 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 \<in> A") force+
- qed
- ultimately show "f \<in> ?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 \<Rightarrow> 'b. range f \<subseteq> B}|"
apply(rule ordIso_symmetric) proof(intro card_of_ordIsoI)
- let ?F = "\<lambda> f (a::'a). Some ((f a)::'b)"
+ let ?F = "\<lambda> f (a::'a). ((f a)::'b)"
show "bij_betw ?F {f. range f \<subseteq> B} (Func UNIV B)"
unfolding bij_betw_def inj_on_def proof safe
- fix h :: "'a \<Rightarrow> 'b option" assume h: "h \<in> Func UNIV B"
- hence "\<forall> a. \<exists> b. h a = Some b" unfolding Func_def by auto
- then obtain f where f: "\<forall> a. h a = Some (f a)" by metis
+ fix h :: "'a \<Rightarrow> 'b" assume h: "h \<in> Func UNIV B"
+ hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
+ then obtain f where f: "\<forall> a. h a = f a" by metis
hence "range f \<subseteq> B" using h unfolding Func_def by auto
- thus "h \<in> (\<lambda>f a. Some (f a)) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
+ thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
qed(unfold Func_def fun_eq_iff, auto)
qed