src/Pure/meta_simplifier.ML
changeset 13607 6908230623a3
parent 13569 69a6b3aa0f38
child 13614 0b91269c0b13
equal deleted inserted replaced
13606:2f121149acfe 13607:6908230623a3
    93 
    93 
    94 fun trace_thm a thm =
    94 fun trace_thm a thm =
    95   let val {sign, prop, ...} = rep_thm thm
    95   let val {sign, prop, ...} = rep_thm thm
    96   in trace_term false a sign prop end;
    96   in trace_term false a sign prop end;
    97 
    97 
    98 fun trace_named_thm a thm =
    98 fun trace_named_thm a (thm, name) =
    99   trace_thm (a ^ " " ^ quote(Thm.name_of_thm thm) ^ ":") thm;
    99   trace_thm (a ^ (if name = "" then "" else " " ^ quote name) ^ ":") thm;
   100 
   100 
   101 end;
   101 end;
   102 
   102 
   103 
   103 
   104 (** meta simp sets **)
   104 (** meta simp sets **)
   105 
   105 
   106 (* basic components *)
   106 (* basic components *)
   107 
   107 
   108 type rrule = {thm: thm, lhs: term, elhs: cterm, fo: bool, perm: bool};
   108 type rrule = {thm: thm, name: string, lhs: term, elhs: cterm, fo: bool, perm: bool};
   109 (* thm: the rewrite rule
   109 (* thm: the rewrite rule
       
   110    name: name of theorem from which rewrite rule was extracted
   110    lhs: the left-hand side
   111    lhs: the left-hand side
   111    elhs: the etac-contracted lhs.
   112    elhs: the etac-contracted lhs.
   112    fo:  use first-order matching
   113    fo:  use first-order matching
   113    perm: the rewrite rule is permutative
   114    perm: the rewrite rule is permutative
   114 Remarks:
   115 Remarks:
   228         mk_rews, termless, depth);
   229         mk_rews, termless, depth);
   229 
   230 
   230 
   231 
   231 (* add_simps *)
   232 (* add_simps *)
   232 
   233 
   233 fun mk_rrule2{thm,lhs,elhs,perm} =
   234 fun mk_rrule2{thm, name, lhs, elhs, perm} =
   234   let val fo = Pattern.first_order (term_of elhs) orelse not(Pattern.pattern (term_of elhs))
   235   let val fo = Pattern.first_order (term_of elhs) orelse not(Pattern.pattern (term_of elhs))
   235   in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
   236   in {thm=thm, name=name, lhs=lhs, elhs=elhs, fo=fo, perm=perm} end
   236 
   237 
   237 fun insert_rrule(mss as Mss {rules,...},
   238 fun insert_rrule quiet (mss as Mss {rules,...},
   238                  rrule as {thm,lhs,elhs,perm}) =
   239                  rrule as {thm,name,lhs,elhs,perm}) =
   239   (trace_named_thm "Adding rewrite rule" thm;
   240   (trace_named_thm "Adding rewrite rule" (thm, name);
   240    let val rrule2 as {elhs,...} = mk_rrule2 rrule
   241    let val rrule2 as {elhs,...} = mk_rrule2 rrule
   241        val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
   242        val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
   242    in upd_rules(mss,rules') end
   243    in upd_rules(mss,rules') end
   243    handle Net.INSERT =>
   244    handle Net.INSERT => if quiet then mss else
   244      (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
   245      (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
   245 
   246 
   246 fun vperm (Var _, Var _) = true
   247 fun vperm (Var _, Var _) = true
   247   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   248   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   248   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   249   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   294   let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
   295   let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
   295     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
   296     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
   296     else (lhs, rhs)
   297     else (lhs, rhs)
   297   end;
   298   end;
   298 
   299 
   299 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
   300 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) (thm, name) =
   300   case mk_eq_True thm of
   301   case mk_eq_True thm of
   301     None => []
   302     None => []
   302   | Some eq_True => let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
   303   | Some eq_True =>
   303                     in [{thm=eq_True, lhs=lhs, elhs=elhs, perm=false}] end;
   304       let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
       
   305       in [{thm=eq_True, name=name, lhs=lhs, elhs=elhs, perm=false}] end;
   304 
   306 
   305 (* create the rewrite rule and possibly also the ==True variant,
   307 (* create the rewrite rule and possibly also the ==True variant,
   306    in case there are extra vars on the rhs *)
   308    in case there are extra vars on the rhs *)
   307 fun rrule_eq_True(thm,lhs,elhs,rhs,mss,thm2) =
   309 fun rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm2) =
   308   let val rrule = {thm=thm, lhs=lhs, elhs=elhs, perm=false}
   310   let val rrule = {thm=thm, name=name, lhs=lhs, elhs=elhs, perm=false}
   309   in if (term_varnames rhs)  subset (term_varnames lhs) andalso
   311   in if (term_varnames rhs)  subset (term_varnames lhs) andalso
   310         (term_tvars rhs) subset (term_tvars lhs)
   312         (term_tvars rhs) subset (term_tvars lhs)
   311      then [rrule]
   313      then [rrule]
   312      else mk_eq_True mss thm2 @ [rrule]
   314      else mk_eq_True mss (thm2, name) @ [rrule]
   313   end;
   315   end;
   314 
   316 
   315 fun mk_rrule mss thm =
   317 fun mk_rrule mss (thm, name) =
   316   let val (_,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   318   let val (_,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   317   in if perm then [{thm=thm, lhs=lhs, elhs=elhs, perm=true}] else
   319   in if perm then [{thm=thm, name=name, lhs=lhs, elhs=elhs, perm=true}] else
   318      (* weak test for loops: *)
   320      (* weak test for loops: *)
   319      if rewrite_rule_extra_vars prems lhs rhs orelse
   321      if rewrite_rule_extra_vars prems lhs rhs orelse
   320         is_Var (term_of elhs)
   322         is_Var (term_of elhs)
   321      then mk_eq_True mss thm
   323      then mk_eq_True mss (thm, name)
   322      else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
   324      else rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm)
   323   end;
   325   end;
   324 
   326 
   325 fun orient_rrule mss thm =
   327 fun orient_rrule mss (thm, name) =
   326   let val (sign,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   328   let val (sign,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   327   in if perm then [{thm=thm,lhs=lhs,elhs=elhs,perm=true}]
   329   in if perm then [{thm=thm, name=name, lhs=lhs, elhs=elhs, perm=true}]
   328      else if reorient sign prems lhs rhs
   330      else if reorient sign prems lhs rhs
   329           then if reorient sign prems rhs lhs
   331           then if reorient sign prems rhs lhs
   330                then mk_eq_True mss thm
   332                then mk_eq_True mss (thm, name)
   331                else let val Mss{mk_rews={mk_sym,...},...} = mss
   333                else let val Mss{mk_rews={mk_sym,...},...} = mss
   332                     in case mk_sym thm of
   334                     in case mk_sym thm of
   333                          None => []
   335                          None => []
   334                        | Some thm' =>
   336                        | Some thm' =>
   335                            let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
   337                            let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
   336                            in rrule_eq_True(thm',lhs',elhs',rhs',mss,thm) end
   338                            in rrule_eq_True(thm',name,lhs',elhs',rhs',mss,thm) end
   337                     end
   339                     end
   338           else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
   340           else rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm)
   339   end;
   341   end;
   340 
   342 
   341 fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
   343 fun extract_rews(Mss{mk_rews = {mk,...},...},thms) =
       
   344   flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
   342 
   345 
   343 fun orient_comb_simps comb mk_rrule (mss,thms) =
   346 fun orient_comb_simps comb mk_rrule (mss,thms) =
   344   let val rews = extract_rews(mss,thms)
   347   let val rews = extract_rews(mss,thms)
   345       val rrules = flat (map mk_rrule rews)
   348       val rrules = flat (map mk_rrule rews)
   346   in foldl comb (mss,rrules) end
   349   in foldl comb (mss,rrules) end
   347 
   350 
   348 (* Add rewrite rules explicitly; do not reorient! *)
   351 (* Add rewrite rules explicitly; do not reorient! *)
   349 fun add_simps(mss,thms) =
   352 fun add_simps(mss,thms) =
   350   orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
   353   orient_comb_simps (insert_rrule false) (mk_rrule mss) (mss,thms);
   351 
   354 
   352 fun mss_of thms =
   355 fun mss_of thms = foldl (insert_rrule false) (empty_mss, flat
   353   foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
   356   (map (fn thm => mk_rrule empty_mss (thm, Thm.name_of_thm thm)) thms));
   354 
   357 
   355 fun extract_safe_rrules(mss,thm) =
   358 fun extract_safe_rrules(mss,thm) =
   356   flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
   359   flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
   357 
       
   358 fun add_safe_simp(mss,thm) =
       
   359   foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
       
   360 
   360 
   361 (* del_simps *)
   361 (* del_simps *)
   362 
   362 
   363 fun del_rrule(mss as Mss {rules,...},
   363 fun del_rrule(mss as Mss {rules,...},
   364               rrule as {thm, elhs, ...}) =
   364               rrule as {thm, elhs, ...}) =
   515   Uses conversions, see:
   515   Uses conversions, see:
   516     L C Paulson, A higher-order implementation of rewriting,
   516     L C Paulson, A higher-order implementation of rewriting,
   517     Science of Computer Programming 3 (1983), pages 119-149.
   517     Science of Computer Programming 3 (1983), pages 119-149.
   518 *)
   518 *)
   519 
   519 
   520 type prover = meta_simpset -> thm -> thm option;
       
   521 type termrec = (Sign.sg_ref * term list) * term;
       
   522 type conv = meta_simpset -> termrec -> termrec;
       
   523 
       
   524 val dest_eq = Drule.dest_equals o cprop_of;
   520 val dest_eq = Drule.dest_equals o cprop_of;
   525 val lhs_of = fst o dest_eq;
   521 val lhs_of = fst o dest_eq;
   526 val rhs_of = snd o dest_eq;
   522 val rhs_of = snd o dest_eq;
   527 
   523 
   528 fun beta_eta_conversion t =
   524 fun beta_eta_conversion t =
   547 
   543 
   548 fun mk_procrule thm =
   544 fun mk_procrule thm =
   549   let val (_,prems,lhs,elhs,rhs,_) = decomp_simp thm
   545   let val (_,prems,lhs,elhs,rhs,_) = decomp_simp thm
   550   in if rewrite_rule_extra_vars prems lhs rhs
   546   in if rewrite_rule_extra_vars prems lhs rhs
   551      then (prthm true "Extra vars on rhs:" thm; [])
   547      then (prthm true "Extra vars on rhs:" thm; [])
   552      else [mk_rrule2{thm=thm, lhs=lhs, elhs=elhs, perm=false}]
   548      else [mk_rrule2{thm=thm, name="", lhs=lhs, elhs=elhs, perm=false}]
   553   end;
   549   end;
   554 
   550 
   555 
   551 
   556 (* conversion to apply the meta simpset to a term *)
   552 (* conversion to apply the meta simpset to a term *)
   557 
   553 
   597   let
   593   let
   598     val eta_thm = Thm.eta_conversion t;
   594     val eta_thm = Thm.eta_conversion t;
   599     val eta_t' = rhs_of eta_thm;
   595     val eta_t' = rhs_of eta_thm;
   600     val eta_t = term_of eta_t';
   596     val eta_t = term_of eta_t';
   601     val tsigt = Sign.tsig_of signt;
   597     val tsigt = Sign.tsig_of signt;
   602     fun rew {thm, lhs, elhs, fo, perm} =
   598     fun rew {thm, name, lhs, elhs, fo, perm} =
   603       let
   599       let
   604         val {sign, prop, maxidx, ...} = rep_thm thm;
   600         val {sign, prop, maxidx, ...} = rep_thm thm;
   605         val _ = if Sign.subsig (sign, signt) then ()
   601         val _ = if Sign.subsig (sign, signt) then ()
   606                 else (prthm true "Ignoring rewrite rule from different theory:" thm;
   602                 else (prthm true "Ignoring rewrite rule from different theory:" thm;
   607                       raise Pattern.MATCH);
   603                       raise Pattern.MATCH);
   613         val prop' = #prop (rep_thm thm');
   609         val prop' = #prop (rep_thm thm');
   614         val unconditional = (Logic.count_prems (prop',0) = 0);
   610         val unconditional = (Logic.count_prems (prop',0) = 0);
   615         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   611         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   616       in
   612       in
   617         if perm andalso not (termless (rhs', lhs'))
   613         if perm andalso not (termless (rhs', lhs'))
   618         then (trace_named_thm "Cannot apply permutative rewrite rule" thm;
   614         then (trace_named_thm "Cannot apply permutative rewrite rule" (thm, name);
   619               trace_thm "Term does not become smaller:" thm'; None)
   615               trace_thm "Term does not become smaller:" thm'; None)
   620         else (trace_named_thm "Applying instance of rewrite rule" thm;
   616         else (trace_named_thm "Applying instance of rewrite rule" (thm, name);
   621            if unconditional
   617            if unconditional
   622            then
   618            then
   623              (trace_thm "Rewriting:" thm';
   619              (trace_thm "Rewriting:" thm';
   624               let val lr = Logic.dest_equals prop;
   620               let val lr = Logic.dest_equals prop;
   625                   val Some thm'' = check_conv false eta_thm thm'
   621                   val Some thm'' = check_conv false eta_thm thm'
   699   end;
   695   end;
   700 
   696 
   701 val (cA, (cB, cC)) =
   697 val (cA, (cB, cC)) =
   702   apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   698   apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   703 
   699 
   704 fun transitive' thm1 None = Some thm1
   700 fun transitive1 None None = None
   705   | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
   701   | transitive1 (Some thm1) None = Some thm1
   706 
   702   | transitive1 None (Some thm2) = Some thm2
   707 fun transitive'' None thm2 = Some thm2
   703   | transitive1 (Some thm1) (Some thm2) = Some (transitive thm1 thm2)
   708   | transitive'' (Some thm1) thm2 = Some (transitive thm1 thm2);
   704 
       
   705 fun transitive2 thm = transitive1 (Some thm);
       
   706 fun transitive3 thm = transitive1 thm o Some;
       
   707 
       
   708 fun imp_cong' e = combination (combination refl_implies e);
   709 
   709 
   710 fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   710 fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   711   let
   711   let
   712     fun botc skel mss t =
   712     fun botc skel mss t =
   713           if is_Var skel then None
   713           if is_Var skel then None
   714           else
   714           else
   715           (case subc skel mss t of
   715           (case subc skel mss t of
   716              some as Some thm1 =>
   716              some as Some thm1 =>
   717                (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   717                (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   718                   Some (thm2, skel2) =>
   718                   Some (thm2, skel2) =>
   719                     transitive' (transitive thm1 thm2)
   719                     transitive2 (transitive thm1 thm2)
   720                       (botc skel2 mss (rhs_of thm2))
   720                       (botc skel2 mss (rhs_of thm2))
   721                 | None => some)
   721                 | None => some)
   722            | None =>
   722            | None =>
   723                (case rewritec (prover, sign, maxidx) mss t of
   723                (case rewritec (prover, sign, maxidx) mss t of
   724                   Some (thm2, skel2) => transitive' thm2
   724                   Some (thm2, skel2) => transitive2 thm2
   725                     (botc skel2 mss (rhs_of thm2))
   725                     (botc skel2 mss (rhs_of thm2))
   726                 | None => None))
   726                 | None => None))
   727 
   727 
   728     and try_botc mss t =
   728     and try_botc mss t =
   729           (case botc skel0 mss t of
   729           (case botc skel0 mss t of
   742                 | None => None
   742                 | None => None
   743              end
   743              end
   744          | t $ _ => (case t of
   744          | t $ _ => (case t of
   745              Const ("==>", _) $ _  =>
   745              Const ("==>", _) $ _  =>
   746                let val (s, u) = Drule.dest_implies t0
   746                let val (s, u) = Drule.dest_implies t0
   747                in impc (s, u, mss) end
   747                in impc t0 mss end
   748            | Abs _ =>
   748            | Abs _ =>
   749                let val thm = beta_conversion false t0
   749                let val thm = beta_conversion false t0
   750                in case subc skel0 mss (rhs_of thm) of
   750                in case subc skel0 mss (rhs_of thm) of
   751                     None => Some thm
   751                     None => Some thm
   752                   | Some thm' => Some (transitive thm thm')
   752                   | Some thm' => Some (transitive thm thm')
   784                              val dVar = Var(("", 0), dummyT)
   784                              val dVar = Var(("", 0), dummyT)
   785                              val skel =
   785                              val skel =
   786                                list_comb (h, replicate (length ts) dVar)
   786                                list_comb (h, replicate (length ts) dVar)
   787                            in case botc skel mss cl of
   787                            in case botc skel mss cl of
   788                                 None => thm
   788                                 None => thm
   789                               | Some thm' => transitive'' thm
   789                               | Some thm' => transitive3 thm
   790                                   (combination thm' (reflexive cr))
   790                                   (combination thm' (reflexive cr))
   791                            end handle TERM _ => error "congc result"
   791                            end handle TERM _ => error "congc result"
   792                                     | Pattern.MATCH => appc ()))
   792                                     | Pattern.MATCH => appc ()))
   793                   | _ => appc ()
   793                   | _ => appc ()
   794                end)
   794                end)
   795          | _ => None)
   795          | _ => None)
   796 
   796 
   797     and impc args =
   797     and impc ct mss =
   798       if mutsimp
   798       if mutsimp then mut_impc0 [] ct [] [] mss else nonmut_impc ct mss
   799       then let val (prem, conc, mss) = args
   799 
   800            in apsome snd (mut_impc ([], prem, conc, mss)) end
   800     and rules_of_prem mss prem =
   801       else nonmut_impc args
   801       if maxidx_of_term (term_of prem) <> ~1
   802 
   802       then (trace_cterm true
   803     and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
   803         "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], None))
   804         None => mut_impc1 (prems, prem, conc, mss)
   804       else
   805       | Some thm1 =>
   805         let val asm = assume prem
   806           let val prem1 = rhs_of thm1
   806         in (extract_safe_rrules (mss, asm), Some asm) end
   807           in (case mut_impc1 (prems, prem1, conc, mss) of
   807 
   808               None => Some (None,
   808     and add_rrules (rrss, asms) mss =
   809                 combination (combination refl_implies thm1) (reflexive conc))
   809       add_prems (foldl (insert_rrule true) (mss, flat rrss), mapfilter I asms)
   810             | Some (x, thm2) => Some (x, transitive (combination (combination
   810 
   811                 refl_implies thm1) (reflexive conc)) thm2))
   811     and disch r (prem, eq) =
   812           end)
       
   813 
       
   814     and mut_impc1 (prems, prem1, conc, mss) =
       
   815       let
   812       let
   816         fun uncond ({thm, lhs, elhs, perm}) =
   813         val (lhs, rhs) = dest_eq eq;
   817           if Thm.no_prems thm then Some lhs else None
   814         val eq' = implies_elim (Thm.instantiate
   818 
   815           ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
   819         val (lhss1, mss1) =
   816           (implies_intr prem eq)
   820           if maxidx_of_term (term_of prem1) <> ~1
   817       in if not r then eq' else
   821           then (trace_cterm true
       
   822             "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
       
   823                 ([],mss))
       
   824           else let val thm = assume prem1
       
   825                    val rrules1 = extract_safe_rrules (mss, thm)
       
   826                    val lhss1 = mapfilter uncond rrules1
       
   827                    val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
       
   828                in (lhss1, mss1) end
       
   829 
       
   830         fun disch1 thm =
       
   831           let val (cB', cC') = dest_eq thm
       
   832           in
       
   833             implies_elim (Thm.instantiate
       
   834               ([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
       
   835               (implies_intr prem1 thm)
       
   836           end
       
   837 
       
   838         fun rebuild None = (case rewritec (prover, sign, maxidx) mss
       
   839             (mk_implies (prem1, conc)) of
       
   840               None => None
       
   841             | Some (thm, _) =>
       
   842                 let val (prem, conc) = Drule.dest_implies (rhs_of thm)
       
   843                 in (case mut_impc (prems, prem, conc, mss) of
       
   844                     None => Some (None, thm)
       
   845                   | Some (x, thm') => Some (x, transitive thm thm'))
       
   846                 end handle TERM _ => Some (None, thm))
       
   847           | rebuild (Some thm2) =
       
   848             let val thm = disch1 thm2
       
   849             in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
       
   850                  None => Some (None, thm)
       
   851                | Some (thm', _) =>
       
   852                    let val (prem, conc) = Drule.dest_implies (rhs_of thm')
       
   853                    in (case mut_impc (prems, prem, conc, mss) of
       
   854                        None => Some (None, transitive thm thm')
       
   855                      | Some (x, thm'') =>
       
   856                          Some (x, transitive (transitive thm thm') thm''))
       
   857                    end handle TERM _ => Some (None, transitive thm thm'))
       
   858             end
       
   859 
       
   860         fun simpconc () =
       
   861           let val (s, t) = Drule.dest_implies conc
       
   862           in case mut_impc (prems @ [prem1], s, t, mss1) of
       
   863                None => rebuild None
       
   864              | Some (Some i, thm2) =>
       
   865                   let
       
   866                     val (prem, cC') = Drule.dest_implies (rhs_of thm2);
       
   867                     val thm2' = transitive (disch1 thm2) (Thm.instantiate
       
   868                       ([], [(cA, prem1), (cB, prem), (cC, cC')])
       
   869                       Drule.swap_prems_eq)
       
   870                   in if i=0 then apsome (apsnd (transitive thm2'))
       
   871                        (mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
       
   872                      else Some (Some (i-1), thm2')
       
   873                   end
       
   874              | Some (None, thm) => rebuild (Some thm)
       
   875           end handle TERM _ => rebuild (botc skel0 mss1 conc)
       
   876 
       
   877       in
       
   878         let
   818         let
   879           val tsig = Sign.tsig_of sign
   819           val (prem', concl) = dest_implies lhs;
   880           fun reducible t =
   820           val (prem'', _) = dest_implies rhs
   881             exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
   821         in transitive (transitive
   882         in case dropwhile (not o reducible) prems of
   822           (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
   883             [] => simpconc ()
   823              Drule.swap_prems_eq) eq')
   884           | red::rest => (trace_cterm false "Can now reduce premise:" red;
   824           (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
   885               Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
   825              Drule.swap_prems_eq)
   886         end
   826         end
   887       end
   827       end
   888 
   828 
       
   829     and rebuild [] _ _ _ _ eq = eq
       
   830       | rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) mss eq =
       
   831           let
       
   832             val mss' = add_rrules (rev rrss, rev asms) mss;
       
   833             val concl' =
       
   834               Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl);
       
   835             val dprem = apsome (curry (disch false) prem)
       
   836           in case rewritec (prover, sign, maxidx) mss' concl' of
       
   837               None => rebuild prems concl' rrss asms mss (dprem eq)
       
   838             | Some (eq', _) => transitive2 (foldl (disch false o swap)
       
   839                   (the (transitive3 (dprem eq) eq'), prems))
       
   840                 (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) mss)
       
   841           end
       
   842           
       
   843     and mut_impc0 prems concl rrss asms mss =
       
   844       let
       
   845         val prems' = strip_imp_prems concl;
       
   846         val (rrss', asms') = split_list (map (rules_of_prem mss) prems')
       
   847       in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
       
   848         (asms @ asms') [] [] [] [] mss ~1 ~1
       
   849       end
       
   850  
       
   851     and mut_impc [] concl [] [] prems' rrss' asms' eqns mss changed k =
       
   852         transitive1 (foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
       
   853             (apsome (curry (disch false) prem) eq2)) (None, eqns ~~ prems'))
       
   854           (if changed > 0 then
       
   855              mut_impc (rev prems') concl (rev rrss') (rev asms')
       
   856                [] [] [] [] mss ~1 changed
       
   857            else rebuild prems' concl rrss' asms' mss
       
   858              (botc skel0 (add_rrules (rev rrss', rev asms') mss) concl))
       
   859 
       
   860       | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
       
   861           prems' rrss' asms' eqns mss changed k =
       
   862         case (if k = 0 then None else botc skel0 (add_rrules
       
   863           (rev rrss' @ rrss, rev asms' @ asms) mss) prem) of
       
   864             None => mut_impc prems concl rrss asms (prem :: prems')
       
   865               (rrs :: rrss') (asm :: asms') (None :: eqns) mss changed
       
   866               (if k = 0 then 0 else k - 1)
       
   867           | Some eqn =>
       
   868             let
       
   869               val prem' = rhs_of eqn;
       
   870               val tprems = map term_of prems;
       
   871               val i = 1 + foldl Int.max (~1, map (fn p =>
       
   872                 find_index_eq p tprems) (#hyps (rep_thm eqn)));
       
   873               val (rrs', asm') = rules_of_prem mss prem'
       
   874             in mut_impc prems concl rrss asms (prem' :: prems')
       
   875               (rrs' :: rrss') (asm' :: asms') (Some (foldr (disch true)
       
   876                 (take (i, prems), imp_cong' eqn (reflexive (Drule.list_implies
       
   877                   (drop (i, prems), concl))))) :: eqns) mss (length prems') ~1
       
   878             end
       
   879 
   889      (* legacy code - only for backwards compatibility *)
   880      (* legacy code - only for backwards compatibility *)
   890      and nonmut_impc (prem, conc, mss) =
   881      and nonmut_impc ct mss =
   891        let val thm1 = if simprem then botc skel0 mss prem else None;
   882        let val (prem, conc) = dest_implies ct;
       
   883            val thm1 = if simprem then botc skel0 mss prem else None;
   892            val prem1 = if_none (apsome rhs_of thm1) prem;
   884            val prem1 = if_none (apsome rhs_of thm1) prem;
   893            val maxidx1 = maxidx_of_term (term_of prem1)
   885            val mss1 = if not useprem then mss else add_rrules
   894            val mss1 =
   886              (apsnd single (apfst single (rules_of_prem mss prem1))) mss
   895              if not useprem then mss else
       
   896              if maxidx1 <> ~1
       
   897              then (trace_cterm true
       
   898                "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
       
   899                    mss)
       
   900              else let val thm = assume prem1
       
   901                   in add_safe_simp (add_prems (mss, [thm]), thm) end
       
   902        in (case botc skel0 mss1 conc of
   887        in (case botc skel0 mss1 conc of
   903            None => (case thm1 of
   888            None => (case thm1 of
   904                None => None
   889                None => None
   905              | Some thm1' => Some (combination
   890              | Some thm1' => Some (imp_cong' thm1' (reflexive conc)))
   906                  (combination refl_implies thm1') (reflexive conc)))
       
   907          | Some thm2 =>
   891          | Some thm2 =>
   908            let
   892            let val thm2' = disch false (prem1, thm2)
   909              val conc2 = rhs_of thm2;
       
   910              val thm2' = implies_elim (Thm.instantiate
       
   911                ([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
       
   912                (implies_intr prem1 thm2)
       
   913            in (case thm1 of
   893            in (case thm1 of
   914                None => Some thm2'
   894                None => Some thm2'
   915              | Some thm1' => Some (transitive (combination
   895              | Some thm1' =>
   916                  (combination refl_implies thm1') (reflexive conc)) thm2'))
   896                  Some (transitive (imp_cong' thm1' (reflexive conc)) thm2'))
   917            end)
   897            end)
   918        end
   898        end
   919 
   899 
   920  in try_botc end;
   900  in try_botc end;
   921 
   901 
   948   let fun gconv i ct =
   928   let fun gconv i ct =
   949         let val (A,B) = Drule.dest_implies ct
   929         let val (A,B) = Drule.dest_implies ct
   950             val (thA,j) = case term_of A of
   930             val (thA,j) = case term_of A of
   951                   Const("=?=",_)$_$_ => (reflexive A, i)
   931                   Const("=?=",_)$_$_ => (reflexive A, i)
   952                 | _ => (if pred i then cv A else reflexive A, i+1)
   932                 | _ => (if pred i then cv A else reflexive A, i+1)
   953         in  combination (combination refl_implies thA) (gconv j B) end
   933         in  imp_cong' thA (gconv j B) end
   954         handle TERM _ => reflexive ct
   934         handle TERM _ => reflexive ct
   955   in gconv 1 end;
   935   in gconv 1 end;
   956 
   936 
   957 (* Rewrite A in !!x1,...,xn. A *)
   937 (* Rewrite A in !!x1,...,xn. A *)
   958 fun forall_conv cv ct =
   938 fun forall_conv cv ct =