author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45693  bbd2c7ffc02c 
child 48272  db75b4005d9a 
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 

35115  20 
syntax 
21 
"_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))") 

22 

23 
parse_translation {* 

26168  24 
let 
28335  25 
fun typerep_tr (*"_TYPEREP"*) [ty] = 
35115  26 
Syntax.const @{const_syntax typerep} $ 
27 
(Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $ 

35363  28 
(Syntax.const @{type_syntax itself} $ ty)) 
28335  29 
 typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); 
35115  30 
in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end 
31 
*} 

32 

42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

33 
typed_print_translation (advanced) {* 
35115  34 
let 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

35 
fun typerep_tr' ctxt (*"typerep"*) 
35430
df2862dc23a8
adapted to authentic syntax  actual types are verbatim;
wenzelm
parents:
35363
diff
changeset

36 
(Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _])) 
35363  37 
(Const (@{const_syntax TYPE}, _) :: ts) = 
35115  38 
Term.list_comb 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

39 
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts) 
28335  40 
 typerep_tr' _ T ts = raise Match; 
35115  41 
in [(@{const_syntax typerep}, typerep_tr')] end 
26168  42 
*} 
43 

31137  44 
setup {* 
45 
let 

26168  46 

31137  47 
fun add_typerep tyco thy = 
26168  48 
let 
28335  49 
val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42247
diff
changeset

50 
val vs = Name.invent_names Name.context "'a" sorts; 
26168  51 
val ty = Type (tyco, map TFree vs); 
28335  52 
val lhs = Const (@{const_name typerep}, Term.itselfT ty > @{typ typerep}) 
26168  53 
$ Free ("T", Term.itselfT ty); 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31137
diff
changeset

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

58 
thy 

38348
cf7b2121ad9d
moved instantiation target formally to class_target.ML
haftmann
parents:
36176
diff
changeset

59 
> Class.instantiation ([tyco], vs, @{sort typerep}) 
26168  60 
> `(fn lthy => Syntax.check_term lthy eq) 
28965  61 
> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) 
26168  62 
> snd 
31137  63 
> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) 
26168  64 
end; 
65 

45693  66 
fun ensure_typerep tyco thy = 
67 
if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}) 

68 
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type} 

31137  69 
then add_typerep tyco thy else thy; 
70 

71 
in 

26168  72 

31137  73 
add_typerep @{type_name fun} 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31205
diff
changeset

74 
#> Typedef.interpretation ensure_typerep 
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35115
diff
changeset

75 
#> Code.datatype_interpretation (ensure_typerep o fst) 
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35115
diff
changeset

76 
#> Code.abstype_interpretation (ensure_typerep o fst) 
26168  77 

31137  78 
end 
26168  79 
*} 
80 

28562  81 
lemma [code]: 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset

82 
"HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset

83 
\<and> list_all2 HOL.equal tys1 tys2" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset

84 
by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric]) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset

85 

97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset

86 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset

87 
"HOL.equal (x :: typerep) x \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset

88 
by (fact equal_refl) 
26168  89 

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

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

31031  96 
code_reserved Eval Term 
26168  97 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35430
diff
changeset

98 
hide_const (open) typerep Typerep 
26168  99 

100 
end 