src/HOL/Typerep.thy
author haftmann
Wed May 06 16:01:06 2009 +0200 (2009-05-06)
changeset 31048 ac146fc38b51
parent 31031 cbec39ebf8f2
child 31137 cd3aafc1c631
permissions -rw-r--r--
refined HOL string theories and corresponding ML fragments
     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 ML {*
    39 structure Typerep =
    40 struct
    41 
    42 fun mk f (Type (tyco, tys)) =
    43       @{term Typerep} $ HOLogic.mk_message_string tyco
    44         $ HOLogic.mk_list @{typ typerep} (map (mk f) tys)
    45   | mk f (TFree v) =
    46       f v;
    47 
    48 fun typerep ty =
    49   Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    50     $ Logic.mk_type ty;
    51 
    52 fun add_def tyco thy =
    53   let
    54     val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
    55     val vs = Name.names Name.context "'a" sorts;
    56     val ty = Type (tyco, map TFree vs);
    57     val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    58       $ Free ("T", Term.itselfT ty);
    59     val rhs = mk (typerep o TFree) ty;
    60     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    61   in
    62     thy
    63     |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
    64     |> `(fn lthy => Syntax.check_term lthy eq)
    65     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    66     |> snd
    67     |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    68     |> LocalTheory.exit_global
    69   end;
    70 
    71 fun perhaps_add_def tyco thy =
    72   let
    73     val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}
    74   in if inst then thy else add_def tyco thy end;
    75 
    76 end;
    77 *}
    78 
    79 setup {*
    80   Typerep.add_def @{type_name fun}
    81   #> Typerep.add_def @{type_name itself}
    82   #> Typerep.add_def @{type_name bool}
    83   #> TypedefPackage.interpretation Typerep.perhaps_add_def
    84 *}
    85 
    86 lemma [code]:
    87   "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
    88      \<and> list_all2 eq_class.eq tys1 tys2"
    89   by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
    90 
    91 code_type typerep
    92   (Eval "Term.typ")
    93 
    94 code_const Typerep
    95   (Eval "Term.Type/ (_, _)")
    96 
    97 code_reserved Eval Term
    98 
    99 hide (open) const typerep Typerep
   100 
   101 end