# HG changeset patch
# User paulson
# Date 827836334 -3600
# Node ID dd66bed09592ea7f3b835edf7e837a6dae886d94
# Parent  248e1e125ca062ebf47c872ea1dd2e04649be162
New example: mutilated checkerboard

diff -r 248e1e125ca0 -r dd66bed09592 src/ZF/ex/Mutil.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Mutil.ML	Tue Mar 26 11:32:14 1996 +0100
@@ -0,0 +1,170 @@
+(*  Title:      ZF/ex/Mutil
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+The Mutilated Checkerboard Problem, formalized inductively
+*)
+
+open Mutil;
+
+
+(** Basic properties of evnodd **)
+
+goalw thy [evnodd_def]
+    "!!i j. [| <i,j>: A;  (i#+j) mod 2 = b |] ==> <i,j>: 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=<i,j>;  <i,j>: 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";
+by (fast_tac ZF_cs 1);
+qed "evnodd_subset";
+
+(* Finite(X) ==> Finite(evnodd(X,b)) *)
+bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite);
+
+goalw thy [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)";
+by (simp_tac (ZF_ss addsimps [Collect_Un]) 1);
+qed "evnodd_Un";
+
+goalw thy [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)";
+by (simp_tac (ZF_ss addsimps [Collect_Diff]) 1);
+qed "evnodd_Diff";
+
+goalw thy [evnodd_def]
+    "evnodd(cons(<i,j>,C), b) = \
+\    if((i#+j) mod 2 = b, cons(<i,j>, evnodd(C,b)), evnodd(C,b))";
+by (asm_simp_tac (ZF_ss addsimps [evnodd_def, Collect_cons] 
+                        setloop split_tac [expand_if]) 1);
+by (fast_tac ZF_cs 1);
+qed "evnodd_cons";
+
+goalw thy [evnodd_def] "evnodd(0, b) = 0";
+by (simp_tac (ZF_ss addsimps [evnodd_def]) 1);
+qed "evnodd_0";
+
+
+(*** Dominoes ***)
+
+goal thy "!!d. d:domino ==> Finite(d)";
+by (fast_tac (ZF_cs addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
+qed "domino_Finite";
+
+goal thy "!!d. [| d:domino; b<2 |] ==> EX i' j'. evnodd(d,b) = {<i',j'>}";
+by (eresolve_tac [domino.elim] 1);
+by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 2);
+by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 1);
+by (REPEAT_FIRST (ares_tac [add_type]));
+(*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*)
+by (REPEAT (asm_simp_tac (arith_ss addsimps [evnodd_cons, evnodd_0, mod_succ,
+					     succ_neq_self] 
+                                   setloop split_tac [expand_if]) 1
+           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 ***)
+
+(** The union of two disjoint tilings is a tiling **)
+
+goal thy "!!t. t: tiling(A) ==> \
+\              ALL u: tiling(A). t Int u = 0 --> t Un u : tiling(A)";
+by (etac tiling.induct 1);
+by (simp_tac (ZF_ss addsimps tiling.intrs) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [Int_Un_distrib, Un_assoc, Un_subset_iff,
+				       subset_empty_iff RS iff_sym]) 1);
+by (safe_tac ZF_cs);
+by (resolve_tac tiling.intrs 1);
+by (assume_tac 1);
+by (fast_tac ZF_cs 1);
+by (fast_tac eq_cs 1);
+val lemma = result();
+
+goal thy "!!t u. [| t: tiling(A);  u: tiling(A);  t Int u = 0 |] ==> \
+\                t Un u : tiling(A)";
+by (fast_tac (ZF_cs addIs [lemma RS bspec RS mp]) 1);
+qed "tiling_UnI";
+
+goal thy "!!t. t:tiling(domino) ==> Finite(t)";
+by (eresolve_tac [tiling.induct] 1);
+by (resolve_tac [Finite_0] 1);
+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);
+qed "tiling_domino_0_1";
+
+goal thy "!!i n. [| i: nat;  n: nat |] ==> {i} * (n #+ n) : tiling(domino)";
+by (nat_ind_tac "n" [] 1);
+by (simp_tac (arith_ss addsimps tiling.intrs) 1);
+by (asm_simp_tac (arith_ss addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
+by (resolve_tac tiling.intrs 1);
+by (assume_tac 2);
+by (subgoal_tac	   (*seems the easiest way of turning one to the other*)
+    "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1);
+by (fast_tac eq_cs 2);
+by (asm_simp_tac (arith_ss addsimps [domino.horiz]) 1);
+by (fast_tac (eq_cs addEs [mem_irrefl, mem_asym]) 1);
+qed "dominoes_tile_row";
+
+goal thy "!!m n. [| m: nat;  n: nat |] ==> m * (n #+ n) : tiling(domino)";
+by (nat_ind_tac "m" [] 1);
+by (simp_tac (arith_ss addsimps tiling.intrs) 1);
+by (asm_simp_tac (arith_ss addsimps [Sigma_succ1]) 1);
+by (fast_tac (eq_cs addIs [tiling_UnI, dominoes_tile_row] 
+                    addEs [mem_irrefl]) 1);
+qed "dominoes_tile_matrix";
+
+
+goal thy "!!m n. [| m: nat;  n: nat;  \
+\                   t = (succ(m)#+succ(m))*(succ(n)#+succ(n));  \
+\                   t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] ==> \
+\                t' ~: tiling(domino)";
+by (resolve_tac [notI] 1);
+by (dresolve_tac [tiling_domino_0_1] 1);
+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);
+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);
+by (asm_simp_tac (arith_ss addsimps add_ac) 2);
+by (asm_full_simp_tac 
+    (arith_ss addsimps [evnodd_Diff, evnodd_cons, evnodd_0, mod2_add_self,
+			mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
+by (resolve_tac [lt_trans] 1);
+by (REPEAT
+    (rtac Finite_imp_cardinal_Diff 1 
+     THEN
+     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));
+qed "mutil_not_tiling";
diff -r 248e1e125ca0 -r dd66bed09592 src/ZF/ex/Mutil.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Mutil.thy	Tue Mar 26 11:32:14 1996 +0100
@@ -0,0 +1,38 @@
+(*  Title:      ZF/ex/Mutil
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+The Mutilated Checkerboard Problem, formalized inductively
+
+Really needs only CardinalArith, not AC, as sets are finite
+*)
+
+Mutil = Cardinal_AC +
+consts
+  domino  :: i
+  evnodd  :: [i,i]=>i
+  tiling  :: i=>i
+
+inductive
+  domains "domino" <= "Pow(nat*nat)"
+  intrs
+    horiz  "[| i: nat;  j: nat |] ==> {<i,j>, <i,succ(j)>} : domino"
+    vertl  "[| i: nat;  j: nat |] ==> {<i,j>, <succ(i),j>} : domino"
+  type_intrs "[empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI]"
+
+
+defs
+  evnodd_def "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
+
+inductive
+    domains "tiling(A)" <= "Pow(Union(A))"
+  intrs
+    empty  "0 : tiling(A)"
+    Un     "[| a: A;  t: tiling(A);  a Int t = 0 |] ==> a Un t : tiling(A)"
+  type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]"
+  type_elims "[make_elim PowD]"
+
+
+end
+