src/HOL/Tools/Lifting/lifting_term.ML
author wenzelm
Sun May 03 14:35:48 2015 +0200 (2015-05-03)
changeset 60239 755e11e2e15d
parent 60222 78fc1b798c61
child 60642 48dd1cefb4ae
permissions -rw-r--r--
make SML/NJ more happy;
kuncar@47308
     1
(*  Title:      HOL/Tools/Lifting/lifting_term.ML
kuncar@47308
     2
    Author:     Ondrej Kuncar
kuncar@47308
     3
kuncar@47308
     4
Proves Quotient theorem.
kuncar@47308
     5
*)
kuncar@47308
     6
kuncar@47308
     7
signature LIFTING_TERM =
kuncar@47308
     8
sig
kuncar@47379
     9
  exception QUOT_THM of typ * typ * Pretty.T
kuncar@50227
    10
  exception PARAM_QUOT_THM of typ * Pretty.T
kuncar@51374
    11
  exception MERGE_TRANSFER_REL of Pretty.T
kuncar@47504
    12
  exception CHECK_RTY of typ * typ
kuncar@47379
    13
kuncar@60217
    14
  type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
kuncar@60217
    15
  comp_lift: typ -> thm * 'a -> thm * 'a }
kuncar@60217
    16
kuncar@60222
    17
  type quotients = Lifting_Info.quotient Symtab.table
kuncar@60222
    18
  
kuncar@60217
    19
  val force_qty_type: Proof.context -> typ -> thm -> thm
kuncar@60217
    20
kuncar@60222
    21
  val prove_schematic_quot_thm: 'a fold_quot_thm -> quotients -> Proof.context -> 
kuncar@60222
    22
    typ * typ -> 'a -> thm * 'a
kuncar@60217
    23
kuncar@57663
    24
  val instantiate_rtys: Proof.context -> typ * typ -> typ * typ
kuncar@57663
    25
kuncar@47504
    26
  val prove_quot_thm: Proof.context -> typ * typ -> thm
kuncar@47308
    27
kuncar@47852
    28
  val abs_fun: Proof.context -> typ * typ -> term
kuncar@47308
    29
kuncar@47308
    30
  val equiv_relation: Proof.context -> typ * typ -> term
kuncar@50227
    31
kuncar@50288
    32
  val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context
kuncar@50288
    33
kuncar@50288
    34
  val generate_parametrized_relator: Proof.context -> typ -> term * term list
kuncar@51374
    35
kuncar@51374
    36
  val merge_transfer_relations: Proof.context -> cterm -> thm
kuncar@51374
    37
kuncar@51374
    38
  val parametrize_transfer_rule: Proof.context -> thm -> thm
kuncar@47308
    39
end
kuncar@47308
    40
kuncar@47308
    41
structure Lifting_Term: LIFTING_TERM =
kuncar@47308
    42
struct
kuncar@47698
    43
open Lifting_Util
kuncar@47698
    44
kuncar@47698
    45
infix 0 MRSL
kuncar@47698
    46
kuncar@47379
    47
exception QUOT_THM_INTERNAL of Pretty.T
kuncar@47379
    48
exception QUOT_THM of typ * typ * Pretty.T
kuncar@50227
    49
exception PARAM_QUOT_THM of typ * Pretty.T
kuncar@51374
    50
exception MERGE_TRANSFER_REL of Pretty.T
kuncar@47504
    51
exception CHECK_RTY of typ * typ
kuncar@47504
    52
kuncar@60222
    53
type quotients = Lifting_Info.quotient Symtab.table
kuncar@60222
    54
kuncar@47504
    55
fun match ctxt err ty_pat ty =
kuncar@47504
    56
  let
kuncar@47504
    57
    val thy = Proof_Context.theory_of ctxt
kuncar@47504
    58
  in
kuncar@47504
    59
    Sign.typ_match thy (ty_pat, ty) Vartab.empty
kuncar@47504
    60
      handle Type.TYPE_MATCH => err ctxt ty_pat ty
kuncar@47504
    61
  end
kuncar@47504
    62
kuncar@47504
    63
fun equiv_match_err ctxt ty_pat ty =
kuncar@47504
    64
  let
kuncar@47504
    65
    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
kuncar@47504
    66
    val ty_str = Syntax.string_of_typ ctxt ty
kuncar@47504
    67
  in
kuncar@47504
    68
    raise QUOT_THM_INTERNAL (Pretty.block
kuncar@47504
    69
      [Pretty.str ("The quotient type " ^ quote ty_str),
kuncar@47504
    70
       Pretty.brk 1,
kuncar@47504
    71
       Pretty.str ("and the quotient type pattern " ^ quote ty_pat_str),
kuncar@47504
    72
       Pretty.brk 1,
kuncar@47504
    73
       Pretty.str "don't match."])
kuncar@47504
    74
  end
kuncar@47308
    75
wenzelm@60239
    76
fun get_quot_data (quotients: quotients) s =
kuncar@60222
    77
  case Symtab.lookup quotients s of
