author  wenzelm 
Wed, 05 Dec 2001 03:07:44 +0100  
changeset 12372  cd3a09c7dac9 
parent 11460  e5fb885bfe3a 
child 12459  6978ab7cac64 
permissions  rwrr 
11453
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

1 
(* Title: HOL/Hilbert_Choice_lemmas 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

2 
ID: $Id$ 
11453
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

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

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

5 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

6 
Lemmas for Hilbert's epsilonoperator and the Axiom of Choice 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

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

8 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

9 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

10 
(* ML bindings *) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

11 
val someI = thm "someI"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

12 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

13 
section "SOME: Hilbert's Epsilonoperator"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

14 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

15 
(*Easier to apply than someI if witness ?a comes from an EXformula*) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

16 
Goal "EX x. P x ==> P (SOME x. P x)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

17 
by (etac exE 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

18 
by (etac someI 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

19 
qed "someI_ex"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

20 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

21 
(*Easier to apply than someI: conclusion has only one occurrence of P*) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

22 
val prems = Goal "[ P a; !!x. P x ==> Q x ] ==> Q (SOME x. P x)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

23 
by (resolve_tac prems 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

24 
by (rtac someI 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

25 
by (resolve_tac prems 1) ; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

26 
qed "someI2"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

27 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

28 
(*Easier to apply than someI2 if witness ?a comes from an EXformula*) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

29 
val [major,minor] = Goal "[ EX a. P a; !!x. P x ==> Q x ] ==> Q (SOME x. P x)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

30 
by (rtac (major RS exE) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

31 
by (etac someI2 1 THEN etac minor 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

32 
qed "someI2_ex"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

33 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

34 
val prems = Goal "[ P a; !!x. P x ==> x=a ] ==> (SOME x. P x) = a"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

35 
by (rtac someI2 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

36 
by (REPEAT (ares_tac prems 1)) ; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

37 
qed "some_equality"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

38 
AddIs [some_equality]; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

39 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

40 
Goal "[ EX!x. P x; P a ] ==> (SOME x. P x) = a"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

41 
by (rtac some_equality 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

42 
by (atac 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

43 
by (etac ex1E 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

44 
by (etac all_dupE 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

45 
by (dtac mp 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

46 
by (atac 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

47 
by (etac ssubst 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

48 
by (etac allE 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

49 
by (etac mp 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

50 
by (atac 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

51 
qed "some1_equality"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

52 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

53 
Goal "P (SOME x. P x) = (EX x. P x)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

54 
by (rtac iffI 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

55 
by (etac exI 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

56 
by (etac exE 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

57 
by (etac someI 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

58 
qed "some_eq_ex"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

59 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

60 
Goal "(SOME y. y=x) = x"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

61 
by (rtac some_equality 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

62 
by (rtac refl 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

63 
by (atac 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

64 
qed "some_eq_trivial"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

65 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

66 
Goal "(SOME y. x=y) = x"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

67 
by (rtac some_equality 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

68 
by (rtac refl 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

69 
by (etac sym 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

70 
qed "some_sym_eq_trivial"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

71 
Addsimps [some_eq_trivial, some_sym_eq_trivial]; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

72 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

73 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

74 
(** "Axiom" of Choice, proved using the description operator **) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

75 

11460  76 
(*Used in Tools/meson.ML*) 
77 
Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"; 

78 
by (fast_tac (claset() addEs [someI]) 1); 

79 
qed "choice"; 

11453
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

80 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

81 
Goal "ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

82 
by (fast_tac (claset() addEs [someI]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

83 
qed "bchoice"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

84 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

85 

11460  86 
section "Function Inverse"; 
11453
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

87 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

88 
val inv_def = thm "inv_def"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

89 
val Inv_def = thm "Inv_def"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

90 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

91 
Goal "inv id = id"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

92 
by (simp_tac (simpset() addsimps [inv_def,id_def]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

93 
qed "inv_id"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

94 
Addsimps [inv_id]; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

95 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

96 
(*A onetoone function has an inverse.*) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

97 
Goalw [inv_def] "inj(f) ==> inv f (f x) = x"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

98 
by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

99 
qed "inv_f_f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

100 
Addsimps [inv_f_f]; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

101 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

102 
Goal "[ inj(f); f x = y ] ==> inv f y = x"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

103 
by (etac subst 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

104 
by (etac inv_f_f 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

105 
qed "inv_f_eq"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

106 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

107 
Goal "[ inj f; ALL x. f(g x) = x ] ==> inv f = g"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

108 
by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

109 
qed "inj_imp_inv_eq"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

110 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

111 
(* Useful??? *) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

112 
val [oneone,minor] = Goal 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

113 
"[ inj(f); !!y. y: range(f) ==> P(inv f y) ] ==> P(x)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

114 
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

115 
by (rtac (rangeI RS minor) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

116 
qed "inj_transfer"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

117 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

118 
Goal "(inj f) = (inv f o f = id)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

119 
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

120 
by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

121 
qed "inj_iff"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

122 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

123 
Goal "inj f ==> surj (inv f)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

124 
by (blast_tac (claset() addIs [surjI, inv_f_f]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

125 
qed "inj_imp_surj_inv"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

126 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

127 
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

128 
by (fast_tac (claset() addIs [someI]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

129 
qed "f_inv_f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

130 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

131 
Goal "surj f ==> f(inv f y) = y"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

132 
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

133 
qed "surj_f_inv_f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

134 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

135 
Goal "[ inv f x = inv f y; x: range(f); y: range(f) ] ==> x=y"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

136 
by (rtac (arg_cong RS box_equals) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

137 
by (REPEAT (ares_tac [f_inv_f] 1)); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

138 
qed "inv_injective"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

139 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

140 
Goal "A <= range(f) ==> inj_on (inv f) A"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

141 
by (fast_tac (claset() addIs [inj_onI] 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

142 
addEs [inv_injective, injD]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

143 
qed "inj_on_inv"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

144 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

145 
Goal "surj f ==> inj (inv f)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

146 
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

147 
qed "surj_imp_inj_inv"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

148 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

149 
Goal "(surj f) = (f o inv f = id)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

150 
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

151 
by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

152 
qed "surj_iff"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

153 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

154 
Goal "[ surj f; ALL x. g(f x) = x ] ==> inv f = g"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

155 
by (rtac ext 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

156 
by (dres_inst_tac [("x","inv f x")] spec 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

157 
by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

158 
qed "surj_imp_inv_eq"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

159 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

160 
Goalw [bij_def] "bij f ==> bij (inv f)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

161 
by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

162 
qed "bij_imp_bij_inv"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

163 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

164 
val prems = 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

165 
Goalw [inv_def] "[ !! x. g (f x) = x; !! y. f (g y) = y ] ==> inv f = g"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

166 
by (rtac ext 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

167 
by (auto_tac (claset(), simpset() addsimps prems)); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

168 
qed "inv_equality"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

169 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

170 
Goalw [bij_def] "bij f ==> inv (inv f) = f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

171 
by (rtac inv_equality 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

172 
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f])); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

173 
qed "inv_inv_eq"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

174 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

175 
(** bij(inv f) implies little about f. Consider f::bool=>bool such that 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

176 
f(True)=f(False)=True. Then it's consistent with axiom someI that 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

177 
inv(f) could be any function at all, including the identity function. 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

178 
If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

179 
inv(inv(f))=f all fail. 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

180 
**) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

181 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

182 
Goalw [bij_def] "[ bij f; bij g ] ==> inv (f o g) = inv g o inv f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

183 
by (rtac (inv_equality) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

184 
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f])); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

185 
qed "o_inv_distrib"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

186 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

187 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

188 
Goal "surj f ==> f ` (inv f ` A) = A"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

189 
by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

190 
qed "image_surj_f_inv_f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

191 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

192 
Goal "inj f ==> (inv f) ` (f ` A) = A"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

193 
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

194 
qed "image_inv_f_f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

195 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

196 
Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

197 
by Auto_tac; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

198 
qed "inv_image_comp"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

199 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

200 
Goal "bij f ==> f ` Collect P = {y. P (inv f y)}"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

201 
by Auto_tac; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

202 
by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

203 
by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

204 
qed "bij_image_Collect_eq"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

205 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

206 
Goal "bij f ==> f ` A = inv f ` A"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

207 
by Safe_tac; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

208 
by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

209 
by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

210 
qed "bij_vimage_eq_inv_image"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

211 

11460  212 

213 
section "Inverse of a PIfunction (restricted domain)"; 

11453
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

214 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

215 
Goalw [Inv_def] "f ` A = B ==> (lam x: B. (Inv A f) x) : B funcset A"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

216 
by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

217 
qed "Inv_funcset"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

218 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

219 
Goal "[ inj_on f A; x : A ] ==> Inv A f (f x) = x"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

220 
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

221 
by (blast_tac (claset() addIs [someI2]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

222 
qed "Inv_f_f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

223 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

224 
Goal "y : f`A ==> f (Inv A f y) = y"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

225 
by (asm_simp_tac (simpset() addsimps [Inv_def]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

226 
by (fast_tac (claset() addIs [someI2]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

227 
qed "f_Inv_f"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

228 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

229 
Goal "[ Inv A f x = Inv A f y; x : f`A; y : f`A ] ==> x=y"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

230 
by (rtac (arg_cong RS box_equals) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

231 
by (REPEAT (ares_tac [f_Inv_f] 1)); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

232 
qed "Inv_injective"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

233 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

234 
Goal "B <= f`A ==> inj_on (Inv A f) B"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

235 
by (rtac inj_onI 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

236 
by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

237 
qed "inj_on_Inv"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

238 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

239 
Goal "[ inj_on f A; f ` A = B ] \ 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

240 
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

241 
by (asm_simp_tac (simpset() addsimps [compose_def]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

242 
by (rtac restrict_ext 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

243 
by Auto_tac; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

244 
by (etac subst 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

245 
by (asm_full_simp_tac (simpset() addsimps [Inv_f_f]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

246 
qed "compose_Inv_id"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

247 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

248 

11460  249 

250 
section "split and SOME"; 

11453
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

251 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

252 
(*Can't be added to simpset: loops!*) 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

253 
Goal "(SOME x. P x) = (SOME (a,b). P(a,b))"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

254 
by (simp_tac (simpset() addsimps [split_Pair_apply]) 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

255 
qed "split_paired_Eps"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

256 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

257 
Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

258 
by (rtac refl 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

259 
qed "Eps_split"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

260 

1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

261 
Goal "(@(x',y'). x = x' & y = y') = (x,y)"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

262 
by (Blast_tac 1); 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

263 
qed "Eps_split_eq"; 
1b15f655da2c
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
diff
changeset

264 
Addsimps [Eps_split_eq]; 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

265 

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

266 

11460  267 
section "A relation is wellfounded iff it has no infinite descending chain"; 
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

268 

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

269 
Goalw [wf_eq_minimal RS eq_reflection] 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

270 
"wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))"; 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

271 
by (rtac iffI 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

272 
by (rtac notI 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

273 
by (etac exE 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

274 
by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

275 
by (Blast_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

276 
by (etac contrapos_np 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

277 
by (Asm_full_simp_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

278 
by (Clarify_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

279 
by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

280 
by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

281 
by (rtac allI 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

282 
by (Simp_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

283 
by (rtac someI2_ex 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

284 
by (Blast_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

285 
by (Blast_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

286 
by (rtac allI 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

287 
by (induct_tac "n" 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

288 
by (Asm_simp_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

289 
by (Simp_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

290 
by (rtac someI2_ex 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

291 
by (Blast_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

292 
by (Blast_tac 1); 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

293 
qed "wf_iff_no_infinite_down_chain"; 
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11453
diff
changeset

294 