merged

--- a/src/HOL/SMT/Z3.thy	Wed Nov 11 15:10:29 2009 +0100
+++ b/src/HOL/SMT/Z3.thy	Wed Nov 11 16:19:28 2009 +0100
@@ -21,6 +21,8 @@
   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
   ring_distribs field_eq_simps if_True if_False
 
+lemma [z3_rewrite]: "(P \<noteq> Q) = (Q = (\<not>P))" by fast
+
 lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast
 lemma [z3_rewrite]: "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" by fast
 lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" by fast

--- a/src/HOL/SMT/etc/settings	Wed Nov 11 15:10:29 2009 +0100
+++ b/src/HOL/SMT/etc/settings	Wed Nov 11 16:19:28 2009 +0100
@@ -2,7 +2,7 @@
 
 REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl"
 
-REMOTE_SMT_URL="http://www4.in.tum.de/smt/smt"
+REMOTE_SMT_URL="http://smt.in.tum.de/smt"
 
 CERT_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/cert_smt.pl"
 

--- a/src/HOL/SupInf.thy	Wed Nov 11 15:10:29 2009 +0100
+++ b/src/HOL/SupInf.thy	Wed Nov 11 16:19:28 2009 +0100
@@ -88,6 +88,12 @@
   finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
 qed
 
+lemma less_SupE:
+  fixes y :: real
+  assumes "y < Sup X" "X \<noteq> {}"
+  obtains x where "x\<in>X" "y < x"
+by (metis SupInf.Sup_least assms linorder_not_less that)
+
 lemma Sup_singleton [simp]: "Sup {x::real} = x"
   by (force intro: Least_equality simp add: Sup_real_def)
  
@@ -459,4 +465,36 @@
   ultimately show ?thesis by arith
 qed
 
+lemma reals_complete_interval:
+  fixes a::real and b::real
+  assumes "a < b" and "P a" and "~P b"
+  shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) &
+             (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)"
+proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
+  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+    by (rule SupInf.Sup_upper [where z=b], auto)
+       (metis prems real_le_linear real_less_def) 
+next
+  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
+    apply (rule SupInf.Sup_least) 
+    apply (auto simp add: )
+    apply (metis less_le_not_le)
+    apply (metis `a<b` `~ P b` real_le_linear real_less_def) 
+    done
+next
+  fix x
+  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+  show "P x"
+    apply (rule less_SupE [OF lt], auto)
+    apply (metis less_le_not_le)
+    apply (metis x) 
+    done
+next
+  fix d
+    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
+    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+      by (rule_tac z="b" in SupInf.Sup_upper, auto) 
+         (metis `a<b` `~ P b` real_le_linear real_less_def) 
+qed
+
 end