src/Pure/thm.ML
changeset 4740 0136b5bbe9fe
parent 4716 a291e858061c
child 4785 52fa5258db2e
     1.1 --- a/src/Pure/thm.ML	Thu Mar 12 12:48:49 1998 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Mar 12 12:49:24 1998 +0100
     1.3 @@ -1682,6 +1682,9 @@
     1.4  fun extract_safe_rrules(mss,thm) =
     1.5    flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
     1.6  
     1.7 +fun add_safe_simp(mss,thm) =
     1.8 +  foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
     1.9 +
    1.10  (* del_simps *)
    1.11  
    1.12  fun del_rrule(mss as Mss {rules,...},
    1.13 @@ -2000,7 +2003,7 @@
    1.14                  | None => None
    1.15               end
    1.16           | t$u => (case t of
    1.17 -             Const("==>",_)$s  => Some(snd(impc([],s,u,mss,etc)))
    1.18 +             Const("==>",_)$s  => Some(impc(s,u,mss,etc))
    1.19             | Abs(_,_,body) =>
    1.20                 let val trec = (subst_bound(u,body), etc)
    1.21                 in case subc mss trec of
    1.22 @@ -2030,28 +2033,32 @@
    1.23                 end)
    1.24           | _ => None)
    1.25  
    1.26 -    and impc(prems, prem, conc, mss, etc) =
    1.27 -      let val (prem1,etc1) = if simprem then try_botc mss (prem,etc)
    1.28 -                             else (prem,etc)
    1.29 -      in impc1(prems, prem1, conc, mss, etc1) end
    1.30 +    and impc args =
    1.31 +      if mutsimp
    1.32 +      then let val (prem, conc, mss, etc) = args
    1.33 +           in snd(mut_impc([], prem, conc, mss, etc)) end
    1.34 +      else nonmut_impc args
    1.35  
    1.36 -    and impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
    1.37 +    and mut_impc (prems, prem, conc, mss, etc) =
    1.38 +      let val (prem1,etc1) = try_botc mss (prem,etc)
    1.39 +      in mut_impc1(prems, prem1, conc, mss, etc1) end
    1.40 +
    1.41 +    and mut_impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
    1.42        let
    1.43          fun uncond({thm,lhs,...}:rrule) =
    1.44            if nprems_of thm = 0 then Some lhs else None
    1.45  
    1.46 -        val (rrules1,lhss1,mss1) =
    1.47 -          if not useprem then ([],[],mss) else
    1.48 +        val (lhss1,mss1) =
    1.49            if maxidx_of_term prem1 <> ~1
    1.50            then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
    1.51                             (Sign.deref sign_ref) prem1;
    1.52 -                ([],[],mss))
    1.53 +                ([],mss))
    1.54            else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, 
    1.55                                             T=propT, maxidx= ~1})
    1.56                     val rrules1 = extract_safe_rrules(mss,thm)
    1.57 -                   val lhss1 = if mutsimp then mapfilter uncond rrules1 else []
    1.58 +                   val lhss1 = mapfilter uncond rrules1
    1.59                     val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
    1.60 -               in (rrules1, lhss1, mss1) end
    1.61 +               in (lhss1, mss1) end
    1.62  
    1.63          fun disch1(conc2,(shyps2,hyps2,ders2)) =
    1.64            let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
    1.65 @@ -2063,24 +2070,23 @@
    1.66            in case rewritec (prover,sign_ref,maxidx) mss trec of
    1.67                 None => (None,trec)
    1.68               | Some(Const("==>",_)$prem$conc,etc) =>
    1.69 -                 impc(prems,prem,conc,mss,etc)
    1.70 +                 mut_impc(prems,prem,conc,mss,etc)
    1.71               | Some(trec') => (None,trec')
    1.72            end
    1.73  
    1.74          fun simpconc() =
    1.75            case conc of
    1.76              Const("==>",_)$s$t =>
    1.77 -              (case impc(prems@[prem1],s,t,mss1,etc1) of
    1.78 +              (case mut_impc(prems@[prem1],s,t,mss1,etc1) of
    1.79                   (Some(i,prem),trec2) =>
    1.80                      let val trec2' = disch1 trec2
    1.81 -                    in if i=0 then impc1(prems,prem,fst trec2',mss,snd trec2')
    1.82 +                    in if i=0 then mut_impc1(prems,prem,fst trec2',mss,snd trec2')
    1.83                         else (Some(i-1,prem),trec2')
    1.84                      end
    1.85                 | (None,trec) => rebuild(trec))
    1.86            | _ => rebuild(try_botc mss1 (conc,etc1))
    1.87  
    1.88 -      in if mutsimp
    1.89 -         then let val sg = Sign.deref sign_ref
    1.90 +      in let val sg = Sign.deref sign_ref
    1.91                    val tsig = #tsig(Sign.rep_sg sg)
    1.92                    fun reducible t =
    1.93                      exists (fn lhs => Pattern.matches_subterm tsig (lhs,t))
    1.94 @@ -2091,9 +2097,26 @@
    1.95                                              red;
    1.96                                   (Some(length rest,prem1),(conc,etc1)))
    1.97                end
    1.98 -         else simpconc()
    1.99        end
   1.100  
   1.101 +     (* legacy code - only for backwards compatibility *)
   1.102 +     and nonmut_impc(prem, conc, mss, etc as (_,hyps1,_)) =
   1.103 +       let val (prem1,etc1) = if simprem then try_botc mss (prem,etc)
   1.104 +                              else (prem,etc)
   1.105 +           val maxidx1 = maxidx_of_term prem1
   1.106 +           val mss1 =
   1.107 +             if not useprem then mss else
   1.108 +             if maxidx1 <> ~1
   1.109 +             then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
   1.110 +                              (Sign.deref sign_ref) prem1;
   1.111 +                   mss)
   1.112 +             else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, 
   1.113 +                                              T=propT, maxidx= ~1})
   1.114 +                  in add_safe_simp(add_prems(mss,[thm]), thm) end
   1.115 +           val (conc2,(shyps2,hyps2,ders2)) = try_botc mss1 (conc,etc1)
   1.116 +           val hyps2' = if prem1 mem hyps1 then hyps2 else hyps2\prem1
   1.117 +       in (Logic.mk_implies(prem1,conc2), (shyps2, hyps2', ders2)) end
   1.118 +
   1.119   in try_botc end;
   1.120  
   1.121