1(* Title: Provers/quantifier1.ML 2 Author: Tobias Nipkow 3 Copyright 1997 TU Munich 4 5Simplification procedures for turning 6 7 ? x. ... & x = t & ... 8 into ? x. x = t & ... & ... 9 where the `? x. x = t &' in the latter formula must be eliminated 10 by ordinary simplification. 11 12 and ! x. (... & x = t & ...) --> P x 13 into ! x. x = t --> (... & ...) --> P x 14 where the `!x. x=t -->' in the latter formula is eliminated 15 by ordinary simplification. 16 17 And analogously for t=x, but the eqn is not turned around! 18 19 NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; 20 "!x. x=t --> P(x)" is covered by the congruence rule for -->; 21 "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. 22 As must be "? x. t=x & P(x)". 23 24 And similarly for the bounded quantifiers. 25 26Gries etc call this the "1 point rules" 27 28The above also works for !x1..xn. and ?x1..xn by moving the defined 29quantifier inside first, but not for nested bounded quantifiers. 30 31For set comprehensions the basic permutations 32 ... & x = t & ... -> x = t & (... & ...) 33 ... & t = x & ... -> t = x & (... & ...) 34are also exported. 35 36To avoid looping, NONE is returned if the term cannot be rearranged, 37esp if x=t/t=x sits at the front already. 38*) 39 40signature QUANTIFIER1_DATA = 41sig 42 (*abstract syntax*) 43 val dest_eq: term -> (term * term) option 44 val dest_conj: term -> (term * term) option 45 val dest_imp: term -> (term * term) option 46 val conj: term 47 val imp: term 48 (*rules*) 49 val iff_reflection: thm (* P <-> Q ==> P == Q *) 50 val iffI: thm 51 val iff_trans: thm 52 val conjI: thm 53 val conjE: thm 54 val impI: thm 55 val mp: thm 56 val exI: thm 57 val exE: thm 58 val uncurry: thm (* P --> Q --> R ==> P & Q --> R *) 59 val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *) 60 val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *) 61 val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *) 62 val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *) 63end; 64 65signature QUANTIFIER1 = 66sig 67 val prove_one_point_all_tac: Proof.context -> tactic 68 val prove_one_point_ex_tac: Proof.context -> tactic 69 val rearrange_all: Proof.context -> cterm -> thm option 70 val rearrange_ex: Proof.context -> cterm -> thm option 71 val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option 72 val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option 73 val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option 74end; 75 76functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 = 77struct 78 79(* FIXME: only test! *) 80fun def xs eq = 81 (case Data.dest_eq eq of 82 SOME (s, t) => 83 let val n = length xs in 84 s = Bound n andalso not (loose_bvar1 (t, n)) orelse 85 t = Bound n andalso not (loose_bvar1 (s, n)) 86 end 87 | NONE => false); 88 89fun extract_conj fst xs t = 90 (case Data.dest_conj t of 91 NONE => NONE 92 | SOME (P, Q) => 93 if def xs P then (if fst then NONE else SOME (xs, P, Q)) 94 else if def xs Q then SOME (xs, Q, P) 95 else 96 (case extract_conj false xs P of 97 SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q) 98 | NONE => 99 (case extract_conj false xs Q of 100 SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q') 101 | NONE => NONE))); 102 103fun extract_imp fst xs t = 104 (case Data.dest_imp t of 105 NONE => NONE 106 | SOME (P, Q) => 107 if def xs P then (if fst then NONE else SOME (xs, P, Q)) 108 else 109 (case extract_conj false xs P of 110 SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q) 111 | NONE => 112 (case extract_imp false xs Q of 113 NONE => NONE 114 | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q')))); 115 116fun extract_quant extract q = 117 let 118 fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) = 119 if qa = q then exqu ((qC, x, T) :: xs) Q else NONE 120 | exqu xs P = extract (null xs) xs P 121 in exqu [] end; 122 123fun prove_conv ctxt tu tac = 124 let 125 val (goal, ctxt') = 126 yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt; 127 val thm = 128 Goal.prove ctxt' [] [] goal 129 (fn {context = ctxt'', ...} => 130 resolve_tac ctxt'' [Data.iff_reflection] 1 THEN tac ctxt''); 131 in singleton (Variable.export ctxt' ctxt) thm end; 132 133fun qcomm_tac ctxt qcomm qI i = 134 REPEAT_DETERM (resolve_tac ctxt [qcomm] i THEN resolve_tac ctxt [qI] i); 135 136(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) 137 Better: instantiate exI 138*) 139local 140 val excomm = Data.ex_comm RS Data.iff_trans; 141in 142 fun prove_one_point_ex_tac ctxt = 143 qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN 144 ALLGOALS 145 (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE], 146 resolve_tac ctxt [Data.exI], 147 DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]]) 148end; 149 150(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) = 151 (! x1..xn x0. x0 = t --> (... & ...) --> P x0) 152*) 153local 154 fun tac ctxt = 155 SELECT_GOAL 156 (EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry], 157 REPEAT o resolve_tac ctxt [Data.impI], 158 eresolve_tac ctxt [Data.mp], 159 REPEAT o eresolve_tac ctxt [Data.conjE], 160 REPEAT o ares_tac ctxt [Data.conjI]]); 161 val allcomm = Data.all_comm RS Data.iff_trans; 162in 163 fun prove_one_point_all_tac ctxt = 164 EVERY1 [qcomm_tac ctxt allcomm Data.iff_allI, 165 resolve_tac ctxt [Data.iff_allI], 166 resolve_tac ctxt [Data.iffI], tac ctxt, tac ctxt]; 167end 168 169fun renumber l u (Bound i) = 170 Bound (if i < l orelse i > u then i else if i = u then l else i + 1) 171 | renumber l u (s $ t) = renumber l u s $ renumber l u t 172 | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t) 173 | renumber _ _ atom = atom; 174 175fun quantify qC x T xs P = 176 let 177 fun quant [] P = P 178 | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P)); 179 val n = length xs; 180 val Q = if n = 0 then P else renumber 0 n P; 181 in quant xs (qC $ Abs (x, T, Q)) end; 182 183fun rearrange_all ctxt ct = 184 (case Thm.term_of ct of 185 F as (all as Const (q, _)) $ Abs (x, T, P) => 186 (case extract_quant extract_imp q P of 187 NONE => NONE 188 | SOME (xs, eq, Q) => 189 let val R = quantify all x T xs (Data.imp $ eq $ Q) 190 in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end) 191 | _ => NONE); 192 193fun rearrange_ball tac ctxt ct = 194 (case Thm.term_of ct of 195 F as Ball $ A $ Abs (x, T, P) => 196 (case extract_imp true [] P of 197 NONE => NONE 198 | SOME (xs, eq, Q) => 199 if not (null xs) then NONE 200 else 201 let val R = Data.imp $ eq $ Q 202 in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end) 203 | _ => NONE); 204 205fun rearrange_ex ctxt ct = 206 (case Thm.term_of ct of 207 F as (ex as Const (q, _)) $ Abs (x, T, P) => 208 (case extract_quant extract_conj q P of 209 NONE => NONE 210 | SOME (xs, eq, Q) => 211 let val R = quantify ex x T xs (Data.conj $ eq $ Q) 212 in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end) 213 | _ => NONE); 214 215fun rearrange_bex tac ctxt ct = 216 (case Thm.term_of ct of 217 F as Bex $ A $ Abs (x, T, P) => 218 (case extract_conj true [] P of 219 NONE => NONE 220 | SOME (xs, eq, Q) => 221 if not (null xs) then NONE 222 else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac)) 223 | _ => NONE); 224 225fun rearrange_Collect tac ctxt ct = 226 (case Thm.term_of ct of 227 F as Collect $ Abs (x, T, P) => 228 (case extract_conj true [] P of 229 NONE => NONE 230 | SOME (_, eq, Q) => 231 let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) 232 in SOME (prove_conv ctxt (F, R) tac) end) 233 | _ => NONE); 234 235end; 236 237