src/Pure/meta_simplifier.ML
changeset 15531 08c8dad8e399
parent 15460 dd48bf51aff1
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -303,8 +303,8 @@
     1.4  val basic_mk_rews: mk_rews =
     1.5   {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
     1.6    mk_cong = I,
     1.7 -  mk_sym = Some o Drule.symmetric_fun,
     1.8 -  mk_eq_True = K None};
     1.9 +  mk_sym = SOME o Drule.symmetric_fun,
    1.10 +  mk_eq_True = K NONE};
    1.11  
    1.12  in
    1.13  
    1.14 @@ -445,8 +445,8 @@
    1.15  
    1.16  fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
    1.17    (case mk_eq_True thm of
    1.18 -    None => []
    1.19 -  | Some eq_True =>
    1.20 +    NONE => []
    1.21 +  | SOME eq_True =>
    1.22        let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True
    1.23        in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
    1.24  
    1.25 @@ -478,8 +478,8 @@
    1.26        else
    1.27          let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in
    1.28            (case mk_sym thm of
    1.29 -            None => []
    1.30 -          | Some thm' =>
    1.31 +            NONE => []
    1.32 +          | SOME thm' =>
    1.33                let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
    1.34                in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
    1.35          end
    1.36 @@ -516,9 +516,9 @@
    1.37  
    1.38  (* congs *)
    1.39  
    1.40 -fun cong_name (Const (a, _)) = Some a
    1.41 -  | cong_name (Free (a, _)) = Some ("Free: " ^ a)
    1.42 -  | cong_name _ = None;
    1.43 +fun cong_name (Const (a, _)) = SOME a
    1.44 +  | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
    1.45 +  | cong_name _ = NONE;
    1.46  
    1.47  local
    1.48  
    1.49 @@ -551,7 +551,7 @@
    1.50        val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
    1.51          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.52      (*val lhs = Pattern.eta_contract lhs;*)
    1.53 -      val a = the (cong_name (head_of (term_of lhs))) handle Library.OPTION =>
    1.54 +      val a = the (cong_name (head_of (term_of lhs))) handle Option =>
    1.55          raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
    1.56        val (alist, weak) = congs;
    1.57        val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
    1.58 @@ -565,12 +565,12 @@
    1.59        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
    1.60          raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.61      (*val lhs = Pattern.eta_contract lhs;*)
    1.62 -      val a = the (cong_name (head_of lhs)) handle Library.OPTION =>
    1.63 +      val a = the (cong_name (head_of lhs)) handle Option =>
    1.64          raise SIMPLIFIER ("Congruence must start with a constant", thm);
    1.65        val (alist, _) = congs;
    1.66        val alist2 = filter (fn (x, _) => x <> a) alist;
    1.67        val weak2 = alist2 |> mapfilter (fn (a, {thm, ...}) =>
    1.68 -        if is_full_cong thm then None else Some a);
    1.69 +        if is_full_cong thm then NONE else SOME a);
    1.70      in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
    1.71  
    1.72  fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
    1.73 @@ -710,12 +710,12 @@
    1.74    let
    1.75      val thm'' = transitive thm (transitive
    1.76        (symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm')
    1.77 -  in if msg then trace_thm "SUCCEEDED" thm' else (); Some thm'' end
    1.78 +  in if msg then trace_thm "SUCCEEDED" thm' else (); SOME thm'' end
    1.79    handle THM _ =>
    1.80      let val {sign, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
    1.81        trace_thm "Proved wrong thm (Check subgoaler?)" thm';
    1.82        trace_term false "Should have proved:" sign prop0;
    1.83 -      None
    1.84 +      NONE
    1.85      end;
    1.86  
    1.87  
    1.88 @@ -764,12 +764,12 @@
    1.89      val Simpset ({depth = depth', ...}, _) = ss';
    1.90    in
    1.91      if depth' > ! simp_depth_limit
    1.92 -    then (warning "simp_depth_limit exceeded - giving up"; None)
    1.93 +    then (warning "simp_depth_limit exceeded - giving up"; NONE)
    1.94      else
    1.95       (if depth' mod 10 = 0
    1.96        then warning ("Simplification depth " ^ string_of_int depth')
    1.97        else ();
    1.98 -      Some ss')
    1.99 +      SOME ss')
   1.100    end;
   1.101  
   1.102  (*
   1.103 @@ -803,34 +803,34 @@
   1.104        in
   1.105          if perm andalso not (termless (rhs', lhs'))
   1.106          then (trace_named_thm "Cannot apply permutative rewrite rule" (thm, name);
   1.107 -              trace_thm "Term does not become smaller:" thm'; None)
   1.108 +              trace_thm "Term does not become smaller:" thm'; NONE)
   1.109          else (trace_named_thm "Applying instance of rewrite rule" (thm, name);
   1.110             if unconditional
   1.111             then
   1.112               (trace_thm "Rewriting:" thm';
   1.113                let val lr = Logic.dest_equals prop;
   1.114 -                  val Some thm'' = check_conv false eta_thm thm'
   1.115 -              in Some (thm'', uncond_skel (congs, lr)) end)
   1.116 +                  val SOME thm'' = check_conv false eta_thm thm'
   1.117 +              in SOME (thm'', uncond_skel (congs, lr)) end)
   1.118             else
   1.119               (trace_thm "Trying to rewrite:" thm';
   1.120                case incr_depth ss of
   1.121 -                None => (trace_thm "FAILED - reached depth limit" thm'; None)
   1.122 -              | Some ss' =>
   1.123 +                NONE => (trace_thm "FAILED - reached depth limit" thm'; NONE)
   1.124 +              | SOME ss' =>
   1.125                (case prover ss' thm' of
   1.126 -                None => (trace_thm "FAILED" thm'; None)
   1.127 -              | Some thm2 =>
   1.128 +                NONE => (trace_thm "FAILED" thm'; NONE)
   1.129 +              | SOME thm2 =>
   1.130                    (case check_conv true eta_thm thm2 of
   1.131 -                     None => None |
   1.132 -                     Some thm2' =>
   1.133 +                     NONE => NONE |
   1.134 +                     SOME thm2' =>
   1.135                         let val concl = Logic.strip_imp_concl prop
   1.136                             val lr = Logic.dest_equals concl
   1.137 -                       in Some (thm2', cond_skel (congs, lr)) end))))
   1.138 +                       in SOME (thm2', cond_skel (congs, lr)) end))))
   1.139        end
   1.140  
   1.141 -    fun rews [] = None
   1.142 +    fun rews [] = NONE
   1.143        | rews (rrule :: rrules) =
   1.144 -          let val opt = rew rrule handle Pattern.MATCH => None
   1.145 -          in case opt of None => rews rrules | some => some end;
   1.146 +          let val opt = rew rrule handle Pattern.MATCH => NONE
   1.147 +          in case opt of NONE => rews rrules | some => some end;
   1.148  
   1.149      fun sort_rrules rrs = let
   1.150        fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of
   1.151 @@ -842,25 +842,25 @@
   1.152                                       else sort rrs (re1,rr::re2)
   1.153      in sort rrs ([],[]) end
   1.154  
   1.155 -    fun proc_rews [] = None
   1.156 +    fun proc_rews [] = NONE
   1.157        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
   1.158            if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then
   1.159              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   1.160               case transform_failure (curry SIMPROC_FAIL name)
   1.161                   (fn () => proc signt ss eta_t) () of
   1.162 -               None => (debug false "FAILED"; proc_rews ps)
   1.163 -             | Some raw_thm =>
   1.164 +               NONE => (debug false "FAILED"; proc_rews ps)
   1.165 +             | SOME raw_thm =>
   1.166                   (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   1.167                    (case rews (mk_procrule raw_thm) of
   1.168 -                    None => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^
   1.169 +                    NONE => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^
   1.170                        " -- does not match") t; proc_rews ps)
   1.171                    | some => some)))
   1.172            else proc_rews ps;
   1.173    in case eta_t of
   1.174 -       Abs _ $ _ => Some (transitive eta_thm
   1.175 +       Abs _ $ _ => SOME (transitive eta_thm
   1.176           (beta_conversion false eta_t'), skel0)
   1.177       | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
   1.178 -               None => proc_rews (Net.match_term procs eta_t)
   1.179 +               NONE => proc_rews (Net.match_term procs eta_t)
   1.180               | some => some)
   1.181    end;
   1.182  
   1.183 @@ -876,67 +876,67 @@
   1.184           is handled when congc is called *)
   1.185        val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   1.186        val unit = trace_thm "Applying congruence rule:" thm';
   1.187 -      fun err (msg, thm) = (trace_thm msg thm; None)
   1.188 +      fun err (msg, thm) = (trace_thm msg thm; NONE)
   1.189    in case prover thm' of
   1.190 -       None => err ("Congruence proof failed.  Could not prove", thm')
   1.191 -     | Some thm2 => (case check_conv true (Drule.beta_eta_conversion t) thm2 of
   1.192 -          None => err ("Congruence proof failed.  Should not have proved", thm2)
   1.193 -        | Some thm2' =>
   1.194 +       NONE => err ("Congruence proof failed.  Could not prove", thm')
   1.195 +     | SOME thm2 => (case check_conv true (Drule.beta_eta_conversion t) thm2 of
   1.196 +          NONE => err ("Congruence proof failed.  Should not have proved", thm2)
   1.197 +        | SOME thm2' =>
   1.198              if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
   1.199 -            then None else Some thm2')
   1.200 +            then NONE else SOME thm2')
   1.201    end;
   1.202  
   1.203  val (cA, (cB, cC)) =
   1.204    apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   1.205  
   1.206 -fun transitive1 None None = None
   1.207 -  | transitive1 (Some thm1) None = Some thm1
   1.208 -  | transitive1 None (Some thm2) = Some thm2
   1.209 -  | transitive1 (Some thm1) (Some thm2) = Some (transitive thm1 thm2)
   1.210 +fun transitive1 NONE NONE = NONE
   1.211 +  | transitive1 (SOME thm1) NONE = SOME thm1
   1.212 +  | transitive1 NONE (SOME thm2) = SOME thm2
   1.213 +  | transitive1 (SOME thm1) (SOME thm2) = SOME (transitive thm1 thm2)
   1.214  
   1.215 -fun transitive2 thm = transitive1 (Some thm);
   1.216 -fun transitive3 thm = transitive1 thm o Some;
   1.217 +fun transitive2 thm = transitive1 (SOME thm);
   1.218 +fun transitive3 thm = transitive1 thm o SOME;
   1.219  
   1.220  fun bottomc ((simprem, useprem, mutsimp), prover, sign, maxidx) =
   1.221    let
   1.222      fun botc skel ss t =
   1.223 -          if is_Var skel then None
   1.224 +          if is_Var skel then NONE
   1.225            else
   1.226            (case subc skel ss t of
   1.227 -             some as Some thm1 =>
   1.228 +             some as SOME thm1 =>
   1.229                 (case rewritec (prover, sign, maxidx) ss (rhs_of thm1) of
   1.230 -                  Some (thm2, skel2) =>
   1.231 +                  SOME (thm2, skel2) =>
   1.232                      transitive2 (transitive thm1 thm2)
   1.233                        (botc skel2 ss (rhs_of thm2))
   1.234 -                | None => some)
   1.235 -           | None =>
   1.236 +                | NONE => some)
   1.237 +           | NONE =>
   1.238                 (case rewritec (prover, sign, maxidx) ss t of
   1.239 -                  Some (thm2, skel2) => transitive2 thm2
   1.240 +                  SOME (thm2, skel2) => transitive2 thm2
   1.241                      (botc skel2 ss (rhs_of thm2))
   1.242 -                | None => None))
   1.243 +                | NONE => NONE))
   1.244  
   1.245      and try_botc ss t =
   1.246            (case botc skel0 ss t of
   1.247 -             Some trec1 => trec1 | None => (reflexive t))
   1.248 +             SOME trec1 => trec1 | NONE => (reflexive t))
   1.249  
   1.250      and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
   1.251         (case term_of t0 of
   1.252             Abs (a, T, t) =>
   1.253               let
   1.254 -                 val (v, t') = Thm.dest_abs (Some ("." ^ a ^ "." ^ string_of_int bounds)) t0;
   1.255 +                 val (v, t') = Thm.dest_abs (SOME ("." ^ a ^ "." ^ string_of_int bounds)) t0;
   1.256                   val ss' = incr_bounds ss;
   1.257                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
   1.258               in case botc skel' ss' t' of
   1.259 -                  Some thm => Some (abstract_rule a v thm)
   1.260 -                | None => None
   1.261 +                  SOME thm => SOME (abstract_rule a v thm)
   1.262 +                | NONE => NONE
   1.263               end
   1.264           | t $ _ => (case t of
   1.265               Const ("==>", _) $ _  => impc t0 ss
   1.266             | Abs _ =>
   1.267                 let val thm = beta_conversion false t0
   1.268                 in case subc skel0 ss (rhs_of thm) of
   1.269 -                    None => Some thm
   1.270 -                  | Some thm' => Some (transitive thm thm')
   1.271 +                    NONE => SOME thm
   1.272 +                  | SOME thm' => SOME (transitive thm thm')
   1.273                 end
   1.274             | _  =>
   1.275                 let fun appc () =
   1.276 @@ -947,21 +947,21 @@
   1.277                         val (ct, cu) = Thm.dest_comb t0
   1.278                       in
   1.279                       (case botc tskel ss ct of
   1.280 -                        Some thm1 =>
   1.281 +                        SOME thm1 =>
   1.282                            (case botc uskel ss cu of
   1.283 -                             Some thm2 => Some (combination thm1 thm2)
   1.284 -                           | None => Some (combination thm1 (reflexive cu)))
   1.285 -                      | None =>
   1.286 +                             SOME thm2 => SOME (combination thm1 thm2)
   1.287 +                           | NONE => SOME (combination thm1 (reflexive cu)))
   1.288 +                      | NONE =>
   1.289                            (case botc uskel ss cu of
   1.290 -                             Some thm1 => Some (combination (reflexive ct) thm1)
   1.291 -                           | None => None))
   1.292 +                             SOME thm1 => SOME (combination (reflexive ct) thm1)
   1.293 +                           | NONE => NONE))
   1.294                       end
   1.295                     val (h, ts) = strip_comb t
   1.296                 in case cong_name h of
   1.297 -                    Some a =>
   1.298 +                    SOME a =>
   1.299                        (case assoc_string (fst congs, a) of
   1.300 -                         None => appc ()
   1.301 -                       | Some cong =>
   1.302 +                         NONE => appc ()
   1.303 +                       | SOME cong =>
   1.304    (*post processing: some partial applications h t1 ... tj, j <= length ts,
   1.305      may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
   1.306                            (let
   1.307 @@ -972,14 +972,14 @@
   1.308                               val skel =
   1.309                                 list_comb (h, replicate (length ts) dVar)
   1.310                             in case botc skel ss cl of
   1.311 -                                None => thm
   1.312 -                              | Some thm' => transitive3 thm
   1.313 +                                NONE => thm
   1.314 +                              | SOME thm' => transitive3 thm
   1.315                                    (combination thm' (reflexive cr))
   1.316                             end handle TERM _ => error "congc result"
   1.317                                      | Pattern.MATCH => appc ()))
   1.318                    | _ => appc ()
   1.319                 end)
   1.320 -         | _ => None)
   1.321 +         | _ => NONE)
   1.322  
   1.323      and impc ct ss =
   1.324        if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
   1.325 @@ -987,10 +987,10 @@
   1.326      and rules_of_prem ss prem =
   1.327        if maxidx_of_term (term_of prem) <> ~1
   1.328        then (trace_cterm true
   1.329 -        "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], None))
   1.330 +        "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], NONE))
   1.331        else
   1.332          let val asm = assume prem
   1.333 -        in (extract_safe_rrules (ss, asm), Some asm) end
   1.334 +        in (extract_safe_rrules (ss, asm), SOME asm) end
   1.335  
   1.336      and add_rrules (rrss, asms) ss =
   1.337        foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
   1.338 @@ -1021,8 +1021,8 @@
   1.339                Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl);
   1.340              val dprem = apsome (curry (disch false) prem)
   1.341            in case rewritec (prover, sign, maxidx) ss' concl' of
   1.342 -              None => rebuild prems concl' rrss asms ss (dprem eq)
   1.343 -            | Some (eq', _) => transitive2 (foldl (disch false o swap)
   1.344 +              NONE => rebuild prems concl' rrss asms ss (dprem eq)
   1.345 +            | SOME (eq', _) => transitive2 (foldl (disch false o swap)
   1.346                    (the (transitive3 (dprem eq) eq'), prems))
   1.347                  (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss)
   1.348            end
   1.349 @@ -1037,7 +1037,7 @@
   1.350  
   1.351      and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
   1.352          transitive1 (foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
   1.353 -            (apsome (curry (disch false) prem) eq2)) (None, eqns ~~ prems'))
   1.354 +            (apsome (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems'))
   1.355            (if changed > 0 then
   1.356               mut_impc (rev prems') concl (rev rrss') (rev asms')
   1.357                 [] [] [] [] ss ~1 changed
   1.358 @@ -1046,12 +1046,12 @@
   1.359  
   1.360        | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
   1.361            prems' rrss' asms' eqns ss changed k =
   1.362 -        case (if k = 0 then None else botc skel0 (add_rrules
   1.363 +        case (if k = 0 then NONE else botc skel0 (add_rrules
   1.364            (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
   1.365 -            None => mut_impc prems concl rrss asms (prem :: prems')
   1.366 -              (rrs :: rrss') (asm :: asms') (None :: eqns) ss changed
   1.367 +            NONE => mut_impc prems concl rrss asms (prem :: prems')
   1.368 +              (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
   1.369                (if k = 0 then 0 else k - 1)
   1.370 -          | Some eqn =>
   1.371 +          | SOME eqn =>
   1.372              let
   1.373                val prem' = rhs_of eqn;
   1.374                val tprems = map term_of prems;
   1.375 @@ -1059,7 +1059,7 @@
   1.376                  find_index_eq p tprems) (#hyps (rep_thm eqn)));
   1.377                val (rrs', asm') = rules_of_prem ss prem'
   1.378              in mut_impc prems concl rrss asms (prem' :: prems')
   1.379 -              (rrs' :: rrss') (asm' :: asms') (Some (foldr (disch true)
   1.380 +              (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
   1.381                  (take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
   1.382                    (drop (i, prems), concl))))) :: eqns) ss (length prems') ~1
   1.383              end
   1.384 @@ -1067,20 +1067,20 @@
   1.385       (*legacy code - only for backwards compatibility*)
   1.386       and nonmut_impc ct ss =
   1.387         let val (prem, conc) = dest_implies ct;
   1.388 -           val thm1 = if simprem then botc skel0 ss prem else None;
   1.389 +           val thm1 = if simprem then botc skel0 ss prem else NONE;
   1.390             val prem1 = if_none (apsome rhs_of thm1) prem;
   1.391             val ss1 = if not useprem then ss else add_rrules
   1.392               (apsnd single (apfst single (rules_of_prem ss prem1))) ss
   1.393         in (case botc skel0 ss1 conc of
   1.394 -           None => (case thm1 of
   1.395 -               None => None
   1.396 -             | Some thm1' => Some (Drule.imp_cong' thm1' (reflexive conc)))
   1.397 -         | Some thm2 =>
   1.398 +           NONE => (case thm1 of
   1.399 +               NONE => NONE
   1.400 +             | SOME thm1' => SOME (Drule.imp_cong' thm1' (reflexive conc)))
   1.401 +         | SOME thm2 =>
   1.402             let val thm2' = disch false (prem1, thm2)
   1.403             in (case thm1 of
   1.404 -               None => Some thm2'
   1.405 -             | Some thm1' =>
   1.406 -                 Some (transitive (Drule.imp_cong' thm1' (reflexive conc)) thm2'))
   1.407 +               NONE => SOME thm2'
   1.408 +             | SOME thm1' =>
   1.409 +                 SOME (transitive (Drule.imp_cong' thm1' (reflexive conc)) thm2'))
   1.410             end)
   1.411         end
   1.412