# HG changeset patch # User paulson # Date 828006970 -3600 # Node ID e2a6102b9369f780411a7fc372ecc0e5a889b1a1 # Parent 2b8573c1b1c10a78d030f02010851c1ba95fc0ec Alternative proof removes dependence upon AC diff -r 2b8573c1b1c1 -r e2a6102b9369 src/ZF/ex/Mutil.ML --- a/src/ZF/ex/Mutil.ML Thu Mar 28 10:52:59 1996 +0100 +++ b/src/ZF/ex/Mutil.ML Thu Mar 28 10:56:10 1996 +0100 @@ -11,20 +11,9 @@ (** Basic properties of evnodd **) -goalw thy [evnodd_def] - "!!i j. [| : A; (i#+j) mod 2 = b |] ==> : evnodd(A,b)"; -by (fast_tac ZF_cs 1); -qed "evnoddI"; - -val major::prems = goalw thy [evnodd_def] - "[| z: evnodd(A,b); \ -\ !!i j. [| z=; : A; (i#+j) mod 2 = b |] ==> P |] ==> P"; -br (major RS CollectE) 1; -by (REPEAT (eresolve_tac [exE,conjE] 1)); -by (resolve_tac prems 1); -by (REPEAT (fast_tac ZF_cs 1)); -qed "evnoddE"; - +goalw thy [evnodd_def] ": evnodd(A,b) <-> : A & (i#+j) mod 2 = b"; +by (fast_tac eq_cs 1); +qed "evnodd_iff"; goalw thy [evnodd_def] "evnodd(A, b) <= A"; by (fast_tac ZF_cs 1); @@ -72,12 +61,6 @@ THEN fast_tac (ZF_cs addDs [ltD]) 1)); qed "domino_singleton"; -val prems = goal thy "[| d:domino; b<2 |] ==> |evnodd(d,b)| = 1"; -by (cut_facts_tac [prems MRS domino_singleton] 1); -by (REPEAT (etac exE 1)); -by (asm_simp_tac (ZF_ss addsimps [cardinal_singleton]) 1); -qed "cardinal_evnodd_domino"; - (*** Tilings ***) @@ -107,18 +90,19 @@ by (fast_tac (ZF_cs addIs [domino_Finite, Finite_Un]) 1); qed "tiling_domino_Finite"; -(*Uses AC in the form of cardinal_disjoint_Un; could instead use - tiling_domino_Finite, well_ord_cardinal_eqE and Finite_imp_well_ord*) goal thy "!!t. t: tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"; by (eresolve_tac [tiling.induct] 1); by (simp_tac (ZF_ss addsimps [evnodd_def]) 1); -by (asm_simp_tac (ZF_ss addsimps [evnodd_Un]) 1); -by (rtac cardinal_disjoint_Un 1); -by (asm_simp_tac (arith_ss addsimps [cardinal_evnodd_domino]) 1); -by (asm_simp_tac (arith_ss addsimps [cardinal_evnodd_domino]) 1); -bw evnodd_def; -by (fast_tac (eq_cs addSEs [equalityE]) 1); -by (fast_tac (eq_cs addSEs [equalityE]) 1); +by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); +by (simp_tac arith_ss 2 THEN assume_tac 1); +by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); +by (simp_tac arith_ss 2 THEN assume_tac 1); +by (step_tac ZF_cs 1); +by (subgoal_tac "ALL p b. p:evnodd(a,b) --> p~:evnodd(ta,b)" 1); +by (asm_simp_tac (ZF_ss addsimps [evnodd_Un, Un_cons, tiling_domino_Finite, + evnodd_subset RS subset_Finite, + Finite_imp_cardinal_cons]) 1); +by (fast_tac (ZF_cs addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); qed "tiling_domino_0_1"; goal thy "!!i n. [| i: nat; n: nat |] ==> {i} * (n #+ n) : tiling(domino)"; @@ -152,6 +136,7 @@ by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1); by (asm_full_simp_tac (ZF_ss addsimps [lt_not_refl]) 1); by (subgoal_tac "t : tiling(domino)" 1); +(*Requires a small simpset that won't move the succ applications*) by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, dominoes_tile_matrix]) 2); by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1); @@ -166,5 +151,6 @@ asm_simp_tac (arith_ss addsimps [tiling_domino_Finite, Finite_evnodd, Finite_Diff]) 1 THEN - asm_simp_tac (arith_ss addsimps [evnoddI, nat_0_le RS ltD, mod2_add_self]) 1)); + asm_simp_tac (arith_ss addsimps [evnodd_iff, nat_0_le RS ltD, + mod2_add_self]) 1)); qed "mutil_not_tiling"; diff -r 2b8573c1b1c1 -r e2a6102b9369 src/ZF/ex/Mutil.thy --- a/src/ZF/ex/Mutil.thy Thu Mar 28 10:52:59 1996 +0100 +++ b/src/ZF/ex/Mutil.thy Thu Mar 28 10:56:10 1996 +0100 @@ -4,11 +4,9 @@ Copyright 1996 University of Cambridge The Mutilated Checkerboard Problem, formalized inductively - -Really needs only CardinalArith, not AC, as sets are finite *) -Mutil = Cardinal_AC + +Mutil = CardinalArith + consts domino :: i evnodd :: [i,i]=>i @@ -33,6 +31,4 @@ type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]" type_elims "[make_elim PowD]" - end -