author  haftmann 
Tue, 19 May 2009 16:54:55 +0200  
changeset 31205  98370b26c2ce 
parent 31137  cd3aafc1c631 
child 31723  f5cafe803b55 
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 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31137
diff
changeset

9 
datatype typerep = Typerep String.literal "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 

31137  38 
setup {* 
39 
let 

26168  40 

31137  41 
fun add_typerep tyco thy = 
26168  42 
let 
28335  43 
val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; 
26168  44 
val vs = Name.names Name.context "'a" sorts; 
45 
val ty = Type (tyco, map TFree vs); 

28335  46 
val lhs = Const (@{const_name typerep}, Term.itselfT ty > @{typ typerep}) 
26168  47 
$ Free ("T", Term.itselfT ty); 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31137
diff
changeset

48 
val rhs = @{term Typerep} $ HOLogic.mk_literal tyco 
31137  49 
$ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs); 
26168  50 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 
51 
in 

52 
thy 

28335  53 
> TheoryTarget.instantiation ([tyco], vs, @{sort typerep}) 
26168  54 
> `(fn lthy => Syntax.check_term lthy eq) 
28965  55 
> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) 
26168  56 
> snd 
31137  57 
> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) 
26168  58 
end; 
59 

31137  60 
fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}) 
61 
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type} 

62 
then add_typerep tyco thy else thy; 

63 

64 
in 

26168  65 

31137  66 
add_typerep @{type_name fun} 
67 
#> TypedefPackage.interpretation ensure_typerep 

68 
#> Code.type_interpretation (ensure_typerep o fst) 

26168  69 

31137  70 
end 
26168  71 
*} 
72 

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

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

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

76 
by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric]) 
26168  77 

28335  78 
code_type typerep 
31031  79 
(Eval "Term.typ") 
26168  80 

28335  81 
code_const Typerep 
31031  82 
(Eval "Term.Type/ (_, _)") 
26168  83 

31031  84 
code_reserved Eval Term 
26168  85 

28335  86 
hide (open) const typerep Typerep 
26168  87 

88 
end 