src/Pure/meta_simplifier.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -402,7 +402,7 @@
     1.4  all its Vars? Better: a dynamic check each time a rule is applied.
     1.5  *)
     1.6  fun rewrite_rule_extra_vars prems elhs erhs =
     1.7 -  not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
     1.8 +  not (term_varnames erhs subset Library.foldl add_term_varnames (term_varnames elhs, prems))
     1.9    orelse
    1.10    not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));
    1.11  
    1.12 @@ -487,16 +487,16 @@
    1.13    end;
    1.14  
    1.15  fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    1.16 -  flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    1.17 +  List.concat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    1.18  
    1.19  fun orient_comb_simps comb mk_rrule (ss, thms) =
    1.20    let
    1.21      val rews = extract_rews (ss, thms);
    1.22 -    val rrules = flat (map mk_rrule rews);
    1.23 -  in foldl comb (ss, rrules) end;
    1.24 +    val rrules = List.concat (map mk_rrule rews);
    1.25 +  in Library.foldl comb (ss, rrules) end;
    1.26  
    1.27  fun extract_safe_rrules (ss, thm) =
    1.28 -  flat (map (orient_rrule ss) (extract_rews (ss, [thm])));
    1.29 +  List.concat (map (orient_rrule ss) (extract_rews (ss, [thm])));
    1.30  
    1.31  (*add rewrite rules explicitly; do not reorient!*)
    1.32  fun ss addsimps thms =
    1.33 @@ -551,7 +551,7 @@
    1.34        val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
    1.35          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.36      (*val lhs = Pattern.eta_contract lhs;*)
    1.37 -      val a = the (cong_name (head_of (term_of lhs))) handle Option =>
    1.38 +      val a = valOf (cong_name (head_of (term_of lhs))) handle Option =>
    1.39          raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
    1.40        val (alist, weak) = congs;
    1.41        val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
    1.42 @@ -565,11 +565,11 @@
    1.43        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
    1.44          raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.45      (*val lhs = Pattern.eta_contract lhs;*)
    1.46 -      val a = the (cong_name (head_of lhs)) handle Option =>
    1.47 +      val a = valOf (cong_name (head_of lhs)) handle Option =>
    1.48          raise SIMPLIFIER ("Congruence must start with a constant", thm);
    1.49        val (alist, _) = congs;
    1.50 -      val alist2 = filter (fn (x, _) => x <> a) alist;
    1.51 -      val weak2 = alist2 |> mapfilter (fn (a, {thm, ...}) =>
    1.52 +      val alist2 = List.filter (fn (x, _) => x <> a) alist;
    1.53 +      val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}) =>
    1.54          if is_full_cong thm then NONE else SOME a);
    1.55      in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
    1.56  
    1.57 @@ -577,8 +577,8 @@
    1.58  
    1.59  in
    1.60  
    1.61 -val (op addeqcongs) = foldl add_cong;
    1.62 -val (op deleqcongs) = foldl del_cong;
    1.63 +val (op addeqcongs) = Library.foldl add_cong;
    1.64 +val (op deleqcongs) = Library.foldl del_cong;
    1.65  
    1.66  fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
    1.67  fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
    1.68 @@ -607,8 +607,8 @@
    1.69  
    1.70  in
    1.71  
    1.72 -val (op addsimprocs) = foldl (fn (ss, Simproc procs) => foldl add_proc (ss, procs));
    1.73 -val (op delsimprocs) = foldl (fn (ss, Simproc procs) => foldl del_proc (ss, procs));
    1.74 +val (op addsimprocs) = Library.foldl (fn (ss, Simproc procs) => Library.foldl add_proc (ss, procs));
    1.75 +val (op delsimprocs) = Library.foldl (fn (ss, Simproc procs) => Library.foldl del_proc (ss, procs));
    1.76  
    1.77  end;
    1.78  
    1.79 @@ -966,7 +966,7 @@
    1.80      may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
    1.81                            (let
    1.82                               val thm = congc (prover ss, sign, maxidx) cong t0;
    1.83 -                             val t = if_none (apsome rhs_of thm) t0;
    1.84 +                             val t = getOpt (Option.map rhs_of thm, t0);
    1.85                               val (cl, cr) = Thm.dest_comb t
    1.86                               val dVar = Var(("", 0), dummyT)
    1.87                               val skel =
    1.88 @@ -993,7 +993,7 @@
    1.89          in (extract_safe_rrules (ss, asm), SOME asm) end
    1.90  
    1.91      and add_rrules (rrss, asms) ss =
    1.92 -      foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
    1.93 +      Library.foldl (insert_rrule true) (ss, List.concat rrss) |> add_prems (List.mapPartial I asms)
    1.94  
    1.95      and disch r (prem, eq) =
    1.96        let
    1.97 @@ -1018,12 +1018,12 @@
    1.98            let
    1.99              val ss' = add_rrules (rev rrss, rev asms) ss;
   1.100              val concl' =
   1.101 -              Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl);
   1.102 -            val dprem = apsome (curry (disch false) prem)
   1.103 +              Drule.mk_implies (prem, getOpt (Option.map rhs_of eq, concl));
   1.104 +            val dprem = Option.map (curry (disch false) prem)
   1.105            in case rewritec (prover, sign, maxidx) ss' concl' of
   1.106                NONE => rebuild prems concl' rrss asms ss (dprem eq)
   1.107 -            | SOME (eq', _) => transitive2 (foldl (disch false o swap)
   1.108 -                  (the (transitive3 (dprem eq) eq'), prems))
   1.109 +            | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
   1.110 +                  (valOf (transitive3 (dprem eq) eq'), prems))
   1.111                  (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss)
   1.112            end
   1.113  
   1.114 @@ -1036,8 +1036,8 @@
   1.115        end
   1.116  
   1.117      and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
   1.118 -        transitive1 (foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
   1.119 -            (apsome (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems'))
   1.120 +        transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
   1.121 +            (Option.map (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems'))
   1.122            (if changed > 0 then
   1.123               mut_impc (rev prems') concl (rev rrss') (rev asms')
   1.124                 [] [] [] [] ss ~1 changed
   1.125 @@ -1055,20 +1055,20 @@
   1.126              let
   1.127                val prem' = rhs_of eqn;
   1.128                val tprems = map term_of prems;
   1.129 -              val i = 1 + foldl Int.max (~1, map (fn p =>
   1.130 +              val i = 1 + Library.foldl Int.max (~1, map (fn p =>
   1.131                  find_index_eq p tprems) (#hyps (rep_thm eqn)));
   1.132                val (rrs', asm') = rules_of_prem ss prem'
   1.133              in mut_impc prems concl rrss asms (prem' :: prems')
   1.134 -              (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
   1.135 -                (take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
   1.136 -                  (drop (i, prems), concl))))) :: eqns) ss (length prems') ~1
   1.137 +              (rrs' :: rrss') (asm' :: asms') (SOME (Library.foldr (disch true)
   1.138 +                (Library.take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
   1.139 +                  (Library.drop (i, prems), concl))))) :: eqns) ss (length prems') ~1
   1.140              end
   1.141  
   1.142       (*legacy code - only for backwards compatibility*)
   1.143       and nonmut_impc ct ss =
   1.144         let val (prem, conc) = dest_implies ct;
   1.145             val thm1 = if simprem then botc skel0 ss prem else NONE;
   1.146 -           val prem1 = if_none (apsome rhs_of thm1) prem;
   1.147 +           val prem1 = getOpt (Option.map rhs_of thm1, prem);
   1.148             val ss1 = if not useprem then ss else add_rrules
   1.149               (apsnd single (apfst single (rules_of_prem ss prem1))) ss
   1.150         in (case botc skel0 ss1 conc of
   1.151 @@ -1169,7 +1169,7 @@
   1.152    let
   1.153      val Simpset (_, {solvers = (unsafe_solvers, _), ...}) = ss;
   1.154      val tacf = solve_all_tac unsafe_solvers;
   1.155 -    fun prover s th = apsome #1 (Seq.pull (tacf s th));
   1.156 +    fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   1.157    in rew mode prover ss thm end;
   1.158  
   1.159  val simp_thm = simp rewrite_thm;