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
419
+ − 139
lemma tst: "EQUIV bla"
+ − 140
sorry
+ − 141
+ − 142
lemma equiv_trans2:
+ − 143
assumes e: "EQUIV R"
+ − 144
and ac: "R a c"
+ − 145
and bd: "R b d"
+ − 146
shows "R a b = R c d"
+ − 147
using ac bd e
+ − 148
unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def
+ − 149
by (blast)
+ − 150
0
+ − 151
section {* type definition for the quotient type *}
+ − 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
(* the auxiliary data for the quotient types *)
264
+ − 154
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
+ − 155
185
+ − 156
declare [[map list = (map, LIST_REL)]]
+ − 157
declare [[map * = (prod_fun, prod_rel)]]
+ − 158
declare [[map "fun" = (fun_map, FUN_REL)]]
+ − 159
+ − 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
(* TODO: Consider defining it with an "if"; sth like:
+ − 174
Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+ − 175
*)
+ − 176
definition
+ − 177
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ − 178
where
+ − 179
"(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
+ − 180
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 181
139
+ − 182
section {* ATOMIZE *}
+ − 183
381
+ − 184
lemma atomize_eqv[atomize]:
+ − 185
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
139
+ − 186
proof
381
+ − 187
assume "A \<equiv> B"
139
+ − 188
then show "Trueprop A \<equiv> Trueprop B" by unfold
+ − 189
next
+ − 190
assume *: "Trueprop A \<equiv> Trueprop B"
+ − 191
have "A = B"
+ − 192
proof (cases A)
+ − 193
case True
+ − 194
have "A" by fact
+ − 195
then show "A = B" using * by simp
+ − 196
next
+ − 197
case False
+ − 198
have "\<not>A" by fact
+ − 199
then show "A = B" using * by auto
+ − 200
qed
+ − 201
then show "A \<equiv> B" by (rule eq_reflection)
+ − 202
qed
+ − 203
+ − 204
ML {*
+ − 205
fun atomize_thm thm =
+ − 206
let
221
+ − 207
val thm' = Thm.freezeT (forall_intr_vars thm)
139
+ − 208
val thm'' = ObjectLogic.atomize (cprop_of thm')
+ − 209
in
404
+ − 210
@{thm equal_elim_rule1} OF [thm'', thm']
139
+ − 211
end
+ − 212
*}
+ − 213
387
+ − 214
section {* infrastructure about id *}
381
+ − 215
+ − 216
lemma prod_fun_id: "prod_fun id id \<equiv> id"
415
+ − 217
by (rule eq_reflection) (simp add: prod_fun_def)
381
+ − 218
+ − 219
lemma map_id: "map id \<equiv> id"
415
+ − 220
apply (rule eq_reflection)
+ − 221
apply (rule ext)
+ − 222
apply (rule_tac list="x" in list.induct)
+ − 223
apply (simp_all)
+ − 224
done
381
+ − 225
409
+ − 226
lemmas id_simps =
+ − 227
FUN_MAP_I[THEN eq_reflection]
+ − 228
id_apply[THEN eq_reflection]
415
+ − 229
id_def[THEN eq_reflection,symmetric]
+ − 230
prod_fun_id map_id
409
+ − 231
381
+ − 232
ML {*
409
+ − 233
fun simp_ids thm =
+ − 234
MetaSimplifier.rewrite_rule @{thms id_simps} thm
381
+ − 235
*}
+ − 236
407
+ − 237
section {* Debugging infrastructure for testing tactics *}
381
+ − 238
+ − 239
ML {*
407
+ − 240
fun my_print_tac ctxt s thm =
+ − 241
let
+ − 242
val prems_str = prems_of thm
+ − 243
|> map (Syntax.string_of_term ctxt)
+ − 244
|> cat_lines
+ − 245
val _ = tracing (s ^ "\n" ^ prems_str)
+ − 246
in
+ − 247
Seq.single thm
+ − 248
end
+ − 249
+ − 250
fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
+ − 251
*}
+ − 252
+ − 253
section {* Infrastructure about definitions *}
+ − 254
+ − 255
(* Does the same as 'subst' in a given theorem *)
+ − 256
ML {*
381
+ − 257
fun eqsubst_thm ctxt thms thm =
+ − 258
let
+ − 259
val goalstate = Goal.init (Thm.cprop_of thm)
+ − 260
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+ − 261
NONE => error "eqsubst_thm"
+ − 262
| SOME th => cprem_of th 1
+ − 263
val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+ − 264
val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
+ − 265
val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
+ − 266
val rt = Goal.prove_internal [] cgoal (fn _ => tac);
+ − 267
in
402
+ − 268
@{thm equal_elim_rule1} OF [rt, thm]
381
+ − 269
end
+ − 270
*}
+ − 271
404
+ − 272
(* expects atomized definitions *)
381
+ − 273
ML {*
+ − 274
fun add_lower_defs_aux lthy thm =
+ − 275
let
+ − 276
val e1 = @{thm fun_cong} OF [thm];
+ − 277
val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
409
+ − 278
val g = simp_ids f
381
+ − 279
in
409
+ − 280
(simp_ids thm) :: (add_lower_defs_aux lthy g)
381
+ − 281
end
409
+ − 282
handle _ => [simp_ids thm]
381
+ − 283
*}
+ − 284
+ − 285
ML {*
+ − 286
fun add_lower_defs lthy def =
+ − 287
let
+ − 288
val def_pre_sym = symmetric def
+ − 289
val def_atom = atomize_thm def_pre_sym
+ − 290
val defs_all = add_lower_defs_aux lthy def_atom
+ − 291
in
+ − 292
map Thm.varifyT defs_all
+ − 293
end
+ − 294
*}
+ − 295
407
+ − 296
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
+ − 297
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 298
ML {*
239
+ − 299
fun lookup_quot_data lthy qty =
+ − 300
let
311
+ − 301
val qty_name = fst (dest_Type qty)
314
+ − 302
val SOME quotdata = quotdata_lookup lthy qty_name
311
+ − 303
(* cu: Changed the lookup\<dots>not sure whether this works *)
303
+ − 304
(* TODO: Should no longer be needed *)
257
+ − 305
val rty = Logic.unvarifyT (#rtyp quotdata)
239
+ − 306
val rel = #rel quotdata
+ − 307
val rel_eqv = #equiv_thm quotdata
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 308
val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv]
239
+ − 309
in
+ − 310
(rty, rel, rel_refl, rel_eqv)
+ − 311
end
+ − 312
*}
+ − 313
+ − 314
ML {*
+ − 315
fun lookup_quot_thms lthy qty_name =
+ − 316
let
+ − 317
val thy = ProofContext.theory_of lthy;
+ − 318
val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
+ − 319
val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
269
+ − 320
val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
239
+ − 321
val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
+ − 322
in
269
+ − 323
(trans2, reps_same, absrep, quot)
239
+ − 324
end
+ − 325
*}
+ − 326
+ − 327
ML {*
+ − 328
fun lookup_quot_consts defs =
+ − 329
let
+ − 330
fun dest_term (a $ b) = (a, b);
+ − 331
val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
+ − 332
in
+ − 333
map (fst o dest_Const o snd o dest_term) def_terms
+ − 334
end
+ − 335
*}
+ − 336
402
+ − 337
section {* Regularization *}
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 338
383
+ − 339
(*
+ − 340
Regularizing an rtrm means:
+ − 341
- quantifiers over a type that needs lifting are replaced by
+ − 342
bounded quantifiers, for example:
+ − 343
\<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
+ − 344
+ − 345
the relation R is given by the rty and qty;
330
+ − 346
383
+ − 347
- abstractions over a type that needs lifting are replaced
+ − 348
by bounded abstractions:
+ − 349
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+ − 350
+ − 351
- equalities over the type being lifted are replaced by
+ − 352
corresponding relations:
+ − 353
A = B \<Longrightarrow> A \<approx> B
+ − 354
+ − 355
example with more complicated types of A, B:
+ − 356
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+ − 357
*)
+ − 358
404
+ − 359
ML {*
383
+ − 360
(* 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
+ − 361
fun mk_resp_arg lthy (rty, qty) =
319
+ − 362
let
+ − 363
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
+ − 364
in
334
+ − 365
if rty = qty
+ − 366
then HOLogic.eq_const rty
+ − 367
else
+ − 368
case (rty, qty) of
+ − 369
(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
+ − 370
if s = s'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 371
then let
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 372
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
+ − 373
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
+ − 374
in
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 375
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
+ − 376
end
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 377
else let
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 378
val SOME qinfo = quotdata_lookup_thy thy s'
330
+ − 379
(* FIXME: check in this case that the rty and qty *)
+ − 380
(* 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
+ − 381
val (s, _) = dest_Const (#rel qinfo)
407
+ − 382
(* FIXME: the relation should only be the string *)
+ − 383
(* FIXME: and the type needs to be calculated as below; *)
+ − 384
(* FIXME: maybe one should actually have a term *)
+ − 385
(* 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
+ − 386
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
+ − 387
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
+ − 388
end
334
+ − 389
| _ => HOLogic.eq_const dummyT
351
+ − 390
(* 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
+ − 391
end
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 392
*}
239
+ − 393
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 394
ML {*
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 395
val mk_babs = Const (@{const_name "Babs"}, dummyT)
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 396
val mk_ball = Const (@{const_name "Ball"}, dummyT)
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 397
val mk_bex = Const (@{const_name "Bex"}, dummyT)
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 398
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
+ − 399
*}
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 400
323
+ − 401
ML {*
330
+ − 402
(* - applies f to the subterm of an abstraction, *)
+ − 403
(* otherwise to the given term, *)
405
+ − 404
(* - used by regularize, therefore abstracted *)
330
+ − 405
(* variables do not have to be treated specially *)
+ − 406
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 407
fun apply_subt f trm1 trm2 =
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
case (trm1, trm2) of
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 409
(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
+ − 410
| _ => f trm1 trm2
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 411
330
+ − 412
(* the major type of All and Ex quantifiers *)
334
+ − 413
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
+ − 414
*}
319
+ − 415
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 416
ML {*
330
+ − 417
(* produces a regularized version of rtm *)
+ − 418
(* - the result is still not completely typed *)
+ − 419
(* - does not need any special treatment of *)
+ − 420
(* bound variables *)
+ − 421
405
+ − 422
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
+ − 423
case (rtrm, qtrm) of
325
+ − 424
(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
+ − 425
let
405
+ − 426
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
+ − 427
in
325
+ − 428
if ty = ty'
+ − 429
then Abs (x, ty, subtrm)
326
+ − 430
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
+ − 431
end
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 432
| (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
+ − 433
let
405
+ − 434
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
+ − 435
in
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 436
if ty = ty'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 437
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
+ − 438
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
+ − 439
end
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 440
| (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
+ − 441
let
405
+ − 442
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
+ − 443
in
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 444
if ty = ty'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 445
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
+ − 446
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
+ − 447
end
351
+ − 448
(* FIXME: Should = only be replaced, when fully applied? *)
+ − 449
(* Then there must be a 2nd argument *)
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
| (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
let
405
+ − 452
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
+ − 453
in
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
if ty = ty'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
then Const (@{const_name "op ="}, ty) $ subtrm
349
+ − 456
else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 457
end
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 458
| (t1 $ t2, t1' $ t2') =>
405
+ − 459
(regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 460
| (Free (x, ty), Free (x', ty')) =>
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 461
if x = x'
330
+ − 462
then rtrm (* FIXME: check whether types corresponds *)
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 463
else raise (LIFT_MATCH "regularize (frees)")
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 464
| (Bound i, Bound i') =>
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 465
if i = i'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
then rtrm
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
else raise (LIFT_MATCH "regularize (bounds)")
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 468
| (Const (s, ty), Const (s', ty')) =>
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 469
if s = s' andalso ty = ty'
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
then rtrm
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 471
else rtrm (* FIXME: check correspondence according to definitions *)
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 472
| (rt, qt) =>
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 473
raise (LIFT_MATCH "regularize (default)")
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 474
*}
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 476
(*
407
+ − 477
FIXME / TODO: needs to be adapted
+ − 478
383
+ − 479
To prove that the raw theorem implies the regularised one,
+ − 480
we try in order:
330
+ − 481
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 482
- 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
+ − 483
- Assumption
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 484
- 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
+ − 485
- 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
+ − 486
- 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
+ − 487
- (\<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
+ − 488
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
*)
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 490
381
+ − 491
lemma universal_twice:
+ − 492
assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
+ − 493
shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
+ − 494
using * by auto
+ − 495
+ − 496
lemma implication_twice:
+ − 497
assumes a: "c \<longrightarrow> a"
390
+ − 498
assumes b: "b \<longrightarrow> d"
381
+ − 499
shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+ − 500
using a b by auto
+ − 501
405
+ − 502
(* version of regularize_tac including debugging information *)
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 503
ML {*
383
+ − 504
fun regularize_tac ctxt rel_eqv rel_refl =
+ − 505
(ObjectLogic.full_atomize_tac) THEN'
400
+ − 506
REPEAT_ALL_NEW (FIRST'
+ − 507
[(K (print_tac "start")) THEN' (K no_tac),
420
+ − 508
DT ctxt "1" (resolve_tac rel_refl),
390
+ − 509
DT ctxt "2" atac,
+ − 510
DT ctxt "3" (rtac @{thm universal_twice}),
+ − 511
DT ctxt "4" (rtac @{thm impI} THEN' atac),
+ − 512
DT ctxt "5" (rtac @{thm implication_twice}),
+ − 513
DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
+ − 514
[(@{thm equiv_res_forall} OF [rel_eqv]),
+ − 515
(@{thm equiv_res_exists} OF [rel_eqv])]),
+ − 516
(* For a = b \<longrightarrow> a \<approx> b *)
420
+ − 517
DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)),
390
+ − 518
DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+ − 519
]);
+ − 520
*}
+ − 521
404
+ − 522
lemma move_forall:
+ − 523
"(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
400
+ − 524
by auto
+ − 525
404
+ − 526
lemma move_exists:
+ − 527
"((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
400
+ − 528
by auto
+ − 529
404
+ − 530
lemma [mono]:
+ − 531
"(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
400
+ − 532
by blast
+ − 533
+ − 534
lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
+ − 535
by auto
+ − 536
+ − 537
lemma ball_respects_refl:
+ − 538
fixes P Q::"'a \<Rightarrow> bool"
+ − 539
and x::"'a"
+ − 540
assumes a: "EQUIV R2"
+ − 541
and b: "\<And>f. Q (f x) \<longrightarrow> P (f x)"
+ − 542
shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))"
+ − 543
apply(rule impI)
+ − 544
apply(rule allI)
+ − 545
apply(drule_tac x="\<lambda>y. f x" in bspec)
+ − 546
apply(simp add: Respects_def IN_RESPECTS)
+ − 547
apply(rule impI)
+ − 548
using a EQUIV_REFL_SYM_TRANS[of "R2"]
+ − 549
apply(simp add: REFL_def)
+ − 550
using b
+ − 551
apply(simp)
+ − 552
done
+ − 553
+ − 554
lemma bex_respects_refl:
+ − 555
fixes P Q::"'a \<Rightarrow> bool"
+ − 556
and x::"'a"
+ − 557
assumes a: "EQUIV R2"
+ − 558
and b: "\<And>f. P (f x) \<longrightarrow> Q (f x)"
+ − 559
shows "(Ex (\<lambda>f. P (f x))) \<longrightarrow> (Bex (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)))"
+ − 560
apply(rule impI)
+ − 561
apply(erule exE)
+ − 562
thm bexI
+ − 563
apply(rule_tac x="\<lambda>y. f x" in bexI)
+ − 564
using b
+ − 565
apply(simp)
+ − 566
apply(simp add: Respects_def IN_RESPECTS)
+ − 567
apply(rule impI)
+ − 568
using a EQUIV_REFL_SYM_TRANS[of "R2"]
+ − 569
apply(simp add: REFL_def)
+ − 570
done
+ − 571
+ − 572
(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
+ − 573
ML {*
+ − 574
fun equiv_tac rel_eqvs =
420
+ − 575
REPEAT_ALL_NEW (FIRST'
+ − 576
[resolve_tac rel_eqvs,
+ − 577
rtac @{thm IDENTITY_EQUIV},
+ − 578
rtac @{thm LIST_EQUIV}])
400
+ − 579
*}
+ − 580
+ − 581
ML {*
+ − 582
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+ − 583
*}
+ − 584
+ − 585
ML {*
+ − 586
fun regularize_tac ctxt rel_eqvs rel_refl =
+ − 587
let
+ − 588
val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs
+ − 589
val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs
+ − 590
val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2)
+ − 591
in
+ − 592
(ObjectLogic.full_atomize_tac) THEN'
+ − 593
(simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs))
+ − 594
THEN'
420
+ − 595
REPEAT_ALL_NEW (FIRST'
+ − 596
[(rtac @{thm RIGHT_RES_FORALL_REGULAR}),
+ − 597
(rtac @{thm LEFT_RES_EXISTS_REGULAR}),
+ − 598
(resolve_tac (Inductive.get_monos ctxt)),
+ − 599
(rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ − 600
(rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ − 601
rtac @{thm move_forall},
+ − 602
rtac @{thm move_exists},
+ − 603
(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))])
400
+ − 604
end
+ − 605
*}
390
+ − 606
+ − 607
section {* Injections of REP and ABSes *}
383
+ − 608
381
+ − 609
(*
+ − 610
Injecting REPABS means:
+ − 611
+ − 612
For abstractions:
+ − 613
* If the type of the abstraction doesn't need lifting we recurse.
+ − 614
* If it does we add RepAbs around the whole term and check if the
+ − 615
variable needs lifting.
+ − 616
* If it doesn't then we recurse
+ − 617
* If it does we recurse and put 'RepAbs' around all occurences
+ − 618
of the variable in the obtained subterm. This in combination
+ − 619
with the RepAbs above will let us change the type of the
+ − 620
abstraction with rewriting.
+ − 621
For applications:
+ − 622
* If the term is 'Respects' applied to anything we leave it unchanged
+ − 623
* If the term needs lifting and the head is a constant that we know
+ − 624
how to lift, we put a RepAbs and recurse
+ − 625
* If the term needs lifting and the head is a free applied to subterms
+ − 626
(if it is not applied we treated it in Abs branch) then we
+ − 627
put RepAbs and recurse
+ − 628
* Otherwise just recurse.
+ − 629
*)
+ − 630
336
+ − 631
ML {*
+ − 632
fun mk_repabs lthy (T, T') trm =
+ − 633
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
+ − 634
$ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
336
+ − 635
*}
+ − 636
+ − 637
ML {*
+ − 638
(* bound variables need to be treated properly, *)
+ − 639
(* as the type of subterms need to be calculated *)
+ − 640
408
+ − 641
fun inj_repabs_trm lthy (rtrm, qtrm) =
336
+ − 642
let
+ − 643
val rty = fastype_of rtrm
+ − 644
val qty = fastype_of qtrm
+ − 645
in
+ − 646
case (rtrm, qtrm) of
+ − 647
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
408
+ − 648
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
336
+ − 649
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
408
+ − 650
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
336
+ − 651
| (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
408
+ − 652
Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
336
+ − 653
| (Abs (x, T, t), Abs (x', T', t')) =>
+ − 654
let
+ − 655
val (y, s) = Term.dest_abs (x, T, t)
+ − 656
val (_, s') = Term.dest_abs (x', T', t')
+ − 657
val yvar = Free (y, T)
408
+ − 658
val result = lambda yvar (inj_repabs_trm lthy (s, s'))
336
+ − 659
in
345
+ − 660
if rty = qty
+ − 661
then result
+ − 662
else mk_repabs lthy (rty, qty) result
336
+ − 663
end
+ − 664
| _ =>
345
+ − 665
(* FIXME / TODO: this is a case that needs to be looked at *)
+ − 666
(* - variables get a rep-abs insde and outside an application *)
+ − 667
(* - constants only get a rep-abs on the outside of the application *)
+ − 668
(* - applications get a rep-abs insde and outside an application *)
336
+ − 669
let
+ − 670
val (rhead, rargs) = strip_comb rtrm
+ − 671
val (qhead, qargs) = strip_comb qtrm
408
+ − 672
val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
336
+ − 673
in
345
+ − 674
if rty = qty
355
+ − 675
then
+ − 676
case (rhead, qhead) of
+ − 677
(Free (_, T), Free (_, T')) =>
+ − 678
if T = T' then list_comb (rhead, rargs')
+ − 679
else list_comb (mk_repabs lthy (T, T') rhead, rargs')
+ − 680
| _ => list_comb (rhead, rargs')
345
+ − 681
else
+ − 682
case (rhead, qhead, length rargs') of
+ − 683
(Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead
355
+ − 684
| (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead
345
+ − 685
| (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs'))
+ − 686
| (Free (x, T), Free (x', T'), _) =>
+ − 687
mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
+ − 688
| (Abs _, Abs _, _ ) =>
408
+ − 689
mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs'))
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 690
| _ => raise (LIFT_MATCH "injection")
336
+ − 691
end
+ − 692
end
+ − 693
*}
+ − 694
404
+ − 695
section {* RepAbs Injection Tactic *}
387
+ − 696
(*
+ − 697
To prove that the regularised theorem implies the abs/rep injected, we first
+ − 698
atomize it and then try:
+ − 699
+ − 700
1) theorems 'trans2' from the appropriate QUOT_TYPE
+ − 701
2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ − 702
3) remove Ball/Bex from the right hand side
+ − 703
4) use user-supplied RSP theorems
+ − 704
5) remove rep_abs from the right side
+ − 705
6) reflexivity of equality
+ − 706
7) split applications of lifted type (apply_rsp)
+ − 707
8) split applications of non-lifted type (cong_tac)
+ − 708
9) apply extentionality
+ − 709
10) reflexivity of the relation
+ − 710
11) assumption
+ − 711
(Lambdas under respects may have left us some assumptions)
+ − 712
12) proving obvious higher order equalities by simplifying fun_rel
+ − 713
(not sure if it is still needed?)
+ − 714
13) unfolding lambda on one side
+ − 715
14) simplifying (= ===> =) for simpler respectfullness
+ − 716
+ − 717
*)
+ − 718
+ − 719
ML {*
+ − 720
fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+ − 721
let
+ − 722
val pat = Drule.strip_imp_concl (cprop_of thm)
+ − 723
val insts = Thm.match (pat, concl)
+ − 724
in
+ − 725
rtac (Drule.instantiate insts thm) 1
+ − 726
end
+ − 727
handle _ => no_tac)
+ − 728
*}
+ − 729
+ − 730
+ − 731
ML {*
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 732
fun quotient_tac quot_thms =
420
+ − 733
REPEAT_ALL_NEW (FIRST'
+ − 734
[rtac @{thm FUN_QUOTIENT},
+ − 735
resolve_tac quot_thms,
+ − 736
rtac @{thm IDENTITY_QUOTIENT},
+ − 737
(* For functional identity quotients, (op = ---> op =) *)
+ − 738
(* TODO: think about the other way around, if we need to shorten the relation *)
+ − 739
CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
387
+ − 740
*}
+ − 741
+ − 742
ML {*
+ − 743
fun LAMBDA_RES_TAC ctxt i st =
+ − 744
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ − 745
(_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
+ − 746
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 747
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 748
| _ => fn _ => no_tac) i st
+ − 749
*}
+ − 750
+ − 751
ML {*
+ − 752
fun WEAK_LAMBDA_RES_TAC ctxt i st =
+ − 753
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ − 754
(_ $ (_ $ _ $ (Abs(_, _, _)))) =>
+ − 755
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 756
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 757
| (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
+ − 758
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ − 759
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ − 760
| _ => fn _ => no_tac) i st
+ − 761
*}
+ − 762
+ − 763
ML {* (* Legacy *)
+ − 764
fun needs_lift (rty as Type (rty_s, _)) ty =
+ − 765
case ty of
+ − 766
Type (s, tys) =>
+ − 767
(s = rty_s) orelse (exists (needs_lift rty) tys)
+ − 768
| _ => false
+ − 769
+ − 770
*}
+ − 771
+ − 772
ML {*
+ − 773
fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
+ − 774
let
+ − 775
val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
+ − 776
val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+ − 777
val insts = Thm.match (pat, concl)
+ − 778
in
+ − 779
if needs_lift rty (type_of f) then
+ − 780
rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+ − 781
else no_tac
+ − 782
end
+ − 783
handle _ => no_tac)
+ − 784
*}
+ − 785
+ − 786
ML {*
+ − 787
val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ − 788
let
+ − 789
val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
+ − 790
(Const (@{const_name Ball}, _) $ _)) = term_of concl
+ − 791
in
+ − 792
((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+ − 793
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+ − 794
THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+ − 795
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+ − 796
end
+ − 797
handle _ => no_tac)
+ − 798
*}
+ − 799
+ − 800
ML {*
+ − 801
val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ − 802
let
+ − 803
val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
+ − 804
(Const (@{const_name Bex}, _) $ _)) = term_of concl
+ − 805
in
+ − 806
((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+ − 807
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+ − 808
THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+ − 809
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+ − 810
end
+ − 811
handle _ => no_tac)
+ − 812
*}
+ − 813
+ − 814
ML {*
419
+ − 815
fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
387
+ − 816
(FIRST' [
420
+ − 817
resolve_tac trans2,
387
+ − 818
LAMBDA_RES_TAC ctxt,
389
+ − 819
rtac @{thm RES_FORALL_RSP},
387
+ − 820
ball_rsp_tac ctxt,
389
+ − 821
rtac @{thm RES_EXISTS_RSP},
387
+ − 822
bex_rsp_tac ctxt,
420
+ − 823
resolve_tac rsp_thms,
+ − 824
rtac @{thm refl},
404
+ − 825
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 826
(RANGE [SOLVES' (quotient_tac quot_thms)])),
404
+ − 827
(APPLY_RSP_TAC rty ctxt THEN'
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 828
(RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
387
+ − 829
Cong_Tac.cong_tac @{thm cong},
+ − 830
rtac @{thm ext},
420
+ − 831
resolve_tac rel_refl,
387
+ − 832
atac,
+ − 833
SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
+ − 834
WEAK_LAMBDA_RES_TAC ctxt,
410
+ − 835
CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
387
+ − 836
])
+ − 837
*}
+ − 838
398
+ − 839
(*
+ − 840
To prove that the regularised theorem implies the abs/rep injected,
+ − 841
we try:
+ − 842
+ − 843
1) theorems 'trans2' from the appropriate QUOT_TYPE
+ − 844
2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ − 845
3) remove Ball/Bex from the right hand side
+ − 846
4) use user-supplied RSP theorems
+ − 847
5) remove rep_abs from the right side
+ − 848
6) reflexivity of equality
+ − 849
7) split applications of lifted type (apply_rsp)
+ − 850
8) split applications of non-lifted type (cong_tac)
+ − 851
9) apply extentionality
+ − 852
10) reflexivity of the relation
+ − 853
11) assumption
+ − 854
(Lambdas under respects may have left us some assumptions)
+ − 855
12) proving obvious higher order equalities by simplifying fun_rel
+ − 856
(not sure if it is still needed?)
+ − 857
13) unfolding lambda on one side
+ − 858
14) simplifying (= ===> =) for simpler respectfulness
+ − 859
+ − 860
*)
+ − 861
+ − 862
ML {*
420
+ − 863
fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
398
+ − 864
REPEAT_ALL_NEW (FIRST' [
+ − 865
(K (print_tac "start")) THEN' (K no_tac),
420
+ − 866
DT ctxt "1" (resolve_tac trans2),
398
+ − 867
DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+ − 868
DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+ − 869
DT ctxt "4" (ball_rsp_tac ctxt),
+ − 870
DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+ − 871
DT ctxt "6" (bex_rsp_tac ctxt),
420
+ − 872
DT ctxt "7" (resolve_tac rsp_thms),
+ − 873
DT ctxt "8" (rtac @{thm refl}),
398
+ − 874
DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 875
THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
398
+ − 876
DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 877
(RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
398
+ − 878
DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+ − 879
DT ctxt "C" (rtac @{thm ext}),
420
+ − 880
DT ctxt "D" (resolve_tac rel_refl),
398
+ − 881
DT ctxt "E" (atac),
+ − 882
DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
+ − 883
DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
410
+ − 884
DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
398
+ − 885
])
+ − 886
*}
+ − 887
+ − 888
387
+ − 889
+ − 890
399
+ − 891
section {* Cleaning of the theorem *}
387
+ − 892
389
+ − 893
ML {*
+ − 894
fun applic_prs lthy absrep (rty, qty) =
+ − 895
let
+ − 896
fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
+ − 897
fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
+ − 898
val (raty, rgty) = Term.strip_type rty;
+ − 899
val (qaty, qgty) = Term.strip_type qty;
+ − 900
val vs = map (fn _ => "x") qaty;
+ − 901
val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+ − 902
val f = Free (fname, qaty ---> qgty);
+ − 903
val args = map Free (vfs ~~ qaty);
+ − 904
val rhs = list_comb(f, args);
+ − 905
val largs = map2 mk_rep (raty ~~ qaty) args;
+ − 906
val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
+ − 907
val llhs = Syntax.check_term lthy lhs;
+ − 908
val eq = Logic.mk_equals (llhs, rhs);
+ − 909
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 910
val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
389
+ − 911
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
415
+ − 912
val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
389
+ − 913
in
+ − 914
singleton (ProofContext.export lthy' lthy) t_id
+ − 915
end
+ − 916
*}
387
+ − 917
+ − 918
ML {*
389
+ − 919
fun find_aps_all rtm qtm =
+ − 920
case (rtm, qtm) of
+ − 921
(Abs(_, T1, s1), Abs(_, T2, s2)) =>
+ − 922
find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
+ − 923
| (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
+ − 924
let
+ − 925
val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+ − 926
in
+ − 927
if T1 = T2 then sub else (T1, T2) :: sub
+ − 928
end
+ − 929
| ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+ − 930
| _ => [];
+ − 931
+ − 932
fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
+ − 933
*}
+ − 934
+ − 935
ML {*
387
+ − 936
fun allex_prs_tac lthy quot =
+ − 937
(EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
420
+ − 938
THEN' (quotient_tac quot)
387
+ − 939
*}
+ − 940
+ − 941
ML {*
+ − 942
fun prep_trm thy (x, (T, t)) =
+ − 943
(cterm_of thy (Var (x, T)), cterm_of thy t)
+ − 944
+ − 945
fun prep_ty thy (x, (S, ty)) =
+ − 946
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+ − 947
*}
+ − 948
+ − 949
ML {*
+ − 950
fun matching_prs thy pat trm =
+ − 951
let
+ − 952
val univ = Unify.matchers thy [(pat, trm)]
+ − 953
val SOME (env, _) = Seq.pull univ
+ − 954
val tenv = Vartab.dest (Envir.term_env env)
+ − 955
val tyenv = Vartab.dest (Envir.type_env env)
+ − 956
in
+ − 957
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ − 958
end
+ − 959
*}
+ − 960
+ − 961
ML {*
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 962
fun lambda_prs_conv1 ctxt quot_thms ctrm =
387
+ − 963
case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
+ − 964
let
+ − 965
val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
+ − 966
val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
+ − 967
val thy = ProofContext.theory_of ctxt;
+ − 968
val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+ − 969
val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
+ − 970
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+ − 971
val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
+ − 972
val tac =
+ − 973
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 974
(quotient_tac quot_thms);
387
+ − 975
val gc = Drule.strip_imp_concl (cprop_of lpi);
+ − 976
val t = Goal.prove_internal [] gc (fn _ => tac 1)
+ − 977
val te = @{thm eq_reflection} OF [t]
415
+ − 978
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
387
+ − 979
val tl = Thm.lhs_of ts
+ − 980
(* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
+ − 981
(* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
+ − 982
val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
+ − 983
val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
+ − 984
(* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+ − 985
in
+ − 986
Conv.rewr_conv ti ctrm
+ − 987
end
+ − 988
(* TODO: We can add a proper error message... *)
+ − 989
handle Bind => Conv.all_conv ctrm
+ − 990
+ − 991
*}
+ − 992
+ − 993
(* quot stands for the QUOTIENT theorems: *)
+ − 994
(* could be potentially all of them *)
+ − 995
ML {*
+ − 996
fun lambda_prs_conv ctxt quot ctrm =
+ − 997
case (term_of ctrm) of
+ − 998
(Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
+ − 999
(Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
+ − 1000
then_conv (lambda_prs_conv1 ctxt quot)) ctrm
+ − 1001
| _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
+ − 1002
| Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
+ − 1003
| _ => Conv.all_conv ctrm
+ − 1004
*}
+ − 1005
+ − 1006
ML {*
+ − 1007
fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
+ − 1008
CONVERSION
+ − 1009
(Conv.params_conv ~1 (fn ctxt =>
+ − 1010
(Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
+ − 1011
Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
+ − 1012
*}
+ − 1013
+ − 1014
ML {*
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1015
fun clean_tac lthy quot defs aps =
387
+ − 1016
let
+ − 1017
val lower = flat (map (add_lower_defs lthy) defs)
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1018
val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1019
val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
389
+ − 1020
val aps_thms = map (applic_prs lthy absrep) aps
387
+ − 1021
in
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1022
EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
387
+ − 1023
lambda_prs_tac lthy quot,
389
+ − 1024
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
387
+ − 1025
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1026
simp_tac (HOL_ss addsimps reps_same)]
387
+ − 1027
end
+ − 1028
*}
381
+ − 1029
404
+ − 1030
section {* Genralisation of free variables in a goal *}
347
+ − 1031
+ − 1032
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
+ − 1033
fun inst_spec ctrm =
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1034
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
+ − 1035
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1036
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
+ − 1037
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
+ − 1038
412
+ − 1039
fun all_list xs trm =
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1040
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
+ − 1041
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1042
fun apply_under_Trueprop f =
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1043
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
362
+ − 1044
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1045
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
+ − 1046
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
+ − 1047
let
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1048
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
+ − 1049
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
+ − 1050
val cvrs = map (cterm_of thy o Free) vrs
412
+ − 1051
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
+ − 1052
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
+ − 1053
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
+ − 1054
(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
+ − 1055
in
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1056
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
+ − 1057
end)
362
+ − 1058
*}
+ − 1059
402
+ − 1060
section {* General outline of the lifting procedure *}
+ − 1061
383
+ − 1062
(* - A is the original raw theorem *)
+ − 1063
(* - B is the regularized theorem *)
+ − 1064
(* - C is the rep/abs injected version of B *)
+ − 1065
(* - D is the lifted theorem *)
+ − 1066
(* *)
+ − 1067
(* - b is the regularization step *)
+ − 1068
(* - c is the rep/abs injection step *)
+ − 1069
(* - d is the cleaning part *)
+ − 1070
413
+ − 1071
lemma lifting_procedure:
360
+ − 1072
assumes a: "A"
+ − 1073
and b: "A \<Longrightarrow> B"
+ − 1074
and c: "B = C"
+ − 1075
and d: "C = D"
+ − 1076
shows "D"
+ − 1077
using a b c d
+ − 1078
by simp
+ − 1079
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1080
ML {*
412
+ − 1081
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
+ − 1082
let
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1083
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
+ − 1084
val qtrm_str = Syntax.string_of_term ctxt qtrm
388
+ − 1085
val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str,
+ − 1086
"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
+ − 1087
in
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1088
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
+ − 1089
end
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1090
*}
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1091
360
+ − 1092
ML {*
+ − 1093
fun procedure_inst ctxt rtrm qtrm =
+ − 1094
let
+ − 1095
val thy = ProofContext.theory_of ctxt
+ − 1096
val rtrm' = HOLogic.dest_Trueprop rtrm
+ − 1097
val qtrm' = HOLogic.dest_Trueprop qtrm
383
+ − 1098
val reg_goal =
405
+ − 1099
Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
412
+ − 1100
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
383
+ − 1101
val inj_goal =
408
+ − 1102
Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
412
+ − 1103
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
360
+ − 1104
in
+ − 1105
Drule.instantiate' []
+ − 1106
[SOME (cterm_of thy rtrm'),
+ − 1107
SOME (cterm_of thy reg_goal),
413
+ − 1108
SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
360
+ − 1109
end
362
+ − 1110
*}
389
+ − 1111
+ − 1112
(* Left for debugging *)
362
+ − 1113
ML {*
389
+ − 1114
fun procedure_tac lthy rthm =
+ − 1115
ObjectLogic.full_atomize_tac
+ − 1116
THEN' gen_frees_tac lthy
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1117
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
389
+ − 1118
let
+ − 1119
val rthm' = atomize_thm rthm
+ − 1120
val rule = procedure_inst context (prop_of rthm') (term_of concl)
+ − 1121
in
412
+ − 1122
EVERY1 [rtac rule, rtac rthm']
+ − 1123
end) lthy
360
+ − 1124
*}
+ − 1125
361
+ − 1126
ML {*
413
+ − 1127
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
419
+ − 1128
fun lift_tac lthy rthm rel_eqv rty quot rsp_thms defs =
389
+ − 1129
ObjectLogic.full_atomize_tac
+ − 1130
THEN' gen_frees_tac lthy
+ − 1131
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+ − 1132
let
+ − 1133
val rthm' = atomize_thm rthm
+ − 1134
val rule = procedure_inst context (prop_of rthm') (term_of concl)
+ − 1135
val aps = find_aps (prop_of rthm') (term_of concl)
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1136
val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
419
+ − 1137
val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
389
+ − 1138
in
413
+ − 1139
EVERY1
+ − 1140
[rtac rule,
+ − 1141
RANGE [rtac rthm',
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1142
regularize_tac lthy rel_eqv rel_refl,
413
+ − 1143
REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 1144
clean_tac lthy quot defs aps]]
412
+ − 1145
end) lthy
361
+ − 1146
*}
+ − 1147
198
+ − 1148
end
239
+ − 1149
347
+ − 1150