# HG changeset patch # User wenzelm # Date 1005686377 -3600 # Node ID f3f7993ae6da956c7c8092f820b45d8f945b4c7c # Parent 5e81c9d539f84810a68e567fe2481a9bb9742bd8 converted; diff -r 5e81c9d539f8 -r f3f7993ae6da src/ZF/Induct/Mutil.ML --- a/src/ZF/Induct/Mutil.ML Tue Nov 13 22:18:46 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,147 +0,0 @@ -(* 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 [evnodd_def] ": evnodd(A,b) <-> : A & (i#+j) mod 2 = b"; -by (Blast_tac 1); -qed "evnodd_iff"; - -Goalw [evnodd_def] "evnodd(A, b) \\ A"; -by (Blast_tac 1); -qed "evnodd_subset"; - -(* Finite(X) ==> Finite(evnodd(X,b)) *) -bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite); - -Goalw [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)"; -by (simp_tac (simpset() addsimps [Collect_Un]) 1); -qed "evnodd_Un"; - -Goalw [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"; -by (simp_tac (simpset() addsimps [Collect_Diff]) 1); -qed "evnodd_Diff"; - -Goalw [evnodd_def] - "evnodd(cons(,C), b) = \ -\ (if (i#+j) mod 2 = b then cons(, evnodd(C,b)) else evnodd(C,b))"; -by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]) 1); -qed "evnodd_cons"; - -Goalw [evnodd_def] "evnodd(0, b) = 0"; -by (simp_tac (simpset() addsimps [evnodd_def]) 1); -qed "evnodd_0"; - -Addsimps [evnodd_cons, evnodd_0]; - -(*** Dominoes ***) - -Goal "d \\ domino ==> Finite(d)"; -by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1); -qed "domino_Finite"; - -Goal "[| d \\ domino; b<2 |] ==> \\i' j'. evnodd(d,b) = {}"; -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 (simpset() addsimps [mod_succ, succ_neq_self]) 1 - THEN blast_tac (claset() addDs [ltD]) 1)); -qed "domino_singleton"; - - -(*** Tilings ***) - -(** The union of two disjoint tilings is a tiling **) - -Goal "t \\ tiling(A) ==> \ -\ u \\ tiling(A) --> t Int u = 0 --> t Un u \\ tiling(A)"; -by (etac tiling.induct 1); -by (simp_tac (simpset() addsimps tiling.intrs) 1); -by (asm_full_simp_tac (simpset() addsimps [Un_assoc, - subset_empty_iff RS iff_sym]) 1); -by (blast_tac (claset() addIs tiling.intrs) 1); -qed_spec_mp "tiling_UnI"; - -Goal "t \\ tiling(domino) ==> Finite(t)"; -by (eresolve_tac [tiling.induct] 1); -by (rtac Finite_0 1); -by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1); -qed "tiling_domino_Finite"; - -Goal "t \\ tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"; -by (eresolve_tac [tiling.induct] 1); -by (simp_tac (simpset() addsimps [evnodd_def]) 1); -by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); -by (Simp_tac 2 THEN assume_tac 1); -by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); -by (Simp_tac 2 THEN assume_tac 1); -by Safe_tac; -by (subgoal_tac "\\p b. p \\ evnodd(a,b) --> p\\evnodd(t,b)" 1); -by (asm_simp_tac - (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite, - evnodd_subset RS subset_Finite, - Finite_imp_cardinal_cons]) 1); -by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] - addEs [equalityE]) 1); -qed "tiling_domino_0_1"; - -Goal "[| i \\ nat; n \\ nat |] ==> {i} * (n #+ n) \\ tiling(domino)"; -by (induct_tac "n" 1); -by (simp_tac (simpset() addsimps tiling.intrs) 1); -by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1); -by (resolve_tac tiling.intrs 1); -by (assume_tac 2); -by (rename_tac "n'" 1); -by (subgoal_tac (*seems the easiest way of turning one to the other*) - "{i}*{succ(n'#+n')} Un {i}*{n'#+n'} = {, }" 1); -by (Blast_tac 2); -by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1); -by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1); -qed "dominoes_tile_row"; - -Goal "[| m \\ nat; n \\ nat |] ==> m * (n #+ n) \\ tiling(domino)"; -by (induct_tac "m" 1); -by (simp_tac (simpset() addsimps tiling.intrs) 1); -by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1); -by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] - addEs [mem_irrefl]) 1); -qed "dominoes_tile_matrix"; - -Goal "[| x=y; x P"; -by Auto_tac; -qed "eq_lt_E"; - -Goal "[| m \\ nat; n \\ nat; \ -\ t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); \ -\ t' = t - {<0,0>} - {} |] \ -\ ==> t' \\ tiling(domino)"; -by (rtac notI 1); -by (dtac tiling_domino_0_1 1); -by (eres_inst_tac [("x", "|?A|")] eq_lt_E 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 (asm_full_simp_tac - (simpset() addsimps [evnodd_Diff, mod2_add_self, - mod2_succ_succ, tiling_domino_0_1 RS sym]) 1); -by (rtac lt_trans 1); -by (REPEAT - (rtac Finite_imp_cardinal_Diff 1 - THEN - asm_simp_tac (simpset() addsimps [tiling_domino_Finite, Finite_evnodd, - Finite_Diff]) 1 - THEN - asm_simp_tac (simpset() addsimps [evnodd_iff, nat_0_le RS ltD, - mod2_add_self]) 1)); -qed "mutil_not_tiling"; diff -r 5e81c9d539f8 -r f3f7993ae6da src/ZF/Induct/Mutil.thy --- a/src/ZF/Induct/Mutil.thy Tue Nov 13 22:18:46 2001 +0100 +++ b/src/ZF/Induct/Mutil.thy Tue Nov 13 22:19:37 2001 +0100 @@ -1,36 +1,158 @@ -(* Title: ZF/ex/Mutil +(* Title: ZF/Induct/Mutil.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge - -The Mutilated Chess Board Problem, formalized inductively - Originator is Max Black, according to J A Robinson. - Popularized as the Mutilated Checkerboard Problem by J McCarthy *) -Mutil = Main + +header {* The Mutilated Chess Board Problem, formalized inductively *} + +theory Mutil = Main: + +text {* + Originator is Max Black, according to J A Robinson. Popularized as + the Mutilated Checkerboard Problem by J McCarthy. +*} + consts - domino :: i - tiling :: i=>i + domino :: i + tiling :: "i => i" + +inductive + domains "domino" \ "Pow(nat \ nat)" + intros + horiz: "[| i \ nat; j \ nat |] ==> {, } \ domino" + vertl: "[| i \ nat; j \ nat |] ==> {, } \ domino" + type_intros empty_subsetI cons_subsetI PowI SigmaI nat_succI inductive - domains "domino" <= "Pow(nat*nat)" - intrs - horiz "[| i \\ nat; j \\ nat |] ==> {, } \\ domino" - vertl "[| i \\ nat; j \\ nat |] ==> {, } \\ domino" - type_intrs empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI + domains "tiling(A)" \ "Pow(Union(A))" + intros + empty: "0 \ tiling(A)" + Un: "[| a \ A; t \ tiling(A); a Int t = 0 |] ==> a Un t \ tiling(A)" + type_intros empty_subsetI Union_upper Un_least PowI + type_elims PowD [elim_format] + +constdefs + evnodd :: "[i, i] => i" + "evnodd(A,b) == {z \ A. \i j. z = \ (i #+ j) mod 2 = b}" + + +subsubsection {* Basic properties of evnodd *} + +lemma evnodd_iff: ": evnodd(A,b) <-> : A & (i#+j) mod 2 = b" + by (unfold evnodd_def) blast + +lemma evnodd_subset: "evnodd(A, b) \ A" + by (unfold evnodd_def) blast + +lemma Finite_evnodd: "Finite(X) ==> Finite(evnodd(X,b))" + by (rule lepoll_Finite, rule subset_imp_lepoll, rule evnodd_subset) + +lemma evnodd_Un: "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)" + by (simp add: evnodd_def Collect_Un) + +lemma evnodd_Diff: "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)" + by (simp add: evnodd_def Collect_Diff) + +lemma evnodd_cons [simp]: + "evnodd(cons(,C), b) = + (if (i#+j) mod 2 = b then cons(, evnodd(C,b)) else evnodd(C,b))" + by (simp add: evnodd_def Collect_cons) + +lemma evnodd_0 [simp]: "evnodd(0, b) = 0" + by (simp add: evnodd_def) + + +subsubsection {* Dominoes *} + +lemma domino_Finite: "d \ domino ==> Finite(d)" + by (blast intro!: Finite_cons Finite_0 elim: domino.cases) + +lemma domino_singleton: "[| d \ domino; b<2 |] ==> \i' j'. evnodd(d,b) = {}" + apply (erule domino.cases) + apply (rule_tac [2] k1 = "i#+j" in mod2_cases [THEN disjE]) + apply (rule_tac k1 = "i#+j" in mod2_cases [THEN disjE]) + apply (rule add_type | assumption)+ + (*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*) + apply (auto simp add: mod_succ succ_neq_self dest: ltD) + done -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]" +subsubsection {* Tilings *} + +text {* The union of two disjoint tilings is a tiling *} + +lemma tiling_UnI: + "t \ tiling(A) ==> u \ tiling(A) ==> t Int u = 0 ==> t Un u \ tiling(A)" + apply (induct set: tiling) + apply (simp add: tiling.intros) + apply (simp add: Un_assoc subset_empty_iff [THEN iff_sym]) + apply (blast intro: tiling.intros) + done + +lemma tiling_domino_Finite: "t \ tiling(domino) ==> Finite(t)" + apply (induct rule: tiling.induct) + apply (rule Finite_0) + apply (blast intro!: Finite_Un intro: domino_Finite) + done + +lemma tiling_domino_0_1: "t \ tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|" + apply (induct rule: tiling.induct) + apply (simp add: evnodd_def) + apply (rule_tac b1 = 0 in domino_singleton [THEN exE]) + prefer 2 + apply simp + apply assumption + apply (rule_tac b1 = 1 in domino_singleton [THEN exE]) + prefer 2 + apply simp + apply assumption + apply safe + apply (subgoal_tac "\p b. p \ evnodd (a,b) --> p\evnodd (t,b)") + apply (simp add: evnodd_Un Un_cons tiling_domino_Finite + evnodd_subset [THEN subset_Finite] Finite_imp_cardinal_cons) + apply (blast dest!: evnodd_subset [THEN subsetD] elim: equalityE) + done -constdefs - evnodd :: [i,i]=>i - "evnodd(A,b) == {z \\ A. \\i j. z= & (i#+j) mod 2 = b}" +lemma dominoes_tile_row: "[| i \ nat; n \ nat |] ==> {i} * (n #+ n) \ tiling(domino)" + apply (induct_tac n) + apply (simp add: tiling.intros) + apply (simp add: Un_assoc [symmetric] Sigma_succ2) + apply (rule tiling.intros) + prefer 2 apply assumption + apply (rename_tac n') + apply (subgoal_tac (*seems the easiest way of turning one to the other*) + "{i}*{succ (n'#+n') } Un {i}*{n'#+n'} = {, }") + prefer 2 apply blast + apply (simp add: domino.horiz) + apply (blast elim: mem_irrefl mem_asym) + done + +lemma dominoes_tile_matrix: "[| m \ nat; n \ nat |] ==> m * (n #+ n) \ tiling(domino)" + apply (induct_tac m) + apply (simp add: tiling.intros) + apply (simp add: Sigma_succ1) + apply (blast intro: tiling_UnI dominoes_tile_row elim: mem_irrefl) + done + +lemma eq_lt_E: "[| x=y; x P" + by auto + +theorem mutil_not_tiling: "[| m \ nat; n \ nat; + t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); + t' = t - {<0,0>} - {} |] + ==> t' \ tiling(domino)" + apply (rule notI) + apply (drule tiling_domino_0_1) + apply (erule_tac x = "|?A|" in eq_lt_E) + apply (subgoal_tac "t \ tiling (domino)") + prefer 2 (*Requires a small simpset that won't move the succ applications*) + apply (simp only: nat_succI add_type dominoes_tile_matrix) + apply (simp add: evnodd_Diff mod2_add_self mod2_succ_succ tiling_domino_0_1 [symmetric]) + apply (rule lt_trans) + apply (rule Finite_imp_cardinal_Diff, + simp add: tiling_domino_Finite Finite_evnodd Finite_Diff, + simp add: evnodd_iff nat_0_le [THEN ltD] mod2_add_self)+ + done end