1438
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1
(* Title: HOL/Tools/Quotient/quotient_tacs.thy
952
+ − 2
Author: Cezary Kaliszyk and Christian Urban
+ − 3
1438
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 4
Tactics for solving goal arising from lifting theorems to quotient
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 5
types.
952
+ − 6
*)
+ − 7
758
+ − 8
signature QUOTIENT_TACS =
+ − 9
sig
853
+ − 10
val regularize_tac: Proof.context -> int -> tactic
+ − 11
val injection_tac: Proof.context -> int -> tactic
+ − 12
val all_injection_tac: Proof.context -> int -> tactic
+ − 13
val clean_tac: Proof.context -> int -> tactic
+ − 14
val procedure_tac: Proof.context -> thm -> int -> tactic
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 15
val lift_tac: Proof.context -> thm list -> int -> tactic
853
+ − 16
val quotient_tac: Proof.context -> int -> tactic
+ − 17
val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
1077
+ − 18
val lifted_attrib: attribute
758
+ − 19
end;
+ − 20
+ − 21
structure Quotient_Tacs: QUOTIENT_TACS =
+ − 22
struct
+ − 23
762
+ − 24
open Quotient_Info;
+ − 25
open Quotient_Term;
+ − 26
848
+ − 27
+ − 28
(** various helper fuctions **)
802
+ − 29
769
d89851ebac9b
cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30
(* Since HOL_basic_ss is too "big" for us, we *)
d89851ebac9b
cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
(* need to set up our own minimal simpset. *)
1113
+ − 32
fun mk_minimal_ss ctxt =
758
+ − 33
Simplifier.context ctxt empty_ss
+ − 34
setsubgoaler asm_simp_tac
+ − 35
setmksimps (mksimps [])
+ − 36
785
+ − 37
(* composition of two theorems, used in maps *)
758
+ − 38
fun OF1 thm1 thm2 = thm2 RS thm1
+ − 39
802
+ − 40
(* prints a warning, if the subgoal is not solved *)
758
+ − 41
fun WARN (tac, msg) i st =
1112
+ − 42
case Seq.pull (SOLVED' tac i st) of
758
+ − 43
NONE => (warning msg; Seq.single st)
+ − 44
| seqcell => Seq.make (fn () => seqcell)
+ − 45
802
+ − 46
fun RANGE_WARN tacs = RANGE (map WARN tacs)
758
+ − 47
+ − 48
fun atomize_thm thm =
+ − 49
let
804
+ − 50
val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
1354
+ − 51
val thm'' = Object_Logic.atomize (cprop_of thm')
758
+ − 52
in
+ − 53
@{thm equal_elim_rule1} OF [thm'', thm']
+ − 54
end
+ − 55
+ − 56
848
+ − 57
+ − 58
(*** Regularize Tactic ***)
758
+ − 59
848
+ − 60
(** solvers for equivp and quotient assumptions **)
+ − 61
+ − 62
fun equiv_tac ctxt =
758
+ − 63
REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
+ − 64
+ − 65
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
+ − 66
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+ − 67
870
2a19e0a37131
Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 68
fun quotient_tac ctxt =
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
(REPEAT_ALL_NEW (FIRST'
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70
[rtac @{thm identity_quotient},
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 71
resolve_tac (quotient_rules_get ctxt)]))
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 72
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 73
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
853
+ − 74
val quotient_solver =
+ − 75
Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
fun solve_quotient_assm ctxt thm =
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
case Seq.pull (quotient_tac ctxt 1 thm) of
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
SOME (t, _) => t
802
+ − 80
| _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 81
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 82
758
+ − 83
fun prep_trm thy (x, (T, t)) =
+ − 84
(cterm_of thy (Var (x, T)), cterm_of thy t)
+ − 85
+ − 86
fun prep_ty thy (x, (S, ty)) =
+ − 87
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+ − 88
772
a95f6bb081cf
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 89
fun get_match_inst thy pat trm =
758
+ − 90
let
+ − 91
val univ = Unify.matchers thy [(pat, trm)]
1438
61671de8a545
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 92
val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *)
758
+ − 93
val tenv = Vartab.dest (Envir.term_env env)
+ − 94
val tyenv = Vartab.dest (Envir.type_env env)
+ − 95
in
+ − 96
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ − 97
end
+ − 98
837
+ − 99
(* Calculates the instantiations for the lemmas:
858
+ − 100
837
+ − 101
ball_reg_eqv_range and bex_reg_eqv_range
858
+ − 102
837
+ − 103
Since the left-hand-side contains a non-pattern '?P (f ?x)'
+ − 104
we rely on unification/instantiation to check whether the
1128
+ − 105
theorem applies and return NONE if it doesn't.
858
+ − 106
*)
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 107
fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
758
+ − 108
let
951
+ − 109
val thy = ProofContext.theory_of ctxt
771
b2231990b059
simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 110
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
951
+ − 111
val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
+ − 112
val trm_inst = map (SOME o cterm_of thy) [R2, R1]
758
+ − 113
in
951
+ − 114
case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
837
+ − 115
NONE => NONE
+ − 116
| SOME thm' =>
+ − 117
(case try (get_match_inst thy (get_lhs thm')) redex of
+ − 118
NONE => NONE
+ − 119
| SOME inst2 => try (Drule.instantiate inst2) thm')
758
+ − 120
end
+ − 121
+ − 122
fun ball_bex_range_simproc ss redex =
+ − 123
let
+ − 124
val ctxt = Simplifier.the_context ss
1128
+ − 125
in
772
a95f6bb081cf
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 126
case redex of
1128
+ − 127
(Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
758
+ − 128
(Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
758
+ − 130
1128
+ − 131
| (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+ − 132
(Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 133
calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 134
758
+ − 135
| _ => NONE
+ − 136
end
+ − 137
858
+ − 138
(* Regularize works as follows:
853
+ − 139
858
+ − 140
0. preliminary simplification step according to
+ − 141
ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
853
+ − 142
1074
+ − 143
1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
858
+ − 144
+ − 145
2. monos
758
+ − 146
858
+ − 147
3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
+ − 148
+ − 149
4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
+ − 150
to avoid loops
853
+ − 151
858
+ − 152
5. then simplification like 0
853
+ − 153
1128
+ − 154
finally jump back to 1
858
+ − 155
*)
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156
758
+ − 157
fun regularize_tac ctxt =
+ − 158
let
+ − 159
val thy = ProofContext.theory_of ctxt
772
a95f6bb081cf
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 160
val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
a95f6bb081cf
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
a95f6bb081cf
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
1128
+ − 163
val simpset = (mk_minimal_ss ctxt)
845
+ − 164
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
1128
+ − 165
addsimprocs [simproc]
772
a95f6bb081cf
on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 166
addSolver equiv_solver addSolver quotient_solver
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 167
val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 168
val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
758
+ − 169
in
+ − 170
simp_tac simpset THEN'
1128
+ − 171
REPEAT_ALL_NEW (CHANGED o FIRST'
946
+ − 172
[resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 173
resolve_tac (Inductive.get_monos ctxt),
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 174
resolve_tac @{thms ball_all_comm bex_ex_comm},
1128
+ − 175
resolve_tac eq_eqvs,
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 176
simp_tac simpset])
758
+ − 177
end
+ − 178
+ − 179
848
+ − 180
+ − 181
(*** Injection Tactic ***)
758
+ − 182
1112
+ − 183
(* Looks for Quot_True assumptions, and in case its parameter
1128
+ − 184
is an application, it returns the function and the argument.
858
+ − 185
*)
758
+ − 186
fun find_qt_asm asms =
+ − 187
let
+ − 188
fun find_fun trm =
+ − 189
case trm of
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 190
(Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
758
+ − 191
| _ => false
+ − 192
in
+ − 193
case find_first find_fun asms of
+ − 194
SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+ − 195
| _ => NONE
+ − 196
end
+ − 197
+ − 198
fun quot_true_simple_conv ctxt fnctn ctrm =
+ − 199
case (term_of ctrm) of
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 200
(Const (@{const_name Quot_True}, _) $ x) =>
758
+ − 201
let
+ − 202
val fx = fnctn x;
+ − 203
val thy = ProofContext.theory_of ctxt;
+ − 204
val cx = cterm_of thy x;
+ − 205
val cfx = cterm_of thy fx;
+ − 206
val cxt = ctyp_of thy (fastype_of x);
+ − 207
val cfxt = ctyp_of thy (fastype_of fx);
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 208
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
758
+ − 209
in
+ − 210
Conv.rewr_conv thm ctrm
+ − 211
end
+ − 212
+ − 213
fun quot_true_conv ctxt fnctn ctrm =
+ − 214
case (term_of ctrm) of
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 215
(Const (@{const_name Quot_True}, _) $ _) =>
758
+ − 216
quot_true_simple_conv ctxt fnctn ctrm
+ − 217
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+ − 218
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+ − 219
| _ => Conv.all_conv ctrm
+ − 220
1128
+ − 221
fun quot_true_tac ctxt fnctn =
758
+ − 222
CONVERSION
+ − 223
((Conv.params_conv ~1 (fn ctxt =>
+ − 224
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
+ − 225
1128
+ − 226
fun dest_comb (f $ a) = (f, a)
+ − 227
fun dest_bcomb ((_ $ l) $ r) = (l, r)
758
+ − 228
+ − 229
fun unlam t =
+ − 230
case t of
+ − 231
(Abs a) => snd (Term.dest_abs a)
+ − 232
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
+ − 233
+ − 234
fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+ − 235
| dest_fun_type _ = error "dest_fun_type"
+ − 236
+ − 237
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
+ − 238
848
+ − 239
(* We apply apply_rsp only in case if the type needs lifting.
+ − 240
This is the case if the type of the data in the Quot_True
1128
+ − 241
assumption is different from the corresponding type in the goal.
858
+ − 242
*)
758
+ − 243
val apply_rsp_tac =
+ − 244
Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ − 245
let
+ − 246
val bare_concl = HOLogic.dest_Trueprop (term_of concl)
+ − 247
val qt_asm = find_qt_asm (map term_of asms)
+ − 248
in
+ − 249
case (bare_concl, qt_asm) of
+ − 250
(R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
1102
+ − 251
if fastype_of qt_fun = fastype_of f
848
+ − 252
then no_tac
+ − 253
else
758
+ − 254
let
+ − 255
val ty_x = fastype_of x
+ − 256
val ty_b = fastype_of qt_arg
848
+ − 257
val ty_f = range_type (fastype_of f)
758
+ − 258
val thy = ProofContext.theory_of context
+ − 259
val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
+ − 260
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
848
+ − 261
val inst_thm = Drule.instantiate' ty_inst
+ − 262
([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
758
+ − 263
in
+ − 264
(rtac inst_thm THEN' quotient_tac context) 1
+ − 265
end
+ − 266
| _ => no_tac
+ − 267
end)
+ − 268
842
+ − 269
(* Instantiates and applies 'equals_rsp'. Since the theorem is
1128
+ − 270
complex we rely on instantiation to tell us if it applies
858
+ − 271
*)
758
+ − 272
fun equals_rsp_tac R ctxt =
+ − 273
let
+ − 274
val thy = ProofContext.theory_of ctxt
+ − 275
in
842
+ − 276
case try (cterm_of thy) R of (* There can be loose bounds in R *)
+ − 277
SOME ctm =>
+ − 278
let
+ − 279
val ty = domain_type (fastype_of R)
+ − 280
in
+ − 281
case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
+ − 282
[SOME (cterm_of thy R)]) @{thm equals_rsp} of
+ − 283
SOME thm => rtac thm THEN' quotient_tac ctxt
+ − 284
| NONE => K no_tac
+ − 285
end
+ − 286
| _ => K no_tac
758
+ − 287
end
+ − 288
847
+ − 289
fun rep_abs_rsp_tac ctxt =
758
+ − 290
SUBGOAL (fn (goal, i) =>
847
+ − 291
case (try bare_concl goal) of
+ − 292
SOME (rel $ _ $ (rep $ (abs $ _))) =>
+ − 293
let
+ − 294
val thy = ProofContext.theory_of ctxt;
+ − 295
val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+ − 296
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+ − 297
in
+ − 298
case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
+ − 299
SOME t_inst =>
+ − 300
(case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
+ − 301
SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
+ − 302
| NONE => no_tac)
+ − 303
| NONE => no_tac
+ − 304
end
758
+ − 305
| _ => no_tac)
+ − 306
+ − 307
858
+ − 308
1128
+ − 309
(* Injection means to prove that the regularised theorem implies
858
+ − 310
the abs/rep injected one.
758
+ − 311
858
+ − 312
The deterministic part:
+ − 313
- remove lambdas from both sides
+ − 314
- prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
+ − 315
- prove Ball/Bex relations unfolding fun_rel_id
+ − 316
- reflexivity of equality
+ − 317
- prove equality of relations using equals_rsp
+ − 318
- use user-supplied RSP theorems
+ − 319
- solve 'relation of relations' goals using quot_rel_rsp
+ − 320
- remove rep_abs from the right side
+ − 321
(Lambdas under respects may have left us some assumptions)
1128
+ − 322
858
+ − 323
Then in order:
+ − 324
- split applications of lifted type (apply_rsp)
+ − 325
- split applications of non-lifted type (cong_tac)
+ − 326
- apply extentionality
+ − 327
- assumption
+ − 328
- reflexivity of the relation
758
+ − 329
*)
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 330
fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
758
+ − 331
(case (bare_concl goal) of
+ − 332
(* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
+ − 333
(Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
+ − 334
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 335
+ − 336
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
+ − 337
| (Const (@{const_name "op ="},_) $
+ − 338
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 339
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ − 340
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+ − 341
+ − 342
(* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
+ − 343
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ − 344
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 345
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 346
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 347
+ − 348
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
+ − 349
| Const (@{const_name "op ="},_) $
+ − 350
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 351
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 352
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+ − 353
+ − 354
(* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
+ − 355
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ − 356
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 357
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 358
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 359
911
+ − 360
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
980
+ − 361
(Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
1120
+ − 362
=> rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
911
+ − 363
758
+ − 364
| (_ $
+ − 365
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 366
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ − 367
=> rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+ − 368
1128
+ − 369
| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
758
+ − 370
(rtac @{thm refl} ORELSE'
+ − 371
(equals_rsp_tac R ctxt THEN' RANGE [
+ − 372
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+ − 373
+ − 374
(* reflexivity of operators arising from Cong_tac *)
+ − 375
| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
+ − 376
+ − 377
(* respectfulness of constants; in particular of a simple relation *)
+ − 378
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ − 379
=> resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+ − 380
+ − 381
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
+ − 382
(* observe fun_map *)
+ − 383
| _ $ _ $ _
1128
+ − 384
=> (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
758
+ − 385
ORELSE' rep_abs_rsp_tac ctxt
+ − 386
+ − 387
| _ => K no_tac
+ − 388
) i)
+ − 389
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 390
fun injection_step_tac ctxt rel_refl =
758
+ − 391
FIRST' [
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 392
injection_match_tac ctxt,
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 393
853
+ − 394
(* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *)
758
+ − 395
apply_rsp_tac ctxt THEN'
+ − 396
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
+ − 397
+ − 398
(* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *)
+ − 399
(* merge with previous tactic *)
+ − 400
Cong_Tac.cong_tac @{thm cong} THEN'
+ − 401
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
853
+ − 402
758
+ − 403
(* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
+ − 404
rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
853
+ − 405
758
+ − 406
(* resolving with R x y assumptions *)
+ − 407
atac,
853
+ − 408
758
+ − 409
(* reflexivity of the basic relations *)
+ − 410
(* R ... ... *)
+ − 411
resolve_tac rel_refl]
+ − 412
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 413
fun injection_tac ctxt =
758
+ − 414
let
+ − 415
val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
+ − 416
in
845
+ − 417
injection_step_tac ctxt rel_refl
758
+ − 418
end
+ − 419
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 420
fun all_injection_tac ctxt =
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 421
REPEAT_ALL_NEW (injection_tac ctxt)
758
+ − 422
+ − 423
+ − 424
858
+ − 425
(*** Cleaning of the Theorem ***)
848
+ − 426
951
+ − 427
(* expands all fun_maps, except in front of the (bound) variables listed in xs *)
758
+ − 428
fun fun_map_simple_conv xs ctrm =
+ − 429
case (term_of ctrm) of
+ − 430
((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
1102
+ − 431
if member (op=) xs h
758
+ − 432
then Conv.all_conv ctrm
1128
+ − 433
else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
758
+ − 434
| _ => Conv.all_conv ctrm
+ − 435
+ − 436
fun fun_map_conv xs ctxt ctrm =
+ − 437
case (term_of ctrm) of
+ − 438
_ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
+ − 439
fun_map_simple_conv xs) ctrm
+ − 440
| Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+ − 441
| _ => Conv.all_conv ctrm
+ − 442
+ − 443
fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+ − 444
951
+ − 445
(* custom matching functions *)
758
+ − 446
fun mk_abs u i t =
1112
+ − 447
if incr_boundvars i u aconv t then Bound i else
+ − 448
case t of
+ − 449
t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
+ − 450
| Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
+ − 451
| Bound j => if i = j then error "make_inst" else t
+ − 452
| _ => t
758
+ − 453
+ − 454
fun make_inst lhs t =
+ − 455
let
+ − 456
val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+ − 457
val _ $ (Abs (_, _, (_ $ g))) = t;
+ − 458
in
+ − 459
(f, Abs ("x", T, mk_abs u 0 g))
+ − 460
end
+ − 461
+ − 462
fun make_inst_id lhs t =
+ − 463
let
+ − 464
val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ − 465
val _ $ (Abs (_, _, g)) = t;
+ − 466
in
+ − 467
(f, Abs ("x", T, mk_abs u 0 g))
+ − 468
end
+ − 469
846
+ − 470
(* Simplifies a redex using the 'lambda_prs' theorem.
+ − 471
First instantiates the types and known subterms.
+ − 472
Then solves the quotient assumptions to get Rep2 and Abs1
+ − 473
Finally instantiates the function f using make_inst
+ − 474
If Rep2 is an identity then the pattern is simpler and
1128
+ − 475
make_inst_id is used
858
+ − 476
*)
758
+ − 477
fun lambda_prs_simple_conv ctxt ctrm =
+ − 478
case (term_of ctrm) of
846
+ − 479
(Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
+ − 480
let
+ − 481
val thy = ProofContext.theory_of ctxt
+ − 482
val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+ − 483
val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ − 484
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+ − 485
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
951
+ − 486
val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
+ − 487
val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
+ − 488
val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
846
+ − 489
val (insp, inst) =
+ − 490
if ty_c = ty_d
951
+ − 491
then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
+ − 492
else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
+ − 493
val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
846
+ − 494
in
951
+ − 495
Conv.rewr_conv thm4 ctrm
846
+ − 496
end
758
+ − 497
| _ => Conv.all_conv ctrm
+ − 498
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 499
fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
758
+ − 500
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
+ − 501
+ − 502
848
+ − 503
(* Cleaning consists of:
858
+ − 504
940
a792bfc1be2b
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 505
1. unfolding of ---> in front of everything, except
1128
+ − 506
bound variables (this prevents lambda_prs from
951
+ − 507
becoming stuck)
848
+ − 508
940
a792bfc1be2b
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 509
2. simplification with lambda_prs
848
+ − 510
1128
+ − 511
3. simplification with:
951
+ − 512
1128
+ − 513
- Quotient_abs_rep Quotient_rel_rep
951
+ − 514
babs_prs all_prs ex_prs ex1_prs
964
+ − 515
1128
+ − 516
- id_simps and preservation lemmas and
964
+ − 517
1128
+ − 518
- symmetric versions of the definitions
+ − 519
(that is definitions of quotient constants
964
+ − 520
are folded)
848
+ − 521
940
a792bfc1be2b
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 522
4. test for refl
858
+ − 523
*)
845
+ − 524
fun clean_tac lthy =
785
+ − 525
let
1157
+ − 526
val defs = map (symmetric o #def) (qconsts_dest lthy)
789
+ − 527
val prs = prs_rules_get lthy
+ − 528
val ids = id_simps_get lthy
951
+ − 529
val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
853
+ − 530
951
+ − 531
val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
785
+ − 532
in
940
a792bfc1be2b
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 533
EVERY' [fun_map_tac lthy,
785
+ − 534
lambda_prs_tac lthy,
940
a792bfc1be2b
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 535
simp_tac ss,
853
+ − 536
TRY o rtac refl]
785
+ − 537
end
758
+ − 538
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 539
848
+ − 540
+ − 541
(** Tactic for Generalising Free Variables in a Goal **)
+ − 542
758
+ − 543
fun inst_spec ctrm =
+ − 544
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+ − 545
+ − 546
fun inst_spec_tac ctrms =
+ − 547
EVERY' (map (dtac o inst_spec) ctrms)
+ − 548
1128
+ − 549
fun all_list xs trm =
758
+ − 550
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
+ − 551
1128
+ − 552
fun apply_under_Trueprop f =
758
+ − 553
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
+ − 554
+ − 555
fun gen_frees_tac ctxt =
853
+ − 556
SUBGOAL (fn (concl, i) =>
+ − 557
let
+ − 558
val thy = ProofContext.theory_of ctxt
+ − 559
val vrs = Term.add_frees concl []
+ − 560
val cvrs = map (cterm_of thy o Free) vrs
+ − 561
val concl' = apply_under_Trueprop (all_list vrs) concl
+ − 562
val goal = Logic.mk_implies (concl', concl)
+ − 563
val rule = Goal.prove ctxt [] [] goal
+ − 564
(K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+ − 565
in
+ − 566
rtac rule i
+ − 567
end)
758
+ − 568
848
+ − 569
+ − 570
(** The General Shape of the Lifting Procedure **)
+ − 571
+ − 572
(* - A is the original raw theorem
858
+ − 573
- B is the regularized theorem
+ − 574
- C is the rep/abs injected version of B
+ − 575
- D is the lifted theorem
758
+ − 576
858
+ − 577
- 1st prem is the regularization step
+ − 578
- 2nd prem is the rep/abs injection step
+ − 579
- 3rd prem is the cleaning part
848
+ − 580
1128
+ − 581
the Quot_True premise in 2nd records the lifted theorem
858
+ − 582
*)
853
+ − 583
val lifting_procedure_thm =
+ − 584
@{lemma "[|A;
+ − 585
A --> B;
+ − 586
Quot_True D ==> B = C;
+ − 587
C = D|] ==> D"
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 588
by (simp add: Quot_True_def)}
758
+ − 589
1112
+ − 590
fun lift_match_error ctxt msg rtrm qtrm =
758
+ − 591
let
+ − 592
val rtrm_str = Syntax.string_of_term ctxt rtrm
+ − 593
val qtrm_str = Syntax.string_of_term ctxt qtrm
1128
+ − 594
val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
848
+ − 595
"", "does not match with original theorem", rtrm_str]
758
+ − 596
in
+ − 597
error msg
+ − 598
end
848
+ − 599
758
+ − 600
fun procedure_inst ctxt rtrm qtrm =
+ − 601
let
+ − 602
val thy = ProofContext.theory_of ctxt
+ − 603
val rtrm' = HOLogic.dest_Trueprop rtrm
+ − 604
val qtrm' = HOLogic.dest_Trueprop qtrm
776
d1064fa29424
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 605
val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
1450
+ − 606
handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
776
d1064fa29424
renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 607
val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
1450
+ − 608
handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm
758
+ − 609
in
+ − 610
Drule.instantiate' []
+ − 611
[SOME (cterm_of thy rtrm'),
+ − 612
SOME (cterm_of thy reg_goal),
+ − 613
NONE,
802
+ − 614
SOME (cterm_of thy inj_goal)] lifting_procedure_thm
758
+ − 615
end
+ − 616
+ − 617
(* the tactic leaves three subgoals to be proved *)
+ − 618
fun procedure_tac ctxt rthm =
1354
+ − 619
Object_Logic.full_atomize_tac
758
+ − 620
THEN' gen_frees_tac ctxt
785
+ − 621
THEN' SUBGOAL (fn (goal, i) =>
758
+ − 622
let
+ − 623
val rthm' = atomize_thm rthm
785
+ − 624
val rule = procedure_inst ctxt (prop_of rthm') goal
758
+ − 625
in
+ − 626
(rtac rule THEN' rtac rthm') i
+ − 627
end)
+ − 628
+ − 629
+ − 630
(* Automatic Proofs *)
+ − 631
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 632
val msg1 = "The regularize proof failed."
1128
+ − 633
val msg2 = cat_lines ["The injection proof failed.",
758
+ − 634
"This is probably due to missing respects lemmas.",
1128
+ − 635
"Try invoking the injection method manually to see",
758
+ − 636
"which lemmas are missing."]
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 637
val msg3 = "The cleaning proof failed."
758
+ − 638
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 639
fun lift_tac ctxt rthms =
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 640
let
1128
+ − 641
fun mk_tac rthm =
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 642
procedure_tac ctxt rthm
1128
+ − 643
THEN' RANGE_WARN
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 644
[(regularize_tac ctxt, msg1),
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 645
(all_injection_tac ctxt, msg2),
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 646
(clean_tac ctxt, msg3)]
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 647
in
1128
+ − 648
simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 649
THEN' RANGE (map mk_tac rthms)
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 650
end
758
+ − 651
1078
+ − 652
(* An Attribute which automatically constructs the qthm *)
+ − 653
fun lifted_attrib_aux context thm =
1068
+ − 654
let
1077
+ − 655
val ctxt = Context.proof_of context
1082
+ − 656
val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
1083
+ − 657
val goal = (quotient_lift_all ctxt' o prop_of) thm'
1068
+ − 658
in
1084
+ − 659
Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
+ − 660
|> singleton (ProofContext.export ctxt' ctxt)
1068
+ − 661
end;
+ − 662
1078
+ − 663
val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
1068
+ − 664
814
+ − 665
end; (* structure *)