restructured
authorimmler
Wed Jun 13 10:45:23 2018 +0200 (11 months ago)
changeset 68437f9b15e7c12bd
parent 68436 1b3edf5da4e4
child 68438 f04d0e75e439
restructured
src/HOL/Types_To_Sets/unoverload_type.ML
     1.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 09:38:07 2018 +0200
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed Jun 13 10:45:23 2018 +0200
     1.3 @@ -13,20 +13,6 @@
     1.4  structure Unoverload_Type : UNOVERLOAD_TYPE =
     1.5  struct
     1.6  
     1.7 -fun those [] = []
     1.8 -  | those (NONE::xs) = those xs
     1.9 -  | those (SOME x::xs) = x::those xs
    1.10 -
    1.11 -fun params_of_sort context sort =
    1.12 -  let
    1.13 -    val algebra = Sign.classes_of (Context.theory_of context)
    1.14 -    val params = List.concat (map (Sorts.super_classes algebra) sort) |>
    1.15 -      map (try (Axclass.get_info (Context.theory_of context))) |>
    1.16 -      those |>
    1.17 -      map #params |>
    1.18 -      List.concat
    1.19 -  in params end
    1.20 -
    1.21  fun internalize_sort' ctvar thm =
    1.22    let
    1.23      val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
    1.24 @@ -39,6 +25,15 @@
    1.25      (tvar, thm')
    1.26    end
    1.27  
    1.28 +fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
    1.29 +
    1.30 +fun params_of_super_classes thy class =
    1.31 +  Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
    1.32 +
    1.33 +fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
    1.34 +
    1.35 +fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty
    1.36 +
    1.37  fun unoverload_single_type context x thm =
    1.38    let
    1.39      val tvars = Term.add_tvars (Thm.prop_of thm) []
    1.40 @@ -49,10 +44,10 @@
    1.41    | SOME (x as (_, sort)) =>
    1.42      let
    1.43        val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
    1.44 -      val consts = params_of_sort context sort |>
    1.45 -        map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
    1.46 +      val consts = params_of_sort thy sort
    1.47 +        |> map (apsnd (subst_TFree "'a" tvar) #> Const #> Thm.global_cterm_of thy)
    1.48      in
    1.49 -      fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
    1.50 +      fold Unoverloading.unoverload consts thm'
    1.51        |> Raw_Simplifier.norm_hhf (Context.proof_of context)
    1.52      end
    1.53    end