src/ZF/Zorn.thy
 author clasohm Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago) changeset 1401 0c439768f45c parent 1155 928a16e02f9f child 1478 2b8c2a7547ab permissions -rw-r--r--
removed quotes from consts and syntax 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@806 14 Zorn = OrderArith + AC + Inductive + lcp@516 15 lcp@516 16 consts clasohm@1401 17 Subset_rel :: i=>i clasohm@1401 18 increasing :: i=>i clasohm@1401 19 chain, maxchain :: i=>i clasohm@1401 20 super :: [i,i]=>i lcp@516 21 lcp@753 22 defs lcp@516 23 Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z= & 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 clasohm@1401 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 clasohm@1155 42 nextI "[| x : TFin(S,next); next: increasing(S) clasohm@1155 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