--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Mutil.thy Tue Mar 26 11:32:14 1996 +0100
@@ -0,0 +1,38 @@
+(* Title: ZF/ex/Mutil
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+The Mutilated Checkerboard Problem, formalized inductively
+
+Really needs only CardinalArith, not AC, as sets are finite
+*)
+
+Mutil = Cardinal_AC +
+consts
+ domino :: i
+ evnodd :: [i,i]=>i
+ tiling :: i=>i
+
+inductive
+ domains "domino" <= "Pow(nat*nat)"
+ intrs
+ horiz "[| i: nat; j: nat |] ==> {<i,j>, <i,succ(j)>} : domino"
+ vertl "[| i: nat; j: nat |] ==> {<i,j>, <succ(i),j>} : domino"
+ type_intrs "[empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI]"
+
+
+defs
+ evnodd_def "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
+
+inductive
+ domains "tiling(A)" <= "Pow(Union(A))"
+ intrs
+ empty "0 : tiling(A)"
+ Un "[| a: A; t: tiling(A); a Int t = 0 |] ==> a Un t : tiling(A)"
+ type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]"
+ type_elims "[make_elim PowD]"
+
+
+end
+