author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 68438 | f04d0e75e439 |
child 69688 | 33843320448f |
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 |
68434 | 9 |
val unoverload_type: Context.generic -> indexname list -> thm -> thm |
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 |
|
68429
38961724a017
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents:
68428
diff
changeset
|
16 |
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
|
17 |
let |
38961724a017
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents:
68428
diff
changeset
|
18 |
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
|
19 |
val class_premise = case Thm.prems_of thm' of t::_=> t | [] => |
68430 | 20 |
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
|
21 |
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
|
22 |
val tvar = case class_vars of [x] => TVar x | _ => |
68430 | 23 |
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
|
24 |
in |
38961724a017
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents:
68428
diff
changeset
|
25 |
(tvar, thm') |
38961724a017
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents:
68428
diff
changeset
|
26 |
end |
38961724a017
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents:
68428
diff
changeset
|
27 |
|
68437 | 28 |
fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these |
29 |
||
30 |
fun params_of_super_classes thy class = |
|
31 |
Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy) |
|
32 |
||
33 |
fun params_of_sort thy sort = maps (params_of_super_classes thy) sort |
|
34 |
||
35 |
fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty |
|
36 |
||
68434 | 37 |
fun unoverload_single_type context x thm = |
68428
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
38 |
let |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
39 |
val tvars = Term.add_tvars (Thm.prop_of thm) [] |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
40 |
val thy = Context.theory_of context |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
41 |
in |
68433 | 42 |
case find_first (fn (y, _) => x = y) tvars of NONE => |
68438 | 43 |
raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (x,[])], []) |
68428
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
44 |
| SOME (x as (_, sort)) => |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
45 |
let |
68429
38961724a017
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
immler
parents:
68428
diff
changeset
|
46 |
val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm |
68437 | 47 |
val consts = params_of_sort thy sort |
48 |
|> map (apsnd (subst_TFree "'a" tvar) #> Const #> Thm.global_cterm_of thy) |
|
68428
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
49 |
in |
68437 | 50 |
fold Unoverloading.unoverload consts thm' |
68436 | 51 |
|> Raw_Simplifier.norm_hhf (Context.proof_of context) |
68428
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
52 |
end |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
53 |
end |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset
|
54 |
|
68434 | 55 |
fun unoverload_type context xs = fold (unoverload_single_type context) xs |
56 |
||
57 |
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
|
58 |
|
69597 | 59 |
val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>unoverload_type\<close> |
68435 | 60 |
(Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr) |
61 |
"internalize and unoverload type class parameters")) |
|
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 |
end |