--- a/src/HOL/SMT/Z3.thy Wed Nov 11 14:15:11 2009 +0100
+++ b/src/HOL/SMT/Z3.thy Wed Nov 11 17:27:48 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 14:15:11 2009 +0100
+++ b/src/HOL/SMT/etc/settings Wed Nov 11 17:27:48 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 14:15:11 2009 +0100
+++ b/src/HOL/SupInf.thy Wed Nov 11 17:27:48 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
--- a/src/HOL/Tools/Function/function_lib.ML Wed Nov 11 14:15:11 2009 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Wed Nov 11 17:27:48 2009 +0100
@@ -30,8 +30,8 @@
| (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
| _ => raise Match
-
-
+
+
fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
let
val (n, body) = Term.dest_abs a
@@ -39,7 +39,7 @@
(Free (n, T), body)
end
| dest_all _ = raise Match
-
+
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
fun dest_all_all (t as (Const ("all",_) $ _)) =
@@ -50,7 +50,7 @@
(v :: vs, b')
end
| dest_all_all t = ([],t)
-
+
(* FIXME: similar to Variable.focus *)
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
@@ -161,9 +161,9 @@
Goal.prove_internal []
(cterm_of thy
(Logic.mk_equals (t,
- if is = []
+ if null is
then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
- else if js = []
+ else if null js
then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
(K (rewrite_goals_tac ac
--- a/src/HOL/Tools/record.ML Wed Nov 11 14:15:11 2009 +0100
+++ b/src/HOL/Tools/record.ML Wed Nov 11 17:27:48 2009 +0100
@@ -1754,11 +1754,12 @@
val ([inject', induct', surjective', split_meta'], thm_thy) =
defs_thy
- |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
+ |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name)
[("ext_inject", inject),
("ext_induct", induct),
("ext_surjective", surject),
- ("ext_split", split_meta)];
+ ("ext_split", split_meta)])
+ ||> Code.add_default_eqn ext_def;
in (thm_thy, extT, induct', inject', split_meta', ext_def) end;
--- a/src/HOL/ex/Records.thy Wed Nov 11 14:15:11 2009 +0100
+++ b/src/HOL/ex/Records.thy Wed Nov 11 17:27:48 2009 +0100
@@ -334,4 +334,8 @@
done
+subsection {* Some code generation *}
+
+export_code foo1 foo3 foo5 foo10 foo11 in SML file -
+
end