src/HOL/Typerep.thy
 author paulson Mon May 23 15:33:24 2016 +0100 (2016-05-23) changeset 63114 27afe7af7379 parent 63064 2f18172214c8 child 63180 ddfd021884b4 permissions -rw-r--r--
Lots of new material for multivariate analysis
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 section \<open>Reflecting Pure types into HOL\<close>
```
```     4
```
```     5 theory Typerep
```
```     6 imports String
```
```     7 begin
```
```     8
```
```     9 datatype typerep = Typerep String.literal "typerep list"
```
```    10
```
```    11 class typerep =
```
```    12   fixes typerep :: "'a itself \<Rightarrow> typerep"
```
```    13 begin
```
```    14
```
```    15 definition typerep_of :: "'a \<Rightarrow> typerep" where
```
```    16   [simp]: "typerep_of x = typerep TYPE('a)"
```
```    17
```
```    18 end
```
```    19
```
```    20 syntax
```
```    21   "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
```
```    22
```
```    23 parse_translation \<open>
```
```    24   let
```
```    25     fun typerep_tr (*"_TYPEREP"*) [ty] =
```
```    26           Syntax.const @{const_syntax typerep} \$
```
```    27             (Syntax.const @{syntax_const "_constrain"} \$ Syntax.const @{const_syntax Pure.type} \$
```
```    28               (Syntax.const @{type_syntax itself} \$ ty))
```
```    29       | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
```
```    30   in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
```
```    31 \<close>
```
```    32
```
```    33 typed_print_translation \<open>
```
```    34   let
```
```    35     fun typerep_tr' ctxt (*"typerep"*)
```
```    36             (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
```
```    37             (Const (@{const_syntax Pure.type}, _) :: ts) =
```
```    38           Term.list_comb
```
```    39             (Syntax.const @{syntax_const "_TYPEREP"} \$ Syntax_Phases.term_of_typ ctxt T, ts)
```
```    40       | typerep_tr' _ T ts = raise Match;
```
```    41   in [(@{const_syntax typerep}, typerep_tr')] end
```
```    42 \<close>
```
```    43
```
```    44 setup \<open>
```
```    45 let
```
```    46
```
```    47 fun add_typerep tyco thy =
```
```    48   let
```
```    49     val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
```
```    50     val vs = Name.invent_names Name.context "'a" sorts;
```
```    51     val ty = Type (tyco, map TFree vs);
```
```    52     val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
```
```    53       \$ Free ("T", Term.itselfT ty);
```
```    54     val rhs = @{term Typerep} \$ HOLogic.mk_literal tyco
```
```    55       \$ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
```
```    56     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
```
```    57   in
```
```    58     thy
```
```    59     |> Class.instantiation ([tyco], vs, @{sort typerep})
```
```    60     |> `(fn lthy => Syntax.check_term lthy eq)
```
```    61     |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
```
```    62     |> snd
```
```    63     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
```
```    64   end;
```
```    65
```
```    66 fun ensure_typerep tyco thy =
```
```    67   if not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep})
```
```    68     andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort type}
```
```    69   then add_typerep tyco thy else thy;
```
```    70
```
```    71 in
```
```    72
```
```    73 add_typerep @{type_name fun}
```
```    74 #> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep)
```
```    75 #> Code.datatype_interpretation (ensure_typerep o fst)
```
```    76 #> Code.abstype_interpretation (ensure_typerep o fst)
```
```    77
```
```    78 end
```
```    79 \<close>
```
```    80
```
```    81 lemma [code]:
```
```    82   "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
```
```    83      \<and> list_all2 HOL.equal tys1 tys2"
```
```    84   by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
```
```    85
```
```    86 lemma [code nbe]:
```
```    87   "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
```
```    88   by (fact equal_refl)
```
```    89
```
```    90 code_printing
```
```    91   type_constructor typerep \<rightharpoonup> (Eval) "Term.typ"
```
```    92 | constant Typerep \<rightharpoonup> (Eval) "Term.Type/ (_, _)"
```
```    93
```
```    94 code_reserved Eval Term
```
```    95
```
```    96 hide_const (open) typerep Typerep
```
```    97
```
```    98 end
```