author  paulson 
Wed, 25 Jul 2001 17:58:26 +0200  
changeset 11454  7514e5e21cb8 
parent 11451  8abfb4f7bd02 
child 11506  244a02a2968b 
permissions  rwrr 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

1 
(* Title: HOL/Hilbert_Choice.thy 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

2 
ID: $Id$ 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

4 
Copyright 2001 University of Cambridge 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

5 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

6 
Hilbert's epsilonoperator and everything to do with the Axiom of Choice 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

7 
*) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

8 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

9 
theory Hilbert_Choice = NatArith 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

10 
files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"): 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

11 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

12 
consts 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

13 
Eps :: "('a => bool) => 'a" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

14 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

15 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

16 
syntax (input) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

17 
"_Eps" :: "[pttrn, bool] => 'a" ("(3\\<epsilon>_./ _)" [0, 10] 10) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

18 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

19 
syntax (HOL) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

20 
"_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

21 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

22 
syntax 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

23 
"_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

24 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

25 
translations 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

26 
"SOME x. P" == "Eps (%x. P)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

27 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

28 
axioms 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

29 
someI: "P (x::'a) ==> P (SOME x. P x)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

30 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

31 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

32 
(*used in TFL*) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

33 
lemma tfl_some: "\\<forall>P x. P x > P (Eps P)" 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

34 
by (blast intro: someI) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

35 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

36 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

37 
constdefs 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

38 
inv :: "('a => 'b) => ('b => 'a)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

39 
"inv(f::'a=>'b) == % y. @x. f(x)=y" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

40 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

41 
Inv :: "['a set, 'a => 'b] => ('b => 'a)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

42 
"Inv A f == (% x. (@ y. y : A & f y = x))" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

43 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

44 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

45 
use "Hilbert_Choice_lemmas.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

46 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

47 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

48 
(** Least value operator **) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

49 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

50 
constdefs 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

51 
LeastM :: "['a => 'b::ord, 'a => bool] => 'a" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

52 
"LeastM m P == @x. P x & (ALL y. P y > m x <= m y)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

53 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

54 
syntax 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

55 
"@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

56 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

57 
translations 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

58 
"LEAST x WRT m. P" == "LeastM m (%x. P)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

59 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

60 
lemma LeastMI2: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

61 
"[ P x; !!y. P y ==> m x <= m y; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

62 
!!x. [ P x; \\<forall>y. P y > m x \\<le> m y ] ==> Q x ] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

63 
==> Q (LeastM m P)"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

64 
apply (unfold LeastM_def) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

65 
apply (rule someI2_ex) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

66 
apply blast 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

67 
apply blast 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

68 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

69 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

70 
lemma LeastM_equality: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

71 
"[ P k; !!x. P x ==> m k <= m x ] ==> m (LEAST x WRT m. P x) = 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

72 
(m k::'a::order)"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

73 
apply (rule LeastMI2) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

74 
apply assumption 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

75 
apply blast 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

76 
apply (blast intro!: order_antisym) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

77 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

78 

11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

79 
lemma wf_linord_ex_has_least: 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

80 
"[wf r; ALL x y. ((x,y):r^+) = ((y,x)~:r^*); P k] \ 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

81 
\ ==> EX x. P x & (!y. P y > (m x,m y):r^*)" 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

82 
apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

83 
apply (drule_tac x = "m`Collect P" in spec) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

84 
apply force 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

85 
done 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

86 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

87 
(* successor of obsolete nonempty_has_least *) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

88 
lemma ex_has_least_nat: 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

89 
"P k ==> EX x. P x & (ALL y. P y > m x <= (m y::nat))" 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

90 
apply (simp only: pred_nat_trancl_eq_le [symmetric]) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

91 
apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

92 
apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

93 
apply assumption 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

94 
done 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

95 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

96 
lemma LeastM_nat_lemma: 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

97 
"P k ==> P (LeastM m P) & (ALL y. P y > m (LeastM m P) <= (m y::nat))" 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

98 
apply (unfold LeastM_def) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

99 
apply (rule someI_ex) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

100 
apply (erule ex_has_least_nat) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

101 
done 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

102 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

103 
lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard] 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

104 

7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

105 
lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)" 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

106 
apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

107 
apply assumption 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

108 
apply assumption 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

109 
done 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset

110 

11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

111 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

112 
(** Greatest value operator **) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

113 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

114 
constdefs 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

115 
GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

116 
"GreatestM m P == @x. P x & (ALL y. P y > m y <= m x)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