kuncar@51374
    78
    SOME qdata => qdata
kuncar@51374
    79
  | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
kuncar@51374
    80
    [Pretty.str ("No quotient type " ^ quote s), 
kuncar@51374
    81
     Pretty.brk 1, 
kuncar@51374
    82
     Pretty.str "found."])
kuncar@51374
    83
kuncar@60222
    84
fun get_quot_thm quotients ctxt s =
kuncar@47308
    85
  let
kuncar@47308
    86
    val thy = Proof_Context.theory_of ctxt
kuncar@47308
    87
  in
kuncar@60222
    88
    Thm.transfer thy (#quot_thm (get_quot_data quotients s))
kuncar@51374
    89
  end
kuncar@51374
    90
kuncar@60222
    91
fun has_pcrel_info quotients s = is_some (#pcr_info (get_quot_data quotients s))
kuncar@55455
    92
kuncar@60222
    93
fun get_pcrel_info quotients s =
kuncar@60222
    94
  case #pcr_info (get_quot_data quotients s) of
kuncar@53219
    95
    SOME pcr_info => pcr_info
kuncar@51374
    96
  | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
kuncar@51374
    97
    [Pretty.str ("No parametrized correspondce relation for " ^ quote s), 
kuncar@51374
    98
     Pretty.brk 1, 
kuncar@51374
    99
     Pretty.str "found."])
kuncar@51374
   100
kuncar@60222
   101
fun get_pcrel_def quotients ctxt s =
kuncar@51374
   102
  let
kuncar@51374
   103
    val thy = Proof_Context.theory_of ctxt
kuncar@51374
   104
  in
kuncar@60222
   105
    Thm.transfer thy (#pcrel_def (get_pcrel_info quotients s))
kuncar@51374
   106
  end
kuncar@51374
   107
kuncar@60222
   108
fun get_pcr_cr_eq quotients ctxt s =
kuncar@51374
   109
  let
kuncar@51374
   110
    val thy = Proof_Context.theory_of ctxt
kuncar@51374
   111
  in
kuncar@60222
   112
    Thm.transfer thy (#pcr_cr_eq (get_pcrel_info quotients s))
kuncar@47308
   113
  end
kuncar@47308
   114
kuncar@47308
   115
fun get_rel_quot_thm ctxt s =
kuncar@47308
   116
   let
kuncar@47308
   117
    val thy = Proof_Context.theory_of ctxt
kuncar@47308
   118
  in
kuncar@53219
   119
    (case Lifting_Info.lookup_quot_maps ctxt s of
kuncar@47777
   120
      SOME map_data => Thm.transfer thy (#rel_quot_thm map_data)
kuncar@47379
   121
    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
kuncar@47379
   122
      [Pretty.str ("No relator for the type " ^ quote s), 
kuncar@47379
   123
       Pretty.brk 1,
kuncar@47379
   124
       Pretty.str "found."]))
kuncar@47308
   125
  end
kuncar@47308
   126
kuncar@51374
   127
fun get_rel_distr_rules ctxt s tm =
kuncar@51374
   128
  let
kuncar@51374
   129
    val thy = Proof_Context.theory_of ctxt
kuncar@51374
   130
  in
kuncar@51374
   131
    (case Lifting_Info.lookup_relator_distr_data ctxt s of
kuncar@51374
   132
      SOME rel_distr_thm => (
kuncar@51374
   133
        case tm of
kuncar@51374
   134
          Const (@{const_name POS}, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm)
kuncar@51374
   135
          | Const (@{const_name NEG}, _) => map (Thm.transfer thy) (#neg_distr_rules rel_distr_thm)
kuncar@51374
   136
      )
kuncar@51374
   137
    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
kuncar@51374
   138
      [Pretty.str ("No relator distr. data for the type " ^ quote s), 
kuncar@51374
   139
       Pretty.brk 1,
kuncar@51374
   140
       Pretty.str "found."]))
kuncar@51374
   141
  end
kuncar@51374
   142
wenzelm@59848
   143
fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient})
kuncar@47504
   144
kuncar@47778
   145
fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars =
kuncar@47778
   146
  case try (get_rel_quot_thm ctxt) type_name of
kuncar@47778
   147
    NONE => rty_Tvars ~~ qty_Tvars
kuncar@47778
   148
    | SOME rel_quot_thm =>
kuncar@47778
   149
      let 
kuncar@47778
   150
        fun quot_term_absT quot_term = 
kuncar@47778
   151
          let 
kuncar@47778
   152
            val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term
kuncar@47778
   153
          in
kuncar@47778
   154
            fastype_of abs
kuncar@47778
   155
          end
kuncar@47778
   156
kuncar@47778
   157
        fun equiv_univ_err ctxt ty_pat ty =
kuncar@47778
   158
          let
kuncar@47778
   159
            val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
kuncar@47778
   160
            val ty_str = Syntax.string_of_typ ctxt ty
kuncar@47778
   161
          in
kuncar@47778
   162
            raise QUOT_THM_INTERNAL (Pretty.block
kuncar@47778
   163
              [Pretty.str ("The type " ^ quote ty_str),
kuncar@47778
   164
               Pretty.brk 1,
kuncar@47778
   165
               Pretty.str ("and the relator type pattern " ^ quote ty_pat_str),
kuncar@47778
   166
               Pretty.brk 1,
kuncar@47778
   167
               Pretty.str "don't unify."])
kuncar@47778
   168
          end
kuncar@47778
   169
kuncar@47778
   170
        fun raw_match (TVar (v, S), T) subs =
kuncar@47778
   171
              (case Vartab.defined subs v of
kuncar@47778
   172
                false => Vartab.update_new (v, (S, T)) subs
kuncar@47778
   173
              | true => subs)
kuncar@47778
   174
          | raw_match (Type (_, Ts), Type (_, Us)) subs =
kuncar@47778
   175
              raw_matches (Ts, Us) subs
kuncar@47778
   176
          | raw_match _ subs = subs
kuncar@47778
   177
        and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs)
