src/HOL/Induct/Mutil.thy
author paulson
Wed Nov 18 15:10:46 1998 +0100 (1998-11-18)
changeset 5931 325300576da7
parent 3424 bf466159ef84
child 8340 c169cd21fe42
permissions -rw-r--r--
Finally removing "Compl" from HOL
     1 (*  Title:      HOL/Induct/Mutil
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 The Mutilated Chess Board Problem, formalized inductively
     7   Originator is Max Black, according to J A Robinson.
     8   Popularized as the Mutilated Checkerboard Problem by J McCarthy
     9 *)
    10 
    11 Mutil = Finite +
    12 consts
    13   domino  :: "(nat*nat)set set"
    14   tiling  :: "'a set set => 'a set set"
    15   below   :: "nat => nat set"
    16   evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
    17 
    18 inductive domino
    19   intrs
    20     horiz  "{(i, j), (i, Suc j)} : domino"
    21     vertl  "{(i, j), (Suc i, j)} : domino"
    22 
    23 inductive "tiling A"
    24   intrs
    25     empty  "{} : tiling A"
    26     Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
    27 
    28 defs
    29   below_def  "below n    == {i. i<n}"
    30   evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
    31 
    32 end