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