src/HOL/Tools/Quotient/quotient_term.ML
author kuncar
Mon Apr 23 17:18:18 2012 +0200 (2012-04-23)
changeset 47698 18202d3d5832
parent 47504 aa1b8a59017f
child 55414 eab03e9cee8a
permissions -rw-r--r--
move MRSL to a separate file
haftmann@37744
     1
(*  Title:      HOL/Tools/Quotient/quotient_term.ML
kaliszyk@35222
     2
    Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@35222
     3
wenzelm@35788
     4
Constructs terms corresponding to goals from lifting theorems to
wenzelm@35788
     5
quotient types.
kaliszyk@35222
     6
*)
kaliszyk@35222
     7
kaliszyk@35222
     8
signature QUOTIENT_TERM =
kaliszyk@35222
     9
sig
kaliszyk@35222
    10
  exception LIFT_MATCH of string
kaliszyk@35222
    11
kaliszyk@35222
    12
  datatype flag = AbsF | RepF
kaliszyk@35222
    13
kuncar@45797
    14
  val absrep_fun: Proof.context -> flag -> typ * typ -> term
kuncar@45797
    15
  val absrep_fun_chk: Proof.context -> flag -> typ * typ -> term
kaliszyk@35222
    16
kaliszyk@35222
    17
  (* Allows Nitpick to represent quotient types as single elements from raw type *)
kuncar@45797
    18
  val absrep_const_chk: Proof.context -> flag -> string -> term
kaliszyk@35222
    19
kaliszyk@35222
    20
  val equiv_relation: Proof.context -> typ * typ -> term
kaliszyk@35222
    21
  val equiv_relation_chk: Proof.context -> typ * typ -> term
kaliszyk@35222
    22
kuncar@47096
    23
  val get_rel_from_quot_thm: thm -> term
kuncar@47504
    24
  val prove_quot_thm: Proof.context -> typ * typ -> thm
kuncar@47096
    25
kaliszyk@35222
    26
  val regularize_trm: Proof.context -> term * term -> term
kaliszyk@35222
    27
  val regularize_trm_chk: Proof.context -> term * term -> term
kaliszyk@35222
    28
kaliszyk@35222
    29
  val inj_repabs_trm: Proof.context -> term * term -> term
kaliszyk@35222
    30
  val inj_repabs_trm_chk: Proof.context -> term * term -> term
kaliszyk@35222
    31
urbanc@38624
    32
  val derive_qtyp: Proof.context -> typ list -> typ -> typ
urbanc@38624
    33
  val derive_qtrm: Proof.context -> typ list -> term -> term
urbanc@38624
    34
  val derive_rtyp: Proof.context -> typ list -> typ -> typ
urbanc@38624
    35
  val derive_rtrm: Proof.context -> typ list -> term -> term
kaliszyk@35222
    36
end;
kaliszyk@35222
    37
kaliszyk@35222
    38
structure Quotient_Term: QUOTIENT_TERM =
kaliszyk@35222
    39
struct
kaliszyk@35222
    40
kaliszyk@35222
    41
exception LIFT_MATCH of string
kaliszyk@35222
    42
kaliszyk@35222
    43
kaliszyk@35222
    44
kaliszyk@35222
    45
(*** Aggregate Rep/Abs Function ***)
kaliszyk@35222
    46
kaliszyk@35222
    47
kaliszyk@35222
    48
(* The flag RepF is for types in negative position; AbsF is for types
kaliszyk@35222
    49
   in positive position. Because of this, function types need to be
kaliszyk@35222
    50
   treated specially, since there the polarity changes.
kaliszyk@35222
    51
*)
kaliszyk@35222
    52
kaliszyk@35222
    53
datatype flag = AbsF | RepF
kaliszyk@35222
    54
kaliszyk@35222
    55
fun negF AbsF = RepF
kaliszyk@35222
    56
  | negF RepF = AbsF
kaliszyk@35222
    57
haftmann@37677
    58
fun is_identity (Const (@{const_name id}, _)) = true
kaliszyk@35222
    59
  | is_identity _ = false
kaliszyk@35222
    60
haftmann@37677
    61
fun mk_identity ty = Const (@{const_name id}, ty --> ty)
kaliszyk@35222
    62
kaliszyk@35222
    63
fun mk_fun_compose flag (trm1, trm2) =
kaliszyk@35222
    64
  case flag of
haftmann@37677
    65
    AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
haftmann@37677
    66
  | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
kaliszyk@35222
    67
kuncar@45796
    68
