4 Basic functions for nominal. |
4 Basic functions for nominal. |
5 *) |
5 *) |
6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
|
9 val last2: 'a list -> 'a * 'a |
|
10 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
|
11 |
9 val is_true: term -> bool |
12 val is_true: term -> bool |
10 |
13 |
11 val last2: 'a list -> 'a * 'a |
|
12 |
|
13 val dest_listT: typ -> typ |
14 val dest_listT: typ -> typ |
|
15 |
|
16 val mk_id: term -> term |
14 |
17 |
15 val size_const: typ -> term |
18 val size_const: typ -> term |
16 |
19 |
17 val sum_case_const: typ -> typ -> typ -> term |
20 val sum_case_const: typ -> typ -> typ -> term |
18 val mk_sum_case: term -> term -> term |
21 val mk_sum_case: term -> term -> term |
89 |
92 |
90 |
93 |
91 structure Nominal_Library: NOMINAL_LIBRARY = |
94 structure Nominal_Library: NOMINAL_LIBRARY = |
92 struct |
95 struct |
93 |
96 |
94 fun is_true @{term "Trueprop True"} = true |
97 (* orders an AList according to keys *) |
95 | is_true _ = false |
98 fun order eq keys list = |
|
99 map (the o AList.lookup eq list) keys |
96 |
100 |
97 fun last2 [] = raise Empty |
101 fun last2 [] = raise Empty |
98 | last2 [_] = raise Empty |
102 | last2 [_] = raise Empty |
99 | last2 [x, y] = (x, y) |
103 | last2 [x, y] = (x, y) |
100 | last2 (_ :: xs) = last2 xs |
104 | last2 (_ :: xs) = last2 xs |
101 |
105 |
|
106 |
|
107 fun is_true @{term "Trueprop True"} = true |
|
108 | is_true _ = false |
|
109 |
102 fun dest_listT (Type (@{type_name list}, [T])) = T |
110 fun dest_listT (Type (@{type_name list}, [T])) = T |
103 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
111 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
|
112 |
|
113 fun mk_id trm = |
|
114 let |
|
115 val ty = fastype_of trm |
|
116 in |
|
117 Const (@{const_name id}, ty --> ty) $ trm |
|
118 end |
|
119 |
104 |
120 |
105 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
121 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
106 |
122 |
107 fun sum_case_const ty1 ty2 ty3 = |
123 fun sum_case_const ty1 ty2 ty3 = |
108 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
124 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |