1(* Title: HOL/Types_To_Sets/internalize_sort.ML 2 Author: Ond��ej Kun��ar, TU M��nchen 3 4A derived rule (by using Thm.unconstrainT) that internalizes 5type class annotations. 6*) 7 8 9(* 10 \<phi>['a::{c_1, ..., c_n} / 'a] 11--------------------------------------------------------------------- 12 class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a] 13 14where class.c is the locale predicate associated with type class c and 15ops are operations associated with type class c. For example: 16If c = semigroup_add, then ops = op-, op+, 0, uminus. 17If c = finite, then ops = TYPE('a::type). 18*) 19 20signature INTERNALIZE_SORT = 21sig 22 val internalize_sort: ctyp -> thm -> typ * thm 23 val internalize_sort_attr: typ -> attribute 24end; 25 26structure Internalize_Sort : INTERNALIZE_SORT = 27struct 28 29fun internalize_sort ctvar thm = 30 let 31 val thy = Thm.theory_of_thm thm; 32 val tvar = Thm.typ_of ctvar; 33 34 val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm); 35 36 fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *) 37 fun reduce_to_non_proper_sort (TVar (name, sort)) = 38 TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort))) 39 | reduce_to_non_proper_sort _ = error "not supported"; 40 41 val data = map #1 (#outer_constraints ucontext) ~~ #constraints ucontext; 42 43 val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' 44 then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data 45 |> the_default tvar; 46 47 fun localify class = Class.rules thy class |> snd |> Thm.transfer thy; 48 49 fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class); 50 51 val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar' 52 then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class) 53 else discharge_of_class ren_tvar class) data; 54 in 55 (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes) 56 end; 57 58val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v 59 | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t)); 60 61fun internalize_sort_attr tvar = 62 Thm.rule_attribute [] (fn context => fn thm => 63 (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm))); 64 65val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>internalize_sort\<close> 66 (tvar >> internalize_sort_attr) "internalize a sort")); 67 68end; 69