(* Title: ZF/AC/AC_Equiv.ML
ID: $Id$
Author: Krzysztof Grabczewski
*)
val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def];
val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def,
AC6_def, AC7_def, AC8_def, AC9_def, AC10_def, AC11_def,
AC12_def, AC13_def, AC14_def, AC15_def, AC16_def,
AC17_def, AC18_def, AC19_def];
val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def];
(* ********************************************************************** *)
(* lemmas concerning FOL and pure ZF theory *)
(* ********************************************************************** *)
(* used only in WO1_DC.ML *)
(*Note simpler proof*)
Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A";
by (asm_simp_tac (simpset() addsimps [image_fun]) 1);
qed "images_eq";
(* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *)
(*I don't know where to put this one.*)
goal Cardinal.thy
"!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m";
by (rtac not_emptyE 1 THEN (assume_tac 1));
by (ftac singleton_subsetI 1);
by (ftac subsetD 1 THEN (assume_tac 1));
by (res_inst_tac [("A2","A")]
(Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1
THEN (REPEAT (assume_tac 2)));
by (Fast_tac 1);
qed "Diff_lepoll";
(* ********************************************************************** *)
(* lemmas concerning lepoll and eqpoll relations *)
(* ********************************************************************** *)
(* ********************************************************************** *)
(* Theorems concerning ordinals *)
(* ********************************************************************** *)
(* lemma for ordertype_Int *)
goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A";
by (rtac equalityI 1);
by Safe_tac;
by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1
THEN (assume_tac 1));
by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1
THEN (REPEAT (assume_tac 1)));
by (fast_tac (claset() addIs [id_conv RS ssubst]) 1);
qed "rvimage_id";
(* used only in Hartog.ML *)
goal Cardinal.thy
"!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)";
by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")]
(rvimage_id RS subst) 1);
by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1);
qed "ordertype_Int";
(* used only in AC16_lemmas.ML *)
goalw CardinalArith.thy [InfCard_def]
"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
qed "Inf_Card_is_InfCard";
Goal "(THE z. {x}={z}) = x";
by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
qed "the_element";
Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})";
by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1);
by (TRYALL (eresolve_tac [RepFunI, RepFunE]));
by (REPEAT (asm_full_simp_tac (simpset() addsimps [the_element]) 1));
qed "lam_sing_bij";
val [major, minor] = Goalw [inj_def]
"[| f:inj(A, B); !!a. a:A ==> f`a : C |] ==> f:inj(A,C)";
by (fast_tac (claset() addSEs [minor]
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
qed "inj_strengthen_type";
Goalw [Finite_def] "~Finite(nat)";
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll]
addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1);
qed "nat_not_Finite";
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll;
(* ********************************************************************** *)
(* Another elimination rule for EX! *)
(* ********************************************************************** *)
Goal "[| EX! x. P(x); P(x); P(y) |] ==> x=y";
by (etac ex1E 1);
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1);
by (Fast_tac 1);
by (Fast_tac 1);
qed "ex1_two_eq";
(* ********************************************************************** *)
(* image of a surjection *)
(* ********************************************************************** *)
Goalw [surj_def] "f : surj(A, B) ==> f``A = B";
by (etac CollectE 1);
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1
THEN (assume_tac 1));
by (fast_tac (claset() addSEs [apply_type] addIs [equalityI]) 1);
qed "surj_image_eq";
Goal "succ(x) lepoll y ==> y ~= 0";
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1);
qed "succ_lepoll_imp_not_empty";
Goal "x eqpoll succ(n) ==> x ~= 0";
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1);
qed "eqpoll_succ_imp_not_empty";