|
15178
|
1 |
exception Fail_conv;
|
|
|
2 |
|
|
|
3 |
fun orelsec conv1 conv2 ct = conv1 ct handle Fail_conv => conv2 ct
|
|
|
4 |
|
|
|
5 |
val allc = Thm.reflexive
|
|
|
6 |
|
|
|
7 |
fun thenc conv1 conv2 ct =
|
|
|
8 |
let
|
|
|
9 |
fun rhs_of t = snd (Thm.dest_comb (strip_imp_concl (cprop_of t)))
|
|
|
10 |
|
|
|
11 |
val eq = conv1 ct
|
|
|
12 |
in
|
|
|
13 |
Thm.transitive eq (conv2 (rhs_of eq))
|
|
|
14 |
end
|
|
|
15 |
|
|
|
16 |
fun subc conv ct =
|
|
|
17 |
case term_of ct of
|
|
|
18 |
_ $ _ =>
|
|
|
19 |
let
|
|
|
20 |
val (ct1, ct2) = Thm.dest_comb ct
|
|
|
21 |
in
|
|
|
22 |
Thm.combination (conv ct1) (conv ct2)
|
|
|
23 |
end
|
|
|
24 |
| _ => allc ct
|
|
|
25 |
|
|
|
26 |
fun botc conv ct = thenc (subc (botc conv)) (orelsec conv allc) ct |