kuncar@47778
   178
          | raw_matches _ subs = subs
kuncar@47778
   179
kuncar@47778
   180
        val rty = Type (type_name, rty_Tvars)
kuncar@47778
   181
        val qty = Type (type_name, qty_Tvars)
wenzelm@59582
   182
        val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm
kuncar@47778
   183
        val schematic_rel_absT = quot_term_absT rel_quot_thm_concl;
kuncar@54946
   184
        val thy = Proof_Context.theory_of ctxt
kuncar@47778
   185
        val absT = rty --> qty
kuncar@54946
   186
        val schematic_absT = 
kuncar@54946
   187
          absT 
kuncar@54946
   188
          |> Logic.type_map (singleton (Variable.polymorphic ctxt))
kuncar@54946
   189
          |> Logic.incr_tvar (maxidx_of_typ schematic_rel_absT + 1) 
kuncar@54946
   190
            (* because absT can already contain schematic variables from rty patterns *)
kuncar@47853
   191
        val maxidx = Term.maxidx_of_typs [schematic_rel_absT, schematic_absT]
kuncar@47853
   192
        val _ = Sign.typ_unify thy (schematic_rel_absT, schematic_absT) (Vartab.empty,maxidx)
kuncar@47778
   193
          handle Type.TUNIFY => equiv_univ_err ctxt schematic_rel_absT schematic_absT
kuncar@47778
   194
        val subs = raw_match (schematic_rel_absT, absT) Vartab.empty
wenzelm@59582
   195
        val rel_quot_thm_prems = (Logic.strip_imp_prems o Thm.prop_of) rel_quot_thm
kuncar@47778
   196
      in
kuncar@47778
   197
        map (dest_funT o 
kuncar@47778
   198
             Envir.subst_type subs o
kuncar@47778
   199
             quot_term_absT) 
kuncar@47778
   200
          rel_quot_thm_prems
kuncar@47778
   201
      end
kuncar@47778
   202
kuncar@60222
   203
fun gen_rty_is_TVar quotients ctxt qty = qty |> Tname |> get_quot_thm quotients ctxt |> 
kuncar@60222
   204
  quot_thm_rty_qty |> fst |> is_TVar
kuncar@55454
   205
kuncar@60222
   206
fun gen_instantiate_rtys quotients ctxt (rty, (qty as Type (qty_name, _))) =
kuncar@51374
   207
  let
kuncar@60222
   208
    val quot_thm = get_quot_thm quotients ctxt qty_name
kuncar@55454
   209
    val (rty_pat, qty_pat) = quot_thm_rty_qty quot_thm
kuncar@55454
   210
kuncar@54945
   211
    fun inst_rty (Type (s, tys), Type (s', tys')) = 
kuncar@54945
   212
        if s = s' then Type (s', map inst_rty (tys ~~ tys'))
kuncar@54945
   213
        else raise QUOT_THM_INTERNAL (Pretty.block 
kuncar@54945
   214
          [Pretty.str "The type",
kuncar@54945
   215
           Pretty.brk 1,
kuncar@54945
   216
           Syntax.pretty_typ ctxt rty,
kuncar@54945
   217
           Pretty.brk 1,
kuncar@54945
   218
           Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"),
kuncar@54945
   219
           Pretty.brk 1,
kuncar@54945
   220
           Pretty.str "the correct raw type must be an instance of",
kuncar@54945
   221
           Pretty.brk 1,
kuncar@54945
   222
           Syntax.pretty_typ ctxt rty_pat])
kuncar@54945
   223
      | inst_rty (t as Type (_, _), TFree _) = t
kuncar@54945
   224
      | inst_rty ((TVar _), rty) = rty
kuncar@54945
   225
      | inst_rty ((TFree _), rty) = rty
kuncar@54945
   226
      | inst_rty (_, _) = error "check_raw_types: we should not be here"
kuncar@54945
   227
kuncar@51374
   228
    val qtyenv = match ctxt equiv_match_err qty_pat qty
kuncar@51374
   229
  in
kuncar@55454
   230
    (inst_rty (rty_pat, rty), Envir.subst_type qtyenv rty_pat)
kuncar@51374
   231
  end
kuncar@60222
   232
  | gen_instantiate_rtys _ _ _ = error "gen_instantiate_rtys: not Type"
kuncar@60222
   233
kuncar@60222
   234
fun instantiate_rtys ctxt (rty, qty) = 
kuncar@60222
   235
  gen_instantiate_rtys (Lifting_Info.get_quotients ctxt) ctxt (rty, qty)
kuncar@51374
   236
kuncar@60217
   237
type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
kuncar@60217
   238
  comp_lift: typ -> thm * 'a -> thm * 'a }
