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