1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Typerep.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,107 @@
     1.4 +(*  Title:      HOL/Library/RType.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Reflecting Pure types into HOL *}
    1.10 +
    1.11 +theory Typerep
    1.12 +imports Plain List Code_Message
    1.13 +begin
    1.14 +
    1.15 +datatype typerep = Typerep message_string "typerep list"
    1.16 +
    1.17 +class typerep =
    1.18 +  fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
    1.19 +begin
    1.20 +
    1.21 +definition
    1.22 +  typerep_of :: "'a \<Rightarrow> typerep"
    1.23 +where
    1.24 +  [simp]: "typerep_of x = typerep TYPE('a)"
    1.25 +
    1.26 +end
    1.27 +
    1.28 +setup {*
    1.29 +let
    1.30 +  fun typerep_tr (*"_TYPEREP"*) [ty] =
    1.31 +        Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
    1.32 +          (Lexicon.const "itself" $ ty))
    1.33 +    | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    1.34 +  fun typerep_tr' show_sorts (*"typerep"*)
    1.35 +          (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
    1.36 +        Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts)
    1.37 +    | typerep_tr' _ T ts = raise Match;
    1.38 +in
    1.39 +  Sign.add_syntax_i
    1.40 +    [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
    1.41 +  #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
    1.42 +  #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
    1.43 +end
    1.44 +*}
    1.45 +
    1.46 +ML {*
    1.47 +structure Typerep =
    1.48 +struct
    1.49 +
    1.50 +fun mk f (Type (tyco, tys)) =
    1.51 +      @{term Typerep} $ Message_String.mk tyco
    1.52 +        $ HOLogic.mk_list @{typ typerep} (map (mk f) tys)
    1.53 +  | mk f (TFree v) =
    1.54 +      f v;
    1.55 +
    1.56 +fun typerep ty =
    1.57 +  Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    1.58 +    $ Logic.mk_type ty;
    1.59 +
    1.60 +fun add_def tyco thy =
    1.61 +  let
    1.62 +    val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
    1.63 +    val vs = Name.names Name.context "'a" sorts;
    1.64 +    val ty = Type (tyco, map TFree vs);
    1.65 +    val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    1.66 +      $ Free ("T", Term.itselfT ty);
    1.67 +    val rhs = mk (typerep o TFree) ty;
    1.68 +    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.69 +  in
    1.70 +    thy
    1.71 +    |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
    1.72 +    |> `(fn lthy => Syntax.check_term lthy eq)
    1.73 +    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
    1.74 +    |> snd
    1.75 +    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.76 +    |> LocalTheory.exit_global
    1.77 +  end;
    1.78 +
    1.79 +fun perhaps_add_def tyco thy =
    1.80 +  let
    1.81 +    val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}
    1.82 +  in if inst then thy else add_def tyco thy end;
    1.83 +
    1.84 +end;
    1.85 +*}
    1.86 +
    1.87 +setup {*
    1.88 +  Typerep.add_def @{type_name prop}
    1.89 +  #> Typerep.add_def @{type_name fun}
    1.90 +  #> Typerep.add_def @{type_name itself}
    1.91 +  #> Typerep.add_def @{type_name bool}
    1.92 +  #> TypedefPackage.interpretation Typerep.perhaps_add_def
    1.93 +*}
    1.94 +
    1.95 +lemma [code]:
    1.96 +  "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
    1.97 +     \<and> list_all2 eq_class.eq tys1 tys2"
    1.98 +  by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
    1.99 +
   1.100 +code_type typerep
   1.101 +  (SML "Term.typ")
   1.102 +
   1.103 +code_const Typerep
   1.104 +  (SML "Term.Type/ (_, _)")
   1.105 +
   1.106 +code_reserved SML Term
   1.107 +
   1.108 +hide (open) const typerep Typerep
   1.109 +
   1.110 +end