New simplifier flag for mutual simplification.
authornipkow
Tue Mar 10 13:24:11 1998 +0100 (1998-03-10)
changeset 4713bea2ab2e360b
parent 4712 facfbbca7242
child 4714 bcdf68c78e18
New simplifier flag for mutual simplification.
TFL/rules.new.sml
src/Provers/simplifier.ML
src/Pure/drule.ML
src/Pure/library.ML
src/Pure/tactic.ML
src/Pure/thm.ML
     1.1 --- a/TFL/rules.new.sml	Tue Mar 10 13:23:35 1998 +0100
     1.2 +++ b/TFL/rules.new.sml	Tue Mar 10 13:24:11 1998 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4  fun SUBS thl = 
     1.5     rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
     1.6  
     1.7 -local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
     1.8 +local fun rew_conv mss = rewrite_cterm (true,false,false) mss (K(K None))
     1.9  in
    1.10  fun simpl_conv ss thl ctm = 
    1.11   rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
    1.12 @@ -654,7 +654,7 @@
    1.13                       val eq = Logic.strip_imp_concl imp
    1.14                       val lhs = tych(get_lhs eq)
    1.15                       val mss' = add_prems(mss, map ASSUME ants)
    1.16 -                     val lhs_eq_lhs1 = rewrite_cterm(false,true)mss' prover lhs
    1.17 +                     val lhs_eq_lhs1 = rewrite_cterm(false,true,false)mss' prover lhs
    1.18                         handle _ => reflexive lhs
    1.19                       val dummy = print_thms "proven:\n" [lhs_eq_lhs1]
    1.20                       val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
    1.21 @@ -676,7 +676,7 @@
    1.22                    val QeqQ1 = pbeta_reduce (tych Q)
    1.23                    val Q1 = #2(D.dest_eq(cconcl QeqQ1))
    1.24                    val mss' = add_prems(mss, map ASSUME ants1)
    1.25 -                  val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
    1.26 +                  val Q1eeqQ2 = rewrite_cterm (false,true,false) mss' prover Q1
    1.27                                  handle _ => reflexive Q1
    1.28                    val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
    1.29                    val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
    1.30 @@ -701,7 +701,7 @@
    1.31                   let val tych = cterm_of sign
    1.32                       val ants1 = map tych ants
    1.33                       val mss' = add_prems(mss, map ASSUME ants1)
    1.34 -                     val Q_eeq_Q1 = rewrite_cterm(false,true) mss' 
    1.35 +                     val Q_eeq_Q1 = rewrite_cterm(false,true,false) mss' 
    1.36                                                       prover (tych Q)
    1.37                        handle _ => reflexive (tych Q)
    1.38                       val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
    1.39 @@ -771,7 +771,7 @@
    1.40      (if (is_cong thm) then cong_prover else restrict_prover) mss thm
    1.41      end
    1.42      val ctm = cprop_of th
    1.43 -    val th1 = rewrite_cterm(false,true) (add_congs(mss_of [cut_lemma'], congs))
    1.44 +    val th1 = rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs))
    1.45                              prover ctm
    1.46      val th2 = equal_elim th1 th
    1.47   in
     2.1 --- a/src/Provers/simplifier.ML	Tue Mar 10 13:23:35 1998 +0100
     2.2 +++ b/src/Provers/simplifier.ML	Tue Mar 10 13:24:11 1998 +0100
     2.3 @@ -323,13 +323,13 @@
     2.4    basic_gen_simp_tac mode (ss setSSolver unsafe_finish_tac);
     2.5  
     2.6  
     2.7 -val          simp_tac = gen_simp_tac (false, false);
     2.8 -val      asm_simp_tac = gen_simp_tac (false, true);
     2.9 -val     full_simp_tac = gen_simp_tac (true,  false);
    2.10 -val asm_full_simp_tac = gen_simp_tac (true,  true);
    2.11 +val          simp_tac = gen_simp_tac (false, false, false);
    2.12 +val      asm_simp_tac = gen_simp_tac (false, true, false);
    2.13 +val     full_simp_tac = gen_simp_tac (true,  false, false);
    2.14 +val asm_full_simp_tac = gen_simp_tac (true,  true, false);
    2.15  
    2.16  (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
    2.17 -val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true);
    2.18 +val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true, false);
    2.19  
    2.20  (** The abstraction over the proof state delays the dereferencing **)
    2.21  
    2.22 @@ -339,7 +339,6 @@
    2.23  fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
    2.24  
    2.25  
    2.26 -
    2.27  (** simplification meta rules **)
    2.28  
    2.29  fun simp mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm =
    2.30 @@ -350,10 +349,10 @@
    2.31      Drule.rewrite_thm mode prover mss thm
    2.32    end;
    2.33  
    2.34 -val          simplify = simp (false, false);
    2.35 -val      asm_simplify = simp (false, true);
    2.36 -val     full_simplify = simp (true, false);
    2.37 -val asm_full_simplify = simp (true, true);
    2.38 +val          simplify = simp (false, false, false);
    2.39 +val      asm_simplify = simp (false, true, false);
    2.40 +val     full_simplify = simp (true, false, false);
    2.41 +val asm_full_simplify = simp (true, true, false);
    2.42  
    2.43  
    2.44  end;
     3.1 --- a/src/Pure/drule.ML	Tue Mar 10 13:23:35 1998 +0100
     3.2 +++ b/src/Pure/drule.ML	Tue Mar 10 13:24:11 1998 +0100
     3.3 @@ -53,12 +53,13 @@
     3.4    val refl_implies      : thm
     3.5    val symmetric_fun     : thm -> thm
     3.6    val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
     3.7 -  val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
     3.8 -	-> meta_simpset -> thm -> thm
     3.9 +  val rewrite_thm	: bool * bool * bool
    3.10 +                          -> (meta_simpset -> thm -> thm option)
    3.11 +                          -> meta_simpset -> thm -> thm
    3.12    val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    3.13 -  val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
    3.14 -        -> meta_simpset -> int -> thm -> thm
    3.15 -
    3.16 +  val rewrite_goal_rule	: bool* bool * bool
    3.17 +                          -> (meta_simpset -> thm -> thm option)
    3.18 +                          -> meta_simpset -> int -> thm -> thm
    3.19    val equal_abs_elim	: cterm  -> thm -> thm
    3.20    val equal_abs_elim_list: cterm list -> thm -> thm
    3.21    val flexpair_abs_elim_list: cterm list -> thm -> thm
    3.22 @@ -446,14 +447,14 @@
    3.23  (*Rewrite a theorem*)
    3.24  fun rewrite_rule_aux _ []   th = th
    3.25    | rewrite_rule_aux prover thms th =
    3.26 -      fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th;
    3.27 +      fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th;
    3.28  
    3.29  fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
    3.30  
    3.31  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
    3.32  fun rewrite_goals_rule_aux _ []   th = th
    3.33    | rewrite_goals_rule_aux prover thms th =
    3.34 -      fconv_rule (goals_conv (K true) (rew_conv (true, true) prover
    3.35 +      fconv_rule (goals_conv (K true) (rew_conv (true, true, false) prover
    3.36          (Thm.mss_of thms))) th;
    3.37  
    3.38  (*Rewrite the subgoal of a proof state (represented by a theorem) *)
     4.1 --- a/src/Pure/library.ML	Tue Mar 10 13:23:35 1998 +0100
     4.2 +++ b/src/Pure/library.ML	Tue Mar 10 13:24:11 1998 +0100
     4.3 @@ -76,6 +76,7 @@
     4.4    val length: 'a list -> int
     4.5    val take: int * 'a list -> 'a list
     4.6    val drop: int * 'a list -> 'a list
     4.7 +  val dropwhile: ('a -> bool) -> 'a list -> 'a list
     4.8    val nth_elem: int * 'a list -> 'a
     4.9    val last_elem: 'a list -> 'a
    4.10    val split_last: 'a list -> 'a list * 'a
    4.11 @@ -424,6 +425,9 @@
    4.12    | drop (n, x :: xs) =
    4.13        if n > 0 then drop (n - 1, xs) else x :: xs;
    4.14  
    4.15 +fun dropwhile P [] = []
    4.16 +  | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
    4.17 +
    4.18  (*return nth element of a list, where 0 designates the first element;
    4.19    raise EXCEPTION if list too short*)
    4.20  fun nth_elem NL =
     5.1 --- a/src/Pure/tactic.ML	Tue Mar 10 13:23:35 1998 +0100
     5.2 +++ b/src/Pure/tactic.ML	Tue Mar 10 13:24:11 1998 +0100
     5.3 @@ -10,7 +10,7 @@
     5.4    sig
     5.5    val ares_tac		: thm list -> int -> tactic
     5.6    val asm_rewrite_goal_tac:
     5.7 -        bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
     5.8 +    bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
     5.9    val assume_tac	: int -> tactic
    5.10    val atac	: int ->tactic
    5.11    val bimatch_from_nets_tac: 
     6.1 --- a/src/Pure/thm.ML	Tue Mar 10 13:23:35 1998 +0100
     6.2 +++ b/src/Pure/thm.ML	Tue Mar 10 13:24:11 1998 +0100
     6.3 @@ -168,7 +168,7 @@
     6.4    val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
     6.5    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
     6.6    val trace_simp        : bool ref
     6.7 -  val rewrite_cterm     : bool * bool -> meta_simpset ->
     6.8 +  val rewrite_cterm     : bool * bool * bool -> meta_simpset ->
     6.9                            (meta_simpset -> thm -> thm option) -> cterm -> thm
    6.10  
    6.11    val invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
    6.12 @@ -1625,38 +1625,50 @@
    6.13    in (sign,prems,lhs,rhs,perm) end;
    6.14  
    6.15  fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
    6.16 -  apsome (fn eq_True => let val (_,_,lhs,_,_) = decomp_simp eq_True
    6.17 -                        in {thm=eq_True, lhs=lhs, perm=false} end)
    6.18 -         (mk_eq_True thm);
    6.19 +  case mk_eq_True thm of
    6.20 +    None => []
    6.21 +  | Some eq_True => let val (_,_,lhs,_,_) = decomp_simp eq_True
    6.22 +                    in [{thm=eq_True, lhs=lhs, perm=false}] end;
    6.23 +
    6.24 +(* create the rewrite rule and possibly also the ==True variant,
    6.25 +   in case there are extra vars on the rhs *)
    6.26 +fun rrule_eq_True(thm,lhs,rhs,mss,thm2) =
    6.27 +  let val rrule = {thm=thm, lhs=lhs, perm=false}
    6.28 +  in if (term_vars rhs)  subset (term_vars lhs) andalso
    6.29 +        (term_tvars rhs) subset (term_tvars lhs)
    6.30 +     then [rrule]
    6.31 +     else mk_eq_True mss thm2 @ [rrule]
    6.32 +  end;
    6.33  
    6.34  fun mk_rrule mss thm =
    6.35    let val (_,prems,lhs,rhs,perm) = decomp_simp thm
    6.36 -  in if perm then Some{thm=thm, lhs=lhs, perm=true} else
    6.37 +  in if perm then [{thm=thm, lhs=lhs, perm=true}] else
    6.38       (* weak test for loops: *)
    6.39       if rewrite_rule_extra_vars prems lhs rhs orelse
    6.40          is_Var (head_of lhs) (* mk_cases may do this! *)
    6.41       then mk_eq_True mss thm
    6.42 -     else Some{thm=thm, lhs=lhs, perm=false}
    6.43 +     else rrule_eq_True(thm,lhs,rhs,mss,thm)
    6.44    end;
    6.45  
    6.46  fun orient_rrule mss thm =
    6.47    let val (sign,prems,lhs,rhs,perm) = decomp_simp thm
    6.48 -  in if perm then Some{thm=thm,lhs=lhs,perm=true}
    6.49 +  in if perm then [{thm=thm,lhs=lhs,perm=true}]
    6.50       else if looptest sign prems lhs rhs
    6.51            then if looptest sign prems rhs lhs
    6.52                 then mk_eq_True mss thm
    6.53                 else let val Mss{mk_rews={mk_sym,...},...} = mss
    6.54 -                    in apsome (fn thm' => {thm=thm', lhs=rhs, perm=false})
    6.55 -                              (mk_sym thm)
    6.56 +                    in case mk_sym thm of
    6.57 +                         None => []
    6.58 +                       | Some thm' => rrule_eq_True(thm',rhs,lhs,mss,thm)
    6.59                      end
    6.60 -          else Some{thm=thm, lhs=lhs, perm=false}
    6.61 +          else rrule_eq_True(thm,lhs,rhs,mss,thm)
    6.62    end;
    6.63  
    6.64  fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
    6.65  
    6.66  fun orient_comb_simps comb mk_rrule (mss,thms) =
    6.67    let val rews = extract_rews(mss,thms)
    6.68 -      val rrules = mapfilter mk_rrule rews
    6.69 +      val rrules = flat (map mk_rrule rews)
    6.70    in foldl comb (mss,rrules) end
    6.71  
    6.72  (* Add rewrite rules explicitly; do not reorient! *)
    6.73 @@ -1664,11 +1676,10 @@
    6.74    orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
    6.75  
    6.76  fun mss_of thms =
    6.77 -  foldl insert_rrule (empty_mss, mapfilter (mk_rrule empty_mss) thms);
    6.78 +  foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
    6.79  
    6.80 -fun safe_add_simps(mss,thms) =
    6.81 -  orient_comb_simps insert_rrule (orient_rrule mss) (mss,thms);
    6.82 -
    6.83 +fun extract_safe_rrules(mss,thm) =
    6.84 +  flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
    6.85  
    6.86  (* del_simps *)
    6.87  
    6.88 @@ -1806,7 +1817,7 @@
    6.89           if (lhs = lhs0) orelse
    6.90              (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
    6.91           then (trace_thm false "SUCCEEDED" thm; 
    6.92 -               Some(shyps, hyps, rhs, der::ders))
    6.93 +               Some(rhs, (shyps, hyps, der::ders)))
    6.94           else err()
    6.95       | _ => err()
    6.96    end;
    6.97 @@ -1848,93 +1859,83 @@
    6.98  
    6.99  fun rewritec (prover,sign_reft,maxt)
   6.100               (mss as Mss{rules, procs, termless, prems, ...}) 
   6.101 -             (shypst,hypst,t,ders) =
   6.102 +             (t:term,etc as (shypst,hypst,ders)) =
   6.103    let
   6.104 -      val signt = Sign.deref sign_reft;
   6.105 -      val tsigt = Sign.tsig_of signt;
   6.106 -      fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...}, lhs, perm} =
   6.107 -        let
   6.108 -            val _ =
   6.109 -              if Sign.subsig (Sign.deref sign_ref, signt) then ()
   6.110 -              else (trace_thm true "rewrite rule from different theory" thm;
   6.111 -                raise Pattern.MATCH);
   6.112 -            val rprop = if maxt = ~1 then prop
   6.113 -                        else Logic.incr_indexes([],maxt+1) prop;
   6.114 -            val rlhs = if maxt = ~1 then lhs
   6.115 -                       else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
   6.116 -            val insts = Pattern.match tsigt (rlhs,t);
   6.117 -            val prop' = ren_inst(insts,rprop,rlhs,t);
   6.118 -            val hyps' = union_term(hyps,hypst);
   6.119 -            val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
   6.120 -            val unconditional = (Logic.count_prems(prop',0) = 0);
   6.121 -            val maxidx' = if unconditional then maxt else maxidx+maxt+1
   6.122 -            val ct' = Cterm{sign_ref = sign_reft,       (*used for deriv only*)
   6.123 -                            t = prop',
   6.124 -                            T = propT,
   6.125 -                            maxidx = maxidx'}
   6.126 -            val der' = infer_derivs (RewriteC ct', [der]);
   6.127 -            val thm' = Thm{sign_ref = sign_reft, 
   6.128 -                           der = der',
   6.129 -                           shyps = shyps',
   6.130 -                           hyps = hyps',
   6.131 -                           prop = prop',
   6.132 -                           maxidx = maxidx'}
   6.133 -            val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
   6.134 -        in
   6.135 -          if perm andalso not(termless(rhs',lhs')) then None
   6.136 -          else
   6.137 -           (trace_thm false "Applying instance of rewrite rule:" thm;
   6.138 -            if unconditional
   6.139 -            then (trace_thm false "Rewriting:" thm'; 
   6.140 -                  Some(shyps', hyps', rhs', der'::ders))
   6.141 -            else (trace_thm false "Trying to rewrite:" thm';
   6.142 -                  case prover mss thm' of
   6.143 -                    None       => (trace_thm false "FAILED" thm'; None)
   6.144 -                  | Some(thm2) => check_conv(thm2,prop',ders)))
   6.145 -        end
   6.146 -
   6.147 -      fun rews [] = None
   6.148 -        | rews (rrule :: rrules) =
   6.149 -            let val opt = rew rrule handle Pattern.MATCH => None
   6.150 -            in case opt of None => rews rrules | some => some end;
   6.151 -
   6.152 -      fun sort_rrules rrs = let
   6.153 -        fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of 
   6.154 -                                        Const("==",_) $ _ $ _ => true
   6.155 -                                        | _                   => false 
   6.156 -        fun sort []        (re1,re2) = re1 @ re2
   6.157 -        |   sort (rr::rrs) (re1,re2) = if is_simple rr 
   6.158 -                                       then sort rrs (rr::re1,re2)
   6.159 -                                       else sort rrs (re1,rr::re2)
   6.160 -      in sort rrs ([],[]) 
   6.161 +    val signt = Sign.deref sign_reft;
   6.162 +    val tsigt = Sign.tsig_of signt;
   6.163 +    fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...}, lhs, perm} =
   6.164 +      let
   6.165 +        val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
   6.166 +                else (trace_thm true "rewrite rule from different theory" thm;
   6.167 +                      raise Pattern.MATCH);
   6.168 +        val rprop = if maxt = ~1 then prop
   6.169 +                    else Logic.incr_indexes([],maxt+1) prop;
   6.170 +        val rlhs = if maxt = ~1 then lhs
   6.171 +                   else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
   6.172 +        val insts = Pattern.match tsigt (rlhs,t);
   6.173 +        val prop' = ren_inst(insts,rprop,rlhs,t);
   6.174 +        val hyps' = union_term(hyps,hypst);
   6.175 +        val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
   6.176 +        val unconditional = (Logic.count_prems(prop',0) = 0);
   6.177 +        val maxidx' = if unconditional then maxt else maxidx+maxt+1
   6.178 +        val ct' = Cterm{sign_ref = sign_reft,       (*used for deriv only*)
   6.179 +                        t = prop', T = propT, maxidx = maxidx'}
   6.180 +        val der' = infer_derivs (RewriteC ct', [der]);
   6.181 +        val thm' = Thm{sign_ref = sign_reft, der = der', shyps = shyps',
   6.182 +                       hyps = hyps', prop = prop', maxidx = maxidx'}
   6.183 +        val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
   6.184 +      in
   6.185 +        if perm andalso not(termless(rhs',lhs')) then None
   6.186 +        else (trace_thm false "Applying instance of rewrite rule:" thm;
   6.187 +              if unconditional
   6.188 +              then (trace_thm false "Rewriting:" thm'; 
   6.189 +                    Some(rhs', (shyps', hyps', der'::ders)))
   6.190 +              else (trace_thm false "Trying to rewrite:" thm';
   6.191 +                    case prover mss thm' of
   6.192 +                      None       => (trace_thm false "FAILED" thm'; None)
   6.193 +                    | Some(thm2) => check_conv(thm2,prop',ders)))
   6.194        end
   6.195  
   6.196 -      fun proc_rews _ ([]:simproc list) = None
   6.197 -        | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
   6.198 -            if Pattern.matches tsigt (plhs, t) then
   6.199 -             (trace_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   6.200 -              case proc signt prems eta_t of
   6.201 -                None => (trace false "FAILED"; proc_rews eta_t ps)
   6.202 -              | Some raw_thm =>
   6.203 +    fun rews [] = None
   6.204 +      | rews (rrule :: rrules) =
   6.205 +          let val opt = rew rrule handle Pattern.MATCH => None
   6.206 +          in case opt of None => rews rrules | some => some end;
   6.207 +
   6.208 +    fun sort_rrules rrs = let
   6.209 +      fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of 
   6.210 +                                      Const("==",_) $ _ $ _ => true
   6.211 +                                      | _                   => false 
   6.212 +      fun sort []        (re1,re2) = re1 @ re2
   6.213 +        | sort (rr::rrs) (re1,re2) = if is_simple rr 
   6.214 +                                     then sort rrs (rr::re1,re2)
   6.215 +                                     else sort rrs (re1,rr::re2)
   6.216 +    in sort rrs ([],[]) end
   6.217 +
   6.218 +    fun proc_rews _ ([]:simproc list) = None
   6.219 +      | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
   6.220 +          if Pattern.matches tsigt (plhs, t) then
   6.221 +            (trace_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   6.222 +             case proc signt prems eta_t of
   6.223 +               None => (trace false "FAILED"; proc_rews eta_t ps)
   6.224 +             | Some raw_thm =>
   6.225                   (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   6.226 -                   (case rews (mk_procrule raw_thm) of
   6.227 -                     None => (trace false "IGNORED"; proc_rews eta_t ps)
   6.228 -                   | some => some)))
   6.229 -            else proc_rews eta_t ps;
   6.230 -  in
   6.231 -    (case t of
   6.232 -      Abs (_, _, body) $ u =>
   6.233 -        Some (shypst, hypst, subst_bound (u, body), ders)
   6.234 -     | _ =>
   6.235 -      (case rews (sort_rrules (Net.match_term rules t)) of
   6.236 -        None => proc_rews (Pattern.eta_contract t) (Net.match_term procs t)
   6.237 -      | some => some))
   6.238 +                  (case rews (mk_procrule raw_thm) of
   6.239 +                    None => (trace false "IGNORED"; proc_rews eta_t ps)
   6.240 +                  | some => some)))
   6.241 +          else proc_rews eta_t ps;
   6.242 +  in case t of
   6.243 +       Abs (_, _, body) $ u =>
   6.244 +         Some (subst_bound (u, body), etc)
   6.245 +     | _ => (case rews (sort_rrules (Net.match_term rules t)) of
   6.246 +               None => proc_rews (Pattern.eta_contract t)
   6.247 +                                 (Net.match_term procs t)
   6.248 +             | some => some)
   6.249    end;
   6.250  
   6.251  
   6.252  (* conversion to apply a congruence rule to a term *)
   6.253  
   6.254 -fun congc (prover,sign_reft,maxt) {thm=cong,lhs=lhs} (shypst,hypst,t,ders) =
   6.255 +fun congc (prover,sign_reft,maxt) {thm=cong,lhs=lhs} (t,(shypst,hypst,ders)) =
   6.256    let val signt = Sign.deref sign_reft;
   6.257        val tsig = Sign.tsig_of signt;
   6.258        val Thm{sign_ref,der,shyps,hyps,maxidx,prop,...} = cong
   6.259 @@ -1969,8 +1970,9 @@
   6.260                          None => err() | some => some)
   6.261    end;
   6.262  
   6.263 -fun bottomc ((simprem,useprem),prover,sign_ref,maxidx) =
   6.264 - let fun botc fail mss trec =
   6.265 +fun bottomc ((simprem,useprem,mutsimp),prover,sign_ref,maxidx) =
   6.266 +  let
   6.267 +    fun botc fail mss trec =
   6.268            (case subc mss trec of
   6.269               some as Some(trec1) =>
   6.270                 (case rewritec (prover,sign_ref,maxidx) mss trec1 of
   6.271 @@ -1981,43 +1983,39 @@
   6.272                    Some(trec2) => botc false mss trec2
   6.273                  | None => if fail then None else Some(trec)))
   6.274  
   6.275 -     and try_botc mss trec = (case botc true mss trec of
   6.276 +    and try_botc mss trec = (case botc true mss trec of
   6.277                                  Some(trec1) => trec1
   6.278                                | None => trec)
   6.279  
   6.280 -     and subc (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless})
   6.281 -              (trec as (shyps,hyps,t0,ders)) =
   6.282 +    and subc (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless})
   6.283 +             (trec as (t0:term,etc:sort list*term list * rule mtree list)) =
   6.284         (case t0 of
   6.285             Abs(a,T,t) =>
   6.286               let val b = variant bounds a
   6.287                   val v = Free("." ^ b,T)
   6.288                   val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
   6.289 -             in case botc true mss' 
   6.290 -                       (shyps,hyps,subst_bound (v,t),ders) of
   6.291 -                  Some(shyps',hyps',t',ders') =>
   6.292 -                    Some(shyps', hyps', Abs(a, T, abstract_over(v,t')), ders')
   6.293 +             in case botc true mss' (subst_bound(v,t),etc) of
   6.294 +                  Some(t',etc') => Some(Abs(a, T, abstract_over(v,t')), etc')
   6.295                  | None => None
   6.296               end
   6.297           | t$u => (case t of
   6.298 -             Const("==>",_)$s  => Some(impc(shyps,hyps,s,u,mss,ders))
   6.299 +             Const("==>",_)$s  => Some(snd(impc([],s,u,mss,etc)))
   6.300             | Abs(_,_,body) =>
   6.301 -               let val trec = (shyps,hyps,subst_bound (u,body),ders)
   6.302 +               let val trec = (subst_bound(u,body), etc)
   6.303                 in case subc mss trec of
   6.304                      None => Some(trec)
   6.305                    | trec => trec
   6.306                 end
   6.307             | _  =>
   6.308                 let fun appc() =
   6.309 -                     (case botc true mss (shyps,hyps,t,ders) of
   6.310 -                        Some(shyps1,hyps1,t1,ders1) =>
   6.311 -                          (case botc true mss (shyps1,hyps1,u,ders1) of
   6.312 -                             Some(shyps2,hyps2,u1,ders2) =>
   6.313 -                               Some(shyps2, hyps2, t1$u1, ders2)
   6.314 -                           | None => Some(shyps1, hyps1, t1$u, ders1))
   6.315 +                     (case botc true mss (t,etc) of
   6.316 +                        Some(t1,etc1) =>
   6.317 +                          (case botc true mss (u,etc1) of
   6.318 +                             Some(u1,etc2) => Some(t1$u1, etc2)
   6.319 +                           | None => Some(t1$u, etc1))
   6.320                        | None =>
   6.321 -                          (case botc true mss (shyps,hyps,u,ders) of
   6.322 -                             Some(shyps1,hyps1,u1,ders1) =>
   6.323 -                               Some(shyps1, hyps1, t$u1, ders1)
   6.324 +                          (case botc true mss (u,etc) of
   6.325 +                             Some(u1,etc1) => Some(t$u1, etc1)
   6.326                             | None => None))
   6.327                     val (h,ts) = strip_comb t
   6.328                 in case h of
   6.329 @@ -2031,24 +2029,67 @@
   6.330                 end)
   6.331           | _ => None)
   6.332  
   6.333 -     and impc(shyps, hyps, s, u, mss, ders) =
   6.334 -       let val (shyps1,hyps1,s1,ders1) =
   6.335 -             if simprem then try_botc mss (shyps,hyps,s,ders)
   6.336 -                        else (shyps,hyps,s,ders);
   6.337 -           val maxidx1 = maxidx_of_term s1
   6.338 -           val mss1 =
   6.339 -             if not useprem then mss else
   6.340 -             if maxidx1 <> ~1 then (trace_term true
   6.341 -"Cannot add premise as rewrite rule because it contains (type) unknowns:"
   6.342 -                                                  (Sign.deref sign_ref) s1; mss)
   6.343 -             else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1, 
   6.344 -                                              T=propT, maxidx= ~1})
   6.345 -                  in safe_add_simps(add_prems(mss,[thm]), [thm]) end
   6.346 -           val (shyps2,hyps2,u1,ders2) = try_botc mss1 (shyps1,hyps1,u,ders1)
   6.347 -           val hyps3 = if gen_mem (op aconv) (s1, hyps1)
   6.348 -                       then hyps2 else hyps2\s1
   6.349 -       in (shyps2, hyps3, Logic.mk_implies(s1,u1), ders2) 
   6.350 -       end
   6.351 +    and impc(prems, prem, conc, mss, etc) =
   6.352 +      let val (prem1,etc1) = if simprem then try_botc mss (prem,etc)
   6.353 +                             else (prem,etc)
   6.354 +      in impc1(prems, prem1, conc, mss, etc1) end
   6.355 +
   6.356 +    and impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
   6.357 +      let
   6.358 +        fun uncond({thm,lhs,...}:rrule) =
   6.359 +          if nprems_of thm = 0 then Some lhs else None
   6.360 +
   6.361 +        val (rrules1,lhss1,mss1) =
   6.362 +          if not useprem then ([],[],mss) else
   6.363 +          if maxidx_of_term prem1 <> ~1
   6.364 +          then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
   6.365 +                           (Sign.deref sign_ref) prem1;
   6.366 +                ([],[],mss))
   6.367 +          else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, 
   6.368 +                                           T=propT, maxidx= ~1})
   6.369 +                   val rrules1 = extract_safe_rrules(mss,thm)
   6.370 +                   val lhss1 = if mutsimp then mapfilter uncond rrules1 else []
   6.371 +                   val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
   6.372 +               in (rrules1, lhss1, mss1) end
   6.373 +
   6.374 +        fun rebuild(conc2,(shyps2,hyps2,ders2)) =
   6.375 +          let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
   6.376 +                           then hyps2 else hyps2\prem1
   6.377 +              val trec = (Logic.mk_implies(prem1,conc2),
   6.378 +                          (shyps2,hyps2',ders2))
   6.379 +          in case rewritec (prover,sign_ref,maxidx) mss trec of
   6.380 +               None => (None,trec)
   6.381 +             | Some(Const("==>",_)$prem$conc,etc) =>
   6.382 +                 impc(prems,prem,conc,mss,etc)
   6.383 +             | Some(trec') => (None,trec')
   6.384 +          end
   6.385 +
   6.386 +        fun simpconc() =
   6.387 +          case conc of
   6.388 +            Const("==>",_)$s$t =>
   6.389 +              (case impc(prems@[prem1],s,t,mss1,etc1) of
   6.390 +                 (Some(i,prem),(conc2,etc2)) =>
   6.391 +                    let val impl = Logic.mk_implies(prem1,conc2)
   6.392 +                    in if i=0 then impc1(prems,prem,impl,mss,etc2)
   6.393 +                       else (Some(i-1,prem),(impl,etc2))
   6.394 +                    end
   6.395 +               | (None,trec) => rebuild(trec))
   6.396 +          | _ => rebuild(try_botc mss1 (conc,etc1))
   6.397 +
   6.398 +      in if mutsimp
   6.399 +         then let val sg = Sign.deref sign_ref
   6.400 +                  val tsig = #tsig(Sign.rep_sg sg)
   6.401 +                  fun reducible t =
   6.402 +                    exists (fn lhs => Pattern.matches_subterm tsig (lhs,t))
   6.403 +                           lhss1;
   6.404 +              in case dropwhile (not o reducible) prems of
   6.405 +                   [] => simpconc()
   6.406 +                 | red::rest => (trace_term false "Can now reduce premise" sg
   6.407 +                                            red;
   6.408 +                                 (Some(length rest,prem1),(conc,etc1)))
   6.409 +              end
   6.410 +         else simpconc()
   6.411 +      end
   6.412  
   6.413   in try_botc end;
   6.414  
   6.415 @@ -2057,7 +2098,10 @@
   6.416  
   6.417  (*
   6.418    Parameters:
   6.419 -    mode = (simplify A, use A in simplifying B) when simplifying A ==> B
   6.420 +    mode = (simplify A,
   6.421 +            use A in simplifying B,
   6.422 +            use prems of B (if B is again a meta-impl.) to simplify A)
   6.423 +           when simplifying A ==> B
   6.424      mss: contains equality theorems of the form [|p1,...|] ==> t==u
   6.425      prover: how to solve premises in conditional rewrites and congruences
   6.426  *)
   6.427 @@ -2066,9 +2110,8 @@
   6.428  
   6.429  fun rewrite_cterm mode mss prover ct =
   6.430    let val Cterm {sign_ref, t, T, maxidx} = ct;
   6.431 -      val (shyps,hyps,u,ders) =
   6.432 -        bottomc (mode,prover, sign_ref, maxidx) mss 
   6.433 -                (add_term_sorts(t,[]), [], t, []);
   6.434 +      val (u,(shyps,hyps,ders)) = bottomc (mode,prover, sign_ref, maxidx) mss 
   6.435 +                                          (t, (add_term_sorts(t,[]), [], []));
   6.436        val prop = Logic.mk_equals(t,u)
   6.437    in
   6.438        Thm{sign_ref = sign_ref,