Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/CCL/Fix.thy
author wenzelm
Tue, 11 Apr 2006 16:00:02 +0200
changeset 19406 410b9d9bf9a1
parent 17456 bcf7544875b2
child 20140 98acc6d0fab6
permissions -rw-r--r--
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;

(*  Title:      CCL/Fix.thy
    ID:         $Id$
    Author:     Martin Coen
    Copyright   1993  University of Cambridge
*)

header {* Tentative attempt at including fixed point induction; justified by Smith *}

theory Fix
imports Type
begin

consts
  idgen      ::       "[i]=>i"
  INCL      :: "[i=>o]=>o"

axioms
  idgen_def:
  "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"

  INCL_def:   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
  po_INCL:    "INCL(%x. a(x) [= b(x))"
  INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"

ML {* use_legacy_bindings (the_context ()) *}

end
isabelle