author  immler 
Wed, 13 Jun 2018 09:38:07 +0200  
changeset 68436  1b3edf5da4e4 
parent 68435  2a2ef4552aaf 
child 68437  f9b15e7c12bd 
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 
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 

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 

68434  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  47 
case find_first (fn (y, _) => x = y) tvars of NONE => 
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' 
68436  56 
> Raw_Simplifier.norm_hhf (Context.proof_of context) 
68428
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 
end 
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset

59 

68434  60 
fun unoverload_type context xs = fold (unoverload_single_type context) xs 
61 

62 
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

63 

46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
diff
changeset

64 
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type} 
68435  65 
(Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr) 
66 
"internalize and unoverload type class parameters")) 

68428
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 