1(* Title: HOL/Types_To_Sets/unoverload_type.ML 2 Author: Fabian Immler, TU M��nchen 3 4Internalize sorts and unoverload parameters of a type variable. 5*) 6 7signature UNOVERLOAD_TYPE = 8sig 9 val unoverload_type: Context.generic -> indexname list -> thm -> thm 10 val unoverload_type_attr: indexname list -> attribute 11end; 12 13structure Unoverload_Type : UNOVERLOAD_TYPE = 14struct 15 16fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these 17 18fun params_of_super_classes thy class = 19 class::Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy) 20 21fun params_of_sort thy sort = maps (params_of_super_classes thy) sort 22 23fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty 24 25fun unoverload_single_type context tvar thm = 26 let 27 val tvars = Term.add_tvars (Thm.prop_of thm) [] 28 val thy = Context.theory_of context 29 in 30 case find_first (fn (y, _) => tvar = y) tvars of NONE => 31 raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (tvar,[])], []) 32 | SOME (x as (_, sort)) => 33 let 34 val (_, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm 35 val prop' = 36 fold (fn _ => Term.dest_comb #> #2) 37 (replicate (Thm.nprems_of thm' - Thm.nprems_of thm) ()) (Thm.prop_of thm') 38 val (tyenv, _) = Pattern.first_order_match thy ((prop', Thm.prop_of thm)) 39 (Vartab.empty, Vartab.empty) 40 val tyenv_list = tyenv |> Vartab.dest 41 |> map (fn (x, (s, TVar (x', _))) => 42 ((x, s), Thm.ctyp_of (Context.proof_of context) (TVar(x', s)))) 43 val thm'' = Drule.instantiate_normalize (tyenv_list, []) thm' 44 val varify_const = 45 apsnd (subst_TFree "'a" (TVar (tvar, @{sort type}))) #> Const #> Thm.global_cterm_of thy 46 val consts = params_of_sort thy sort 47 |> map varify_const 48 in 49 fold Unoverloading.unoverload consts thm'' 50 |> Raw_Simplifier.norm_hhf (Context.proof_of context) 51 end 52 end 53 54fun unoverload_type context xs = fold (unoverload_single_type context) xs 55 56fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs) 57 58val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>unoverload_type\<close> 59 (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr) 60 "internalize and unoverload type class parameters")) 61 62end