tuned whitespace;
authorwenzelm
Thu Dec 12 16:17:35 2013 +0100 (2013-12-12)
changeset 54725fc384e0a7f51
parent 54724 b92694e756b8
child 54726 5285805af26c
tuned whitespace;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu Dec 12 14:35:31 2013 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Dec 12 16:17:35 2013 +0100
     1.3 @@ -946,30 +946,33 @@
     1.4          val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
     1.5          val prop' = Thm.prop_of thm';
     1.6          val unconditional = (Logic.count_prems prop' = 0);
     1.7 -        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
     1.8 +        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
     1.9        in
    1.10          if perm andalso not (termless (rhs', lhs'))
    1.11 -        then (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name);
    1.12 -              trace_thm ctxt (fn () => "Term does not become smaller:") thm'; NONE)
    1.13 -        else (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name);
    1.14 -           if unconditional
    1.15 -           then
    1.16 -             (trace_thm ctxt (fn () => "Rewriting:") thm';
    1.17 +        then
    1.18 +         (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name);
    1.19 +          trace_thm ctxt (fn () => "Term does not become smaller:") thm';
    1.20 +          NONE)
    1.21 +        else
    1.22 +         (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name);
    1.23 +          if unconditional
    1.24 +          then
    1.25 +           (trace_thm ctxt (fn () => "Rewriting:") thm';
    1.26 +            let
    1.27 +              val lr = Logic.dest_equals prop;
    1.28 +              val SOME thm'' = check_conv ctxt false eta_thm thm';
    1.29 +            in SOME (thm'', uncond_skel (congs, lr)) end)
    1.30 +          else
    1.31 +           (trace_thm ctxt (fn () => "Trying to rewrite:") thm';
    1.32 +            if simp_depth ctxt > Config.get ctxt simp_depth_limit
    1.33 +            then
    1.34                let
    1.35 -                val lr = Logic.dest_equals prop;
    1.36 -                val SOME thm'' = check_conv ctxt false eta_thm thm';
    1.37 -              in SOME (thm'', uncond_skel (congs, lr)) end)
    1.38 -           else
    1.39 -             (trace_thm ctxt (fn () => "Trying to rewrite:") thm';
    1.40 -              if simp_depth ctxt > Config.get ctxt simp_depth_limit
    1.41 -              then
    1.42 -                let
    1.43 -                  val s = "simp_depth_limit exceeded - giving up";
    1.44 -                  val _ = trace ctxt false (fn () => s);
    1.45 -                  val _ = Context_Position.if_visible ctxt warning s;
    1.46 -                in NONE end
    1.47 -              else
    1.48 -              case prover ctxt thm' of
    1.49 +                val s = "simp_depth_limit exceeded - giving up";
    1.50 +                val _ = trace ctxt false (fn () => s);
    1.51 +                val _ = Context_Position.if_visible ctxt warning s;
    1.52 +              in NONE end
    1.53 +            else
    1.54 +              (case prover ctxt thm' of
    1.55                  NONE => (trace_thm ctxt (fn () => "FAILED") thm'; NONE)
    1.56                | SOME thm2 =>
    1.57                    (case check_conv ctxt true eta_thm thm2 of
    1.58 @@ -978,13 +981,13 @@
    1.59                        let
    1.60                          val concl = Logic.strip_imp_concl prop;
    1.61                          val lr = Logic.dest_equals concl;
    1.62 -                      in SOME (thm2', cond_skel (congs, lr)) end)))
    1.63 +                      in SOME (thm2', cond_skel (congs, lr)) end))))
    1.64        end;
    1.65  
    1.66      fun rews [] = NONE
    1.67        | rews (rrule :: rrules) =
    1.68            let val opt = rew rrule handle Pattern.MATCH => NONE
    1.69 -          in case opt of NONE => rews rrules | some => some end;
    1.70 +          in (case opt of NONE => rews rrules | some => some) end;
    1.71  
    1.72      fun sort_rrules rrs =
    1.73        let
    1.74 @@ -1003,7 +1006,7 @@
    1.75        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
    1.76            if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
    1.77              (debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t;
    1.78 -             case proc ctxt eta_t' of
    1.79 +             (case proc ctxt eta_t' of
    1.80                 NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps)
    1.81               | SOME raw_thm =>
    1.82                   (trace_thm ctxt (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
    1.83 @@ -1011,7 +1014,7 @@
    1.84                    (case rews (mk_procrule ctxt raw_thm) of
    1.85                      NONE => (trace_cterm ctxt true (fn () => "IGNORED result of simproc " ^ quote name ^
    1.86                        " -- does not match") t; proc_rews ps)
    1.87 -                  | some => some)))
    1.88 +                  | some => some))))
    1.89            else proc_rews ps;
    1.90    in
    1.91      (case eta_t of
    1.92 @@ -1052,7 +1055,7 @@
    1.93  fun transitive1 NONE NONE = NONE
    1.94    | transitive1 (SOME thm1) NONE = SOME thm1
    1.95    | transitive1 NONE (SOME thm2) = SOME thm2
    1.96 -  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
    1.97 +  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2);
    1.98  
    1.99  fun transitive2 thm = transitive1 (SOME thm);
   1.100  fun transitive3 thm = transitive1 thm o SOME;
   1.101 @@ -1060,25 +1063,25 @@
   1.102  fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) =
   1.103    let
   1.104      fun botc skel ctxt t =
   1.105 -          if is_Var skel then NONE
   1.106 -          else
   1.107 -          (case subc skel ctxt t of
   1.108 -             some as SOME thm1 =>
   1.109 -               (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
   1.110 -                  SOME (thm2, skel2) =>
   1.111 -                    transitive2 (Thm.transitive thm1 thm2)
   1.112 -                      (botc skel2 ctxt (Thm.rhs_of thm2))
   1.113 -                | NONE => some)
   1.114 -           | NONE =>
   1.115 -               (case rewritec (prover, maxidx) ctxt t of
   1.116 -                  SOME (thm2, skel2) => transitive2 thm2
   1.117 +      if is_Var skel then NONE
   1.118 +      else
   1.119 +        (case subc skel ctxt t of
   1.120 +           some as SOME thm1 =>
   1.121 +             (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
   1.122 +                SOME (thm2, skel2) =>
   1.123 +                  transitive2 (Thm.transitive thm1 thm2)
   1.124                      (botc skel2 ctxt (Thm.rhs_of thm2))
   1.125 -                | NONE => NONE))
   1.126 +              | NONE => some)
   1.127 +         | NONE =>
   1.128 +             (case rewritec (prover, maxidx) ctxt t of
   1.129 +                SOME (thm2, skel2) => transitive2 thm2
   1.130 +                  (botc skel2 ctxt (Thm.rhs_of thm2))
   1.131 +              | NONE => NONE))
   1.132  
   1.133      and try_botc ctxt t =
   1.134 -          (case botc skel0 ctxt t of
   1.135 -            SOME trec1 => trec1
   1.136 -          | NONE => (Thm.reflexive t))
   1.137 +      (case botc skel0 ctxt t of
   1.138 +        SOME trec1 => trec1
   1.139 +      | NONE => Thm.reflexive t)
   1.140  
   1.141      and subc skel ctxt t0 =
   1.142          let val Simpset ({bounds, ...}, {congs, ...}) = simpset_of ctxt in
   1.143 @@ -1094,64 +1097,70 @@
   1.144                            quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
   1.145                        else ();
   1.146                      val ctxt' = add_bound ((b', T), a) ctxt;
   1.147 -                    val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
   1.148 +                    val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
   1.149                  in
   1.150                    (case botc skel' ctxt' t' of
   1.151                      SOME thm => SOME (Thm.abstract_rule a v thm)
   1.152                    | NONE => NONE)
   1.153                  end
   1.154 -            | t $ _ => (case t of
   1.155 +            | t $ _ =>
   1.156 +              (case t of
   1.157                  Const ("==>", _) $ _  => impc t0 ctxt
   1.158                | Abs _ =>
   1.159                    let val thm = Thm.beta_conversion false t0
   1.160 -                  in case subc skel0 ctxt (Thm.rhs_of thm) of
   1.161 -                       NONE => SOME thm
   1.162 -                     | SOME thm' => SOME (Thm.transitive thm thm')
   1.163 +                  in
   1.164 +                    (case subc skel0 ctxt (Thm.rhs_of thm) of
   1.165 +                      NONE => SOME thm
   1.166 +                    | SOME thm' => SOME (Thm.transitive thm thm'))
   1.167                    end
   1.168                | _  =>
   1.169                    let fun appc () =
   1.170                          let
   1.171 -                          val (tskel, uskel) = case skel of
   1.172 +                          val (tskel, uskel) =
   1.173 +                            (case skel of
   1.174                                tskel $ uskel => (tskel, uskel)
   1.175 -                            | _ => (skel0, skel0);
   1.176 -                          val (ct, cu) = Thm.dest_comb t0
   1.177 +                            | _ => (skel0, skel0));
   1.178 +                          val (ct, cu) = Thm.dest_comb t0;
   1.179                          in
   1.180 -                        (case botc tskel ctxt ct of
   1.181 -                           SOME thm1 =>
   1.182 -                             (case botc uskel ctxt cu of
   1.183 +                          (case botc tskel ctxt ct of
   1.184 +                            SOME thm1 =>
   1.185 +                              (case botc uskel ctxt cu of
   1.186                                  SOME thm2 => SOME (Thm.combination thm1 thm2)
   1.187                                | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
   1.188 -                         | NONE =>
   1.189 -                             (case botc uskel ctxt cu of
   1.190 +                          | NONE =>
   1.191 +                              (case botc uskel ctxt cu of
   1.192                                  SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
   1.193                                | NONE => NONE))
   1.194                          end
   1.195 -                      val (h, ts) = strip_comb t
   1.196 -                  in case cong_name h of
   1.197 -                       SOME a =>
   1.198 -                         (case AList.lookup (op =) (fst congs) a of
   1.199 -                            NONE => appc ()
   1.200 -                          | SOME cong =>
   1.201 +                      val (h, ts) = strip_comb t;
   1.202 +                  in
   1.203 +                    (case cong_name h of
   1.204 +                      SOME a =>
   1.205 +                        (case AList.lookup (op =) (fst congs) a of
   1.206 +                           NONE => appc ()
   1.207 +                        | SOME cong =>
   1.208       (*post processing: some partial applications h t1 ... tj, j <= length ts,
   1.209         may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
   1.210 -                             (let
   1.211 -                                val thm = congc (prover ctxt) ctxt maxidx cong t0;
   1.212 -                                val t = the_default t0 (Option.map Thm.rhs_of thm);
   1.213 -                                val (cl, cr) = Thm.dest_comb t
   1.214 -                                val dVar = Var(("", 0), dummyT)
   1.215 -                                val skel =
   1.216 -                                  list_comb (h, replicate (length ts) dVar)
   1.217 -                              in case botc skel ctxt cl of
   1.218 -                                   NONE => thm
   1.219 -                                 | SOME thm' => transitive3 thm
   1.220 -                                     (Thm.combination thm' (Thm.reflexive cr))
   1.221 -                              end handle Pattern.MATCH => appc ()))
   1.222 -                     | _ => appc ()
   1.223 +                           (let
   1.224 +                              val thm = congc (prover ctxt) ctxt maxidx cong t0;
   1.225 +                              val t = the_default t0 (Option.map Thm.rhs_of thm);
   1.226 +                              val (cl, cr) = Thm.dest_comb t
   1.227 +                              val dVar = Var(("", 0), dummyT)
   1.228 +                              val skel =
   1.229 +                                list_comb (h, replicate (length ts) dVar)
   1.230 +                            in
   1.231 +                              (case botc skel ctxt cl of
   1.232 +                                NONE => thm
   1.233 +                              | SOME thm' =>
   1.234 +                                  transitive3 thm (Thm.combination thm' (Thm.reflexive cr)))
   1.235 +                            end handle Pattern.MATCH => appc ()))
   1.236 +                     | _ => appc ())
   1.237                    end)
   1.238              | _ => NONE)
   1.239          end
   1.240      and impc ct ctxt =
   1.241 -      if mutsimp then mut_impc0 [] ct [] [] ctxt else nonmut_impc ct ctxt
   1.242 +      if mutsimp then mut_impc0 [] ct [] [] ctxt
   1.243 +      else nonmut_impc ct ctxt
   1.244  
   1.245      and rules_of_prem ctxt prem =
   1.246        if maxidx_of_term (term_of prem) <> ~1
   1.247 @@ -1171,16 +1180,18 @@
   1.248          val eq' = Thm.implies_elim (Thm.instantiate
   1.249            ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
   1.250            (Thm.implies_intr prem eq)
   1.251 -      in if not r then eq' else
   1.252 -        let
   1.253 -          val (prem', concl) = Thm.dest_implies lhs;
   1.254 -          val (prem'', _) = Thm.dest_implies rhs
   1.255 -        in Thm.transitive (Thm.transitive
   1.256 -          (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
   1.257 -             Drule.swap_prems_eq) eq')
   1.258 -          (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
   1.259 -             Drule.swap_prems_eq)
   1.260 -        end
   1.261 +      in
   1.262 +        if not r then eq'
   1.263 +        else
   1.264 +          let
   1.265 +            val (prem', concl) = Thm.dest_implies lhs;
   1.266 +            val (prem'', _) = Thm.dest_implies rhs
   1.267 +          in Thm.transitive (Thm.transitive
   1.268 +            (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
   1.269 +               Drule.swap_prems_eq) eq')
   1.270 +            (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
   1.271 +               Drule.swap_prems_eq)
   1.272 +          end
   1.273        end
   1.274  
   1.275      and rebuild [] _ _ _ _ eq = eq
   1.276 @@ -1218,27 +1229,29 @@
   1.277  
   1.278        | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
   1.279            prems' rrss' asms' eqns ctxt changed k =
   1.280 -        case (if k = 0 then NONE else botc skel0 (add_rrules
   1.281 +        (case (if k = 0 then NONE else botc skel0 (add_rrules
   1.282            (rev rrss' @ rrss, rev asms' @ asms) ctxt) prem) of
   1.283              NONE => mut_impc prems concl rrss asms (prem :: prems')
   1.284                (rrs :: rrss') (asm :: asms') (NONE :: eqns) ctxt changed
   1.285                (if k = 0 then 0 else k - 1)
   1.286 -          | SOME eqn =>
   1.287 +        | SOME eqn =>
   1.288              let
   1.289                val prem' = Thm.rhs_of eqn;
   1.290                val tprems = map term_of prems;
   1.291                val i = 1 + fold Integer.max (map (fn p =>
   1.292                  find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
   1.293                val (rrs', asm') = rules_of_prem ctxt prem';
   1.294 -            in mut_impc prems concl rrss asms (prem' :: prems')
   1.295 -              (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
   1.296 -                (take i prems)
   1.297 -                (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
   1.298 -                  (drop i prems, concl))))) :: eqns)
   1.299 -                  ctxt (length prems') ~1
   1.300 -            end
   1.301 +            in
   1.302 +              mut_impc prems concl rrss asms (prem' :: prems')
   1.303 +                (rrs' :: rrss') (asm' :: asms')
   1.304 +                (SOME (fold_rev (disch true)
   1.305 +                  (take i prems)
   1.306 +                  (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
   1.307 +                    (drop i prems, concl))))) :: eqns)
   1.308 +                ctxt (length prems') ~1
   1.309 +            end)
   1.310  
   1.311 -     (*legacy code - only for backwards compatibility*)
   1.312 +    (*legacy code -- only for backwards compatibility*)
   1.313      and nonmut_impc ct ctxt =
   1.314        let
   1.315          val (prem, conc) = Thm.dest_implies ct;
   1.316 @@ -1260,9 +1273,9 @@
   1.317                | SOME thm1' =>
   1.318                   SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
   1.319              end)
   1.320 -      end
   1.321 +      end;
   1.322  
   1.323 - in try_botc end;
   1.324 +  in try_botc end;
   1.325  
   1.326  
   1.327  (* Meta-rewriting: rewrites t to u and returns the theorem t==u *)