src/ZF/Zorn.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1478 2b8c2a7547ab
child 6053 8a1059aa01f0
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:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/Zorn.thy
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     4
    Copyright   1994  University of Cambridge
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     5
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     6
Based upon the article
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     7
    Abrial & Laffitte, 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     8
    Towards the Mechanization of the Proofs of Some 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     9
    Classical Theorems of Set Theory. 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    10
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    11
Union_in_Pow is proved in ZF.ML
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    12
*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    13
806
6330ca0a3ac5 removed quotes around "Inductive"
lcp
parents: 753
diff changeset
    14
Zorn = OrderArith + AC + Inductive +
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    15
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    16
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    17
  Subset_rel      :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    18
  increasing      :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    19
  chain, maxchain :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    20
  super           :: [i,i]=>i
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    21
753
ec86863e87c8 replaced "rules" by "defs"
lcp
parents: 578
diff changeset
    22
defs
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    23
  Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    24
  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    25
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    26
  chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    27
  super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    28
  maxchain_def   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    29
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    30
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    31
(** We could make the inductive definition conditional on next: increasing(S)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    32
    but instead we make this a side-condition of an introduction rule.  Thus
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    33
    the induction rule lets us assume that condition!  Many inductive proofs
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    34
    are therefore unconditional.
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    35
**)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    36
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    37
  "TFin" :: [i,i]=>i
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    38
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    39
inductive
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    40
  domains       "TFin(S,next)" <= "Pow(S)"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    41
  intrs
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    42
    nextI       "[| x : TFin(S,next);  next: increasing(S) 
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 806
diff changeset
    43
                |] ==> next`x : TFin(S,next)"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    44
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    45
    Pow_UnionI  "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    46
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    47
  monos         "[Pow_mono]"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    48
  con_defs      "[increasing_def]"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    49
  type_intrs    "[CollectD1 RS apply_funtype, Union_in_Pow]"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    50
  
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    51
end