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;
```