src/HOL/Types_To_Sets/unoverload_type.ML
author immler
Wed, 13 Jun 2018 09:26:04 +0200
changeset 68435 2a2ef4552aaf
parent 68434 c6a38342376e
child 68436 1b3edf5da4e4
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
68434
c6a38342376e allow for a list of vars
immler
parents: 68433
diff changeset
     9
  val unoverload_type: Context.generic -> indexname list -> thm -> thm
c6a38342376e allow for a list of vars
immler
parents: 68433
diff changeset
    10
  val unoverload_type_attr: indexname list -> attribute
68428
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
68434
c6a38342376e allow for a list of vars
immler
parents: 68433
diff changeset
    42
fun unoverload_single_type context x thm =
68428
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
68433
f396f5490a8c parse var
immler
parents: 68430
diff changeset
    47
  case find_first (fn (y, _) => x = y) tvars of NONE =>
f396f5490a8c parse var
immler
parents: 68430
diff changeset
    48
    raise THM ("unoverload_type: type variable ("^(@{make_string} x)^") 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
68434
c6a38342376e allow for a list of vars
immler
parents: 68433
diff changeset
    59
fun unoverload_type context xs = fold (unoverload_single_type context) xs
c6a38342376e allow for a list of vars
immler
parents: 68433
diff changeset
    60
c6a38342376e allow for a list of vars
immler
parents: 68433
diff changeset
    61
fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
68428
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
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
68435
immler
parents: 68434
diff changeset
    64
  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr)
immler
parents: 68434
diff changeset
    65
    "internalize and unoverload type class parameters"))
68428
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    66
46beee72fb66 a derived rule combining unoverload and internalize_sort
immler
parents:
diff changeset
    67
end