equal
deleted
inserted
replaced
16 end; |
16 end; |
17 |
17 |
18 structure Lifting_Def: LIFTING_DEF = |
18 structure Lifting_Def: LIFTING_DEF = |
19 struct |
19 struct |
20 |
20 |
21 (** Interface and Syntax Setup **) |
21 open Lifting_Util |
|
22 |
|
23 infix 0 MRSL |
22 |
24 |
23 (* Generation of the code certificate from the rsp theorem *) |
25 (* Generation of the code certificate from the rsp theorem *) |
24 |
|
25 infix 0 MRSL |
|
26 |
|
27 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
|
28 |
26 |
29 fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) |
27 fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) |
30 | get_body_types (U, V) = (U, V) |
28 | get_body_types (U, V) = (U, V) |
31 |
29 |
32 fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) |
30 fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) |