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
```