src/Pure/thm.ML
changeset 1580 e3fd931e6095
parent 1576 af8f43f742a0
child 1597 54ece585bf62
equal deleted inserted replaced
1579:688e18023915 1580:e3fd931e6095
  1351 
  1351 
  1352 exception SIMPLIFIER of string * thm;
  1352 exception SIMPLIFIER of string * thm;
  1353 
  1353 
  1354 fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
  1354 fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
  1355 
  1355 
       
  1356 fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t));
       
  1357 
  1356 val trace_simp = ref false;
  1358 val trace_simp = ref false;
  1357 
  1359 
  1358 fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
  1360 fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
  1359 
  1361 
  1360 fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
  1362 fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
       
  1363 
       
  1364 fun trace_term_warning a sign t = if !trace_simp then prtm_warning a sign t else ();
       
  1365 
       
  1366 fun trace_thm_warning a (Thm{sign,prop,...}) = trace_term_warning a sign prop;
  1361 
  1367 
  1362 fun vperm(Var _, Var _) = true
  1368 fun vperm(Var _, Var _) = true
  1363   | vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t)
  1369   | vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t)
  1364   | vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2)
  1370   | vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2)
  1365   | vperm(t,u) = (t=u);
  1371   | vperm(t,u) = (t=u);
  1393       val (elhs,erhs) = Logic.dest_equals econcl
  1399       val (elhs,erhs) = Logic.dest_equals econcl
  1394       val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs)
  1400       val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs)
  1395                                      andalso not(is_Var(elhs))
  1401                                      andalso not(is_Var(elhs))
  1396   in
  1402   in
  1397      if not perm andalso loops sign prems (elhs,erhs) then
  1403      if not perm andalso loops sign prems (elhs,erhs) then
  1398        (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
  1404        (prtm_warning "ignoring looping rewrite rule" sign prop; None)
  1399      else Some{thm=thm,lhs=lhs,perm=perm}
  1405      else Some{thm=thm,lhs=lhs,perm=perm}
  1400   end;
  1406   end;
  1401 
  1407 
  1402 local
  1408 local
  1403  fun eq({thm=Thm{prop=p1,...},...}:rrule,
  1409  fun eq({thm=Thm{prop=p1,...},...}:rrule,
  1410     None => mss
  1416     None => mss
  1411   | Some(rrule as {lhs,...}) =>
  1417   | Some(rrule as {lhs,...}) =>
  1412       (trace_thm "Adding rewrite rule:" thm;
  1418       (trace_thm "Adding rewrite rule:" thm;
  1413        Mss{net = (Net.insert_term((lhs,rrule),net,eq)
  1419        Mss{net = (Net.insert_term((lhs,rrule),net,eq)
  1414                  handle Net.INSERT =>
  1420                  handle Net.INSERT =>
  1415                   (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
  1421                   (prtm_warning "ignoring duplicate rewrite rule" sign prop;
  1416                    net)),
  1422                    net)),
  1417            congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews});
  1423            congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews});
  1418 
  1424 
  1419 fun del_simp(mss as Mss{net,congs,bounds,prems,mk_rews},
  1425 fun del_simp(mss as Mss{net,congs,bounds,prems,mk_rews},
  1420              thm as Thm{sign,prop,...}) =
  1426              thm as Thm{sign,prop,...}) =
  1421   case mk_rrule thm of
  1427   case mk_rrule thm of
  1422     None => mss
  1428     None => mss
  1423   | Some(rrule as {lhs,...}) =>
  1429   | Some(rrule as {lhs,...}) =>
  1424       Mss{net = (Net.delete_term((lhs,rrule),net,eq)
  1430       Mss{net = (Net.delete_term((lhs,rrule),net,eq)
  1425                 handle Net.INSERT =>
  1431                 handle Net.INSERT =>
  1426                  (prtm "Warning: rewrite rule not in simpset" sign prop;
  1432                  (prtm_warning "rewrite rule not in simpset" sign prop;
  1427                   net)),
  1433                   net)),
  1428              congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}
  1434              congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}
  1429 
  1435 
  1430 end;
  1436 end;
  1431 
  1437 
  1541 fun rewritec (prover,signt) (mss as Mss{net,...}) 
  1547 fun rewritec (prover,signt) (mss as Mss{net,...}) 
  1542              (shypst,hypst,maxidxt,t,ders) =
  1548              (shypst,hypst,maxidxt,t,ders) =
  1543   let val etat = Pattern.eta_contract t;
  1549   let val etat = Pattern.eta_contract t;
  1544       fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
  1550       fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
  1545         let val unit = if Sign.subsig(sign,signt) then ()
  1551         let val unit = if Sign.subsig(sign,signt) then ()
  1546                   else (trace_thm"Warning: rewrite rule from different theory"
  1552                   else (trace_thm_warning "rewrite rule from different theory"
  1547                           thm;
  1553                           thm;
  1548                         raise Pattern.MATCH)
  1554                         raise Pattern.MATCH)
  1549             val rprop = if maxidxt = ~1 then prop
  1555             val rprop = if maxidxt = ~1 then prop
  1550                         else Logic.incr_indexes([],maxidxt+1) prop;
  1556                         else Logic.incr_indexes([],maxidxt+1) prop;
  1551             val rlhs = if maxidxt = ~1 then lhs
  1557             val rlhs = if maxidxt = ~1 then lhs