src/Provers/quantifier1.ML
 author nipkow Sat May 16 11:28:02 2009 +0200 (2009-05-16) changeset 31166 a90fe83f58ea parent 20049 f48c4a3a34bc child 31197 c1c163ec6c44 permissions -rw-r--r--
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".
 nipkow@4319 ` 1` ```(* Title: Provers/quantifier1 ``` nipkow@4319 ` 2` ``` ID: \$Id\$ ``` nipkow@4319 ` 3` ``` Author: Tobias Nipkow ``` nipkow@4319 ` 4` ``` Copyright 1997 TU Munich ``` nipkow@4319 ` 5` nipkow@4319 ` 6` ```Simplification procedures for turning ``` nipkow@4319 ` 7` nipkow@4319 ` 8` ``` ? x. ... & x = t & ... ``` nipkow@4319 ` 9` ``` into ? x. x = t & ... & ... ``` nipkow@11232 ` 10` ``` where the `? x. x = t &' in the latter formula must be eliminated ``` nipkow@4319 ` 11` ``` by ordinary simplification. ``` nipkow@4319 ` 12` nipkow@4319 ` 13` ``` and ! x. (... & x = t & ...) --> P x ``` nipkow@4319 ` 14` ``` into ! x. x = t --> (... & ...) --> P x ``` nipkow@4319 ` 15` ``` where the `!x. x=t -->' in the latter formula is eliminated ``` nipkow@4319 ` 16` ``` by ordinary simplification. ``` nipkow@4319 ` 17` nipkow@11232 ` 18` ``` And analogously for t=x, but the eqn is not turned around! ``` nipkow@11232 ` 19` nipkow@4319 ` 20` ``` NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; ``` nipkow@4319 ` 21` ``` "!x. x=t --> P(x)" is covered by the congreunce rule for -->; ``` nipkow@4319 ` 22` ``` "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. ``` nipkow@11232 ` 23` ``` As must be "? x. t=x & P(x)". ``` nipkow@11232 ` 24` ``` ``` nipkow@11221 ` 25` ``` And similarly for the bounded quantifiers. ``` nipkow@11221 ` 26` nipkow@4319 ` 27` ```Gries etc call this the "1 point rules" ``` nipkow@31166 ` 28` nipkow@31166 ` 29` ```The above also works for !x1..xn. and ?x1..xn by moving the defined ``` nipkow@31166 ` 30` ```qunatifier inside first, but not for nested bounded quantifiers. ``` nipkow@31166 ` 31` nipkow@31166 ` 32` ```For set comprehensions the basic permutations ``` nipkow@31166 ` 33` ``` ... & x = t & ... -> x = t & (... & ...) ``` nipkow@31166 ` 34` ``` ... & t = x & ... -> t = x & (... & ...) ``` nipkow@31166 ` 35` ```are also exported. ``` nipkow@31166 ` 36` nipkow@31166 ` 37` ```To avoid looping, NONE is returned if the term cannot be rearranged, ``` nipkow@31166 ` 38` ```esp if x=t/t=x sits at the front already. ``` nipkow@4319 ` 39` ```*) ``` nipkow@4319 ` 40` nipkow@4319 ` 41` ```signature QUANTIFIER1_DATA = ``` nipkow@4319 ` 42` ```sig ``` nipkow@4319 ` 43` ``` (*abstract syntax*) ``` nipkow@4319 ` 44` ``` val dest_eq: term -> (term*term*term)option ``` nipkow@4319 ` 45` ``` val dest_conj: term -> (term*term*term)option ``` nipkow@11232 ` 46` ``` val dest_imp: term -> (term*term*term)option ``` nipkow@4319 ` 47` ``` val conj: term ``` nipkow@4319 ` 48` ``` val imp: term ``` nipkow@4319 ` 49` ``` (*rules*) ``` nipkow@4319 ` 50` ``` val iff_reflection: thm (* P <-> Q ==> P == Q *) ``` nipkow@4319 ` 51` ``` val iffI: thm ``` nipkow@12523 ` 52` ``` val iff_trans: thm ``` nipkow@4319 ` 53` ``` val conjI: thm ``` nipkow@4319 ` 54` ``` val conjE: thm ``` nipkow@4319 ` 55` ``` val impI: thm ``` nipkow@4319 ` 56` ``` val mp: thm ``` nipkow@4319 ` 57` ``` val exI: thm ``` nipkow@4319 ` 58` ``` val exE: thm ``` nipkow@11232 ` 59` ``` val uncurry: thm (* P --> Q --> R ==> P & Q --> R *) ``` nipkow@11232 ` 60` ``` val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *) ``` nipkow@12523 ` 61` ``` val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *) ``` nipkow@12523 ` 62` ``` val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *) ``` nipkow@12523 ` 63` ``` val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *) ``` nipkow@4319 ` 64` ```end; ``` nipkow@4319 ` 65` nipkow@4319 ` 66` ```signature QUANTIFIER1 = ``` nipkow@4319 ` 67` ```sig ``` nipkow@11221 ` 68` ``` val prove_one_point_all_tac: tactic ``` nipkow@11221 ` 69` ``` val prove_one_point_ex_tac: tactic ``` wenzelm@17002 ` 70` ``` val rearrange_all: theory -> simpset -> term -> thm option ``` wenzelm@17002 ` 71` ``` val rearrange_ex: theory -> simpset -> term -> thm option ``` wenzelm@17002 ` 72` ``` val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option ``` wenzelm@17002 ` 73` ``` val rearrange_bex: (simpset -> tactic) -> theory -> simpset -> term -> thm option ``` nipkow@31166 ` 74` ``` val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option ``` nipkow@4319 ` 75` ```end; ``` nipkow@4319 ` 76` nipkow@4319 ` 77` ```functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = ``` nipkow@4319 ` 78` ```struct ``` nipkow@4319 ` 79` nipkow@4319 ` 80` ```open Data; ``` nipkow@4319 ` 81` nipkow@11232 ` 82` ```(* FIXME: only test! *) ``` nipkow@12523 ` 83` ```fun def xs eq = ``` nipkow@31166 ` 84` ``` (case dest_eq eq of ``` nipkow@31166 ` 85` ``` SOME(c,s,t) => ``` nipkow@31166 ` 86` ``` let val n = length xs ``` nipkow@31166 ` 87` ``` in s = Bound n andalso not(loose_bvar1(t,n)) orelse ``` nipkow@31166 ` 88` ``` t = Bound n andalso not(loose_bvar1(s,n)) end ``` nipkow@31166 ` 89` ``` | NONE => false); ``` nipkow@4319 ` 90` nipkow@31166 ` 91` ```fun extract_conj fst xs t = case dest_conj t of NONE => NONE ``` skalberg@15531 ` 92` ``` | SOME(conj,P,Q) => ``` nipkow@31166 ` 93` ``` (if not fst andalso def xs P then SOME(xs,P,Q) else ``` skalberg@15531 ` 94` ``` if def xs Q then SOME(xs,Q,P) else ``` nipkow@31166 ` 95` ``` (case extract_conj false xs P of ``` skalberg@15531 ` 96` ``` SOME(xs,eq,P') => SOME(xs,eq, conj \$ P' \$ Q) ``` nipkow@31166 ` 97` ``` | NONE => (case extract_conj false xs Q of ``` skalberg@15531 ` 98` ``` SOME(xs,eq,Q') => SOME(xs,eq,conj \$ P \$ Q') ``` skalberg@15531 ` 99` ``` | NONE => NONE))); ``` nipkow@11232 ` 100` nipkow@31166 ` 101` ```fun extract_imp fst xs t = case dest_imp t of NONE => NONE ``` nipkow@31166 ` 102` ``` | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q) ``` nipkow@31166 ` 103` ``` else (case extract_conj false xs P of ``` skalberg@15531 ` 104` ``` SOME(xs,eq,P') => SOME(xs, eq, imp \$ P' \$ Q) ``` nipkow@31166 ` 105` ``` | NONE => (case extract_imp false xs Q of ``` skalberg@15531 ` 106` ``` NONE => NONE ``` skalberg@15531 ` 107` ``` | SOME(xs,eq,Q') => ``` skalberg@15531 ` 108` ``` SOME(xs,eq,imp\$P\$Q'))); ``` nipkow@12523 ` 109` nipkow@12523 ` 110` ```fun extract_quant extract q = ``` nipkow@12523 ` 111` ``` let fun exqu xs ((qC as Const(qa,_)) \$ Abs(x,T,Q)) = ``` skalberg@15531 ` 112` ``` if qa = q then exqu ((qC,x,T)::xs) Q else NONE ``` nipkow@31166 ` 113` ``` | exqu xs P = extract (null xs) xs P ``` nipkow@31166 ` 114` ``` in exqu [] end; ``` nipkow@4319 ` 115` wenzelm@17002 ` 116` ```fun prove_conv tac thy tu = ``` wenzelm@20049 ` 117` ``` Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) ``` wenzelm@20049 ` 118` ``` (K (rtac iff_reflection 1 THEN tac)); ``` nipkow@4319 ` 119` nipkow@12523 ` 120` ```fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) ``` nipkow@12523 ` 121` nipkow@12523 ` 122` ```(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) ``` nipkow@11221 ` 123` ``` Better: instantiate exI ``` nipkow@11221 ` 124` ```*) ``` nipkow@12523 ` 125` ```local ``` nipkow@12523 ` 126` ```val excomm = ex_comm RS iff_trans ``` nipkow@12523 ` 127` ```in ``` nipkow@12523 ` 128` ```val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN ``` nipkow@11221 ` 129` ``` ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI, ``` nipkow@12523 ` 130` ``` DEPTH_SOLVE_1 o (ares_tac [conjI])]) ``` nipkow@12523 ` 131` ```end; ``` nipkow@11221 ` 132` nipkow@12523 ` 133` ```(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) = ``` nipkow@12523 ` 134` ``` (! x1..xn x0. x0 = t --> (... & ...) --> P x0) ``` nipkow@11221 ` 135` ```*) ``` nipkow@11232 ` 136` ```local ``` nipkow@11232 ` 137` ```val tac = SELECT_GOAL ``` nipkow@11232 ` 138` ``` (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp, ``` nipkow@11232 ` 139` ``` REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])]) ``` nipkow@12523 ` 140` ```val allcomm = all_comm RS iff_trans ``` nipkow@11232 ` 141` ```in ``` nipkow@12523 ` 142` ```val prove_one_point_all_tac = ``` nipkow@12523 ` 143` ``` EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac] ``` nipkow@11232 ` 144` ```end ``` nipkow@4319 ` 145` nipkow@12523 ` 146` ```fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else ``` nipkow@12523 ` 147` ``` if i=u then l else i+1) ``` nipkow@12523 ` 148` ``` | renumber l u (s\$t) = renumber l u s \$ renumber l u t ``` nipkow@12523 ` 149` ``` | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t) ``` nipkow@12523 ` 150` ``` | renumber _ _ atom = atom; ``` nipkow@12523 ` 151` nipkow@12523 ` 152` ```fun quantify qC x T xs P = ``` nipkow@12523 ` 153` ``` let fun quant [] P = P ``` nipkow@12523 ` 154` ``` | quant ((qC,x,T)::xs) P = quant xs (qC \$ Abs(x,T,P)) ``` nipkow@12523 ` 155` ``` val n = length xs ``` nipkow@12523 ` 156` ``` val Q = if n=0 then P else renumber 0 n P ``` nipkow@12523 ` 157` ``` in quant xs (qC \$ Abs(x,T,Q)) end; ``` nipkow@12523 ` 158` wenzelm@17002 ` 159` ```fun rearrange_all thy _ (F as (all as Const(q,_)) \$ Abs(x,T, P)) = ``` nipkow@31166 ` 160` ``` (case extract_quant extract_imp q P of ``` skalberg@15531 ` 161` ``` NONE => NONE ``` skalberg@15531 ` 162` ``` | SOME(xs,eq,Q) => ``` nipkow@12523 ` 163` ``` let val R = quantify all x T xs (imp \$ eq \$ Q) ``` wenzelm@17002 ` 164` ``` in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end) ``` skalberg@15531 ` 165` ``` | rearrange_all _ _ _ = NONE; ``` nipkow@4319 ` 166` wenzelm@17002 ` 167` ```fun rearrange_ball tac thy ss (F as Ball \$ A \$ Abs(x,T,P)) = ``` nipkow@31166 ` 168` ``` (case extract_imp true [] P of ``` skalberg@15531 ` 169` ``` NONE => NONE ``` skalberg@15531 ` 170` ``` | SOME(xs,eq,Q) => if not(null xs) then NONE else ``` nipkow@11232 ` 171` ``` let val R = imp \$ eq \$ Q ``` wenzelm@17002 ` 172` ``` in SOME(prove_conv (tac ss) thy (F,Ball \$ A \$ Abs(x,T,R))) end) ``` skalberg@15531 ` 173` ``` | rearrange_ball _ _ _ _ = NONE; ``` nipkow@4319 ` 174` wenzelm@17002 ` 175` ```fun rearrange_ex thy _ (F as (ex as Const(q,_)) \$ Abs(x,T,P)) = ``` nipkow@31166 ` 176` ``` (case extract_quant extract_conj q P of ``` skalberg@15531 ` 177` ``` NONE => NONE ``` skalberg@15531 ` 178` ``` | SOME(xs,eq,Q) => ``` nipkow@12523 ` 179` ``` let val R = quantify ex x T xs (conj \$ eq \$ Q) ``` wenzelm@17002 ` 180` ``` in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end) ``` skalberg@15531 ` 181` ``` | rearrange_ex _ _ _ = NONE; ``` nipkow@4319 ` 182` wenzelm@17002 ` 183` ```fun rearrange_bex tac thy ss (F as Bex \$ A \$ Abs(x,T,P)) = ``` nipkow@31166 ` 184` ``` (case extract_conj true [] P of ``` skalberg@15531 ` 185` ``` NONE => NONE ``` skalberg@15531 ` 186` ``` | SOME(xs,eq,Q) => if not(null xs) then NONE else ``` wenzelm@17002 ` 187` ``` SOME(prove_conv (tac ss) thy (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q)))) ``` skalberg@15531 ` 188` ``` | rearrange_bex _ _ _ _ = NONE; ``` nipkow@11221 ` 189` nipkow@31166 ` 190` ```fun rearrange_Coll tac thy _ (F as Coll \$ Abs(x,T,P)) = ``` nipkow@31166 ` 191` ``` (case extract_conj true [] P of ``` nipkow@31166 ` 192` ``` NONE => NONE ``` nipkow@31166 ` 193` ``` | SOME(_,eq,Q) => ``` nipkow@31166 ` 194` ``` let val R = Coll \$ Abs(x,T, conj \$ eq \$ Q) ``` nipkow@31166 ` 195` ``` in SOME(prove_conv tac thy (F,R)) end); ``` nipkow@31166 ` 196` nipkow@4319 ` 197` ```end; ```