758
+ − 1
signature QUOTIENT_TACS =
+ − 2
sig
+ − 3
val regularize_tac: Proof.context -> int -> tactic
+ − 4
val all_inj_repabs_tac: Proof.context -> int -> tactic
+ − 5
val clean_tac: Proof.context -> int -> tactic
+ − 6
val procedure_tac: Proof.context -> thm -> int -> tactic
+ − 7
val lift_tac: Proof.context ->thm -> int -> tactic
+ − 8
val quotient_tac: Proof.context -> int -> tactic
+ − 9
end;
+ − 10
+ − 11
structure Quotient_Tacs: QUOTIENT_TACS =
+ − 12
struct
+ − 13
762
+ − 14
open Quotient_Info;
+ − 15
open Quotient_Type;
+ − 16
open Quotient_Term;
+ − 17
+ − 18
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
+ − 19
(* 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
+ − 20
(* need to set up our own minimal simpset. *)
758
+ − 21
fun mk_minimal_ss ctxt =
+ − 22
Simplifier.context ctxt empty_ss
+ − 23
setsubgoaler asm_simp_tac
+ − 24
setmksimps (mksimps [])
+ − 25
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
+ − 26
(* various helper fuctions *)
758
+ − 27
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
+ − 28
(* composition of two theorems, used in map *)
758
+ − 29
fun OF1 thm1 thm2 = thm2 RS thm1
+ − 30
+ − 31
(* makes sure a subgoal is solved *)
+ − 32
fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
+ − 33
+ − 34
(* prints warning, if goal is unsolved *)
+ − 35
fun WARN (tac, msg) i st =
+ − 36
case Seq.pull ((SOLVES' tac) i st) of
+ − 37
NONE => (warning msg; Seq.single st)
+ − 38
| seqcell => Seq.make (fn () => seqcell)
+ − 39
+ − 40
fun RANGE_WARN xs = RANGE (map WARN xs)
+ − 41
+ − 42
fun atomize_thm thm =
+ − 43
let
+ − 44
val thm' = Thm.freezeT (forall_intr_vars thm)
+ − 45
val thm'' = ObjectLogic.atomize (cprop_of thm')
+ − 46
in
+ − 47
@{thm equal_elim_rule1} OF [thm'', thm']
+ − 48
end
+ − 49
+ − 50
+ − 51
(* Regularize Tactic *)
+ − 52
+ − 53
fun equiv_tac ctxt =
+ − 54
REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
+ − 55
+ − 56
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
+ − 57
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+ − 58
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
+ − 59
fun solve_equiv_assm ctxt thm =
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
+ − 60
case Seq.pull (equiv_tac ctxt 1 thm) of
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
+ − 61
SOME (t, _) => t
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
+ − 62
| _ => error "solve_equiv_assm failed."
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
+ − 63
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
+ − 64
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
+ − 65
758
+ − 66
fun prep_trm thy (x, (T, t)) =
+ − 67
(cterm_of thy (Var (x, T)), cterm_of thy t)
+ − 68
+ − 69
fun prep_ty thy (x, (S, ty)) =
+ − 70
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+ − 71
+ − 72
fun matching_prs thy pat trm =
+ − 73
let
+ − 74
val univ = Unify.matchers thy [(pat, trm)]
+ − 75
val SOME (env, _) = Seq.pull univ
+ − 76
val tenv = Vartab.dest (Envir.term_env env)
+ − 77
val tyenv = Vartab.dest (Envir.type_env env)
+ − 78
in
+ − 79
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ − 80
end
+ − 81
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
+ − 82
(* calculates the instantiations for te lemmas *)
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
+ − 83
(* ball_reg_eqv_range and bex_reg_eqv_range *)
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
+ − 84
fun calculate_instance ctxt ball_bex_thm redex R1 R2 =
758
+ − 85
let
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
+ − 86
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
758
+ − 87
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
+ − 88
val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
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
+ − 89
val trm_inst1 = map (SOME o cterm_of thy) [R2, R1]
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
+ − 90
val thm' = Drule.instantiate' typ_inst1 trm_inst1 ball_bex_thm
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
+ − 91
val inst2 = matching_prs thy (get_lhs thm') redex
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
+ − 92
val thm'' = Drule.instantiate inst2 thm'
758
+ − 93
in
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
+ − 94
SOME thm''
758
+ − 95
end
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
+ − 96
handle _ => NONE
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
+ − 97
(* FIXME/TODO: !!!CLEVER CODE!!! *)
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
+ − 98
(* FIXME/TODO: What is the place where the exception is raised, *)
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
+ − 99
(* FIXME/TODO: and which exception is it? *)
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
+ − 100
(* FIXME/TODO: Can one not find out from the types of R1 or R2, *)
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
+ − 101
(* FIXME/TODO: or from their form, when NONE should be returned? *)
758
+ − 102
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
+ − 103
758
+ − 104
fun ball_bex_range_simproc ss redex =
+ − 105
let
+ − 106
val ctxt = Simplifier.the_context ss
+ − 107
in
+ − 108
case redex of
+ − 109
(Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
+ − 110
(Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
770
+ − 111
calculate_instance ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
758
+ − 112
+ − 113
| (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+ − 114
(Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
770
+ − 115
calculate_instance ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
758
+ − 116
| _ => NONE
+ − 117
end
+ − 118
+ − 119
(* test whether DETERM makes any difference *)
+ − 120
fun quotient_tac ctxt = SOLVES'
+ − 121
(REPEAT_ALL_NEW (FIRST'
+ − 122
[rtac @{thm identity_quotient},
+ − 123
resolve_tac (quotient_rules_get ctxt)]))
+ − 124
+ − 125
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+ − 126
val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+ − 127
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
+ − 128
fun solve_quotient_assm ctxt thm =
758
+ − 129
case Seq.pull (quotient_tac ctxt 1 thm) of
+ − 130
SOME (t, _) => t
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
+ − 131
| _ => error "solve_quotient_assm failed. Maybe a quotient_thm is missing"
758
+ − 132
+ − 133
+ − 134
(* 0. preliminary simplification step according to *)
+ − 135
(* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *)
+ − 136
(* ball_reg_eqv_range bex_reg_eqv_range *)
+ − 137
(* *)
+ − 138
(* 1. eliminating simple Ball/Bex instances *)
+ − 139
(* thm ball_reg_right bex_reg_left *)
+ − 140
(* *)
+ − 141
(* 2. monos *)
+ − 142
(* 3. commutation rules for ball and bex *)
+ − 143
(* thm ball_all_comm bex_ex_comm *)
+ − 144
(* *)
+ − 145
(* 4. then rel-equality (which need to be *)
+ − 146
(* instantiated to avoid loops) *)
+ − 147
(* thm eq_imp_rel *)
+ − 148
(* *)
+ − 149
(* 5. then simplification like 0 *)
+ − 150
(* *)
+ − 151
(* finally jump back to 1 *)
+ − 152
+ − 153
fun regularize_tac ctxt =
+ − 154
let
+ − 155
val thy = ProofContext.theory_of ctxt
+ − 156
val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
+ − 157
val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"}
+ − 158
val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+ − 159
val simpset = (mk_minimal_ss ctxt)
+ − 160
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+ − 161
addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver
+ − 162
val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
+ − 163
in
+ − 164
simp_tac simpset THEN'
+ − 165
REPEAT_ALL_NEW (CHANGED o FIRST' [
+ − 166
resolve_tac @{thms ball_reg_right bex_reg_left},
+ − 167
resolve_tac (Inductive.get_monos ctxt),
+ − 168
resolve_tac @{thms ball_all_comm bex_ex_comm},
+ − 169
resolve_tac eq_eqvs,
+ − 170
simp_tac simpset])
+ − 171
end
+ − 172
+ − 173
+ − 174
+ − 175
(* Injection Tactic *)
+ − 176
+ − 177
(* looks for QUOT_TRUE assumtions, and in case its parameter *)
+ − 178
(* is an application, it returns the function and the argument *)
+ − 179
fun find_qt_asm asms =
+ − 180
let
+ − 181
fun find_fun trm =
+ − 182
case trm of
+ − 183
(Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+ − 184
| _ => false
+ − 185
in
+ − 186
case find_first find_fun asms of
+ − 187
SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+ − 188
| _ => NONE
+ − 189
end
+ − 190
+ − 191
fun quot_true_simple_conv ctxt fnctn ctrm =
+ − 192
case (term_of ctrm) of
+ − 193
(Const (@{const_name QUOT_TRUE}, _) $ x) =>
+ − 194
let
+ − 195
val fx = fnctn x;
+ − 196
val thy = ProofContext.theory_of ctxt;
+ − 197
val cx = cterm_of thy x;
+ − 198
val cfx = cterm_of thy fx;
+ − 199
val cxt = ctyp_of thy (fastype_of x);
+ − 200
val cfxt = ctyp_of thy (fastype_of fx);
+ − 201
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
+ − 202
in
+ − 203
Conv.rewr_conv thm ctrm
+ − 204
end
+ − 205
+ − 206
fun quot_true_conv ctxt fnctn ctrm =
+ − 207
case (term_of ctrm) of
+ − 208
(Const (@{const_name QUOT_TRUE}, _) $ _) =>
+ − 209
quot_true_simple_conv ctxt fnctn ctrm
+ − 210
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+ − 211
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+ − 212
| _ => Conv.all_conv ctrm
+ − 213
+ − 214
fun quot_true_tac ctxt fnctn =
+ − 215
CONVERSION
+ − 216
((Conv.params_conv ~1 (fn ctxt =>
+ − 217
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
+ − 218
+ − 219
fun dest_comb (f $ a) = (f, a)
+ − 220
fun dest_bcomb ((_ $ l) $ r) = (l, r)
+ − 221
+ − 222
(* TODO: Can this be done easier? *)
+ − 223
fun unlam t =
+ − 224
case t of
+ − 225
(Abs a) => snd (Term.dest_abs a)
+ − 226
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
+ − 227
+ − 228
fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+ − 229
| dest_fun_type _ = error "dest_fun_type"
+ − 230
+ − 231
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
+ − 232
+ − 233
+ − 234
(* we apply apply_rsp only in case if the type needs lifting, *)
+ − 235
(* which is the case if the type of the data in the QUOT_TRUE *)
+ − 236
(* assumption is different from the corresponding type in the goal *)
+ − 237
val apply_rsp_tac =
+ − 238
Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ − 239
let
+ − 240
val bare_concl = HOLogic.dest_Trueprop (term_of concl)
+ − 241
val qt_asm = find_qt_asm (map term_of asms)
+ − 242
in
+ − 243
case (bare_concl, qt_asm) of
+ − 244
(R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
+ − 245
if (fastype_of qt_fun) = (fastype_of f)
+ − 246
then no_tac
+ − 247
else
+ − 248
let
+ − 249
val ty_x = fastype_of x
+ − 250
val ty_b = fastype_of qt_arg
+ − 251
val ty_f = range_type (fastype_of f)
+ − 252
val thy = ProofContext.theory_of context
+ − 253
val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
+ − 254
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+ − 255
val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
+ − 256
in
+ − 257
(rtac inst_thm THEN' quotient_tac context) 1
+ − 258
end
+ − 259
| _ => no_tac
+ − 260
end)
+ − 261
+ − 262
fun equals_rsp_tac R ctxt =
+ − 263
let
+ − 264
val ty = domain_type (fastype_of R);
+ − 265
val thy = ProofContext.theory_of ctxt
+ − 266
val thm = Drule.instantiate'
+ − 267
[SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
+ − 268
in
+ − 269
rtac thm THEN' quotient_tac ctxt
+ − 270
end
+ − 271
(* raised by instantiate' *)
+ − 272
handle THM _ => K no_tac
+ − 273
| TYPE _ => K no_tac
+ − 274
| TERM _ => K no_tac
+ − 275
+ − 276
+ − 277
fun rep_abs_rsp_tac ctxt =
+ − 278
SUBGOAL (fn (goal, i) =>
+ − 279
case (bare_concl goal) of
+ − 280
(rel $ _ $ (rep $ (abs $ _))) =>
+ − 281
(let
+ − 282
val thy = ProofContext.theory_of ctxt;
+ − 283
val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+ − 284
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+ − 285
val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
+ − 286
val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+ − 287
in
+ − 288
(rtac inst_thm THEN' quotient_tac ctxt) i
+ − 289
end
+ − 290
handle THM _ => no_tac | TYPE _ => no_tac)
+ − 291
| _ => no_tac)
+ − 292
+ − 293
+ − 294
(* FIXME /TODO needs to be adapted *)
+ − 295
(*
+ − 296
To prove that the regularised theorem implies the abs/rep injected,
+ − 297
we try:
+ − 298
+ − 299
1) theorems 'trans2' from the appropriate QUOT_TYPE
+ − 300
2) remove lambdas from both sides: lambda_rsp_tac
+ − 301
3) remove Ball/Bex from the right hand side
+ − 302
4) use user-supplied RSP theorems
+ − 303
5) remove rep_abs from the right side
+ − 304
6) reflexivity of equality
+ − 305
7) split applications of lifted type (apply_rsp)
+ − 306
8) split applications of non-lifted type (cong_tac)
+ − 307
9) apply extentionality
+ − 308
A) reflexivity of the relation
+ − 309
B) assumption
+ − 310
(Lambdas under respects may have left us some assumptions)
+ − 311
C) proving obvious higher order equalities by simplifying fun_rel
+ − 312
(not sure if it is still needed?)
+ − 313
D) unfolding lambda on one side
+ − 314
E) simplifying (= ===> =) for simpler respectfulness
+ − 315
*)
+ − 316
+ − 317
+ − 318
fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
+ − 319
(case (bare_concl goal) of
+ − 320
(* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
+ − 321
(Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
+ − 322
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 323
+ − 324
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
+ − 325
| (Const (@{const_name "op ="},_) $
+ − 326
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 327
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ − 328
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+ − 329
+ − 330
(* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
+ − 331
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ − 332
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 333
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 334
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 335
+ − 336
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
+ − 337
| Const (@{const_name "op ="},_) $
+ − 338
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 339
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 340
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+ − 341
+ − 342
(* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
+ − 343
| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ − 344
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 345
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ − 346
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+ − 347
+ − 348
| (_ $
+ − 349
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ − 350
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ − 351
=> rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+ − 352
+ − 353
| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+ − 354
(rtac @{thm refl} ORELSE'
+ − 355
(equals_rsp_tac R ctxt THEN' RANGE [
+ − 356
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+ − 357
+ − 358
(* reflexivity of operators arising from Cong_tac *)
+ − 359
| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
+ − 360
+ − 361
(* respectfulness of constants; in particular of a simple relation *)
+ − 362
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ − 363
=> resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+ − 364
+ − 365
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
+ − 366
(* observe fun_map *)
+ − 367
| _ $ _ $ _
+ − 368
=> (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
+ − 369
ORELSE' rep_abs_rsp_tac ctxt
+ − 370
+ − 371
| _ => K no_tac
+ − 372
) i)
+ − 373
+ − 374
fun inj_repabs_step_tac ctxt rel_refl =
+ − 375
FIRST' [
+ − 376
inj_repabs_tac_match ctxt,
+ − 377
(* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *)
+ − 378
+ − 379
apply_rsp_tac ctxt THEN'
+ − 380
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
+ − 381
+ − 382
(* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *)
+ − 383
(* merge with previous tactic *)
+ − 384
Cong_Tac.cong_tac @{thm cong} THEN'
+ − 385
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
+ − 386
+ − 387
(* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
+ − 388
rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
+ − 389
+ − 390
(* resolving with R x y assumptions *)
+ − 391
atac,
+ − 392
+ − 393
(* reflexivity of the basic relations *)
+ − 394
(* R ... ... *)
+ − 395
resolve_tac rel_refl]
+ − 396
+ − 397
fun inj_repabs_tac ctxt =
+ − 398
let
+ − 399
val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
+ − 400
in
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 401
simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *)
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 402
THEN' inj_repabs_step_tac ctxt rel_refl
758
+ − 403
end
+ − 404
+ − 405
fun all_inj_repabs_tac ctxt =
+ − 406
REPEAT_ALL_NEW (inj_repabs_tac ctxt)
+ − 407
+ − 408
+ − 409
(* Cleaning of the Theorem *)
+ − 410
+ − 411
+ − 412
(* expands all fun_maps, except in front of bound variables *)
+ − 413
fun fun_map_simple_conv xs ctrm =
+ − 414
case (term_of ctrm) of
+ − 415
((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
+ − 416
if (member (op=) xs h)
+ − 417
then Conv.all_conv ctrm
+ − 418
else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm
+ − 419
| _ => Conv.all_conv ctrm
+ − 420
+ − 421
fun fun_map_conv xs ctxt ctrm =
+ − 422
case (term_of ctrm) of
+ − 423
_ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
+ − 424
fun_map_simple_conv xs) ctrm
+ − 425
| Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+ − 426
| _ => Conv.all_conv ctrm
+ − 427
+ − 428
fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+ − 429
+ − 430
fun mk_abs u i t =
+ − 431
if incr_boundvars i u aconv t then Bound i
+ − 432
else (case t of
+ − 433
t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2)
+ − 434
| Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
+ − 435
| Bound j => if i = j then error "make_inst" else t
+ − 436
| _ => t)
+ − 437
+ − 438
fun make_inst lhs t =
+ − 439
let
+ − 440
val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+ − 441
val _ $ (Abs (_, _, (_ $ g))) = t;
+ − 442
in
+ − 443
(f, Abs ("x", T, mk_abs u 0 g))
+ − 444
end
+ − 445
+ − 446
fun make_inst_id lhs t =
+ − 447
let
+ − 448
val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ − 449
val _ $ (Abs (_, _, g)) = t;
+ − 450
in
+ − 451
(f, Abs ("x", T, mk_abs u 0 g))
+ − 452
end
+ − 453
+ − 454
(* Simplifies a redex using the 'lambda_prs' theorem. *)
+ − 455
(* First instantiates the types and known subterms. *)
+ − 456
(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
+ − 457
(* Finally instantiates the function f using make_inst *)
+ − 458
(* If Rep2 is identity then the pattern is simpler and *)
+ − 459
(* make_inst_id is used *)
+ − 460
fun lambda_prs_simple_conv ctxt ctrm =
+ − 461
case (term_of ctrm) of
+ − 462
(Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
+ − 463
(let
+ − 464
val thy = ProofContext.theory_of ctxt
+ − 465
val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+ − 466
val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ − 467
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+ − 468
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
770
+ − 469
val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
+ − 470
val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
758
+ − 471
val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+ − 472
val make_inst = if ty_c = ty_d then make_inst_id else make_inst
+ − 473
val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+ − 474
val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+ − 475
in
+ − 476
Conv.rewr_conv ti ctrm
+ − 477
end
+ − 478
handle _ => Conv.all_conv ctrm)
+ − 479
| _ => Conv.all_conv ctrm
+ − 480
+ − 481
val lambda_prs_conv =
+ − 482
More_Conv.top_conv lambda_prs_simple_conv
+ − 483
+ − 484
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
+ − 485
+ − 486
+ − 487
(* 1. folding of definitions and preservation lemmas; *)
+ − 488
(* and simplification with *)
+ − 489
(* thm babs_prs all_prs ex_prs *)
+ − 490
(* *)
+ − 491
(* 2. unfolding of ---> in front of everything, except *)
+ − 492
(* bound variables (this prevents lambda_prs from *)
+ − 493
(* becoming stuck *)
+ − 494
(* thm fun_map.simps *)
+ − 495
(* *)
+ − 496
(* 3. simplification with *)
+ − 497
(* thm lambda_prs *)
+ − 498
(* *)
+ − 499
(* 4. simplification with *)
+ − 500
(* thm Quotient_abs_rep Quotient_rel_rep id_simps *)
+ − 501
(* *)
+ − 502
(* 5. Test for refl *)
+ − 503
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 504
fun clean_tac_aux lthy =
758
+ − 505
let
+ − 506
val thy = ProofContext.theory_of lthy;
+ − 507
val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+ − 508
(* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+ − 509
+ − 510
val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
+ − 511
val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
+ − 512
fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+ − 513
in
+ − 514
EVERY' [simp_tac (simps thms1),
+ − 515
fun_map_tac lthy,
+ − 516
lambda_prs_tac lthy,
+ − 517
simp_tac (simps thms2),
+ − 518
TRY o rtac refl]
+ − 519
end
+ − 520
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 521
fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)
758
+ − 522
+ − 523
(* Tactic for Genralisation of Free Variables in a Goal *)
+ − 524
+ − 525
fun inst_spec ctrm =
+ − 526
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+ − 527
+ − 528
fun inst_spec_tac ctrms =
+ − 529
EVERY' (map (dtac o inst_spec) ctrms)
+ − 530
+ − 531
fun all_list xs trm =
+ − 532
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
+ − 533
+ − 534
fun apply_under_Trueprop f =
+ − 535
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
+ − 536
+ − 537
fun gen_frees_tac ctxt =
+ − 538
SUBGOAL (fn (concl, i) =>
+ − 539
let
+ − 540
val thy = ProofContext.theory_of ctxt
+ − 541
val vrs = Term.add_frees concl []
+ − 542
val cvrs = map (cterm_of thy o Free) vrs
+ − 543
val concl' = apply_under_Trueprop (all_list vrs) concl
+ − 544
val goal = Logic.mk_implies (concl', concl)
+ − 545
val rule = Goal.prove ctxt [] [] goal
+ − 546
(K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+ − 547
in
+ − 548
rtac rule i
+ − 549
end)
+ − 550
+ − 551
+ − 552
(* The General Shape of the Lifting Procedure *)
+ − 553
+ − 554
(* - A is the original raw theorem *)
+ − 555
(* - B is the regularized theorem *)
+ − 556
(* - C is the rep/abs injected version of B *)
+ − 557
(* - D is the lifted theorem *)
+ − 558
(* *)
+ − 559
(* - 1st prem is the regularization step *)
+ − 560
(* - 2nd prem is the rep/abs injection step *)
+ − 561
(* - 3rd prem is the cleaning part *)
+ − 562
(* *)
+ − 563
(* the QUOT_TRUE premise in 2 records the lifted theorem *)
+ − 564
+ − 565
val lifting_procedure =
+ − 566
@{lemma "[|A;
+ − 567
A --> B;
+ − 568
QUOT_TRUE D ==> B = C;
+ − 569
C = D|] ==> D"
+ − 570
by (simp add: QUOT_TRUE_def)}
+ − 571
+ − 572
fun lift_match_error ctxt fun_str rtrm qtrm =
+ − 573
let
+ − 574
val rtrm_str = Syntax.string_of_term ctxt rtrm
+ − 575
val qtrm_str = Syntax.string_of_term ctxt qtrm
+ − 576
val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str,
+ − 577
"", "does not match with original theorem", rtrm_str]
+ − 578
in
+ − 579
error msg
+ − 580
end
+ − 581
+ − 582
fun procedure_inst ctxt rtrm qtrm =
+ − 583
let
+ − 584
val thy = ProofContext.theory_of ctxt
+ − 585
val rtrm' = HOLogic.dest_Trueprop rtrm
+ − 586
val qtrm' = HOLogic.dest_Trueprop qtrm
+ − 587
val reg_goal =
+ − 588
Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
+ − 589
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+ − 590
val inj_goal =
+ − 591
Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
+ − 592
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+ − 593
in
+ − 594
Drule.instantiate' []
+ − 595
[SOME (cterm_of thy rtrm'),
+ − 596
SOME (cterm_of thy reg_goal),
+ − 597
NONE,
+ − 598
SOME (cterm_of thy inj_goal)] lifting_procedure
+ − 599
end
+ − 600
+ − 601
+ − 602
(* the tactic leaves three subgoals to be proved *)
+ − 603
fun procedure_tac ctxt rthm =
+ − 604
ObjectLogic.full_atomize_tac
+ − 605
THEN' gen_frees_tac ctxt
+ − 606
THEN' CSUBGOAL (fn (goal, i) =>
+ − 607
let
+ − 608
val rthm' = atomize_thm rthm
+ − 609
val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
+ − 610
in
+ − 611
(rtac rule THEN' rtac rthm') i
+ − 612
end)
+ − 613
+ − 614
+ − 615
(* Automatic Proofs *)
+ − 616
+ − 617
val msg1 = "Regularize proof failed."
+ − 618
val msg2 = cat_lines ["Injection proof failed.",
+ − 619
"This is probably due to missing respects lemmas.",
+ − 620
"Try invoking the injection method manually to see",
+ − 621
"which lemmas are missing."]
+ − 622
val msg3 = "Cleaning proof failed."
+ − 623
+ − 624
fun lift_tac ctxt rthm =
+ − 625
procedure_tac ctxt rthm
+ − 626
THEN' RANGE_WARN
+ − 627
[(regularize_tac ctxt, msg1),
+ − 628
(all_inj_repabs_tac ctxt, msg2),
+ − 629
(clean_tac ctxt, msg3)]
+ − 630
762
+ − 631
end; (* structure *)