author | immler |
Tue, 12 Jun 2018 19:32:42 +0200 | |
changeset 68430 | b0eb6a91924d |
parent 68429 | 38961724a017 |
child 68433 | f396f5490a8c |
permissions | -rw-r--r-- |
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 | 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 | 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 | 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 |