logic: loops -> rewrite_rule_ok
authornipkow
Tue Nov 04 12:58:10 1997 +0100 (1997-11-04)
changeset 411642606637f87f
parent 4115 9405ebe284bf
child 4117 cf71befb65e8
logic: loops -> rewrite_rule_ok
added rewrite_rule_extra_vars

thm: Rewrite rules must not introduce new type vars on rhs.
This lead to an incompleteness, is now banned, and the code
has been simplified.
src/Pure/logic.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/logic.ML	Tue Nov 04 12:46:50 1997 +0100
     1.2 +++ b/src/Pure/logic.ML	Tue Nov 04 12:58:10 1997 +0100
     1.3 @@ -26,7 +26,8 @@
     1.4    val list_flexpairs	: (term*term)list * term -> term
     1.5    val list_implies	: term list * term -> term
     1.6    val list_rename_params: string list * term -> term
     1.7 -  val loops		: Sign.sg -> term list -> term -> term
     1.8 +  val rewrite_rule_extra_vars: term list -> term -> term -> string option
     1.9 +  val rewrite_rule_ok   : Sign.sg -> term list -> term -> term
    1.10                            -> string option * bool
    1.11    val mk_equals		: term * term -> term
    1.12    val mk_flexpair	: term * term -> term
    1.13 @@ -350,7 +351,7 @@
    1.14  
    1.15  fun termless tu = (termord tu = LESS);
    1.16  
    1.17 -(** Check for looping rewrite rules **)
    1.18 +(** Test wellformedness of rewrite rules **)
    1.19  
    1.20  fun vperm (Var _, Var _) = true
    1.21    | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    1.22 @@ -373,18 +374,26 @@
    1.23    although the rhs is an instance of the lhs. Example:
    1.24    ?m < ?n ==> f(?n) == f(?m)*)
    1.25  
    1.26 -fun loops sign prems lhs rhs =
    1.27 +fun rewrite_rule_extra_vars prems elhs erhs =
    1.28 +  if not ((term_vars erhs) subset
    1.29 +          (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.30 +  then Some("extra Var(s) on rhs") else
    1.31 +  if not ((term_tvars erhs) subset
    1.32 +          (term_tvars elhs  union  List.concat(map term_tvars prems)))
    1.33 +  then Some("extra TVar(s) on rhs")
    1.34 +  else None;
    1.35 +
    1.36 +fun rewrite_rule_ok sign prems lhs rhs =
    1.37    let
    1.38      val elhs = Pattern.eta_contract lhs;
    1.39      val erhs = Pattern.eta_contract rhs;
    1.40      val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
    1.41                 andalso not (is_Var elhs)
    1.42 -  in (if not ((term_vars erhs) subset
    1.43 -              (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.44 -      then Some("extra Var(s) on rhs") else
    1.45 -      if not perm andalso looptest sign prems elhs erhs
    1.46 -      then Some("loops")
    1.47 -      else None
    1.48 +  in (case rewrite_rule_extra_vars prems elhs erhs of
    1.49 +        None => if not perm andalso looptest sign prems elhs erhs
    1.50 +                then Some("loops")
    1.51 +                else None
    1.52 +      | some => some
    1.53        ,perm)
    1.54    end;
    1.55  
     2.1 --- a/src/Pure/thm.ML	Tue Nov 04 12:46:50 1997 +0100
     2.2 +++ b/src/Pure/thm.ML	Tue Nov 04 12:58:10 1997 +0100
     2.3 @@ -1571,7 +1571,7 @@
     2.4      val concl = Logic.strip_imp_concl prop;
     2.5      val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
     2.6        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     2.7 -  in case Logic.loops sign prems lhs rhs of
     2.8 +  in case Logic.rewrite_rule_ok sign prems lhs rhs of
     2.9       (None,perm) => Some {thm = thm, lhs = lhs, perm = perm}
    2.10     | (Some msg,_) =>
    2.11          (prtm true ("ignoring rewrite rule ("^msg^")") sign prop; None)
    2.12 @@ -1714,7 +1714,7 @@
    2.13  type termrec = (Sign.sg_ref * term list) * term;
    2.14  type conv = meta_simpset -> termrec -> termrec;
    2.15  
    2.16 -fun check_conv (thm as Thm{shyps,hyps,prop,sign_ref,der,maxidx,...}, prop0, ders) =
    2.17 +fun check_conv (thm as Thm{shyps,hyps,prop,sign_ref,der,...}, prop0, ders) =
    2.18    let fun err() = (trace_thm false "Proved wrong thm (Check subgoaler?)" thm;
    2.19                     trace_term false "Should have proved" (Sign.deref sign_ref) prop0;
    2.20                     None)
    2.21 @@ -1724,7 +1724,7 @@
    2.22           if (lhs = lhs0) orelse
    2.23              (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
    2.24           then (trace_thm false "SUCCEEDED" thm; 
    2.25 -               Some(shyps, hyps, maxidx, rhs, der::ders))
    2.26 +               Some(shyps, hyps, rhs, der::ders))
    2.27           else err()
    2.28       | _ => err()
    2.29    end;
    2.30 @@ -1752,11 +1752,9 @@
    2.31        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
    2.32      val econcl = Pattern.eta_contract concl;
    2.33      val (elhs, erhs) = Logic.dest_equals econcl;
    2.34 -  in
    2.35 -    if not ((term_vars erhs) subset
    2.36 -        (union_term (term_vars elhs, List.concat(map term_vars prems)))) 
    2.37 -    then (prtm true "extra Var(s) on rhs" sign prop; [])
    2.38 -    else [{thm = thm, lhs = lhs, perm = false}]
    2.39 +  in case Logic.rewrite_rule_extra_vars prems elhs erhs of
    2.40 +       Some msg => (prtm true msg sign prop; [])
    2.41 +     | None => [{thm = thm, lhs = lhs, perm = false}]
    2.42    end;
    2.43  
    2.44  
    2.45 @@ -1768,14 +1766,18 @@
    2.46      (2) unconditional rewrite rules
    2.47      (3) conditional rewrite rules
    2.48      (4) simplification procedures
    2.49 +
    2.50 +  IMPORTANT: rewrite rules must not introduce new Vars or TVars!
    2.51 +
    2.52  *)
    2.53  
    2.54 -fun rewritec (prover,sign_reft) (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
    2.55 -             (shypst,hypst,maxt,t,ders) =
    2.56 +fun rewritec (prover,sign_reft,maxt)
    2.57 +             (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
    2.58 +             (shypst,hypst,t,ders) =
    2.59    let
    2.60        val signt = Sign.deref sign_reft;
    2.61        val tsigt = Sign.tsig_of signt;
    2.62 -      fun rew {thm as Thm{sign_ref,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
    2.63 +      fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...}, lhs, perm} =
    2.64          let
    2.65              val _ =
    2.66                if Sign.subsig (Sign.deref sign_ref, signt) then ()
    2.67 @@ -1789,7 +1791,8 @@
    2.68              val prop' = ren_inst(insts,rprop,rlhs,t);
    2.69              val hyps' = union_term(hyps,hypst);
    2.70              val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
    2.71 -            val maxidx' = maxidx_of_term prop'
    2.72 +            val unconditional = (Logic.count_prems(prop',0) = 0);
    2.73 +            val maxidx' = if unconditional then maxt else maxidx+maxt+1
    2.74              val ct' = Cterm{sign_ref = sign_reft,       (*used for deriv only*)
    2.75                              t = prop',
    2.76                              T = propT,
    2.77 @@ -1803,9 +1806,9 @@
    2.78                             maxidx = maxidx'}
    2.79              val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
    2.80          in if perm andalso not(termless(rhs',lhs')) then None else
    2.81 -           if Logic.count_prems(prop',0) = 0
    2.82 +           if unconditional
    2.83             then (trace_thm false "Rewriting:" thm'; 
    2.84 -                 Some(shyps', hyps', maxidx', rhs', der'::ders))
    2.85 +                 Some(shyps', hyps', rhs', der'::ders))
    2.86             else (trace_thm false "Trying to rewrite:" thm';
    2.87                   case prover mss thm' of
    2.88                     None       => (trace_thm false "FAILED" thm'; None)
    2.89 @@ -1843,7 +1846,7 @@
    2.90    in
    2.91      (case t of
    2.92        Abs (_, _, body) $ u =>
    2.93 -        Some (shypst, hypst, maxt, subst_bound (u, body), ders)
    2.94 +        Some (shypst, hypst, subst_bound (u, body), ders)
    2.95       | _ =>
    2.96        (case rews (sort_rrules (Net.match_term rules t)) of
    2.97          None => proc_rews (Pattern.eta_contract t) (Net.match_term procs t)
    2.98 @@ -1853,7 +1856,7 @@
    2.99  
   2.100  (* conversion to apply a congruence rule to a term *)
   2.101  
   2.102 -fun congc (prover,sign_reft) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) =
   2.103 +fun congc (prover,sign_reft,maxt) {thm=cong,lhs=lhs} (shypst,hypst,t,ders) =
   2.104    let val signt = Sign.deref sign_reft;
   2.105        val tsig = Sign.tsig_of signt;
   2.106        val Thm{sign_ref,der,shyps,hyps,maxidx,prop,...} = cong
   2.107 @@ -1888,17 +1891,15 @@
   2.108                          None => err() | some => some)
   2.109    end;
   2.110  
   2.111 -
   2.112 -
   2.113 -fun bottomc ((simprem,useprem),prover,sign_ref) =
   2.114 +fun bottomc ((simprem,useprem),prover,sign_ref,maxidx) =
   2.115   let fun botc fail mss trec =
   2.116            (case subc mss trec of
   2.117               some as Some(trec1) =>
   2.118 -               (case rewritec (prover,sign_ref) mss trec1 of
   2.119 +               (case rewritec (prover,sign_ref,maxidx) mss trec1 of
   2.120                    Some(trec2) => botc false mss trec2
   2.121                  | None => some)
   2.122             | None =>
   2.123 -               (case rewritec (prover,sign_ref) mss trec of
   2.124 +               (case rewritec (prover,sign_ref,maxidx) mss trec of
   2.125                    Some(trec2) => botc false mss trec2
   2.126                  | None => if fail then None else Some(trec)))
   2.127  
   2.128 @@ -1907,60 +1908,55 @@
   2.129                                | None => trec)
   2.130  
   2.131       and subc (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless})
   2.132 -              (trec as (shyps,hyps,maxidx,t0,ders)) =
   2.133 +              (trec as (shyps,hyps,t0,ders)) =
   2.134         (case t0 of
   2.135             Abs(a,T,t) =>
   2.136               let val b = variant bounds a
   2.137                   val v = Free("." ^ b,T)
   2.138                   val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
   2.139               in case botc true mss' 
   2.140 -                       (shyps,hyps,maxidx,subst_bound (v,t),ders) of
   2.141 -                  Some(shyps',hyps',maxidx',t',ders') =>
   2.142 -                    Some(shyps', hyps', maxidx',
   2.143 -                         Abs(a, T, abstract_over(v,t')),
   2.144 -                         ders')
   2.145 +                       (shyps,hyps,subst_bound (v,t),ders) of
   2.146 +                  Some(shyps',hyps',t',ders') =>
   2.147 +                    Some(shyps', hyps', Abs(a, T, abstract_over(v,t')), ders')
   2.148                  | None => None
   2.149               end
   2.150           | t$u => (case t of
   2.151 -             Const("==>",_)$s  => Some(impc(shyps,hyps,maxidx,s,u,mss,ders))
   2.152 +             Const("==>",_)$s  => Some(impc(shyps,hyps,s,u,mss,ders))
   2.153             | Abs(_,_,body) =>
   2.154 -               let val trec = (shyps,hyps,maxidx,subst_bound (u,body),ders)
   2.155 +               let val trec = (shyps,hyps,subst_bound (u,body),ders)
   2.156                 in case subc mss trec of
   2.157                      None => Some(trec)
   2.158                    | trec => trec
   2.159                 end
   2.160             | _  =>
   2.161                 let fun appc() =
   2.162 -                     (case botc true mss (shyps,hyps,maxidx,t,ders) of
   2.163 -                        Some(shyps1,hyps1,maxidx1,t1,ders1) =>
   2.164 -                          (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of
   2.165 -                             Some(shyps2,hyps2,maxidx2,u1,ders2) =>
   2.166 -                               Some(shyps2, hyps2, Int.max(maxidx1,maxidx2),
   2.167 -                                    t1$u1, ders2)
   2.168 -                           | None =>
   2.169 -                               Some(shyps1, hyps1, Int.max(maxidx1,maxidx), t1$u,
   2.170 -                                    ders1))
   2.171 +                     (case botc true mss (shyps,hyps,t,ders) of
   2.172 +                        Some(shyps1,hyps1,t1,ders1) =>
   2.173 +                          (case botc true mss (shyps1,hyps1,u,ders1) of
   2.174 +                             Some(shyps2,hyps2,u1,ders2) =>
   2.175 +                               Some(shyps2, hyps2, t1$u1, ders2)
   2.176 +                           | None => Some(shyps1, hyps1, t1$u, ders1))
   2.177                        | None =>
   2.178 -                          (case botc true mss (shyps,hyps,maxidx,u,ders) of
   2.179 -                             Some(shyps1,hyps1,maxidx1,u1,ders1) =>
   2.180 -                               Some(shyps1, hyps1, Int.max(maxidx,maxidx1), 
   2.181 -                                    t$u1, ders1)
   2.182 +                          (case botc true mss (shyps,hyps,u,ders) of
   2.183 +                             Some(shyps1,hyps1,u1,ders1) =>
   2.184 +                               Some(shyps1, hyps1, t$u1, ders1)
   2.185                             | None => None))
   2.186                     val (h,ts) = strip_comb t
   2.187                 in case h of
   2.188                      Const(a,_) =>
   2.189                        (case assoc_string(congs,a) of
   2.190                           None => appc()
   2.191 -                       | Some(cong) => (congc (prover mss,sign_ref) cong trec
   2.192 -                                        handle Pattern.MATCH => appc() ) )
   2.193 +                       | Some(cong) =>
   2.194 +                           (congc (prover mss,sign_ref,maxidx) cong trec
   2.195 +                            handle Pattern.MATCH => appc() ) )
   2.196                    | _ => appc()
   2.197                 end)
   2.198           | _ => None)
   2.199  
   2.200 -     and impc(shyps, hyps, maxidx, s, u, mss as Mss{mk_rews,...}, ders) =
   2.201 -       let val (shyps1,hyps1,_,s1,ders1) =
   2.202 -             if simprem then try_botc mss (shyps,hyps,maxidx,s,ders)
   2.203 -                        else (shyps,hyps,0,s,ders);
   2.204 +     and impc(shyps, hyps, s, u, mss as Mss{mk_rews,...}, ders) =
   2.205 +       let val (shyps1,hyps1,s1,ders1) =
   2.206 +             if simprem then try_botc mss (shyps,hyps,s,ders)
   2.207 +                        else (shyps,hyps,s,ders);
   2.208             val maxidx1 = maxidx_of_term s1
   2.209             val mss1 =
   2.210               if not useprem then mss else
   2.211 @@ -1968,14 +1964,12 @@
   2.212  "Cannot add premise as rewrite rule because it contains (type) unknowns:"
   2.213                                                    (Sign.deref sign_ref) s1; mss)
   2.214               else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1, 
   2.215 -                                              T=propT, maxidx=maxidx1})
   2.216 +                                              T=propT, maxidx= ~1})
   2.217                    in add_simps(add_prems(mss,[thm]), mk_rews thm) end
   2.218 -           val (shyps2,hyps2,maxidx2,u1,ders2) = 
   2.219 -               try_botc mss1 (shyps1,hyps1,maxidx,u,ders1)
   2.220 -           val hyps3 = if gen_mem (op aconv) (s1, hyps1) 
   2.221 +           val (shyps2,hyps2,u1,ders2) = try_botc mss1 (shyps1,hyps1,u,ders1)
   2.222 +           val hyps3 = if gen_mem (op aconv) (s1, hyps1)
   2.223                         then hyps2 else hyps2\s1
   2.224 -       in (shyps2, hyps3, Int.max(maxidx1,maxidx2), 
   2.225 -           Logic.mk_implies(s1,u1), ders2) 
   2.226 +       in (shyps2, hyps3, Logic.mk_implies(s1,u1), ders2) 
   2.227         end
   2.228  
   2.229   in try_botc end;
   2.230 @@ -1994,14 +1988,14 @@
   2.231  
   2.232  fun rewrite_cterm mode mss prover ct =
   2.233    let val Cterm {sign_ref, t, T, maxidx} = ct;
   2.234 -      val (shyps,hyps,maxu,u,ders) =
   2.235 -        bottomc (mode,prover, sign_ref) mss 
   2.236 -                (add_term_sorts(t,[]), [], maxidx, t, []);
   2.237 +      val (shyps,hyps,u,ders) =
   2.238 +        bottomc (mode,prover, sign_ref, maxidx) mss 
   2.239 +                (add_term_sorts(t,[]), [], t, []);
   2.240        val prop = Logic.mk_equals(t,u)
   2.241    in
   2.242        Thm{sign_ref = sign_ref, 
   2.243            der = infer_derivs (Rewrite_cterm ct, ders),
   2.244 -          maxidx = Int.max (maxidx,maxu),
   2.245 +          maxidx = maxidx,
   2.246            shyps = shyps, 
   2.247            hyps = hyps, 
   2.248            prop = prop}