src/ZF/Zorn0.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 485 5e00a676a211
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/Zorn0.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     2
    ID:         $Id$
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     5
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     6
Based upon the article
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     7
    Abrial & Laffitte, 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     8
    Towards the Mechanization of the Proofs of Some 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     9
    Classical Theorems of Set Theory. 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    10
*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    11
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    12
Zorn0 = OrderArith + AC + "inductive" +
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    13
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    14
consts
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    15
  Subset_rel      :: "i=>i"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    16
  increasing      :: "i=>i"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    17
  chain, maxchain :: "i=>i"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    18
  super           :: "[i,i]=>i"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    19
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    20
rules
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    21
  Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    22
  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    23
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    24
  chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    25
  super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    26
  maxchain_def   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    27
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    28
end