# HG changeset patch
# User wenzelm
# Date 1439732166 -7200
# Node ID 46ec72073dc12aacbf8ae7b0a2997e0822b371a1
# Parent  88aaecbaf61ebbf219f34567e3c5542a98d122ab
delete precisely the added rules;
tuned;

diff -r 88aaecbaf61e -r 46ec72073dc1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Aug 16 14:48:37 2015 +0200
+++ b/src/Provers/classical.ML	Sun Aug 16 15:36:06 2015 +0200
@@ -305,7 +305,7 @@
   warn_rules ctxt "Rule already declared as elimination (elim)\n" unsafeEs r;
 
 
-(*** Safe rules ***)
+(*** add rules ***)
 
 fun add_safe_intro w r
     (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
@@ -359,30 +359,6 @@
         extra_netpair = insert' (the_default 0 w) (nI, nE) ([], [th]) extra_netpair}
     end;
 
-fun addSI w ctxt th (cs as CS {safeIs, ...}) =
-  let
-    val th' = flat_rule ctxt th;
-    val r = (th, th', th');
-    val _ =
-      warn_rules ctxt "Ignoring duplicate safe introduction (intro!)\n" safeIs r orelse
-      warn_claset ctxt r cs;
-  in add_safe_intro w r cs end;
-
-fun addSE w ctxt th (cs as CS {safeEs, ...}) =
-  let
-    val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
-    val th' = classical_rule ctxt (flat_rule ctxt th);
-    val r = (th, th', th');
-    val _ =
-      warn_rules ctxt "Ignoring duplicate safe elimination (elim!)\n" safeEs r orelse
-      warn_claset ctxt r cs;
-  in add_safe_elim w r cs end;
-
-fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th);
-
-
-(*** Unsafe rules ***)
-
 fun add_unsafe_intro w r
     (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
@@ -431,6 +407,27 @@
         extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair}
     end;
 
+fun addSI w ctxt th (cs as CS {safeIs, ...}) =
+  let
+    val th' = flat_rule ctxt th;
+    val r = (th, th', th');
+    val _ =
+      warn_rules ctxt "Ignoring duplicate safe introduction (intro!)\n" safeIs r orelse
+      warn_claset ctxt r cs;
+  in add_safe_intro w r cs end;
+
+fun addSE w ctxt th (cs as CS {safeEs, ...}) =
+  let
+    val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
+    val th' = classical_rule ctxt (flat_rule ctxt th);
+    val r = (th, th', th');
+    val _ =
+      warn_rules ctxt "Ignoring duplicate safe elimination (elim!)\n" safeEs r orelse
+      warn_claset ctxt r cs;
+  in add_safe_elim w r cs end;
+
+fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th);
+
 fun addI w ctxt th (cs as CS {unsafeIs, ...}) =
   let
     val th' = flat_rule ctxt th;
@@ -455,108 +452,89 @@
 fun addD w ctxt th = addE w ctxt (make_elim ctxt th);
 
 
-(*** Deletion of rules
-     Working out what to delete, requires repeating much of the code used
-        to insert.
-***)
+(*** delete rules ***)
+
+local
 
