# HG changeset patch # User paulson # Date 967107920 -7200 # Node ID f87c8c449018c663212599ec0f5a1d6c055960c5 # Parent 00f8be1b7209f334f1a97d9a053548454b34bc15 added some xsymbols, and tidied diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/AC/AC18_AC19.ML --- 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)); diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/AC/AC7_AC9.ML --- 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"; diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/AC/AC_Equiv.ML --- 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"; diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/AC/DC.ML --- 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)"; diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/Arith.thy --- 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 "#\\" 70) end diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/Cardinal.ML --- 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"; diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/Cardinal.thy --- 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 "\\" 50) + "op lepoll" :: [i,i] => o (infixl "\\" 50) + "op lesspoll" :: [i,i] => o (infixl "\\" 50) + end diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/CardinalArith.thy --- 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 i (infixr "|\\|" 70) +syntax (xsymbols) + "op |+|" :: [i,i] => i (infixl "\\" 65) + "op |*|" :: [i,i] => i (infixl "\\" 70) end diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/Coind/Map.ML --- 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 *) diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/Order.thy --- 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). - {}" + UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {}" constdefs first :: [i, i, i] => o "first(u, X, R) == u:X & (ALL v:X. v~=u --> : R)" +syntax (xsymbols) + ord_iso :: [i,i,i,i]=>i ("('(_,_') \\ '(_,_'))" 50) + + end diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/OrderType.thy --- 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 "\\\\" 70) +syntax (xsymbols) + "op **" :: [i,i] => i (infixl "\\\\" 70) end diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/ZF.thy --- 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\\ _\\_./ _)" 10) "@PROD" :: [pttrn, i, i] => i ("(3\\ _\\_./ _)" 10) "@SUM" :: [pttrn, i, i] => i ("(3\\ _\\_./ _)" 10) + "@lam" :: [pttrn, i, i] => i ("(3\\ _:_./ _)" 10) "@Ball" :: [pttrn, i, o] => o ("(3\\ _\\_./ _)" 10) "@Bex" :: [pttrn, i, o] => o ("(3\\ _\\_./ _)" 10) (* diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/func.ML --- 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}"; -by (Blast_tac 1); -qed "singleton_fun"; - -Addsimps [Pi_empty1, singleton_fun]; - (*** Function Application ***) Goalw [Pi_def, function_def] "[| : f; : 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}"; +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 \\ X=0 & (A \\ 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 **)