src/ZF/Induct/Mutil.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Mutil.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,36 @@
+(*  Title:      ZF/ex/Mutil
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+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 = Main +
+consts
+  domino  :: i
+  tiling  :: i=>i
+
+inductive
+  domains "domino" <= "Pow(nat*nat)"
+  intrs
+    horiz  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <i,succ(j)>} \\<in> domino"
+    vertl  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <succ(i),j>} \\<in> domino"
+  type_intrs  empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
+
+
+inductive
+    domains "tiling(A)" <= "Pow(Union(A))"
+  intrs
+    empty  "0 \\<in> tiling(A)"
+    Un     "[| a \\<in> A;  t \\<in> tiling(A);  a Int t = 0 |] ==> a Un t \\<in> tiling(A)"
+  type_intrs  empty_subsetI, Union_upper, Un_least, PowI
+  type_elims "[make_elim PowD]"
+
+constdefs
+  evnodd  :: [i,i]=>i
+  "evnodd(A,b) == {z \\<in> A. \\<exists>i j. z=<i,j> & (i#+j) mod 2 = b}"
+
+end