src/HOL/Typerep.thy
author haftmann
Wed May 13 18:41:39 2009 +0200 (2009-05-13)
changeset 31137 cd3aafc1c631
parent 31048 ac146fc38b51
child 31205 98370b26c2ce
permissions -rw-r--r--
tuned construction of typerep instances
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Reflecting Pure types into HOL *}
     4 
     5 theory Typerep
     6 imports Plain String
     7 begin
     8 
     9 datatype typerep = Typerep message_string "typerep list"
    10 
    11 class typerep =
    12   fixes typerep :: "'a itself \<Rightarrow> typerep"
    13 begin
    14 
    15 definition typerep_of :: "'a \<Rightarrow> typerep" where
    16   [simp]: "typerep_of x = typerep TYPE('a)"
    17 
    18 end
    19 
    20 setup {*
    21 let
    22   fun typerep_tr (*"_TYPEREP"*) [ty] =
    23         Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
    24           (Lexicon.const "itself" $ ty))
    25     | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    26   fun typerep_tr' show_sorts (*"typerep"*)
    27           (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
    28         Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts)
    29     | typerep_tr' _ T ts = raise Match;
    30 in
    31   Sign.add_syntax_i
    32     [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
    33   #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
    34   #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
    35 end
    36 *}
    37 
    38 setup {*
    39 let
    40 
    41 fun add_typerep tyco thy =
    42   let
    43     val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
    44     val vs = Name.names Name.context "'a" sorts;
    45     val ty = Type (tyco, map TFree vs);
    46     val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    47       $ Free ("T", Term.itselfT ty);
    48     val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
    49       $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
    50     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    51   in
    52     thy
    53     |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
    54     |> `(fn lthy => Syntax.check_term lthy eq)
    55     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    56     |> snd
    57     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    58   end;
    59 
    60 fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
    61   andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
    62   then add_typerep tyco thy else thy;
    63 
    64 in
    65 
    66 add_typerep @{type_name fun}
    67 #> TypedefPackage.interpretation ensure_typerep
    68 #> Code.type_interpretation (ensure_typerep o fst)
    69 
    70 end
    71 *}
    72 
    73 lemma [code]:
    74   "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
    75      \<and> list_all2 eq_class.eq tys1 tys2"
    76   by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
    77 
    78 code_type typerep
    79   (Eval "Term.typ")
    80 
    81 code_const Typerep
    82   (Eval "Term.Type/ (_, _)")
    83 
    84 code_reserved Eval Term
    85 
    86 hide (open) const typerep Typerep
    87 
    88 end