-fun delSI ctxt th
-    (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
-      safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
-  if Item_Net.member safeIs (th, th, th) then
-    let
-      val th' = flat_rule ctxt th;
-      val r = (th, th', th');
-      val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
-    in
-      CS
-       {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
-        safep_netpair = delete (safep_rls, []) safep_netpair,
-        safeIs = Item_Net.remove r safeIs,
-        safeEs = safeEs,
-        unsafeIs = unsafeIs,
-        unsafeEs = unsafeEs,
-        swrappers = swrappers,
-        uwrappers = uwrappers,
-        unsafe_netpair = unsafe_netpair,
-        dup_netpair = dup_netpair,
-        extra_netpair = delete' ([th], []) extra_netpair}
-    end
-  else cs;
+fun del_safe_intro (r: rule)
+  (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
+    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
+  let
+    val (th, th', _) = r;
+    val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
+  in
+    CS
+     {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
+      safep_netpair = delete (safep_rls, []) safep_netpair,
+      safeIs = Item_Net.remove r safeIs,
+      safeEs = safeEs,
+      unsafeIs = unsafeIs,
+      unsafeEs = unsafeEs,
+      swrappers = swrappers,
+      uwrappers = uwrappers,
+      unsafe_netpair = unsafe_netpair,
+      dup_netpair = dup_netpair,
+      extra_netpair = delete' ([th], []) extra_netpair}
+  end;
 
-fun delSE ctxt th
-    (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
-      safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
-  if Item_Net.member safeEs (th, th, th) then
-    let
-      val th' = classical_rule ctxt (flat_rule ctxt th);
-      val r = (th, th', th');
-      val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th'];
-    in
-      CS
-       {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
-        safep_netpair = delete ([], safep_rls) safep_netpair,
-        safeIs = safeIs,
-        safeEs = Item_Net.remove r safeEs,
-        unsafeIs = unsafeIs,
-        unsafeEs = unsafeEs,
-        swrappers = swrappers,
-        uwrappers = uwrappers,
-        unsafe_netpair = unsafe_netpair,
-        dup_netpair = dup_netpair,
-        extra_netpair = delete' ([], [th]) extra_netpair}
-    end
-  else cs;
+fun del_safe_elim (r: rule)
+  (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
+    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
+  let
+    val (th, th', _) = r;
+    val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th'];
+  in
+    CS
+     {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
+      safep_netpair = delete ([], safep_rls) safep_netpair,
+      safeIs = safeIs,
+      safeEs = Item_Net.remove r safeEs,
+      unsafeIs = unsafeIs,
+      unsafeEs = unsafeEs,
+      swrappers = swrappers,
+      uwrappers = uwrappers,
+      unsafe_netpair = unsafe_netpair,
+      dup_netpair = dup_netpair,
+      extra_netpair = delete' ([], [th]) extra_netpair}
+  end;
 
-fun delI ctxt th
-    (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
-      safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
-  if Item_Net.member unsafeIs (th, th, th) then
-    let
-      val th' = flat_rule ctxt th;
-      val th'' = dup_intr th';
-      val r = (th, th', th'');
-    in
-      CS
-       {unsafe_netpair = delete ([th'], []) unsafe_netpair,
-        dup_netpair = delete ([th''], []) dup_netpair,
-        safeIs = safeIs,
-        safeEs = safeEs,
-        unsafeIs = Item_Net.remove r unsafeIs,
-        unsafeEs = unsafeEs,
-        swrappers = swrappers,
-        uwrappers = uwrappers,
-        safe0_netpair = safe0_netpair,
-        safep_netpair = safep_netpair,
-        extra_netpair = delete' ([th], []) extra_netpair}
-    end
-  else cs;
+fun del_unsafe_intro (r as (th, th', th''))
+  (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
+    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
+  CS
+   {unsafe_netpair = delete ([th'], []) unsafe_netpair,
+    dup_netpair = delete ([th''], []) dup_netpair,
+    safeIs = safeIs,
+    safeEs = safeEs,
+    unsafeIs = Item_Net.remove r unsafeIs,
+    unsafeEs = unsafeEs,
+    swrappers = swrappers,
+    uwrappers = uwrappers,
+    safe0_netpair = safe0_netpair,
+    safep_netpair = safep_netpair,
+    extra_netpair = delete' ([th], []) extra_netpair};
 
-fun delE ctxt th
-    (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
-      safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
-  if Item_Net.member unsafeEs (th, th, th) then
-    let
-      val th' = classical_rule ctxt (flat_rule ctxt th);
-      val th'' = dup_elim ctxt th';
-      val r = (th, th', th'');
-    in
-      CS
-       {unsafe_netpair = delete ([], [th']) unsafe_netpair,
-        dup_netpair = delete ([], [th'']) dup_netpair,
-        safeIs = safeIs,
-        safeEs = safeEs,
-        unsafeIs = unsafeIs,
-        unsafeEs = Item_Net.remove r unsafeEs,
-        swrappers = swrappers,
-        uwrappers = uwrappers,
-        safe0_netpair = safe0_netpair,
-        safep_netpair = safep_netpair,
-        extra_netpair = delete' ([], [th]) extra_netpair}
-    end
-  else cs;
+fun del_unsafe_elim (r as (th, th', th''))
+  (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers,
+    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
+  CS
+   {unsafe_netpair = delete ([], [th']) unsafe_netpair,
+    dup_netpair = delete ([], [th'']) dup_netpair,
+    safeIs = safeIs,
+    safeEs = safeEs,
+    unsafeIs = unsafeIs,
+    unsafeEs = Item_Net.remove r unsafeEs,
+    swrappers = swrappers,
+    uwrappers = uwrappers,
+    safe0_netpair = safe0_netpair,
+    safep_netpair = safep_netpair,
+    extra_netpair = delete' ([], [th]) extra_netpair};
 
-(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
+fun del f rules th cs =
+  fold f (Item_Net.lookup rules (th, th, th)) cs;
+
+in
+
 fun delrule ctxt th (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) =
   let
     val th' = Tactic.make_elim th;
@@ -568,15 +546,17 @@
       Item_Net.member safeEs r' orelse Item_Net.member unsafeEs r'
     then
       cs
-      |> delE ctxt th'
-      |> delSE ctxt th'
-      |> delE ctxt th
-      |> delI ctxt th
-      |> delSE ctxt th
-      |> delSI ctxt th
+      |> del del_safe_intro safeIs th
+      |> del del_safe_elim safeEs th
+      |> del del_safe_elim safeEs th'
+      |> del del_unsafe_intro unsafeIs th
+      |> del del_unsafe_elim unsafeEs th
+      |> del del_unsafe_elim unsafeEs th'
     else (warn_thm ctxt "Undeclared classical rule\n" th; cs)
   end;
 
+end;
+
 
 
 (** claset data **)
diff -r 88aaecbaf61e -r 46ec72073dc1 src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Sun Aug 16 14:48:37 2015 +0200
+++ b/src/Pure/item_net.ML	Sun Aug 16 15:36:06 2015 +0200
@@ -14,6 +14,7 @@
   val retrieve: 'a T -> term -> 'a list
   val retrieve_matching: 'a T -> term -> 'a list
   val member: 'a T -> 'a -> bool
+  val lookup: 'a T -> 'a -> 'a list
   val merge: 'a T * 'a T -> 'a T
   val remove: 'a -> 'a T -> 'a T
   val update: 'a -> 'a T -> 'a T
@@ -50,6 +51,12 @@
     [] => Library.member eq content x
   | t :: _ => exists (fn (_, y) => eq (x, y)) (Net.unify_term net t));
 
+fun lookup (Items {eq, index, content, net, ...}) x =
+  (case index x of
+    [] => content
+  | t :: _ => map #2 (Net.unify_term net t))
+  |> filter (fn y => eq (x, y));
+
 fun cons x (Items {eq, index, content, next, net}) =
   mk_items eq index (x :: content) (next - 1)
     (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);