0
+ − 1
theory QuotMain
6
+ − 2
imports QuotScript QuotList Prove
544
+ − 3
uses ("quotient_info.ML")
264
+ − 4
("quotient.ML")
277
+ − 5
("quotient_def.ML")
0
+ − 6
begin
+ − 7
582
+ − 8
0
+ − 9
locale QUOT_TYPE =
+ − 10
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ − 11
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ − 12
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
582
+ − 13
assumes equivp: "equivp R"
0
+ − 14
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ − 15
and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ − 16
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ − 17
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
15
+ − 18
begin
0
+ − 19
+ − 20
definition
200
+ − 21
ABS::"'a \<Rightarrow> 'b"
+ − 22
where
0
+ − 23
"ABS x \<equiv> Abs (R x)"
+ − 24
+ − 25
definition
200
+ − 26
REP::"'b \<Rightarrow> 'a"
+ − 27
where
0
+ − 28
"REP a = Eps (Rep a)"
+ − 29
15
+ − 30
lemma lem9:
0
+ − 31
shows "R (Eps (R x)) = R x"
+ − 32
proof -
582
+ − 33
have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
0
+ − 34
then have "R x (Eps (R x))" by (rule someI)
15
+ − 35
then show "R (Eps (R x)) = R x"
582
+ − 36
using equivp unfolding equivp_def by simp
0
+ − 37
qed
+ − 38
+ − 39
theorem thm10:
24
+ − 40
shows "ABS (REP a) \<equiv> a"
+ − 41
apply (rule eq_reflection)
+ − 42
unfolding ABS_def REP_def
0
+ − 43
proof -
15
+ − 44
from rep_prop
0
+ − 45
obtain x where eq: "Rep a = R x" by auto
+ − 46
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ − 47
also have "\<dots> = Abs (R x)" using lem9 by simp
+ − 48
also have "\<dots> = Abs (Rep a)" using eq by simp
+ − 49
also have "\<dots> = a" using rep_inverse by simp
+ − 50
finally
+ − 51
show "Abs (R (Eps (Rep a))) = a" by simp
+ − 52
qed
+ − 53
15
+ − 54
lemma REP_refl:
0
+ − 55
shows "R (REP a) (REP a)"
+ − 56
unfolding REP_def
582
+ − 57
by (simp add: equivp[simplified equivp_def])
0
+ − 58
+ − 59
lemma lem7:
22
+ − 60
shows "(R x = R y) = (Abs (R x) = Abs (R y))"
0
+ − 61
apply(rule iffI)
+ − 62
apply(simp)
+ − 63
apply(drule rep_inject[THEN iffD2])
+ − 64
apply(simp add: abs_inverse)
+ − 65
done
15
+ − 66
0
+ − 67
theorem thm11:
+ − 68
shows "R r r' = (ABS r = ABS r')"
+ − 69
unfolding ABS_def
582
+ − 70
by (simp only: equivp[simplified equivp_def] lem7)
0
+ − 71
4
+ − 72
2
+ − 73
lemma REP_ABS_rsp:
4
+ − 74
shows "R f (REP (ABS g)) = R f g"
+ − 75
and "R (REP (ABS g)) f = R g f"
23
+ − 76
by (simp_all add: thm10 thm11)
4
+ − 77
529
+ − 78
lemma Quotient:
+ − 79
"Quotient R ABS REP"
+ − 80
apply(unfold Quotient_def)
0
+ − 81
apply(simp add: thm10)
+ − 82
apply(simp add: REP_refl)
+ − 83
apply(subst thm11[symmetric])
582
+ − 84
apply(simp add: equivp[simplified equivp_def])
0
+ − 85
done
+ − 86
21
+ − 87
lemma R_trans:
49
+ − 88
assumes ab: "R a b"
+ − 89
and bc: "R b c"
22
+ − 90
shows "R a c"
21
+ − 91
proof -
582
+ − 92
have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
21
+ − 93
moreover have ab: "R a b" by fact
+ − 94
moreover have bc: "R b c" by fact
529
+ − 95
ultimately show "R a c" unfolding transp_def by blast
21
+ − 96
qed
+ − 97
+ − 98
lemma R_sym:
49
+ − 99
assumes ab: "R a b"
22
+ − 100
shows "R b a"
21
+ − 101
proof -
582
+ − 102
have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
529
+ − 103
then show "R b a" using ab unfolding symp_def by blast
21
+ − 104
qed
+ − 105
49
+ − 106
lemma R_trans2:
+ − 107
assumes ac: "R a c"
22
+ − 108
and bd: "R b d"
21
+ − 109
shows "R a b = R c d"
200
+ − 110
using ac bd
+ − 111
by (blast intro: R_trans R_sym)
21
+ − 112
+ − 113
lemma REPS_same:
25
+ − 114
shows "R (REP a) (REP b) \<equiv> (a = b)"
38
+ − 115
proof -
+ − 116
have "R (REP a) (REP b) = (a = b)"
+ − 117
proof
+ − 118
assume as: "R (REP a) (REP b)"
+ − 119
from rep_prop
+ − 120
obtain x y
+ − 121
where eqs: "Rep a = R x" "Rep b = R y" by blast
+ − 122
from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+ − 123
then have "R x (Eps (R y))" using lem9 by simp
+ − 124
then have "R (Eps (R y)) x" using R_sym by blast
+ − 125
then have "R y x" using lem9 by simp
+ − 126
then have "R x y" using R_sym by blast
+ − 127
then have "ABS x = ABS y" using thm11 by simp
+ − 128
then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+ − 129
then show "a = b" using rep_inverse by simp
+ − 130
next
+ − 131
assume ab: "a = b"
582
+ − 132
have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
529
+ − 133
then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
38
+ − 134
qed
+ − 135
then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
21
+ − 136
qed
+ − 137
0
+ − 138
end
+ − 139
+ − 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
537
+ − 145
declare [[map list = (map, list_rel)]]
185
+ − 146
declare [[map * = (prod_fun, prod_rel)]]
536
+ − 147
declare [[map "fun" = (fun_map, fun_rel)]]
185
+ − 148
537
+ − 149
lemmas [quotient_thm] =
+ − 150
fun_quotient list_quotient
506
+ − 151
555
b460565dbb58
Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 152
lemmas [quotient_rsp] =
566
+ − 153
quot_rel_rsp nil_rsp cons_rsp foldl_rsp
555
b460565dbb58
Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 154
582
+ − 155
(* OPTION, PRODUCTS *)
+ − 156
lemmas [quotient_equiv] =
+ − 157
identity_equivp list_equivp
+ − 158
+ − 159
185
+ − 160
ML {* maps_lookup @{theory} "List.list" *}
+ − 161
ML {* maps_lookup @{theory} "*" *}
+ − 162
ML {* maps_lookup @{theory} "fun" *}
174
+ − 163
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
+ − 164
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
+ − 165
(* definition of the quotient types *)
277
+ − 166
(* 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
+ − 167
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
+ − 168
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
+ − 169
277
+ − 170
(* lifting of constants *)
+ − 171
use "quotient_def.ML"
+ − 172
381
+ − 173
definition
+ − 174
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ − 175
where
+ − 176
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 177
544
+ − 178
section {* atomize *}
139
+ − 179
381
+ − 180
lemma atomize_eqv[atomize]:
+ − 181
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
139
+ − 182
proof
381
+ − 183
assume "A \<equiv> B"
139
+ − 184
then show "Trueprop A \<equiv> Trueprop B" by unfold
+ − 185
next
+ − 186
assume *: "Trueprop A \<equiv> Trueprop B"
+ − 187
have "A = B"
+ − 188
proof (cases A)
+ − 189
case True
+ − 190
have "A" by fact
+ − 191
then show "A = B" using * by simp
+ − 192
next
+ − 193
case False
+ − 194
have "\<not>A" by fact
+ − 195
then show "A = B" using * by auto
+ − 196
qed
+ − 197
then show "A \<equiv> B" by (rule eq_reflection)
+ − 198
qed
+ − 199
+ − 200
ML {*
+ − 201
fun atomize_thm thm =
+ − 202
let
221
+ − 203
val thm' = Thm.freezeT (forall_intr_vars thm)
139
+ − 204
val thm'' = ObjectLogic.atomize (cprop_of thm')
+ − 205
in
404
+ − 206
@{thm equal_elim_rule1} OF [thm'', thm']
139
+ − 207
end
+ − 208
*}
+ − 209
387
+ − 210
section {* infrastructure about id *}
381
+ − 211
+ − 212
lemma prod_fun_id: "prod_fun id id \<equiv> id"
415
+ − 213
by (rule eq_reflection) (simp add: prod_fun_def)
381
+ − 214
+ − 215
lemma map_id: "map id \<equiv> id"
415
+ − 216
apply (rule eq_reflection)
+ − 217
apply (rule ext)
+ − 218
apply (rule_tac list="x" in list.induct)
+ − 219
apply (simp_all)
+ − 220
done
381
+ − 221
409
+ − 222
lemmas id_simps =
537
+ − 223
fun_map_id[THEN eq_reflection]
409
+ − 224
id_apply[THEN eq_reflection]
415
+ − 225
id_def[THEN eq_reflection,symmetric]
+ − 226
prod_fun_id map_id
409
+ − 227
381
+ − 228
ML {*
409
+ − 229
fun simp_ids thm =
+ − 230
MetaSimplifier.rewrite_rule @{thms id_simps} thm
381
+ − 231
*}
+ − 232
407
+ − 233
section {* Debugging infrastructure for testing tactics *}
381
+ − 234
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 235
ML {*
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 236
fun my_print_tac ctxt s i thm =
407
+ − 237
let
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 238
val prem_str = nth (prems_of thm) (i - 1)
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 239
|> Syntax.string_of_term ctxt
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 240
handle Subscript => "no subgoal"
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 241
val _ = tracing (s ^ "\n" ^ prem_str)
407
+ − 242
in
+ − 243
Seq.single thm
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 244
end *}
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 245
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 246
ML {*
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 247
fun DT ctxt s tac i thm =
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 248
let
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 249
val before_goal = nth (prems_of thm) (i - 1)
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 250
|> Syntax.string_of_term ctxt
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 251
val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
|> cat_lines
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 253
in
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 254
EVERY [tac i, my_print_tac ctxt before_msg i] thm
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
end
444
+ − 256
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 257
fun NDT ctxt s tac thm = tac thm
407
+ − 258
*}
+ − 259
576
+ − 260
section {* Matching of terms and types *}
+ − 261
+ − 262
ML {*
+ − 263
fun matches_typ (ty, ty') =
+ − 264
case (ty, ty') of
+ − 265
(_, TVar _) => true
+ − 266
| (TFree x, TFree x') => x = x'
+ − 267
| (Type (s, tys), Type (s', tys')) =>
+ − 268
s = s' andalso
+ − 269
if (length tys = length tys')
+ − 270
then (List.all matches_typ (tys ~~ tys'))
+ − 271
else false
+ − 272
| _ => false
+ − 273
*}
577
+ − 274
576
+ − 275
ML {*
+ − 276
fun matches_term (trm, trm') =
+ − 277
case (trm, trm') of
+ − 278
(_, Var _) => true
+ − 279
| (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
+ − 280
| (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
+ − 281
| (Bound i, Bound j) => i = j
+ − 282
| (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
+ − 283
| (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s')
+ − 284
| _ => false
+ − 285
*}
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286
407
+ − 287
section {* Infrastructure for collecting theorems for starting the lifting *}
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 288
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 289
ML {*
239
+ − 290
fun lookup_quot_data lthy qty =
+ − 291
let
311
+ − 292
val qty_name = fst (dest_Type qty)
314
+ − 293
val SOME quotdata = quotdata_lookup lthy qty_name
303
+ − 294
(* TODO: Should no longer be needed *)
257
+ − 295
val rty = Logic.unvarifyT (#rtyp quotdata)
239
+ − 296
val rel = #rel quotdata
+ − 297
val rel_eqv = #equiv_thm quotdata
529
+ − 298
val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
239
+ − 299
in
+ − 300
(rty, rel, rel_refl, rel_eqv)
+ − 301
end
+ − 302
*}
+ − 303
+ − 304
ML {*
+ − 305
fun lookup_quot_thms lthy qty_name =
+ − 306
let
+ − 307
val thy = ProofContext.theory_of lthy;
+ − 308
val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
+ − 309
val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
269
+ − 310
val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
529
+ − 311
val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
239
+ − 312
in
269
+ − 313
(trans2, reps_same, absrep, quot)
239
+ − 314
end
+ − 315
*}
+ − 316
402
+ − 317
section {* Regularization *}
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 318
383
+ − 319
(*
+ − 320
Regularizing an rtrm means:
+ − 321
- quantifiers over a type that needs lifting are replaced by
+ − 322
bounded quantifiers, for example:
+ − 323
\<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
+ − 324
+ − 325
the relation R is given by the rty and qty;
330
+ − 326
383
+ − 327
- abstractions over a type that needs lifting are replaced
+ − 328
by bounded abstractions:
+ − 329
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+ − 330
+ − 331
- equalities over the type being lifted are replaced by
+ − 332
corresponding relations:
+ − 333
A = B \<Longrightarrow> A \<approx> B
+ − 334
+ − 335
example with more complicated types of A, B:
+ − 336
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+ − 337
*)
+ − 338
404
+ − 339
ML {*
383
+ − 340
(* builds the relation that is the argument of respects *)
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 341
fun mk_resp_arg lthy (rty, qty) =
319
+ − 342
let
+ − 343
val thy = ProofContext.theory_of lthy
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 344
in
334
+ − 345
if rty = qty
+ − 346
then HOLogic.eq_const rty
+ − 347
else
+ − 348
case (rty, qty) of
+ − 349
(Type (s, tys), Type (s', tys')) =>
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 350
if s = s'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 351
then let
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 352
val SOME map_info = maps_lookup thy s
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 353
val args = map (mk_resp_arg lthy) (tys ~~ tys')
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 354
in
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 355
list_comb (Const (#relfun map_info, dummyT), args)
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 356
end
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 357
else let
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 358
val SOME qinfo = quotdata_lookup_thy thy s'
330
+ − 359
(* FIXME: check in this case that the rty and qty *)
+ − 360
(* FIXME: correspond to each other *)
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 361
val (s, _) = dest_Const (#rel qinfo)
407
+ − 362
(* FIXME: the relation should only be the string *)
+ − 363
(* FIXME: and the type needs to be calculated as below; *)
+ − 364
(* FIXME: maybe one should actually have a term *)
+ − 365
(* FIXME: and one needs to force it to have this type *)
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 366
in
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 367
Const (s, rty --> rty --> @{typ bool})
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 368
end
334
+ − 369
| _ => HOLogic.eq_const dummyT
351
+ − 370
(* FIXME: check that the types correspond to each other? *)
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 371
end
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 372
*}
239
+ − 373
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 374
ML {*
467
+ − 375
val mk_babs = Const (@{const_name Babs}, dummyT)
+ − 376
val mk_ball = Const (@{const_name Ball}, dummyT)
+ − 377
val mk_bex = Const (@{const_name Bex}, dummyT)
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 378
val mk_resp = Const (@{const_name Respects}, dummyT)
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 379
*}
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 380
323
+ − 381
ML {*
330
+ − 382
(* - applies f to the subterm of an abstraction, *)
+ − 383
(* otherwise to the given term, *)
405
+ − 384
(* - used by regularize, therefore abstracted *)
330
+ − 385
(* variables do not have to be treated specially *)
+ − 386
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 387
fun apply_subt f trm1 trm2 =
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 388
case (trm1, trm2) of
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 389
(Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 390
| _ => f trm1 trm2
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 391
330
+ − 392
(* the major type of All and Ex quantifiers *)
334
+ − 393
fun qnt_typ ty = domain_type (domain_type ty)
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 394
*}
319
+ − 395
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 396
ML {*
330
+ − 397
(* produces a regularized version of rtm *)
+ − 398
(* - the result is still not completely typed *)
+ − 399
(* - does not need any special treatment of *)
+ − 400
(* bound variables *)
+ − 401
405
+ − 402
fun regularize_trm lthy rtrm qtrm =
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 403
case (rtrm, qtrm) of
325
+ − 404
(Abs (x, ty, t), Abs (x', ty', t')) =>
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 405
let
405
+ − 406
val subtrm = regularize_trm lthy t t'
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 407
in
325
+ − 408
if ty = ty'
+ − 409
then Abs (x, ty, subtrm)
326
+ − 410
else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 411
end
549
+ − 412
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 413
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 414
let
405
+ − 415
val subtrm = apply_subt (regularize_trm lthy) t t'
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 416
in
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 417
if ty = ty'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 418
then Const (@{const_name "All"}, ty) $ subtrm
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 419
else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 420
end
549
+ − 421
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 422
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 423
let
405
+ − 424
val subtrm = apply_subt (regularize_trm lthy) t t'
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 425
in
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 426
if ty = ty'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
then Const (@{const_name "Ex"}, ty) $ subtrm
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 428
else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 429
end
549
+ − 430
+ − 431
| (* equalities need to be replaced by appropriate equivalence relations *)
+ − 432
(Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+ − 433
if ty = ty'
+ − 434
then rtrm
+ − 435
else mk_resp_arg lthy (domain_type ty, domain_type ty')
+ − 436
+ − 437
| (* in this case we check whether the given equivalence relation is correct *)
+ − 438
(rel, Const (@{const_name "op ="}, ty')) =>
+ − 439
let
+ − 440
val exc = LIFT_MATCH "regularise (relation mismatch)"
+ − 441
val rel_ty = (fastype_of rel) handle TERM _ => raise exc
+ − 442
val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty')
+ − 443
in
+ − 444
if rel' = rel
+ − 445
then rtrm
+ − 446
else raise exc
+ − 447
end
+ − 448
| (_, Const (s, _)) =>
+ − 449
let
+ − 450
fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
+ − 451
| same_name _ _ = false
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
in
549
+ − 453
if same_name rtrm qtrm
+ − 454
then rtrm
+ − 455
else
+ − 456
let
+ − 457
fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)")
+ − 458
val exc2 = LIFT_MATCH ("regularize (constant mismatch)")
+ − 459
val thy = ProofContext.theory_of lthy
+ − 460
val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s)
+ − 461
in
+ − 462
if matches_term (rtrm, rtrm')
+ − 463
then rtrm
+ − 464
else raise exc2
+ − 465
end
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
end
549
+ − 467
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 468
| (t1 $ t2, t1' $ t2') =>
405
+ − 469
(regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
549
+ − 470
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 471
| (Free (x, ty), Free (x', ty')) =>
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 472
(* this case cannot arrise as we start with two fully atomized terms *)
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 473
raise (LIFT_MATCH "regularize (frees)")
549
+ − 474
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
| (Bound i, Bound i') =>
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 476
if i = i'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 477
then rtrm
549
+ − 478
else raise (LIFT_MATCH "regularize (bounds mismatch)")
+ − 479
+ − 480
| (rt, qt) =>
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 481
raise (LIFT_MATCH "regularize (default)")
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 482
*}
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 483
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 484
(*
407
+ − 485
FIXME / TODO: needs to be adapted
+ − 486
383
+ − 487
To prove that the raw theorem implies the regularised one,
+ − 488
we try in order:
330
+ − 489
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 490
- Reflexivity of the relation
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 491
- Assumption
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 492
- Elimnating quantifiers on both sides of toplevel implication
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
- Simplifying implications on both sides of toplevel implication
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
- Ball (Respects ?E) ?P = All ?P
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 495
- (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 496
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 497
*)
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 498
400
+ − 499
ML {*
582
+ − 500
fun equiv_tac ctxt =
420
+ − 501
REPEAT_ALL_NEW (FIRST'
582
+ − 502
[resolve_tac (equiv_rules_get ctxt)])
400
+ − 503
*}
+ − 504
+ − 505
ML {*
583
+ − 506
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
+ − 507
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+ − 508
*}
+ − 509
+ − 510
ML {*
582
+ − 511
fun ball_reg_eqv_simproc ss redex =
432
+ − 512
let
+ − 513
val ctxt = Simplifier.the_context ss
+ − 514
val thy = ProofContext.theory_of ctxt
+ − 515
in
+ − 516
case redex of
+ − 517
(ogl as ((Const (@{const_name "Ball"}, _)) $
+ − 518
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
+ − 519
(let
529
+ − 520
val gl = Const (@{const_name "equivp"}, dummyT) $ R;
432
+ − 521
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
582
+ − 522
val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
+ − 523
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
+ − 524
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+ − 525
in
+ − 526
SOME thm
+ − 527
end
+ − 528
handle _ => NONE
+ − 529
)
+ − 530
| _ => NONE
+ − 531
end
+ − 532
*}
+ − 533
+ − 534
ML {*
582
+ − 535
fun bex_reg_eqv_simproc ss redex =
432
+ − 536
let
+ − 537
val ctxt = Simplifier.the_context ss
+ − 538
val thy = ProofContext.theory_of ctxt
+ − 539
in
+ − 540
case redex of
+ − 541
(ogl as ((Const (@{const_name "Bex"}, _)) $
+ − 542
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
+ − 543
(let
529
+ − 544
val gl = Const (@{const_name "equivp"}, dummyT) $ R;
432
+ − 545
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
582
+ − 546
val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
+ − 547
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
+ − 548
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+ − 549
in
+ − 550
SOME thm
+ − 551
end
+ − 552
handle _ => NONE
+ − 553
)
+ − 554
| _ => NONE
+ − 555
end
+ − 556
*}
+ − 557
+ − 558
ML {*
+ − 559
fun prep_trm thy (x, (T, t)) =
+ − 560
(cterm_of thy (Var (x, T)), cterm_of thy t)
+ − 561
+ − 562
fun prep_ty thy (x, (S, ty)) =
+ − 563
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+ − 564
*}
+ − 565
+ − 566
ML {*
+ − 567
fun matching_prs thy pat trm =
+ − 568
let
+ − 569
val univ = Unify.matchers thy [(pat, trm)]
+ − 570
val SOME (env, _) = Seq.pull univ
+ − 571
val tenv = Vartab.dest (Envir.term_env env)
+ − 572
val tyenv = Vartab.dest (Envir.type_env env)
+ − 573
in
+ − 574
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ − 575
end
400
+ − 576
*}
+ − 577
+ − 578
ML {*
582
+ − 579
fun ball_reg_eqv_range_simproc ss redex =
400
+ − 580
let
432
+ − 581
val ctxt = Simplifier.the_context ss
+ − 582
val thy = ProofContext.theory_of ctxt
400
+ − 583
in
432
+ − 584
case redex of
+ − 585
(ogl as ((Const (@{const_name "Ball"}, _)) $
536
+ − 586
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
432
+ − 587
(let
529
+ − 588
val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
432
+ − 589
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
487
+ − 590
(* val _ = tracing (Syntax.string_of_term ctxt glc);*)
582
+ − 591
val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
+ − 592
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
+ − 593
val R1c = cterm_of thy R1;
+ − 594
val thmi = Drule.instantiate' [] [SOME R1c] thm;
487
+ − 595
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*)
432
+ − 596
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
+ − 597
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
487
+ − 598
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *)
432
+ − 599
in
+ − 600
SOME thm2
+ − 601
end
+ − 602
handle _ => NONE
+ − 603
+ − 604
)
+ − 605
| _ => NONE
400
+ − 606
end
+ − 607
*}
432
+ − 608
583
+ − 609
578
+ − 610
thm bex_reg_eqv_range
583
+ − 611
thm ball_reg_eqv
+ − 612
thm bex_reg_eqv
578
+ − 613
432
+ − 614
ML {*
582
+ − 615
fun bex_reg_eqv_range_simproc ss redex =
432
+ − 616
let
+ − 617
val ctxt = Simplifier.the_context ss
+ − 618
val thy = ProofContext.theory_of ctxt
+ − 619
in
+ − 620
case redex of
+ − 621
(ogl as ((Const (@{const_name "Bex"}, _)) $
536
+ − 622
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
432
+ − 623
(let
529
+ − 624
val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
432
+ − 625
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
487
+ − 626
(* val _ = tracing (Syntax.string_of_term ctxt glc); *)
582
+ − 627
val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
432
+ − 628
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
+ − 629
val R1c = cterm_of thy R1;
+ − 630
val thmi = Drule.instantiate' [] [SOME R1c] thm;
+ − 631
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
+ − 632
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
+ − 633
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
487
+ − 634
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*)
432
+ − 635
in
+ − 636
SOME thm2
+ − 637
end
+ − 638
handle _ => NONE
+ − 639
+ − 640
)
+ − 641
| _ => NONE
+ − 642
end
+ − 643
*}
+ − 644
529
+ − 645
lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+ − 646
by (simp add: equivp_reflp)
432
+ − 647
583
+ − 648
(* does not work yet
432
+ − 649
ML {*
582
+ − 650
fun regularize_tac ctxt =
432
+ − 651
let
+ − 652
val pat1 = [@{term "Ball (Respects R) P"}];
+ − 653
val pat2 = [@{term "Bex (Respects R) P"}];
+ − 654
val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+ − 655
val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
+ − 656
val thy = ProofContext.theory_of ctxt
582
+ − 657
val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
+ − 658
val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
+ − 659
val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
+ − 660
val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
583
+ − 661
val simp_set = HOL_basic_ss addsimps @{thms ball_reg_eqv bex_reg_eqv}
+ − 662
addsimprocs [simproc3, simproc4]
+ − 663
addSolver equiv_solver
+ − 664
* TODO: Make sure that there are no list_rel, pair_rel etc involved *
582
+ − 665
val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
432
+ − 666
in
+ − 667
ObjectLogic.full_atomize_tac THEN'
583
+ − 668
simp_tac simp_set THEN'
432
+ − 669
REPEAT_ALL_NEW (FIRST' [
+ − 670
rtac @{thm ball_reg_right},
+ − 671
rtac @{thm bex_reg_left},
+ − 672
resolve_tac (Inductive.get_monos ctxt),
+ − 673
rtac @{thm ball_all_comm},
+ − 674
rtac @{thm bex_ex_comm},
+ − 675
resolve_tac eq_eqvs,
583
+ − 676
simp_tac simp_set
432
+ − 677
])
+ − 678
end
583
+ − 679
*}*)
+ − 680
+ − 681
ML {*
+ − 682
fun regularize_tac ctxt =
+ − 683
let
+ − 684
val pat1 = [@{term "Ball (Respects R) P"}];
+ − 685
val pat2 = [@{term "Bex (Respects R) P"}];
+ − 686
val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+ − 687
val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
+ − 688
val thy = ProofContext.theory_of ctxt
+ − 689
val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
+ − 690
val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
+ − 691
val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
+ − 692
val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
+ − 693
val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
+ − 694
(* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
+ − 695
val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
+ − 696
in
+ − 697
ObjectLogic.full_atomize_tac THEN'
+ − 698
simp_tac simp_ctxt THEN'
+ − 699
REPEAT_ALL_NEW (FIRST' [
+ − 700
rtac @{thm ball_reg_right},
+ − 701
rtac @{thm bex_reg_left},
+ − 702
resolve_tac (Inductive.get_monos ctxt),
+ − 703
rtac @{thm ball_all_comm},
+ − 704
rtac @{thm bex_ex_comm},
+ − 705
resolve_tac eq_eqvs,
+ − 706
simp_tac simp_ctxt])
+ − 707
end
432
+ − 708
*}
390
+ − 709
544
+ − 710
section {* Injections of rep and abses *}
383
+ − 711
381
+ − 712
(*
544
+ − 713
Injecting repabs means:
381
+ − 714
+ − 715
For abstractions:
+ − 716
* If the type of the abstraction doesn't need lifting we recurse.
+ − 717
* If it does we add RepAbs around the whole term and check if the
+ − 718
variable needs lifting.
+ − 719
* If it doesn't then we recurse
+ − 720
* If it does we recurse and put 'RepAbs' around all occurences
+ − 721
of the variable in the obtained subterm. This in combination
+ − 722
with the RepAbs above will let us change the type of the
+ − 723
abstraction with rewriting.
+ − 724
For applications:
+ − 725
* If the term is 'Respects' applied to anything we leave it unchanged
+ − 726
* If the term needs lifting and the head is a constant that we know
+ − 727
how to lift, we put a RepAbs and recurse
+ − 728
* If the term needs lifting and the head is a free applied to subterms
+ − 729
(if it is not applied we treated it in Abs branch) then we
+ − 730
put RepAbs and recurse
+ − 731
* Otherwise just recurse.
+ − 732
*)
+ − 733
336
+ − 734
ML {*
+ − 735
fun mk_repabs lthy (T, T') trm =
+ − 736
Quotient_Def.get_fun repF lthy (T, T')
354
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 737
$ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
336
+ − 738
*}
+ − 739
+ − 740
ML {*
563
+ − 741
(* bound variables need to be treated properly, *)
+ − 742
(* as the type of subterms need to be calculated *)
+ − 743
(* in the abstraction case *)
336
+ − 744
408
+ − 745
fun inj_repabs_trm lthy (rtrm, qtrm) =
563
+ − 746
case (rtrm, qtrm) of
336
+ − 747
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
408
+ − 748
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 749
336
+ − 750
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
408
+ − 751
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 752
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 753
| (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
408
+ − 754
Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 755
336
+ − 756
| (Abs (x, T, t), Abs (x', T', t')) =>
+ − 757
let
563
+ − 758
val rty = fastype_of rtrm
+ − 759
val qty = fastype_of qtrm
336
+ − 760
val (y, s) = Term.dest_abs (x, T, t)
+ − 761
val (_, s') = Term.dest_abs (x', T', t')
+ − 762
val yvar = Free (y, T)
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 763
val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
336
+ − 764
in
345
+ − 765
if rty = qty
+ − 766
then result
+ − 767
else mk_repabs lthy (rty, qty) result
336
+ − 768
end
560
+ − 769
+ − 770
| (t $ s, t' $ s') =>
+ − 771
(inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+ − 772
563
+ − 773
| (Free (_, T), Free (_, T')) =>
560
+ − 774
if T = T'
+ − 775
then rtrm
+ − 776
else mk_repabs lthy (T, T') rtrm
+ − 777
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 778
| (_, Const (@{const_name "op ="}, _)) => rtrm
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 779
576
+ − 780
(* FIXME: check here that rtrm is the corresponding definition for the const *)
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 781
| (_, Const (_, T')) =>
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 782
let
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 783
val rty = fastype_of rtrm
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 784
in
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 785
if rty = T'
560
+ − 786
then rtrm
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 787
else mk_repabs lthy (rty, T') rtrm
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 788
end
560
+ − 789
+ − 790
| _ => raise (LIFT_MATCH "injection")
336
+ − 791
*}
+ − 792
404
+ − 793
section {* RepAbs Injection Tactic *}
387
+ − 794
+ − 795
ML {*
506
+ − 796
fun quotient_tac ctxt =
468
+ − 797
REPEAT_ALL_NEW (FIRST'
542
+ − 798
[rtac @{thm identity_quotient},
510
8dbc521ee97f
Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 799
resolve_tac (quotient_rules_get ctxt)])
387
+ − 800
*}
+ − 801
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 802
(* solver for the simplifier *)
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 803
ML {*
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 804
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 805
val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 806
*}
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 807
576
+ − 808
ML {*
+ − 809
fun solve_quotient_assums ctxt thm =
+ − 810
let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
+ − 811
thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
+ − 812
end
+ − 813
handle _ => error "solve_quotient_assums"
+ − 814
*}
+ − 815
+ − 816
(* It proves the Quotient assumptions by calling quotient_tac *)
+ − 817
ML {*
+ − 818
fun solve_quotient_assum i ctxt thm =
+ − 819
let
+ − 820
val tac =
+ − 821
(compose_tac (false, thm, i)) THEN_ALL_NEW
+ − 822
(quotient_tac ctxt);
+ − 823
val gc = Drule.strip_imp_concl (cprop_of thm);
+ − 824
in
+ − 825
Goal.prove_internal [] gc (fn _ => tac 1)
+ − 826
end
+ − 827
handle _ => error "solve_quotient_assum"
+ − 828
*}
+ − 829
480
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 830
definition
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 831
"QUOT_TRUE x \<equiv> True"
472
+ − 832
387
+ − 833
ML {*
480
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 834
fun find_qt_asm asms =
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 835
let
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 836
fun find_fun trm =
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 837
case trm of
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 838
(Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 839
| _ => false
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 840
in
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 841
case find_first find_fun asms of
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 842
SOME (_ $ (_ $ (f $ a))) => (f, a)
575
334b3e9ea3e0
Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 843
| SOME _ => error "find_qt_asm: no pair"
334b3e9ea3e0
Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 844
| NONE => error "find_qt_asm: no assumption"
480
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 845
end
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 846
*}
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 847
398
+ − 848
(*
+ − 849
To prove that the regularised theorem implies the abs/rep injected,
+ − 850
we try:
+ − 851
+ − 852
1) theorems 'trans2' from the appropriate QUOT_TYPE
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 853
2) remove lambdas from both sides: lambda_rsp_tac
398
+ − 854
3) remove Ball/Bex from the right hand side
+ − 855
4) use user-supplied RSP theorems
+ − 856
5) remove rep_abs from the right side
+ − 857
6) reflexivity of equality
+ − 858
7) split applications of lifted type (apply_rsp)
+ − 859
8) split applications of non-lifted type (cong_tac)
+ − 860
9) apply extentionality
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 861
A) reflexivity of the relation
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 862
B) assumption
398
+ − 863
(Lambdas under respects may have left us some assumptions)
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 864
C) proving obvious higher order equalities by simplifying fun_rel
398
+ − 865
(not sure if it is still needed?)
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 866
D) unfolding lambda on one side
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 867
E) simplifying (= ===> =) for simpler respectfulness
398
+ − 868
+ − 869
*)
+ − 870
469
+ − 871
lemma quot_true_dests:
+ − 872
shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 873
and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
469
+ − 874
and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 875
and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 876
apply(simp_all add: QUOT_TRUE_def ext)
469
+ − 877
done
+ − 878
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 879
lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 880
by (simp add: QUOT_TRUE_def)
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 881
479
+ − 882
lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 883
by (simp add: QUOT_TRUE_def)
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 884
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 885
ML {*
479
+ − 886
fun quot_true_conv1 ctxt fnctn ctrm =
+ − 887
case (term_of ctrm) of
+ − 888
(Const (@{const_name QUOT_TRUE}, _) $ x) =>
+ − 889
let
+ − 890
val fx = fnctn x;
+ − 891
val thy = ProofContext.theory_of ctxt;
+ − 892
val cx = cterm_of thy x;
+ − 893
val cfx = cterm_of thy fx;
+ − 894
val cxt = ctyp_of thy (fastype_of x);
+ − 895
val cfxt = ctyp_of thy (fastype_of fx);
+ − 896
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
+ − 897
in
+ − 898
Conv.rewr_conv thm ctrm
+ − 899
end
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 900
*}
469
+ − 901
479
+ − 902
ML {*
+ − 903
fun quot_true_conv ctxt fnctn ctrm =
+ − 904
case (term_of ctrm) of
+ − 905
(Const (@{const_name QUOT_TRUE}, _) $ _) =>
+ − 906
quot_true_conv1 ctxt fnctn ctrm
+ − 907
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+ − 908
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+ − 909
| _ => Conv.all_conv ctrm
+ − 910
*}
+ − 911
+ − 912
ML {*
493
+ − 913
fun quot_true_tac ctxt fnctn = CONVERSION
+ − 914
((Conv.params_conv ~1 (fn ctxt =>
+ − 915
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
479
+ − 916
*}
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 917
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 918
ML {* fun dest_comb (f $ a) = (f, a) *}
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 919
ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
481
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 920
(* TODO: Can this be done easier? *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 921
ML {*
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 922
fun unlam t =
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 923
case t of
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 924
(Abs a) => snd (Term.dest_abs a)
525
+ − 925
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
398
+ − 926
*}
+ − 927
522
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 928
ML {*
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 929
fun dest_fun_type (Type("fun", [T, S])) = (T, S)
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 930
| dest_fun_type _ = error "dest_fun_type"
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 931
*}
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 932
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 933
ML {*
551
+ − 934
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
+ − 935
*}
+ − 936
+ − 937
ML {*
576
+ − 938
val apply_rsp_tac =
+ − 939
Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ − 940
case ((HOLogic.dest_Trueprop (term_of concl))) of
+ − 941
((R2 $ (f $ x) $ (g $ y))) =>
+ − 942
(let
+ − 943
val (asmf, asma) = find_qt_asm (map term_of asms);
+ − 944
in
+ − 945
if (fastype_of asmf) = (fastype_of f) then no_tac else let
+ − 946
val ty_a = fastype_of x;
+ − 947
val ty_b = fastype_of asma;
+ − 948
val ty_c = range_type (type_of f);
+ − 949
val thy = ProofContext.theory_of context;
+ − 950
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
+ − 951
val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
+ − 952
val te = solve_quotient_assums context thm
+ − 953
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+ − 954
val thm = Drule.instantiate' [] t_inst te
+ − 955
in
+ − 956
compose_tac (false, thm, 2) 1
+ − 957
end
+ − 958
end
+ − 959
handle ERROR "find_qt_asm: no pair" => no_tac)
+ − 960
| _ => no_tac)
+ − 961
*}
+ − 962
ML {*
+ − 963
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+ − 964
*}
+ − 965
+ − 966
ML {*
548
9fb773ec083c
Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 967
fun rep_abs_rsp_tac ctxt =
9fb773ec083c
Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 968
SUBGOAL (fn (goal, i) =>
551
+ − 969
case (bare_concl goal) of
+ − 970
(rel $ _ $ (rep $ (abs $ _))) =>
+ − 971
(let
+ − 972
val thy = ProofContext.theory_of ctxt;
+ − 973
val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+ − 974
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+ − 975
val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
+ − 976
val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+ − 977
val te = solve_quotient_assums ctxt thm
+ − 978
in
+ − 979
rtac te i
+ − 980
end
+ − 981
handle _ => no_tac)
+ − 982
| _ => no_tac)
522
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 983
*}
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 984
512
+ − 985
ML {*
525
+ − 986
fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
551
+ − 987
(case (bare_concl goal) of
525
+ − 988
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
536
+ − 989
((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+ − 990
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
577
+ − 991
525
+ − 992
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
512
+ − 993
| (Const (@{const_name "op ="},_) $
+ − 994
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 995
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ − 996
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
577
+ − 997
525
+ − 998
(* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
536
+ − 999
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
512
+ − 1000
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 1001
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
536
+ − 1002
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
577
+ − 1003
525
+ − 1004
(* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
512
+ − 1005
| Const (@{const_name "op ="},_) $
+ − 1006
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 1007
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 1008
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
577
+ − 1009
525
+ − 1010
(* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
536
+ − 1011
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
512
+ − 1012
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 1013
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
536
+ − 1014
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
577
+ − 1015
525
+ − 1016
(* reflexivity of operators arising from Cong_tac *)
577
+ − 1017
| Const (@{const_name "op ="},_) $ _ $ _
+ − 1018
=> rtac @{thm refl} ORELSE'
+ − 1019
(resolve_tac trans2 THEN' RANGE [
+ − 1020
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+ − 1021
561
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1022
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1023
(Const (@{const_name fun_rel}, _) $ _ $ _) $
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1024
(Const (@{const_name fun_rel}, _) $ _ $ _)
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1025
=> rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
577
+ − 1026
+ − 1027
(* respectfulness of constants; in particular of a simple relation *)
+ − 1028
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ − 1029
=> resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+ − 1030
525
+ − 1031
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+ − 1032
(* observe ---> *)
577
+ − 1033
| _ $ _ $ _
+ − 1034
=> rep_abs_rsp_tac ctxt
+ − 1035
522
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1036
| _ => error "inj_repabs_tac not a relation"
512
+ − 1037
) i)
+ − 1038
*}
+ − 1039
+ − 1040
ML {*
525
+ − 1041
fun inj_repabs_tac ctxt rel_refl trans2 =
512
+ − 1042
(FIRST' [
525
+ − 1043
inj_repabs_tac_match ctxt trans2,
527
+ − 1044
(* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *)
+ − 1045
NDT ctxt "A" (apply_rsp_tac ctxt THEN'
517
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1046
(RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
525
+ − 1047
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
+ − 1048
(* merge with previous tactic *)
512
+ − 1049
NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+ − 1050
(RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
525
+ − 1051
(* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
512
+ − 1052
NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
525
+ − 1053
(* resolving with R x y assumptions *)
512
+ − 1054
NDT ctxt "E" (atac),
525
+ − 1055
(* reflexivity of the basic relations *)
+ − 1056
(* R \<dots> \<dots> *)
555
b460565dbb58
Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1057
NDT ctxt "D" (resolve_tac rel_refl)
515
+ − 1058
])
512
+ − 1059
*}
+ − 1060
+ − 1061
ML {*
525
+ − 1062
fun all_inj_repabs_tac ctxt rel_refl trans2 =
+ − 1063
REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
512
+ − 1064
*}
+ − 1065
399
+ − 1066
section {* Cleaning of the theorem *}
387
+ − 1067
+ − 1068
ML {*
440
+ − 1069
fun make_inst lhs t =
+ − 1070
let
+ − 1071
val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ − 1072
val _ $ (Abs (_, _, g)) = t;
+ − 1073
fun mk_abs i t =
+ − 1074
if incr_boundvars i u aconv t then Bound i
+ − 1075
else (case t of
+ − 1076
t1 $ t2 => mk_abs i t1 $ mk_abs i t2
469
+ − 1077
| Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
440
+ − 1078
| Bound j => if i = j then error "make_inst" else t
+ − 1079
| _ => t);
+ − 1080
in (f, Abs ("x", T, mk_abs 0 g)) end;
490
+ − 1081
*}
440
+ − 1082
492
+ − 1083
ML {*
571
+ − 1084
fun lambda_prs_simple_conv ctxt ctrm =
492
+ − 1085
case (term_of ctrm) of
586
+ − 1086
((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1087
let
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1088
val thy = ProofContext.theory_of ctxt
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1089
val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1090
val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1091
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1092
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1093
val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1094
val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1095
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1096
val tl = Thm.lhs_of ts
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1097
val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1098
val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
586
+ − 1099
val _ = if not (s = @{const_name "id"}) then
+ − 1100
(tracing "lambda_prs";
+ − 1101
tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+ − 1102
tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
+ − 1103
tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
+ − 1104
tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+ − 1105
tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
+ − 1106
else ()
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1107
in
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1108
Conv.rewr_conv ti ctrm
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1109
end
490
+ − 1110
| _ => Conv.all_conv ctrm
387
+ − 1111
*}
+ − 1112
+ − 1113
ML {*
571
+ − 1114
val lambda_prs_conv =
+ − 1115
More_Conv.top_conv lambda_prs_simple_conv
387
+ − 1116
571
+ − 1117
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
387
+ − 1118
*}
+ − 1119
457
+ − 1120
(*
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1121
Cleaning the theorem consists of three rewriting steps.
465
+ − 1122
The first two need to be done before fun_map is unfolded
457
+ − 1123
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1124
1) lambda_prs:
469
+ − 1125
(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
+ − 1126
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1127
Implemented as conversion since it is not a pattern.
469
+ − 1128
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1129
2) all_prs (the same for exists):
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1130
Ball (Respects R) ((abs ---> id) f) ----> All f
469
+ − 1131
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1132
Rewriting with definitions from the argument defs
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1133
(rep ---> abs) oldConst ----> newconst
469
+ − 1134
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1135
3) Quotient_rel_rep:
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1136
Rel (Rep x) (Rep y) ----> x = y
469
+ − 1137
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1138
Quotient_abs_rep:
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1139
Abs (Rep x) ----> x
457
+ − 1140
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1141
id_simps; fun_map.simps
457
+ − 1142
*)
469
+ − 1143
556
+ − 1144
ML {*
506
+ − 1145
fun clean_tac lthy =
387
+ − 1146
let
498
+ − 1147
val thy = ProofContext.theory_of lthy;
566
+ − 1148
val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1149
(* FIXME: shouldn't the definitions already be varified? *)
567
+ − 1150
val thms1 = @{thms all_prs ex_prs} @ defs
564
96c241932603
moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1151
val thms2 = @{thms eq_reflection[OF fun_map.simps]}
96c241932603
moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1152
@ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1153
fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1154
(* FIXME: use of someting smaller than HOL_basic_ss *)
387
+ − 1155
in
572
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1156
EVERY' [lambda_prs_tac lthy,
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1157
simp_tac (simps thms1),
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1158
simp_tac (simps thms2),
a68c51dd85b3
working on lambda_prs with examples; polished code of clean_tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1159
TRY o rtac refl]
387
+ − 1160
end
+ − 1161
*}
381
+ − 1162
404
+ − 1163
section {* Genralisation of free variables in a goal *}
347
+ − 1164
+ − 1165
ML {*
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1166
fun inst_spec ctrm =
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1167
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1168
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1169
fun inst_spec_tac ctrms =
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1170
EVERY' (map (dtac o inst_spec) ctrms)
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1171
412
+ − 1172
fun all_list xs trm =
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1173
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1174
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1175
fun apply_under_Trueprop f =
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1176
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
362
+ − 1177
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1178
fun gen_frees_tac ctxt =
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1179
SUBGOAL (fn (concl, i) =>
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1180
let
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1181
val thy = ProofContext.theory_of ctxt
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1182
val vrs = Term.add_frees concl []
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1183
val cvrs = map (cterm_of thy o Free) vrs
412
+ − 1184
val concl' = apply_under_Trueprop (all_list vrs) concl
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1185
val goal = Logic.mk_implies (concl', concl)
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1186
val rule = Goal.prove ctxt [] [] goal
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1187
(K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1188
in
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1189
rtac rule i
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1190
end)
362
+ − 1191
*}
+ − 1192
402
+ − 1193
section {* General outline of the lifting procedure *}
+ − 1194
383
+ − 1195
(* - A is the original raw theorem *)
+ − 1196
(* - B is the regularized theorem *)
+ − 1197
(* - C is the rep/abs injected version of B *)
+ − 1198
(* - D is the lifted theorem *)
+ − 1199
(* *)
+ − 1200
(* - b is the regularization step *)
+ − 1201
(* - c is the rep/abs injection step *)
+ − 1202
(* - d is the cleaning part *)
+ − 1203
413
+ − 1204
lemma lifting_procedure:
360
+ − 1205
assumes a: "A"
+ − 1206
and b: "A \<Longrightarrow> B"
+ − 1207
and c: "B = C"
+ − 1208
and d: "C = D"
+ − 1209
shows "D"
+ − 1210
using a b c d
+ − 1211
by simp
+ − 1212
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1213
ML {*
412
+ − 1214
fun lift_match_error ctxt fun_str rtrm qtrm =
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1215
let
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1216
val rtrm_str = Syntax.string_of_term ctxt rtrm
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1217
val qtrm_str = Syntax.string_of_term ctxt qtrm
388
+ − 1218
val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str,
+ − 1219
"and the lifted theorem\n", rtrm_str, "do not match"]
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1220
in
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1221
error (space_implode " " msg)
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1222
end
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1223
*}
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1224
360
+ − 1225
ML {*
+ − 1226
fun procedure_inst ctxt rtrm qtrm =
+ − 1227
let
+ − 1228
val thy = ProofContext.theory_of ctxt
+ − 1229
val rtrm' = HOLogic.dest_Trueprop rtrm
+ − 1230
val qtrm' = HOLogic.dest_Trueprop qtrm
383
+ − 1231
val reg_goal =
405
+ − 1232
Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
412
+ − 1233
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
564
96c241932603
moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1234
val _ = warning "Regularization done."
383
+ − 1235
val inj_goal =
408
+ − 1236
Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
412
+ − 1237
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
564
96c241932603
moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1238
val _ = warning "RepAbs Injection done."
360
+ − 1239
in
+ − 1240
Drule.instantiate' []
+ − 1241
[SOME (cterm_of thy rtrm'),
+ − 1242
SOME (cterm_of thy reg_goal),
413
+ − 1243
SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
360
+ − 1244
end
362
+ − 1245
*}
389
+ − 1246
+ − 1247
(* Left for debugging *)
362
+ − 1248
ML {*
547
+ − 1249
fun procedure_tac ctxt rthm =
389
+ − 1250
ObjectLogic.full_atomize_tac
547
+ − 1251
THEN' gen_frees_tac ctxt
+ − 1252
THEN' CSUBGOAL (fn (gl, i) =>
389
+ − 1253
let
+ − 1254
val rthm' = atomize_thm rthm
547
+ − 1255
val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
+ − 1256
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
389
+ − 1257
in
547
+ − 1258
(rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i
+ − 1259
end)
360
+ − 1260
*}
+ − 1261
361
+ − 1262
ML {*
413
+ − 1263
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
489
+ − 1264
582
+ − 1265
fun lift_tac ctxt rthm =
389
+ − 1266
ObjectLogic.full_atomize_tac
547
+ − 1267
THEN' gen_frees_tac ctxt
+ − 1268
THEN' CSUBGOAL (fn (gl, i) =>
389
+ − 1269
let
+ − 1270
val rthm' = atomize_thm rthm
547
+ − 1271
val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
582
+ − 1272
val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
547
+ − 1273
val quotients = quotient_rules_get ctxt
527
+ − 1274
val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
547
+ − 1275
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
389
+ − 1276
in
547
+ − 1277
(rtac rule THEN'
+ − 1278
RANGE [rtac rthm',
582
+ − 1279
regularize_tac ctxt,
547
+ − 1280
rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
+ − 1281
clean_tac ctxt]) i
+ − 1282
end)
361
+ − 1283
*}
+ − 1284
198
+ − 1285
end
239
+ − 1286