# HG changeset patch
# User wenzelm
# Date 1440958655 -7200
# Node ID 6fc78876f9be7e701dfe4a5d6c4e1ca495d6e75b
# Parent  add998b3c5973588076310225ed1c5aae140e0f1
store result of swapify, to avoid later access to implicit context;

diff -r add998b3c597 -r 6fc78876f9be src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Aug 30 17:34:29 2015 +0200
+++ b/src/Provers/classical.ML	Sun Aug 30 20:17:35 2015 +0200
@@ -77,7 +77,6 @@
   val dup_step_tac: Proof.context -> int -> tactic
   val eq_mp_tac: Proof.context -> int -> tactic
   val unsafe_step_tac: Proof.context -> int -> tactic
-  val joinrules: thm list * thm list -> (bool * thm) list
   val mp_tac: Proof.context -> int -> tactic
   val safe_tac: Proof.context -> tactic
   val safe_steps_tac: Proof.context -> int -> tactic
@@ -97,7 +96,7 @@
 sig
   include BASIC_CLASSICAL
   val classical_rule: Proof.context -> thm -> thm
-  type rule = thm * thm * thm
+  type rule = thm * (thm * thm list) * (thm * thm list)
   type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
   val rep_cs: claset ->
    {safeIs: rule Item_Net.T,
@@ -210,7 +209,9 @@
 
 (**** Classical rule sets ****)
 
-type rule = thm * thm * thm;  (*external form vs. internal forms*)
+type rule = thm * (thm * thm list) * (thm * thm list);
+  (*external form, internal form (possibly swapped), dup form (possibly swapped)*)
+
 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
 type wrapper = (int -> tactic) -> int -> tactic;
 
@@ -255,13 +256,7 @@
     In case of overlap, new rules are tried BEFORE old ones!!
 ***)
 
-(*For use with biresolve_tac.  Combines intro rules with swap to handle negated
-  assumptions.  Pairs elim rules with true. *)
-fun joinrules (intrs, elims) =
-  (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs;
-
-fun joinrules' (intrs, elims) =
-  map (pair true) elims @ map (pair false) intrs;
+fun joinrules (intrs, elims) = map (pair true) elims @ map (pair false) intrs;
 
 (*Priority: prefer rules with fewest subgoals,
   then rules added most recently (preferring the head of the list).*)
@@ -279,11 +274,10 @@
   Count the intr rules double (to account for swapify).  Negate to give the
   new insertions the lowest priority.*)
 fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
-fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
+fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules;
 
 fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
 fun delete x = delete_tagged_list (joinrules x);
-fun delete' x = delete_tagged_list (joinrules' x);
 
 fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Display.string_of_thm ctxt th);
 
@@ -313,16 +307,16 @@
   if Item_Net.member safeIs r then cs
   else
     let
