author  berghofe 
Wed, 23 Apr 2003 00:12:14 +0200  
changeset 13916  f078a758e5d8 
parent 13602  4cecd1e0f4a9 
child 14981  e73f8140af78 
permissions  rwrr 
13404  1 
(* Title: HOL/Tools/rewrite_hol_proof.ML 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer, TU Muenchen 

4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

5 

6 
Rewrite rules for HOL proofs 

7 
*) 

8 

9 
signature REWRITE_HOL_PROOF = 

10 
sig 

11 
val rews: (Proofterm.proof * Proofterm.proof) list 

12 
val elim_cong: typ list > Proofterm.proof > Proofterm.proof option 

13 
end; 

14 

15 
structure RewriteHOLProof : REWRITE_HOL_PROOF = 

16 
struct 

17 

18 
open Proofterm; 

19 

20 
val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o 

21 
Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT) 

22 

23 
(** eliminate metaequality rules **) 

24 

25 
["(equal_elim % x1 % x2 %% \ 

26 
\ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \ 

27 
\ (axm.reflexive % TYPE('T3) % x4) %% prf1) %% prf2) == \ 

28 
\ (iffD1 % A % B %% \ 

29 
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)", 

30 

31 
"(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \ 

32 
\ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \ 

33 
\ (axm.reflexive % TYPE('T4) % x6) %% prf1)) %% prf2) == \ 

34 
\ (iffD2 % A % B %% \ 

35 
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)", 

36 

37 
"(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \ 

38 
\ (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) == \ 

39 
\ (cong % TYPE('U) % TYPE('T) % f % g % x % y %% \ 

40 
\ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \ 

41 
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))", 

42 

43 
"(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \ 

44 
\ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \ 

45 
\ (trans % TYPE('T) % x % y % z %% \ 

46 
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \ 

47 
\ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))", 

48 

49 
"(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \ 

50 
\ (refl % TYPE('T) % x)", 

51 

52 
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% \ 

53 
\ (axm.symmetric % TYPE('T) % x % y %% prf)) == \ 

54 
\ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))", 

55 

56 
"(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \ 

57 
\ (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) == \ 

58 
\ (ext % TYPE('U) % TYPE('T) % f % g %% \ 

59 
\ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))", 

60 

61 
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% \ 

62 
\ (eq_reflection % TYPE('T) % x % y %% prf)) == prf", 

63 

64 
"(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ 

65 
\ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \ 

66 
\ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \ 

67 
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \ 

68 
\ (iffD1 % A = C % B = D %% \ 

69 
\ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \ 

70 
\ (cong % TYPE('T=>bool) % TYPE('T) % \ 

71 
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ 

72 
\ (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ 

73 
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ 

74 
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ 

75 
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))", 

76 

77 
"(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ 

78 
\ (axm.symmetric % TYPE('T2) % x5 % x6 %% \ 

79 
\ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \ 

80 
\ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \ 

81 
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \ 

82 
\ (iffD2 % A = C % B = D %% \ 

83 
\ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \ 

84 
\ (cong % TYPE('T=>bool) % TYPE('T) % \ 

85 
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ 

86 
\ (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ 

87 
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ 

88 
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ 

89 
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))", 

90 

91 
(** rewriting on bool: insert proper congruence rules for logical connectives **) 

92 

93 
(* All *) 

94 

95 
"(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ 

96 
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ 

97 
\ (allI % TYPE('a) % Q %% \ 

98 
\ (Lam x. \ 

99 
\ iffD1 % P x % Q x %% (prf % x) %% \ 

100 
\ (spec % TYPE('a) % P % x %% prf')))", 

101 

102 
"(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ 

103 
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ 

104 
\ (allI % TYPE('a) % P %% \ 

105 
\ (Lam x. \ 

106 
\ iffD2 % P x % Q x %% (prf % x) %% \ 

107 
\ (spec % TYPE('a) % ?Q % x %% prf')))", 

108 

109 
(* Ex *) 

110 

111 
"(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \ 

112 
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ 

113 
\ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \ 

114 
\ (Lam x H : P x. \ 

115 
\ exI % TYPE('a) % Q % x %% \ 

116 
\ (iffD1 % P x % Q x %% (prf % x) %% H)))", 

117 

118 
"(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \ 

119 
\ (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ 

120 
\ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \ 

121 
\ (Lam x H : Q x. \ 

122 
\ exI % TYPE('a) % P % x %% \ 

123 
\ (iffD2 % P x % Q x %% (prf % x) %% H)))", 

124 

125 
(* & *) 

126 

127 
"(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ 

128 
\ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \ 

129 
\ (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \ 

130 
\ (conjI % B % D %% \ 

131 
\ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \ 

132 
\ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))", 

133 

134 
"(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ 

135 
\ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \ 

136 
\ (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \ 

137 
\ (conjI % A % C %% \ 

138 
\ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \ 

139 
\ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))", 

140 

13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

141 
"(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

142 
\ (refl % TYPE(bool=>bool) % op & A)) == \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

143 
\ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

144 
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

145 
\ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

146 
\ (refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

147 
\ (refl % TYPE(bool) % A)))", 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

148 

13404  149 
(*  *) 
150 

151 
"(iffD1 % A  C % B  D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ 

152 
\ (cong % TYPE('T3) % TYPE('T4) % op  % op  % A % B %% \ 

153 
\ (refl % TYPE('T5) % op  ) %% prf1) %% prf2) %% prf3) == \ 

154 
\ (disjE % A % C % B  D %% prf3 %% \ 

155 
\ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \ 

156 
\ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))", 

157 

158 
"(iffD2 % A  C % B  D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ 

159 
\ (cong % TYPE('T3) % TYPE('T4) % op  % op  % A % B %% \ 

160 
\ (refl % TYPE('T5) % op  ) %% prf1) %% prf2) %% prf3) == \ 

161 
\ (disjE % B % D % A  C %% prf3 %% \ 

162 
\ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \ 

163 
\ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))", 

164 

13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

165 
"(cong % TYPE(bool) % TYPE(bool) % op  A % op  A % B % C %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

166 
\ (refl % TYPE(bool=>bool) % op  A)) == \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

167 
\ (cong % TYPE(bool) % TYPE(bool) % op  A % op  A % B % C %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

168 
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

169 
\ (op  :: bool=>bool=>bool) % (op  :: bool=>bool=>bool) % A % A %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

170 
\ (refl % TYPE(bool=>bool=>bool) % (op  :: bool=>bool=>bool)) %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

171 
\ (refl % TYPE(bool) % A)))", 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

172 

13404  173 
(* > *) 
174 

175 
"(iffD1 % A > C % B > D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ 

176 
\ (cong % TYPE('T3) % TYPE('T4) % op > % op > % A % B %% \ 

177 
\ (refl % TYPE('T5) % op > ) %% prf1) %% prf2) %% prf3) == \ 

178 
\ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \ 

179 
\ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))", 

180 

181 
"(iffD2 % A > C % B > D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ 

182 
\ (cong % TYPE('T3) % TYPE('T4) % op > % op > % A % B %% \ 

183 
\ (refl % TYPE('T5) % op > ) %% prf1) %% prf2) %% prf3) == \ 

184 
\ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \ 

185 
\ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))", 

186 

13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

187 
"(cong % TYPE(bool) % TYPE(bool) % op > A % op > A % B % C %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

188 
\ (refl % TYPE(bool=>bool) % op > A)) == \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

189 
\ (cong % TYPE(bool) % TYPE(bool) % op > A % op > A % B % C %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

190 
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

191 
\ (op > :: bool=>bool=>bool) % (op > :: bool=>bool=>bool) % A % A %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

192 
\ (refl % TYPE(bool=>bool=>bool) % (op > :: bool=>bool=>bool)) %% \ 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

193 
\ (refl % TYPE(bool) % A)))", 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

194 

13404  195 
(* ~ *) 
196 

197 
"(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \ 

198 
\ (refl % TYPE('T3) % Not) %% prf1) %% prf2) == \ 

199 
\ (notI % Q %% (Lam H: Q. \ 

200 
\ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))", 

201 

202 
"(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \ 

203 
\ (refl % TYPE('T3) % Not) %% prf1) %% prf2) == \ 

204 
\ (notI % P %% (Lam H: P. \ 

205 
\ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))", 

206 

207 
(* = *) 

208 

209 
"(iffD1 % B % D %% \ 

210 
\ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ 

211 
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ 

212 
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ 

213 
\ (iffD1 % C % D %% prf2 %% \ 

214 
\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))", 

215 

216 
"(iffD2 % B % D %% \ 

217 
\ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ 

218 
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ 

219 
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ 

220 
\ (iffD1 % A % B %% prf1 %% \ 

221 
\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))", 

222 

223 
"(iffD1 % A % C %% \ 

224 
\ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ 

225 
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ 

226 
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \ 

227 
\ (iffD2 % C % D %% prf2 %% \ 

228 
\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))", 

229 

230 
"(iffD2 % A % C %% \ 

231 
\ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ 

232 
\ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ 

233 
\ (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ 

234 
\ (iffD2 % A % B %% prf1 %% \ 

235 
\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))", 

236 

237 
"(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \ 

13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

238 
\ (refl % TYPE(bool=>bool) % op = A)) == \ 
13404  239 
\ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \ 
240 
\ (cong % TYPE(bool=>bool) % TYPE(bool) % \ 

241 
\ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \ 

242 
\ (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \ 

13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

243 
\ (refl % TYPE(bool) % A)))", 
13404  244 

13916
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

245 
(** transitivity, reflexivity, and symmetry **) 
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

246 

13404  247 
"(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \ 
248 
\ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))", 

249 

250 
"(iffD2 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \ 

251 
\ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))", 

252 

253 
"(iffD1 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf", 

254 

255 
"(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf", 

256 

13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

257 
"(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)", 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

258 

4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

259 
"(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)", 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

260 

13404  261 
(** normalization of HOL proofs **) 
262 

263 
"(mp % A % B %% (impI % A % B %% prf)) == prf", 

264 

265 
"(impI % A % B %% (mp % A % B %% prf)) == prf", 

266 

267 
"(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x", 

268 

269 
"(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf", 

270 

13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

271 
"(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)", 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

272 

4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

273 
"(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf", 
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

274 

13404  275 
"(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)", 
276 

277 
"(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)", 

278 

279 
"(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1", 

280 

281 
"(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2", 

282 

283 
"(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1", 

284 

285 
"(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"]; 

286 

287 

288 
(** Replace congruence rules by substitution rules **) 

289 

290 
fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % Some x % Some y %% 

291 
prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1 

292 
 strip_cong ps (PThm (("HOL.refl", _), _, _, _) % Some f) = Some (f, ps) 

293 
 strip_cong _ _ = None; 

294 

295 
val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst)))); 

296 
val sym_prf = fst (strip_combt (#2 (#der (rep_thm sym)))); 

297 

298 
fun make_subst Ts prf xs (_, []) = prf 

299 
 make_subst Ts prf xs (f, ((x, y), prf') :: ps) = 

300 
let val T = fastype_of1 (Ts, x) 

301 
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps) 

302 
else change_type (Some [T]) subst_prf %> x %> y %> 

303 
Abs ("z", T, list_comb (incr_boundvars 1 f, 

304 
map (incr_boundvars 1) xs @ Bound 0 :: 

305 
map (incr_boundvars 1 o snd o fst) ps)) %% prf' %% 

306 
make_subst Ts prf (xs @ [x]) (f, ps) 

307 
end; 

308 

309 
fun make_sym Ts ((x, y), prf) = 

310 
((y, x), change_type (Some [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf); 

311 

13916
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

312 
fun mk_AbsP P t = AbsP ("H", P, t); 
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

313 

13404  314 
fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) = 
315 
apsome (make_subst Ts prf2 []) (strip_cong [] prf1) 

13916
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

316 
 elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % P % _ %% prf) = 
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

317 
apsome (mk_AbsP P o make_subst Ts (PBound 0) []) 
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

318 
(strip_cong [] (incr_pboundvars 1 0 prf)) 
13404  319 
 elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) = 
320 
apsome (make_subst Ts prf2 [] o 

321 
apsnd (map (make_sym Ts))) (strip_cong [] prf1) 

13916
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

322 
 elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % P %% prf) = 
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

323 
apsome (mk_AbsP P o make_subst Ts (PBound 0) [] o 
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

324 
apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf)) 
13404  325 
 elim_cong _ _ = None; 
326 

327 
end; 