author  lcp 
Thu, 25 Aug 1994 12:09:21 +0200  
changeset 578  efc648d29dd0 
parent 516  1957113f0d7d 
child 753  ec86863e87c8 
permissions  rwrr 
516  1 
(* Title: ZF/Zorn.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1994 University of Cambridge 

5 

6 
Based upon the article 

7 
Abrial & Laffitte, 

8 
Towards the Mechanization of the Proofs of Some 

9 
Classical Theorems of Set Theory. 

10 

11 
Union_in_Pow is proved in ZF.ML 

12 
*) 

13 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
516
diff
changeset

14 
Zorn = OrderArith + AC + "Inductive" + 
516  15 

16 
consts 

17 
Subset_rel :: "i=>i" 

18 
increasing :: "i=>i" 

19 
chain, maxchain :: "i=>i" 

20 
super :: "[i,i]=>i" 

21 

22 
rules 

23 
Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}" 

24 
increasing_def "increasing(A) == {f: Pow(A)>Pow(A). ALL x. x<=A > x<=f`x}" 

485  25 

516  26 
chain_def "chain(A) == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y  Y<=X}" 
27 
super_def "super(A,c) == {d: chain(A). c<=d & c~=d}" 

28 
maxchain_def "maxchain(A) == {c: chain(A). super(A,c)=0}" 

29 

30 

31 
(** We could make the inductive definition conditional on next: increasing(S) 

32 
but instead we make this a sidecondition of an introduction rule. Thus 

33 
the induction rule lets us assume that condition! Many inductive proofs 

34 
are therefore unconditional. 

35 
**) 

36 
consts 

37 
"TFin" :: "[i,i]=>i" 

38 

39 
inductive 

40 
domains "TFin(S,next)" <= "Pow(S)" 

41 
intrs 

42 
nextI "[ x : TFin(S,next); next: increasing(S) \ 

43 
\ ] ==> next`x : TFin(S,next)" 

44 

45 
Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)" 

46 

47 
monos "[Pow_mono]" 

48 
con_defs "[increasing_def]" 

49 
type_intrs "[CollectD1 RS apply_funtype, Union_in_Pow]" 

50 

51 
end 