--- 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] "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b";
-by (Blast_tac 1);
-qed "evnodd_iff";
-
-Goalw [evnodd_def] "evnodd(A, b) \\<subseteq> 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(<i,j>,C), b) = \
-\ (if (i#+j) mod 2 = b then cons(<i,j>, 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 \\<in> domino ==> Finite(d)";
-by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
-qed "domino_Finite";
-
-Goal "[| d \\<in> domino; b<2 |] ==> \\<exists>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 (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 \\<in> tiling(A) ==> \
-\ u \\<in> tiling(A) --> t Int u = 0 --> t Un u \\<in> 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 \\<in> 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 \\<in> 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 "\\<forall>p b. p \\<in> evnodd(a,b) --> p\\<notin>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 \\<in> nat; n \\<in> nat |] ==> {i} * (n #+ n) \\<in> 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'} = {<i,n'#+n'>, <i,succ(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 \\<in> nat; n \\<in> nat |] ==> m * (n #+ n) \\<in> 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<y |] ==> P";
-by Auto_tac;
-qed "eq_lt_E";
-
-Goal "[| m \\<in> nat; n \\<in> nat; \
-\ t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); \
-\ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] \
-\ ==> t' \\<notin> 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 \\<in> 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";
--- 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" \<subseteq> "Pow(nat \<times> nat)"
+ intros
+ horiz: "[| i \<in> nat; j \<in> nat |] ==> {<i,j>, <i,succ(j)>} \<in> domino"
+ vertl: "[| i \<in> nat; j \<in> nat |] ==> {<i,j>, <succ(i),j>} \<in> domino"
+ type_intros empty_subsetI cons_subsetI PowI SigmaI nat_succI
inductive
- domains "domino" <= "Pow(nat*nat)"
- intrs
- horiz "[| i \\<in> nat; j \\<in> nat |] ==> {<i,j>, <i,succ(j)>} \\<in> domino"
- vertl "[| i \\<in> nat; j \\<in> nat |] ==> {<i,j>, <succ(i),j>} \\<in> domino"
- type_intrs empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
+ domains "tiling(A)" \<subseteq> "Pow(Union(A))"
+ intros
+ empty: "0 \<in> tiling(A)"
+ Un: "[| a \<in> A; t \<in> tiling(A); a Int t = 0 |] ==> a Un t \<in> 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 \<in> A. \<exists>i j. z = <i,j> \<and> (i #+ j) mod 2 = b}"
+
+
+subsubsection {* Basic properties of evnodd *}
+
+lemma evnodd_iff: "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b"
+ by (unfold evnodd_def) blast
+
+lemma evnodd_subset: "evnodd(A, b) \<subseteq> 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(<i,j>,C), b) =
+ (if (i#+j) mod 2 = b then cons(<i,j>, 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 \<in> domino ==> Finite(d)"
+ by (blast intro!: Finite_cons Finite_0 elim: domino.cases)
+
+lemma domino_singleton: "[| d \<in> domino; b<2 |] ==> \<exists>i' j'. evnodd(d,b) = {<i',j'>}"
+ 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 \\<in> tiling(A)"
- Un "[| a \\<in> A; t \\<in> tiling(A); a Int t = 0 |] ==> a Un t \\<in> 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 \<in> tiling(A) ==> u \<in> tiling(A) ==> t Int u = 0 ==> t Un u \<in> 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 \<in> 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 \<in> 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 "\<forall>p b. p \<in> evnodd (a,b) --> p\<notin>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 \\<in> A. \\<exists>i j. z=<i,j> & (i#+j) mod 2 = b}"
+lemma dominoes_tile_row: "[| i \<in> nat; n \<in> nat |] ==> {i} * (n #+ n) \<in> 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'} = {<i,n'#+n'>, <i,succ (n'#+n') >}")
+ prefer 2 apply blast
+ apply (simp add: domino.horiz)
+ apply (blast elim: mem_irrefl mem_asym)
+ done
+
+lemma dominoes_tile_matrix: "[| m \<in> nat; n \<in> nat |] ==> m * (n #+ n) \<in> 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<y |] ==> P"
+ by auto
+
+theorem mutil_not_tiling: "[| m \<in> nat; n \<in> nat;
+ t = (succ(m)#+succ(m))*(succ(n)#+succ(n));
+ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |]
+ ==> t' \<notin> tiling(domino)"
+ apply (rule notI)
+ apply (drule tiling_domino_0_1)
+ apply (erule_tac x = "|?A|" in eq_lt_E)
+ apply (subgoal_tac "t \<in> 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