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