a derived rule combining unoverload and internalize_sort
authorimmler
Tue Jun 12 16:21:52 2018 +0200 (11 months ago)
changeset 6842846beee72fb66
parent 68427 f75d765a281f
child 68429 38961724a017
child 68444 ff61cbfb3f2d
a derived rule combining unoverload and internalize_sort
src/HOL/Types_To_Sets/Examples/T2_Spaces.thy
src/HOL/Types_To_Sets/Types_To_Sets.thy
src/HOL/Types_To_Sets/unoverload_type.ML
     1.1 --- a/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy	Tue Jun 12 11:18:35 2018 +0100
     1.2 +++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy	Tue Jun 12 16:21:52 2018 +0200
     1.3 @@ -120,6 +120,9 @@
     1.4       for the original relativization algorithm.\<close>
     1.5  thm dictionary_second_step
     1.6  
     1.7 +text \<open>Alternative construction using \<open>unoverload_type\<close>
     1.8 +  (This does not require fiddling with \<open>Sign.add_const_constraint\<close>).\<close>
     1.9 +lemmas dictionary_second_step' = dictionary_first_step[unoverload_type 'a]
    1.10  
    1.11  text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
    1.12  lemma compact_imp_closed_set_based:
     2.1 --- a/src/HOL/Types_To_Sets/Types_To_Sets.thy	Tue Jun 12 11:18:35 2018 +0100
     2.2 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Tue Jun 12 16:21:52 2018 +0200
     2.3 @@ -24,4 +24,8 @@
     2.4  text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
     2.5  ML_file "internalize_sort.ML"
     2.6  
     2.7 +text\<open>The following file provides some automation to unoverload and internalize the parameters o
     2.8 +  the sort constraints of a type variable.\<close>
     2.9 +ML_file \<open>unoverload_type.ML\<close>
    2.10 +
    2.11  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 16:21:52 2018 +0200
     3.3 @@ -0,0 +1,56 @@
     3.4 +(*  Title:      HOL/Types_To_Sets/unoverload_type.ML
     3.5 +    Author:     Fabian Immler, TU M√ľnchen
     3.6 +
     3.7 +Internalize sorts and unoverload parameters of a type variable.
     3.8 +*)
     3.9 +
    3.10 +signature UNOVERLOAD_TYPE =
    3.11 +sig
    3.12 +  val unoverload_type: Context.generic -> string -> thm -> thm
    3.13 +  val unoverload_type_attr: string -> attribute
    3.14 +end;
    3.15 +
    3.16 +structure Unoverload_Type : UNOVERLOAD_TYPE =
    3.17 +struct
    3.18 +
    3.19 +fun those [] = []
    3.20 +  | those (NONE::xs) = those xs
    3.21 +  | those (SOME x::xs) = x::those xs
    3.22 +
    3.23 +fun params_of_sort context sort =
    3.24 +  let
    3.25 +    val algebra = Sign.classes_of (Context.theory_of context)
    3.26 +    val params = List.concat (map (Sorts.super_classes algebra) sort) |>
    3.27 +      map (try (Axclass.get_info (Context.theory_of context))) |>
    3.28 +      those |>
    3.29 +      map #params |>
    3.30 +      List.concat
    3.31 +  in params end
    3.32 +
    3.33 +fun unoverload_type context s thm =
    3.34 +  let
    3.35 +    val tvars = Term.add_tvars (Thm.prop_of thm) []
    3.36 +    val thy = Context.theory_of context
    3.37 +  in
    3.38 +  case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
    3.39 +    raise THM ("unoverload_internalize_deps: type variable ("^s^") not in theorem", 0, [thm])
    3.40 +  | SOME (x as (_, sort)) =>
    3.41 +    let
    3.42 +      val (tvar, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
    3.43 +      val consts = params_of_sort context sort |>
    3.44 +        map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
    3.45 +    in
    3.46 +      fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
    3.47 +    end
    3.48 +  end
    3.49 +
    3.50 +val tyN = (Args.context -- Args.typ) >>
    3.51 +  (fn (_, TFree (n, _)) => n
    3.52 +  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
    3.53 +
    3.54 +fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
    3.55 +
    3.56 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
    3.57 +  (tyN >> unoverload_type_attr) "internalize a sort"))
    3.58 +
    3.59 +end
    3.60 \ No newline at end of file