0
+ − 1
theory QuotMain
6
+ − 2
imports QuotScript QuotList Prove
264
+ − 3
uses ("quotient_info.ML")
+ − 4
("quotient.ML")
277
+ − 5
("quotient_def.ML")
0
+ − 6
begin
+ − 7
+ − 8
locale QUOT_TYPE =
+ − 9
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ − 10
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ − 11
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ − 12
assumes equiv: "EQUIV R"
+ − 13
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ − 14
and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ − 15
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ − 16
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
15
+ − 17
begin
0
+ − 18
+ − 19
definition
200
+ − 20
ABS::"'a \<Rightarrow> 'b"
+ − 21
where
0
+ − 22
"ABS x \<equiv> Abs (R x)"
+ − 23
+ − 24
definition
200
+ − 25
REP::"'b \<Rightarrow> 'a"
+ − 26
where
0
+ − 27
"REP a = Eps (Rep a)"
+ − 28
15
+ − 29
lemma lem9:
0
+ − 30
shows "R (Eps (R x)) = R x"
+ − 31
proof -
+ − 32
have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
+ − 33
then have "R x (Eps (R x))" by (rule someI)
15
+ − 34
then show "R (Eps (R x)) = R x"
0
+ − 35
using equiv unfolding EQUIV_def by simp
+ − 36
qed
+ − 37
+ − 38
theorem thm10:
24
+ − 39
shows "ABS (REP a) \<equiv> a"
+ − 40
apply (rule eq_reflection)
+ − 41
unfolding ABS_def REP_def
0
+ − 42
proof -
15
+ − 43
from rep_prop
0
+ − 44
obtain x where eq: "Rep a = R x" by auto
+ − 45
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ − 46
also have "\<dots> = Abs (R x)" using lem9 by simp
+ − 47
also have "\<dots> = Abs (Rep a)" using eq by simp
+ − 48
also have "\<dots> = a" using rep_inverse by simp
+ − 49
finally
+ − 50
show "Abs (R (Eps (Rep a))) = a" by simp
+ − 51
qed
+ − 52
15
+ − 53
lemma REP_refl:
0
+ − 54
shows "R (REP a) (REP a)"
+ − 55
unfolding REP_def
+ − 56
by (simp add: equiv[simplified EQUIV_def])
+ − 57
+ − 58
lemma lem7:
22
+ − 59
shows "(R x = R y) = (Abs (R x) = Abs (R y))"
0
+ − 60
apply(rule iffI)
+ − 61
apply(simp)
+ − 62
apply(drule rep_inject[THEN iffD2])
+ − 63
apply(simp add: abs_inverse)
+ − 64
done
15
+ − 65
0
+ − 66
theorem thm11:
+ − 67
shows "R r r' = (ABS r = ABS r')"
+ − 68
unfolding ABS_def
+ − 69
by (simp only: equiv[simplified EQUIV_def] lem7)
+ − 70
4
+ − 71
2
+ − 72
lemma REP_ABS_rsp:
4
+ − 73
shows "R f (REP (ABS g)) = R f g"
+ − 74
and "R (REP (ABS g)) f = R g f"
23
+ − 75
by (simp_all add: thm10 thm11)
4
+ − 76
0
+ − 77
lemma QUOTIENT:
+ − 78
"QUOTIENT R ABS REP"
+ − 79
apply(unfold QUOTIENT_def)
+ − 80
apply(simp add: thm10)
+ − 81
apply(simp add: REP_refl)
+ − 82
apply(subst thm11[symmetric])
+ − 83
apply(simp add: equiv[simplified EQUIV_def])
+ − 84
done
+ − 85
21
+ − 86
lemma R_trans:
49
+ − 87
assumes ab: "R a b"
+ − 88
and bc: "R b c"
22
+ − 89
shows "R a c"
21
+ − 90
proof -
+ − 91
have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ − 92
moreover have ab: "R a b" by fact
+ − 93
moreover have bc: "R b c" by fact
22
+ − 94
ultimately show "R a c" unfolding TRANS_def by blast
21
+ − 95
qed
+ − 96
+ − 97
lemma R_sym:
49
+ − 98
assumes ab: "R a b"
22
+ − 99
shows "R b a"
21
+ − 100
proof -
+ − 101
have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
22
+ − 102
then show "R b a" using ab unfolding SYM_def by blast
21
+ − 103
qed
+ − 104
49
+ − 105
lemma R_trans2:
+ − 106
assumes ac: "R a c"
22
+ − 107
and bd: "R b d"
21
+ − 108
shows "R a b = R c d"
200
+ − 109
using ac bd
+ − 110
by (blast intro: R_trans R_sym)
21
+ − 111
+ − 112
lemma REPS_same:
25
+ − 113
shows "R (REP a) (REP b) \<equiv> (a = b)"
38
+ − 114
proof -
+ − 115
have "R (REP a) (REP b) = (a = b)"
+ − 116
proof
+ − 117
assume as: "R (REP a) (REP b)"
+ − 118
from rep_prop
+ − 119
obtain x y
+ − 120
where eqs: "Rep a = R x" "Rep b = R y" by blast
+ − 121
from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+ − 122
then have "R x (Eps (R y))" using lem9 by simp
+ − 123
then have "R (Eps (R y)) x" using R_sym by blast
+ − 124
then have "R y x" using lem9 by simp
+ − 125
then have "R x y" using R_sym by blast
+ − 126
then have "ABS x = ABS y" using thm11 by simp
+ − 127
then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+ − 128
then show "a = b" using rep_inverse by simp
+ − 129
next
+ − 130
assume ab: "a = b"
+ − 131
have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ − 132
then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+ − 133
qed
+ − 134
then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
21
+ − 135
qed
+ − 136
0
+ − 137
end
+ − 138
127
b054cf6bd179
the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
0
+ − 140
section {* type definition for the quotient type *}
+ − 141
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
(* the auxiliary data for the quotient types *)
264
+ − 143
use "quotient_info.ML"
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
185
+ − 145
declare [[map list = (map, LIST_REL)]]
+ − 146
declare [[map * = (prod_fun, prod_rel)]]
+ − 147
declare [[map "fun" = (fun_map, FUN_REL)]]
+ − 148
+ − 149
ML {* maps_lookup @{theory} "List.list" *}
+ − 150
ML {* maps_lookup @{theory} "*" *}
+ − 151
ML {* maps_lookup @{theory} "fun" *}
174
+ − 152
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
(* definition of the quotient types *)
277
+ − 155
(* FIXME: should be called quotient_typ.ML *)
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156
use "quotient.ML"
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 157
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 158
277
+ − 159
(* lifting of constants *)
+ − 160
use "quotient_def.ML"
+ − 161
+ − 162
218
+ − 163
text {* FIXME: auxiliary function *}
193
+ − 164
ML {*
14
+ − 165
val no_vars = Thm.rule_attribute (fn context => fn th =>
+ − 166
let
+ − 167
val ctxt = Variable.set_body false (Context.proof_of context);
+ − 168
val ((_, [th']), _) = Variable.import true [th] ctxt;
+ − 169
in th' end);
+ − 170
*}
+ − 171
139
+ − 172
section {* ATOMIZE *}
+ − 173
+ − 174
text {*
+ − 175
Unabs_def converts a definition given as
+ − 176
+ − 177
c \<equiv> %x. %y. f x y
+ − 178
+ − 179
to a theorem of the form
+ − 180
+ − 181
c x y \<equiv> f x y
+ − 182
+ − 183
This function is needed to rewrite the right-hand
+ − 184
side to the left-hand side.
+ − 185
*}
+ − 186
+ − 187
ML {*
+ − 188
fun unabs_def ctxt def =
+ − 189
let
+ − 190
val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+ − 191
val xs = strip_abs_vars (term_of rhs)
+ − 192
val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
+ − 193
+ − 194
val thy = ProofContext.theory_of ctxt'
+ − 195
val cxs = map (cterm_of thy o Free) xs
+ − 196
val new_lhs = Drule.list_comb (lhs, cxs)
+ − 197
+ − 198
fun get_conv [] = Conv.rewr_conv def
+ − 199
| get_conv (x::xs) = Conv.fun_conv (get_conv xs)
+ − 200
in
+ − 201
get_conv xs new_lhs |>
+ − 202
singleton (ProofContext.export ctxt' ctxt)
+ − 203
end
+ − 204
*}
+ − 205
+ − 206
lemma atomize_eqv[atomize]:
+ − 207
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+ − 208
proof
+ − 209
assume "A \<equiv> B"
+ − 210
then show "Trueprop A \<equiv> Trueprop B" by unfold
+ − 211
next
+ − 212
assume *: "Trueprop A \<equiv> Trueprop B"
+ − 213
have "A = B"
+ − 214
proof (cases A)
+ − 215
case True
+ − 216
have "A" by fact
+ − 217
then show "A = B" using * by simp
+ − 218
next
+ − 219
case False
+ − 220
have "\<not>A" by fact
+ − 221
then show "A = B" using * by auto
+ − 222
qed
+ − 223
then show "A \<equiv> B" by (rule eq_reflection)
+ − 224
qed
+ − 225
+ − 226
ML {*
+ − 227
fun atomize_thm thm =
+ − 228
let
221
+ − 229
val thm' = Thm.freezeT (forall_intr_vars thm)
139
+ − 230
val thm'' = ObjectLogic.atomize (cprop_of thm')
+ − 231
in
221
+ − 232
@{thm Pure.equal_elim_rule1} OF [thm'', thm']
139
+ − 233
end
+ − 234
*}
+ − 235
140
+ − 236
ML {* atomize_thm @{thm list.induct} *}
139
+ − 237
+ − 238
section {* REGULARIZE *}
282
+ − 239
(*
+ − 240
+ − 241
Regularizing a theorem means:
+ − 242
- Quantifiers over a type that needs lifting are replaced by
+ − 243
bounded quantifiers, for example:
+ − 244
\<forall>x. P \<Longrightarrow> \<forall>x\<in>(Respects R). P
+ − 245
- Abstractions over a type that needs lifting are replaced
+ − 246
by bounded abstactions:
+ − 247
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+ − 248
+ − 249
- Equalities over the type being lifted are replaced by
+ − 250
appropriate relations:
+ − 251
A = B \<Longrightarrow> A \<approx> B
+ − 252
Example with more complicated types of A, B:
+ − 253
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+ − 254
+ − 255
Regularizing is done in 3 phases:
+ − 256
- First a regularized term is created
+ − 257
- Next we prove that the original theorem implies the new one
+ − 258
- Finally using MP we get the new theorem.
+ − 259
+ − 260
To prove that the old theorem implies the new one, we first
+ − 261
atomize it and then try:
+ − 262
- Reflexivity of the relation
+ − 263
- Assumption
+ − 264
- Elimnating quantifiers on both sides of toplevel implication
+ − 265
- Simplifying implications on both sides of toplevel implication
+ − 266
- Ball (Respects ?E) ?P = All ?P
+ − 267
- (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+ − 268
+ − 269
*)
139
+ − 270
+ − 271
text {* tyRel takes a type and builds a relation that a quantifier over this
+ − 272
type needs to respect. *}
+ − 273
ML {*
257
+ − 274
fun matches (ty1, ty2) =
+ − 275
Type.raw_instance (ty1, Logic.varifyT ty2);
+ − 276
139
+ − 277
fun tyRel ty rty rel lthy =
257
+ − 278
if matches (rty, ty)
139
+ − 279
then rel
+ − 280
else (case ty of
+ − 281
Type (s, tys) =>
+ − 282
let
+ − 283
val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
+ − 284
val ty_out = ty --> ty --> @{typ bool};
+ − 285
val tys_out = tys_rel ---> ty_out;
+ − 286
in
+ − 287
(case (maps_lookup (ProofContext.theory_of lthy) s) of
+ − 288
SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+ − 289
| NONE => HOLogic.eq_const ty
+ − 290
)
+ − 291
end
+ − 292
| _ => HOLogic.eq_const ty)
+ − 293
*}
+ − 294
+ − 295
definition
+ − 296
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ − 297
where
+ − 298
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+ − 299
(* TODO: Consider defining it with an "if"; sth like:
+ − 300
Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+ − 301
*)
+ − 302
+ − 303
ML {*
+ − 304
fun needs_lift (rty as Type (rty_s, _)) ty =
+ − 305
case ty of
+ − 306
Type (s, tys) =>
+ − 307
(s = rty_s) orelse (exists (needs_lift rty) tys)
+ − 308
| _ => false
+ − 309
+ − 310
*}
+ − 311
+ − 312
ML {*
+ − 313
fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
+ − 314
fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
+ − 315
fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
+ − 316
fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
+ − 317
*}
+ − 318
+ − 319
(* applies f to the subterm of an abstractions, otherwise to the given term *)
+ − 320
ML {*
+ − 321
fun apply_subt f trm =
+ − 322
case trm of
145
+ − 323
Abs (x, T, t) =>
+ − 324
let
+ − 325
val (x', t') = Term.dest_abs (x, T, t)
+ − 326
in
+ − 327
Term.absfree (x', T, f t')
+ − 328
end
139
+ − 329
| _ => f trm
+ − 330
*}
+ − 331
+ − 332
(* FIXME: if there are more than one quotient, then you have to look up the relation *)
+ − 333
ML {*
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 334
fun my_reg lthy rel rty trm =
139
+ − 335
case trm of
+ − 336
Abs (x, T, t) =>
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 337
if (needs_lift rty T) then
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 338
let
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 339
val rrel = tyRel T rty rel lthy
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 340
in
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 341
(mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 342
end
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 343
else
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 344
Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 345
| Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346
let
139
+ − 347
val ty1 = domain_type ty
+ − 348
val ty2 = domain_type ty1
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 349
val rrel = tyRel T rty rel lthy
139
+ − 350
in
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 351
if (needs_lift rty T) then
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 352
(mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 353
else
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354
Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
139
+ − 355
end
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 356
| Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 357
let
139
+ − 358
val ty1 = domain_type ty
+ − 359
val ty2 = domain_type ty1
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360
val rrel = tyRel T rty rel lthy
139
+ − 361
in
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 362
if (needs_lift rty T) then
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 363
(mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 364
else
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 365
Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
139
+ − 366
end
251
+ − 367
| Const (@{const_name "op ="}, ty) $ t =>
+ − 368
if needs_lift rty (fastype_of t) then
+ − 369
(tyRel (fastype_of t) rty rel lthy) $ t
+ − 370
else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 371
| t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
139
+ − 372
| _ => trm
+ − 373
*}
+ − 374
141
+ − 375
text {* Assumes that the given theorem is atomized *}
140
+ − 376
ML {*
+ − 377
fun build_regularize_goal thm rty rel lthy =
+ − 378
Logic.mk_implies
+ − 379
((prop_of thm),
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 380
(my_reg lthy rel rty (prop_of thm)))
140
+ − 381
*}
+ − 382
277
+ − 383
lemma universal_twice:
+ − 384
"(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 385
by auto
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 386
277
+ − 387
lemma implication_twice:
+ − 388
"(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 389
by auto
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 390
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 391
(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 392
by auto*)
251
+ − 393
187
+ − 394
ML {*
251
+ − 395
fun regularize thm rty rel rel_eqv rel_refl lthy =
187
+ − 396
let
+ − 397
val g = build_regularize_goal thm rty rel lthy;
+ − 398
fun tac ctxt =
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 399
(ObjectLogic.full_atomize_tac) THEN'
251
+ − 400
REPEAT_ALL_NEW (FIRST' [
+ − 401
rtac rel_refl,
+ − 402
atac,
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 403
rtac @{thm universal_twice},
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 404
(rtac @{thm impI} THEN' atac),
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 405
rtac @{thm implication_twice},
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 406
(*rtac @{thm equality_twice},*)
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 407
EqSubst.eqsubst_tac ctxt [0]
187
+ − 408
[(@{thm equiv_res_forall} OF [rel_eqv]),
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 409
(@{thm equiv_res_exists} OF [rel_eqv])],
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 410
(rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 411
(rtac @{thm RIGHT_RES_FORALL_REGULAR})
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 412
]);
187
+ − 413
val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
+ − 414
in
+ − 415
cthm OF [thm]
+ − 416
end
+ − 417
*}
+ − 418
140
+ − 419
section {* RepAbs injection *}
139
+ − 420
161
+ − 421
(* Needed to have a meta-equality *)
+ − 422
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
+ − 423
by (simp add: id_def)
+ − 424
139
+ − 425
ML {*
218
+ − 426
fun old_exchange_ty rty qty ty =
+ − 427
if ty = rty
+ − 428
then qty
+ − 429
else
+ − 430
(case ty of
+ − 431
Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
+ − 432
| _ => ty
+ − 433
)
+ − 434
*}
+ − 435
277
+ − 436
218
+ − 437
ML {*
+ − 438
fun old_get_fun flag rty qty lthy ty =
+ − 439
get_fun flag [(qty, rty)] lthy ty
+ − 440
+ − 441
fun old_make_const_def nconst_bname otrm mx rty qty lthy =
277
+ − 442
make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy
218
+ − 443
*}
+ − 444
235
+ − 445
text {* Does the same as 'subst' in a given prop or theorem *}
+ − 446
ML {*
+ − 447
fun eqsubst_prop ctxt thms t =
+ − 448
let
+ − 449
val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
+ − 450
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+ − 451
NONE => error "eqsubst_prop"
+ − 452
| SOME th => cprem_of th 1
+ − 453
in term_of a' end
+ − 454
*}
+ − 455
+ − 456
ML {*
+ − 457
fun repeat_eqsubst_prop ctxt thms t =
+ − 458
repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
+ − 459
handle _ => t
+ − 460
*}
+ − 461
+ − 462
+ − 463
ML {*
+ − 464
fun eqsubst_thm ctxt thms thm =
+ − 465
let
+ − 466
val goalstate = Goal.init (Thm.cprop_of thm)
+ − 467
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+ − 468
NONE => error "eqsubst_thm"
+ − 469
| SOME th => cprem_of th 1
+ − 470
val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+ − 471
val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
+ − 472
val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
+ − 473
in
+ − 474
@{thm Pure.equal_elim_rule1} OF [rt,thm]
+ − 475
end
+ − 476
*}
+ − 477
+ − 478
ML {*
+ − 479
fun repeat_eqsubst_thm ctxt thms thm =
+ − 480
repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+ − 481
handle _ => thm
+ − 482
*}
+ − 483
218
+ − 484
ML {*
140
+ − 485
fun build_repabs_term lthy thm constructors rty qty =
139
+ − 486
let
+ − 487
fun mk_rep tm =
+ − 488
let
218
+ − 489
val ty = old_exchange_ty rty qty (fastype_of tm)
+ − 490
in fst (old_get_fun repF rty qty lthy ty) $ tm end
139
+ − 491
+ − 492
fun mk_abs tm =
+ − 493
let
218
+ − 494
val ty = old_exchange_ty rty qty (fastype_of tm) in
+ − 495
fst (old_get_fun absF rty qty lthy ty) $ tm end
139
+ − 496
+ − 497
fun is_constructor (Const (x, _)) = member (op =) constructors x
+ − 498
| is_constructor _ = false;
+ − 499
+ − 500
fun build_aux lthy tm =
+ − 501
case tm of
+ − 502
Abs (a as (_, vty, _)) =>
+ − 503
let
+ − 504
val (vs, t) = Term.dest_abs a;
+ − 505
val v = Free(vs, vty);
+ − 506
val t' = lambda v (build_aux lthy t)
+ − 507
in
+ − 508
if (not (needs_lift rty (fastype_of tm))) then t'
+ − 509
else mk_rep (mk_abs (
+ − 510
if not (needs_lift rty vty) then t'
+ − 511
else
+ − 512
let
+ − 513
val v' = mk_rep (mk_abs v);
+ − 514
val t1 = Envir.beta_norm (t' $ v')
+ − 515
in
+ − 516
lambda v t1
+ − 517
end
+ − 518
))
+ − 519
end
+ − 520
| x =>
+ − 521
let
+ − 522
val (opp, tms0) = Term.strip_comb tm
+ − 523
val tms = map (build_aux lthy) tms0
+ − 524
val ty = fastype_of tm
+ − 525
in
+ − 526
if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
+ − 527
then (list_comb (opp, (hd tms0) :: (tl tms)))
+ − 528
else if (is_constructor opp andalso needs_lift rty ty) then
+ − 529
mk_rep (mk_abs (list_comb (opp,tms)))
+ − 530
else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
149
+ − 531
mk_rep(mk_abs(list_comb(opp,tms)))
139
+ − 532
else if tms = [] then opp
+ − 533
else list_comb(opp, tms)
+ − 534
end
+ − 535
in
235
+ − 536
repeat_eqsubst_prop lthy @{thms id_def_sym}
161
+ − 537
(build_aux lthy (Thm.prop_of thm))
139
+ − 538
end
+ − 539
*}
+ − 540
141
+ − 541
text {* Assumes that it is given a regularized theorem *}
139
+ − 542
ML {*
140
+ − 543
fun build_repabs_goal ctxt thm cons rty qty =
+ − 544
Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
139
+ − 545
*}
+ − 546
187
+ − 547
ML {*
+ − 548
fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+ − 549
let
+ − 550
val pat = Drule.strip_imp_concl (cprop_of thm)
+ − 551
val insts = Thm.match (pat, concl)
+ − 552
in
+ − 553
rtac (Drule.instantiate insts thm) 1
152
53277fbb2dba
Simplified the proof with some tactic... Still hangs sometimes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 554
end
187
+ − 555
handle _ => no_tac
+ − 556
)
+ − 557
*}
+ − 558
+ − 559
+ − 560
+ − 561
ML {*
+ − 562
fun quotient_tac quot_thm =
+ − 563
REPEAT_ALL_NEW (FIRST' [
+ − 564
rtac @{thm FUN_QUOTIENT},
+ − 565
rtac quot_thm,
+ − 566
rtac @{thm IDENTITY_QUOTIENT}
+ − 567
])
+ − 568
*}
+ − 569
+ − 570
ML {*
+ − 571
fun LAMBDA_RES_TAC ctxt i st =
+ − 572
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ − 573
(_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
+ − 574
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 575
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 576
| _ => fn _ => no_tac) i st
+ − 577
*}
+ − 578
+ − 579
ML {*
+ − 580
fun WEAK_LAMBDA_RES_TAC ctxt i st =
+ − 581
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ − 582
(_ $ (_ $ _$(Abs(_,_,_)))) =>
+ − 583
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 584
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 585
| (_ $ (_ $ (Abs(_,_,_))$_)) =>
+ − 586
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 587
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 588
| _ => fn _ => no_tac) i st
+ − 589
*}
+ − 590
206
+ − 591
ML {*
+ − 592
fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
+ − 593
let
+ − 594
val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
+ − 595
val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+ − 596
val insts = Thm.match (pat, concl)
+ − 597
in
+ − 598
if needs_lift rty (type_of f) then
+ − 599
rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+ − 600
else no_tac
+ − 601
end
+ − 602
handle _ => no_tac)
+ − 603
*}
187
+ − 604
+ − 605
ML {*
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 606
val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 607
let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 608
val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 609
in
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 610
((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 611
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 612
THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 613
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 614
end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 615
handle _ => no_tac
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 616
)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 617
*}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 618
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 619
ML {*
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 620
val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 621
let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 622
val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 623
in
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 624
((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 625
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 626
THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 627
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 628
end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 629
handle _ => no_tac
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 630
)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 631
*}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 632
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 633
ML {*
206
+ − 634
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
187
+ − 635
(FIRST' [
259
+ − 636
(* rtac @{thm FUN_QUOTIENT},
187
+ − 637
rtac quot_thm,
259
+ − 638
rtac @{thm IDENTITY_QUOTIENT},*)
187
+ − 639
rtac trans_thm,
+ − 640
LAMBDA_RES_TAC ctxt,
+ − 641
res_forall_rsp_tac ctxt,
+ − 642
res_exists_rsp_tac ctxt,
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 643
FIRST' (map rtac rsp_thms),
187
+ − 644
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+ − 645
rtac refl,
206
+ − 646
(* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
+ − 647
(APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+ − 648
Cong_Tac.cong_tac @{thm cong},
+ − 649
rtac @{thm ext},
187
+ − 650
rtac reflex_thm,
+ − 651
atac,
+ − 652
(
+ − 653
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+ − 654
THEN_ALL_NEW (fn _ => no_tac)
+ − 655
),
+ − 656
WEAK_LAMBDA_RES_TAC ctxt
+ − 657
])
+ − 658
*}
+ − 659
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 660
ML {*
210
+ − 661
fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 662
let
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 663
val rt = build_repabs_term lthy thm constructors rty qty;
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 664
val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 665
fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
206
+ − 666
(REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 667
val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 668
in
210
+ − 669
@{thm Pure.equal_elim_rule1} OF [cthm, thm]
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 670
end
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 671
*}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 672
187
+ − 673
section {* Cleaning the goal *}
+ − 674
236
+ − 675
lemma prod_fun_id: "prod_fun id id = id"
+ − 676
apply (simp add: prod_fun_def)
+ − 677
done
+ − 678
lemma map_id: "map id x = x"
+ − 679
apply (induct x)
+ − 680
apply (simp_all add: map.simps)
+ − 681
done
+ − 682
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 683
text {* expects atomized definition *}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 684
ML {*
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 685
fun add_lower_defs_aux ctxt thm =
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 686
let
209
+ − 687
val e1 = @{thm fun_cong} OF [thm];
+ − 688
val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
+ − 689
val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
236
+ − 690
val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 691
in
236
+ − 692
thm :: (add_lower_defs_aux ctxt h)
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 693
end
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 694
handle _ => [thm]
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 695
*}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 696
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 697
ML {*
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 698
fun add_lower_defs ctxt defs =
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 699
let
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 700
val defs_pre_sym = map symmetric defs
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 701
val defs_atom = map atomize_thm defs_pre_sym
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 702
val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 703
in
214
+ − 704
map Thm.varifyT defs_all
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 705
end
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 706
*}
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 707
191
+ − 708
ML {*
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 709
fun findabs_all rty tm =
191
+ − 710
case tm of
+ − 711
Abs(_, T, b) =>
+ − 712
let
+ − 713
val b' = subst_bound ((Free ("x", T)), b);
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 714
val tys = findabs_all rty b'
191
+ − 715
val ty = fastype_of tm
+ − 716
in if needs_lift rty ty then (ty :: tys) else tys
+ − 717
end
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 718
| f $ a => (findabs_all rty f) @ (findabs_all rty a)
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 719
| _ => [];
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 720
fun findabs rty tm = distinct (op =) (findabs_all rty tm)
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 721
*}
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 722
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 723
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 724
ML {*
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 725
fun findaps_all rty tm =
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 726
case tm of
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 727
Abs(_, T, b) =>
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 728
findaps_all rty (subst_bound ((Free ("x", T)), b))
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 729
| (f $ a) => (findaps_all rty f @ findaps_all rty a)
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 730
| Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else [])
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 731
| _ => [];
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 732
fun findaps rty tm = distinct (op =) (findaps_all rty tm)
191
+ − 733
*}
190
ca1a24aa822e
Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 734
197
+ − 735
ML {*
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 736
fun make_simp_prs_thm lthy quot_thm thm typ =
197
+ − 737
let
+ − 738
val (_, [lty, rty]) = dest_Type typ;
+ − 739
val thy = ProofContext.theory_of lthy;
+ − 740
val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
+ − 741
val inst = [SOME lcty, NONE, SOME rcty];
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 742
val lpi = Drule.instantiate' inst [] thm;
197
+ − 743
val tac =
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 744
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
197
+ − 745
(quotient_tac quot_thm);
259
+ − 746
val gc = Drule.strip_imp_concl (cprop_of lpi);
+ − 747
val t = Goal.prove_internal [] gc (fn _ => tac 1)
197
+ − 748
in
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 749
MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
197
+ − 750
end
+ − 751
*}
+ − 752
+ − 753
ML {*
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 754
fun findallex_all rty qty tm =
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 755
case tm of
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 756
Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 757
let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 758
val (tya, tye) = findallex_all rty qty s
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 759
in if needs_lift rty T then
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 760
((T :: tya), tye)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 761
else (tya, tye) end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 762
| Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 763
let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 764
val (tya, tye) = findallex_all rty qty s
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 765
in if needs_lift rty T then
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 766
(tya, (T :: tye))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 767
else (tya, tye) end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 768
| Abs(_, T, b) =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 769
findallex_all rty qty (subst_bound ((Free ("x", T)), b))
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 770
| f $ a =>
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 771
let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 772
val (a1, e1) = findallex_all rty qty f;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 773
val (a2, e2) = findallex_all rty qty a;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 774
in (a1 @ a2, e1 @ e2) end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 775
| _ => ([], []);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 776
*}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 777
ML {*
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 778
fun findallex rty qty tm =
197
+ − 779
let
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 780
val (a, e) = findallex_all rty qty tm;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 781
val (ad, ed) = (map domain_type a, map domain_type e);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 782
val (au, eu) = (distinct (op =) ad, distinct (op =) ed)
197
+ − 783
in
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 784
(map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu)
197
+ − 785
end
+ − 786
*}
+ − 787
198
+ − 788
ML {*
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 789
fun make_allex_prs_thm lthy quot_thm thm typ =
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 790
let
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 791
val (_, [lty, rty]) = dest_Type typ;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 792
val thy = ProofContext.theory_of lthy;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 793
val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 794
val inst = [NONE, SOME lcty];
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 795
val lpi = Drule.instantiate' inst [] thm;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 796
val tac =
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 797
(compose_tac (false, lpi, 1)) THEN_ALL_NEW
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 798
(quotient_tac quot_thm);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 799
val gc = Drule.strip_imp_concl (cprop_of lpi);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 800
val t = Goal.prove_internal [] gc (fn _ => tac 1)
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 801
val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t;
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 802
val t_sym = @{thm "HOL.sym"} OF [t_noid];
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 803
val t_eq = @{thm "eq_reflection"} OF [t_sym]
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 804
in
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 805
t_eq
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 806
end
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 807
*}
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 808
269
+ − 809
ML {*
+ − 810
fun applic_prs lthy rty qty absrep ty =
+ − 811
let
+ − 812
fun absty ty =
+ − 813
old_exchange_ty rty qty ty
+ − 814
fun mk_rep tm =
+ − 815
let
+ − 816
val ty = old_exchange_ty rty qty (fastype_of tm)
+ − 817
in fst (old_get_fun repF rty qty lthy ty) $ tm end;
+ − 818
fun mk_abs tm =
+ − 819
let
+ − 820
val ty = old_exchange_ty rty qty (fastype_of tm) in
+ − 821
fst (old_get_fun absF rty qty lthy ty) $ tm end;
+ − 822
val (l, ltl) = Term.strip_type ty;
+ − 823
val nl = map absty l;
+ − 824
val vs = map (fn _ => "x") l;
+ − 825
val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+ − 826
val args = map Free (vfs ~~ nl);
+ − 827
val lhs = list_comb((Free (fname, nl ---> ltl)), args);
+ − 828
val rargs = map mk_rep args;
+ − 829
val f = Free (fname, nl ---> ltl);
+ − 830
val rhs = mk_abs (list_comb((mk_rep f), rargs));
+ − 831
val eq = Logic.mk_equals (rhs, lhs);
+ − 832
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+ − 833
val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps});
+ − 834
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+ − 835
val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
+ − 836
in
+ − 837
singleton (ProofContext.export lthy' lthy) t_id
+ − 838
end
+ − 839
*}
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 840
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 841
ML {*
239
+ − 842
fun lookup_quot_data lthy qty =
+ − 843
let
257
+ − 844
val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+ − 845
val rty = Logic.unvarifyT (#rtyp quotdata)
239
+ − 846
val rel = #rel quotdata
+ − 847
val rel_eqv = #equiv_thm quotdata
+ − 848
val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
+ − 849
val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
+ − 850
in
+ − 851
(rty, rel, rel_refl, rel_eqv)
+ − 852
end
+ − 853
*}
+ − 854
+ − 855
ML {*
+ − 856
fun lookup_quot_thms lthy qty_name =
+ − 857
let
+ − 858
val thy = ProofContext.theory_of lthy;
+ − 859
val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
+ − 860
val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
269
+ − 861
val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
239
+ − 862
val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
+ − 863
in
269
+ − 864
(trans2, reps_same, absrep, quot)
239
+ − 865
end
+ − 866
*}
+ − 867
+ − 868
ML {*
+ − 869
fun lookup_quot_consts defs =
+ − 870
let
+ − 871
fun dest_term (a $ b) = (a, b);
+ − 872
val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
+ − 873
in
+ − 874
map (fst o dest_Const o snd o dest_term) def_terms
+ − 875
end
+ − 876
*}
+ − 877
275
+ − 878
239
+ − 879
ML {*
+ − 880
fun lift_thm lthy qty qty_name rsp_thms defs t = let
+ − 881
val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
269
+ − 882
val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
239
+ − 883
val consts = lookup_quot_consts defs;
198
+ − 884
val t_a = atomize_thm t;
251
+ − 885
val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
210
+ − 886
val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 887
val (alls, exs) = findallex rty qty (prop_of t_a);
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 888
val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 889
val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 890
val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
198
+ − 891
val abs = findabs rty (prop_of t_a);
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 892
val aps = findaps rty (prop_of t_a);
269
+ − 893
val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 894
val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
259
+ − 895
val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
239
+ − 896
val defs_sym = add_lower_defs lthy defs;
259
+ − 897
val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
+ − 898
val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;
+ − 899
val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
198
+ − 900
val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+ − 901
in
+ − 902
ObjectLogic.rulify t_r
187
+ − 903
end
198
+ − 904
*}
+ − 905
273
+ − 906
ML {*
+ − 907
fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
+ − 908
let
+ − 909
val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
+ − 910
val (_, lthy2) = note (name, lifted_thm) lthy;
+ − 911
in
+ − 912
lthy2
+ − 913
end;
+ − 914
*}
+ − 915
239
+ − 916
198
+ − 917
end
239
+ − 918