fun get_mapfun_data ctxt s =
kuncar@45796
    69
  (case Symtab.lookup (Enriched_Type.entries ctxt) s of
kuncar@45795
    70
    SOME [map_data] => (case try dest_Const (#mapper map_data) of
kuncar@45795
    71
      SOME (c, _) => (Const (c, dummyT), #variances map_data)
kuncar@45795
    72
    | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant."))
kuncar@45795
    73
  | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.")
kuncar@45795
    74
  | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) 
kaliszyk@35222
    75
kuncar@45796
    76
fun defined_mapfun_data ctxt s =
kuncar@45796
    77
  Symtab.defined (Enriched_Type.entries ctxt) s
kaliszyk@35222
    78
kaliszyk@35222
    79
(* looks up the (varified) rty and qty for
kaliszyk@35222
    80
   a quotient definition
kaliszyk@35222
    81
*)
kuncar@45796
    82
fun get_rty_qty ctxt s =
kuncar@45796
    83
  let
kuncar@45796
    84
    val thy = Proof_Context.theory_of ctxt
kuncar@45796
    85
  in
kuncar@45796
    86
    (case Quotient_Info.lookup_quotients_global thy s of
kuncar@45796
    87
      SOME qdata => (#rtyp qdata, #qtyp qdata)
kuncar@45796
    88
    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
kuncar@45796
    89
  end
kaliszyk@35222
    90
kaliszyk@35222
    91
(* matches a type pattern with a type *)
kaliszyk@35222
    92
fun match ctxt err ty_pat ty =
wenzelm@41444
    93
  let
wenzelm@42361
    94
    val thy = Proof_Context.theory_of ctxt
wenzelm@41444
    95
  in
wenzelm@41444
    96
    Sign.typ_match thy (ty_pat, ty) Vartab.empty
wenzelm@41444
    97
      handle Type.TYPE_MATCH => err ctxt ty_pat ty
wenzelm@41444
    98
  end
kaliszyk@35222
    99
kaliszyk@35222
   100
(* produces the rep or abs constant for a qty *)
kuncar@45797
   101
fun absrep_const ctxt flag qty_str =
wenzelm@41444
   102
  let
bulwahn@45534
   103
    (* FIXME *)
bulwahn@45534
   104
    fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
urbanc@45628
   105
      | mk_dummyT (Free (c, _)) = Free (c, dummyT)
urbanc@45628
   106
      | mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable"     
wenzelm@41444
   107
  in
bulwahn@45534
   108
    case Quotient_Info.lookup_abs_rep ctxt qty_str of
bulwahn@45534
   109
      SOME abs_rep => 
bulwahn@45534
   110
        mk_dummyT (case flag of
bulwahn@45534
   111
          AbsF => #abs abs_rep
bulwahn@45534
   112
        | RepF => #rep abs_rep)
bulwahn@45534
   113
      | NONE => error ("No abs/rep terms for " ^ quote qty_str)
wenzelm@41444
   114
  end
bulwahn@45534
   115
  
kaliszyk@35222
   116
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
kuncar@45797
   117
fun absrep_const_chk ctxt flag qty_str =
kuncar@45797
   118
  Syntax.check_term ctxt (absrep_const ctxt flag qty_str)
kaliszyk@35222
   119
kaliszyk@35222
   120
fun absrep_match_err ctxt ty_pat ty =
wenzelm@41444
   121
  let
wenzelm@41444
   122
    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
wenzelm@41444
   123
    val ty_str = Syntax.string_of_typ ctxt ty
wenzelm@41444
   124
  in
wenzelm@41444
   125
    raise LIFT_MATCH (space_implode " "
wenzelm@41444
   126
      ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
wenzelm@41444
   127
  end
kaliszyk@35222
   128
kaliszyk@35222
   129
kaliszyk@35222
   130
(** generation of an aggregate absrep function **)
kaliszyk@35222
   131
kaliszyk@35222
   132
(* - In case of equal types we just return the identity.
kaliszyk@35222
   133
kaliszyk@35222
   134
   - In case of TFrees we also return the identity.
kaliszyk@35222
   135
kaliszyk@35222
   136
   - In case of function types we recurse taking
kaliszyk@35222
   137
     the polarity change into account.
kaliszyk@35222
   138
kaliszyk@35222
   139
   - If the type constructors are equal, we recurse for the
kaliszyk@35222
   140
     arguments and build the appropriate map function.
kaliszyk@35222
   141
kaliszyk@35222
   142
   - If the type constructors are unequal, there must be an
kaliszyk@35222
   143
     instance of quotient types:
kaliszyk@35222
   144
kaliszyk@35222
   145
       - we first look up the corresponding rty_pat and qty_pat
kaliszyk@35222
   146
         from the quotient definition; the arguments of qty_pat
kaliszyk@35222
   147
         must be some distinct TVars
kaliszyk@35222
   148
       - we then match the rty_pat with rty and qty_pat with qty;
kaliszyk@35222
   149
         if matching fails the types do not correspond -> error
kaliszyk@35222
   150
       - the matching produces two environments; we look up the
kaliszyk@35222
   151
         assignments for the qty_pat variables and recurse on the
kaliszyk@35222
   152
         assignments
kaliszyk@35222
   153
       - we prefix the aggregate map function for the rty_pat,
kaliszyk@35222
   154
         which is an abstraction over all type variables
kaliszyk@35222
   155
       - finally we compose the result with the appropriate
kaliszyk@35222
   156
         absrep function in case at least one argument produced
kaliszyk@35222
   157
         a non-identity function /
kaliszyk@35222
   158
         otherwise we just return the appropriate absrep
kaliszyk@35222
   159
         function
kaliszyk@35222
   160
kaliszyk@35222
   161
     The composition is necessary for types like
kaliszyk@35222
   162
kaliszyk@35222
   163
        ('a list) list / ('a foo) foo
kaliszyk@35222
   164
kaliszyk@35222
   165
     The matching is necessary for types like
kaliszyk@35222
   166
kaliszyk@35222
   167
        ('a * 'a) list / 'a bar
kaliszyk@35222
   168
kaliszyk@35222
   169
     The test is necessary in order to eliminate superfluous
kaliszyk@35222
   170
     identity maps.
kaliszyk@35222
   171
*)
kaliszyk@35222
   172
kuncar@45797
   173
fun absrep_fun ctxt flag (rty, qty) =
wenzelm@45340
   174
  let
kuncar@45795
   175
    fun absrep_args tys tys' variances =
kuncar@45795
   176
      let
kuncar@45795
   177
        fun absrep_arg (types, (_, variant)) =
kuncar@45795
   178
          (case variant of
kuncar@45795
   179
            (false, false) => []
kuncar@45797
   180
          | (true, false) => [(absrep_fun ctxt flag types)]
kuncar@45797
   181
          | (false, true) => [(absrep_fun ctxt (negF flag) types)]
kuncar@45797
   182
          | (true, true) => [(absrep_fun ctxt flag types),(absrep_fun ctxt (negF flag) types)])
kuncar@45795
   183
      in
kuncar@45795
   184
        maps absrep_arg ((tys ~~ tys') ~~ variances)
kuncar@45795
   185
      end
kuncar@45795
   186
    fun test_identities tys rtys' s s' =
kuncar@45795
   187
      let
kuncar@45797
   188
        val args = map (absrep_fun ctxt flag) (tys ~~ rtys')
kuncar@45795
   189
      in
kuncar@45795
   190
        if forall is_identity args
kuncar@45795
   191
        then 
kuncar@45797
   192
          absrep_const ctxt flag s'
kuncar@45795
   193
        else 
kuncar@45795
   194
          raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
kuncar@45795
   195
      end
wenzelm@45340
   196
  in
wenzelm@45340
   197
    if rty = qty
wenzelm@45340
   198
    then mk_identity rty
wenzelm@45340
   199
    else
wenzelm@45340
   200
      case (rty, qty) of
kuncar@45795
   201
        (Type (s, tys), Type (s', tys')) =>
wenzelm@45340
   202
          if s = s'
wenzelm@45340
   203
          then
wenzelm@45340
   204
            let
kuncar@45796
   205
              val (map_fun, variances) = get_mapfun_data ctxt s
kuncar@45795
   206
              val args = absrep_args tys tys' variances
wenzelm@45340
   207
            in
kuncar@45795
   208
              list_comb (map_fun, args)
wenzelm@45340
   209
            end
wenzelm@45340
   210
          else
wenzelm@45340
   211
            let
kuncar@45796
   212
              val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
wenzelm@45340
   213
              val qtyenv = match ctxt absrep_match_err qty_pat qty
kuncar@45795
   214
              val rtys' = map (Envir.subst_type qtyenv) rtys
wenzelm@45340
   215
            in
kuncar@45796
   216
              if not (defined_mapfun_data ctxt s)
kuncar@45795
   217
              then
kuncar@45795
   218
                (*
kuncar@45795
   219
                    If we don't know a map function for the raw type,
kuncar@45795
   220
                    we are not necessarilly in troubles because
kuncar@45795
   221
                    it can still be the case we don't need the map 
kuncar@45795
   222
                    function <=> all abs/rep functions are identities.
kuncar@45795
   223
                *)
kuncar@45795
   224
                test_identities tys rtys' s s'
wenzelm@45340
   225
              else
wenzelm@45340
   226
                let
kuncar@45796
   227
                  val (map_fun, variances) = get_mapfun_data ctxt s
kuncar@45795
   228
                  val args = absrep_args tys rtys' variances
wenzelm@45340
   229
                in
kuncar@45795
   230
                  if forall is_identity args
kuncar@45797
   231
                  then absrep_const ctxt flag s'
kuncar@45795
   232
                  else
kuncar@45795
   233
                    let
kuncar@45795
   234
                      val result = list_comb (map_fun, args)
kuncar@45795
   235
                    in
kuncar@45797
   236
                      mk_fun_compose flag (absrep_const ctxt flag s', result)
kuncar@45795
   237
                    end
wenzelm@45340
   238
                end
wenzelm@45340
   239
            end
wenzelm@45340
   240
      | (TFree x, TFree x') =>
wenzelm@45340
   241
          if x = x'
wenzelm@45340
   242
          then mk_identity rty
wenzelm@45340
   243
          else raise (LIFT_MATCH "absrep_fun (frees)")
wenzelm@45340
   244
      | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
wenzelm@45340
   245
      | _ => raise (LIFT_MATCH "absrep_fun (default)")
wenzelm@45340
   246
  end
kaliszyk@35222
   247
kuncar@45797
   248
fun absrep_fun_chk ctxt flag (rty, qty) =
kuncar@45797
   249
  absrep_fun ctxt flag (rty, qty)
kaliszyk@35222
   250
  |> Syntax.check_term ctxt
kaliszyk@35222
   251
kaliszyk@35222
   252
kaliszyk@35222
   253
kaliszyk@35222
   254
(*** Aggregate Equivalence Relation ***)
kaliszyk@35222
   255
kaliszyk@35222
   256
kaliszyk@35222
   257
(* works very similar to the absrep generation,
kaliszyk@35222
   258
   except there is no need for polarities
kaliszyk@35222
   259
*)
kaliszyk@35222
   260
kaliszyk@35222
   261
(* instantiates TVars so that the term is of type ty *)
kaliszyk@35222
   262
fun force_typ ctxt trm ty =
wenzelm@41444
   263
  let
wenzelm@42361
   264
    val thy = Proof_Context.theory_of ctxt
wenzelm@41444
   265
    val trm_ty = fastype_of trm
wenzelm@41444
   266
    val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
wenzelm@41444
   267
  in
wenzelm@41444
   268
    map_types (Envir.subst_type ty_inst) trm
wenzelm@41444
   269
  end
kaliszyk@35222
   270
haftmann@38864
   271
fun is_eq (Const (@{const_name HOL.eq}, _)) = true
kaliszyk@35222
   272
  | is_eq _ = false
kaliszyk@35222
   273
kaliszyk@35222
   274
fun mk_rel_compose (trm1, trm2) =
wenzelm@35402
   275
  Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
kaliszyk@35222
   276
wenzelm@45340
   277
fun get_relmap thy s =
wenzelm@45340
   278
  (case Quotient_Info.lookup_quotmaps thy s of
bulwahn@45273
   279
    SOME map_data => Const (#relmap map_data, dummyT)
wenzelm@45279
   280
  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
kaliszyk@35222
   281
wenzelm@45340
   282
fun get_equiv_rel thy s =
wenzelm@45340
   283
  (case Quotient_Info.lookup_quotients thy s of
wenzelm@45279
   284
    SOME qdata => #equiv_rel qdata
kuncar@47095
   285
  | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
kaliszyk@35222
   286
kaliszyk@35222
   287
fun equiv_match_err ctxt ty_pat ty =
wenzelm@41444
   288
  let
wenzelm@41444
   289
    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
wenzelm@41444
   290
    val ty_str = Syntax.string_of_typ ctxt ty
wenzelm@41444
   291
  in
wenzelm@41444
   292
    raise LIFT_MATCH (space_implode " "
wenzelm@41444
   293
      ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
wenzelm@41444
   294
  end
kaliszyk@35222
   295
kaliszyk@35222
   296
(* builds the aggregate equivalence relation
kaliszyk@35222
   297
   that will be the argument of Respects
kaliszyk@35222
   298
*)
kaliszyk@35222
   299
fun equiv_relation ctxt (rty, qty) =
kuncar@45796
   300
  if rty = qty
kuncar@45796
   301
  then HOLogic.eq_const rty
kuncar@45796
   302
  else
kuncar@45796
   303
    case (rty, qty) of
kuncar@45796
   304
      (Type (s, tys), Type (s', tys')) =>
kuncar@45796
   305
        if s = s'
kuncar@45796
   306
        then
kuncar@45796
   307
          let
kuncar@45796
   308
            val args = map (equiv_relation ctxt) (tys ~~ tys')
kuncar@45796
   309
          in
kuncar@45796
   310
            list_comb (get_relmap ctxt s, args)
kuncar@45796
   311
          end
kuncar@45796
   312
        else
kuncar@45796
   313
          let
kuncar@47095
   314
            val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
kuncar@45796
   315
            val qtyenv = match ctxt equiv_match_err qty_pat qty
kuncar@47095
   316
            val rtys' = map (Envir.subst_type qtyenv) rtys
kuncar@47095
   317
            val args = map (equiv_relation ctxt) (tys ~~ rtys')
kuncar@45796
   318
            val eqv_rel = get_equiv_rel ctxt s'
kuncar@45796
   319
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
kuncar@45796
   320
          in
kuncar@45796
   321
            if forall is_eq args
kuncar@45796
   322
            then eqv_rel'
kuncar@45796
   323
            else
kuncar@45796
   324
              let
kuncar@47095
   325
                val result = list_comb (get_relmap ctxt s, args)
kuncar@45796
   326
              in
kuncar@45796
   327
                mk_rel_compose (result, eqv_rel')
kuncar@45796
   328
              end
kuncar@45796
   329
          end
kuncar@45796
   330
    | _ => HOLogic.eq_const rty
kuncar@45796
   331
kaliszyk@35222
   332
kaliszyk@35222
   333
fun equiv_relation_chk ctxt (rty, qty) =
kaliszyk@35222
   334
  equiv_relation ctxt (rty, qty)
kaliszyk@35222
   335
  |> Syntax.check_term ctxt
kaliszyk@35222
   336
kuncar@47096
   337
(* generation of the Quotient theorem  *)
kuncar@47096
   338
kuncar@47106
   339
exception CODE_GEN of string
kuncar@47106
   340
kuncar@47096
   341
fun get_quot_thm ctxt s =
kuncar@47096
   342
  let
kuncar@47096
   343
    val thy = Proof_Context.theory_of ctxt
kuncar@47096
   344
  in
kuncar@47106
   345
    (case Quotient_Info.lookup_quotients ctxt s of
kuncar@47106
   346
      SOME qdata => Thm.transfer thy (#quot_thm qdata)
kuncar@47106
   347
    | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
kuncar@47096
   348
  end
kuncar@47096
   349
kuncar@47106
   350
fun get_rel_quot_thm ctxt s =
kuncar@47106
   351
   let
kuncar@47106
   352
    val thy = Proof_Context.theory_of ctxt
kuncar@47106
   353
  in
kuncar@47106
   354
    (case Quotient_Info.lookup_quotmaps ctxt s of
kuncar@47106
   355
      SOME map_data => Thm.transfer thy (#quot_thm map_data)
kuncar@47106
   356
    | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
kuncar@47106
   357
  end
kuncar@47096
   358
kuncar@47308
   359
fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3})
kuncar@47096
   360
kuncar@47698
   361
open Lifting_Util
kuncar@47096
   362
kuncar@47698
   363
infix 0 MRSL
kuncar@47096
   364
kuncar@47096
   365
exception NOT_IMPL of string
kuncar@47096
   366
kuncar@47096
   367
fun get_rel_from_quot_thm quot_thm = 
kuncar@47096
   368
  let
kuncar@47096
   369
    val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
kuncar@47096
   370
  in
kuncar@47096
   371
    rel
kuncar@47096
   372
  end
kuncar@47096
   373
kuncar@47096
   374
fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = 
kuncar@47096
   375
  let
kuncar@47096
   376
    val quot_thm_rel = get_rel_from_quot_thm quot_thm
kuncar@47096
   377
  in
kuncar@47308
   378
    if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3}
kuncar@47096
   379
    else raise NOT_IMPL "nested quotients: not implemented yet"
kuncar@47096
   380
  end
kuncar@47096
   381
kuncar@47504
   382
fun prove_quot_thm ctxt (rty, qty) =
kuncar@47096
   383
  if rty = qty
kuncar@47308
   384
  then @{thm identity_quotient3}
kuncar@47096
   385
  else
kuncar@47096
   386
    case (rty, qty) of
kuncar@47096
   387
      (Type (s, tys), Type (s', tys')) =>
kuncar@47096
   388
        if s = s'
kuncar@47096
   389
        then
kuncar@47096
   390
          let
kuncar@47504
   391
            val args = map (prove_quot_thm ctxt) (tys ~~ tys')
kuncar@47096
   392
          in
kuncar@47096
   393
            args MRSL (get_rel_quot_thm ctxt s)
kuncar@47096
   394
          end
kuncar@47096
   395
        else
kuncar@47096
   396
          let
kuncar@47096
   397
            val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
kuncar@47096
   398
            val qtyenv = match ctxt equiv_match_err qty_pat qty
kuncar@47096
   399
            val rtys' = map (Envir.subst_type qtyenv) rtys
kuncar@47504
   400
            val args = map (prove_quot_thm ctxt) (tys ~~ rtys')
kuncar@47096
   401
            val quot_thm = get_quot_thm ctxt s'
kuncar@47096
   402
          in
kuncar@47096
   403
            if forall is_id_quot args
kuncar@47096
   404
            then
kuncar@47096
   405
              quot_thm
kuncar@47096
   406
            else
kuncar@47096
   407
              let
kuncar@47096
   408
                val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
kuncar@47096
   409
              in
kuncar@47096
   410
                mk_quot_thm_compose (rel_quot_thm, quot_thm)
kuncar@47096
   411
             end
kuncar@47096
   412
          end
kuncar@47308
   413
    | _ => @{thm identity_quotient3}
kuncar@47096
   414
kaliszyk@35222
   415
kaliszyk@35222
   416
kaliszyk@35222
   417
(*** Regularization ***)
kaliszyk@35222
   418
kaliszyk@35222
   419
(* Regularizing an rtrm means:
kaliszyk@35222
   420
kaliszyk@35222
   421
 - Quantifiers over types that need lifting are replaced
kaliszyk@35222
   422
   by bounded quantifiers, for example:
kaliszyk@35222
   423
kaliszyk@35222
   424
      All P  ----> All (Respects R) P
kaliszyk@35222
   425
kaliszyk@35222
   426
   where the aggregate relation R is given by the rty and qty;
kaliszyk@35222
   427
kaliszyk@35222
   428
 - Abstractions over types that need lifting are replaced
kaliszyk@35222
   429
   by bounded abstractions, for example:
kaliszyk@35222
   430
kaliszyk@35222
   431
      %x. P  ----> Ball (Respects R) %x. P
kaliszyk@35222
   432
kaliszyk@35222
   433
 - Equalities over types that need lifting are replaced by
kaliszyk@35222
   434
   corresponding equivalence relations, for example:
kaliszyk@35222
   435
kaliszyk@35222
   436
      A = B  ----> R A B
kaliszyk@35222
   437
kaliszyk@35222
   438
   or
kaliszyk@35222
   439
kaliszyk@35222
   440
      A = B  ----> (R ===> R) A B
kaliszyk@35222
   441
kaliszyk@35222
   442
   for more complicated types of A and B
kaliszyk@35222
   443
kaliszyk@35222
   444
kaliszyk@35222
   445
 The regularize_trm accepts raw theorems in which equalities
kaliszyk@35222
   446
 and quantifiers match exactly the ones in the lifted theorem
kaliszyk@35222
   447
 but also accepts partially regularized terms.
kaliszyk@35222
   448
kaliszyk@35222
   449
 This means that the raw theorems can have:
kaliszyk@35222
   450
   Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
kaliszyk@35222
   451
 in the places where:
kaliszyk@35222
   452
   All, Ex, Ex1, %, (op =)
kaliszyk@35222
   453
 is required the lifted theorem.
kaliszyk@35222
   454
kaliszyk@35222
   455
*)
kaliszyk@35222
   456
kaliszyk@35222
   457
val mk_babs = Const (@{const_name Babs}, dummyT)
kaliszyk@35222
   458
val mk_ball = Const (@{const_name Ball}, dummyT)
kaliszyk@35222
   459
val mk_bex  = Const (@{const_name Bex}, dummyT)
kaliszyk@35222
   460
val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
kaliszyk@35222
   461
val mk_resp = Const (@{const_name Respects}, dummyT)
kaliszyk@35222
   462
kaliszyk@35222
   463
(* - applies f to the subterm of an abstraction,
kaliszyk@35222
   464
     otherwise to the given term,
kaliszyk@35222
   465
   - used by regularize, therefore abstracted
kaliszyk@35222
   466
     variables do not have to be treated specially
kaliszyk@35222
   467
*)
kaliszyk@35222
   468
fun apply_subt f (trm1, trm2) =
kaliszyk@35222
   469
  case (trm1, trm2) of
kaliszyk@35222
   470
    (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
kaliszyk@35222
   471
  | _ => f (trm1, trm2)
kaliszyk@35222
   472
kaliszyk@35222
   473
fun term_mismatch str ctxt t1 t2 =
wenzelm@41444
   474
  let
wenzelm@41444
   475
    val t1_str = Syntax.string_of_term ctxt t1
wenzelm@41444
   476
    val t2_str = Syntax.string_of_term ctxt t2
wenzelm@41444
   477
    val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
wenzelm@41444
   478
    val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
wenzelm@41444
   479
  in
wenzelm@41444
   480
    raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
wenzelm@41444
   481
  end
kaliszyk@35222
   482
kaliszyk@35222
   483
(* the major type of All and Ex quantifiers *)
kaliszyk@35222
   484
fun qnt_typ ty = domain_type (domain_type ty)
kaliszyk@35222
   485
kaliszyk@35222
   486
(* Checks that two types match, for example:
kaliszyk@35222
   487
     rty -> rty   matches   qty -> qty *)
wenzelm@45280
   488
fun matches_typ ctxt rT qT =
wenzelm@45340
   489
  let
wenzelm@45340
   490
    val thy = Proof_Context.theory_of ctxt
wenzelm@45340
   491
  in
wenzelm@45340
   492
    if rT = qT then true
wenzelm@45340
   493
    else
wenzelm@45340
   494
      (case (rT, qT) of
wenzelm@45340
   495
        (Type (rs, rtys), Type (qs, qtys)) =>
wenzelm@45340
   496
          if rs = qs then
wenzelm@45340
   497
            if length rtys <> length qtys then false
wenzelm@45340
   498
            else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
wenzelm@45340
   499
          else
wenzelm@45340
   500
            (case Quotient_Info.lookup_quotients_global thy qs of
wenzelm@45340
   501
              SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
wenzelm@45340
   502
            | NONE => false)
wenzelm@45340
   503
      | _ => false)
wenzelm@45340
   504
  end
kaliszyk@35222
   505
kaliszyk@35222
   506
kaliszyk@35222
   507
(* produces a regularized version of rtrm
kaliszyk@35222
   508
kaliszyk@35222
   509
   - the result might contain dummyTs
kaliszyk@35222
   510
urbanc@38718
   511
   - for regularization we do not need any
kaliszyk@35222
   512
     special treatment of bound variables
kaliszyk@35222
   513
*)
kaliszyk@35222
   514
fun regularize_trm ctxt (rtrm, qtrm) =
wenzelm@45280
   515
  (case (rtrm, qtrm) of
kaliszyk@35222
   516
    (Abs (x, ty, t), Abs (_, ty', t')) =>
wenzelm@41444
   517
      let
wenzelm@41444
   518
        val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
wenzelm@41444
   519
      in
wenzelm@41444
   520
        if ty = ty' then subtrm
wenzelm@41444
   521
        else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
wenzelm@41444
   522
      end
wenzelm@45280
   523
haftmann@37677
   524
  | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
wenzelm@41444
   525
      let
wenzelm@41444
   526
        val subtrm = regularize_trm ctxt (t, t')
wenzelm@41444
   527
        val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
wenzelm@41444
   528
      in
wenzelm@41444
   529
        if resrel <> needres
wenzelm@41444
   530
        then term_mismatch "regularize (Babs)" ctxt resrel needres
wenzelm@41444
   531
        else mk_babs $ resrel $ subtrm
wenzelm@41444
   532
      end
kaliszyk@35222
   533
haftmann@37677
   534
  | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
wenzelm@41444
   535
      let
wenzelm@41444
   536
        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
wenzelm@41444
   537
      in
wenzelm@41444
   538
        if ty = ty' then Const (@{const_name All}, ty) $ subtrm
wenzelm@41444
   539
        else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
wenzelm@41444
   540
      end
kaliszyk@35222
   541
haftmann@37677
   542
  | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
wenzelm@41444
   543
      let
wenzelm@41444
   544
        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
wenzelm@41444
   545
      in
wenzelm@41444
   546
        if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
wenzelm@41444
   547
        else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
wenzelm@41444
   548
      end
kaliszyk@35222
   549
haftmann@37677
   550
  | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
haftmann@38795
   551
      (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
haftmann@37677
   552
        (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
haftmann@37677
   553
     Const (@{const_name Ex1}, ty') $ t') =>
wenzelm@41444
   554
      let
wenzelm@41444
   555
        val t_ = incr_boundvars (~1) t
wenzelm@41444
   556
        val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
wenzelm@41444
   557
        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
wenzelm@41444
   558
      in
wenzelm@41444
   559
        if resrel <> needrel
wenzelm@41444
   560
        then term_mismatch "regularize (Bex1)" ctxt resrel needrel
wenzelm@41444
   561
        else mk_bex1_rel $ resrel $ subtrm
wenzelm@41444
   562
      end
kaliszyk@35222
   563
haftmann@38558
   564
  | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
wenzelm@41444
   565
      let
wenzelm@41444
   566
        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
wenzelm@41444
   567
      in
wenzelm@41444
   568
        if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
wenzelm@41444
   569
        else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
wenzelm@41444
   570
      end
kaliszyk@35222
   571
urbanc@38624
   572
  | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
haftmann@38558
   573
     Const (@{const_name All}, ty') $ t') =>
wenzelm@41444
   574
      let
wenzelm@41444
   575
        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
wenzelm@41444
   576
        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
wenzelm@41444
   577
      in
wenzelm@41444
   578
        if resrel <> needrel
wenzelm@41444
   579
        then term_mismatch "regularize (Ball)" ctxt resrel needrel
wenzelm@41444
   580
        else mk_ball $ (mk_resp $ resrel) $ subtrm
wenzelm@41444
   581
      end
kaliszyk@35222
   582
urbanc@38624
   583
  | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
haftmann@38558
   584
     Const (@{const_name Ex}, ty') $ t') =>
wenzelm@41444
   585
      let
wenzelm@41444
   586
        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
wenzelm@41444
   587
        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
wenzelm@41444
   588
      in
wenzelm@41444
   589
        if resrel <> needrel
wenzelm@41444
   590
        then term_mismatch "regularize (Bex)" ctxt resrel needrel
wenzelm@41444
   591
        else mk_bex $ (mk_resp $ resrel) $ subtrm
wenzelm@41444
   592
      end
kaliszyk@35222
   593
urbanc@38624
   594
  | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
wenzelm@41444
   595
      let
wenzelm@41444
   596
        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
wenzelm@41444
   597
        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
wenzelm@41444
   598
      in
wenzelm@41444
   599
        if resrel <> needrel
wenzelm@41444
   600
        then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
wenzelm@41444
   601
        else mk_bex1_rel $ resrel $ subtrm
wenzelm@41444
   602
      end
kaliszyk@35222
   603
kaliszyk@35222
   604
  | (* equalities need to be replaced by appropriate equivalence relations *)
haftmann@38864
   605
    (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
wenzelm@41444
   606
        if ty = ty' then rtrm
wenzelm@41444
   607
        else equiv_relation ctxt (domain_type ty, domain_type ty')
kaliszyk@35222
   608
kaliszyk@35222
   609
  | (* in this case we just check whether the given equivalence relation is correct *)
haftmann@38864
   610
    (rel, Const (@{const_name HOL.eq}, ty')) =>
wenzelm@41444
   611
      let
wenzelm@41444
   612
        val rel_ty = fastype_of rel
wenzelm@41444
   613
        val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
wenzelm@41444
   614
      in
wenzelm@41444
   615
        if rel' aconv rel then rtrm
wenzelm@41444
   616
        else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
wenzelm@41444
   617
      end
kaliszyk@35222
   618
kaliszyk@35222
   619
  | (_, Const _) =>
wenzelm@41444
   620
      let
wenzelm@42361
   621
        val thy = Proof_Context.theory_of ctxt
wenzelm@45280
   622
        fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
wenzelm@41444
   623
          | same_const _ _ = false
wenzelm@41444
   624
      in
wenzelm@41444
   625
        if same_const rtrm qtrm then rtrm
wenzelm@41444
   626
        else
wenzelm@41444
   627
          let
wenzelm@45279
   628
            val rtrm' =
wenzelm@45340
   629
              (case Quotient_Info.lookup_quotconsts_global thy qtrm of
wenzelm@45279
   630
                SOME qconst_info => #rconst qconst_info
wenzelm@45279
   631
              | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
wenzelm@41444
   632
          in
wenzelm@41444
   633
            if Pattern.matches thy (rtrm', rtrm)
wenzelm@41444
   634
            then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
wenzelm@41444
   635
          end
wenzelm@41444
   636
      end
kaliszyk@35222
   637
haftmann@37591
   638
  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
haftmann@37591
   639
     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
kaliszyk@35222
   640
       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
kaliszyk@35222
   641
haftmann@37591
   642
  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
haftmann@37591
   643
     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
kaliszyk@35222
   644
       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
kaliszyk@35222
   645
kaliszyk@35222
   646
  | (t1 $ t2, t1' $ t2') =>
kaliszyk@35222
   647
       regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
kaliszyk@35222
   648
kaliszyk@35222
   649
  | (Bound i, Bound i') =>
wenzelm@41444
   650
      if i = i' then rtrm
wenzelm@41444
   651
      else raise (LIFT_MATCH "regularize (bounds mismatch)")
kaliszyk@35222
   652
kaliszyk@35222
   653
  | _ =>
wenzelm@41444
   654
      let
wenzelm@41444
   655
        val rtrm_str = Syntax.string_of_term ctxt rtrm
wenzelm@41444
   656
        val qtrm_str = Syntax.string_of_term ctxt qtrm
wenzelm@41444
   657
      in
wenzelm@41444
   658
        raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
wenzelm@45280
   659
      end)
kaliszyk@35222
   660
kaliszyk@35222
   661
fun regularize_trm_chk ctxt (rtrm, qtrm) =
kaliszyk@35222
   662
  regularize_trm ctxt (rtrm, qtrm)
kaliszyk@35222
   663
  |> Syntax.check_term ctxt
kaliszyk@35222
   664
kaliszyk@35222
   665
kaliszyk@35222
   666
kaliszyk@35222
   667
(*** Rep/Abs Injection ***)
kaliszyk@35222
   668
kaliszyk@35222
   669
(*
kaliszyk@35222
   670
Injection of Rep/Abs means:
kaliszyk@35222
   671
kaliszyk@35222
   672
  For abstractions:
kaliszyk@35222
   673
kaliszyk@35222
   674
  * If the type of the abstraction needs lifting, then we add Rep/Abs
kaliszyk@35222
   675
    around the abstraction; otherwise we leave it unchanged.
kaliszyk@35222
   676
kaliszyk@35222
   677
  For applications:
kaliszyk@35222
   678
kaliszyk@35222
   679
  * If the application involves a bounded quantifier, we recurse on
kaliszyk@35222
   680
    the second argument. If the application is a bounded abstraction,
kaliszyk@35222
   681
    we always put an Rep/Abs around it (since bounded abstractions
kaliszyk@35222
   682
    are assumed to always need lifting). Otherwise we recurse on both
kaliszyk@35222
   683
    arguments.
kaliszyk@35222
   684
kaliszyk@35222
   685
  For constants:
kaliszyk@35222
   686
kaliszyk@35222
   687
  * If the constant is (op =), we leave it always unchanged.
kaliszyk@35222
   688
    Otherwise the type of the constant needs lifting, we put
kaliszyk@35222
   689
    and Rep/Abs around it.
kaliszyk@35222
   690
kaliszyk@35222
   691
  For free variables:
kaliszyk@35222
   692
kaliszyk@35222
   693
  * We put a Rep/Abs around it if the type needs lifting.
kaliszyk@35222
   694
kaliszyk@35222
   695
  Vars case cannot occur.
kaliszyk@35222
   696
*)
kaliszyk@35222
   697
kaliszyk@35222
   698
fun mk_repabs ctxt (T, T') trm =
kuncar@45797
   699
  absrep_fun ctxt RepF (T, T') $ (absrep_fun ctxt AbsF (T, T') $ trm)
kaliszyk@35222
   700
kaliszyk@35222
   701
fun inj_repabs_err ctxt msg rtrm qtrm =
wenzelm@41444
   702
  let
wenzelm@41444
   703
    val rtrm_str = Syntax.string_of_term ctxt rtrm
wenzelm@41444
   704
    val qtrm_str = Syntax.string_of_term ctxt qtrm
wenzelm@41444
   705
  in
wenzelm@41444
   706
    raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
wenzelm@41444
   707
  end
kaliszyk@35222
   708
kaliszyk@35222
   709
kaliszyk@35222
   710
(* bound variables need to be treated properly,
kaliszyk@35222
   711
   as the type of subterms needs to be calculated   *)
kaliszyk@35222
   712
fun inj_repabs_trm ctxt (rtrm, qtrm) =
kaliszyk@35222
   713
 case (rtrm, qtrm) of
urbanc@38624
   714
    (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
urbanc@38624
   715
       Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
kaliszyk@35222
   716
urbanc@38624
   717
  | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
urbanc@38624
   718
       Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
kaliszyk@35222
   719
urbanc@38624
   720
  | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) =>
kaliszyk@35222
   721
      let
kaliszyk@35222
   722
        val rty = fastype_of rtrm
kaliszyk@35222
   723
        val qty = fastype_of qtrm
kaliszyk@35222
   724
      in
urbanc@38624
   725
        mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
kaliszyk@35222
   726
      end
kaliszyk@35222
   727
kaliszyk@35222
   728
  | (Abs (x, T, t), Abs (x', T', t')) =>
kaliszyk@35222
   729
      let
kaliszyk@35222
   730
        val rty = fastype_of rtrm
kaliszyk@35222
   731
        val qty = fastype_of qtrm
kaliszyk@35222
   732
        val (y, s) = Term.dest_abs (x, T, t)
kaliszyk@35222
   733
        val (_, s') = Term.dest_abs (x', T', t')
kaliszyk@35222
   734
        val yvar = Free (y, T)
kaliszyk@35222
   735
        val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
kaliszyk@35222
   736
      in
kaliszyk@35222
   737
        if rty = qty then result
kaliszyk@35222
   738
        else mk_repabs ctxt (rty, qty) result
kaliszyk@35222
   739
      end
kaliszyk@35222
   740
kaliszyk@35222
   741
  | (t $ s, t' $ s') =>
kaliszyk@35222
   742
       (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
kaliszyk@35222
   743
kaliszyk@35222
   744
  | (Free (_, T), Free (_, T')) =>
kaliszyk@35222
   745
        if T = T' then rtrm
kaliszyk@35222
   746
        else mk_repabs ctxt (T, T') rtrm
kaliszyk@35222
   747
haftmann@38864
   748
  | (_, Const (@{const_name HOL.eq}, _)) => rtrm
kaliszyk@35222
   749
kaliszyk@35222
   750
  | (_, Const (_, T')) =>
kaliszyk@35222
   751
      let
kaliszyk@35222
   752
        val rty = fastype_of rtrm
kaliszyk@35222
   753
      in
kaliszyk@35222
   754
        if rty = T' then rtrm
kaliszyk@35222
   755
        else mk_repabs ctxt (rty, T') rtrm
kaliszyk@35222
   756
      end
kaliszyk@35222
   757
kaliszyk@35222
   758
  | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
kaliszyk@35222
   759
kaliszyk@35222
   760
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
kaliszyk@35222
   761
  inj_repabs_trm ctxt (rtrm, qtrm)
kaliszyk@35222
   762
  |> Syntax.check_term ctxt
kaliszyk@35222
   763
kaliszyk@35222
   764
kaliszyk@35222
   765
kaliszyk@35222
   766
(*** Wrapper for automatically transforming an rthm into a qthm ***)
kaliszyk@35222
   767
urbanc@37592
   768
(* substitutions functions for r/q-types and
urbanc@37592
   769
   r/q-constants, respectively
urbanc@37560
   770
*)
urbanc@37592
   771
fun subst_typ ctxt ty_subst rty =
urbanc@37560
   772
  case rty of
urbanc@37560
   773
    Type (s, rtys) =>
urbanc@37560
   774
      let
wenzelm@42361
   775
        val thy = Proof_Context.theory_of ctxt
urbanc@37592
   776
        val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys)
urbanc@37560
   777
urbanc@37560
   778
        fun matches [] = rty'
urbanc@37560
   779
          | matches ((rty, qty)::tail) =
wenzelm@45280
   780
              (case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
urbanc@37560
   781
                NONE => matches tail
cezarykaliszyk@46416
   782
              | SOME inst => subst_typ ctxt ty_subst (Envir.subst_type inst qty))
urbanc@37560
   783
      in
wenzelm@41444
   784
        matches ty_subst
wenzelm@41444
   785
      end
urbanc@37560
   786
  | _ => rty
urbanc@37560
   787
urbanc@37592
   788
fun subst_trm ctxt ty_subst trm_subst rtrm =
urbanc@37560
   789
  case rtrm of
urbanc@37592
   790
    t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2)
urbanc@37592
   791
  | Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t)
urbanc@37592
   792
  | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
urbanc@37592
   793
  | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
urbanc@37560
   794
  | Bound i => Bound i
wenzelm@41444
   795
  | Const (a, ty) =>
urbanc@37560
   796
      let
wenzelm@42361
   797
        val thy = Proof_Context.theory_of ctxt
kaliszyk@35222
   798
urbanc@37592
   799
        fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
urbanc@37560
   800
          | matches ((rconst, qconst)::tail) =
wenzelm@45280
   801
              (case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
urbanc@37560
   802
                NONE => matches tail
cezarykaliszyk@46416
   803
              | SOME inst => subst_trm ctxt ty_subst trm_subst (Envir.subst_term inst qconst))
urbanc@37560
   804
      in
urbanc@37560
   805
        matches trm_subst
urbanc@37560
   806
      end
urbanc@37560
   807
urbanc@37592
   808
(* generate type and term substitutions out of the
wenzelm@41444
   809
   qtypes involved in a quotient; the direction flag
wenzelm@41444
   810
   indicates in which direction the substitutions work:
wenzelm@41444
   811
urbanc@37592
   812
     true:  quotient -> raw
urbanc@37592
   813
     false: raw -> quotient
urbanc@37560
   814
*)
urbanc@37592
   815
fun mk_ty_subst qtys direction ctxt =
wenzelm@41444
   816
  let
wenzelm@42361
   817
    val thy = Proof_Context.theory_of ctxt
wenzelm@41444
   818
  in
wenzelm@45279
   819
    Quotient_Info.dest_quotients ctxt
wenzelm@41444
   820
    |> map (fn x => (#rtyp x, #qtyp x))
wenzelm@41444
   821
    |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
wenzelm@41444
   822
    |> map (if direction then swap else I)
wenzelm@41444
   823
  end
kaliszyk@35222
   824
urbanc@37592
   825
fun mk_trm_subst qtys direction ctxt =
wenzelm@41444
   826
  let
wenzelm@41444
   827
    val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
wenzelm@41444
   828
    fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
kaliszyk@37563
   829
wenzelm@41444
   830
    val const_substs =
wenzelm@45279
   831
      Quotient_Info.dest_quotconsts ctxt
wenzelm@41444
   832
      |> map (fn x => (#rconst x, #qconst x))
wenzelm@41444
   833
      |> map (if direction then swap else I)
urbanc@37560
   834
wenzelm@41444
   835
    val rel_substs =
wenzelm@45279
   836
      Quotient_Info.dest_quotients ctxt
wenzelm@41444
   837
      |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
wenzelm@41444
   838
      |> map (if direction then swap else I)
wenzelm@41444
   839
  in
wenzelm@41444
   840
    filter proper (const_substs @ rel_substs)
wenzelm@41444
   841
  end
kaliszyk@35222
   842
urbanc@37592
   843
urbanc@37560
   844
(* derives a qtyp and qtrm out of a rtyp and rtrm,
wenzelm@41444
   845
   respectively
urbanc@37560
   846
*)
urbanc@38624
   847
fun derive_qtyp ctxt qtys rty =
urbanc@37592
   848
  subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
urbanc@37592
   849
urbanc@38624
   850
fun derive_qtrm ctxt qtys rtrm =
urbanc@37592
   851
  subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
kaliszyk@35222
   852
urbanc@37592
   853
(* derives a rtyp and rtrm out of a qtyp and qtrm,
wenzelm@41444
   854
   respectively
urbanc@37592
   855
*)
urbanc@38624
   856
fun derive_rtyp ctxt qtys qty =
urbanc@37592
   857
  subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
urbanc@37592
   858
urbanc@38624
   859
fun derive_rtrm ctxt qtys qtrm =
urbanc@37592
   860
  subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
urbanc@37560
   861
kaliszyk@35222
   862
wenzelm@45279
   863
end;