26168

1 
(* Title: HOL/Library/RType.thy


2 
ID: $Id$


3 
Author: Florian Haftmann, TU Muenchen


4 
*)


5 


6 
header {* Reflecting Pure types into HOL *}


7 


8 
theory RType


9 
imports Main Code_Message


10 
begin


11 


12 
datatype "rtype" = RType message_string "rtype list"


13 


14 
class rtype =


15 
fixes rtype :: "'a\<Colon>{} itself \<Rightarrow> rtype"


16 
begin


17 


18 
definition


19 
rtype_of :: "'a \<Rightarrow> rtype"


20 
where


21 
[simp]: "rtype_of x = rtype TYPE('a)"


22 


23 
end


24 


25 
setup {*


26 
let


27 
fun rtype_tr (*"_RTYPE"*) [ty] =


28 
Lexicon.const @{const_syntax rtype} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $


29 
(Lexicon.const "itself" $ ty))


30 
 rtype_tr (*"_RTYPE"*) ts = raise TERM ("rtype_tr", ts);


31 
fun rtype_tr' show_sorts (*"rtype"*)


32 
(Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =


33 
Term.list_comb (Lexicon.const "_RTYPE" $ Syntax.term_of_typ show_sorts T, ts)


34 
 rtype_tr' _ T ts = raise Match;


35 
in


36 
Sign.add_syntax_i


37 
[("_RTYPE", SimpleSyntax.read_typ "type => logic", Delimfix "(1RTYPE/(1'(_')))")]


38 
#> Sign.add_trfuns ([], [("_RTYPE", rtype_tr)], [], [])


39 
#> Sign.add_trfunsT [(@{const_syntax rtype}, rtype_tr')]


40 
end


41 
*}


42 


43 
ML {*


44 
structure RType =


45 
struct


46 


47 
fun mk f (Type (tyco, tys)) =


48 
@{term RType} $ Message_String.mk tyco


49 
$ HOLogic.mk_list @{typ rtype} (map (mk f) tys)


50 
 mk f (TFree v) =


51 
f v;


52 


53 
fun rtype ty =


54 
Const (@{const_name rtype}, Term.itselfT ty > @{typ rtype})


55 
$ Logic.mk_type ty;


56 


57 
fun add_def tyco thy =


58 
let


59 
val sorts = replicate (Sign.arity_number thy tyco) @{sort rtype};


60 
val vs = Name.names Name.context "'a" sorts;


61 
val ty = Type (tyco, map TFree vs);


62 
val lhs = Const (@{const_name rtype}, Term.itselfT ty > @{typ rtype})


63 
$ Free ("T", Term.itselfT ty);


64 
val rhs = mk (rtype o TFree) ty;


65 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));


66 
in


67 
thy


68 
> TheoryTarget.instantiation ([tyco], vs, @{sort rtype})


69 
> `(fn lthy => Syntax.check_term lthy eq)


70 
> (fn eq => Specification.definition (NONE, (("", []), eq)))


71 
> snd


72 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))


73 
> LocalTheory.exit


74 
> ProofContext.theory_of


75 
end;


76 


77 
fun perhaps_add_def tyco thy =


78 
let


79 
val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort rtype}


80 
in if inst then thy else add_def tyco thy end;


81 


82 
end;


83 
*}


84 


85 
setup {*


86 
RType.add_def @{type_name prop}


87 
#> RType.add_def @{type_name fun}


88 
#> RType.add_def @{type_name itself}


89 
#> RType.add_def @{type_name bool}


90 
#> RType.add_def @{type_name set}


91 
#> TypedefPackage.interpretation RType.perhaps_add_def


92 
*}


93 


94 
lemma [code func]:


95 
"RType tyco1 tys1 = RType tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2


96 
\<and> list_all2 (op =) tys1 tys2"


97 
by (auto simp add: list_all2_eq [symmetric])


98 


99 
code_type rtype


100 
(SML "Term.typ")


101 


102 
code_const RType


103 
(SML "Term.Type/ (_, _)")


104 


105 
code_reserved SML Term


106 


107 
hide (open) const rtype RType


108 


109 
end
