Completely reimplemented mutual simplification of premises.
authorberghofe
Mon Sep 30 16:38:22 2002 +0200 (2002-09-30)
changeset 136076908230623a3
parent 13606 2f121149acfe
child 13608 9a6f43b8eae1
Completely reimplemented mutual simplification of premises.
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon Sep 30 16:37:44 2002 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Sep 30 16:38:22 2002 +0200
     1.3 @@ -95,8 +95,8 @@
     1.4    let val {sign, prop, ...} = rep_thm thm
     1.5    in trace_term false a sign prop end;
     1.6  
     1.7 -fun trace_named_thm a thm =
     1.8 -  trace_thm (a ^ " " ^ quote(Thm.name_of_thm thm) ^ ":") thm;
     1.9 +fun trace_named_thm a (thm, name) =
    1.10 +  trace_thm (a ^ (if name = "" then "" else " " ^ quote name) ^ ":") thm;
    1.11  
    1.12  end;
    1.13  
    1.14 @@ -105,8 +105,9 @@
    1.15  
    1.16  (* basic components *)
    1.17  
    1.18 -type rrule = {thm: thm, lhs: term, elhs: cterm, fo: bool, perm: bool};
    1.19 +type rrule = {thm: thm, name: string, lhs: term, elhs: cterm, fo: bool, perm: bool};
    1.20  (* thm: the rewrite rule
    1.21 +   name: name of theorem from which rewrite rule was extracted
    1.22     lhs: the left-hand side
    1.23     elhs: the etac-contracted lhs.
    1.24     fo:  use first-order matching
    1.25 @@ -230,17 +231,17 @@
    1.26  
    1.27  (* add_simps *)
    1.28  
    1.29 -fun mk_rrule2{thm,lhs,elhs,perm} =
    1.30 +fun mk_rrule2{thm, name, lhs, elhs, perm} =
    1.31    let val fo = Pattern.first_order (term_of elhs) orelse not(Pattern.pattern (term_of elhs))
    1.32 -  in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
    1.33 +  in {thm=thm, name=name, lhs=lhs, elhs=elhs, fo=fo, perm=perm} end
    1.34  
    1.35 -fun insert_rrule(mss as Mss {rules,...},
    1.36 -                 rrule as {thm,lhs,elhs,perm}) =
    1.37 -  (trace_named_thm "Adding rewrite rule" thm;
    1.38 +fun insert_rrule quiet (mss as Mss {rules,...},
    1.39 +                 rrule as {thm,name,lhs,elhs,perm}) =
    1.40 +  (trace_named_thm "Adding rewrite rule" (thm, name);
    1.41     let val rrule2 as {elhs,...} = mk_rrule2 rrule
    1.42         val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
    1.43     in upd_rules(mss,rules') end
    1.44 -   handle Net.INSERT =>
    1.45 +   handle Net.INSERT => if quiet then mss else
    1.46       (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
    1.47  
    1.48  fun vperm (Var _, Var _) = true
    1.49 @@ -296,49 +297,51 @@
    1.50      else (lhs, rhs)
    1.51    end;
    1.52  
    1.53 -fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
    1.54 +fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) (thm, name) =
    1.55    case mk_eq_True thm of
    1.56      None => []
    1.57 -  | Some eq_True => let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
    1.58 -                    in [{thm=eq_True, lhs=lhs, elhs=elhs, perm=false}] end;
    1.59 +  | Some eq_True =>
    1.60 +      let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
    1.61 +      in [{thm=eq_True, name=name, lhs=lhs, elhs=elhs, perm=false}] end;
    1.62  
    1.63  (* create the rewrite rule and possibly also the ==True variant,
    1.64     in case there are extra vars on the rhs *)
    1.65 -fun rrule_eq_True(thm,lhs,elhs,rhs,mss,thm2) =
    1.66 -  let val rrule = {thm=thm, lhs=lhs, elhs=elhs, perm=false}
    1.67 +fun rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm2) =
    1.68 +  let val rrule = {thm=thm, name=name, lhs=lhs, elhs=elhs, perm=false}
    1.69    in if (term_varnames rhs)  subset (term_varnames lhs) andalso
    1.70          (term_tvars rhs) subset (term_tvars lhs)
    1.71       then [rrule]
    1.72 -     else mk_eq_True mss thm2 @ [rrule]
    1.73 +     else mk_eq_True mss (thm2, name) @ [rrule]
    1.74    end;
    1.75  
    1.76 -fun mk_rrule mss thm =
    1.77 +fun mk_rrule mss (thm, name) =
    1.78    let val (_,prems,lhs,elhs,rhs,perm) = decomp_simp thm
    1.79 -  in if perm then [{thm=thm, lhs=lhs, elhs=elhs, perm=true}] else
    1.80 +  in if perm then [{thm=thm, name=name, lhs=lhs, elhs=elhs, perm=true}] else
    1.81       (* weak test for loops: *)
    1.82       if rewrite_rule_extra_vars prems lhs rhs orelse
    1.83          is_Var (term_of elhs)
    1.84 -     then mk_eq_True mss thm
    1.85 -     else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
    1.86 +     then mk_eq_True mss (thm, name)
    1.87 +     else rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm)
    1.88    end;
    1.89  
    1.90 -fun orient_rrule mss thm =
    1.91 +fun orient_rrule mss (thm, name) =
    1.92    let val (sign,prems,lhs,elhs,rhs,perm) = decomp_simp thm
    1.93 -  in if perm then [{thm=thm,lhs=lhs,elhs=elhs,perm=true}]
    1.94 +  in if perm then [{thm=thm, name=name, lhs=lhs, elhs=elhs, perm=true}]
    1.95       else if reorient sign prems lhs rhs
    1.96            then if reorient sign prems rhs lhs
    1.97 -               then mk_eq_True mss thm
    1.98 +               then mk_eq_True mss (thm, name)
    1.99                 else let val Mss{mk_rews={mk_sym,...},...} = mss
   1.100                      in case mk_sym thm of
   1.101                           None => []
   1.102                         | Some thm' =>
   1.103                             let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
   1.104 -                           in rrule_eq_True(thm',lhs',elhs',rhs',mss,thm) end
   1.105 +                           in rrule_eq_True(thm',name,lhs',elhs',rhs',mss,thm) end
   1.106                      end
   1.107 -          else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
   1.108 +          else rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm)
   1.109    end;
   1.110  
   1.111 -fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
   1.112 +fun extract_rews(Mss{mk_rews = {mk,...},...},thms) =
   1.113 +  flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
   1.114  
   1.115  fun orient_comb_simps comb mk_rrule (mss,thms) =
   1.116    let val rews = extract_rews(mss,thms)
   1.117 @@ -347,17 +350,14 @@
   1.118  
   1.119  (* Add rewrite rules explicitly; do not reorient! *)
   1.120  fun add_simps(mss,thms) =
   1.121 -  orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
   1.122 +  orient_comb_simps (insert_rrule false) (mk_rrule mss) (mss,thms);
   1.123  
   1.124 -fun mss_of thms =
   1.125 -  foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
   1.126 +fun mss_of thms = foldl (insert_rrule false) (empty_mss, flat
   1.127 +  (map (fn thm => mk_rrule empty_mss (thm, Thm.name_of_thm thm)) thms));
   1.128  
   1.129  fun extract_safe_rrules(mss,thm) =
   1.130    flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
   1.131  
   1.132 -fun add_safe_simp(mss,thm) =
   1.133 -  foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
   1.134 -
   1.135  (* del_simps *)
   1.136  
   1.137  fun del_rrule(mss as Mss {rules,...},
   1.138 @@ -517,10 +517,6 @@
   1.139      Science of Computer Programming 3 (1983), pages 119-149.
   1.140  *)
   1.141  
   1.142 -type prover = meta_simpset -> thm -> thm option;
   1.143 -type termrec = (Sign.sg_ref * term list) * term;
   1.144 -type conv = meta_simpset -> termrec -> termrec;
   1.145 -
   1.146  val dest_eq = Drule.dest_equals o cprop_of;
   1.147  val lhs_of = fst o dest_eq;
   1.148  val rhs_of = snd o dest_eq;
   1.149 @@ -549,7 +545,7 @@
   1.150    let val (_,prems,lhs,elhs,rhs,_) = decomp_simp thm
   1.151    in if rewrite_rule_extra_vars prems lhs rhs
   1.152       then (prthm true "Extra vars on rhs:" thm; [])
   1.153 -     else [mk_rrule2{thm=thm, lhs=lhs, elhs=elhs, perm=false}]
   1.154 +     else [mk_rrule2{thm=thm, name="", lhs=lhs, elhs=elhs, perm=false}]
   1.155    end;
   1.156  
   1.157  
   1.158 @@ -599,7 +595,7 @@
   1.159      val eta_t' = rhs_of eta_thm;
   1.160      val eta_t = term_of eta_t';
   1.161      val tsigt = Sign.tsig_of signt;
   1.162 -    fun rew {thm, lhs, elhs, fo, perm} =
   1.163 +    fun rew {thm, name, lhs, elhs, fo, perm} =
   1.164        let
   1.165          val {sign, prop, maxidx, ...} = rep_thm thm;
   1.166          val _ = if Sign.subsig (sign, signt) then ()
   1.167 @@ -615,9 +611,9 @@
   1.168          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   1.169        in
   1.170          if perm andalso not (termless (rhs', lhs'))
   1.171 -        then (trace_named_thm "Cannot apply permutative rewrite rule" thm;
   1.172 +        then (trace_named_thm "Cannot apply permutative rewrite rule" (thm, name);
   1.173                trace_thm "Term does not become smaller:" thm'; None)
   1.174 -        else (trace_named_thm "Applying instance of rewrite rule" thm;
   1.175 +        else (trace_named_thm "Applying instance of rewrite rule" (thm, name);
   1.176             if unconditional
   1.177             then
   1.178               (trace_thm "Rewriting:" thm';
   1.179 @@ -701,11 +697,15 @@
   1.180  val (cA, (cB, cC)) =
   1.181    apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   1.182  
   1.183 -fun transitive' thm1 None = Some thm1
   1.184 -  | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
   1.185 +fun transitive1 None None = None
   1.186 +  | transitive1 (Some thm1) None = Some thm1
   1.187 +  | transitive1 None (Some thm2) = Some thm2
   1.188 +  | transitive1 (Some thm1) (Some thm2) = Some (transitive thm1 thm2)
   1.189  
   1.190 -fun transitive'' None thm2 = Some thm2
   1.191 -  | transitive'' (Some thm1) thm2 = Some (transitive thm1 thm2);
   1.192 +fun transitive2 thm = transitive1 (Some thm);
   1.193 +fun transitive3 thm = transitive1 thm o Some;
   1.194 +
   1.195 +fun imp_cong' e = combination (combination refl_implies e);
   1.196  
   1.197  fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   1.198    let
   1.199 @@ -716,12 +716,12 @@
   1.200               some as Some thm1 =>
   1.201                 (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   1.202                    Some (thm2, skel2) =>
   1.203 -                    transitive' (transitive thm1 thm2)
   1.204 +                    transitive2 (transitive thm1 thm2)
   1.205                        (botc skel2 mss (rhs_of thm2))
   1.206                  | None => some)
   1.207             | None =>
   1.208                 (case rewritec (prover, sign, maxidx) mss t of
   1.209 -                  Some (thm2, skel2) => transitive' thm2
   1.210 +                  Some (thm2, skel2) => transitive2 thm2
   1.211                      (botc skel2 mss (rhs_of thm2))
   1.212                  | None => None))
   1.213  
   1.214 @@ -744,7 +744,7 @@
   1.215           | t $ _ => (case t of
   1.216               Const ("==>", _) $ _  =>
   1.217                 let val (s, u) = Drule.dest_implies t0
   1.218 -               in impc (s, u, mss) end
   1.219 +               in impc t0 mss end
   1.220             | Abs _ =>
   1.221                 let val thm = beta_conversion false t0
   1.222                 in case subc skel0 mss (rhs_of thm) of
   1.223 @@ -786,7 +786,7 @@
   1.224                                 list_comb (h, replicate (length ts) dVar)
   1.225                             in case botc skel mss cl of
   1.226                                  None => thm
   1.227 -                              | Some thm' => transitive'' thm
   1.228 +                              | Some thm' => transitive3 thm
   1.229                                    (combination thm' (reflexive cr))
   1.230                             end handle TERM _ => error "congc result"
   1.231                                      | Pattern.MATCH => appc ()))
   1.232 @@ -794,126 +794,106 @@
   1.233                 end)
   1.234           | _ => None)
   1.235  
   1.236 -    and impc args =
   1.237 -      if mutsimp
   1.238 -      then let val (prem, conc, mss) = args
   1.239 -           in apsome snd (mut_impc ([], prem, conc, mss)) end
   1.240 -      else nonmut_impc args
   1.241 -
   1.242 -    and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
   1.243 -        None => mut_impc1 (prems, prem, conc, mss)
   1.244 -      | Some thm1 =>
   1.245 -          let val prem1 = rhs_of thm1
   1.246 -          in (case mut_impc1 (prems, prem1, conc, mss) of
   1.247 -              None => Some (None,
   1.248 -                combination (combination refl_implies thm1) (reflexive conc))
   1.249 -            | Some (x, thm2) => Some (x, transitive (combination (combination
   1.250 -                refl_implies thm1) (reflexive conc)) thm2))
   1.251 -          end)
   1.252 +    and impc ct mss =
   1.253 +      if mutsimp then mut_impc0 [] ct [] [] mss else nonmut_impc ct mss
   1.254  
   1.255 -    and mut_impc1 (prems, prem1, conc, mss) =
   1.256 -      let
   1.257 -        fun uncond ({thm, lhs, elhs, perm}) =
   1.258 -          if Thm.no_prems thm then Some lhs else None
   1.259 +    and rules_of_prem mss prem =
   1.260 +      if maxidx_of_term (term_of prem) <> ~1
   1.261 +      then (trace_cterm true
   1.262 +        "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], None))
   1.263 +      else
   1.264 +        let val asm = assume prem
   1.265 +        in (extract_safe_rrules (mss, asm), Some asm) end
   1.266  
   1.267 -        val (lhss1, mss1) =
   1.268 -          if maxidx_of_term (term_of prem1) <> ~1
   1.269 -          then (trace_cterm true
   1.270 -            "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   1.271 -                ([],mss))
   1.272 -          else let val thm = assume prem1
   1.273 -                   val rrules1 = extract_safe_rrules (mss, thm)
   1.274 -                   val lhss1 = mapfilter uncond rrules1
   1.275 -                   val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
   1.276 -               in (lhss1, mss1) end
   1.277 -
   1.278 -        fun disch1 thm =
   1.279 -          let val (cB', cC') = dest_eq thm
   1.280 -          in
   1.281 -            implies_elim (Thm.instantiate
   1.282 -              ([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
   1.283 -              (implies_intr prem1 thm)
   1.284 -          end
   1.285 +    and add_rrules (rrss, asms) mss =
   1.286 +      add_prems (foldl (insert_rrule true) (mss, flat rrss), mapfilter I asms)
   1.287  
   1.288 -        fun rebuild None = (case rewritec (prover, sign, maxidx) mss
   1.289 -            (mk_implies (prem1, conc)) of
   1.290 -              None => None
   1.291 -            | Some (thm, _) =>
   1.292 -                let val (prem, conc) = Drule.dest_implies (rhs_of thm)
   1.293 -                in (case mut_impc (prems, prem, conc, mss) of
   1.294 -                    None => Some (None, thm)
   1.295 -                  | Some (x, thm') => Some (x, transitive thm thm'))
   1.296 -                end handle TERM _ => Some (None, thm))
   1.297 -          | rebuild (Some thm2) =
   1.298 -            let val thm = disch1 thm2
   1.299 -            in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
   1.300 -                 None => Some (None, thm)
   1.301 -               | Some (thm', _) =>
   1.302 -                   let val (prem, conc) = Drule.dest_implies (rhs_of thm')
   1.303 -                   in (case mut_impc (prems, prem, conc, mss) of
   1.304 -                       None => Some (None, transitive thm thm')
   1.305 -                     | Some (x, thm'') =>
   1.306 -                         Some (x, transitive (transitive thm thm') thm''))
   1.307 -                   end handle TERM _ => Some (None, transitive thm thm'))
   1.308 -            end
   1.309 -
   1.310 -        fun simpconc () =
   1.311 -          let val (s, t) = Drule.dest_implies conc
   1.312 -          in case mut_impc (prems @ [prem1], s, t, mss1) of
   1.313 -               None => rebuild None
   1.314 -             | Some (Some i, thm2) =>
   1.315 -                  let
   1.316 -                    val (prem, cC') = Drule.dest_implies (rhs_of thm2);
   1.317 -                    val thm2' = transitive (disch1 thm2) (Thm.instantiate
   1.318 -                      ([], [(cA, prem1), (cB, prem), (cC, cC')])
   1.319 -                      Drule.swap_prems_eq)
   1.320 -                  in if i=0 then apsome (apsnd (transitive thm2'))
   1.321 -                       (mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
   1.322 -                     else Some (Some (i-1), thm2')
   1.323 -                  end
   1.324 -             | Some (None, thm) => rebuild (Some thm)
   1.325 -          end handle TERM _ => rebuild (botc skel0 mss1 conc)
   1.326 -
   1.327 -      in
   1.328 +    and disch r (prem, eq) =
   1.329 +      let
   1.330 +        val (lhs, rhs) = dest_eq eq;
   1.331 +        val eq' = implies_elim (Thm.instantiate
   1.332 +          ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
   1.333 +          (implies_intr prem eq)
   1.334 +      in if not r then eq' else
   1.335          let
   1.336 -          val tsig = Sign.tsig_of sign
   1.337 -          fun reducible t =
   1.338 -            exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
   1.339 -        in case dropwhile (not o reducible) prems of
   1.340 -            [] => simpconc ()
   1.341 -          | red::rest => (trace_cterm false "Can now reduce premise:" red;
   1.342 -              Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
   1.343 +          val (prem', concl) = dest_implies lhs;
   1.344 +          val (prem'', _) = dest_implies rhs
   1.345 +        in transitive (transitive
   1.346 +          (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
   1.347 +             Drule.swap_prems_eq) eq')
   1.348 +          (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
   1.349 +             Drule.swap_prems_eq)
   1.350          end
   1.351        end
   1.352  
   1.353 +    and rebuild [] _ _ _ _ eq = eq
   1.354 +      | rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) mss eq =
   1.355 +          let
   1.356 +            val mss' = add_rrules (rev rrss, rev asms) mss;
   1.357 +            val concl' =
   1.358 +              Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl);
   1.359 +            val dprem = apsome (curry (disch false) prem)
   1.360 +          in case rewritec (prover, sign, maxidx) mss' concl' of
   1.361 +              None => rebuild prems concl' rrss asms mss (dprem eq)
   1.362 +            | Some (eq', _) => transitive2 (foldl (disch false o swap)
   1.363 +                  (the (transitive3 (dprem eq) eq'), prems))
   1.364 +                (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) mss)
   1.365 +          end
   1.366 +          
   1.367 +    and mut_impc0 prems concl rrss asms mss =
   1.368 +      let
   1.369 +        val prems' = strip_imp_prems concl;
   1.370 +        val (rrss', asms') = split_list (map (rules_of_prem mss) prems')
   1.371 +      in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
   1.372 +        (asms @ asms') [] [] [] [] mss ~1 ~1
   1.373 +      end
   1.374 + 
   1.375 +    and mut_impc [] concl [] [] prems' rrss' asms' eqns mss changed k =
   1.376 +        transitive1 (foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
   1.377 +            (apsome (curry (disch false) prem) eq2)) (None, eqns ~~ prems'))
   1.378 +          (if changed > 0 then
   1.379 +             mut_impc (rev prems') concl (rev rrss') (rev asms')
   1.380 +               [] [] [] [] mss ~1 changed
   1.381 +           else rebuild prems' concl rrss' asms' mss
   1.382 +             (botc skel0 (add_rrules (rev rrss', rev asms') mss) concl))
   1.383 +
   1.384 +      | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
   1.385 +          prems' rrss' asms' eqns mss changed k =
   1.386 +        case (if k = 0 then None else botc skel0 (add_rrules
   1.387 +          (rev rrss' @ rrss, rev asms' @ asms) mss) prem) of
   1.388 +            None => mut_impc prems concl rrss asms (prem :: prems')
   1.389 +              (rrs :: rrss') (asm :: asms') (None :: eqns) mss changed
   1.390 +              (if k = 0 then 0 else k - 1)
   1.391 +          | Some eqn =>
   1.392 +            let
   1.393 +              val prem' = rhs_of eqn;
   1.394 +              val tprems = map term_of prems;
   1.395 +              val i = 1 + foldl Int.max (~1, map (fn p =>
   1.396 +                find_index_eq p tprems) (#hyps (rep_thm eqn)));
   1.397 +              val (rrs', asm') = rules_of_prem mss prem'
   1.398 +            in mut_impc prems concl rrss asms (prem' :: prems')
   1.399 +              (rrs' :: rrss') (asm' :: asms') (Some (foldr (disch true)
   1.400 +                (take (i, prems), imp_cong' eqn (reflexive (Drule.list_implies
   1.401 +                  (drop (i, prems), concl))))) :: eqns) mss (length prems') ~1
   1.402 +            end
   1.403 +
   1.404       (* legacy code - only for backwards compatibility *)
   1.405 -     and nonmut_impc (prem, conc, mss) =
   1.406 -       let val thm1 = if simprem then botc skel0 mss prem else None;
   1.407 +     and nonmut_impc ct mss =
   1.408 +       let val (prem, conc) = dest_implies ct;
   1.409 +           val thm1 = if simprem then botc skel0 mss prem else None;
   1.410             val prem1 = if_none (apsome rhs_of thm1) prem;
   1.411 -           val maxidx1 = maxidx_of_term (term_of prem1)
   1.412 -           val mss1 =
   1.413 -             if not useprem then mss else
   1.414 -             if maxidx1 <> ~1
   1.415 -             then (trace_cterm true
   1.416 -               "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   1.417 -                   mss)
   1.418 -             else let val thm = assume prem1
   1.419 -                  in add_safe_simp (add_prems (mss, [thm]), thm) end
   1.420 +           val mss1 = if not useprem then mss else add_rrules
   1.421 +             (apsnd single (apfst single (rules_of_prem mss prem1))) mss
   1.422         in (case botc skel0 mss1 conc of
   1.423             None => (case thm1 of
   1.424                 None => None
   1.425 -             | Some thm1' => Some (combination
   1.426 -                 (combination refl_implies thm1') (reflexive conc)))
   1.427 +             | Some thm1' => Some (imp_cong' thm1' (reflexive conc)))
   1.428           | Some thm2 =>
   1.429 -           let
   1.430 -             val conc2 = rhs_of thm2;
   1.431 -             val thm2' = implies_elim (Thm.instantiate
   1.432 -               ([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
   1.433 -               (implies_intr prem1 thm2)
   1.434 +           let val thm2' = disch false (prem1, thm2)
   1.435             in (case thm1 of
   1.436                 None => Some thm2'
   1.437 -             | Some thm1' => Some (transitive (combination
   1.438 -                 (combination refl_implies thm1') (reflexive conc)) thm2'))
   1.439 +             | Some thm1' =>
   1.440 +                 Some (transitive (imp_cong' thm1' (reflexive conc)) thm2'))
   1.441             end)
   1.442         end
   1.443  
   1.444 @@ -950,7 +930,7 @@
   1.445              val (thA,j) = case term_of A of
   1.446                    Const("=?=",_)$_$_ => (reflexive A, i)
   1.447                  | _ => (if pred i then cv A else reflexive A, i+1)
   1.448 -        in  combination (combination refl_implies thA) (gconv j B) end
   1.449 +        in  imp_cong' thA (gconv j B) end
   1.450          handle TERM _ => reflexive ct
   1.451    in gconv 1 end;
   1.452