-      val (th, th', _) = r;
+      val (th, rl, _) = r;
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
-        List.partition Thm.no_prems [th'];
+        List.partition (Thm.no_prems o fst) [rl];
       val nI = Item_Net.length safeIs + 1;
       val nE = Item_Net.length safeEs;
     in
       CS
        {safeIs = Item_Net.update r safeIs,
-        safe0_netpair = insert (nI, nE) (safe0_rls, []) safe0_netpair,
-        safep_netpair = insert (nI, nE) (safep_rls, []) safep_netpair,
+        safe0_netpair = insert (nI, nE) (map fst safe0_rls, maps snd safe0_rls) safe0_netpair,
+        safep_netpair = insert (nI, nE) (map fst safep_rls, maps snd safep_rls) safep_netpair,
         safeEs = safeEs,
         unsafeIs = unsafeIs,
         unsafeEs = unsafeEs,
@@ -339,16 +333,16 @@
   if Item_Net.member safeEs r then cs
   else
     let
-      val (th, th', _) = r;
+      val (th, rl, _) = r;
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
-        List.partition (fn rl => Thm.nprems_of rl = 1) [th'];
+        List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl];
       val nI = Item_Net.length safeIs;
       val nE = Item_Net.length safeEs + 1;
     in
       CS
        {safeEs = Item_Net.update r safeEs,
-        safe0_netpair = insert (nI, nE) ([], safe0_rls) safe0_netpair,
-        safep_netpair = insert (nI, nE) ([], safep_rls) safep_netpair,
+        safe0_netpair = insert (nI, nE) ([], map fst safe0_rls) safe0_netpair,
+        safep_netpair = insert (nI, nE) ([], map fst safep_rls) safep_netpair,
         safeIs = safeIs,
         unsafeIs = unsafeIs,
         unsafeEs = unsafeEs,
@@ -365,14 +359,14 @@
   if Item_Net.member unsafeIs r then cs
   else
     let
-      val (th, th', th'') = r;
+      val (th, rl, dup_rl) = r;
       val nI = Item_Net.length unsafeIs + 1;
       val nE = Item_Net.length unsafeEs;
     in
       CS
        {unsafeIs = Item_Net.update r unsafeIs,
-        unsafe_netpair = insert (nI, nE) ([th'], []) unsafe_netpair,
-        dup_netpair = insert (nI, nE) ([th''], []) dup_netpair,
+        unsafe_netpair = insert (nI, nE) ([fst rl], snd rl) unsafe_netpair,
+        dup_netpair = insert (nI, nE) ([fst dup_rl], snd dup_rl) dup_netpair,
         safeIs = safeIs,
         safeEs = safeEs,
         unsafeEs = unsafeEs,
@@ -389,14 +383,14 @@
   if Item_Net.member unsafeEs r then cs
   else
     let
-      val (th, th', th'') = r;
+      val (th, rl, dup_rl) = r;
       val nI = Item_Net.length unsafeIs;
       val nE = Item_Net.length unsafeEs + 1;
     in
       CS
        {unsafeEs = Item_Net.update r unsafeEs,
-        unsafe_netpair = insert (nI, nE) ([], [th']) unsafe_netpair,
-        dup_netpair = insert (nI, nE) ([], [th'']) dup_netpair,
+        unsafe_netpair = insert (nI, nE) ([], [fst rl]) unsafe_netpair,
+        dup_netpair = insert (nI, nE) ([], [fst dup_rl]) dup_netpair,
         safeIs = safeIs,
         safeEs = safeEs,
         unsafeIs = unsafeIs,
@@ -410,7 +404,8 @@
 fun addSI w ctxt th (cs as CS {safeIs, ...}) =
   let
     val th' = flat_rule ctxt th;
-    val r = (th, th', th');
+    val rl = (th', swapify [th']);
+    val r = (th, rl, rl);
     val _ =
       warn_rules ctxt "Ignoring duplicate safe introduction (intro!)\n" safeIs r orelse
       warn_claset ctxt r cs;
@@ -420,7 +415,8 @@
   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 rl = (th', []);
+    val r = (th, rl, rl);
     val _ =
       warn_rules ctxt "Ignoring duplicate safe elimination (elim!)\n" safeEs r orelse
       warn_claset ctxt r cs;
@@ -431,8 +427,8 @@
 fun addI w ctxt th (cs as CS {unsafeIs, ...}) =
   let
     val th' = flat_rule ctxt th;
-    val th'' = dup_intr th' handle THM _ => bad_thm ctxt "Ill-formed introduction rule" th;
-    val r = (th, th', th'');
+    val dup_th' = dup_intr th' handle THM _ => bad_thm ctxt "Ill-formed introduction rule" th;
+    val r = (th, (th', swapify [th']), (dup_th', swapify [dup_th']));
     val _ =
       warn_rules ctxt "Ignoring duplicate introduction (intro)\n" unsafeIs r orelse
       warn_claset ctxt r cs;
@@ -442,8 +438,8 @@
   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 th'' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th;
-    val r = (th, th', th'');
+    val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th;
+    val r = (th, (th', []), (dup_th', []));
     val _ =
       warn_rules ctxt "Ignoring duplicate elimination (elim)\n" unsafeEs r orelse
       warn_claset ctxt r cs;
@@ -460,12 +456,12 @@
   (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'];
+    val (th, rl, _) = r;
+    val (safe0_rls, safep_rls) = List.partition (Thm.no_prems o fst) [rl];
   in
     CS
-     {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
-      safep_netpair = delete (safep_rls, []) safep_netpair,
+     {safe0_netpair = delete (map fst safe0_rls, maps snd safe0_rls) safe0_netpair,
+      safep_netpair = delete (map fst safep_rls, maps snd safep_rls) safep_netpair,
       safeIs = Item_Net.remove r safeIs,
       safeEs = safeEs,
       unsafeIs = unsafeIs,
@@ -474,19 +470,19 @@
       uwrappers = uwrappers,
       unsafe_netpair = unsafe_netpair,
       dup_netpair = dup_netpair,
-      extra_netpair = delete' ([th], []) extra_netpair}
+      extra_netpair = delete ([th], []) extra_netpair}
   end;
 
 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'];
+    val (th, rl, _) = r;
+    val (safe0_rls, safep_rls) = List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl];
   in
     CS
-     {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
-      safep_netpair = delete ([], safep_rls) safep_netpair,
+     {safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair,
+      safep_netpair = delete ([], map fst safep_rls) safep_netpair,
       safeIs = safeIs,
       safeEs = Item_Net.remove r safeEs,
       unsafeIs = unsafeIs,
@@ -495,15 +491,15 @@
       uwrappers = uwrappers,
       unsafe_netpair = unsafe_netpair,
       dup_netpair = dup_netpair,
-      extra_netpair = delete' ([], [th]) extra_netpair}
+      extra_netpair = delete ([], [th]) extra_netpair}
   end;
 
-fun del_unsafe_intro (r as (th, th', th''))
+fun del_unsafe_intro (r as (th, (th', swapped_th'), (dup_th', swapped_dup_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,
+   {unsafe_netpair = delete ([th'], swapped_th') unsafe_netpair,
+    dup_netpair = delete ([dup_th'], swapped_dup_th') dup_netpair,
     safeIs = safeIs,
     safeEs = safeEs,
     unsafeIs = Item_Net.remove r unsafeIs,
@@ -512,14 +508,14 @@
     uwrappers = uwrappers,
     safe0_netpair = safe0_netpair,
     safep_netpair = safep_netpair,
-    extra_netpair = delete' ([th], []) extra_netpair};
+    extra_netpair = delete ([th], []) extra_netpair};
 
-fun del_unsafe_elim (r as (th, th', th''))
+fun del_unsafe_elim (r as (th, (th', _), (dup_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,
+    dup_netpair = delete ([], [dup_th']) dup_netpair,
     safeIs = safeIs,
     safeEs = safeEs,
     unsafeIs = unsafeIs,
@@ -528,18 +524,18 @@
     uwrappers = uwrappers,
     safe0_netpair = safe0_netpair,
     safep_netpair = safep_netpair,
-    extra_netpair = delete' ([], [th]) extra_netpair};
+    extra_netpair = delete ([], [th]) extra_netpair};
 
 fun del f rules th cs =
-  fold f (Item_Net.lookup rules (th, th, 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;
-    val r = (th, th, th);
-    val r' = (th', th', th');
+    val r = (th, (th, []), (th, []));
+    val r' = (th', (th', []), (th', []));
   in
     if Item_Net.member safeIs r orelse Item_Net.member safeEs r orelse
       Item_Net.member unsafeIs r orelse Item_Net.member unsafeEs r orelse