author | blanchet |
Tue, 14 Sep 2010 13:24:18 +0200 | |
changeset 39359 | 6f49c7fbb1b1 |
parent 38857 | 97775f3e8722 |
child 42245 | 29e3967550d5 |
permissions | -rw-r--r-- |
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 |
||
33 |
typed_print_translation {* |
|
34 |
let |
|
35363 | 35 |
fun typerep_tr' show_sorts (*"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 |
39 |
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts 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}; |
26168 | 50 |
val vs = Name.names Name.context "'a" sorts; |
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 |
||
31137 | 66 |
fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}) |
67 |
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type} |
|
68 |
then add_typerep tyco thy else thy; |
|
69 |
||
70 |
in |
|
26168 | 71 |
|
31137 | 72 |
add_typerep @{type_name fun} |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31205
diff
changeset
|
73 |
#> Typedef.interpretation ensure_typerep |
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35115
diff
changeset
|
74 |
#> Code.datatype_interpretation (ensure_typerep o fst) |
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35115
diff
changeset
|
75 |
#> Code.abstype_interpretation (ensure_typerep o fst) |
26168 | 76 |
|
31137 | 77 |
end |
26168 | 78 |
*} |
79 |
||
28562 | 80 |
lemma [code]: |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset
|
81 |
"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
|
82 |
\<and> list_all2 HOL.equal tys1 tys2" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset
|
83 |
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
|
84 |
|
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset
|
85 |
lemma [code nbe]: |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset
|
86 |
"HOL.equal (x :: typerep) x \<longleftrightarrow> True" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset
|
87 |
by (fact equal_refl) |
26168 | 88 |
|
28335 | 89 |
code_type typerep |
31031 | 90 |
(Eval "Term.typ") |
26168 | 91 |
|
28335 | 92 |
code_const Typerep |
31031 | 93 |
(Eval "Term.Type/ (_, _)") |
26168 | 94 |
|
31031 | 95 |
code_reserved Eval Term |
26168 | 96 |
|
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
|
97 |
hide_const (open) typerep Typerep |
26168 | 98 |
|
99 |
end |