--- a/src/ZF/AC/AC18_AC19.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/AC/AC18_AC19.ML Thu Aug 24 11:05:20 2000 +0200
@@ -5,19 +5,15 @@
The proof of AC1 ==> AC18 ==> AC19 ==> AC1
*)
-open AC18_AC19;
-
(* ********************************************************************** *)
(* AC1 ==> AC18 *)
(* ********************************************************************** *)
-Goal "[| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |] \
-\ ==> (lam a:A. f`P(a)):(PROD a:A. Q(a))";
+Goal "[| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |] \
+\ ==> (lam a:A. f`P(a)) : (PROD a:A. Q(a))";
by (rtac lam_type 1);
by (dtac apply_type 1);
-by (rtac RepFunI 1 THEN (assume_tac 1));
-by (dtac bspec 1 THEN (assume_tac 1));
-by (etac subsetD 1 THEN (assume_tac 1));
+by Auto_tac;
qed "PROD_subsets";
Goal "[| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \
@@ -104,9 +100,9 @@
val lemma3 = result();
Goalw AC_defs "AC19 ==> AC1";
-by (REPEAT (resolve_tac [allI,impI] 1));
-by (excluded_middle_tac "A=0" 1);
-by (fast_tac (claset() addSIs [exI, empty_fun]) 2);
+by (Clarify_tac 1);
+by (case_tac "A=0" 1);
+by (Force_tac 1);
by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1);
by (etac impE 1);
by (etac RepRep_conj 1 THEN (assume_tac 1));
--- a/src/ZF/AC/AC7_AC9.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/AC/AC7_AC9.ML Thu Aug 24 11:05:20 2000 +0200
@@ -9,36 +9,14 @@
(* ********************************************************************** *)
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *)
(* - Sigma_fun_space_not0 *)
-(* - all_eqpoll_imp_pair_eqpoll *)
(* - Sigma_fun_space_eqpoll *)
(* ********************************************************************** *)
-Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
+Goal "[| 0~:A; B:A |] ==> (nat->Union(A)) * B ~= 0";
by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1,
- Union_empty_iff RS iffD1]
- addDs [fun_space_emptyD]) 1);
+ Union_empty_iff RS iffD1]) 1);
qed "Sigma_fun_space_not0";
-Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
-by (REPEAT (rtac ballI 1));
-by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
- THEN REPEAT (assume_tac 1));
-qed "all_eqpoll_imp_pair_eqpoll";
-
-Goal "[| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A |] \
-\ ==> P(b)=R(b)";
-by Auto_tac;
-qed "if_eqE1";
-
-Goal "ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \
-\ ==> ALL a:A. a~=b --> Q(a)=S(a)";
-by Auto_tac;
-qed "if_eqE2";
-
-Goal "[| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
-by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1);
-qed "lam_eqE";
-
Goalw [inj_def]
"C:A ==> (lam g:(nat->Union(A))*C. \
\ (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \
@@ -101,13 +79,13 @@
Goalw AC_defs "AC7 ==> AC6";
by (rtac allI 1);
by (rtac impI 1);
-by (excluded_middle_tac "A=0" 1);
-by (fast_tac (claset() addSIs [not_emptyI, empty_fun]) 2);
+by (case_tac "A=0" 1);
+by (Asm_simp_tac 1);
by (rtac lemma1 1);
by (etac allE 1);
by (etac impE 1 THEN (assume_tac 2));
-by (fast_tac (claset() addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
- Sigma_fun_space_eqpoll]) 1);
+by (blast_tac (claset() addSIs [lemma2]
+ addIs [eqpoll_sym, eqpoll_trans, Sigma_fun_space_eqpoll]) 1);
qed "AC7_AC6";
@@ -171,17 +149,16 @@
((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
-Goal "[| 0~:A; A~=0 |] \
-\ ==> ALL B1: ({((nat->Union(A))*B)*nat. B:A} \
-\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \
-\ ALL B2: ({((nat->Union(A))*B)*nat. B:A} \
-\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \
-\ B1 eqpoll B2";
-by (fast_tac (claset() addSIs [all_eqpoll_imp_pair_eqpoll, ballI,
- nat_cons_eqpoll RS eqpoll_trans]
- addEs [Sigma_fun_space_not0 RS not_emptyE]
- addIs [snd_lepoll_SigmaI, eqpoll_refl RSN
- (2, prod_eqpoll_cong), Sigma_fun_space_eqpoll]) 1);
+Goal "[| 0~:A; A~=0; \
+\ C = {((nat->Union(A))*B)*nat. B:A} Un \
+\ {cons(0,((nat->Union(A))*B)*nat). B:A}; \
+\ B1: C; B2: C |] \
+\ ==> B1 eqpoll B2";
+by (blast_tac (claset() addSIs [nat_cons_eqpoll RS eqpoll_trans]
+ addDs [Sigma_fun_space_not0]
+ addIs [eqpoll_trans, eqpoll_sym, snd_lepoll_SigmaI,
+ eqpoll_refl RSN (2, prod_eqpoll_cong),
+ Sigma_fun_space_eqpoll]) 1);
val lemma1 = result();
Goal "ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}. \
@@ -200,9 +177,7 @@
by (rtac allI 1);
by (rtac impI 1);
by (etac allE 1);
-by (excluded_middle_tac "A=0" 1);
-by (etac impE 1);
-by (rtac lemma1 1 THEN (REPEAT (assume_tac 1)));
-by (fast_tac (claset() addSEs [lemma2]) 1);
-by (fast_tac (claset() addSIs [empty_fun]) 1);
+by (case_tac "A=0" 1);
+by (blast_tac (claset() addDs [lemma1,lemma2]) 2);
+by Auto_tac;
qed "AC9_AC1";
--- a/src/ZF/AC/AC_Equiv.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Thu Aug 24 11:05:20 2000 +0200
@@ -18,10 +18,6 @@
(* lemmas concerning FOL and pure ZF theory *)
(* ********************************************************************** *)
-Goal "(A->X)=0 ==> X=0";
-by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
-qed "fun_space_emptyD";
-
(* 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";
@@ -84,14 +80,8 @@
by (REPEAT (asm_full_simp_tac (simpset() addsimps [the_element]) 1));
qed "lam_sing_bij";
-val [major,minor] = goal thy
- "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)";
-by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD,
- major RS apply_type]) 1);
-qed "Pi_weaken_type";
-
-val [major, minor] = goalw thy [inj_def]
- "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)";
+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";
--- a/src/ZF/AC/DC.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/AC/DC.ML Thu Aug 24 11:05:20 2000 +0200
@@ -49,11 +49,12 @@
by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1);
by (rtac CollectI 1);
by (rtac SigmaI 1);
-by (fast_tac (claset() addSIs [nat_0I RS UN_I, empty_fun]) 1);
+by (rtac (nat_0I RS UN_I) 1);
+by (asm_simp_tac (simpset() addsimps [nat_0I RS UN_I]) 1);
by (rtac (nat_1I RS UN_I) 1);
-by (asm_full_simp_tac (simpset() addsimps [singleton_0]) 2);
+by (asm_simp_tac (simpset() addsimps [singleton_0]) 2);
by (force_tac (claset() addSIs [singleton_fun RS Pi_type],
- simpset() addsimps [singleton_0 RS sym]) 1);
+ simpset() addsimps [singleton_0 RS sym]) 1);
qed "lemma1_2";
Goalw [RR_def, XX_def] "range(RR) <= domain(RR)";
--- a/src/ZF/Arith.thy Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Arith.thy Thu Aug 24 11:05:20 2000 +0200
@@ -56,7 +56,7 @@
mod :: [i,i]=>i (infixl "mod" 70)
"m mod n == raw_mod (natify(m), natify(n))"
-syntax (symbols)
+syntax (xsymbols)
"mult" :: [i, i] => i (infixr "#\\<times>" 70)
end
--- a/src/ZF/Cardinal.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Cardinal.ML Thu Aug 24 11:05:20 2000 +0200
@@ -469,12 +469,11 @@
qed "succ_lepoll_succD";
Goal "m:nat ==> ALL n: nat. m lepoll n --> m le n";
-by (nat_ind_tac "m" [] 1);
+by (nat_ind_tac "m" [] 1); (*induct_tac isn't available yet*)
by (blast_tac (claset() addSIs [nat_0_le]) 1);
by (rtac ballI 1);
by (eres_inst_tac [("n","n")] natE 1);
-by (asm_simp_tac (simpset() addsimps [lepoll_def, inj_def,
- succI1 RS Pi_empty2]) 1);
+by (asm_simp_tac (simpset() addsimps [lepoll_def, inj_def]) 1);
by (blast_tac (claset() addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
qed_spec_mp "nat_lepoll_imp_le";
--- a/src/ZF/Cardinal.thy Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Cardinal.thy Thu Aug 24 11:05:20 2000 +0200
@@ -31,4 +31,9 @@
Card_def "Card(i) == (i = |i|)"
+syntax (xsymbols)
+ "op eqpoll" :: [i,i] => o (infixl "\\<approx>" 50)
+ "op lepoll" :: [i,i] => o (infixl "\\<lesssim>" 50)
+ "op lesspoll" :: [i,i] => o (infixl "\\<prec>" 50)
+
end
--- a/src/ZF/CardinalArith.thy Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/CardinalArith.thy Thu Aug 24 11:05:20 2000 +0200
@@ -39,7 +39,8 @@
(*needed because jump_cardinal(K) might not be the successor of K*)
csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
-syntax (symbols)
- "op |*|" :: [i,i] => i (infixr "|\\<times>|" 70)
+syntax (xsymbols)
+ "op |+|" :: [i,i] => i (infixl "\\<oplus>" 65)
+ "op |*|" :: [i,i] => i (infixl "\\<otimes>" 70)
end
--- a/src/ZF/Coind/Map.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Coind/Map.ML Thu Aug 24 11:05:20 2000 +0200
@@ -4,8 +4,6 @@
Copyright 1995 University of Cambridge
*)
-open Map;
-
(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
Goalw [TMap_def] "{0,1} <= {1} Un TMap(I, {0,1})";
@@ -20,7 +18,7 @@
by (Blast_tac 1);
result();
-(*TOO SLOW
+(*
Goalw [TMap_def]
"{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) <= \
\ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
@@ -81,7 +79,7 @@
(* ############################################################ *)
Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "map_mono";
(* Rename to pmap_mono *)
--- a/src/ZF/Order.thy Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Order.thy Thu Aug 24 11:05:20 2000 +0200
@@ -35,12 +35,15 @@
ord_iso_map_def
"ord_iso_map(A,r,B,s) ==
- UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).
- {<x,y>}"
+ UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
constdefs
first :: [i, i, i] => o
"first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
+syntax (xsymbols)
+ ord_iso :: [i,i,i,i]=>i ("('(_,_') \\<cong> '(_,_'))" 50)
+
+
end
--- a/src/ZF/OrderType.thy Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/OrderType.thy Thu Aug 24 11:05:20 2000 +0200
@@ -38,7 +38,7 @@
(*ordinal subtraction*)
odiff_def "i -- j == ordertype(i-j, Memrel(i))"
-syntax (symbols)
- "op **" :: [i,i] => i (infixr "\\<times>\\<times>" 70)
+syntax (xsymbols)
+ "op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
end
--- a/src/ZF/ZF.thy Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/ZF.thy Thu Aug 24 11:05:20 2000 +0200
@@ -157,6 +157,7 @@
"@UNION" :: [pttrn, i, i] => i ("(3\\<Union> _\\<in>_./ _)" 10)
"@PROD" :: [pttrn, i, i] => i ("(3\\<Pi> _\\<in>_./ _)" 10)
"@SUM" :: [pttrn, i, i] => i ("(3\\<Sigma> _\\<in>_./ _)" 10)
+ "@lam" :: [pttrn, i, i] => i ("(3\\<lambda> _:_./ _)" 10)
"@Ball" :: [pttrn, i, o] => o ("(3\\<forall> _\\<in>_./ _)" 10)
"@Bex" :: [pttrn, i, o] => o ("(3\\<exists> _\\<in>_./ _)" 10)
(*
--- a/src/ZF/func.ML Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/func.ML Thu Aug 24 11:05:20 2000 +0200
@@ -47,27 +47,6 @@
by (Best_tac 1);
qed "fun_weaken_type";
-(*Empty function spaces*)
-Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
-by (Blast_tac 1);
-qed "Pi_empty1";
-
-Goalw [Pi_def] "a:A ==> A->0 = 0";
-by (Blast_tac 1);
-qed "Pi_empty2";
-
-(*The empty function*)
-Goalw [Pi_def, function_def] "0: Pi(0,B)";
-by (Blast_tac 1);
-qed "empty_fun";
-
-(*The singleton function*)
-Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
-by (Blast_tac 1);
-qed "singleton_fun";
-
-Addsimps [Pi_empty1, singleton_fun];
-
(*** Function Application ***)
Goalw [Pi_def, function_def] "[| <a,b>: f; <a,c>: f; f: Pi(A,B) |] ==> b=c";
@@ -130,6 +109,12 @@
by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1);
qed "Pi_Collect_iff";
+val [major,minor] = Goal
+ "[| f : Pi(A,B); !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)";
+by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD,
+ major RS apply_type]) 1);
+qed "Pi_weaken_type";
+
(** Elimination of membership in a function **)
@@ -204,6 +189,34 @@
by (etac (major RS theI) 1);
qed "lam_theI";
+Goal "[| (lam x:A. f(x)) = (lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
+by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1);
+qed "lam_eqE";
+
+
+(*Empty function spaces*)
+Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
+by (Blast_tac 1);
+qed "Pi_empty1";
+Addsimps [Pi_empty1];
+
+(*The singleton function*)
+Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
+by (Blast_tac 1);
+qed "singleton_fun";
+Addsimps [singleton_fun];
+
+Goalw [Pi_def, function_def] "(A->0) = (if A=0 then {0} else 0)";
+by (Force_tac 1);
+qed "Pi_empty2";
+Addsimps [Pi_empty2];
+
+Goal "(A->X)=0 \\<longleftrightarrow> X=0 & (A \\<noteq> 0)";
+by Auto_tac;
+by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
+qed "fun_space_empty_iff";
+AddIffs [fun_space_empty_iff];
+
(** Extensionality **)