equal
deleted
inserted
replaced
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 is_true: term -> bool |
|
10 |
9 val last2: 'a list -> 'a * 'a |
11 val last2: 'a list -> 'a * 'a |
10 |
12 |
11 val dest_listT: typ -> typ |
13 val dest_listT: typ -> typ |
12 |
14 |
13 val size_const: typ -> term |
15 val size_const: typ -> term |
84 end |
86 end |
85 |
87 |
86 |
88 |
87 structure Nominal_Library: NOMINAL_LIBRARY = |
89 structure Nominal_Library: NOMINAL_LIBRARY = |
88 struct |
90 struct |
|
91 |
|
92 fun is_true @{term "Trueprop True"} = true |
|
93 | is_true _ = false |
89 |
94 |
90 fun last2 [] = raise Empty |
95 fun last2 [] = raise Empty |
91 | last2 [_] = raise Empty |
96 | last2 [_] = raise Empty |
92 | last2 [x, y] = (x, y) |
97 | last2 [x, y] = (x, y) |
93 | last2 (_ :: xs) = last2 xs |
98 | last2 (_ :: xs) = last2 xs |
254 let |
259 let |
255 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
260 fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = |
256 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
261 SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) |
257 | mk_size_measure T = size_const T |
262 | mk_size_measure T = size_const T |
258 |
263 |
259 val ((_ $ (_ $ rel)) :: tl) = prems_of st |
264 val ((_ $ (_ $ rel)) :: _) = prems_of st |
260 val measure_trm = |
265 val measure_trm = |
261 fastype_of rel |
266 fastype_of rel |
262 |> HOLogic.dest_setT |
267 |> HOLogic.dest_setT |
263 |> mk_size_measure |
268 |> mk_size_measure |
264 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
269 |> curry (op $) (Const (@{const_name measure}, dummyT)) |
322 (* |
327 (* |
323 inductive premises can be of the form |
328 inductive premises can be of the form |
324 R ... /\ P ...; split_conj_i picks out |
329 R ... /\ P ...; split_conj_i picks out |
325 the part R or P part |
330 the part R or P part |
326 *) |
331 *) |
327 fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = |
332 fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = |
328 (case head_of f1 of |
333 (case head_of f1 of |
329 Const (name, _) => if member (op =) names name then SOME f1 else NONE |
334 Const (name, _) => if member (op =) names name then SOME f1 else NONE |
330 | _ => NONE) |
335 | _ => NONE) |
331 | split_conj1 _ _ = NONE; |
336 | split_conj1 _ _ = NONE; |
332 |
337 |