author | wenzelm |
Sun, 22 Jul 2012 12:26:41 +0200 | |
changeset 48423 | 0ccf143a2a69 |
parent 43333 | 2bdec7f430d3 |
child 49974 | 791157a4179a |
permissions | -rw-r--r-- |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/conv.ML |
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
2 |
Author: Amine Chaieb, TU Muenchen |
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
3 |
Author: Sascha Boehme, TU Muenchen |
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
4 |
Author: Makarius |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
5 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
6 |
Conversions: primitive equality reasoning. |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
7 |
*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
8 |
|
22937 | 9 |
infix 1 then_conv; |
10 |
infix 0 else_conv; |
|
23169 | 11 |
|
30136
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
12 |
signature BASIC_CONV = |
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
13 |
sig |
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
14 |
val then_conv: conv * conv -> conv |
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
15 |
val else_conv: conv * conv -> conv |
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
16 |
end; |
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
17 |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
18 |
signature CONV = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
19 |
sig |
30136
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
20 |
include BASIC_CONV |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
21 |
val no_conv: conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
22 |
val all_conv: conv |
22926 | 23 |
val first_conv: conv list -> conv |
24 |
val every_conv: conv list -> conv |
|
22937 | 25 |
val try_conv: conv -> conv |
26 |
val repeat_conv: conv -> conv |
|
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
27 |
val cache_conv: conv -> conv |
26571 | 28 |
val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv |
22926 | 29 |
val combination_conv: conv -> conv -> conv |
30 |
val comb_conv: conv -> conv |
|
31 |
val arg_conv: conv -> conv |
|
32 |
val fun_conv: conv -> conv |
|
33 |
val arg1_conv: conv -> conv |
|
34 |
val fun2_conv: conv -> conv |
|
23034 | 35 |
val binop_conv: conv -> conv |
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
36 |
val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv |
26571 | 37 |
val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv |
38 |
val implies_conv: conv -> conv -> conv |
|
39 |
val implies_concl_conv: conv -> conv |
|
40 |
val rewr_conv: thm -> conv |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
41 |
val rewrs_conv: thm list -> conv |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
42 |
val sub_conv: (Proof.context -> conv) -> Proof.context -> conv |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
43 |
val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
44 |
val top_conv: (Proof.context -> conv) -> Proof.context -> conv |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
45 |
val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv |
26571 | 46 |
val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv |
47 |
val prems_conv: int -> conv -> conv |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
48 |
val concl_conv: int -> conv -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
49 |
val fconv_rule: conv -> thm -> thm |
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
50 |
val gconv_rule: conv -> int -> thm -> thm |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
51 |
end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
52 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
53 |
structure Conv: CONV = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
54 |
struct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
55 |
|
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
56 |
(* basic conversionals *) |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
57 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
58 |
fun no_conv _ = raise CTERM ("no conversion", []); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
59 |
val all_conv = Thm.reflexive; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
60 |
|
22937 | 61 |
fun (cv1 then_conv cv2) ct = |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
62 |
let |
22926 | 63 |
val eq1 = cv1 ct; |
64 |
val eq2 = cv2 (Thm.rhs_of eq1); |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
65 |
in |
23596 | 66 |
if Thm.is_reflexive eq1 then eq2 |
67 |
else if Thm.is_reflexive eq2 then eq1 |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
68 |
else Thm.transitive eq1 eq2 |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
69 |
end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
70 |
|
22937 | 71 |
fun (cv1 else_conv cv2) ct = |
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
72 |
(cv1 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
73 |
handle THM _ => cv2 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
74 |
| CTERM _ => cv2 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
75 |
| TERM _ => cv2 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
76 |
| TYPE _ => cv2 ct); |
22926 | 77 |
|
22937 | 78 |
fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv; |
79 |
fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; |
|
22926 | 80 |
|
22937 | 81 |
fun try_conv cv = cv else_conv all_conv; |
82 |
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; |
|
22926 | 83 |
|
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
84 |
fun cache_conv (cv: conv) = Thm.cterm_cache cv; |
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
85 |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
86 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
87 |
|
22926 | 88 |
(** Pure conversions **) |
89 |
||
90 |
(* lambda terms *) |
|
91 |
||
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset
|
92 |
fun abs_conv cv ctxt ct = |
23587 | 93 |
(case Thm.term_of ct of |
22926 | 94 |
Abs (x, _, _) => |
23596 | 95 |
let |
42485 | 96 |
val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt; |
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset
|
97 |
val (v, ct') = Thm.dest_abs (SOME u) ct; |
26571 | 98 |
val eq = cv (v, ctxt') ct'; |
23596 | 99 |
in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end |
22926 | 100 |
| _ => raise CTERM ("abs_conv", [ct])); |
101 |
||
102 |
fun combination_conv cv1 cv2 ct = |
|
103 |
let val (ct1, ct2) = Thm.dest_comb ct |
|
104 |
in Thm.combination (cv1 ct1) (cv2 ct2) end; |
|
105 |
||
106 |
fun comb_conv cv = combination_conv cv cv; |
|
107 |
fun arg_conv cv = combination_conv all_conv cv; |
|
108 |
fun fun_conv cv = combination_conv cv all_conv; |
|
109 |
||
110 |
val arg1_conv = fun_conv o arg_conv; |
|
111 |
val fun2_conv = fun_conv o fun_conv; |
|
112 |
||
23034 | 113 |
fun binop_conv cv = combination_conv (arg_conv cv) cv; |
22926 | 114 |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
115 |
fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt); |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
116 |
|
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
117 |
|
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
118 |
(* subterm structure *) |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
119 |
|
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
120 |
(*cf. SUB_CONV in HOL*) |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
121 |
fun sub_conv conv ctxt = |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
122 |
comb_conv (conv ctxt) else_conv |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
123 |
abs_conv (conv o snd) ctxt else_conv |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
124 |
all_conv; |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
125 |
|
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
126 |
(*cf. BOTTOM_CONV in HOL*) |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
127 |
fun bottom_conv conv ctxt ct = |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
128 |
(sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct; |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
129 |
|
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
130 |
(*cf. TOP_CONV in HOL*) |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
131 |
fun top_conv conv ctxt ct = |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
132 |
(conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct; |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
133 |
|
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
134 |
(*cf. TOP_SWEEP_CONV in HOL*) |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
135 |
fun top_sweep_conv conv ctxt ct = |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
136 |
(conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct; |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
137 |
|
23169 | 138 |
|
26571 | 139 |
(* primitive logic *) |
140 |
||
141 |
fun forall_conv cv ctxt ct = |
|
142 |
(case Thm.term_of ct of |
|
143 |
Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct |
|
144 |
| _ => raise CTERM ("forall_conv", [ct])); |
|
145 |
||
146 |
fun implies_conv cv1 cv2 ct = |
|
147 |
(case Thm.term_of ct of |
|
148 |
Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct |
|
149 |
| _ => raise CTERM ("implies_conv", [ct])); |
|
150 |
||
151 |
fun implies_concl_conv cv ct = |
|
152 |
(case Thm.term_of ct of |
|
153 |
Const ("==>", _) $ _ $ _ => arg_conv cv ct |
|
154 |
| _ => raise CTERM ("implies_concl_conv", [ct])); |
|
155 |
||
156 |
||
157 |
(* single rewrite step, cf. REWR_CONV in HOL *) |
|
158 |
||
159 |
fun rewr_conv rule ct = |
|
160 |
let |
|
161 |
val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule; |
|
162 |
val lhs = Thm.lhs_of rule1; |
|
163 |
val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1; |
|
164 |
in |
|
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42485
diff
changeset
|
165 |
Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2 |
26571 | 166 |
handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct]) |
167 |
end; |
|
168 |
||
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
169 |
fun rewrs_conv rules = first_conv (map rewr_conv rules); |
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
32843
diff
changeset
|
170 |
|
26571 | 171 |
|
172 |
(* conversions on HHF rules *) |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
173 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
174 |
(*rewrite B in !!x1 ... xn. B*) |
26571 | 175 |
fun params_conv n cv ctxt ct = |
27332 | 176 |
if n <> 0 andalso Logic.is_all (Thm.term_of ct) |
26571 | 177 |
then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct |
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset
|
178 |
else cv ctxt ct; |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
179 |
|
26571 | 180 |
(*rewrite the A's in A1 ==> ... ==> An ==> B*) |
181 |
fun prems_conv 0 _ ct = all_conv ct |
|
182 |
| prems_conv n cv ct = |
|
183 |
(case try Thm.dest_implies ct of |
|
184 |
NONE => all_conv ct |
|
185 |
| SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B)); |
|
186 |
||
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
187 |
(*rewrite B in A1 ==> ... ==> An ==> B*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
188 |
fun concl_conv 0 cv ct = cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
189 |
| concl_conv n cv ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
190 |
(case try Thm.dest_implies ct of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
191 |
NONE => cv ct |
22926 | 192 |
| SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B)); |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
193 |
|
23596 | 194 |
|
26571 | 195 |
(* conversions as inference rules *) |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
196 |
|
23596 | 197 |
(*forward conversion, cf. FCONV_RULE in LCF*) |
198 |
fun fconv_rule cv th = |
|
199 |
let val eq = cv (Thm.cprop_of th) in |
|
200 |
if Thm.is_reflexive eq then th |
|
201 |
else Thm.equal_elim eq th |
|
202 |
end; |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
203 |
|
23596 | 204 |
(*goal conversion*) |
205 |
fun gconv_rule cv i th = |
|
206 |
(case try (Thm.cprem_of th) i of |
|
207 |
SOME ct => |
|
208 |
let val eq = cv ct in |
|
209 |
if Thm.is_reflexive eq then th |
|
210 |
else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th |
|
211 |
end |
|
212 |
| NONE => raise THM ("gconv_rule", i, [th])); |
|
23411
c524900454f3
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
chaieb
parents:
23169
diff
changeset
|
213 |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
214 |
end; |
30136
6a874aedb964
Made then_conv and else_conv available as infix operations.
boehmes
parents:
29606
diff
changeset
|
215 |
|
32843
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
216 |
structure Basic_Conv: BASIC_CONV = Conv; |
c8f5a7c8353f
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents:
30136
diff
changeset
|
217 |
open Basic_Conv; |