src/ZF/Zorn.thy
author lcp
Fri Aug 12 12:51:34 1994 +0200 (1994-08-12)
changeset 516 1957113f0d7d
parent 485 5e00a676a211
child 578 efc648d29dd0
permissions -rw-r--r--
installation of new inductive/datatype sections
lcp@516
     1
(*  Title: 	ZF/Zorn.thy
lcp@516
     2
    ID:         $Id$
lcp@516
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     4
    Copyright   1994  University of Cambridge
lcp@516
     5
lcp@516
     6
Based upon the article
lcp@516
     7
    Abrial & Laffitte, 
lcp@516
     8
    Towards the Mechanization of the Proofs of Some 
lcp@516
     9
    Classical Theorems of Set Theory. 
lcp@516
    10
lcp@516
    11
Union_in_Pow is proved in ZF.ML
lcp@516
    12
*)
lcp@516
    13
lcp@516
    14
Zorn = OrderArith + AC + "inductive" +
lcp@516
    15
lcp@516
    16
consts
lcp@516
    17
  Subset_rel      :: "i=>i"
lcp@516
    18
  increasing      :: "i=>i"
lcp@516
    19
  chain, maxchain :: "i=>i"
lcp@516
    20
  super           :: "[i,i]=>i"
lcp@516
    21
lcp@516
    22
rules
lcp@516
    23
  Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
lcp@516
    24
  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
lcp@485
    25
lcp@516
    26
  chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
lcp@516
    27
  super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
lcp@516
    28
  maxchain_def   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
lcp@516
    29
lcp@516
    30
lcp@516
    31
(** We could make the inductive definition conditional on next: increasing(S)
lcp@516
    32
    but instead we make this a side-condition of an introduction rule.  Thus
lcp@516
    33
    the induction rule lets us assume that condition!  Many inductive proofs
lcp@516
    34
    are therefore unconditional.
lcp@516
    35
**)
lcp@516
    36
consts
lcp@516
    37
  "TFin" :: "[i,i]=>i"
lcp@516
    38
lcp@516
    39
inductive
lcp@516
    40
  domains       "TFin(S,next)" <= "Pow(S)"
lcp@516
    41
  intrs
lcp@516
    42
    nextI	"[| x : TFin(S,next);  next: increasing(S) \
lcp@516
    43
\                |] ==> next`x : TFin(S,next)"
lcp@516
    44
lcp@516
    45
    Pow_UnionI	"Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
lcp@516
    46
lcp@516
    47
  monos         "[Pow_mono]"
lcp@516
    48
  con_defs      "[increasing_def]"
lcp@516
    49
  type_intrs    "[CollectD1 RS apply_funtype, Union_in_Pow]"
lcp@516
    50
  
lcp@516
    51
end