src/Provers/quantifier1.ML
changeset 12523 0d8d5bf549b0
parent 11232 558a4feebb04
child 13480 bb72bd43c6c3
     1.1 --- a/src/Provers/quantifier1.ML	Mon Dec 17 13:25:18 2001 +0100
     1.2 +++ b/src/Provers/quantifier1.ML	Mon Dec 17 14:21:59 2001 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    (*rules*)
     1.5    val iff_reflection: thm (* P <-> Q ==> P == Q *)
     1.6    val iffI:  thm
     1.7 +  val iff_trans: thm
     1.8    val conjI: thm
     1.9    val conjE: thm
    1.10    val impI:  thm
    1.11 @@ -47,6 +48,9 @@
    1.12    val exE:   thm
    1.13    val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
    1.14    val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
    1.15 +  val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
    1.16 +  val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
    1.17 +  val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
    1.18  end;
    1.19  
    1.20  signature QUANTIFIER1 =
    1.21 @@ -65,30 +69,39 @@
    1.22  open Data;
    1.23  
    1.24  (* FIXME: only test! *)
    1.25 -fun def eq = case dest_eq eq of
    1.26 +fun def xs eq =
    1.27 +  let val n = length xs
    1.28 +  in case dest_eq eq of
    1.29        Some(c,s,t) =>
    1.30 -        s = Bound 0 andalso not(loose_bvar1(t,0)) orelse
    1.31 -        t = Bound 0 andalso not(loose_bvar1(s,0))
    1.32 -    | None => false;
    1.33 +        s = Bound n andalso not(loose_bvar1(t,n)) orelse
    1.34 +        t = Bound n andalso not(loose_bvar1(s,n))
    1.35 +    | None => false
    1.36 +  end;
    1.37  
    1.38 -fun extract_conj t = case dest_conj t of None => None
    1.39 +fun extract_conj xs t = case dest_conj t of None => None
    1.40      | Some(conj,P,Q) =>
    1.41 -        (if def P then Some(P,Q) else
    1.42 -         if def Q then Some(Q,P) else
    1.43 -         (case extract_conj P of
    1.44 -            Some(eq,P') => Some(eq, conj $ P' $ Q)
    1.45 -          | None => (case extract_conj Q of
    1.46 -                       Some(eq,Q') => Some(eq,conj $ P $ Q')
    1.47 +        (if def xs P then Some(xs,P,Q) else
    1.48 +         if def xs Q then Some(xs,Q,P) else
    1.49 +         (case extract_conj xs P of
    1.50 +            Some(xs,eq,P') => Some(xs,eq, conj $ P' $ Q)
    1.51 +          | None => (case extract_conj xs Q of
    1.52 +                       Some(xs,eq,Q') => Some(xs,eq,conj $ P $ Q')
    1.53                       | None => None)));
    1.54  
    1.55 -fun extract_imp t = case dest_imp t of None => None
    1.56 -    | Some(imp,P,Q) => if def P then Some(P,Q)
    1.57 -                       else (case extract_conj P of
    1.58 -                               Some(eq,P') => Some(eq, imp $ P' $ Q)
    1.59 -                             | None => (case extract_imp Q of
    1.60 +fun extract_imp xs t = case dest_imp t of None => None
    1.61 +    | Some(imp,P,Q) => if def xs P then Some(xs,P,Q)
    1.62 +                       else (case extract_conj xs P of
    1.63 +                               Some(xs,eq,P') => Some(xs, eq, imp $ P' $ Q)
    1.64 +                             | None => (case extract_imp xs Q of
    1.65                                            None => None
    1.66 -                                        | Some(eq,Q') => Some(eq, imp$P$Q')));
    1.67 -    
    1.68 +                                        | Some(xs,eq,Q') =>
    1.69 +                                            Some(xs,eq,imp$P$Q')));
    1.70 +
    1.71 +fun extract_quant extract q =
    1.72 +  let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
    1.73 +            if qa = q then exqu ((qC,x,T)::xs) Q else None
    1.74 +        | exqu xs P = extract xs P
    1.75 +  in exqu end;
    1.76  
    1.77  fun prove_conv tac sg tu =
    1.78    let val meta_eq = cterm_of sg (Logic.mk_equals tu)
    1.79 @@ -98,51 +111,73 @@
    1.80                    string_of_cterm meta_eq)
    1.81    end;
    1.82  
    1.83 -(* Proves (? x. ... & x = t & ...) = (? x. x = t & ... & ...)
    1.84 +fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
    1.85 +
    1.86 +(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
    1.87     Better: instantiate exI
    1.88  *)
    1.89 -val prove_one_point_ex_tac = rtac iffI 1 THEN
    1.90 +local
    1.91 +val excomm = ex_comm RS iff_trans
    1.92 +in
    1.93 +val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
    1.94      ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
    1.95 -                    DEPTH_SOLVE_1 o (ares_tac [conjI])]);
    1.96 +                    DEPTH_SOLVE_1 o (ares_tac [conjI])])
    1.97 +end;
    1.98  
    1.99 -(* Proves (! x. (... & x = t & ...) --> P x) =
   1.100 -          (! x. x = t --> (... & ...) --> P x)
   1.101 +(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
   1.102 +          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
   1.103  *)
   1.104  local
   1.105  val tac = SELECT_GOAL
   1.106            (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
   1.107                    REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
   1.108 +val allcomm = all_comm RS iff_trans
   1.109  in
   1.110 -val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]
   1.111 +val prove_one_point_all_tac =
   1.112 +      EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
   1.113  end
   1.114  
   1.115 -fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =
   1.116 -     (case extract_imp P of
   1.117 +fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
   1.118 +                                   if i=u then l else i+1)
   1.119 +  | renumber l u (s$t) = renumber l u s $ renumber l u t
   1.120 +  | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
   1.121 +  | renumber _ _ atom = atom;
   1.122 +
   1.123 +fun quantify qC x T xs P =
   1.124 +  let fun quant [] P = P
   1.125 +        | quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P))
   1.126 +      val n = length xs
   1.127 +      val Q = if n=0 then P else renumber 0 n P
   1.128 +  in quant xs (qC $ Abs(x,T,Q)) end;
   1.129 +
   1.130 +fun rearrange_all sg _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
   1.131 +     (case extract_quant extract_imp q [] P of
   1.132          None => None
   1.133 -      | Some(eq,Q) =>
   1.134 -          let val R = imp $ eq $ Q
   1.135 -          in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)
   1.136 +      | Some(xs,eq,Q) =>
   1.137 +          let val R = quantify all x T xs (imp $ eq $ Q)
   1.138 +          in Some(prove_conv prove_one_point_all_tac sg (F,R)) end)
   1.139    | rearrange_all _ _ _ = None;
   1.140  
   1.141  fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
   1.142 -     (case extract_imp P of
   1.143 +     (case extract_imp [] P of
   1.144          None => None
   1.145 -      | Some(eq,Q) =>
   1.146 +      | Some(xs,eq,Q) => if not(null xs) then None else
   1.147            let val R = imp $ eq $ Q
   1.148            in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
   1.149    | rearrange_ball _ _ _ _ = None;
   1.150  
   1.151 -fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
   1.152 -     (case extract_conj P of
   1.153 +fun rearrange_ex sg _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
   1.154 +     (case extract_quant extract_conj q [] P of
   1.155          None => None
   1.156 -      | Some(eq,Q) =>
   1.157 -          Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
   1.158 +      | Some(xs,eq,Q) =>
   1.159 +          let val R = quantify ex x T xs (conj $ eq $ Q)
   1.160 +          in Some(prove_conv prove_one_point_ex_tac sg (F,R)) end)
   1.161    | rearrange_ex _ _ _ = None;
   1.162  
   1.163  fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
   1.164 -     (case extract_conj P of
   1.165 +     (case extract_conj [] P of
   1.166          None => None
   1.167 -      | Some(eq,Q) =>
   1.168 +      | Some(xs,eq,Q) => if not(null xs) then None else
   1.169            Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
   1.170    | rearrange_bex _ _ _ _ = None;
   1.171