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_All: Proof.context -> cterm -> thm option 71 val rearrange_ex: Proof.context -> cterm -> thm option 72 val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option 73 val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option 74 val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option 75end; 76 77functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 = 78struct 79 80(* FIXME: only test! *) 81fun def xs eq = 82 (case Data.dest_eq eq of 83 SOME (s, t) => 84 let val n = length xs in 85 s = Bound n andalso not (loose_bvar1 (t, n)) orelse 86 t = Bound n andalso not (loose_bvar1 (s, n)) 87 end 88 | NONE => false); 89 90fun extract_conj fst xs t = 91 (case Data.dest_conj t of 92 NONE => NONE 93 | SOME (P, Q) => 94 if def xs P then (if fst then NONE else SOME (xs, P, Q)) 95 else if def xs Q then SOME (xs, Q, P) 96 else 97 (case extract_conj false xs P of 98 SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q) 99 | NONE => 100 (case extract_conj false xs Q of 101 SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q') 102 | NONE => NONE))); 103 104fun extract_imp fst xs t = 105 (case Data.dest_imp t of 106 NONE => NONE 107 | SOME (P, Q) => 108 if def xs P then (if fst then NONE else SOME (xs, P, Q)) 109 else 110 (case extract_conj false xs P of 111 SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q) 112 | NONE => 113 (case extract_imp false xs Q of 114 NONE => NONE 115 | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q')))); 116 117fun extract_conj_from_judgment ctxt fst xs t = 118 if Object_Logic.is_judgment ctxt t 119 then 120 (case extract_conj fst xs (Object_Logic.drop_judgment ctxt t) of 121 NONE => NONE 122 | SOME (xs, eq, P) => SOME (xs, Object_Logic.ensure_propT ctxt eq, Object_Logic.ensure_propT ctxt P)) 123 else NONE; 124 125fun extract_implies ctxt fst xs t = 126 (case try Logic.dest_implies t of 127 NONE => NONE 128 | SOME (P, Q) => 129 if def xs P then (if fst then NONE else SOME (xs, P, Q)) 130 else 131 (case extract_conj_from_judgment ctxt false xs P of 132 SOME (xs, eq, P') => SOME (xs, eq, Logic.implies $ P' $ Q) 133 | NONE => 134 (case extract_implies ctxt false xs Q of 135 NONE => NONE 136 | SOME (xs, eq, Q') => (SOME (xs, eq, Logic.implies $ P $ Q'))))); 137 138fun extract_quant ctxt extract q = 139 let 140 fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) = 141 if qa = q then exqu ((qC, x, T) :: xs) Q else NONE 142 | exqu xs P = extract ctxt (null xs) xs P 143 in exqu [] end; 144 145fun iff_reflection_tac ctxt = 146 resolve_tac ctxt [Data.iff_reflection] 1; 147 148fun qcomm_tac ctxt qcomm qI i = 149 REPEAT_DETERM (resolve_tac ctxt [qcomm] i THEN resolve_tac ctxt [qI] i); 150 151(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) 152 Better: instantiate exI 153*) 154local 155 val excomm = Data.ex_comm RS Data.iff_trans; 156in 157 fun prove_one_point_ex_tac ctxt = 158 qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN 159 ALLGOALS 160 (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE], 161 resolve_tac ctxt [Data.exI], 162 DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]]) 163end; 164 165(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) = 166 (! x1..xn x0. x0 = t --> (... & ...) --> P x0) 167*) 168local 169 fun tac ctxt = 170 SELECT_GOAL 171 (EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry], 172 REPEAT o resolve_tac ctxt [Data.impI], 173 eresolve_tac ctxt [Data.mp], 174 REPEAT o eresolve_tac ctxt [Data.conjE], 175 REPEAT o ares_tac ctxt [Data.conjI]]); 176 val all_comm = Data.all_comm RS Data.iff_trans; 177 val All_comm = @{thm swap_params [THEN transitive]}; 178in 179 fun prove_one_point_all_tac ctxt = 180 EVERY1 [qcomm_tac ctxt all_comm Data.iff_allI, 181 resolve_tac ctxt [Data.iff_allI], 182 resolve_tac ctxt [Data.iffI], 183 tac ctxt, 184 tac ctxt]; 185 fun prove_one_point_All_tac ctxt = 186 EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI}, 187 resolve_tac ctxt [@{thm equal_allI}], 188 resolve_tac ctxt [@{thm equal_intr_rule}], 189 Object_Logic.atomize_prems_tac ctxt, 190 tac ctxt, 191 Object_Logic.atomize_prems_tac ctxt, 192 tac ctxt]; 193end 194 195fun prove_conv ctxt tu tac = 196 let 197 val (goal, ctxt') = 198 yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt; 199 val thm = 200 Goal.prove ctxt' [] [] goal 201 (fn {context = ctxt'', ...} => tac ctxt''); 202 in singleton (Variable.export ctxt' ctxt) thm end; 203 204fun renumber l u (Bound i) = 205 Bound (if i < l orelse i > u then i else if i = u then l else i + 1) 206 | renumber l u (s $ t) = renumber l u s $ renumber l u t 207 | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t) 208 | renumber _ _ atom = atom; 209 210fun quantify qC x T xs P = 211 let 212 fun quant [] P = P 213 | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P)); 214 val n = length xs; 215 val Q = if n = 0 then P else renumber 0 n P; 216 in quant xs (qC $ Abs (x, T, Q)) end; 217 218fun rearrange_all ctxt ct = 219 (case Thm.term_of ct of 220 F as (all as Const (q, _)) $ Abs (x, T, P) => 221 (case extract_quant ctxt (K extract_imp) q P of 222 NONE => NONE 223 | SOME (xs, eq, Q) => 224 let val R = quantify all x T xs (Data.imp $ eq $ Q) 225 in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_all_tac)) end) 226 | _ => NONE); 227 228fun rearrange_All ctxt ct = 229 (case Thm.term_of ct of 230 F as (all as Const (q, _)) $ Abs (x, T, P) => 231 (case extract_quant ctxt extract_implies q P of 232 NONE => NONE 233 | SOME (xs, eq, Q) => 234 let val R = quantify all x T xs (Logic.implies $ eq $ Q) 235 in SOME (prove_conv ctxt (F, R) prove_one_point_All_tac) end) 236 | _ => NONE); 237 238fun rearrange_ball tac ctxt ct = 239 (case Thm.term_of ct of 240 F as Ball $ A $ Abs (x, T, P) => 241 (case extract_imp true [] P of 242 NONE => NONE 243 | SOME (xs, eq, Q) => 244 if not (null xs) then NONE 245 else 246 let val R = Data.imp $ eq $ Q 247 in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) (iff_reflection_tac THEN' tac)) end) 248 | _ => NONE); 249 250fun rearrange_ex ctxt ct = 251 (case Thm.term_of ct of 252 F as (ex as Const (q, _)) $ Abs (x, T, P) => 253 (case extract_quant ctxt (K extract_conj) q P of 254 NONE => NONE 255 | SOME (xs, eq, Q) => 256 let val R = quantify ex x T xs (Data.conj $ eq $ Q) 257 in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_ex_tac)) end) 258 | _ => NONE); 259 260fun rearrange_bex tac ctxt ct = 261 (case Thm.term_of ct of 262 F as Bex $ A $ Abs (x, T, P) => 263 (case extract_conj true [] P of 264 NONE => NONE 265 | SOME (xs, eq, Q) => 266 if not (null xs) then NONE 267 else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) (iff_reflection_tac THEN' tac))) 268 | _ => NONE); 269 270fun rearrange_Collect tac ctxt ct = 271 (case Thm.term_of ct of 272 F as Collect $ Abs (x, T, P) => 273 (case extract_conj true [] P of 274 NONE => NONE 275 | SOME (_, eq, Q) => 276 let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) 277 in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' tac)) end) 278 | _ => NONE); 279 280end; 281 282