3 Author: Amine Chaieb and Makarius |
3 Author: Amine Chaieb and Makarius |
4 |
4 |
5 Conversions: primitive equality reasoning. |
5 Conversions: primitive equality reasoning. |
6 *) |
6 *) |
7 |
7 |
8 infix 1 thenc; |
8 infix 1 then_conv; |
9 infix 0 orelsec; |
9 infix 0 else_conv; |
10 |
10 |
11 signature CONV = |
11 signature CONV = |
12 sig |
12 sig |
13 type conv = cterm -> thm |
13 type conv = cterm -> thm |
14 val no_conv: conv |
14 val no_conv: conv |
15 val all_conv: conv |
15 val all_conv: conv |
16 val thenc: conv * conv -> conv |
16 val then_conv: conv * conv -> conv |
17 val orelsec: conv * conv -> conv |
17 val else_conv: conv * conv -> conv |
18 val first_conv: conv list -> conv |
18 val first_conv: conv list -> conv |
19 val every_conv: conv list -> conv |
19 val every_conv: conv list -> conv |
20 val tryc: conv -> conv |
20 val try_conv: conv -> conv |
21 val repeatc: conv -> conv |
21 val repeat_conv: conv -> conv |
22 val cache_conv: conv -> conv |
22 val cache_conv: conv -> conv |
23 val abs_conv: conv -> conv |
23 val abs_conv: conv -> conv |
24 val combination_conv: conv -> conv -> conv |
24 val combination_conv: conv -> conv -> conv |
25 val comb_conv: conv -> conv |
25 val comb_conv: conv -> conv |
26 val arg_conv: conv -> conv |
26 val arg_conv: conv -> conv |
44 fun no_conv _ = raise CTERM ("no conversion", []); |
44 fun no_conv _ = raise CTERM ("no conversion", []); |
45 val all_conv = Thm.reflexive; |
45 val all_conv = Thm.reflexive; |
46 |
46 |
47 val is_refl = op aconv o Logic.dest_equals o Thm.prop_of; |
47 val is_refl = op aconv o Logic.dest_equals o Thm.prop_of; |
48 |
48 |
49 fun (cv1 thenc cv2) ct = |
49 fun (cv1 then_conv cv2) ct = |
50 let |
50 let |
51 val eq1 = cv1 ct; |
51 val eq1 = cv1 ct; |
52 val eq2 = cv2 (Thm.rhs_of eq1); |
52 val eq2 = cv2 (Thm.rhs_of eq1); |
53 in |
53 in |
54 if is_refl eq1 then eq2 |
54 if is_refl eq1 then eq2 |
55 else if is_refl eq2 then eq1 |
55 else if is_refl eq2 then eq1 |
56 else Thm.transitive eq1 eq2 |
56 else Thm.transitive eq1 eq2 |
57 end; |
57 end; |
58 |
58 |
59 fun (cv1 orelsec cv2) ct = |
59 fun (cv1 else_conv cv2) ct = |
60 (case try cv1 ct of SOME eq => eq | NONE => cv2 ct); |
60 (case try cv1 ct of SOME eq => eq | NONE => cv2 ct); |
61 |
61 |
62 fun first_conv cvs = fold_rev (curry op orelsec) cvs no_conv; |
62 fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv; |
63 fun every_conv cvs = fold_rev (curry op thenc) cvs all_conv; |
63 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; |
64 |
64 |
65 fun tryc cv = cv orelsec all_conv; |
65 fun try_conv cv = cv else_conv all_conv; |
66 fun repeatc cv ct = tryc (cv thenc repeatc cv) ct; |
66 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; |
67 |
67 |
68 fun cache_conv cv = |
68 fun cache_conv cv = |
69 let |
69 let |
70 val cache = ref Termtab.empty; |
70 val cache = ref Termtab.empty; |
71 fun conv ct = |
71 fun conv ct = |