Merge remote-tracking branch 'origin/develop' into probability_dev

help/Docfiles/Tactic.drule_all.doc

@@ -54,6 +54,10 @@ list as they resolve against the theorem. The variant {drule_all_then}
 allows a continuation other than {MP_TAC} to be used. The variant
 {dxrule_all_then} combines both.
 
+A negated conclusion ({~Q}) is not treated as an implication ({Q ==> F})
+so the tactic will not attempt to find an instantiation of {Q} among the
+assumptions.
+
 \SEEALSO
 Tactic.drule, Tactic.IMP_RES_TAC.
 

src/1/Tactic.sml

@@ -1243,7 +1243,7 @@ fun dxrule_at_then p k     = dGEN first_x_assum     p       k
 fun rev_drule_at_then p k  = dGEN last_assum        p       k
 fun rev_dxrule_at_then p k = dGEN last_x_assum      p       k
 
-fun isfa_imp th = th |> concl |> strip_forall |> #2 |> is_imp
+fun isfa_imp th = th |> concl |> strip_forall |> #2 |> is_imp_only
 fun dall_prim k fa ith0 g =
   REPEAT_GTCL (fn ttcl => fn th => fa (mp_then (Pos hd) ttcl th))
               (k o assert (not o isfa_imp))

src/1/selftest.sml

@@ -1147,21 +1147,30 @@ val _ = let
   val asl = [“Q (a:ind) (b:'b):bool”,  “P (a:ind):bool”, “R T : bool”,
              “!x:ind. P x ==> !c:'b. Q x c ==> F”]
   val g = (asl, “p /\ q”)
-  val eres = Exn.capture (#1 o VALID (first_x_assum drule_all)) g
   val (asl', _) = front_last asl
   val expected = (asl', “F ==> p /\ q”)
 in
-  case eres of
-      Exn.Res res =>
-      if ListPair.allEq goal_equal ([expected], res) then OK()
-      else die ("Unexpected result:\n  " ^
-                PP.pp_to_string 70
-                                (fn r => PP.block PP.CONSISTENT 2 [pp_goals r])
-                                res
-               )
-    | Exn.Exn e => die ("Unexpected exception: " ^ General.exnMessage e)
+  require_pretty_msg
+    (check_result (fn r => ListPair.allEq goal_equal ([expected], r)))
+    pp_goals
+    (#1 o VALID (first_x_assum drule_all))
+    g
 end
 
+val _ = let
+  val _ = tprint "drule_all 3 (ith with negated concl.)"
+  val asl = [“Q(a:ind) (b:'b):bool”, “P (a:ind):bool”,
+             “!x:ind. P x ==> !c:'b. Q x c ==> !z:'b. ~R c z”]
+  val g = (asl, “p /\ q”)
+  val (asl', _) = front_last asl
+  val expected = (asl', “(!z:'b. ~R (b:'b) z) ==> p /\ q”)
+in
+  require_pretty_msg
+    (check_result (fn r => ListPair.allEq goal_equal ([expected], r)))
+    pp_goals
+    (#1 o VALID (first_x_assum drule_all))
+    g
+end
 
 val _ = let
   val _ = tprint "dxrule_all 1"