--- a/src/ZF/ex/Mutil.thy Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* 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