isabelle: src/ZF/ex/Mutil.thy@a528a716a312 (annotated)

1606 dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	1	(* Title: ZF/ex/Mutil
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	2	ID: $Id$
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	4	Copyright 1996 University of Cambridge
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	5
1702 4aa538e82f76 Cosmetic re-ordering of declarations paulson parents: 1624 diff changeset	6	The Mutilated Chess Board Problem, formalized inductively
4aa538e82f76 Cosmetic re-ordering of declarations paulson parents: 1624 diff changeset	7	Originator is Max Black, according to J A Robinson.
4aa538e82f76 Cosmetic re-ordering of declarations paulson parents: 1624 diff changeset	8	Popularized as the Mutilated Checkerboard Problem by J McCarthy
1606 dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	9	*)
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	10
11354 9b80fe19407f examples files start from Main instead of various ZF theories paulson parents: 11316 diff changeset	11	Mutil = Main +
1606 dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	12	consts
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	13	domino :: i
1702 4aa538e82f76 Cosmetic re-ordering of declarations paulson parents: 1624 diff changeset	14	tiling :: i=>i
1606 dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	15
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	16	inductive
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	17	domains "domino" <= "Pow(nat*nat)"
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	18	intrs
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6117 diff changeset	19	horiz "[\| i \\<in> nat; j \\<in> nat \|] ==> {<i,j>, <i,succ(j)>} \\<in> domino"
b4e71bd751e4 X-symbols for set theory paulson parents: 6117 diff changeset	20	vertl "[\| i \\<in> nat; j \\<in> nat \|] ==> {<i,j>, <succ(i),j>} \\<in> domino"
6117 f9aad8ccd590 tidying of datatype and inductive definitions paulson parents: 1806 diff changeset	21	type_intrs empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
1606 dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	22
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	23
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	24	inductive
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	25	domains "tiling(A)" <= "Pow(Union(A))"
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	26	intrs
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6117 diff changeset	27	empty "0 \\<in> tiling(A)"
b4e71bd751e4 X-symbols for set theory paulson parents: 6117 diff changeset	28	Un "[\| a \\<in> A; t \\<in> tiling(A); a Int t = 0 \|] ==> a Un t \\<in> tiling(A)"
6117 f9aad8ccd590 tidying of datatype and inductive definitions paulson parents: 1806 diff changeset	29	type_intrs empty_subsetI, Union_upper, Un_least, PowI
1606 dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	30	type_elims "[make_elim PowD]"
dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	31
1806 12708740f58d Converted to use constdefs instead of defs paulson parents: 1702 diff changeset	32	constdefs
12708740f58d Converted to use constdefs instead of defs paulson parents: 1702 diff changeset	33	evnodd :: [i,i]=>i
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6117 diff changeset	34	"evnodd(A,b) == {z \\<in> A. \\<exists>i j. z=<i,j> & (i#+j) mod 2 = b}"
1702 4aa538e82f76 Cosmetic re-ordering of declarations paulson parents: 1624 diff changeset	35
1606 dd66bed09592 New example: mutilated checkerboard paulson parents: diff changeset	36	end

author	wenzelm
	Sat, 20 Oct 2001 20:20:41 +0200
changeset 11852	a528a716a312
parent 11354	9b80fe19407f
permissions	-rw-r--r--