equal
deleted
inserted
replaced
4 |
4 |
5 theory Typerep |
5 theory Typerep |
6 imports Plain String |
6 imports Plain String |
7 begin |
7 begin |
8 |
8 |
9 datatype typerep = Typerep message_string "typerep list" |
9 datatype typerep = Typerep String.literal "typerep list" |
10 |
10 |
11 class typerep = |
11 class typerep = |
12 fixes typerep :: "'a itself \<Rightarrow> typerep" |
12 fixes typerep :: "'a itself \<Rightarrow> typerep" |
13 begin |
13 begin |
14 |
14 |
43 val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; |
43 val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; |
44 val vs = Name.names Name.context "'a" sorts; |
44 val vs = Name.names Name.context "'a" sorts; |
45 val ty = Type (tyco, map TFree vs); |
45 val ty = Type (tyco, map TFree vs); |
46 val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep}) |
46 val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep}) |
47 $ Free ("T", Term.itselfT ty); |
47 $ Free ("T", Term.itselfT ty); |
48 val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco |
48 val rhs = @{term Typerep} $ HOLogic.mk_literal tyco |
49 $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs); |
49 $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs); |
50 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
50 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
51 in |
51 in |
52 thy |
52 thy |
53 |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep}) |
53 |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep}) |