src/HOL/Types_To_Sets/unoverload_type.ML
author immler
Tue, 12 Jun 2018 19:32:42 +0200
changeset 68430 b0eb6a91924d
parent 68429 38961724a017
child 68433 f396f5490a8c
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68428
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     1
(*  Title:      HOL/Types_To_Sets/unoverload_type.ML
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     2
    Author:     Fabian Immler, TU M√ľnchen
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     3
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     4
Internalize sorts and unoverload parameters of a type variable.
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     5
*)
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     6
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     7
signature UNOVERLOAD_TYPE =
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     8
sig
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
     9
  val unoverload_type: Context.generic -> string -> thm -> thm
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    10
  val unoverload_type_attr: string -> attribute
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    11
end;
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    12
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    13
structure Unoverload_Type : UNOVERLOAD_TYPE =
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    14
struct
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    15
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    16
fun those [] = []
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    17
  | those (NONE::xs) = those xs
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    18
  | those (SOME x::xs) = x::those xs
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    19
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    20
fun params_of_sort context sort =
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    21
  let
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    22
    val algebra = Sign.classes_of (Context.theory_of context)
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    23
    val params = List.concat (map (Sorts.super_classes algebra) sort) |>
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    24
      map (try (Axclass.get_info (Context.theory_of context))) |>
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    25
      those |>
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    26
      map #params |>
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    27
      List.concat
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    28
  in params end
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    29
68429
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    30
fun internalize_sort' ctvar thm =
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    31
  let
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    32
    val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    33
    val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
68430
immler
parents: 68429
diff changeset
    34
      raise THM ("internalize_sort': no premise?", 0, [thm'])
68429
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    35
    val class_vars = Term.add_tvars class_premise []
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    36
    val tvar = case class_vars of [x] => TVar x | _ =>
68430
immler
parents: 68429
diff changeset
    37
      raise TERM ("internalize_sort': not one type class variable.", [class_premise])
68429
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    38
  in
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    39
    (tvar, thm')
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    40
  end
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    41
68428
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    42
fun unoverload_type context s thm =
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    43
  let
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    44
    val tvars = Term.add_tvars (Thm.prop_of thm) []
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    45
    val thy = Context.theory_of context
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    46
  in
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    47
  case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
68430
immler
parents: 68429
diff changeset
    48
    raise THM ("unoverload_type: type variable ("^s^") not in theorem", 0, [thm])
68428
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    49
  | SOME (x as (_, sort)) =>
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    50
    let
68429
38961724a017 workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents: 68428
diff changeset
    51
      val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
68428
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    52
      val consts = params_of_sort context sort |>
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    53
        map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    54
    in
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    55
      fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    56
    end
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    57
  end
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    58
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    59
val tyN = (Args.context -- Args.typ) >>
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    60
  (fn (_, TFree (n, _)) => n
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    61
  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    62
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    63
fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    64
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    65
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    66
  (tyN >> unoverload_type_attr) "internalize a sort"))
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    67
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    68
end