src/Provers/quantifier1.ML
 changeset 31166 a90fe83f58ea parent 20049 f48c4a3a34bc child 31197 c1c163ec6c44
```     1.1 --- a/src/Provers/quantifier1.ML	Fri May 15 10:01:57 2009 +0200
1.2 +++ b/src/Provers/quantifier1.ML	Sat May 16 11:28:02 2009 +0200
1.3 @@ -21,11 +21,21 @@
1.4          "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
1.5          "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
1.6          As must be "? x. t=x & P(x)".
1.7 -
1.8
1.9       And similarly for the bounded quantifiers.
1.10
1.11  Gries etc call this the "1 point rules"
1.12 +
1.13 +The above also works for !x1..xn. and ?x1..xn by moving the defined
1.14 +qunatifier inside first, but not for nested bounded quantifiers.
1.15 +
1.16 +For set comprehensions the basic permutations
1.17 +      ... & x = t & ...  ->  x = t & (... & ...)
1.18 +      ... & t = x & ...  ->  t = x & (... & ...)
1.19 +are also exported.
1.20 +
1.21 +To avoid looping, NONE is returned if the term cannot be rearranged,
1.22 +esp if x=t/t=x sits at the front already.
1.23  *)
1.24
1.25  signature QUANTIFIER1_DATA =
1.26 @@ -61,6 +71,7 @@
1.27    val rearrange_ex:  theory -> simpset -> term -> thm option
1.28    val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
1.29    val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
1.30 +  val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
1.31  end;
1.32
1.33  functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
1.34 @@ -70,29 +81,28 @@
1.35
1.36  (* FIXME: only test! *)
1.37  fun def xs eq =
1.38 -  let val n = length xs
1.39 -  in case dest_eq eq of
1.40 -      SOME(c,s,t) =>
1.41 -        s = Bound n andalso not(loose_bvar1(t,n)) orelse
1.42 -        t = Bound n andalso not(loose_bvar1(s,n))
1.43 -    | NONE => false
1.44 -  end;
1.45 +  (case dest_eq eq of
1.46 +     SOME(c,s,t) =>
1.47 +       let val n = length xs
1.48 +       in s = Bound n andalso not(loose_bvar1(t,n)) orelse
1.49 +          t = Bound n andalso not(loose_bvar1(s,n)) end
1.50 +   | NONE => false);
1.51
1.52 -fun extract_conj xs t = case dest_conj t of NONE => NONE
1.53 +fun extract_conj fst xs t = case dest_conj t of NONE => NONE
1.54      | SOME(conj,P,Q) =>
1.55 -        (if def xs P then SOME(xs,P,Q) else
1.56 +        (if not fst andalso def xs P then SOME(xs,P,Q) else
1.57           if def xs Q then SOME(xs,Q,P) else
1.58 -         (case extract_conj xs P of
1.59 +         (case extract_conj false xs P of
1.60              SOME(xs,eq,P') => SOME(xs,eq, conj \$ P' \$ Q)
1.61 -          | NONE => (case extract_conj xs Q of
1.62 +          | NONE => (case extract_conj false xs Q of
1.63                         SOME(xs,eq,Q') => SOME(xs,eq,conj \$ P \$ Q')
1.64                       | NONE => NONE)));
1.65
1.66 -fun extract_imp xs t = case dest_imp t of NONE => NONE
1.67 -    | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q)
1.68 -                       else (case extract_conj xs P of
1.69 +fun extract_imp fst xs t = case dest_imp t of NONE => NONE
1.70 +    | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
1.71 +                       else (case extract_conj false xs P of
1.72                                 SOME(xs,eq,P') => SOME(xs, eq, imp \$ P' \$ Q)
1.73 -                             | NONE => (case extract_imp xs Q of
1.74 +                             | NONE => (case extract_imp false xs Q of
1.75                                            NONE => NONE
1.76                                          | SOME(xs,eq,Q') =>
1.77                                              SOME(xs,eq,imp\$P\$Q')));
1.78 @@ -100,8 +110,8 @@
1.79  fun extract_quant extract q =
1.80    let fun exqu xs ((qC as Const(qa,_)) \$ Abs(x,T,Q)) =
1.81              if qa = q then exqu ((qC,x,T)::xs) Q else NONE
1.82 -        | exqu xs P = extract xs P
1.83 -  in exqu end;
1.84 +        | exqu xs P = extract (null xs) xs P
1.85 +  in exqu [] end;
1.86
1.87  fun prove_conv tac thy tu =
1.88    Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
1.89 @@ -147,7 +157,7 @@
1.90    in quant xs (qC \$ Abs(x,T,Q)) end;
1.91
1.92  fun rearrange_all thy _ (F as (all as Const(q,_)) \$ Abs(x,T, P)) =
1.93 -     (case extract_quant extract_imp q [] P of
1.94 +     (case extract_quant extract_imp q P of
1.95          NONE => NONE
1.96        | SOME(xs,eq,Q) =>
1.97            let val R = quantify all x T xs (imp \$ eq \$ Q)
1.98 @@ -155,7 +165,7 @@
1.99    | rearrange_all _ _ _ = NONE;
1.100
1.101  fun rearrange_ball tac thy ss (F as Ball \$ A \$ Abs(x,T,P)) =
1.102 -     (case extract_imp [] P of
1.103 +     (case extract_imp true [] P of
1.104          NONE => NONE
1.105        | SOME(xs,eq,Q) => if not(null xs) then NONE else
1.106            let val R = imp \$ eq \$ Q
1.107 @@ -163,7 +173,7 @@
1.108    | rearrange_ball _ _ _ _ = NONE;
1.109
1.110  fun rearrange_ex thy _ (F as (ex as Const(q,_)) \$ Abs(x,T,P)) =
1.111 -     (case extract_quant extract_conj q [] P of
1.112 +     (case extract_quant extract_conj q P of
1.113          NONE => NONE
1.114        | SOME(xs,eq,Q) =>
1.115            let val R = quantify ex x T xs (conj \$ eq \$ Q)
1.116 @@ -171,10 +181,17 @@
1.117    | rearrange_ex _ _ _ = NONE;
1.118
1.119  fun rearrange_bex tac thy ss (F as Bex \$ A \$ Abs(x,T,P)) =
1.120 -     (case extract_conj [] P of
1.121 +     (case extract_conj true [] P of
1.122          NONE => NONE
1.123        | SOME(xs,eq,Q) => if not(null xs) then NONE else
1.124            SOME(prove_conv (tac ss) thy (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
1.125    | rearrange_bex _ _ _ _ = NONE;
1.126
1.127 +fun rearrange_Coll tac thy _ (F as Coll \$ Abs(x,T,P)) =
1.128 +     (case extract_conj true [] P of
1.129 +        NONE => NONE
1.130 +      | SOME(_,eq,Q) =>
1.131 +          let val R = Coll \$ Abs(x,T, conj \$ eq \$ Q)
1.132 +          in SOME(prove_conv tac thy (F,R)) end);
1.133 +
1.134  end;
```