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/ZF/Zorn0.thy
author oheimb
Fri, 02 Jun 2000 17:46:32 +0200
changeset 9020 1056cbbaeb29
parent 485 5e00a676a211
permissions -rw-r--r--
added split_eta_SetCompr2 (also to simpset), generalized SetCompr_Sigma_eq

(*  Title: 	ZF/Zorn0.thy
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Based upon the article
    Abrial & Laffitte, 
    Towards the Mechanization of the Proofs of Some 
    Classical Theorems of Set Theory. 
*)

Zorn0 = OrderArith + AC + "inductive" +

consts
  Subset_rel      :: "i=>i"
  increasing      :: "i=>i"
  chain, maxchain :: "i=>i"
  super           :: "[i,i]=>i"

rules
  Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"

  chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
  super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
  maxchain_def   "maxchain(A)   == {c: chain(A). super(A,c)=0}"

end
isabelle