kuncar@60217
   239
wenzelm@60239
   240
fun prove_schematic_quot_thm (actions: 'a fold_quot_thm) quotients ctxt (rty, qty) fold_val =
kuncar@55454
   241
  let
kuncar@55454
   242
    fun lifting_step (rty, qty) =
kuncar@55454
   243
      let
kuncar@60222
   244
        val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty)
kuncar@60222
   245
        val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) 
kuncar@55454
   246
          else (Targs rty', Targs rtyq) 
kuncar@60217
   247
        val (args, fold_val) = 
kuncar@60222
   248
          fold_map (prove_schematic_quot_thm actions quotients ctxt) (rty's ~~ rtyqs) fold_val
kuncar@55454
   249
      in
kuncar@55454
   250
        if forall is_id_quot args
kuncar@55454
   251
        then
kuncar@60217
   252
          let
kuncar@60222
   253
            val quot_thm = get_quot_thm quotients ctxt (Tname qty)
kuncar@60217
   254
          in
kuncar@60217
   255
            #lift actions qty (quot_thm, fold_val)
kuncar@60217
   256
          end
kuncar@55454
   257
        else
kuncar@55454
   258
          let
kuncar@60222
   259
            val quot_thm = get_quot_thm quotients ctxt (Tname qty)
kuncar@60222
   260
            val rel_quot_thm = if gen_rty_is_TVar quotients ctxt qty then the_single args else
kuncar@55454
   261
              args MRSL (get_rel_quot_thm ctxt (Tname rty))
kuncar@60217
   262
            val comp_quot_thm = [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
kuncar@55454
   263
          in
kuncar@60217
   264
            #comp_lift actions qty (comp_quot_thm, fold_val)
kuncar@55454
   265
         end
kuncar@55454
   266
      end
kuncar@55454
   267
  in
kuncar@55454
   268
    (case (rty, qty) of
kuncar@55454
   269
      (Type (s, tys), Type (s', tys')) =>
kuncar@55454
   270
        if s = s'
kuncar@55454
   271
        then
kuncar@55454
   272
          let
kuncar@60217
   273
            val (args, fold_val) = 
kuncar@60222
   274
              fold_map (prove_schematic_quot_thm actions quotients ctxt) 
kuncar@60222
   275
                (zip_Tvars ctxt s tys tys') fold_val
kuncar@55454
   276
          in
kuncar@55454
   277
            if forall is_id_quot args
kuncar@55454
   278
            then
kuncar@60217
   279
              (@{thm identity_quotient}, fold_val)
kuncar@55454
   280
            else
kuncar@60217
   281
              let
kuncar@60217
   282
                val quot_thm = args MRSL (get_rel_quot_thm ctxt s)
kuncar@60217
   283
              in
kuncar@60217
   284
                #constr actions qty (quot_thm, fold_val)
kuncar@60217
   285
              end
kuncar@55454
   286
          end
kuncar@55454
   287
        else
kuncar@55454
   288
          lifting_step (rty, qty)
kuncar@55454
   289
      | (_, Type (s', tys')) => 
kuncar@60222
   290
        (case try (get_quot_thm quotients ctxt) s' of
kuncar@55454
   291
          SOME quot_thm => 
kuncar@47504
   292
            let
kuncar@55454
   293
              val rty_pat = (fst o quot_thm_rty_qty) quot_thm
kuncar@47504
   294
            in
kuncar@55454
   295
              lifting_step (rty_pat, qty)              
kuncar@55454
   296
            end
kuncar@55454
   297
          | NONE =>
kuncar@55454
   298
            let                                               
kuncar@55454
   299
              val rty_pat = Type (s', map (fn _ => TFree ("a",[])) tys')
kuncar@55454
   300
            in
kuncar@60222
   301
              prove_schematic_quot_thm actions quotients ctxt (rty_pat, qty) fold_val
kuncar@55454
   302
            end)
kuncar@60217
   303
      | _ => (@{thm identity_quotient}, fold_val)
kuncar@60217
   304
      )
kuncar@55454
   305
  end
kuncar@55454
   306
  handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
kuncar@47308
   307
wenzelm@59630
   308
fun force_qty_type ctxt qty quot_thm =
kuncar@47308
   309
  let
wenzelm@59630
   310
    val thy = Proof_Context.theory_of ctxt
kuncar@47504
   311
    val (_, qty_schematic) = quot_thm_rty_qty quot_thm
kuncar@47504
   312
    val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
wenzelm@59630
   313
    fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty)
wenzelm@59630
   314
    val ty_inst = Vartab.fold (cons o prep_ty) match_env []
kuncar@47308
   315
  in
kuncar@47504
   316
    Thm.instantiate (ty_inst, []) quot_thm
kuncar@47504
   317
  end
kuncar@47504
   318
kuncar@47504
   319
fun check_rty_type ctxt rty quot_thm =
kuncar@47504
   320
  let  
kuncar@47504
   321
    val thy = Proof_Context.theory_of ctxt
kuncar@47504
   322
    val (rty_forced, _) = quot_thm_rty_qty quot_thm
kuncar@47504
   323
    val rty_schematic = Logic.type_map (singleton (Variable.polymorphic ctxt)) rty
kuncar@47504
   324
    val _ = Sign.typ_match thy (rty_schematic, rty_forced) Vartab.empty
kuncar@47504
   325
      handle Type.TYPE_MATCH => raise CHECK_RTY (rty_schematic, rty_forced)
kuncar@47504
   326
  in
kuncar@47504
   327
    ()
kuncar@47504
   328
  end
kuncar@47504
   329
kuncar@47852
   330
(*
kuncar@47852
   331
  The function tries to prove that rty and qty form a quotient.
kuncar@47852
   332
kuncar@47852
   333
  Returns: Quotient theorem; an abstract type of the theorem is exactly
kuncar@47852
   334
    qty, a representation type of the theorem is an instance of rty in general.
kuncar@47852
   335
*)
kuncar@47852
   336
kuncar@60217
   337
kuncar@60217
   338
local
kuncar@60217
   339
  val id_actions = { constr = K I, lift = K I, comp_lift = K I }
kuncar@60217
   340
in
kuncar@60217
   341
  fun prove_quot_thm ctxt (rty, qty) =
kuncar@60217
   342
    let
kuncar@60222
   343
      val quotients = Lifting_Info.get_quotients ctxt
kuncar@60222
   344
      val (schematic_quot_thm, _) = prove_schematic_quot_thm id_actions quotients ctxt (rty, qty) ()
kuncar@60222
   345
      val quot_thm = force_qty_type ctxt qty schematic_quot_thm
kuncar@60217
   346
      val _ = check_rty_type ctxt rty quot_thm
kuncar@60217
   347
    in
kuncar@60217
   348
      quot_thm
kuncar@60217
   349
    end
kuncar@60217
   350
end
kuncar@47308
   351
kuncar@54335
   352
(*
kuncar@54335
   353
  Computes the composed abstraction function for rty and qty.
kuncar@54335
   354
*)
kuncar@54335
   355
kuncar@47852
   356
fun abs_fun ctxt (rty, qty) =
kuncar@47504
   357
  quot_thm_abs (prove_quot_thm ctxt (rty, qty))
huffman@47350
   358
kuncar@54335
   359
(*
kuncar@54335
   360
  Computes the composed equivalence relation for rty and qty.
kuncar@54335
   361
*)
kuncar@54335
   362
kuncar@47308
   363
fun equiv_relation ctxt (rty, qty) =
kuncar@47504
   364
  quot_thm_rel (prove_quot_thm ctxt (rty, qty))
kuncar@47308
   365
kuncar@50288
   366
val get_fresh_Q_t =
kuncar@50227
   367
  let
kuncar@50288
   368
    val Q_t = @{term "Trueprop (Quotient R Abs Rep T)"}
kuncar@50227
   369
    val frees_Q_t = Term.add_free_names Q_t []
kuncar@50288
   370
    val tfrees_Q_t = rev (Term.add_tfree_names Q_t [])
kuncar@50227
   371
  in
kuncar@50288
   372
    fn ctxt =>
kuncar@50288
   373
    let
kuncar@50288
   374
      fun rename_free_var tab (Free (name, typ)) = Free (the_default name (AList.lookup op= tab name),typ)
kuncar@50288
   375
        | rename_free_var _ t = t
kuncar@50288
   376
      
kuncar@50288
   377
      fun rename_free_vars tab = map_aterms (rename_free_var tab)
kuncar@50288
   378
      
kuncar@50288
   379
      fun rename_free_tvars tab =
kuncar@50288
   380
        map_types (map_type_tfree (fn (name, sort) => TFree (the_default name (AList.lookup op= tab name), sort)))
kuncar@50288
   381
      
kuncar@50288
   382
      val (new_frees_Q_t, ctxt) = Variable.variant_fixes frees_Q_t ctxt
kuncar@50288
   383
      val tab_frees = frees_Q_t ~~ new_frees_Q_t
kuncar@50288
   384
      
kuncar@50288
   385
      val (new_tfrees_Q_t, ctxt) = Variable.invent_types (replicate (length tfrees_Q_t) []) ctxt
kuncar@50288
   386
      val tab_tfrees = tfrees_Q_t ~~ (fst o split_list) new_tfrees_Q_t
kuncar@50288
   387
kuncar@50288
   388
      val renamed_Q_t = rename_free_vars tab_frees Q_t
kuncar@50288
   389
      val renamed_Q_t = rename_free_tvars tab_tfrees renamed_Q_t
kuncar@50288
   390
    in
kuncar@50288
   391
      (renamed_Q_t, ctxt)
kuncar@50288
   392
    end
kuncar@50227
   393
  end
kuncar@50227
   394
kuncar@54335
   395
(*
kuncar@54335
   396
  For the given type, it proves a composed Quotient map theorem, where for each type variable
kuncar@54335
   397
  extra Quotient assumption is generated. E.g., for 'a list it generates exactly
kuncar@54335
   398
  the Quotient map theorem for the list type. The function generalizes this for the whole
kuncar@54335
   399
  type universe. New fresh variables in the assumptions are fixed in the returned context.
kuncar@54335
   400
kuncar@54335
   401
  Returns: the composed Quotient map theorem and list mapping each type variable in ty
kuncar@54335
   402
  to the corresponding assumption in the returned theorem.
kuncar@54335
   403
*)
kuncar@54335
   404
kuncar@50227
   405
fun prove_param_quot_thm ctxt ty = 
kuncar@50227
   406
  let 
kuncar@50227
   407
    fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) =
kuncar@50227
   408
      if null tys 
kuncar@50227
   409
      then 
kuncar@50227
   410
        let 
wenzelm@59582
   411
          val instantiated_id_quot_thm =
wenzelm@59630
   412
            instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
kuncar@50227
   413
        in
kuncar@50227
   414
          (instantiated_id_quot_thm, (table, ctxt)) 
kuncar@50227
   415
        end
kuncar@50227
   416
      else
kuncar@50227
   417
        let
kuncar@50227
   418
          val (args, table_ctxt) = fold_map generate tys table_ctxt
kuncar@50227
   419
        in
kuncar@50227
   420
          (args MRSL (get_rel_quot_thm ctxt s), table_ctxt)
kuncar@50227
   421
        end 
kuncar@51374
   422
      | generate ty (table, ctxt) =
kuncar@50227
   423
        if AList.defined (op=) table ty 
kuncar@50227
   424
        then (the (AList.lookup (op=) table ty), (table, ctxt))
kuncar@50227
   425
        else 
kuncar@50227
   426
          let
kuncar@50227
   427
            val (Q_t, ctxt') = get_fresh_Q_t ctxt
wenzelm@59630
   428
            val Q_thm = Thm.assume (Thm.cterm_of ctxt' Q_t)
wenzelm@59630
   429
            val table' = (ty, Q_thm) :: table
kuncar@50227
   430
          in
kuncar@50227
   431
            (Q_thm, (table', ctxt'))
kuncar@50227
   432
          end
kuncar@50227
   433
kuncar@50288
   434
    val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt)
kuncar@50227
   435
  in
kuncar@50288
   436
    (param_quot_thm, rev table, ctxt)
kuncar@50227
   437
  end
kuncar@50227
   438
  handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg)
kuncar@50227
   439
kuncar@54335
   440
(*
kuncar@54335
   441
  It computes a parametrized relator for the given type ty. E.g., for 'a dlist:
kuncar@54335
   442
  list_all2 ?R OO cr_dlist with parameters [?R].
kuncar@54335
   443
  
kuncar@54335
   444
  Returns: the definitional term and list of parameters (relations).
kuncar@54335
   445
*)
kuncar@54335
   446
kuncar@50288
   447
fun generate_parametrized_relator ctxt ty =
kuncar@50288
   448
  let
kuncar@50288
   449
    val orig_ctxt = ctxt
kuncar@50288
   450
    val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty
kuncar@50288
   451
    val parametrized_relator = quot_thm_crel quot_thm
kuncar@50288
   452
    val args = map (fn (_, q_thm) => quot_thm_crel q_thm) table
kuncar@50288
   453
    val exported_terms = Variable.exportT_terms ctxt orig_ctxt (parametrized_relator :: args)
kuncar@50288
   454
  in
kuncar@50288
   455
    (hd exported_terms, tl exported_terms)
kuncar@50288
   456
  end
kuncar@50288
   457
kuncar@51374
   458
(* Parametrization *)
kuncar@51374
   459
kuncar@51374
   460
local
wenzelm@59582
   461
  fun get_lhs rule = (Thm.dest_fun o Thm.dest_arg o strip_imp_concl o Thm.cprop_of) rule;
kuncar@51374
   462
  
kuncar@51374
   463
  fun no_imp _ = raise CTERM ("no implication", []);
kuncar@51374
   464
  
kuncar@51374
   465
  infix 0 else_imp
kuncar@51374
   466
kuncar@51374
   467
  fun (cv1 else_imp cv2) ct =
kuncar@51374
   468
    (cv1 ct
kuncar@51374
   469
      handle THM _ => cv2 ct
kuncar@51374
   470
        | CTERM _ => cv2 ct
kuncar@51374
   471
        | TERM _ => cv2 ct
kuncar@51374
   472
        | TYPE _ => cv2 ct);
kuncar@51374
   473
  
kuncar@51374
   474
  fun first_imp cvs = fold_rev (curry op else_imp) cvs no_imp
kuncar@51374
   475
  
kuncar@51374
   476
  fun rewr_imp rule ct = 
kuncar@51374
   477
    let
wenzelm@59586
   478
      val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
kuncar@51374
   479
      val lhs_rule = get_lhs rule1;
kuncar@51374
   480
      val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1;
kuncar@51374
   481
      val lhs_ct = Thm.dest_fun ct
kuncar@51374
   482
    in
kuncar@51374
   483
        Thm.instantiate (Thm.match (lhs_rule, lhs_ct)) rule2
kuncar@51374
   484
          handle Pattern.MATCH => raise CTERM ("rewr_imp", [lhs_rule, lhs_ct])
kuncar@51374
   485
   end
kuncar@51374
   486
  
kuncar@51374
   487
  fun rewrs_imp rules = first_imp (map rewr_imp rules)
kuncar@51374
   488
in
kuncar@54335
   489
kuncar@60222
   490
  fun gen_merge_transfer_relations quotients ctxt ctm =
kuncar@51374
   491
    let
kuncar@51374
   492
      val ctm = Thm.dest_arg ctm
wenzelm@59582
   493
      val tm = Thm.term_of ctm
kuncar@51374
   494
      val rel = (hd o get_args 2) tm
kuncar@51374
   495
  
kuncar@51374
   496
      fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
kuncar@51374
   497
        | same_constants _ _  = false
kuncar@51374
   498
      
kuncar@51374
   499
      fun prove_extra_assms ctxt ctm distr_rule =
kuncar@51374
   500
        let
wenzelm@59582
   501
          fun prove_assm assm = try (Goal.prove ctxt [] [] (Thm.term_of assm))
wenzelm@59498
   502
            (fn _ => SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (Transfer.get_transfer_raw ctxt))) 1)
