src/FOLP/simp.ML
changeset 60645 2affe7e97a34
parent 60644 4af8b9c2b52f
child 60646 441e268564c7
     1.1 --- a/src/FOLP/simp.ML	Sun Jul 05 16:39:25 2015 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sun Jul 05 16:44:59 2015 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    val delcongs  : simpset * thm list -> simpset
     1.5    val delrews   : simpset * thm list -> simpset
     1.6    val dest_ss   : simpset -> thm list * thm list
     1.7 -  val print_ss  : simpset -> unit
     1.8 +  val print_ss  : Proof.context -> simpset -> unit
     1.9    val setauto   : simpset * (int -> tactic) -> simpset
    1.10    val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
    1.11    val ASM_SIMP_TAC      : simpset -> int -> tactic
    1.12 @@ -249,13 +249,11 @@
    1.13  (** Insertion of congruences and rewrites **)
    1.14  
    1.15  (*insert a thm in a thm net*)
    1.16 -fun insert_thm_warn th net =
    1.17 +fun insert_thm th net =
    1.18    Net.insert_term Thm.eq_thm_prop (Thm.concl_of th, th) net
    1.19 -  handle Net.INSERT =>
    1.20 -    (writeln ("Duplicate rewrite or congruence rule:\n" ^
    1.21 -        Display.string_of_thm_without_context th); net);
    1.22 +    handle Net.INSERT => net;
    1.23  
    1.24 -val insert_thms = fold_rev insert_thm_warn;
    1.25 +val insert_thms = fold_rev insert_thm;
    1.26  
    1.27  fun addrew ctxt thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
    1.28  let val thms = mk_simps ctxt thm
    1.29 @@ -273,13 +271,11 @@
    1.30  (** Deletion of congruences and rewrites **)
    1.31  
    1.32  (*delete a thm from a thm net*)
    1.33 -fun delete_thm_warn th net =
    1.34 +fun delete_thm th net =
    1.35    Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net
    1.36 -  handle Net.DELETE =>
    1.37 -    (writeln ("No such rewrite or congruence rule:\n" ^
    1.38 -        Display.string_of_thm_without_context th); net);
    1.39 +    handle Net.DELETE => net;
    1.40  
    1.41 -val delete_thms = fold_rev delete_thm_warn;
    1.42 +val delete_thms = fold_rev delete_thm;
    1.43  
    1.44  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.45  let val congs' = fold (remove Thm.eq_thm_prop) thms congs
    1.46 @@ -291,9 +287,7 @@
    1.47  fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
    1.48  let fun find((p as (th,ths))::ps',ps) =
    1.49            if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.50 -      | find([],simps') =
    1.51 -          (writeln ("No such rewrite or congruence rule:\n" ^
    1.52 -              Display.string_of_thm_without_context thm); ([], simps'))
    1.53 +      | find([],simps') = ([], simps')
    1.54      val (thms,simps') = find(simps,[])
    1.55  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    1.56        simps = simps', simp_net = delete_thms thms simp_net }
    1.57 @@ -311,10 +305,10 @@
    1.58  
    1.59  fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
    1.60  
    1.61 -fun print_ss(SS{congs,simps,...}) =
    1.62 +fun print_ss ctxt (SS{congs,simps,...}) =
    1.63    writeln (cat_lines
    1.64 -   (["Congruences:"] @ map Display.string_of_thm_without_context congs @
    1.65 -    ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps));
    1.66 +   (["Congruences:"] @ map (Display.string_of_thm ctxt) congs @
    1.67 +    ["Rewrite Rules:"] @ map (Display.string_of_thm ctxt o #1) simps));
    1.68  
    1.69  
    1.70  (* Rewriting with conditionals *)
    1.71 @@ -436,12 +430,7 @@
    1.72          val new_rws = maps mk_rew_rules thms;
    1.73          val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.74          val anet' = fold_rev lhs_insert_thm rwrls anet;
    1.75 -    in  if !tracing andalso not(null new_rws)
    1.76 -        then writeln (cat_lines
    1.77 -          ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
    1.78 -        else ();
    1.79 -        (ss,thm,anet',anet::ats,cs)
    1.80 -    end;
    1.81 +    in (ss,thm,anet',anet::ats,cs) end;
    1.82  
    1.83  fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
    1.84        SOME(thm',seq') =>