author  haftmann 
Wed, 06 May 2009 16:01:06 +0200  
changeset 31048  ac146fc38b51 
parent 31031  cbec39ebf8f2 
child 31137  cd3aafc1c631 
permissions  rwrr 
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

1 
(* Author: Florian Haftmann, TU Muenchen *) 
26168  2 

3 
header {* Reflecting Pure types into HOL *} 

4 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

5 
theory Typerep 
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

6 
imports Plain String 
26168  7 
begin 
8 

28335  9 
datatype typerep = Typerep message_string "typerep list" 
26168  10 

28335  11 
class typerep = 
31031  12 
fixes typerep :: "'a itself \<Rightarrow> typerep" 
26168  13 
begin 
14 

29574  15 
definition typerep_of :: "'a \<Rightarrow> typerep" where 
28335  16 
[simp]: "typerep_of x = typerep TYPE('a)" 
26168  17 

18 
end 

19 

20 
setup {* 

21 
let 

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

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

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

26168  30 
in 
31 
Sign.add_syntax_i 

28335  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')] 

26168  35 
end 
36 
*} 

37 

38 
ML {* 

28335  39 
structure Typerep = 
26168  40 
struct 
41 

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

31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

43 
@{term Typerep} $ HOLogic.mk_message_string tyco 
28335  44 
$ HOLogic.mk_list @{typ typerep} (map (mk f) tys) 
26168  45 
 mk f (TFree v) = 
46 
f v; 

47 

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

26168  50 
$ Logic.mk_type ty; 
51 

52 
fun add_def tyco thy = 

53 
let 

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

28335  57 
val lhs = Const (@{const_name typerep}, Term.itselfT ty > @{typ typerep}) 
26168  58 
$ Free ("T", Term.itselfT ty); 
28335  59 
val rhs = mk (typerep o TFree) ty; 
26168  60 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 
61 
in 

62 
thy 

28335  63 
> TheoryTarget.instantiation ([tyco], vs, @{sort typerep}) 
26168  64 
> `(fn lthy => Syntax.check_term lthy eq) 
28965  65 
> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) 
26168  66 
> snd 
67 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 

28394  68 
> LocalTheory.exit_global 
26168  69 
end; 
70 

71 
fun perhaps_add_def tyco thy = 

72 
let 

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

76 
end; 

77 
*} 

78 

79 
setup {* 

31031  80 
Typerep.add_def @{type_name fun} 
28335  81 
#> Typerep.add_def @{type_name itself} 
82 
#> Typerep.add_def @{type_name bool} 

83 
#> TypedefPackage.interpretation Typerep.perhaps_add_def 

26168  84 
*} 
85 

28562  86 
lemma [code]: 
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28335
diff
changeset

87 
"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

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

89 
by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric]) 
26168  90 

28335  91 
code_type typerep 
31031  92 
(Eval "Term.typ") 
26168  93 

28335  94 
code_const Typerep 
31031  95 
(Eval "Term.Type/ (_, _)") 
26168  96 

31031  97 
code_reserved Eval Term 
26168  98 

28335  99 
hide (open) const typerep Typerep 
26168  100 

101 
end 