src/HOL/Typerep.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45693 bbd2c7ffc02c
child 48272 db75b4005d9a
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31048
ac146fc38b51 refined HOL string theories and corresponding ML fragments
haftmann
parents: 31031
diff changeset
     1
(* Author: Florian Haftmann, TU Muenchen *)
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
     2
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
     3
header {* Reflecting Pure types into HOL *}
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
     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
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
     7
begin
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
     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
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    10
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    11
class typerep =
31031
cbec39ebf8f2 class typerep inherits from type
haftmann
parents: 29574
diff changeset
    12
  fixes typerep :: "'a itself \<Rightarrow> typerep"
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    13
begin
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    14
29574
haftmann
parents: 28965
diff changeset
    15
definition typerep_of :: "'a \<Rightarrow> typerep" where
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    16
  [simp]: "typerep_of x = typerep TYPE('a)"
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    17
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    18
end
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    19
35115
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    20
syntax
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    21
  "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    22
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    23
parse_translation {*
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    24
let
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    25
  fun typerep_tr (*"_TYPEREP"*) [ty] =
35115
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    26
        Syntax.const @{const_syntax typerep} $
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    27
          (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
35363
09489d8ffece explicit @{type_syntax} markup;
wenzelm
parents: 35299
diff changeset
    28
            (Syntax.const @{type_syntax itself} $ ty))
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    29
    | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
35115
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    30
in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    31
*}
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    32
42247
12fe41a92cd5 typed_print_translation: discontinued show_sorts argument;
wenzelm
parents: 42245
diff changeset
    33
typed_print_translation (advanced) {*
35115
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    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
09489d8ffece explicit @{type_syntax} markup;
wenzelm
parents: 35299
diff changeset
    37
          (Const (@{const_syntax TYPE}, _) :: ts) =
35115
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    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
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    40
    | typerep_tr' _ T ts = raise Match;
35115
446c5063e4fd modernized translations;
wenzelm
parents: 33553
diff changeset
    41
in [(@{const_syntax typerep}, typerep_tr')] end
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    42
*}
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    43
31137
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    44
setup {*
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    45
let
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    46
31137
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    47
fun add_typerep tyco thy =
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    48
  let
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    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
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    51
    val ty = Type (tyco, map TFree vs);
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    52
    val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    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
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    55
      $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    56
    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    57
  in
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    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
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    60
    |> `(fn lthy => Syntax.check_term lthy eq)
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28952
diff changeset
    61
    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    62
    |> snd
31137
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    63
    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    64
  end;
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    65
45693
bbd2c7ffc02c tuned layout;
wenzelm
parents: 43329
diff changeset
    66
fun ensure_typerep tyco thy =
bbd2c7ffc02c tuned layout;
wenzelm
parents: 43329
diff changeset
    67
  if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
bbd2c7ffc02c tuned layout;
wenzelm
parents: 43329
diff changeset
    68
    andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
31137
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    69
  then add_typerep tyco thy else thy;
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    70
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    71
in
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    72
31137
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    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
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    77
31137
cd3aafc1c631 tuned construction of typerep instances
haftmann
parents: 31048
diff changeset
    78
end
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    79
*}
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    80
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28394
diff changeset
    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
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    89
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    90
code_type typerep
31031
cbec39ebf8f2 class typerep inherits from type
haftmann
parents: 29574
diff changeset
    91
  (Eval "Term.typ")
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    92
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28228
diff changeset
    93
code_const Typerep
31031
cbec39ebf8f2 class typerep inherits from type
haftmann
parents: 29574
diff changeset
    94
  (Eval "Term.Type/ (_, _)")
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    95
31031
cbec39ebf8f2 class typerep inherits from type
haftmann
parents: 29574
diff changeset
    96
code_reserved Eval Term
26168
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    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
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
    99
3bd9ac4e0b97 added theory for reflected types
haftmann
parents:
diff changeset
   100
end