597
+ − 1
theory QuotMain
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2
imports QuotScript Prove
597
+ − 3
uses ("quotient_info.ML")
+ − 4
("quotient.ML")
+ − 5
("quotient_def.ML")
+ − 6
begin
+ − 7
+ − 8
+ − 9
locale QUOT_TYPE =
+ − 10
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ − 11
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ − 12
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ − 13
assumes equivp: "equivp R"
+ − 14
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ − 15
and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ − 16
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ − 17
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+ − 18
begin
+ − 19
+ − 20
definition
+ − 21
ABS::"'a \<Rightarrow> 'b"
+ − 22
where
+ − 23
"ABS x \<equiv> Abs (R x)"
+ − 24
+ − 25
definition
+ − 26
REP::"'b \<Rightarrow> 'a"
+ − 27
where
+ − 28
"REP a = Eps (Rep a)"
+ − 29
+ − 30
lemma lem9:
+ − 31
shows "R (Eps (R x)) = R x"
+ − 32
proof -
+ − 33
have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
+ − 34
then have "R x (Eps (R x))" by (rule someI)
+ − 35
then show "R (Eps (R x)) = R x"
+ − 36
using equivp unfolding equivp_def by simp
+ − 37
qed
+ − 38
+ − 39
theorem thm10:
+ − 40
shows "ABS (REP a) \<equiv> a"
+ − 41
apply (rule eq_reflection)
+ − 42
unfolding ABS_def REP_def
+ − 43
proof -
+ − 44
from rep_prop
+ − 45
obtain x where eq: "Rep a = R x" by auto
+ − 46
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ − 47
also have "\<dots> = Abs (R x)" using lem9 by simp
+ − 48
also have "\<dots> = Abs (Rep a)" using eq by simp
+ − 49
also have "\<dots> = a" using rep_inverse by simp
+ − 50
finally
+ − 51
show "Abs (R (Eps (Rep a))) = a" by simp
+ − 52
qed
+ − 53
+ − 54
lemma REP_refl:
+ − 55
shows "R (REP a) (REP a)"
+ − 56
unfolding REP_def
+ − 57
by (simp add: equivp[simplified equivp_def])
+ − 58
+ − 59
lemma lem7:
+ − 60
shows "(R x = R y) = (Abs (R x) = Abs (R y))"
+ − 61
apply(rule iffI)
+ − 62
apply(simp)
+ − 63
apply(drule rep_inject[THEN iffD2])
+ − 64
apply(simp add: abs_inverse)
+ − 65
done
+ − 66
+ − 67
theorem thm11:
+ − 68
shows "R r r' = (ABS r = ABS r')"
+ − 69
unfolding ABS_def
+ − 70
by (simp only: equivp[simplified equivp_def] lem7)
+ − 71
+ − 72
+ − 73
lemma REP_ABS_rsp:
+ − 74
shows "R f (REP (ABS g)) = R f g"
+ − 75
and "R (REP (ABS g)) f = R g f"
+ − 76
by (simp_all add: thm10 thm11)
+ − 77
+ − 78
lemma Quotient:
+ − 79
"Quotient R ABS REP"
+ − 80
apply(unfold Quotient_def)
+ − 81
apply(simp add: thm10)
+ − 82
apply(simp add: REP_refl)
+ − 83
apply(subst thm11[symmetric])
+ − 84
apply(simp add: equivp[simplified equivp_def])
+ − 85
done
+ − 86
+ − 87
end
+ − 88
+ − 89
section {* type definition for the quotient type *}
+ − 90
+ − 91
(* the auxiliary data for the quotient types *)
+ − 92
use "quotient_info.ML"
+ − 93
+ − 94
declare [[map "fun" = (fun_map, fun_rel)]]
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 96
lemmas [quot_thm] = fun_quotient
597
+ − 97
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 98
lemmas [quot_respect] = quot_rel_rsp
597
+ − 99
+ − 100
(* fun_map is not here since equivp is not true *)
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
lemmas [quot_equiv] = identity_equivp
597
+ − 102
+ − 103
(* definition of the quotient types *)
+ − 104
(* FIXME: should be called quotient_typ.ML *)
+ − 105
use "quotient.ML"
+ − 106
+ − 107
(* lifting of constants *)
+ − 108
use "quotient_def.ML"
+ − 109
+ − 110
section {* Simset setup *}
+ − 111
614
+ − 112
(* Since HOL_basic_ss is too "big" for us, *)
+ − 113
(* we set up our own minimal simpset. *)
597
+ − 114
ML {*
+ − 115
fun mk_minimal_ss ctxt =
+ − 116
Simplifier.context ctxt empty_ss
+ − 117
setsubgoaler asm_simp_tac
+ − 118
setmksimps (mksimps [])
+ − 119
*}
+ − 120
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 121
ML {*
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
fun OF1 thm1 thm2 = thm2 RS thm1
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 123
*}
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 124
614
+ − 125
section {* Atomize Infrastructure *}
597
+ − 126
+ − 127
lemma atomize_eqv[atomize]:
+ − 128
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+ − 129
proof
+ − 130
assume "A \<equiv> B"
+ − 131
then show "Trueprop A \<equiv> Trueprop B" by unfold
+ − 132
next
+ − 133
assume *: "Trueprop A \<equiv> Trueprop B"
+ − 134
have "A = B"
+ − 135
proof (cases A)
+ − 136
case True
+ − 137
have "A" by fact
+ − 138
then show "A = B" using * by simp
+ − 139
next
+ − 140
case False
+ − 141
have "\<not>A" by fact
+ − 142
then show "A = B" using * by auto
+ − 143
qed
+ − 144
then show "A \<equiv> B" by (rule eq_reflection)
+ − 145
qed
+ − 146
+ − 147
ML {*
+ − 148
fun atomize_thm thm =
+ − 149
let
+ − 150
val thm' = Thm.freezeT (forall_intr_vars thm)
+ − 151
val thm'' = ObjectLogic.atomize (cprop_of thm')
+ − 152
in
+ − 153
@{thm equal_elim_rule1} OF [thm'', thm']
+ − 154
end
+ − 155
*}
+ − 156
614
+ − 157
section {* Infrastructure about id *}
+ − 158
668
+ − 159
lemmas [id_simps] =
597
+ − 160
fun_map_id[THEN eq_reflection]
+ − 161
id_apply[THEN eq_reflection]
+ − 162
id_def[THEN eq_reflection,symmetric]
+ − 163
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 164
section {* Matching of Terms and Types *}
597
+ − 165
+ − 166
ML {*
665
+ − 167
fun struct_match_typ (ty, ty') =
597
+ − 168
case (ty, ty') of
+ − 169
(_, TVar _) => true
+ − 170
| (TFree x, TFree x') => x = x'
+ − 171
| (Type (s, tys), Type (s', tys')) =>
+ − 172
s = s' andalso
+ − 173
if (length tys = length tys')
665
+ − 174
then (List.all struct_match_typ (tys ~~ tys'))
597
+ − 175
else false
+ − 176
| _ => false
+ − 177
665
+ − 178
fun struct_match_term (trm, trm') =
597
+ − 179
case (trm, trm') of
+ − 180
(_, Var _) => true
665
+ − 181
| (Const (s, ty), Const (s', ty')) => s = s' andalso struct_match_typ (ty, ty')
+ − 182
| (Free (x, ty), Free (x', ty')) => x = x' andalso struct_match_typ (ty, ty')
597
+ − 183
| (Bound i, Bound j) => i = j
665
+ − 184
| (Abs (_, T, t), Abs (_, T', t')) => struct_match_typ (T, T') andalso struct_match_term (t, t')
+ − 185
| (t $ s, t' $ s') => struct_match_term (t, t') andalso struct_match_term (s, s')
597
+ − 186
| _ => false
+ − 187
*}
+ − 188
612
+ − 189
section {* Computation of the Regularize Goal *}
597
+ − 190
+ − 191
(*
+ − 192
Regularizing an rtrm means:
+ − 193
- quantifiers over a type that needs lifting are replaced by
+ − 194
bounded quantifiers, for example:
+ − 195
\<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
+ − 196
+ − 197
the relation R is given by the rty and qty;
+ − 198
+ − 199
- abstractions over a type that needs lifting are replaced
+ − 200
by bounded abstractions:
+ − 201
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+ − 202
+ − 203
- equalities over the type being lifted are replaced by
+ − 204
corresponding relations:
+ − 205
A = B \<Longrightarrow> A \<approx> B
+ − 206
+ − 207
example with more complicated types of A, B:
+ − 208
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
+ − 209
*)
+ − 210
+ − 211
ML {*
+ − 212
(* builds the relation that is the argument of respects *)
+ − 213
fun mk_resp_arg lthy (rty, qty) =
+ − 214
let
+ − 215
val thy = ProofContext.theory_of lthy
+ − 216
in
+ − 217
if rty = qty
+ − 218
then HOLogic.eq_const rty
+ − 219
else
+ − 220
case (rty, qty) of
+ − 221
(Type (s, tys), Type (s', tys')) =>
+ − 222
if s = s'
+ − 223
then let
+ − 224
val SOME map_info = maps_lookup thy s
+ − 225
val args = map (mk_resp_arg lthy) (tys ~~ tys')
+ − 226
in
+ − 227
list_comb (Const (#relfun map_info, dummyT), args)
+ − 228
end
+ − 229
else let
+ − 230
val SOME qinfo = quotdata_lookup_thy thy s'
+ − 231
(* FIXME: check in this case that the rty and qty *)
+ − 232
(* FIXME: correspond to each other *)
+ − 233
val (s, _) = dest_Const (#rel qinfo)
+ − 234
(* FIXME: the relation should only be the string *)
+ − 235
(* FIXME: and the type needs to be calculated as below; *)
+ − 236
(* FIXME: maybe one should actually have a term *)
+ − 237
(* FIXME: and one needs to force it to have this type *)
+ − 238
in
+ − 239
Const (s, rty --> rty --> @{typ bool})
+ − 240
end
+ − 241
| _ => HOLogic.eq_const dummyT
+ − 242
(* FIXME: check that the types correspond to each other? *)
+ − 243
end
+ − 244
*}
+ − 245
+ − 246
ML {*
+ − 247
val mk_babs = Const (@{const_name Babs}, dummyT)
+ − 248
val mk_ball = Const (@{const_name Ball}, dummyT)
+ − 249
val mk_bex = Const (@{const_name Bex}, dummyT)
+ − 250
val mk_resp = Const (@{const_name Respects}, dummyT)
+ − 251
*}
+ − 252
+ − 253
ML {*
+ − 254
(* - applies f to the subterm of an abstraction, *)
+ − 255
(* otherwise to the given term, *)
+ − 256
(* - used by regularize, therefore abstracted *)
+ − 257
(* variables do not have to be treated specially *)
+ − 258
+ − 259
fun apply_subt f trm1 trm2 =
+ − 260
case (trm1, trm2) of
+ − 261
(Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
+ − 262
| _ => f trm1 trm2
+ − 263
+ − 264
(* the major type of All and Ex quantifiers *)
+ − 265
fun qnt_typ ty = domain_type (domain_type ty)
+ − 266
*}
+ − 267
+ − 268
ML {*
632
+ − 269
(* produces a regularized version of rtrm *)
+ − 270
(* - the result is contains dummyT *)
597
+ − 271
(* - does not need any special treatment of *)
+ − 272
(* bound variables *)
+ − 273
+ − 274
fun regularize_trm lthy rtrm qtrm =
+ − 275
case (rtrm, qtrm) of
+ − 276
(Abs (x, ty, t), Abs (x', ty', t')) =>
+ − 277
let
+ − 278
val subtrm = Abs(x, ty, regularize_trm lthy t t')
+ − 279
in
632
+ − 280
if ty = ty' then subtrm
597
+ − 281
else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
+ − 282
end
+ − 283
+ − 284
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+ − 285
let
+ − 286
val subtrm = apply_subt (regularize_trm lthy) t t'
+ − 287
in
655
+ − 288
if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
597
+ − 289
else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ − 290
end
+ − 291
+ − 292
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+ − 293
let
+ − 294
val subtrm = apply_subt (regularize_trm lthy) t t'
+ − 295
in
655
+ − 296
if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
597
+ − 297
else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ − 298
end
+ − 299
+ − 300
| (* equalities need to be replaced by appropriate equivalence relations *)
+ − 301
(Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
632
+ − 302
if ty = ty' then rtrm
597
+ − 303
else mk_resp_arg lthy (domain_type ty, domain_type ty')
+ − 304
+ − 305
| (* in this case we check whether the given equivalence relation is correct *)
+ − 306
(rel, Const (@{const_name "op ="}, ty')) =>
+ − 307
let
+ − 308
val exc = LIFT_MATCH "regularise (relation mismatch)"
+ − 309
val rel_ty = (fastype_of rel) handle TERM _ => raise exc
+ − 310
val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty')
+ − 311
in
655
+ − 312
if rel' = rel then rtrm else raise exc
597
+ − 313
end
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 314
| (_, Const (s, Type(st, _))) =>
597
+ − 315
let
+ − 316
fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
+ − 317
| same_name _ _ = false
+ − 318
in
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 319
(* TODO/FIXME: This test is not enough *)
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 320
if same_name rtrm qtrm then rtrm
597
+ − 321
else
+ − 322
let
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 323
val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)")
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 324
val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)")
597
+ − 325
val thy = ProofContext.theory_of lthy
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 326
val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
597
+ − 327
in
665
+ − 328
if struct_match_term (rtrm, rtrm') then rtrm else
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 329
let
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 330
val _ = tracing (Syntax.string_of_term @{context} rtrm);
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 331
val _ = tracing (Syntax.string_of_term @{context} rtrm');
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 332
in raise exc2 end
597
+ − 333
end
+ − 334
end
+ − 335
+ − 336
| (t1 $ t2, t1' $ t2') =>
+ − 337
(regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
+ − 338
+ − 339
| (Free (x, ty), Free (x', ty')) =>
+ − 340
(* this case cannot arrise as we start with two fully atomized terms *)
+ − 341
raise (LIFT_MATCH "regularize (frees)")
+ − 342
+ − 343
| (Bound i, Bound i') =>
632
+ − 344
if i = i' then rtrm
597
+ − 345
else raise (LIFT_MATCH "regularize (bounds mismatch)")
+ − 346
+ − 347
| (rt, qt) =>
632
+ − 348
raise (LIFT_MATCH "regularize failed (default)")
597
+ − 349
*}
+ − 350
612
+ − 351
section {* Regularize Tactic *}
+ − 352
597
+ − 353
ML {*
+ − 354
fun equiv_tac ctxt =
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 355
REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
597
+ − 356
+ − 357
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
+ − 358
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+ − 359
*}
+ − 360
+ − 361
ML {*
+ − 362
fun prep_trm thy (x, (T, t)) =
+ − 363
(cterm_of thy (Var (x, T)), cterm_of thy t)
+ − 364
+ − 365
fun prep_ty thy (x, (S, ty)) =
+ − 366
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+ − 367
*}
+ − 368
+ − 369
ML {*
+ − 370
fun matching_prs thy pat trm =
+ − 371
let
+ − 372
val univ = Unify.matchers thy [(pat, trm)]
+ − 373
val SOME (env, _) = Seq.pull univ
+ − 374
val tenv = Vartab.dest (Envir.term_env env)
+ − 375
val tyenv = Vartab.dest (Envir.type_env env)
+ − 376
in
+ − 377
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ − 378
end
+ − 379
*}
+ − 380
+ − 381
ML {*
+ − 382
fun calculate_instance ctxt thm redex R1 R2 =
+ − 383
let
+ − 384
val thy = ProofContext.theory_of ctxt
+ − 385
val goal = Const (@{const_name "equivp"}, dummyT) $ R2
+ − 386
|> Syntax.check_term ctxt
+ − 387
|> HOLogic.mk_Trueprop
+ − 388
val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)
+ − 389
val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
+ − 390
val R1c = cterm_of thy R1
+ − 391
val thmi = Drule.instantiate' [] [SOME R1c] thm
+ − 392
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
+ − 393
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
+ − 394
in
+ − 395
SOME thm2
+ − 396
end
+ − 397
handle _ => NONE
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 398
(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
597
+ − 399
*}
+ − 400
+ − 401
ML {*
+ − 402
fun ball_bex_range_simproc ss redex =
+ − 403
let
+ − 404
val ctxt = Simplifier.the_context ss
+ − 405
in
+ − 406
case redex of
+ − 407
(Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
+ − 408
(Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ − 409
calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
+ − 410
| (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+ − 411
(Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ − 412
calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
+ − 413
| _ => NONE
+ − 414
end
+ − 415
*}
+ − 416
+ − 417
lemma eq_imp_rel:
+ − 418
shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+ − 419
by (simp add: equivp_reflp)
+ − 420
612
+ − 421
(* Regularize Tactic *)
597
+ − 422
612
+ − 423
(* 0. preliminary simplification step according to *)
+ − 424
thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
+ − 425
ball_reg_eqv_range bex_reg_eqv_range
+ − 426
(* 1. eliminating simple Ball/Bex instances*)
+ − 427
thm ball_reg_right bex_reg_left
+ − 428
(* 2. monos *)
+ − 429
(* 3. commutation rules for ball and bex *)
+ − 430
thm ball_all_comm bex_ex_comm
+ − 431
(* 4. then rel-equality (which need to be instantiated to avoid loops *)
+ − 432
thm eq_imp_rel
+ − 433
(* 5. then simplification like 0 *)
+ − 434
(* finally jump back to 1 *)
597
+ − 435
612
+ − 436
597
+ − 437
ML {*
+ − 438
fun regularize_tac ctxt =
+ − 439
let
+ − 440
val thy = ProofContext.theory_of ctxt
+ − 441
val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
+ − 442
val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"}
+ − 443
val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+ − 444
val simpset = (mk_minimal_ss ctxt)
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 445
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
597
+ − 446
addsimprocs [simproc] addSolver equiv_solver
+ − 447
(* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
(* can this cause loops in equiv_tac ? *)
612
+ − 449
val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
597
+ − 450
in
+ − 451
simp_tac simpset THEN'
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
REPEAT_ALL_NEW (CHANGED o FIRST' [
612
+ − 453
resolve_tac @{thms ball_reg_right bex_reg_left},
597
+ − 454
resolve_tac (Inductive.get_monos ctxt),
612
+ − 455
resolve_tac @{thms ball_all_comm bex_ex_comm},
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 456
resolve_tac eq_eqvs,
597
+ − 457
simp_tac simpset])
+ − 458
end
+ − 459
*}
+ − 460
612
+ − 461
section {* Calculation of the Injected Goal *}
597
+ − 462
+ − 463
(*
+ − 464
Injecting repabs means:
+ − 465
+ − 466
For abstractions:
+ − 467
* If the type of the abstraction doesn't need lifting we recurse.
+ − 468
* If it does we add RepAbs around the whole term and check if the
+ − 469
variable needs lifting.
+ − 470
* If it doesn't then we recurse
+ − 471
* If it does we recurse and put 'RepAbs' around all occurences
+ − 472
of the variable in the obtained subterm. This in combination
+ − 473
with the RepAbs above will let us change the type of the
+ − 474
abstraction with rewriting.
+ − 475
For applications:
+ − 476
* If the term is 'Respects' applied to anything we leave it unchanged
+ − 477
* If the term needs lifting and the head is a constant that we know
+ − 478
how to lift, we put a RepAbs and recurse
+ − 479
* If the term needs lifting and the head is a free applied to subterms
+ − 480
(if it is not applied we treated it in Abs branch) then we
+ − 481
put RepAbs and recurse
+ − 482
* Otherwise just recurse.
+ − 483
*)
+ − 484
+ − 485
ML {*
+ − 486
fun mk_repabs lthy (T, T') trm =
+ − 487
Quotient_Def.get_fun repF lthy (T, T')
+ − 488
$ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+ − 489
*}
+ − 490
+ − 491
ML {*
+ − 492
(* bound variables need to be treated properly, *)
+ − 493
(* as the type of subterms need to be calculated *)
+ − 494
(* in the abstraction case *)
+ − 495
+ − 496
fun inj_repabs_trm lthy (rtrm, qtrm) =
+ − 497
case (rtrm, qtrm) of
+ − 498
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+ − 499
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+ − 500
+ − 501
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+ − 502
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+ − 503
+ − 504
| (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
621
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 505
let
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 506
val rty = fastype_of rtrm
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 507
val qty = fastype_of qtrm
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 508
in
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 509
mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 510
end
597
+ − 511
+ − 512
| (Abs (x, T, t), Abs (x', T', t')) =>
+ − 513
let
+ − 514
val rty = fastype_of rtrm
+ − 515
val qty = fastype_of qtrm
+ − 516
val (y, s) = Term.dest_abs (x, T, t)
+ − 517
val (_, s') = Term.dest_abs (x', T', t')
+ − 518
val yvar = Free (y, T)
+ − 519
val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
+ − 520
in
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 521
if rty = qty then result
597
+ − 522
else mk_repabs lthy (rty, qty) result
+ − 523
end
+ − 524
+ − 525
| (t $ s, t' $ s') =>
+ − 526
(inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+ − 527
+ − 528
| (Free (_, T), Free (_, T')) =>
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 529
if T = T' then rtrm
597
+ − 530
else mk_repabs lthy (T, T') rtrm
+ − 531
+ − 532
| (_, Const (@{const_name "op ="}, _)) => rtrm
+ − 533
+ − 534
(* FIXME: check here that rtrm is the corresponding definition for the const *)
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 535
(* Hasn't it already been checked in regularize? *)
597
+ − 536
| (_, Const (_, T')) =>
+ − 537
let
+ − 538
val rty = fastype_of rtrm
+ − 539
in
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 540
if rty = T' then rtrm
597
+ − 541
else mk_repabs lthy (rty, T') rtrm
+ − 542
end
+ − 543
+ − 544
| _ => raise (LIFT_MATCH "injection")
+ − 545
*}
+ − 546
612
+ − 547
section {* Injection Tactic *}
597
+ − 548
+ − 549
ML {*
+ − 550
fun quotient_tac ctxt =
+ − 551
REPEAT_ALL_NEW (FIRST'
+ − 552
[rtac @{thm identity_quotient},
+ − 553
resolve_tac (quotient_rules_get ctxt)])
+ − 554
+ − 555
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+ − 556
val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+ − 557
*}
+ − 558
+ − 559
ML {*
+ − 560
fun solve_quotient_assums ctxt thm =
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 561
let
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 562
val goal = hd (Drule.strip_imp_prems (cprop_of thm))
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 563
in
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 564
thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 565
end
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 566
handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
597
+ − 567
*}
+ − 568
+ − 569
definition
+ − 570
"QUOT_TRUE x \<equiv> True"
+ − 571
+ − 572
ML {*
+ − 573
fun find_qt_asm asms =
+ − 574
let
+ − 575
fun find_fun trm =
+ − 576
case trm of
+ − 577
(Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+ − 578
| _ => false
+ − 579
in
+ − 580
case find_first find_fun asms of
+ − 581
SOME (_ $ (_ $ (f $ a))) => (f, a)
+ − 582
| SOME _ => error "find_qt_asm: no pair"
+ − 583
| NONE => error "find_qt_asm: no assumption"
+ − 584
end
+ − 585
*}
+ − 586
+ − 587
(*
+ − 588
To prove that the regularised theorem implies the abs/rep injected,
+ − 589
we try:
+ − 590
+ − 591
1) theorems 'trans2' from the appropriate QUOT_TYPE
+ − 592
2) remove lambdas from both sides: lambda_rsp_tac
+ − 593
3) remove Ball/Bex from the right hand side
+ − 594
4) use user-supplied RSP theorems
+ − 595
5) remove rep_abs from the right side
+ − 596
6) reflexivity of equality
+ − 597
7) split applications of lifted type (apply_rsp)
+ − 598
8) split applications of non-lifted type (cong_tac)
+ − 599
9) apply extentionality
+ − 600
A) reflexivity of the relation
+ − 601
B) assumption
+ − 602
(Lambdas under respects may have left us some assumptions)
+ − 603
C) proving obvious higher order equalities by simplifying fun_rel
+ − 604
(not sure if it is still needed?)
+ − 605
D) unfolding lambda on one side
+ − 606
E) simplifying (= ===> =) for simpler respectfulness
+ − 607
+ − 608
*)
+ − 609
+ − 610
lemma quot_true_dests:
+ − 611
shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
+ − 612
and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
+ − 613
and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
+ − 614
and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
655
+ − 615
by (simp_all add: QUOT_TRUE_def ext)
597
+ − 616
+ − 617
lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
+ − 618
by (simp add: QUOT_TRUE_def)
+ − 619
+ − 620
ML {*
+ − 621
fun quot_true_conv1 ctxt fnctn ctrm =
+ − 622
case (term_of ctrm) of
+ − 623
(Const (@{const_name QUOT_TRUE}, _) $ x) =>
+ − 624
let
+ − 625
val fx = fnctn x;
+ − 626
val thy = ProofContext.theory_of ctxt;
+ − 627
val cx = cterm_of thy x;
+ − 628
val cfx = cterm_of thy fx;
+ − 629
val cxt = ctyp_of thy (fastype_of x);
+ − 630
val cfxt = ctyp_of thy (fastype_of fx);
+ − 631
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
+ − 632
in
+ − 633
Conv.rewr_conv thm ctrm
+ − 634
end
+ − 635
*}
+ − 636
+ − 637
ML {*
+ − 638
fun quot_true_conv ctxt fnctn ctrm =
+ − 639
case (term_of ctrm) of
+ − 640
(Const (@{const_name QUOT_TRUE}, _) $ _) =>
+ − 641
quot_true_conv1 ctxt fnctn ctrm
+ − 642
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+ − 643
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+ − 644
| _ => Conv.all_conv ctrm
+ − 645
*}
+ − 646
+ − 647
ML {*
+ − 648
fun quot_true_tac ctxt fnctn = CONVERSION
+ − 649
((Conv.params_conv ~1 (fn ctxt =>
+ − 650
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
+ − 651
*}
+ − 652
+ − 653
ML {* fun dest_comb (f $ a) = (f, a) *}
+ − 654
ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
+ − 655
(* TODO: Can this be done easier? *)
+ − 656
ML {*
+ − 657
fun unlam t =
+ − 658
case t of
+ − 659
(Abs a) => snd (Term.dest_abs a)
+ − 660
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
+ − 661
*}
+ − 662
+ − 663
ML {*
+ − 664
fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+ − 665
| dest_fun_type _ = error "dest_fun_type"
+ − 666
*}
+ − 667
+ − 668
ML {*
+ − 669
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
+ − 670
*}
+ − 671
+ − 672
ML {*
+ − 673
val apply_rsp_tac =
+ − 674
Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ − 675
case ((HOLogic.dest_Trueprop (term_of concl))) of
+ − 676
((R2 $ (f $ x) $ (g $ y))) =>
+ − 677
(let
+ − 678
val (asmf, asma) = find_qt_asm (map term_of asms);
+ − 679
in
+ − 680
if (fastype_of asmf) = (fastype_of f) then no_tac else let
+ − 681
val ty_a = fastype_of x;
+ − 682
val ty_b = fastype_of asma;
+ − 683
val ty_c = range_type (type_of f);
+ − 684
val thy = ProofContext.theory_of context;
+ − 685
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
+ − 686
val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
+ − 687
val te = solve_quotient_assums context thm
+ − 688
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+ − 689
val thm = Drule.instantiate' [] t_inst te
+ − 690
in
+ − 691
compose_tac (false, thm, 2) 1
+ − 692
end
+ − 693
end
+ − 694
handle ERROR "find_qt_asm: no pair" => no_tac)
+ − 695
| _ => no_tac)
+ − 696
*}
+ − 697
+ − 698
ML {*
629
+ − 699
fun equals_rsp_tac R ctxt =
+ − 700
let
690
+ − 701
val ty = domain_type (fastype_of R);
629
+ − 702
val thy = ProofContext.theory_of ctxt
690
+ − 703
val thm = Drule.instantiate'
+ − 704
[SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
629
+ − 705
in
690
+ − 706
rtac thm THEN' quotient_tac ctxt
629
+ − 707
end
690
+ − 708
handle THM _ => K no_tac
+ − 709
| TYPE _ => K no_tac
+ − 710
| TERM _ => K no_tac
629
+ − 711
*}
+ − 712
+ − 713
ML {*
597
+ − 714
fun rep_abs_rsp_tac ctxt =
+ − 715
SUBGOAL (fn (goal, i) =>
+ − 716
case (bare_concl goal) of
+ − 717
(rel $ _ $ (rep $ (abs $ _))) =>
+ − 718
(let
+ − 719
val thy = ProofContext.theory_of ctxt;
+ − 720
val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+ − 721
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+ − 722
val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
+ − 723
val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+ − 724
val te = solve_quotient_assums ctxt thm
+ − 725
in
+ − 726
rtac te i
+ − 727
end
+ − 728
handle _ => no_tac)
+ − 729
| _ => no_tac)
+ − 730
*}
+ − 731
+ − 732
ML {*
629
+ − 733
fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
597
+ − 734
(case (bare_concl goal) of
+ − 735
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+ − 736
((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+ − 737
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 738
+ − 739
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ − 740
| (Const (@{const_name "op ="},_) $
+ − 741
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 742
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ − 743
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+ − 744
+ − 745
(* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
+ − 746
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ − 747
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 748
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 749
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 750
+ − 751
(* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ − 752
| Const (@{const_name "op ="},_) $
+ − 753
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 754
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 755
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+ − 756
+ − 757
(* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
+ − 758
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ − 759
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 760
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 761
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 762
+ − 763
| (_ $
+ − 764
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 765
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ − 766
=> rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+ − 767
629
+ − 768
| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE'
+ − 769
(equals_rsp_tac R ctxt THEN' RANGE [
+ − 770
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+ − 771
597
+ − 772
(* reflexivity of operators arising from Cong_tac *)
629
+ − 773
| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
597
+ − 774
+ − 775
(* respectfulness of constants; in particular of a simple relation *)
+ − 776
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ − 777
=> resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+ − 778
+ − 779
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+ − 780
(* observe ---> *)
624
c4299ce27e46
Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 781
| _ $ _ $ _
c4299ce27e46
Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 782
=> (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt
597
+ − 783
+ − 784
| _ => error "inj_repabs_tac not a relation"
+ − 785
) i)
+ − 786
*}
+ − 787
+ − 788
ML {*
629
+ − 789
fun inj_repabs_step_tac ctxt rel_refl =
597
+ − 790
(FIRST' [
686
+ − 791
inj_repabs_tac_match ctxt,
597
+ − 792
(* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *)
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 793
686
+ − 794
apply_rsp_tac ctxt THEN'
+ − 795
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 796
597
+ − 797
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
+ − 798
(* merge with previous tactic *)
686
+ − 799
Cong_Tac.cong_tac @{thm cong} THEN'
+ − 800
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 801
597
+ − 802
(* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
686
+ − 803
rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 804
597
+ − 805
(* resolving with R x y assumptions *)
686
+ − 806
atac,
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 807
597
+ − 808
(* reflexivity of the basic relations *)
+ − 809
(* R \<dots> \<dots> *)
686
+ − 810
resolve_tac rel_refl])
597
+ − 811
*}
+ − 812
+ − 813
ML {*
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 814
fun inj_repabs_tac ctxt =
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 815
let
612
+ − 816
val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 817
in
629
+ − 818
inj_repabs_step_tac ctxt rel_refl
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 819
end
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 820
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 821
fun all_inj_repabs_tac ctxt =
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 822
REPEAT_ALL_NEW (inj_repabs_tac ctxt)
597
+ − 823
*}
+ − 824
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 825
section {* Cleaning of the Theorem *}
597
+ − 826
659
+ − 827
ML {*
+ − 828
fun fun_map_simple_conv xs ctxt ctrm =
+ − 829
case (term_of ctrm) of
+ − 830
((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
+ − 831
if (member (op=) xs h)
+ − 832
then Conv.all_conv ctrm
+ − 833
else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm
+ − 834
| _ => Conv.all_conv ctrm
+ − 835
+ − 836
fun fun_map_conv xs ctxt ctrm =
+ − 837
case (term_of ctrm) of
+ − 838
_ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
+ − 839
fun_map_simple_conv xs ctxt) ctrm
+ − 840
| Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+ − 841
| _ => Conv.all_conv ctrm
+ − 842
+ − 843
fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+ − 844
*}
+ − 845
631
+ − 846
(* Since the patterns for the lhs are different; there are 3 different make-insts *)
+ − 847
(* 1: does ? \<rightarrow> id *)
+ − 848
(* 2: does id \<rightarrow> ? *)
+ − 849
(* 3: does ? \<rightarrow> ? *)
597
+ − 850
ML {*
+ − 851
fun make_inst lhs t =
+ − 852
let
+ − 853
val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ − 854
val _ $ (Abs (_, _, g)) = t;
+ − 855
fun mk_abs i t =
+ − 856
if incr_boundvars i u aconv t then Bound i
+ − 857
else (case t of
+ − 858
t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+ − 859
| Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
+ − 860
| Bound j => if i = j then error "make_inst" else t
+ − 861
| _ => t);
+ − 862
in (f, Abs ("x", T, mk_abs 0 g)) end;
+ − 863
*}
+ − 864
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 865
ML {*
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 866
fun make_inst2 lhs t =
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 867
let
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 868
val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
631
+ − 869
val _ $ (Abs (_, _, (_ $ g))) = t;
+ − 870
fun mk_abs i t =
+ − 871
if incr_boundvars i u aconv t then Bound i
+ − 872
else (case t of
+ − 873
t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+ − 874
| Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
+ − 875
| Bound j => if i = j then error "make_inst" else t
+ − 876
| _ => t);
+ − 877
in (f, Abs ("x", T, mk_abs 0 g)) end;
+ − 878
*}
+ − 879
+ − 880
ML {*
597
+ − 881
fun lambda_prs_simple_conv ctxt ctrm =
+ − 882
case (term_of ctrm) of
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 883
((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
608
+ − 884
(let
597
+ − 885
val thy = ProofContext.theory_of ctxt
+ − 886
val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+ − 887
val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ − 888
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+ − 889
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+ − 890
val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
+ − 891
val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 892
val ti =
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 893
(let
614
+ − 894
val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 895
val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 896
in
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 897
Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
608
+ − 898
end handle _ => (* TODO handle only Bind | Error "make_inst" *)
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 899
let
631
+ − 900
val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+ − 901
val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+ − 902
val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+ − 903
val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm)
+ − 904
in
+ − 905
Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+ − 906
end handle _ => (* TODO handle only Bind | Error "make_inst" *)
+ − 907
let
662
+ − 908
val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 909
val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 910
in
614
+ − 911
MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 912
end);
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 913
val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
597
+ − 914
(tracing "lambda_prs";
+ − 915
tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+ − 916
tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
+ − 917
tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
602
e56eeb9fedb3
make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 918
tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
597
+ − 919
else ()
631
+ − 920
597
+ − 921
in
+ − 922
Conv.rewr_conv ti ctrm
+ − 923
end
608
+ − 924
handle _ => Conv.all_conv ctrm)
597
+ − 925
| _ => Conv.all_conv ctrm
+ − 926
*}
+ − 927
+ − 928
ML {*
+ − 929
val lambda_prs_conv =
+ − 930
More_Conv.top_conv lambda_prs_simple_conv
+ − 931
+ − 932
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
+ − 933
*}
+ − 934
659
+ − 935
(* 1. folding of definitions and preservation lemmas; *)
+ − 936
(* and simplification with *)
+ − 937
thm babs_prs all_prs ex_prs
+ − 938
(* 2. unfolding of ---> in front of everything, except *)
+ − 939
(* bound variables *)
660
+ − 940
thm fun_map.simps
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 941
(* 3. simplification with *)
661
+ − 942
thm lambda_prs
660
+ − 943
(* 4. simplification with *)
659
+ − 944
thm Quotient_abs_rep Quotient_rel_rep id_simps
660
+ − 945
(* 5. Test for refl *)
597
+ − 946
652
d8f07b5bcfae
implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 947
ML {*
597
+ − 948
fun clean_tac lthy =
+ − 949
let
+ − 950
val thy = ProofContext.theory_of lthy;
+ − 951
val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 952
(* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
658
+ − 953
656
c86a47d4966e
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 954
val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
658
+ − 955
val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
597
+ − 956
fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+ − 957
in
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 958
EVERY' [simp_tac (simps thms1),
658
+ − 959
fun_map_tac lthy,
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 960
lambda_prs_tac lthy,
597
+ − 961
simp_tac (simps thms2),
+ − 962
TRY o rtac refl]
+ − 963
end
+ − 964
*}
+ − 965
689
+ − 966
section {* Tactic for Genralisation of Free Variables in a Goal *}
597
+ − 967
+ − 968
ML {*
+ − 969
fun inst_spec ctrm =
+ − 970
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+ − 971
+ − 972
fun inst_spec_tac ctrms =
+ − 973
EVERY' (map (dtac o inst_spec) ctrms)
+ − 974
+ − 975
fun all_list xs trm =
+ − 976
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
+ − 977
+ − 978
fun apply_under_Trueprop f =
+ − 979
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
+ − 980
+ − 981
fun gen_frees_tac ctxt =
+ − 982
SUBGOAL (fn (concl, i) =>
+ − 983
let
+ − 984
val thy = ProofContext.theory_of ctxt
+ − 985
val vrs = Term.add_frees concl []
+ − 986
val cvrs = map (cterm_of thy o Free) vrs
+ − 987
val concl' = apply_under_Trueprop (all_list vrs) concl
+ − 988
val goal = Logic.mk_implies (concl', concl)
+ − 989
val rule = Goal.prove ctxt [] [] goal
+ − 990
(K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+ − 991
in
+ − 992
rtac rule i
+ − 993
end)
+ − 994
*}
+ − 995
616
+ − 996
section {* General Shape of the Lifting Procedure *}
597
+ − 997
689
+ − 998
(* - A is the original raw theorem *)
+ − 999
(* - B is the regularized theorem *)
+ − 1000
(* - C is the rep/abs injected version of B *)
+ − 1001
(* - D is the lifted theorem *)
+ − 1002
(* *)
+ − 1003
(* - b is the regularization step *)
+ − 1004
(* - c is the rep/abs injection step *)
+ − 1005
(* - d is the cleaning part *)
+ − 1006
(* *)
+ − 1007
(* the QUOT_TRUE premise records the lifted theorem *)
597
+ − 1008
+ − 1009
lemma lifting_procedure:
+ − 1010
assumes a: "A"
606
+ − 1011
and b: "A \<longrightarrow> B"
688
+ − 1012
and c: "QUOT_TRUE D \<Longrightarrow> B = C"
597
+ − 1013
and d: "C = D"
+ − 1014
shows "D"
612
+ − 1015
using a b c d
688
+ − 1016
by (simp add: QUOT_TRUE_def)
597
+ − 1017
+ − 1018
ML {*
+ − 1019
fun lift_match_error ctxt fun_str rtrm qtrm =
+ − 1020
let
+ − 1021
val rtrm_str = Syntax.string_of_term ctxt rtrm
+ − 1022
val qtrm_str = Syntax.string_of_term ctxt qtrm
+ − 1023
val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str,
+ − 1024
"and the lifted theorem\n", rtrm_str, "do not match"]
+ − 1025
in
+ − 1026
error (space_implode " " msg)
+ − 1027
end
+ − 1028
*}
+ − 1029
+ − 1030
ML {*
+ − 1031
fun procedure_inst ctxt rtrm qtrm =
+ − 1032
let
+ − 1033
val thy = ProofContext.theory_of ctxt
+ − 1034
val rtrm' = HOLogic.dest_Trueprop rtrm
+ − 1035
val qtrm' = HOLogic.dest_Trueprop qtrm
+ − 1036
val reg_goal =
+ − 1037
Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
+ − 1038
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+ − 1039
val inj_goal =
+ − 1040
Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
+ − 1041
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+ − 1042
in
+ − 1043
Drule.instantiate' []
+ − 1044
[SOME (cterm_of thy rtrm'),
+ − 1045
SOME (cterm_of thy reg_goal),
688
+ − 1046
NONE,
597
+ − 1047
SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
+ − 1048
end
+ − 1049
*}
+ − 1050
+ − 1051
ML {*
616
+ − 1052
(* the tactic leaves three subgoals to be proved *)
597
+ − 1053
fun procedure_tac ctxt rthm =
+ − 1054
ObjectLogic.full_atomize_tac
+ − 1055
THEN' gen_frees_tac ctxt
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1056
THEN' CSUBGOAL (fn (goal, i) =>
597
+ − 1057
let
+ − 1058
val rthm' = atomize_thm rthm
610
2bee5ca44ef5
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1059
val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
597
+ − 1060
in
688
+ − 1061
(rtac rule THEN' rtac rthm') i
597
+ − 1062
end)
+ − 1063
*}
+ − 1064
689
+ − 1065
section {* Automatic Proofs *}
+ − 1066
612
+ − 1067
ML {*
616
+ − 1068
fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1069
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1070
fun WARN (tac, msg) i st =
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1071
case Seq.pull ((SOLVES' tac) i st) of
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1072
NONE => (warning msg; Seq.single st)
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1073
| seqcell => Seq.make (fn () => seqcell)
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1074
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1075
fun RANGE_WARN xs = RANGE (map WARN xs)
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1076
*}
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1077
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1078
ML {*
612
+ − 1079
fun lift_tac ctxt rthm =
+ − 1080
procedure_tac ctxt rthm
688
+ − 1081
THEN' RANGE_WARN
+ − 1082
[(regularize_tac ctxt, "Regularize proof failed."),
+ − 1083
(all_inj_repabs_tac ctxt, "Injection proof failed."),
+ − 1084
(clean_tac ctxt, "Cleaning proof failed.")]
612
+ − 1085
*}
+ − 1086
689
+ − 1087
section {* Methods / Interface *}
+ − 1088
632
+ − 1089
ML {*
+ − 1090
fun mk_method1 tac thm ctxt =
+ − 1091
SIMPLE_METHOD (HEADGOAL (tac ctxt thm))
+ − 1092
+ − 1093
fun mk_method2 tac ctxt =
+ − 1094
SIMPLE_METHOD (HEADGOAL (tac ctxt))
+ − 1095
*}
+ − 1096
+ − 1097
method_setup lifting =
637
+ − 1098
{* Attrib.thm >> (mk_method1 lift_tac) *}
632
+ − 1099
{* Lifting of theorems to quotient types. *}
+ − 1100
+ − 1101
method_setup lifting_setup =
637
+ − 1102
{* Attrib.thm >> (mk_method1 procedure_tac) *}
632
+ − 1103
{* Sets up the three goals for the lifting procedure. *}
+ − 1104
+ − 1105
method_setup regularize =
+ − 1106
{* Scan.succeed (mk_method2 regularize_tac) *}
+ − 1107
{* Proves automatically the regularization goals from the lifting procedure. *}
+ − 1108
+ − 1109
method_setup injection =
+ − 1110
{* Scan.succeed (mk_method2 all_inj_repabs_tac) *}
+ − 1111
{* Proves automatically the rep/abs injection goals from the lifting procedure. *}
+ − 1112
+ − 1113
method_setup cleaning =
+ − 1114
{* Scan.succeed (mk_method2 clean_tac) *}
+ − 1115
{* Proves automatically the cleaning goals from the lifting procedure. *}
+ − 1116
597
+ − 1117
end
+ − 1118