src/HOL/Tools/Quotient/quotient_tacs.ML
author wenzelm
Wed Mar 04 19:53:18 2015 +0100 (2015-03-04)
changeset 59582 0fbed69ff081
parent 59498 50b60f501b05
child 59585 68a770a8a09f
permissions -rw-r--r--
tuned signature -- prefer qualified names;
haftmann@37744
     1
(*  Title:      HOL/Tools/Quotient/quotient_tacs.ML
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
wenzelm@41444
    14
urbanc@38859
    15
  val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
urbanc@38859
    16
  val descend_tac: Proof.context -> thm list -> int -> tactic
urbanc@45782
    17
  val partiality_descend_procedure_tac: Proof.context -> thm list -> int -> tactic
urbanc@45782
    18
  val partiality_descend_tac: Proof.context -> thm list -> int -> tactic
urbanc@45782
    19
wenzelm@41444
    20
urbanc@38859
    21
  val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
urbanc@38859
    22
  val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
urbanc@37593
    23
urbanc@38625
    24
  val lifted: Proof.context -> typ list -> thm list -> thm -> thm
kaliszyk@35222
    25
  val lifted_attrib: attribute
kaliszyk@35222
    26
end;
kaliszyk@35222
    27
kaliszyk@35222
    28
structure Quotient_Tacs: QUOTIENT_TACS =
kaliszyk@35222
    29
struct
kaliszyk@35222
    30
kaliszyk@35222
    31
(** various helper fuctions **)
kaliszyk@35222
    32
kaliszyk@35222
    33
(* Since HOL_basic_ss is too "big" for us, we *)
kaliszyk@35222
    34
(* need to set up our own minimal simpset.    *)
wenzelm@51717
    35
fun mk_minimal_simpset ctxt =
wenzelm@51717
    36
  empty_simpset ctxt
wenzelm@45625
    37
  |> Simplifier.set_subgoaler asm_simp_tac
wenzelm@45625
    38
  |> Simplifier.set_mksimps (mksimps [])
kaliszyk@35222
    39
kaliszyk@35222
    40
(* composition of two theorems, used in maps *)
kaliszyk@35222
    41
fun OF1 thm1 thm2 = thm2 RS thm1
kaliszyk@35222
    42
wenzelm@54742
    43
fun atomize_thm ctxt thm =
wenzelm@41444
    44
  let
wenzelm@41444
    45
    val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
wenzelm@59582
    46
    val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
wenzelm@41444
    47
  in
wenzelm@41444
    48
    @{thm equal_elim_rule1} OF [thm'', thm']
wenzelm@41444
    49
  end
kaliszyk@35222
    50
kaliszyk@35222
    51
kaliszyk@35222
    52
kaliszyk@35222
    53
(*** Regularize Tactic ***)
kaliszyk@35222
    54
kaliszyk@35222
    55
(** solvers for equivp and quotient assumptions **)
kaliszyk@35222
    56
kaliszyk@35222
    57
fun equiv_tac ctxt =
wenzelm@59498
    58
  REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})))
kaliszyk@35222
    59
wenzelm@51717
    60
val equiv_solver = mk_solver "Equivalence goal solver" equiv_tac
kaliszyk@35222
    61
kaliszyk@35222
    62
fun quotient_tac ctxt =
kaliszyk@35222
    63
  (REPEAT_ALL_NEW (FIRST'
kuncar@47308
    64
    [rtac @{thm identity_quotient3},
wenzelm@59498
    65
     resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_thm}))]))
kaliszyk@35222
    66
wenzelm@51717
    67
val quotient_solver = mk_solver "Quotient goal solver" quotient_tac
kaliszyk@35222
    68
kaliszyk@35222
    69
fun solve_quotient_assm ctxt thm =
kaliszyk@35222
    70
  case Seq.pull (quotient_tac ctxt 1 thm) of
kaliszyk@35222
    71
    SOME (t, _) => t
kaliszyk@35222
    72
  | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
kaliszyk@35222
    73
kaliszyk@35222
    74
kaliszyk@35222
    75
fun prep_trm thy (x, (T, t)) =
wenzelm@59582
    76
  (Thm.cterm_of thy (Var (x, T)), Thm.cterm_of thy t)
kaliszyk@35222
    77
kaliszyk@35222
    78
fun prep_ty thy (x, (S, ty)) =
wenzelm@59582
    79
  (Thm.ctyp_of thy (TVar (x, S)), Thm.ctyp_of thy ty)
kaliszyk@35222
    80
kaliszyk@35222
    81
fun get_match_inst thy pat trm =
wenzelm@41444
    82
  let
wenzelm@58950
    83
    val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
wenzelm@41444
    84
    val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
wenzelm@41444
    85
    val tenv = Vartab.dest (Envir.term_env env)
wenzelm@41444
    86
    val tyenv = Vartab.dest (Envir.type_env env)
wenzelm@41444
    87
  in