117 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

118 
Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

119 
"Greatest == GreatestM (%x. x)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

120 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

121 
syntax 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

122 
"@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

123 
("GREATEST _ WRT _. _" [0,4,10]10) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

124 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

125 
translations 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

126 
"GREATEST x WRT m. P" == "GreatestM m (%x. P)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

127 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

128 
lemma GreatestMI2: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

129 
"[ P x; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

130 
!!y. P y ==> m y <= m x; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

131 
!!x. [ P x; \\<forall>y. P y > m y \\<le> m x ] ==> Q x ] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

132 
==> Q (GreatestM m P)"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

133 
apply (unfold GreatestM_def) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

134 
apply (rule someI2_ex) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

135 
apply blast 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

136 
apply blast 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

137 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

138 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

139 
lemma GreatestM_equality: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

140 
"[ P k; !!x. P x ==> m x <= m k ] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

141 
==> m (GREATEST x WRT m. P x) = (m k::'a::order)"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

142 
apply (rule_tac m=m in GreatestMI2) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

143 
apply assumption 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

144 
apply blast 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

145 
apply (blast intro!: order_antisym) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

146 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

147 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

148 
lemma Greatest_equality: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

149 
"[ P (k::'a::order); !!x. P x ==> x <= k ] ==> (GREATEST x. P x) = k"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

150 
apply (unfold Greatest_def) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

151 
apply (erule GreatestM_equality) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

152 
apply blast 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

153 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

154 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

155 
lemma ex_has_greatest_nat_lemma: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

156 
"[P k; ALL x. P x > (EX y. P y & ~ ((m y::nat) <= m x))] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

157 
==> EX y. P y & ~ (m y < m k + n)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

158 
apply (induct_tac "n") 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

159 
apply force 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

160 
(*ind step*) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

161 
apply (force simp add: le_Suc_eq) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

162 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

163 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

164 
lemma ex_has_greatest_nat: "[P k; ! y. P y > m y < b] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

165 
==> ? x. P x & (! y. P y > (m y::nat) <= m x)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

166 
apply (rule ccontr) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

167 
apply (cut_tac P = "P" and n = "b  m k" in ex_has_greatest_nat_lemma) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

168 
apply (subgoal_tac [3] "m k <= b") 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

169 
apply auto 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

170 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

171 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

172 
lemma GreatestM_nat_lemma: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

173 
"[P k; ! y. P y > m y < b] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

174 
==> P (GreatestM m P) & (!y. P y > (m y::nat) <= m (GreatestM m P))" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

175 
apply (unfold GreatestM_def) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

176 
apply (rule someI_ex) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

177 
apply (erule ex_has_greatest_nat) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

178 
apply assumption 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

179 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

180 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

181 
lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

182 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

183 
lemma GreatestM_nat_le: "[P x; ! y. P y > m y < b] 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

184 
==> (m x::nat) <= m (GreatestM m P)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

185 
apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

186 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

187 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

188 
(** Specialization to GREATEST **) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

189 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

190 
lemma GreatestI: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

191 
"[P (k::nat); ! y. P y > y < b] ==> P (GREATEST x. P x)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

192 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

193 
apply (unfold Greatest_def) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

194 
apply (rule GreatestM_natI) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

195 
apply auto 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

196 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

197 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

198 
lemma Greatest_le: 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

199 
"[P x; ! y. P y > y < b] ==> (x::nat) <= (GREATEST x. P x)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

200 
apply (unfold Greatest_def) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

201 
apply (rule GreatestM_nat_le) 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

202 
apply auto 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

203 
done 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

204 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

205 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

206 
ML {* 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

207 
val LeastMI2 = thm "LeastMI2"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

208 
val LeastM_equality = thm "LeastM_equality"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

209 
val GreatestM_def = thm "GreatestM_def"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

210 
val GreatestMI2 = thm "GreatestMI2"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

211 
val GreatestM_equality = thm "GreatestM_equality"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

212 
val Greatest_def = thm "Greatest_def"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

213 
val Greatest_equality = thm "Greatest_equality"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

214 
val GreatestM_natI = thm "GreatestM_natI"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

215 
val GreatestM_nat_le = thm "GreatestM_nat_le"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

216 
val GreatestI = thm "GreatestI"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

217 
val Greatest_le = thm "Greatest_le"; 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

218 
*} 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

219 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

220 
use "meson_lemmas.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

221 
use "Tools/meson.ML" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

222 
setup meson_setup 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

223 

8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

224 
end 