src/Pure/thm.ML
changeset 4716 a291e858061c
parent 4713 bea2ab2e360b
child 4740 0136b5bbe9fe
     1.1 --- a/src/Pure/thm.ML	Tue Mar 10 14:27:44 1998 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Mar 10 16:47:26 1998 +0100
     1.3 @@ -1597,8 +1597,8 @@
     1.4    not ((term_tvars erhs) subset
     1.5         (term_tvars elhs  union  List.concat(map term_tvars prems)));
     1.6  
     1.7 -(*simple test for looping rewrite*)
     1.8 -fun looptest sign prems lhs rhs =
     1.9 +(*Simple test for looping rewrite rules and stupid orientations*)
    1.10 +fun reorient sign prems lhs rhs =
    1.11     rewrite_rule_extra_vars prems lhs rhs
    1.12    orelse
    1.13     is_Var (head_of lhs)
    1.14 @@ -1607,10 +1607,11 @@
    1.15    orelse
    1.16     (null prems andalso
    1.17      Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
    1.18 -(*the condition "null prems" in the last cases is necessary because
    1.19 -  conditional rewrites with extra variables in the conditions may terminate
    1.20 -  although the rhs is an instance of the lhs. Example:
    1.21 -  ?m < ?n ==> f(?n) == f(?m)*)
    1.22 +    (*the condition "null prems" is necessary because conditional rewrites
    1.23 +      with extra variables in the conditions may terminate although
    1.24 +      the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
    1.25 +  orelse
    1.26 +   (is_Const lhs andalso not(is_Const rhs))
    1.27  
    1.28  fun decomp_simp(thm as Thm {sign_ref, prop, ...}) =
    1.29    let val sign = Sign.deref sign_ref;
    1.30 @@ -1653,8 +1654,8 @@
    1.31  fun orient_rrule mss thm =
    1.32    let val (sign,prems,lhs,rhs,perm) = decomp_simp thm
    1.33    in if perm then [{thm=thm,lhs=lhs,perm=true}]
    1.34 -     else if looptest sign prems lhs rhs
    1.35 -          then if looptest sign prems rhs lhs
    1.36 +     else if reorient sign prems lhs rhs
    1.37 +          then if reorient sign prems rhs lhs
    1.38                 then mk_eq_True mss thm
    1.39                 else let val Mss{mk_rews={mk_sym,...},...} = mss
    1.40                      in case mk_sym thm of
    1.41 @@ -2052,11 +2053,13 @@
    1.42                     val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
    1.43                 in (rrules1, lhss1, mss1) end
    1.44  
    1.45 -        fun rebuild(conc2,(shyps2,hyps2,ders2)) =
    1.46 +        fun disch1(conc2,(shyps2,hyps2,ders2)) =
    1.47            let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
    1.48                             then hyps2 else hyps2\prem1
    1.49 -              val trec = (Logic.mk_implies(prem1,conc2),
    1.50 -                          (shyps2,hyps2',ders2))
    1.51 +          in (Logic.mk_implies(prem1,conc2),(shyps2,hyps2',ders2)) end
    1.52 +
    1.53 +        fun rebuild trec2 =
    1.54 +          let val trec = disch1 trec2
    1.55            in case rewritec (prover,sign_ref,maxidx) mss trec of
    1.56                 None => (None,trec)
    1.57               | Some(Const("==>",_)$prem$conc,etc) =>
    1.58 @@ -2068,10 +2071,10 @@
    1.59            case conc of
    1.60              Const("==>",_)$s$t =>
    1.61                (case impc(prems@[prem1],s,t,mss1,etc1) of
    1.62 -                 (Some(i,prem),(conc2,etc2)) =>
    1.63 -                    let val impl = Logic.mk_implies(prem1,conc2)
    1.64 -                    in if i=0 then impc1(prems,prem,impl,mss,etc2)
    1.65 -                       else (Some(i-1,prem),(impl,etc2))
    1.66 +                 (Some(i,prem),trec2) =>
    1.67 +                    let val trec2' = disch1 trec2
    1.68 +                    in if i=0 then impc1(prems,prem,fst trec2',mss,snd trec2')
    1.69 +                       else (Some(i-1,prem),trec2')
    1.70                      end
    1.71                 | (None,trec) => rebuild(trec))
    1.72            | _ => rebuild(try_botc mss1 (conc,etc1))