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;