isabelle: src/CCL/Fix.thy@4328356ab7e6 (annotated)

17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	1	(* Title: CCL/Fix.thy
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	3	Author: Martin Coen
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	6
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	7	header {* Tentative attempt at including fixed point induction; justified by Smith *}
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	8
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	9	theory Fix
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	10	imports Type
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	11	begin
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	12
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	consts
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	14	idgen :: "[i]=>i"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	15	INCL :: "[i=>o]=>o"
a5a9c433f639 Initial revision clasohm parents: diff changeset	16
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	17	axioms
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	18	idgen_def:
3837 d7f033c74b38 fixed dots; wenzelm parents: 1474 diff changeset	19	"idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	20
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	21	INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	22	po_INCL: "INCL(%x. a(x) [= b(x))"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	23	INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	24
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3837 diff changeset	25	ML {* use_legacy_bindings (the_context ()) *}
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26
a5a9c433f639 Initial revision clasohm parents: diff changeset	27	end

author	huffman
	Sun, 06 Nov 2005 00:22:03 +0100
changeset 18095	4328356ab7e6
parent 17456	bcf7544875b2
child 20140	98acc6d0fab6
permissions	-rw-r--r--