# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1465563290 -3600
# Node ID 9a2377b96ffd6a707451dd01ffb4b974a87c770e
# Parent  6b6f0eb9825b3f87920a8c455d4e415fad7ae11b
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.

diff -r 6b6f0eb9825b -r 9a2377b96ffd src/HOL/Multivariate_Analysis/Polytope.thy
--- a/src/HOL/Multivariate_Analysis/Polytope.thy	Thu Jun 09 16:42:10 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Polytope.thy	Fri Jun 10 13:54:50 2016 +0100
@@ -2163,32 +2163,7 @@
   fixes S :: "'a :: euclidean_space set"
   assumes "polyhedron S" "c face_of S"
     shows "polyhedron c"
-proof -
-  obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
-             and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
-             and min:   "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
-    using assms by (simp add: polyhedron_Int_affine_minimal) meson
-  then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
-    by metis
-  show ?thesis
-  proof (cases "c = {} \<or> c = S")
-    case True with assms show ?thesis
-      by auto
-  next
-    case False
-    let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
-    have "{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h} \<subseteq> {S \<inter> ?ab h |h. h \<in> F}"
-      by blast
-    then have fin: "finite ({S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h})"
-      by (rule finite_subset) (simp add: \<open>finite F\<close>)
-    then have "polyhedron (\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h})"
-      by (auto simp: \<open>polyhedron S\<close> polyhedron_hyperplane)
-    with False show ?thesis
-      using face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] assms
-      by auto
-  qed
-qed
-
+by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_closed polyhedron_imp_convex)
 
 lemma finite_polyhedron_faces:
   fixes S :: "'a :: euclidean_space set"
diff -r 6b6f0eb9825b -r 9a2377b96ffd src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Jun 09 16:42:10 2016 +0200
+++ b/src/Provers/blast.ML	Fri Jun 10 13:54:50 2016 +0100
@@ -29,7 +29,7 @@
         the formulae get into the wrong order (see WRONG below).
 
   With substition for equalities (hyp_subst_tac):
-        When substitution affects an unsage formula or literal, it is moved
+        When substitution affects an unsafe formula or literal, it is moved
         back to the list of safe formulae.
         But there's no way of putting it in the right place.  A "moved" or
         "no DETERM" flag would prevent proofs failing here.
@@ -82,7 +82,7 @@
 
 
 datatype term =
-    Const  of string * term list  (*typargs constant--as a terms!*)
+    Const  of string * term list  (*typargs constant--as a term!*)
   | Skolem of string * term option Unsynchronized.ref list
   | Free   of string
   | Var    of term option Unsynchronized.ref
@@ -110,15 +110,15 @@
   nclosed: int Unsynchronized.ref,
   ntried: int Unsynchronized.ref}
 
-fun reject_const thy c =
+fun reserved_const thy c =
   is_some (Sign.const_type thy c) andalso
-    error ("blast: theory contains illegal constant " ^ quote c);
+    error ("blast: theory contains reserved constant " ^ quote c);
 
 fun initialize ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val _ = reject_const thy "*Goal*";
-    val _ = reject_const thy "*False*";
+    val _ = reserved_const thy "*Goal*";
+    val _ = reserved_const thy "*False*";
   in
     State
      {ctxt = ctxt,
@@ -558,6 +558,10 @@
   | toTerm d (Abs(a,_))    = dummyVar
   | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
 
+(*Too flexible assertions or goals. Motivated by examples such as "(\<And>P. ~P) \<Longrightarrow> 0==1"*)
+fun isVarForm (Var _) = true
+  | isVarForm (Const (c, _) $ Var _) = (c = Data.not_name)
+  | isVarForm _ = false;
 
 fun netMkRules state P vars (nps: Classical.netpair list) =
   case P of
@@ -566,6 +570,8 @@
             val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
         in  map (fromIntrRule state vars o #2) (order_list intrs)  end
     | _ =>
+        if isVarForm P then [] (*The formula is too flexible, reject*)
+        else
         let val pP = mk_Trueprop (toTerm 3 P)
             val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
         in  map_filter (fromRule state vars o #2) (order_list elims)  end;