kuncar@51374
   503
  
kuncar@51374
   504
          fun is_POS_or_NEG ctm =
wenzelm@59582
   505
            case (head_of o Thm.term_of o Thm.dest_arg) ctm of
kuncar@51374
   506
              Const (@{const_name POS}, _) => true
kuncar@51374
   507
              | Const (@{const_name NEG}, _) => true
kuncar@51374
   508
              | _ => false
kuncar@51374
   509
  
kuncar@51374
   510
          val inst_distr_rule = rewr_imp distr_rule ctm
kuncar@51374
   511
          val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule)
kuncar@51374
   512
          val proved_assms = map_interrupt prove_assm extra_assms
kuncar@51374
   513
        in
kuncar@51374
   514
          Option.map (curry op OF inst_distr_rule) proved_assms
kuncar@51374
   515
        end
kuncar@51374
   516
        handle CTERM _ => NONE
kuncar@51374
   517
  
kuncar@51374
   518
      fun cannot_merge_error_msg () = Pretty.block
kuncar@51374
   519
         [Pretty.str "Rewriting (merging) of this term has failed:",
kuncar@51374
   520
          Pretty.brk 1,
kuncar@51374
   521
          Syntax.pretty_term ctxt rel]
kuncar@51374
   522
  
kuncar@51374
   523
    in
