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