19 |
19 |
20 NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; |
20 NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; |
21 "!x. x=t --> P(x)" is covered by the congreunce rule for -->; |
21 "!x. x=t --> P(x)" is covered by the congreunce rule for -->; |
22 "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. |
22 "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. |
23 As must be "? x. t=x & P(x)". |
23 As must be "? x. t=x & P(x)". |
24 |
|
25 |
24 |
26 And similarly for the bounded quantifiers. |
25 And similarly for the bounded quantifiers. |
27 |
26 |
28 Gries etc call this the "1 point rules" |
27 Gries etc call this the "1 point rules" |
|
28 |
|
29 The above also works for !x1..xn. and ?x1..xn by moving the defined |
|
30 qunatifier inside first, but not for nested bounded quantifiers. |
|
31 |
|
32 For set comprehensions the basic permutations |
|
33 ... & x = t & ... -> x = t & (... & ...) |
|
34 ... & t = x & ... -> t = x & (... & ...) |
|
35 are also exported. |
|
36 |
|
37 To avoid looping, NONE is returned if the term cannot be rearranged, |
|
38 esp if x=t/t=x sits at the front already. |
29 *) |
39 *) |
30 |
40 |
31 signature QUANTIFIER1_DATA = |
41 signature QUANTIFIER1_DATA = |
32 sig |
42 sig |
33 (*abstract syntax*) |
43 (*abstract syntax*) |
59 val prove_one_point_ex_tac: tactic |
69 val prove_one_point_ex_tac: tactic |
60 val rearrange_all: theory -> simpset -> term -> thm option |
70 val rearrange_all: theory -> simpset -> term -> thm option |
61 val rearrange_ex: theory -> simpset -> term -> thm option |
71 val rearrange_ex: theory -> simpset -> term -> thm option |
62 val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option |
72 val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option |
63 val rearrange_bex: (simpset -> tactic) -> theory -> simpset -> term -> thm option |
73 val rearrange_bex: (simpset -> tactic) -> theory -> simpset -> term -> thm option |
|
74 val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option |
64 end; |
75 end; |
65 |
76 |
66 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = |
77 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = |
67 struct |
78 struct |
68 |
79 |
69 open Data; |
80 open Data; |
70 |
81 |
71 (* FIXME: only test! *) |
82 (* FIXME: only test! *) |
72 fun def xs eq = |
83 fun def xs eq = |
73 let val n = length xs |
84 (case dest_eq eq of |
74 in case dest_eq eq of |
85 SOME(c,s,t) => |
75 SOME(c,s,t) => |
86 let val n = length xs |
76 s = Bound n andalso not(loose_bvar1(t,n)) orelse |
87 in s = Bound n andalso not(loose_bvar1(t,n)) orelse |
77 t = Bound n andalso not(loose_bvar1(s,n)) |
88 t = Bound n andalso not(loose_bvar1(s,n)) end |
78 | NONE => false |
89 | NONE => false); |
79 end; |
|
80 |
90 |
81 fun extract_conj xs t = case dest_conj t of NONE => NONE |
91 fun extract_conj fst xs t = case dest_conj t of NONE => NONE |
82 | SOME(conj,P,Q) => |
92 | SOME(conj,P,Q) => |
83 (if def xs P then SOME(xs,P,Q) else |
93 (if not fst andalso def xs P then SOME(xs,P,Q) else |
84 if def xs Q then SOME(xs,Q,P) else |
94 if def xs Q then SOME(xs,Q,P) else |
85 (case extract_conj xs P of |
95 (case extract_conj false xs P of |
86 SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q) |
96 SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q) |
87 | NONE => (case extract_conj xs Q of |
97 | NONE => (case extract_conj false xs Q of |
88 SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q') |
98 SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q') |
89 | NONE => NONE))); |
99 | NONE => NONE))); |
90 |
100 |
91 fun extract_imp xs t = case dest_imp t of NONE => NONE |
101 fun extract_imp fst xs t = case dest_imp t of NONE => NONE |
92 | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q) |
102 | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q) |
93 else (case extract_conj xs P of |
103 else (case extract_conj false xs P of |
94 SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q) |
104 SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q) |
95 | NONE => (case extract_imp xs Q of |
105 | NONE => (case extract_imp false xs Q of |
96 NONE => NONE |
106 NONE => NONE |
97 | SOME(xs,eq,Q') => |
107 | SOME(xs,eq,Q') => |
98 SOME(xs,eq,imp$P$Q'))); |
108 SOME(xs,eq,imp$P$Q'))); |
99 |
109 |
100 fun extract_quant extract q = |
110 fun extract_quant extract q = |
101 let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) = |
111 let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) = |
102 if qa = q then exqu ((qC,x,T)::xs) Q else NONE |
112 if qa = q then exqu ((qC,x,T)::xs) Q else NONE |
103 | exqu xs P = extract xs P |
113 | exqu xs P = extract (null xs) xs P |
104 in exqu end; |
114 in exqu [] end; |
105 |
115 |
106 fun prove_conv tac thy tu = |
116 fun prove_conv tac thy tu = |
107 Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) |
117 Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) |
108 (K (rtac iff_reflection 1 THEN tac)); |
118 (K (rtac iff_reflection 1 THEN tac)); |
109 |
119 |
145 val n = length xs |
155 val n = length xs |
146 val Q = if n=0 then P else renumber 0 n P |
156 val Q = if n=0 then P else renumber 0 n P |
147 in quant xs (qC $ Abs(x,T,Q)) end; |
157 in quant xs (qC $ Abs(x,T,Q)) end; |
148 |
158 |
149 fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) = |
159 fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) = |
150 (case extract_quant extract_imp q [] P of |
160 (case extract_quant extract_imp q P of |
151 NONE => NONE |
161 NONE => NONE |
152 | SOME(xs,eq,Q) => |
162 | SOME(xs,eq,Q) => |
153 let val R = quantify all x T xs (imp $ eq $ Q) |
163 let val R = quantify all x T xs (imp $ eq $ Q) |
154 in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end) |
164 in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end) |
155 | rearrange_all _ _ _ = NONE; |
165 | rearrange_all _ _ _ = NONE; |
156 |
166 |
157 fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) = |
167 fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) = |
158 (case extract_imp [] P of |
168 (case extract_imp true [] P of |
159 NONE => NONE |
169 NONE => NONE |
160 | SOME(xs,eq,Q) => if not(null xs) then NONE else |
170 | SOME(xs,eq,Q) => if not(null xs) then NONE else |
161 let val R = imp $ eq $ Q |
171 let val R = imp $ eq $ Q |
162 in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end) |
172 in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end) |
163 | rearrange_ball _ _ _ _ = NONE; |
173 | rearrange_ball _ _ _ _ = NONE; |
164 |
174 |
165 fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) = |
175 fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) = |
166 (case extract_quant extract_conj q [] P of |
176 (case extract_quant extract_conj q P of |
167 NONE => NONE |
177 NONE => NONE |
168 | SOME(xs,eq,Q) => |
178 | SOME(xs,eq,Q) => |
169 let val R = quantify ex x T xs (conj $ eq $ Q) |
179 let val R = quantify ex x T xs (conj $ eq $ Q) |
170 in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end) |
180 in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end) |
171 | rearrange_ex _ _ _ = NONE; |
181 | rearrange_ex _ _ _ = NONE; |
172 |
182 |
173 fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) = |
183 fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) = |
174 (case extract_conj [] P of |
184 (case extract_conj true [] P of |
175 NONE => NONE |
185 NONE => NONE |
176 | SOME(xs,eq,Q) => if not(null xs) then NONE else |
186 | SOME(xs,eq,Q) => if not(null xs) then NONE else |
177 SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q)))) |
187 SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q)))) |
178 | rearrange_bex _ _ _ _ = NONE; |
188 | rearrange_bex _ _ _ _ = NONE; |
179 |
189 |
|
190 fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) = |
|
191 (case extract_conj true [] P of |
|
192 NONE => NONE |
|
193 | SOME(_,eq,Q) => |
|
194 let val R = Coll $ Abs(x,T, conj $ eq $ Q) |
|
195 in SOME(prove_conv tac thy (F,R)) end); |
|
196 |
180 end; |
197 end; |