# HG changeset patch # User paulson # Date 830429114 -7200 # Node ID 3eaf3ab530825fc0b1ca0bdc85737fa7b2866a75 # Parent a5bcaf5894f37518f5784897165f8598c0a8af65 Rearrangement and polishing to look for for publication diff -r a5bcaf5894f3 -r 3eaf3ab53082 src/HOL/ex/Mutil.ML --- a/src/HOL/ex/Mutil.ML Thu Apr 25 11:48:13 1996 +0200 +++ b/src/HOL/ex/Mutil.ML Thu Apr 25 12:45:14 1996 +0200 @@ -3,18 +3,73 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge -The Mutilated Checkerboard Problem, formalized inductively +The Mutilated Chess Board Problem, formalized inductively *) open Mutil; -(*SHOULD NOT BE NECESSARY!*) -Addsimps [ball_rew,mem_Sigma_iff]; +Addsimps tiling.intrs; + +(** The union of two disjoint tilings is a tiling **) + +goal thy "!!t. t: tiling A ==> \ +\ u: tiling A --> t Int u = {} --> t Un u : tiling A"; +by (etac tiling.induct 1); +by (Simp_tac 1); +by (fast_tac (set_cs addIs tiling.intrs + addss (HOL_ss addsimps [Un_assoc, + subset_empty_iff RS sym])) 1); +bind_thm ("tiling_UnI", result() RS mp RS mp); + + +(*** Chess boards ***) + +val [below_0, below_Suc] = nat_recs below_def; +Addsimps [below_0]; +(*below_Suc should NOT be added, or Sigma_Suc1,2 cannot be used*) + +goal thy "(i: below k) = (i finite d"; -by (fast_tac (set_cs addSIs [finite_insertI, finite_emptyI] addEs [domino.elim]) 1); -qed "domino_finite"; - -goal thy "!!d. [| d:domino; b<2 |] ==> EX i' j'. evnodd d b = {(i',j')}"; +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); @@ -63,19 +114,13 @@ THEN fast_tac less_cs 1)); qed "domino_singleton"; - -(*** Tilings ***) - -(** The union of two disjoint tilings is a tiling **) +goal thy "!!d. d:domino ==> finite d"; +by (fast_tac (set_cs addSIs [finite_insertI, finite_emptyI] + addEs [domino.elim]) 1); +qed "domino_finite"; -goal thy "!!t. t: tiling A ==> \ -\ u: tiling A --> t Int u = {} --> t Un u : tiling A"; -by (etac tiling.induct 1); -by (simp_tac (!simpset addsimps tiling.intrs) 1); -by (fast_tac (set_cs addIs tiling.intrs - addss (HOL_ss addsimps [Un_assoc, - subset_empty_iff RS sym])) 1); -bind_thm ("tiling_UnI", result() RS mp RS mp); + +(*** Tilings of dominoes ***) goal thy "!!t. t:tiling domino ==> finite t"; by (eresolve_tac [tiling.induct] 1); @@ -99,56 +144,8 @@ by (fast_tac (set_cs addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1); qed "tiling_domino_0_1"; - -val [below_0, below_Suc] = nat_recs below_def; -Addsimps [below_0]; -(*below_Suc should NOT be added, or Sigma_Suc1,2 cannot be used*) - -goal thy "(i: below k) = (i t' ~: tiling domino"; by (rtac notI 1); by (dtac tiling_domino_0_1 1); diff -r a5bcaf5894f3 -r 3eaf3ab53082 src/HOL/ex/Mutil.thy --- a/src/HOL/ex/Mutil.thy Thu Apr 25 11:48:13 1996 +0200 +++ b/src/HOL/ex/Mutil.thy Thu Apr 25 12:45:14 1996 +0200 @@ -3,19 +3,17 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge -The Mutilated Checkerboard Problem, formalized inductively +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 = Finite + consts - below :: nat => nat set - evnodd :: "[(nat*nat)set, nat] => (nat*nat)set" domino :: "(nat*nat)set set" tiling :: 'a set set => 'a set set - -defs - below_def "below n == nat_rec n {} insert" - evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}" + below :: nat => nat set + evnodd :: "[(nat*nat)set, nat] => (nat*nat)set" inductive "domino" intrs @@ -27,4 +25,8 @@ empty "{} : tiling A" Un "[| a: A; t: tiling A; a Int t = {} |] ==> a Un t : tiling A" +defs + below_def "below n == nat_rec n {} insert" + evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}" + end