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