author  haftmann 
Thu, 25 Sep 2008 09:28:03 +0200  
changeset 28346  b8390cd56b8f 
parent 28335  25326092cf9a 
child 28394  b9c8e3a12a98 
permissions  rwrr 
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 

28228  9 
imports Plain "~~/src/HOL/List" "~~/src/HOL/Library/Code_Message" 
26168  10 
begin 
11 

28335  12 
datatype typerep = Typerep message_string "typerep list" 
26168  13 

28335  14 
class typerep = 
15 
fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep" 

26168  16 
begin 
17 

18 
definition 

28335  19 
typerep_of :: "'a \<Rightarrow> typerep" 
26168  20 
where 
28335  21 
[simp]: "typerep_of x = typerep TYPE('a)" 
26168  22 

23 
end 

24 

25 
setup {* 

26 
let 

28335  27 
fun typerep_tr (*"_TYPEREP"*) [ty] = 
28 
Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ 

26168  29 
(Lexicon.const "itself" $ ty)) 
28335  30 
 typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); 
31 
fun typerep_tr' show_sorts (*"typerep"*) 

26168  32 
(Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) = 
28335  33 
Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts) 
34 
 typerep_tr' _ T ts = raise Match; 

26168  35 
in 
36 
Sign.add_syntax_i 

28335  37 
[("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")] 
38 
#> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], []) 

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

26168  40 
end 
41 
*} 

42 

43 
ML {* 

28335  44 
structure Typerep = 
26168  45 
struct 
46 

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

28335  48 
@{term Typerep} $ Message_String.mk tyco 
49 
$ HOLogic.mk_list @{typ typerep} (map (mk f) tys) 

26168  50 
 mk f (TFree v) = 
51 
f v; 

52 

28335  53 
fun typerep ty = 
54 
Const (@{const_name typerep}, Term.itselfT ty > @{typ typerep}) 

26168  55 
$ Logic.mk_type ty; 
56 

57 
fun add_def tyco thy = 

58 
let 

28335  59 
val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; 
26168  60 
val vs = Name.names Name.context "'a" sorts; 
61 
val ty = Type (tyco, map TFree vs); 

28335  62 
val lhs = Const (@{const_name typerep}, Term.itselfT ty > @{typ typerep}) 
26168  63 
$ Free ("T", Term.itselfT ty); 
28335  64 
val rhs = mk (typerep o TFree) ty; 
26168  65 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 
66 
in 

67 
thy 

28335  68 
> TheoryTarget.instantiation ([tyco], vs, @{sort typerep}) 
26168  69 
> `(fn lthy => Syntax.check_term lthy eq) 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

70 
> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) 
26168  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 

28335  79 
val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep} 
26168  80 
in if inst then thy else add_def tyco thy end; 
81 

82 
end; 

83 
*} 

84 

85 
setup {* 

28335  86 
Typerep.add_def @{type_name prop} 
87 
#> Typerep.add_def @{type_name fun} 

88 
#> Typerep.add_def @{type_name itself} 

89 
#> Typerep.add_def @{type_name bool} 

90 
#> TypedefPackage.interpretation Typerep.perhaps_add_def 

26168  91 
*} 
92 

93 
lemma [code func]: 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28335
diff
changeset

94 
"eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2 
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28335
diff
changeset

95 
\<and> list_all2 eq_class.eq tys1 tys2" 
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28335
diff
changeset

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

28335  98 
code_type typerep 
26168  99 
(SML "Term.typ") 
100 

28335  101 
code_const Typerep 
26168  102 
(SML "Term.Type/ (_, _)") 
103 

104 
code_reserved SML Term 

105 

28335  106 
hide (open) const typerep Typerep 
26168  107 

108 
end 