src/Provers/quantifier1.ML
changeset 42458 5dfae6d348fd
parent 42457 de868abd131e
child 42459 38b9f023cc34
     1.1 --- a/src/Provers/quantifier1.ML	Fri Apr 22 14:38:49 2011 +0200
     1.2 +++ b/src/Provers/quantifier1.ML	Fri Apr 22 14:53:11 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4              ? x. ... & x = t & ...
     1.5       into   ? x. x = t & ... & ...
     1.6       where the `? x. x = t &' in the latter formula must be eliminated
     1.7 -           by ordinary simplification. 
     1.8 +           by ordinary simplification.
     1.9  
    1.10       and   ! x. (... & x = t & ...) --> P x
    1.11       into  ! x. x = t --> (... & ...) --> P x
    1.12 @@ -20,7 +20,7 @@
    1.13          "!x. x=t --> P(x)" is covered by the congruence rule for -->;
    1.14          "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
    1.15          As must be "? x. t=x & P(x)".
    1.16 -        
    1.17 +
    1.18       And similarly for the bounded quantifiers.
    1.19  
    1.20  Gries etc call this the "1 point rules"
    1.21 @@ -40,21 +40,21 @@
    1.22  signature QUANTIFIER1_DATA =
    1.23  sig
    1.24    (*abstract syntax*)
    1.25 -  val dest_eq: term -> (term*term*term)option
    1.26 -  val dest_conj: term -> (term*term*term)option
    1.27 -  val dest_imp:  term -> (term*term*term)option
    1.28 +  val dest_eq: term -> (term * term * term) option
    1.29 +  val dest_conj: term -> (term * term * term) option
    1.30 +  val dest_imp: term -> (term * term * term) option
    1.31    val conj: term
    1.32 -  val imp:  term
    1.33 +  val imp: term
    1.34    (*rules*)
    1.35    val iff_reflection: thm (* P <-> Q ==> P == Q *)
    1.36 -  val iffI:  thm
    1.37 +  val iffI: thm
    1.38    val iff_trans: thm
    1.39    val conjI: thm
    1.40    val conjE: thm
    1.41 -  val impI:  thm
    1.42 -  val mp:    thm
    1.43 -  val exI:   thm
    1.44 -  val exE:   thm
    1.45 +  val impI: thm
    1.46 +  val mp: thm
    1.47 +  val exI: thm
    1.48 +  val exE: thm
    1.49    val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
    1.50    val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
    1.51    val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
    1.52 @@ -73,41 +73,51 @@
    1.53    val rearrange_Collect: tactic -> simpset -> term -> thm option
    1.54  end;
    1.55  
    1.56 -functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    1.57 +functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    1.58  struct
    1.59  
    1.60  (* FIXME: only test! *)
    1.61  fun def xs eq =
    1.62    (case Data.dest_eq eq of
    1.63 -     SOME(c,s,t) =>
    1.64 -       let val n = length xs
    1.65 -       in s = Bound n andalso not(loose_bvar1(t,n)) orelse
    1.66 -          t = Bound n andalso not(loose_bvar1(s,n)) end
    1.67 -   | NONE => false);
    1.68 +    SOME (c, s, t) =>
    1.69 +      let val n = length xs in
    1.70 +        s = Bound n andalso not (loose_bvar1 (t, n)) orelse
    1.71 +        t = Bound n andalso not (loose_bvar1 (s, n))
    1.72 +      end
    1.73 +  | NONE => false);
    1.74  
    1.75 -fun extract_conj fst xs t = case Data.dest_conj t of NONE => NONE
    1.76 -    | SOME(conj,P,Q) =>
    1.77 -        (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
    1.78 -         if def xs Q then SOME(xs,Q,P) else
    1.79 -         (case extract_conj false xs P of
    1.80 -            SOME(xs,eq,P') => SOME(xs,eq, Data.conj $ P' $ Q)
    1.81 -          | NONE => (case extract_conj false xs Q of
    1.82 -                       SOME(xs,eq,Q') => SOME(xs,eq,Data.conj $ P $ Q')
    1.83 -                     | NONE => NONE)));
    1.84 +fun extract_conj fst xs t =
    1.85 +  (case Data.dest_conj t of
    1.86 +    NONE => NONE
    1.87 +  | SOME (conj, P, Q) =>
    1.88 +      if def xs P then (if fst then NONE else SOME (xs, P, Q))
    1.89 +      else if def xs Q then SOME (xs, Q, P)
    1.90 +      else
    1.91 +        (case extract_conj false xs P of
    1.92 +          SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q)
    1.93 +        | NONE =>
    1.94 +            (case extract_conj false xs Q of
    1.95 +              SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q')
    1.96 +            | NONE => NONE)));
    1.97  
    1.98 -fun extract_imp fst xs t = case Data.dest_imp t of NONE => NONE
    1.99 -    | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
   1.100 -                       else (case extract_conj false xs P of
   1.101 -                               SOME(xs,eq,P') => SOME(xs, eq, Data.imp $ P' $ Q)
   1.102 -                             | NONE => (case extract_imp false xs Q of
   1.103 -                                          NONE => NONE
   1.104 -                                        | SOME(xs,eq,Q') =>
   1.105 -                                            SOME(xs,eq,Data.imp$P$Q')));
   1.106 +fun extract_imp fst xs t =
   1.107 +  (case Data.dest_imp t of
   1.108 +    NONE => NONE
   1.109 +  | SOME (imp, P, Q) =>
   1.110 +      if def xs P then (if fst then NONE else SOME (xs, P, Q))
   1.111 +      else
   1.112 +        (case extract_conj false xs P of
   1.113 +          SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q)
   1.114 +        | NONE =>
   1.115 +            (case extract_imp false xs Q of
   1.116 +              NONE => NONE
   1.117 +            | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q'))));
   1.118  
   1.119  fun extract_quant extract q =
   1.120 -  let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
   1.121 -            if qa = q then exqu ((qC,x,T)::xs) Q else NONE
   1.122 -        | exqu xs P = extract (null xs) xs P
   1.123 +  let
   1.124 +    fun exqu xs ((qC as Const(qa, _)) $ Abs (x, T, Q)) =
   1.125 +          if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
   1.126 +      | exqu xs P = extract (null xs) xs P
   1.127    in exqu [] end;
   1.128  
   1.129  fun prove_conv tac ss tu =
   1.130 @@ -119,81 +129,89 @@
   1.131        Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
   1.132    in singleton (Variable.export ctxt' ctxt) thm end;
   1.133  
   1.134 -fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
   1.135 +fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
   1.136  
   1.137  (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
   1.138     Better: instantiate exI
   1.139  *)
   1.140  local
   1.141 -val excomm = Data.ex_comm RS Data.iff_trans
   1.142 +  val excomm = Data.ex_comm RS Data.iff_trans;
   1.143  in
   1.144 -val prove_one_point_ex_tac = qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
   1.145 -    ALLGOALS(EVERY'[etac Data.exE, REPEAT_DETERM o (etac Data.conjE), rtac Data.exI,
   1.146 -                    DEPTH_SOLVE_1 o (ares_tac [Data.conjI])])
   1.147 +  val prove_one_point_ex_tac =
   1.148 +    qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
   1.149 +    ALLGOALS
   1.150 +      (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI,
   1.151 +        DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
   1.152  end;
   1.153  
   1.154  (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
   1.155            (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
   1.156  *)
   1.157  local
   1.158 -val tac = SELECT_GOAL
   1.159 -          (EVERY1[REPEAT o (dtac Data.uncurry), REPEAT o (rtac Data.impI), etac Data.mp,
   1.160 -                  REPEAT o (etac Data.conjE), REPEAT o (ares_tac [Data.conjI])])
   1.161 -val allcomm = Data.all_comm RS Data.iff_trans
   1.162 +  val tac =
   1.163 +    SELECT_GOAL
   1.164 +      (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp,
   1.165 +        REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]);
   1.166 +  val allcomm = Data.all_comm RS Data.iff_trans;
   1.167  in
   1.168 -val prove_one_point_all_tac =
   1.169 -      EVERY1[qcomm_tac allcomm Data.iff_allI,rtac Data.iff_allI, rtac Data.iffI, tac, tac]
   1.170 +  val prove_one_point_all_tac =
   1.171 +    EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac];
   1.172  end
   1.173  
   1.174 -fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
   1.175 -                                   if i=u then l else i+1)
   1.176 -  | renumber l u (s$t) = renumber l u s $ renumber l u t
   1.177 -  | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
   1.178 +fun renumber l u (Bound i) =
   1.179 +      Bound (if i < l orelse i > u then i else if i = u then l else i + 1)
   1.180 +  | renumber l u (s $ t) = renumber l u s $ renumber l u t
   1.181 +  | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t)
   1.182    | renumber _ _ atom = atom;
   1.183  
   1.184  fun quantify qC x T xs P =
   1.185 -  let fun quant [] P = P
   1.186 -        | quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P))
   1.187 -      val n = length xs
   1.188 -      val Q = if n=0 then P else renumber 0 n P
   1.189 -  in quant xs (qC $ Abs(x,T,Q)) end;
   1.190 +  let
   1.191 +    fun quant [] P = P
   1.192 +      | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P));
   1.193 +    val n = length xs;
   1.194 +    val Q = if n = 0 then P else renumber 0 n P;
   1.195 +  in quant xs (qC $ Abs (x, T, Q)) end;
   1.196  
   1.197 -fun rearrange_all ss (F as (all as Const(q,_)) $ Abs(x,T, P)) =
   1.198 -     (case extract_quant extract_imp q P of
   1.199 +fun rearrange_all ss (F as (all as Const (q, _)) $ Abs (x, T, P)) =
   1.200 +      (case extract_quant extract_imp q P of
   1.201          NONE => NONE
   1.202 -      | SOME(xs,eq,Q) =>
   1.203 +      | SOME (xs, eq, Q) =>
   1.204            let val R = quantify all x T xs (Data.imp $ eq $ Q)
   1.205 -          in SOME (prove_conv prove_one_point_all_tac ss (F,R)) end)
   1.206 +          in SOME (prove_conv prove_one_point_all_tac ss (F, R)) end)
   1.207    | rearrange_all _ _ = NONE;
   1.208  
   1.209 -fun rearrange_ball tac ss (F as Ball $ A $ Abs(x,T,P)) =
   1.210 -     (case extract_imp true [] P of
   1.211 +fun rearrange_ball tac ss (F as Ball $ A $ Abs (x, T, P)) =
   1.212 +      (case extract_imp true [] P of
   1.213          NONE => NONE
   1.214 -      | SOME(xs,eq,Q) => if not(null xs) then NONE else
   1.215 -          let val R = Data.imp $ eq $ Q
   1.216 -          in SOME (prove_conv tac ss (F,Ball $ A $ Abs(x,T,R))) end)
   1.217 +      | SOME (xs, eq, Q) =>
   1.218 +          if not (null xs) then NONE
   1.219 +          else
   1.220 +            let val R = Data.imp $ eq $ Q
   1.221 +            in SOME (prove_conv tac ss (F, Ball $ A $ Abs (x, T, R))) end)
   1.222    | rearrange_ball _ _ _ = NONE;
   1.223  
   1.224 -fun rearrange_ex ss (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
   1.225 -     (case extract_quant extract_conj q P of
   1.226 +fun rearrange_ex ss (F as (ex as Const (q, _)) $ Abs (x, T, P)) =
   1.227 +      (case extract_quant extract_conj q P of
   1.228          NONE => NONE
   1.229 -      | SOME(xs,eq,Q) =>
   1.230 +      | SOME (xs, eq, Q) =>
   1.231            let val R = quantify ex x T xs (Data.conj $ eq $ Q)
   1.232 -          in SOME(prove_conv prove_one_point_ex_tac ss (F,R)) end)
   1.233 +          in SOME (prove_conv prove_one_point_ex_tac ss (F, R)) end)
   1.234    | rearrange_ex _ _ = NONE;
   1.235  
   1.236 -fun rearrange_bex tac ss (F as Bex $ A $ Abs(x,T,P)) =
   1.237 -     (case extract_conj true [] P of
   1.238 +fun rearrange_bex tac ss (F as Bex $ A $ Abs (x, T, P)) =
   1.239 +      (case extract_conj true [] P of
   1.240          NONE => NONE
   1.241 -      | SOME(xs,eq,Q) => if not(null xs) then NONE else
   1.242 -          SOME(prove_conv tac ss (F,Bex $ A $ Abs(x,T,Data.conj$eq$Q))))
   1.243 +      | SOME (xs, eq, Q) =>
   1.244 +          if not (null xs) then NONE
   1.245 +          else SOME (prove_conv tac ss (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
   1.246    | rearrange_bex _ _ _ = NONE;
   1.247  
   1.248 -fun rearrange_Collect tac ss (F as Coll $ Abs(x,T,P)) =
   1.249 -     (case extract_conj true [] P of
   1.250 +fun rearrange_Collect tac ss (F as Collect $ Abs (x, T, P)) =
   1.251 +      (case extract_conj true [] P of
   1.252          NONE => NONE
   1.253 -      | SOME(_,eq,Q) =>
   1.254 -          let val R = Coll $ Abs(x,T, Data.conj $ eq $ Q)
   1.255 -          in SOME(prove_conv tac ss (F,R)) end);
   1.256 +      | SOME (_, eq, Q) =>
   1.257 +          let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
   1.258 +          in SOME (prove_conv tac ss (F, R)) end)
   1.259 +  | rearrange_Collect _ _ _ = NONE;
   1.260  
   1.261  end;