wenzelm@41444
    88
    (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
wenzelm@41444
    89
  end
kaliszyk@35222
    90
kaliszyk@35222
    91
(* Calculates the instantiations for the lemmas:
kaliszyk@35222
    92
kaliszyk@35222
    93
      ball_reg_eqv_range and bex_reg_eqv_range
kaliszyk@35222
    94
kaliszyk@35222
    95
   Since the left-hand-side contains a non-pattern '?P (f ?x)'
kaliszyk@35222
    96
   we rely on unification/instantiation to check whether the
kaliszyk@35222
    97
   theorem applies and return NONE if it doesn't.
kaliszyk@35222
    98
*)
kaliszyk@35222
    99
fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
wenzelm@41444
   100
  let
wenzelm@42361
   101
    val thy = Proof_Context.theory_of ctxt
wenzelm@41444
   102
    fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
wenzelm@59582
   103
    val ty_inst = map (SOME o Thm.ctyp_of thy) [domain_type (fastype_of R2)]
wenzelm@59582
   104
    val trm_inst = map (SOME o Thm.cterm_of thy) [R2, R1]
wenzelm@41444
   105
  in
wenzelm@41444
   106
    (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
wenzelm@41444
   107
      NONE => NONE
wenzelm@41444
   108
    | SOME thm' =>
wenzelm@41444
   109
        (case try (get_match_inst thy (get_lhs thm')) redex of
wenzelm@41444
   110
          NONE => NONE
wenzelm@43333
   111
        | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
wenzelm@41444
   112
  end
kaliszyk@35222
   113
wenzelm@51717
   114
fun ball_bex_range_simproc ctxt redex =
wenzelm@51717
   115
  case redex of
wenzelm@51717
   116
    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
blanchet@55945
   117
      (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
wenzelm@51717
   118
        calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
kaliszyk@35222
   119
wenzelm@51717
   120
  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
blanchet@55945
   121
      (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
wenzelm@51717
   122
        calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
kaliszyk@35222
   123
wenzelm@51717
   124
  | _ => NONE
kaliszyk@35222
   125
kaliszyk@35222
   126
(* Regularize works as follows:
kaliszyk@35222
   127
kaliszyk@35222
   128
  0. preliminary simplification step according to
kaliszyk@35222
   129
     ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
kaliszyk@35222
   130
kaliszyk@35222
   131
  1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
kaliszyk@35222
   132
kaliszyk@35222
   133
  2. monos
kaliszyk@35222
   134
kaliszyk@35222
   135
  3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
kaliszyk@35222
   136
kaliszyk@35222
   137
  4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
kaliszyk@35222
   138
     to avoid loops
kaliszyk@35222
   139
kaliszyk@35222
   140
  5. then simplification like 0
kaliszyk@35222
   141
kaliszyk@35222
   142
  finally jump back to 1
kaliszyk@35222
   143
*)
kaliszyk@35222
   144
kaliszyk@37493
   145
fun reflp_get ctxt =
wenzelm@59582
   146
  map_filter (fn th => if Thm.prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
wenzelm@57960
   147
    handle THM _ => NONE) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
kaliszyk@37493
   148
kaliszyk@37493
   149
val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
kaliszyk@37493
   150
wenzelm@57960
   151
fun eq_imp_rel_get ctxt =
wenzelm@57960
   152
  map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
kaliszyk@37493
   153
kaliszyk@35222
   154
fun regularize_tac ctxt =
wenzelm@41444
   155
  let
wenzelm@42361
   156
    val thy = Proof_Context.theory_of ctxt
wenzelm@41444
   157
    val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
wenzelm@41444
   158
    val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
wenzelm@41444
   159
    val simproc =
wenzelm@51717
   160
      Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] ball_bex_range_simproc
wenzelm@41444
   161
    val simpset =
wenzelm@51717
   162
      mk_minimal_simpset ctxt
wenzelm@41444
   163
      addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
wenzelm@41444
   164
      addsimprocs [simproc]
wenzelm@41444
   165
      addSolver equiv_solver addSolver quotient_solver
wenzelm@41444
   166
    val eq_eqvs = eq_imp_rel_get ctxt
wenzelm@41444
   167
  in
wenzelm@41444
   168
    simp_tac simpset THEN'
kaliszyk@44285
   169
    TRY o REPEAT_ALL_NEW (CHANGED o FIRST'
wenzelm@59498
   170
      [resolve_tac ctxt @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
wenzelm@59498
   171
       resolve_tac ctxt (Inductive.get_monos ctxt),
wenzelm@59498
   172
       resolve_tac ctxt @{thms ball_all_comm bex_ex_comm},
wenzelm@59498
   173
       resolve_tac ctxt eq_eqvs,
wenzelm@41444
   174
       simp_tac simpset])
wenzelm@41444
   175
  end
kaliszyk@35222
   176
kaliszyk@35222
   177
kaliszyk@35222
   178
kaliszyk@35222
   179
(*** Injection Tactic ***)
kaliszyk@35222
   180
kaliszyk@35222
   181
(* Looks for Quot_True assumptions, and in case its parameter
kaliszyk@35222
   182
   is an application, it returns the function and the argument.
kaliszyk@35222
   183
*)
kaliszyk@35222
   184
fun find_qt_asm asms =
wenzelm@41444
   185
  let
wenzelm@41444
   186
    fun find_fun trm =
wenzelm@41444
   187
      (case trm of
wenzelm@41444
   188
        (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
wenzelm@41444
   189
      | _ => false)
wenzelm@41444
   190
  in
wenzelm@41444
   191
     (case find_first find_fun asms of
wenzelm@41444
   192
       SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
wenzelm@41444
   193
     | _ => NONE)
wenzelm@41444
   194
  end
kaliszyk@35222
   195
kaliszyk@35222
   196
fun quot_true_simple_conv ctxt fnctn ctrm =
wenzelm@59582
   197
  (case Thm.term_of ctrm of
kaliszyk@35222
   198
    (Const (@{const_name Quot_True}, _) $ x) =>
wenzelm@41444
   199
      let
wenzelm@41444
   200
        val fx = fnctn x;
wenzelm@42361
   201
        val thy = Proof_Context.theory_of ctxt;
wenzelm@59582
   202
        val cx = Thm.cterm_of thy x;
wenzelm@59582
   203
        val cfx = Thm.cterm_of thy fx;
wenzelm@59582
   204
        val cxt = Thm.ctyp_of thy (fastype_of x);
wenzelm@59582
   205
        val cfxt = Thm.ctyp_of thy (fastype_of fx);
wenzelm@41444
   206
        val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
wenzelm@41444
   207
      in
wenzelm@41444
   208
        Conv.rewr_conv thm ctrm
wenzelm@59582
   209
      end)
kaliszyk@35222
   210
kaliszyk@35222
   211
fun quot_true_conv ctxt fnctn ctrm =
wenzelm@59582
   212
  (case Thm.term_of ctrm of
kaliszyk@35222
   213
    (Const (@{const_name Quot_True}, _) $ _) =>
kaliszyk@35222
   214
      quot_true_simple_conv ctxt fnctn ctrm
kaliszyk@35222
   215
  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
kaliszyk@35222
   216
  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
wenzelm@41444
   217
  | _ => Conv.all_conv ctrm)
kaliszyk@35222
   218
kaliszyk@35222
   219
fun quot_true_tac ctxt fnctn =
wenzelm@41444
   220
  CONVERSION
kaliszyk@35222
   221
    ((Conv.params_conv ~1 (fn ctxt =>
wenzelm@41444
   222
        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
kaliszyk@35222
   223
kaliszyk@35222
   224
fun dest_comb (f $ a) = (f, a)
kaliszyk@35222
   225
fun dest_bcomb ((_ $ l) $ r) = (l, r)
kaliszyk@35222
   226
kaliszyk@35222
   227
fun unlam t =
wenzelm@41444
   228
  (case t of
wenzelm@41444
   229
    Abs a => snd (Term.dest_abs a)
wenzelm@41444
   230
  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
kaliszyk@35222
   231
kaliszyk@35222
   232
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
kaliszyk@35222
   233
kaliszyk@35222
   234
(* We apply apply_rsp only in case if the type needs lifting.
kaliszyk@35222
   235
   This is the case if the type of the data in the Quot_True
kaliszyk@35222
   236
   assumption is different from the corresponding type in the goal.
kaliszyk@35222
   237
*)
kaliszyk@35222
   238
val apply_rsp_tac =
kaliszyk@35222
   239
  Subgoal.FOCUS (fn {concl, asms, context,...} =>
wenzelm@41444
   240
    let
wenzelm@59582
   241
      val bare_concl = HOLogic.dest_Trueprop (Thm.term_of concl)
wenzelm@59582
   242
      val qt_asm = find_qt_asm (map Thm.term_of asms)
wenzelm@41444
   243
    in
wenzelm@41444
   244
      case (bare_concl, qt_asm) of
wenzelm@41444
   245
        (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
wenzelm@41444
   246
          if fastype_of qt_fun = fastype_of f
wenzelm@41444
   247
          then no_tac
wenzelm@41444
   248
          else
wenzelm@41444
   249
            let
wenzelm@41444
   250
              val ty_x = fastype_of x
wenzelm@41444
   251
              val ty_b = fastype_of qt_arg
wenzelm@41444
   252
              val ty_f = range_type (fastype_of f)
wenzelm@42361
   253
              val thy = Proof_Context.theory_of context
wenzelm@59582
   254
              val ty_inst = map (SOME o Thm.ctyp_of thy) [ty_x, ty_b, ty_f]
wenzelm@59582
   255
              val t_inst = map (SOME o Thm.cterm_of thy) [R2, f, g, x, y];
wenzelm@41444
   256
              val inst_thm = Drule.instantiate' ty_inst
kuncar@47308
   257
                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
wenzelm@41444
   258
            in
wenzelm@41444
   259
              (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
wenzelm@41444
   260
            end
wenzelm@41444
   261
      | _ => no_tac
wenzelm@41444
   262
    end)
kaliszyk@35222
   263
kaliszyk@35222
   264
(* Instantiates and applies 'equals_rsp'. Since the theorem is
kaliszyk@35222
   265
   complex we rely on instantiation to tell us if it applies
kaliszyk@35222
   266
*)
kaliszyk@35222
   267
fun equals_rsp_tac R ctxt =
wenzelm@41444
   268
  let
wenzelm@42361
   269
    val thy = Proof_Context.theory_of ctxt
wenzelm@41444
   270
  in
wenzelm@59582
   271
    case try (Thm.cterm_of thy) R of (* There can be loose bounds in R *)
wenzelm@41444
   272
      SOME ctm =>
wenzelm@41444
   273
        let
wenzelm@41444
   274
          val ty = domain_type (fastype_of R)
wenzelm@41444
   275
        in
wenzelm@59582
   276
          case try (Drule.instantiate' [SOME (Thm.ctyp_of thy ty)]
wenzelm@59582
   277
              [SOME (Thm.cterm_of thy R)]) @{thm equals_rsp} of
wenzelm@41444
   278
            SOME thm => rtac thm THEN' quotient_tac ctxt
wenzelm@41444
   279
          | NONE => K no_tac
wenzelm@41444
   280
        end
wenzelm@41444
   281
    | _ => K no_tac
wenzelm@41444
   282
  end
kaliszyk@35222
   283
kaliszyk@35222
   284
fun rep_abs_rsp_tac ctxt =
kaliszyk@35222
   285
  SUBGOAL (fn (goal, i) =>
wenzelm@41444
   286
    (case try bare_concl goal of
kaliszyk@43934
   287
      SOME (rel $ _ $ (rep $ (abs $ _))) =>
kaliszyk@43934
   288
        (let
wenzelm@42361
   289
          val thy = Proof_Context.theory_of ctxt;
wenzelm@40840
   290
          val (ty_a, ty_b) = dest_funT (fastype_of abs);
wenzelm@59582
   291
          val ty_inst = map (SOME o Thm.ctyp_of thy) [ty_a, ty_b];
kaliszyk@35222
   292
        in
wenzelm@59582
   293
          case try (map (SOME o Thm.cterm_of thy)) [rel, abs, rep] of
kaliszyk@35222
   294
            SOME t_inst =>
kaliszyk@35222
   295
              (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
kaliszyk@35222
   296
                SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
kaliszyk@35222
   297
              | NONE => no_tac)
kaliszyk@35222
   298
          | NONE => no_tac
kaliszyk@35222
   299
        end
kaliszyk@43934
   300
        handle TERM _ => no_tac)
wenzelm@41444
   301
    | _ => no_tac))
kaliszyk@35222
   302
kaliszyk@35222
   303
urbanc@38718
   304
(* Injection means to prove that the regularized theorem implies
kaliszyk@35222
   305
   the abs/rep injected one.
kaliszyk@35222
   306
kaliszyk@35222
   307
   The deterministic part:
kaliszyk@35222
   308
    - remove lambdas from both sides
kaliszyk@35222
   309
    - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
blanchet@55945
   310
    - prove Ball/Bex relations using rel_funI
kaliszyk@35222
   311
    - reflexivity of equality
kaliszyk@35222
   312
    - prove equality of relations using equals_rsp
kaliszyk@35222
   313
    - use user-supplied RSP theorems
kaliszyk@35222
   314
    - solve 'relation of relations' goals using quot_rel_rsp
kaliszyk@35222
   315
    - remove rep_abs from the right side
kaliszyk@35222
   316
      (Lambdas under respects may have left us some assumptions)
kaliszyk@35222
   317
kaliszyk@35222
   318
   Then in order:
kaliszyk@35222
   319
    - split applications of lifted type (apply_rsp)
kaliszyk@35222
   320
    - split applications of non-lifted type (cong_tac)
kaliszyk@35222
   321
    - apply extentionality
kaliszyk@35222
   322
    - assumption
kaliszyk@35222
   323
    - reflexivity of the relation
kaliszyk@35222
   324
*)
kaliszyk@35222
   325
fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
wenzelm@41444
   326
  (case bare_concl goal of
wenzelm@41444
   327
      (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
blanchet@55945
   328
    (Const (@{const_name rel_fun}, _) $ _ $ _) $ (Abs _) $ (Abs _)
blanchet@55945
   329
        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
kaliszyk@35222
   330
wenzelm@41444
   331
      (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
wenzelm@41444
   332
  | (Const (@{const_name HOL.eq},_) $
wenzelm@41444
   333
      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41444
   334
      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
wenzelm@41444
   335
        => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
kaliszyk@35222
   336
wenzelm@41444
   337
      (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
blanchet@55945
   338
  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
wenzelm@41444
   339
      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41444
   340
      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
blanchet@55945
   341
        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
kaliszyk@35222
   342
wenzelm@41444
   343
      (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
wenzelm@41444
   344
  | Const (@{const_name HOL.eq},_) $
wenzelm@41444
   345
      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41444
   346
      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
wenzelm@41444
   347
        => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
kaliszyk@35222
   348
wenzelm@41444
   349
      (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
blanchet@55945
   350
  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
wenzelm@41444
   351
      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41444
   352
      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
blanchet@55945
   353
        => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
kaliszyk@35222
   354
blanchet@55945
   355
  | (Const (@{const_name rel_fun}, _) $ _ $ _) $
wenzelm@41444
   356
      (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
wenzelm@41444
   357
        => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
kaliszyk@35222
   358
wenzelm@41444
   359
  | (_ $
wenzelm@41444
   360
      (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41444
   361
      (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
wenzelm@46468
   362
        => rtac @{thm babs_rsp} THEN' quotient_tac ctxt
kaliszyk@35222
   363
wenzelm@41444
   364
  | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
wenzelm@41444
   365
     (rtac @{thm refl} ORELSE'
wenzelm@41444
   366
      (equals_rsp_tac R ctxt THEN' RANGE [
wenzelm@41444
   367
         quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
kaliszyk@35222
   368
wenzelm@41444
   369
      (* reflexivity of operators arising from Cong_tac *)
wenzelm@41444
   370
  | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
kaliszyk@35222
   371
wenzelm@41444
   372
     (* respectfulness of constants; in particular of a simple relation *)
blanchet@55945
   373
  | _ $ (Const _) $ (Const _)  (* rel_fun, list_rel, etc but not equality *)
wenzelm@59498
   374
      => resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems quot_respect}))
wenzelm@57960
   375
          THEN_ALL_NEW quotient_tac ctxt
kaliszyk@35222
   376
wenzelm@41444
   377
      (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
wenzelm@41444
   378
      (* observe map_fun *)
wenzelm@41444
   379
  | _ $ _ $ _
wenzelm@41444
   380
      => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
wenzelm@41444
   381
         ORELSE' rep_abs_rsp_tac ctxt
kaliszyk@35222
   382
wenzelm@41444
   383
  | _ => K no_tac) i)
kaliszyk@35222
   384
kaliszyk@35222
   385
fun injection_step_tac ctxt rel_refl =
wenzelm@41444
   386
  FIRST' [
kaliszyk@35222
   387
    injection_match_tac ctxt,
kaliszyk@35222
   388
kaliszyk@35222
   389
    (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
kaliszyk@35222
   390
    apply_rsp_tac ctxt THEN'
kaliszyk@35222
   391
                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
kaliszyk@35222
   392
kaliszyk@35222
   393
    (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
kaliszyk@35222
   394
    (* merge with previous tactic *)
wenzelm@58956
   395
    Cong_Tac.cong_tac ctxt @{thm cong} THEN'
kaliszyk@35222
   396
                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
kaliszyk@35222
   397
kaliszyk@44285
   398
    (* resolving with R x y assumptions *)
wenzelm@58963
   399
    assume_tac ctxt,
kaliszyk@44285
   400
kaliszyk@35222
   401
    (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
kaliszyk@35222
   402
    rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
kaliszyk@35222
   403
kaliszyk@35222
   404
    (* reflexivity of the basic relations *)
kaliszyk@35222
   405
    (* R ... ... *)
wenzelm@59498
   406
    resolve_tac ctxt rel_refl]
kaliszyk@35222
   407
kaliszyk@35222
   408
fun injection_tac ctxt =
wenzelm@41444
   409
  let
wenzelm@41444
   410
    val rel_refl = reflp_get ctxt
wenzelm@41444
   411
  in
wenzelm@41444
   412
    injection_step_tac ctxt rel_refl
wenzelm@41444
   413
  end
kaliszyk@35222
   414
kaliszyk@35222
   415
fun all_injection_tac ctxt =
kaliszyk@35222
   416
  REPEAT_ALL_NEW (injection_tac ctxt)
kaliszyk@35222
   417
kaliszyk@35222
   418
kaliszyk@35222
   419
kaliszyk@35222
   420
(*** Cleaning of the Theorem ***)
kaliszyk@35222
   421
haftmann@40602
   422
(* expands all map_funs, except in front of the (bound) variables listed in xs *)
haftmann@40602
   423
fun map_fun_simple_conv xs ctrm =
wenzelm@59582
   424
  (case Thm.term_of ctrm of
haftmann@40602
   425
    ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
kaliszyk@35222
   426
        if member (op=) xs h
kaliszyk@35222
   427
        then Conv.all_conv ctrm
haftmann@40602
   428
        else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
wenzelm@41444
   429
  | _ => Conv.all_conv ctrm)
kaliszyk@35222
   430
haftmann@40602
   431
fun map_fun_conv xs ctxt ctrm =
wenzelm@59582
   432
  (case Thm.term_of ctrm of
wenzelm@41444
   433
    _ $ _ =>
wenzelm@41444
   434
      (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
wenzelm@41444
   435
        map_fun_simple_conv xs) ctrm
wenzelm@59582
   436
  | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv (Thm.term_of x :: xs) ctxt) ctxt ctrm
wenzelm@41444
   437
  | _ => Conv.all_conv ctrm)
kaliszyk@35222
   438
haftmann@40602
   439
fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
kaliszyk@35222
   440
kaliszyk@35222
   441
(* custom matching functions *)
kaliszyk@35222
   442
fun mk_abs u i t =
wenzelm@41444
   443
  if incr_boundvars i u aconv t then Bound i
wenzelm@41444
   444
  else
wenzelm@41444
   445
    case t of
wenzelm@41444
   446
      t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
wenzelm@41444
   447
    | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
wenzelm@41444
   448
    | Bound j => if i = j then error "make_inst" else t
wenzelm@41444
   449
    | _ => t
kaliszyk@35222
   450
kaliszyk@35222
   451
fun make_inst lhs t =
wenzelm@41444
   452
  let
wenzelm@41444
   453
    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
wenzelm@41444
   454
    val _ $ (Abs (_, _, (_ $ g))) = t;
wenzelm@41444
   455
  in
wenzelm@41444
   456
    (f, Abs ("x", T, mk_abs u 0 g))
wenzelm@41444
   457
  end
kaliszyk@35222
   458
kaliszyk@35222
   459
fun make_inst_id lhs t =
wenzelm@41444
   460
  let
wenzelm@41444
   461
    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
wenzelm@41444
   462
    val _ $ (Abs (_, _, g)) = t;
wenzelm@41444
   463
  in
wenzelm@41444
   464
    (f, Abs ("x", T, mk_abs u 0 g))
wenzelm@41444
   465
  end
kaliszyk@35222
   466
kaliszyk@35222
   467
(* Simplifies a redex using the 'lambda_prs' theorem.
kaliszyk@35222
   468
   First instantiates the types and known subterms.
kaliszyk@35222
   469
   Then solves the quotient assumptions to get Rep2 and Abs1
kaliszyk@35222
   470
   Finally instantiates the function f using make_inst
kaliszyk@35222
   471
   If Rep2 is an identity then the pattern is simpler and
kaliszyk@35222
   472
   make_inst_id is used
kaliszyk@35222
   473
*)
kaliszyk@35222
   474
fun lambda_prs_simple_conv ctxt ctrm =
wenzelm@59582
   475
  (case Thm.term_of ctrm of
haftmann@40602
   476
    (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
kaliszyk@35222
   477
      let
wenzelm@42361
   478
        val thy = Proof_Context.theory_of ctxt
wenzelm@40840
   479
        val (ty_b, ty_a) = dest_funT (fastype_of r1)
wenzelm@40840
   480
        val (ty_c, ty_d) = dest_funT (fastype_of a2)
wenzelm@59582
   481
        val tyinst = map (SOME o Thm.ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
wenzelm@59582
   482
        val tinst = [NONE, NONE, SOME (Thm.cterm_of thy r1), NONE, SOME (Thm.cterm_of thy a2)]
kaliszyk@35222
   483
        val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
kaliszyk@35222
   484
        val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
wenzelm@54742
   485
        val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
kaliszyk@35222
   486
        val (insp, inst) =
kaliszyk@35222
   487
          if ty_c = ty_d
wenzelm@59582
   488
          then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
wenzelm@59582
   489
          else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
wenzelm@59582
   490
        val thm4 =
wenzelm@59582
   491
          Drule.instantiate_normalize ([], [(Thm.cterm_of thy insp, Thm.cterm_of thy inst)]) thm3
kaliszyk@35222
   492
      in
kaliszyk@35222
   493
        Conv.rewr_conv thm4 ctrm
kaliszyk@35222
   494
      end
wenzelm@41444
   495
  | _ => Conv.all_conv ctrm)
kaliszyk@35222
   496
wenzelm@36936
   497
fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
kaliszyk@35222
   498
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
kaliszyk@35222
   499
kaliszyk@35222
   500
kaliszyk@35222
   501
(* Cleaning consists of:
kaliszyk@35222
   502
kaliszyk@35222
   503
  1. unfolding of ---> in front of everything, except
kaliszyk@35222
   504
     bound variables (this prevents lambda_prs from
kaliszyk@35222
   505
     becoming stuck)
kaliszyk@35222
   506
kaliszyk@35222
   507
  2. simplification with lambda_prs
kaliszyk@35222
   508
kaliszyk@35222
   509
  3. simplification with:
kaliszyk@35222
   510
kaliszyk@35222
   511
      - Quotient_abs_rep Quotient_rel_rep
kaliszyk@35222
   512
        babs_prs all_prs ex_prs ex1_prs
kaliszyk@35222
   513
kaliszyk@35222
   514
      - id_simps and preservation lemmas and
kaliszyk@35222
   515
kaliszyk@35222
   516
      - symmetric versions of the definitions
kaliszyk@35222
   517
        (that is definitions of quotient constants
kaliszyk@35222
   518
         are folded)
kaliszyk@35222
   519
kaliszyk@35222
   520
  4. test for refl
kaliszyk@35222
   521
*)
wenzelm@57960
   522
fun clean_tac ctxt =
wenzelm@41444
   523
  let
wenzelm@57960
   524
    val thy =  Proof_Context.theory_of ctxt
urbanc@45350
   525
    val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy)
wenzelm@57960
   526
    val prs = rev (Named_Theorems.get ctxt @{named_theorems quot_preserve})
wenzelm@57960
   527
    val ids = rev (Named_Theorems.get ctxt @{named_theorems id_simps})
wenzelm@41444
   528
    val thms =
kuncar@47308
   529
      @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
kaliszyk@35222
   530
wenzelm@57960
   531
    val simpset = (mk_minimal_simpset ctxt) addsimps thms addSolver quotient_solver
wenzelm@41444
   532
  in
wenzelm@41451
   533
    EVERY' [
wenzelm@57960
   534
      map_fun_tac ctxt,
wenzelm@57960
   535
      lambda_prs_tac ctxt,
wenzelm@51717
   536
      simp_tac simpset,
wenzelm@41451
   537
      TRY o rtac refl]
wenzelm@41444
   538
  end
kaliszyk@35222
   539
kaliszyk@35222
   540
urbanc@38718
   541
(* Tactic for Generalising Free Variables in a Goal *)
kaliszyk@35222
   542
kaliszyk@35222
   543
fun inst_spec ctrm =
wenzelm@59582
   544
  Drule.instantiate' [SOME (Thm.ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
kaliszyk@35222
   545
kaliszyk@35222
   546
fun inst_spec_tac ctrms =
kaliszyk@35222
   547
  EVERY' (map (dtac o inst_spec) ctrms)
kaliszyk@35222
   548
kaliszyk@35222
   549
fun all_list xs trm =
kaliszyk@35222
   550
  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
kaliszyk@35222
   551
kaliszyk@35222
   552
fun apply_under_Trueprop f =
kaliszyk@35222
   553
  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
kaliszyk@35222
   554
kaliszyk@35222
   555
fun gen_frees_tac ctxt =
kaliszyk@35222
   556
  SUBGOAL (fn (concl, i) =>
kaliszyk@35222
   557
    let
wenzelm@42361
   558
      val thy = Proof_Context.theory_of ctxt
kaliszyk@35222
   559
      val vrs = Term.add_frees concl []
wenzelm@59582
   560
      val cvrs = map (Thm.cterm_of thy o Free) vrs
kaliszyk@35222
   561
      val concl' = apply_under_Trueprop (all_list vrs) concl
kaliszyk@35222
   562
      val goal = Logic.mk_implies (concl', concl)
kaliszyk@35222
   563
      val rule = Goal.prove ctxt [] [] goal
wenzelm@58963
   564
        (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt]))
kaliszyk@35222
   565
    in
kaliszyk@35222
   566
      rtac rule i
kaliszyk@35222
   567
    end)
kaliszyk@35222
   568
kaliszyk@35222
   569
kaliszyk@35222
   570
(** The General Shape of the Lifting Procedure **)
kaliszyk@35222
   571
kaliszyk@35222
   572
(* - A is the original raw theorem
kaliszyk@35222
   573
   - B is the regularized theorem
kaliszyk@35222
   574
   - C is the rep/abs injected version of B
kaliszyk@35222
   575
   - D is the lifted theorem
kaliszyk@35222
   576
kaliszyk@35222
   577
   - 1st prem is the regularization step
kaliszyk@35222
   578
   - 2nd prem is the rep/abs injection step
kaliszyk@35222
   579
   - 3rd prem is the cleaning part
kaliszyk@35222
   580
kaliszyk@35222
   581
   the Quot_True premise in 2nd records the lifted theorem
kaliszyk@35222
   582
*)
urbanc@45782
   583
val procedure_thm =
kaliszyk@35222
   584
  @{lemma  "[|A;
kaliszyk@35222
   585
              A --> B;
kaliszyk@35222
   586
              Quot_True D ==> B = C;
kaliszyk@35222
   587
              C = D|] ==> D"
kaliszyk@35222
   588
      by (simp add: Quot_True_def)}
kaliszyk@35222
   589
urbanc@45782
   590
(* in case of partial equivalence relations, this form of the 
urbanc@45782
   591
   procedure theorem results in solvable proof obligations 
urbanc@45782
   592
*)
urbanc@45782
   593
val partiality_procedure_thm =
urbanc@45782
   594
  @{lemma  "[|B; 
urbanc@45782
   595
              Quot_True D ==> B = C;
urbanc@45782
   596
              C = D|] ==> D"
urbanc@45782
   597
      by (simp add: Quot_True_def)}
urbanc@45782
   598
kaliszyk@35222
   599
fun lift_match_error ctxt msg rtrm qtrm =
wenzelm@41444
   600
  let
wenzelm@41444
   601
    val rtrm_str = Syntax.string_of_term ctxt rtrm
wenzelm@41444
   602
    val qtrm_str = Syntax.string_of_term ctxt qtrm
wenzelm@41444
   603
    val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
wenzelm@41444
   604
      "", "does not match with original theorem", rtrm_str]
wenzelm@41444
   605
  in
wenzelm@41444
   606
    error msg
wenzelm@41444
   607
  end
kaliszyk@35222
   608
kaliszyk@35222
   609
fun procedure_inst ctxt rtrm qtrm =
wenzelm@41444
   610
  let
wenzelm@42361
   611
    val thy = Proof_Context.theory_of ctxt
wenzelm@41444
   612
    val rtrm' = HOLogic.dest_Trueprop rtrm
wenzelm@41444
   613
    val qtrm' = HOLogic.dest_Trueprop qtrm
wenzelm@41451
   614
    val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
wenzelm@41451
   615
      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
wenzelm@41451
   616
    val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
wenzelm@41451
   617
      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
wenzelm@41444
   618
  in
wenzelm@41444
   619
    Drule.instantiate' []
wenzelm@59582
   620
      [SOME (Thm.cterm_of thy rtrm'),
wenzelm@59582
   621
       SOME (Thm.cterm_of thy reg_goal),
wenzelm@41444
   622
       NONE,
wenzelm@59582
   623
       SOME (Thm.cterm_of thy inj_goal)] procedure_thm
wenzelm@41444
   624
  end
kaliszyk@35222
   625
urbanc@37593
   626
urbanc@38860
   627
(* Since we use Ball and Bex during the lifting and descending,
kaliszyk@38862
   628
   we cannot deal with lemmas containing them, unless we unfold
kaliszyk@38862
   629
   them by default. *)
urbanc@38860
   630
kaliszyk@38862
   631
val default_unfolds = @{thms Ball_def Bex_def}
urbanc@38860
   632
urbanc@38860
   633
urbanc@37593
   634
(** descending as tactic **)
urbanc@37593
   635
urbanc@38859
   636
fun descend_procedure_tac ctxt simps =
wenzelm@41444
   637
  let
wenzelm@51717
   638
    val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
wenzelm@41444
   639
  in
wenzelm@51717
   640
    full_simp_tac simpset
wenzelm@54742
   641
    THEN' Object_Logic.full_atomize_tac ctxt
wenzelm@41444
   642
    THEN' gen_frees_tac ctxt
wenzelm@41444
   643
    THEN' SUBGOAL (fn (goal, i) =>
wenzelm@41444
   644
      let
wenzelm@45279
   645
        val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
wenzelm@41451
   646
        val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
wenzelm@41444
   647
        val rule = procedure_inst ctxt rtrm  goal
wenzelm@41444
   648
      in
wenzelm@41444
   649
        rtac rule i
wenzelm@41444
   650
      end)
wenzelm@41444
   651
  end
urbanc@37593
   652
urbanc@38859
   653
fun descend_tac ctxt simps =
wenzelm@41444
   654
  let
wenzelm@41444
   655
    val mk_tac_raw =
wenzelm@41444
   656
      descend_procedure_tac ctxt simps
wenzelm@41444
   657
      THEN' RANGE
wenzelm@54742
   658
        [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
wenzelm@41444
   659
         regularize_tac ctxt,
wenzelm@41444
   660
         all_injection_tac ctxt,
wenzelm@41444
   661
         clean_tac ctxt]
wenzelm@41444
   662
  in
wenzelm@41444
   663
    Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
wenzelm@41444
   664
  end
kaliszyk@35222
   665
kaliszyk@35222
   666
urbanc@45782
   667
(** descending for partial equivalence relations **)
urbanc@45782
   668
urbanc@45782
   669
fun partiality_procedure_inst ctxt rtrm qtrm =
urbanc@45782
   670
  let
urbanc@45782
   671
    val thy = Proof_Context.theory_of ctxt
urbanc@45782
   672
    val rtrm' = HOLogic.dest_Trueprop rtrm
urbanc@45782
   673
    val qtrm' = HOLogic.dest_Trueprop qtrm
urbanc@45782
   674
    val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
urbanc@45782
   675
      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
urbanc@45782
   676
    val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
urbanc@45782
   677
      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
urbanc@45782
   678
  in
urbanc@45782
   679
    Drule.instantiate' []
wenzelm@59582
   680
      [SOME (Thm.cterm_of thy reg_goal),
urbanc@45782
   681
       NONE,
wenzelm@59582
   682
       SOME (Thm.cterm_of thy inj_goal)] partiality_procedure_thm
urbanc@45782
   683
  end
urbanc@45782
   684
urbanc@45782
   685
urbanc@45782
   686
fun partiality_descend_procedure_tac ctxt simps =
urbanc@45782
   687
  let
wenzelm@51717
   688
    val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
urbanc@45782
   689
  in
wenzelm@51717
   690
    full_simp_tac simpset
wenzelm@54742
   691
    THEN' Object_Logic.full_atomize_tac ctxt
urbanc@45782
   692
    THEN' gen_frees_tac ctxt
urbanc@45782
   693
    THEN' SUBGOAL (fn (goal, i) =>
urbanc@45782
   694
      let
urbanc@45782
   695
        val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
urbanc@45782
   696
        val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
urbanc@45782
   697
        val rule = partiality_procedure_inst ctxt rtrm  goal
urbanc@45782
   698
      in
urbanc@45782
   699
        rtac rule i
urbanc@45782
   700
      end)
urbanc@45782
   701
  end
urbanc@45782
   702
urbanc@45782
   703
fun partiality_descend_tac ctxt simps =
urbanc@45782
   704
  let
urbanc@45782
   705
    val mk_tac_raw =
urbanc@45782
   706
      partiality_descend_procedure_tac ctxt simps
urbanc@45782
   707
      THEN' RANGE
wenzelm@54742
   708
        [Object_Logic.rulify_tac ctxt THEN' (K all_tac),
urbanc@45782
   709
         all_injection_tac ctxt,
urbanc@45782
   710
         clean_tac ctxt]
urbanc@45782
   711
  in
urbanc@45782
   712
    Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
urbanc@45782
   713
  end
urbanc@45782
   714
urbanc@45782
   715
urbanc@45782
   716
urbanc@38625
   717
(** lifting as a tactic **)
urbanc@37593
   718
urbanc@38718
   719
urbanc@37593
   720
(* the tactic leaves three subgoals to be proved *)
urbanc@38859
   721
fun lift_procedure_tac ctxt simps rthm =
wenzelm@41444
   722
  let
wenzelm@51717
   723
    val simpset = (mk_minimal_simpset ctxt) addsimps (simps @ default_unfolds)
wenzelm@41444
   724
  in
wenzelm@51717
   725
    full_simp_tac simpset
wenzelm@54742
   726
    THEN' Object_Logic.full_atomize_tac ctxt
wenzelm@41444
   727
    THEN' gen_frees_tac ctxt
wenzelm@41444
   728
    THEN' SUBGOAL (fn (goal, i) =>
wenzelm@41444
   729
      let
wenzelm@41444
   730
        (* full_atomize_tac contracts eta redexes,
wenzelm@41444
   731
           so we do it also in the original theorem *)
wenzelm@41444
   732
        val rthm' =
wenzelm@51717
   733
          rthm |> full_simplify simpset
wenzelm@41444
   734
               |> Drule.eta_contraction_rule
wenzelm@41444
   735
               |> Thm.forall_intr_frees
wenzelm@54742
   736
               |> atomize_thm ctxt
urbanc@38717
   737
wenzelm@59582
   738
        val rule = procedure_inst ctxt (Thm.prop_of rthm') goal
wenzelm@41444
   739
      in
wenzelm@41444
   740
        (rtac rule THEN' rtac rthm') i
wenzelm@41444
   741
      end)
wenzelm@41444
   742
  end
urbanc@38625
   743
wenzelm@41444
   744
fun lift_single_tac ctxt simps rthm =
urbanc@38859
   745
  lift_procedure_tac ctxt simps rthm
urbanc@38625
   746
  THEN' RANGE
urbanc@38625
   747
    [ regularize_tac ctxt,
urbanc@38625
   748
      all_injection_tac ctxt,
urbanc@38625
   749
      clean_tac ctxt ]
urbanc@38625
   750
urbanc@38859
   751
fun lift_tac ctxt simps rthms =
wenzelm@41444
   752
  Goal.conjunction_tac
urbanc@38859
   753
  THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
urbanc@38625
   754
urbanc@38625
   755
urbanc@38625
   756
(* automated lifting with pre-simplification of the theorems;
urbanc@38625
   757
   for internal usage *)
urbanc@38625
   758
fun lifted ctxt qtys simps rthm =
wenzelm@41444
   759
  let
wenzelm@41444
   760
    val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
wenzelm@59582
   761
    val goal = Quotient_Term.derive_qtrm ctxt' qtys (Thm.prop_of rthm')
wenzelm@41444
   762
  in
wenzelm@41444
   763
    Goal.prove ctxt' [] [] goal
wenzelm@41444
   764
      (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
wenzelm@42361
   765
    |> singleton (Proof_Context.export ctxt' ctxt)
wenzelm@41444
   766
  end
kaliszyk@35222
   767
urbanc@37593
   768
urbanc@38625
   769
(* lifting as an attribute *)
kaliszyk@35222
   770
wenzelm@41444
   771
val lifted_attrib = Thm.rule_attribute (fn context =>
urbanc@37593
   772
  let
urbanc@37593
   773
    val ctxt = Context.proof_of context
wenzelm@45279
   774
    val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
urbanc@37593
   775
  in
urbanc@38625
   776
    lifted ctxt qtys []
urbanc@37593
   777
  end)
kaliszyk@35222
   778
kaliszyk@35222
   779
end; (* structure *)