kuncar@51374
   524
      case get_args 2 rel of
kuncar@51374
   525
          [Const (@{const_name "HOL.eq"}, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
kuncar@51374
   526
          | [_, Const (@{const_name "HOL.eq"}, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
kuncar@51374
   527
          | [_, trans_rel] =>
kuncar@51374
   528
            let
kuncar@51374
   529
              val (rty', qty) = (relation_types o fastype_of) trans_rel
kuncar@51374
   530
            in
kuncar@55454
   531
              if same_type_constrs (rty', qty) then
kuncar@51374
   532
                let
kuncar@55454
   533
                  val distr_rules = get_rel_distr_rules ctxt ((fst o dest_Type) rty') (head_of tm)
kuncar@51374
   534
                  val distr_rule = get_first (prove_extra_assms ctxt ctm) distr_rules
kuncar@51374
   535
                in
kuncar@51374
   536
                  case distr_rule of
kuncar@51374
   537
                    NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
kuncar@60222
   538
                    | SOME distr_rule =>  (map (gen_merge_transfer_relations quotients ctxt) 
kuncar@60222
   539
                                            (cprems_of distr_rule)) 
kuncar@51374
   540
                      MRSL distr_rule
kuncar@51374
   541
                end
kuncar@51374
   542
              else
kuncar@51374
   543
                let 
kuncar@60222
   544
                  val pcrel_def = get_pcrel_def quotients ctxt ((fst o dest_Type) qty)
wenzelm@59582
   545
                  val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def
kuncar@51374
   546
                in
kuncar@51374
   547
                  if same_constants pcrel_const (head_of trans_rel) then
kuncar@51374
   548
                    let
kuncar@51374
   549
                      val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
kuncar@51374
   550
                      val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
kuncar@60222
   551
                      val result = (map (gen_merge_transfer_relations quotients ctxt) 
kuncar@60222
   552
                        (cprems_of distr_rule)) MRSL distr_rule
kuncar@51374
   553
                      val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
kuncar@51374
   554
                    in  
kuncar@51374
   555
                      Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv 
kuncar@51374
   556
                        (Conv.arg_conv (Conv.arg_conv fold_pcr_rel)) fold_pcr_rel)) result
kuncar@51374
   557
                    end
kuncar@51374
   558
                  else
kuncar@51374
   559
                    raise MERGE_TRANSFER_REL (Pretty.str "Non-parametric correspondence relation used.")
kuncar@51374
   560
                end
kuncar@51374
   561
            end
kuncar@51374
   562
    end
kuncar@51374
   563
    handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
kuncar@60222
   564
kuncar@60222
   565
  (*
kuncar@60222
   566
    ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer 
kuncar@60222
   567
    relation for t and T is a transfer relation between t and f, which consists only from
kuncar@60222
   568
    parametrized transfer relations (i.e., pcr_?) and equalities op=. POS or NEG encodes
kuncar@60222
   569
    co-variance or contra-variance.
kuncar@60222
   570
    
kuncar@60222
   571
    The function merges par_R OO T using definitions of parametrized correspondence relations
kuncar@60222
   572
    (e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T).
kuncar@60222
   573
  *)
kuncar@60222
   574
kuncar@60222
   575
  fun merge_transfer_relations ctxt ctm = gen_merge_transfer_relations 
kuncar@60222
   576
    (Lifting_Info.get_quotients ctxt) ctxt ctm
kuncar@51374
   577
end
kuncar@51374
   578
kuncar@60222
   579
fun gen_parametrize_transfer_rule quotients ctxt thm =
kuncar@51374
   580
  let
kuncar@51374
   581
    fun parametrize_relation_conv ctm =
kuncar@51374
   582
      let
wenzelm@59582
   583
        val (rty, qty) = (relation_types o fastype_of) (Thm.term_of ctm)
kuncar@51374
   584
      in
kuncar@55454
   585
        if same_type_constrs (rty, qty) then
kuncar@55454
   586
          if forall op= (Targs rty ~~ Targs qty) then
kuncar@55454
   587
            Conv.all_conv ctm
kuncar@55454
   588
          else
kuncar@55454
   589
            all_args_conv parametrize_relation_conv ctm
kuncar@55454
   590
        else
kuncar@55454
   591
          if is_Type qty then
kuncar@55454
   592
            let
kuncar@55454
   593
              val q = (fst o dest_Type) qty
kuncar@55454
   594
            in
kuncar@55454
   595
              let
kuncar@60222
   596
                val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty)
kuncar@60222
   597
                val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) 
kuncar@55454
   598
                  else (Targs rty', Targs rtyq)
kuncar@55454
   599
              in
kuncar@55454
   600
                if forall op= (rty's ~~ rtyqs) then
kuncar@55454
   601
                  let
kuncar@60222
   602
                    val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq quotients ctxt q)
kuncar@55454
   603
                  in      
kuncar@55454
   604
                    Conv.rewr_conv pcr_cr_eq ctm
kuncar@55454
   605
                  end
kuncar@55454
   606
                  handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm
kuncar@55454
   607
                else
kuncar@60222
   608
                  if has_pcrel_info quotients q then
kuncar@55455
   609
                    let 
kuncar@60222
   610
                      val pcrel_def = Thm.symmetric (get_pcrel_def quotients ctxt q)
kuncar@55455
   611
                    in
kuncar@55455
   612
                      (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
kuncar@55455
   613
                    end
kuncar@55455
   614
                  else Conv.arg1_conv (all_args_conv parametrize_relation_conv) ctm
kuncar@55454
   615
              end  
kuncar@55454
   616
            end
kuncar@55454
   617
          else Conv.all_conv ctm
kuncar@51374
   618
      end
kuncar@51374
   619
    in
kuncar@51374
   620
      Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
kuncar@51374
   621
    end
kuncar@60222
   622
kuncar@60222
   623
(*
kuncar@60222
   624
  It replaces cr_T by pcr_T op= in the transfer relation. For composed
kuncar@60222
   625
  abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
kuncar@60222
   626
  correspondce relation does not exist, the original relation is kept.
kuncar@60222
   627
kuncar@60222
   628
  thm - a transfer rule
kuncar@60222
   629
*)
kuncar@60222
   630
kuncar@60222
   631
fun parametrize_transfer_rule ctxt thm = 
kuncar@60222
   632
  gen_parametrize_transfer_rule (Lifting_Info.get_quotients ctxt) ctxt thm
kuncar@60222
   633
kuncar@53651
   634
end