src/HOL/Induct/Mutil.thy
 changeset 8340 c169cd21fe42 parent 5931 325300576da7 child 8399 86b04d47b853
```     1.1 --- a/src/HOL/Induct/Mutil.thy	Sat Mar 04 11:52:42 2000 +0100
1.2 +++ b/src/HOL/Induct/Mutil.thy	Sat Mar 04 12:02:41 2000 +0100
1.3 @@ -8,25 +8,25 @@
1.4    Popularized as the Mutilated Checkerboard Problem by J McCarthy
1.5  *)
1.6
1.7 -Mutil = Finite +
1.8 -consts
1.9 -  domino  :: "(nat*nat)set set"
1.10 -  tiling  :: "'a set set => 'a set set"
1.11 -  below   :: "nat => nat set"
1.12 -  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
1.13 +Mutil = Main +
1.14
1.15 +consts    domino :: "(nat*nat)set set"
1.16  inductive domino
1.17    intrs
1.18      horiz  "{(i, j), (i, Suc j)} : domino"
1.19      vertl  "{(i, j), (Suc i, j)} : domino"
1.20
1.21 +consts     tiling :: "'a set set => 'a set set"
1.22  inductive "tiling A"
1.23    intrs
1.24      empty  "{} : tiling A"
1.25      Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
1.26
1.27 -defs
1.28 -  below_def  "below n    == {i. i<n}"
1.29 -  evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
1.30 +constdefs
1.31 +  below   :: "nat => nat set"
1.32 +   "below n    == {i. i<n}"
1.33 +
1.34 +  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
1.35 +   "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
1.36
1.37  end
```