--- a/doc-src/Nitpick/nitpick.tex Thu Mar 11 09:09:43 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Mar 11 09:09:51 2010 +0100
@@ -4,6 +4,7 @@
\usepackage{amssymb}
\usepackage[english,french]{babel}
\usepackage{color}
+\usepackage{footmisc}
\usepackage{graphicx}
%\usepackage{mathpazo}
\usepackage{multicol}
@@ -1019,7 +1020,7 @@
can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
bisimilarity check is then performed \textsl{after} the counterexample has been
found to ensure correctness. If this after-the-fact check fails, the
-counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
+counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
check for the previous example saves approximately 150~milli\-seconds; the speed
gains can be more significant for larger scopes.
@@ -1031,7 +1032,7 @@
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
-\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
+\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $a = a_1$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
@@ -1901,7 +1902,7 @@
\textbf{Warning:} If the option is set to \textit{true}, Nitpick might
nonetheless ignore some polymorphic axioms. Counterexamples generated under
-these conditions are tagged as ``likely genuine.'' The \textit{debug}
+these conditions are tagged as ``quasi genuine.'' The \textit{debug}
(\S\ref{output-format}) option can be used to find out which axioms were
considered.
@@ -2002,7 +2003,7 @@
\begin{enum}
\item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
predicate as if it were well-founded. Since this is generally not sound when the
-predicate is not well-founded, the counterexamples are tagged as ``likely
+predicate is not well-founded, the counterexamples are tagged as ``quasi
genuine.''
\item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
@@ -2050,7 +2051,7 @@
of $-1$ means that no predicate is generated, in which case Nitpick performs an
after-the-fact check to see if the known coinductive datatype values are
bidissimilar. If two values are found to be bisimilar, the counterexample is
-tagged as ``likely genuine.'' The iteration counts are automatically bounded by
+tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
the sum of the cardinalities of the coinductive datatypes occurring in the
formula to falsify.
@@ -2100,7 +2101,7 @@
\begin{enum}
\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
-unsound, counterexamples generated under these conditions are tagged as ``likely
+unsound, counterexamples generated under these conditions are tagged as ``quasi
genuine.''
\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
@@ -2268,7 +2269,7 @@
{\small See also \textit{max\_potential} (\S\ref{output-format}).}
\opfalse{check\_genuine}{trust\_genuine}
-Specifies whether genuine and likely genuine counterexamples should be given to
+Specifies whether genuine and quasi genuine counterexamples should be given to
Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
counterexample is shown to be spurious, the user is kindly asked to send a bug
report to the author at
@@ -2282,7 +2283,7 @@
\begin{enum}
\item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
-\item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely
+\item[$\bullet$] \textbf{\textit{quasi\_genuine}}: Nitpick found a ``quasi
genuine'' counterexample (i.e., a counterexample that is genuine unless
it contradicts a missing axiom or a dangerous option was used inappropriately).
\item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
@@ -2313,12 +2314,18 @@
The supported solvers are listed below:
+\let\foo
+
\begin{enum}
\item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
written in \cpp{}. To use MiniSat, set the environment variable
\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
-executable. The \cpp{} sources and executables for MiniSat are available at
+executable.%
+\footnote{Important note for Cygwin users: The path must be specified using
+native Windows syntax. Make sure to escape backslashes properly.%
+\label{cygwin-paths}}
+The \cpp{} sources and executables for MiniSat are available at
\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
and 2.0 beta (2007-07-21).
@@ -2333,14 +2340,17 @@
\item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
written in C. You can install a standard version of
PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
-that contains the \texttt{picosat} executable. The C sources for PicoSAT are
+that contains the \texttt{picosat} executable.%
+\footref{cygwin-paths}
+The C sources for PicoSAT are
available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
Nitpick has been tested with version 913.
\item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
-the directory that contains the \texttt{zchaff} executable. The \cpp{} sources
-and executables for zChaff are available at
+the directory that contains the \texttt{zchaff} executable.%
+\footref{cygwin-paths}
+The \cpp{} sources and executables for zChaff are available at
\url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
versions 2004-05-13, 2004-11-15, and 2007-03-12.
@@ -2350,26 +2360,32 @@
\item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
\cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
-directory that contains the \texttt{rsat} executable. The \cpp{} sources for
-RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been
-tested with version 2.01.
+directory that contains the \texttt{rsat} executable.%
+\footref{cygwin-paths}
+The \cpp{} sources for RSat are available at
+\url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
+2.01.
\item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
written in C. To use BerkMin, set the environment variable
\texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
-executable. The BerkMin executables are available at
+executable.\footref{cygwin-paths}
+The BerkMin executables are available at
\url{http://eigold.tripod.com/BerkMin.html}.
\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
version of BerkMin, set the environment variable
\texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
-executable.
+executable.%
+\footref{cygwin-paths}
\item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
written in C. To use Jerusat, set the environment variable
\texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
-executable. The C sources for Jerusat are available at
+executable.%
+\footref{cygwin-paths}
+The C sources for Jerusat are available at
\url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
\item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
@@ -2384,7 +2400,9 @@
\item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
experimental solver written in \cpp. To use HaifaSat, set the environment
variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
-\texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at
+\texttt{HaifaSat} executable.%
+\footref{cygwin-paths}
+The \cpp{} sources for HaifaSat are available at
\url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
@@ -2668,7 +2686,7 @@
\postw
The return value is a new proof state paired with an outcome string
-(``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
+(``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
\textit{params} type is a large record that lets you set Nitpick's options. The
current default options can be retrieved by calling the following function
defined in the \textit{Nitpick\_Isar} structure:
--- a/src/HOL/Auth/TLS.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Auth/TLS.thy Thu Mar 11 09:09:51 2010 +0100
@@ -41,7 +41,7 @@
header{*The TLS Protocol: Transport Layer Security*}
-theory TLS imports Public Nat_Int_Bij begin
+theory TLS imports Public Nat_Bijection begin
definition certificate :: "[agent,key] => msg" where
"certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
@@ -74,19 +74,17 @@
specification (PRF)
inj_PRF: "inj PRF"
--{*the pseudo-random function is collision-free*}
- apply (rule exI [of _ "%(x,y,z). nat2_to_nat(x, nat2_to_nat(y,z))"])
- apply (simp add: inj_on_def)
- apply (blast dest!: nat2_to_nat_inj [THEN injD])
+ apply (rule exI [of _ "%(x,y,z). prod_encode(x, prod_encode(y,z))"])
+ apply (simp add: inj_on_def prod_encode_eq)
done
specification (sessionK)
inj_sessionK: "inj sessionK"
--{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
apply (rule exI [of _
- "%((x,y,z), r). nat2_to_nat(role_case 0 1 r,
- nat2_to_nat(x, nat2_to_nat(y,z)))"])
- apply (simp add: inj_on_def split: role.split)
- apply (blast dest!: nat2_to_nat_inj [THEN injD])
+ "%((x,y,z), r). prod_encode(role_case 0 1 r,
+ prod_encode(x, prod_encode(y,z)))"])
+ apply (simp add: inj_on_def prod_encode_eq split: role.split)
done
axioms
--- a/src/HOL/IsaMakefile Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 11 09:09:51 2010 +0100
@@ -393,7 +393,7 @@
Library/Inner_Product.thy Library/Kleene_Algebra.thy \
Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
- Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy \
+ Library/State_Monad.thy Library/Multiset.thy \
Library/Permutation.thy Library/Quotient_Type.thy \
Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \
Library/README.html Library/Continuity.thy \
@@ -415,6 +415,7 @@
Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \
Library/Quotient_Option.thy Library/Quotient_Product.thy \
Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
+ Library/Nat_Bijection.thy \
$(SRC)/Tools/float.ML \
$(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
--- a/src/HOL/Library/Countable.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Library/Countable.thy Thu Mar 11 09:09:51 2010 +0100
@@ -5,7 +5,7 @@
header {* Encoding (almost) everything into natural numbers *}
theory Countable
-imports Main Rat Nat_Int_Bij
+imports Main Rat Nat_Bijection
begin
subsection {* The class of countable types *}
@@ -48,7 +48,7 @@
subsection {* Countable types *}
instance nat :: countable
- by (rule countable_classI [of "id"]) simp
+ by (rule countable_classI [of "id"]) simp
subclass (in finite) countable
proof
@@ -63,47 +63,9 @@
text {* Pairs *}
-primrec sum :: "nat \<Rightarrow> nat"
-where
- "sum 0 = 0"
-| "sum (Suc n) = Suc n + sum n"
-
-lemma sum_arith: "sum n = n * Suc n div 2"
- by (induct n) auto
-
-lemma sum_mono: "n \<ge> m \<Longrightarrow> sum n \<ge> sum m"
- by (induct n m rule: diff_induct) auto
-
-definition
- "pair_encode = (\<lambda>(m, n). sum (m + n) + m)"
-
-lemma inj_pair_cencode: "inj pair_encode"
- unfolding pair_encode_def
-proof (rule injI, simp only: split_paired_all split_conv)
- fix a b c d
- assume eq: "sum (a + b) + a = sum (c + d) + c"
- have "a + b = c + d \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
- then
- show "(a, b) = (c, d)"
- proof (elim disjE)
- assume sumeq: "a + b = c + d"
- then have "a = c" using eq by auto
- moreover from sumeq this have "b = d" by auto
- ultimately show ?thesis by simp
- next
- assume "a + b \<ge> Suc (c + d)"
- from sum_mono[OF this] eq
- show ?thesis by auto
- next
- assume "c + d \<ge> Suc (a + b)"
- from sum_mono[OF this] eq
- show ?thesis by auto
- qed
-qed
-
instance "*" :: (countable, countable) countable
-by (rule countable_classI [of "\<lambda>(x, y). pair_encode (to_nat x, to_nat y)"])
- (auto dest: injD [OF inj_pair_cencode] injD [OF inj_to_nat])
+ by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
+ (auto simp add: prod_encode_eq)
text {* Sums *}
@@ -111,76 +73,28 @@
instance "+":: (countable, countable) countable
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
- (auto split:sum.splits)
+ (simp split: sum.split_asm)
text {* Integers *}
-lemma int_cases: "(i::int) = 0 \<or> i < 0 \<or> i > 0"
-by presburger
-
-lemma int_pos_neg_zero:
- obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0"
- | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n"
- | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n"
-apply atomize_elim
-apply (insert int_cases[of z])
-apply (auto simp:zsgn_def)
-apply (rule_tac x="nat (-z)" in exI, simp)
-apply (rule_tac x="nat z" in exI, simp)
-done
-
instance int :: countable
-proof (rule countable_classI [of "(\<lambda>i. to_nat (nat (sgn i + 1), nat (abs i)))"],
- auto dest: injD [OF inj_to_nat])
- fix x y
- assume a: "nat (sgn x + 1) = nat (sgn y + 1)" "nat (abs x) = nat (abs y)"
- show "x = y"
- proof (cases rule: int_pos_neg_zero[of x])
- case zero
- with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
- next
- case (pos n)
- with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
- next
- case (neg n)
- with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
- qed
-qed
+ by (rule countable_classI [of "int_encode"])
+ (simp add: int_encode_eq)
text {* Options *}
instance option :: (countable) countable
-by (rule countable_classI[of "\<lambda>x. case x of None \<Rightarrow> 0
- | Some y \<Rightarrow> Suc (to_nat y)"])
- (auto split:option.splits)
+ by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"])
+ (simp split: option.split_asm)
text {* Lists *}
-lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
- by (simp add: comp_def)
-
-primrec
- list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
-where
- "list_encode [] = 0"
-| "list_encode (x#xs) = Suc (to_nat (x, list_encode xs))"
-
instance list :: (countable) countable
-proof (rule countable_classI [of "list_encode"])
- fix xs ys :: "'a list"
- assume cenc: "list_encode xs = list_encode ys"
- then show "xs = ys"
- proof (induct xs arbitrary: ys)
- case (Nil ys)
- with cenc show ?case by (cases ys, auto)
- next
- case (Cons x xs' ys)
- thus ?case by (cases ys) auto
- qed
-qed
+ by (rule countable_classI [of "list_encode \<circ> map to_nat"])
+ (simp add: list_encode_eq)
text {* Functions *}
@@ -200,8 +114,8 @@
subsection {* The Rationals are Countably Infinite *}
definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
-"nat_to_rat_surj n = (let (a,b) = nat_to_nat2 n
- in Fract (nat_to_int_bij a) (nat_to_int_bij b))"
+"nat_to_rat_surj n = (let (a,b) = prod_decode n
+ in Fract (int_decode a) (int_decode b))"
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
unfolding surj_def
@@ -210,10 +124,9 @@
show "\<exists>n. r = nat_to_rat_surj n"
proof (cases r)
fix i j assume [simp]: "r = Fract i j" and "j > 0"
- have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
- in nat_to_rat_surj(nat2_to_nat (m,n)))"
- using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]
- by(simp add:Let_def nat_to_rat_surj_def nat_to_nat2_def)
+ have "r = (let m = int_encode i; n = int_encode j
+ in nat_to_rat_surj(prod_encode (m,n)))"
+ by (simp add: Let_def nat_to_rat_surj_def)
thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
qed
qed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Nat_Bijection.thy Thu Mar 11 09:09:51 2010 +0100
@@ -0,0 +1,370 @@
+(* Title: HOL/Nat_Bijection.thy
+ Author: Brian Huffman
+ Author: Florian Haftmann
+ Author: Stefan Richter
+ Author: Tobias Nipkow
+ Author: Alexander Krauss
+*)
+
+header {* Bijections between natural numbers and other types *}
+
+theory Nat_Bijection
+imports Main Parity
+begin
+
+subsection {* Type @{typ "nat \<times> nat"} *}
+
+text "Triangle numbers: 0, 1, 3, 6, 10, 15, ..."
+
+definition
+ triangle :: "nat \<Rightarrow> nat"
+where
+ "triangle n = n * Suc n div 2"
+
+lemma triangle_0 [simp]: "triangle 0 = 0"
+unfolding triangle_def by simp
+
+lemma triangle_Suc [simp]: "triangle (Suc n) = triangle n + Suc n"
+unfolding triangle_def by simp
+
+definition
+ prod_encode :: "nat \<times> nat \<Rightarrow> nat"
+where
+ "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)"
+
+text {* In this auxiliary function, @{term "triangle k + m"} is an invariant. *}
+
+fun
+ prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
+where
+ "prod_decode_aux k m =
+ (if m \<le> k then (m, k - m) else prod_decode_aux (Suc k) (m - Suc k))"
+
+declare prod_decode_aux.simps [simp del]
+
+definition
+ prod_decode :: "nat \<Rightarrow> nat \<times> nat"
+where
+ "prod_decode = prod_decode_aux 0"
+
+lemma prod_encode_prod_decode_aux:
+ "prod_encode (prod_decode_aux k m) = triangle k + m"
+apply (induct k m rule: prod_decode_aux.induct)
+apply (subst prod_decode_aux.simps)
+apply (simp add: prod_encode_def)
+done
+
+lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n"
+unfolding prod_decode_def by (simp add: prod_encode_prod_decode_aux)
+
+lemma prod_decode_triangle_add:
+ "prod_decode (triangle k + m) = prod_decode_aux k m"
+apply (induct k arbitrary: m)
+apply (simp add: prod_decode_def)
+apply (simp only: triangle_Suc add_assoc)
+apply (subst prod_decode_aux.simps, simp)
+done
+
+lemma prod_encode_inverse [simp]: "prod_decode (prod_encode x) = x"
+unfolding prod_encode_def
+apply (induct x)
+apply (simp add: prod_decode_triangle_add)
+apply (subst prod_decode_aux.simps, simp)
+done
+
+lemma inj_prod_encode: "inj_on prod_encode A"
+by (rule inj_on_inverseI, rule prod_encode_inverse)
+
+lemma inj_prod_decode: "inj_on prod_decode A"
+by (rule inj_on_inverseI, rule prod_decode_inverse)
+
+lemma surj_prod_encode: "surj prod_encode"
+by (rule surjI, rule prod_decode_inverse)
+
+lemma surj_prod_decode: "surj prod_decode"
+by (rule surjI, rule prod_encode_inverse)
+
+lemma bij_prod_encode: "bij prod_encode"
+by (rule bijI [OF inj_prod_encode surj_prod_encode])
+
+lemma bij_prod_decode: "bij prod_decode"
+by (rule bijI [OF inj_prod_decode surj_prod_decode])
+
+lemma prod_encode_eq: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
+by (rule inj_prod_encode [THEN inj_eq])
+
+lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
+by (rule inj_prod_decode [THEN inj_eq])
+
+text {* Ordering properties *}
+
+lemma le_prod_encode_1: "a \<le> prod_encode (a, b)"
+unfolding prod_encode_def by simp
+
+lemma le_prod_encode_2: "b \<le> prod_encode (a, b)"
+unfolding prod_encode_def by (induct b, simp_all)
+
+
+subsection {* Type @{typ "nat + nat"} *}
+
+definition
+ sum_encode :: "nat + nat \<Rightarrow> nat"
+where
+ "sum_encode x = (case x of Inl a \<Rightarrow> 2 * a | Inr b \<Rightarrow> Suc (2 * b))"
+
+definition
+ sum_decode :: "nat \<Rightarrow> nat + nat"
+where
+ "sum_decode n = (if even n then Inl (n div 2) else Inr (n div 2))"
+
+lemma sum_encode_inverse [simp]: "sum_decode (sum_encode x) = x"
+unfolding sum_decode_def sum_encode_def
+by (induct x) simp_all
+
+lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
+unfolding sum_decode_def sum_encode_def numeral_2_eq_2
+by (simp add: even_nat_div_two_times_two odd_nat_div_two_times_two_plus_one
+ del: mult_Suc)
+
+lemma inj_sum_encode: "inj_on sum_encode A"
+by (rule inj_on_inverseI, rule sum_encode_inverse)
+
+lemma inj_sum_decode: "inj_on sum_decode A"
+by (rule inj_on_inverseI, rule sum_decode_inverse)
+
+lemma surj_sum_encode: "surj sum_encode"
+by (rule surjI, rule sum_decode_inverse)
+
+lemma surj_sum_decode: "surj sum_decode"
+by (rule surjI, rule sum_encode_inverse)
+
+lemma bij_sum_encode: "bij sum_encode"
+by (rule bijI [OF inj_sum_encode surj_sum_encode])
+
+lemma bij_sum_decode: "bij sum_decode"
+by (rule bijI [OF inj_sum_decode surj_sum_decode])
+
+lemma sum_encode_eq: "sum_encode x = sum_encode y \<longleftrightarrow> x = y"
+by (rule inj_sum_encode [THEN inj_eq])
+
+lemma sum_decode_eq: "sum_decode x = sum_decode y \<longleftrightarrow> x = y"
+by (rule inj_sum_decode [THEN inj_eq])
+
+
+subsection {* Type @{typ "int"} *}
+
+definition
+ int_encode :: "int \<Rightarrow> nat"
+where
+ "int_encode i = sum_encode (if 0 \<le> i then Inl (nat i) else Inr (nat (- i - 1)))"
+
+definition
+ int_decode :: "nat \<Rightarrow> int"
+where
+ "int_decode n = (case sum_decode n of Inl a \<Rightarrow> int a | Inr b \<Rightarrow> - int b - 1)"
+
+lemma int_encode_inverse [simp]: "int_decode (int_encode x) = x"
+unfolding int_decode_def int_encode_def by simp
+
+lemma int_decode_inverse [simp]: "int_encode (int_decode n) = n"
+unfolding int_decode_def int_encode_def using sum_decode_inverse [of n]
+by (cases "sum_decode n", simp_all)
+
+lemma inj_int_encode: "inj_on int_encode A"
+by (rule inj_on_inverseI, rule int_encode_inverse)
+
+lemma inj_int_decode: "inj_on int_decode A"
+by (rule inj_on_inverseI, rule int_decode_inverse)
+
+lemma surj_int_encode: "surj int_encode"
+by (rule surjI, rule int_decode_inverse)
+
+lemma surj_int_decode: "surj int_decode"
+by (rule surjI, rule int_encode_inverse)
+
+lemma bij_int_encode: "bij int_encode"
+by (rule bijI [OF inj_int_encode surj_int_encode])
+
+lemma bij_int_decode: "bij int_decode"
+by (rule bijI [OF inj_int_decode surj_int_decode])
+
+lemma int_encode_eq: "int_encode x = int_encode y \<longleftrightarrow> x = y"
+by (rule inj_int_encode [THEN inj_eq])
+
+lemma int_decode_eq: "int_decode x = int_decode y \<longleftrightarrow> x = y"
+by (rule inj_int_decode [THEN inj_eq])
+
+
+subsection {* Type @{typ "nat list"} *}
+
+fun
+ list_encode :: "nat list \<Rightarrow> nat"
+where
+ "list_encode [] = 0"
+| "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))"
+
+function
+ list_decode :: "nat \<Rightarrow> nat list"
+where
+ "list_decode 0 = []"
+| "list_decode (Suc n) = (case prod_decode n of (x, y) \<Rightarrow> x # list_decode y)"
+by pat_completeness auto
+
+termination list_decode
+apply (relation "measure id", simp_all)
+apply (drule arg_cong [where f="prod_encode"])
+apply (simp add: le_imp_less_Suc le_prod_encode_2)
+done
+
+lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x"
+by (induct x rule: list_encode.induct) simp_all
+
+lemma list_decode_inverse [simp]: "list_encode (list_decode n) = n"
+apply (induct n rule: list_decode.induct, simp)
+apply (simp split: prod.split)
+apply (simp add: prod_decode_eq [symmetric])
+done
+
+lemma inj_list_encode: "inj_on list_encode A"
+by (rule inj_on_inverseI, rule list_encode_inverse)
+
+lemma inj_list_decode: "inj_on list_decode A"
+by (rule inj_on_inverseI, rule list_decode_inverse)
+
+lemma surj_list_encode: "surj list_encode"
+by (rule surjI, rule list_decode_inverse)
+
+lemma surj_list_decode: "surj list_decode"
+by (rule surjI, rule list_encode_inverse)
+
+lemma bij_list_encode: "bij list_encode"
+by (rule bijI [OF inj_list_encode surj_list_encode])
+
+lemma bij_list_decode: "bij list_decode"
+by (rule bijI [OF inj_list_decode surj_list_decode])
+
+lemma list_encode_eq: "list_encode x = list_encode y \<longleftrightarrow> x = y"
+by (rule inj_list_encode [THEN inj_eq])
+
+lemma list_decode_eq: "list_decode x = list_decode y \<longleftrightarrow> x = y"
+by (rule inj_list_decode [THEN inj_eq])
+
+
+subsection {* Finite sets of naturals *}
+
+subsubsection {* Preliminaries *}
+
+lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
+apply (safe intro!: finite_vimageI inj_Suc)
+apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
+apply (rule subsetI, case_tac x, simp, simp)
+apply (rule finite_insert [THEN iffD2])
+apply (erule finite_imageI)
+done
+
+lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
+by auto
+
+lemma vimage_Suc_insert_Suc:
+ "Suc -` insert (Suc n) A = insert n (Suc -` A)"
+by auto
+
+lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
+by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
+
+lemma div2_even_ext_nat:
+ "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
+apply (rule mod_div_equality [of x 2, THEN subst])
+apply (rule mod_div_equality [of y 2, THEN subst])
+apply (case_tac "even x")
+apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
+apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
+done
+
+subsubsection {* From sets to naturals *}
+
+definition
+ set_encode :: "nat set \<Rightarrow> nat"
+where
+ "set_encode = setsum (op ^ 2)"
+
+lemma set_encode_empty [simp]: "set_encode {} = 0"
+by (simp add: set_encode_def)
+
+lemma set_encode_insert [simp]:
+ "\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set_encode (insert n A) = 2^n + set_encode A"
+by (simp add: set_encode_def)
+
+lemma even_set_encode_iff: "finite A \<Longrightarrow> even (set_encode A) \<longleftrightarrow> 0 \<notin> A"
+unfolding set_encode_def by (induct set: finite, auto)
+
+lemma set_encode_vimage_Suc: "set_encode (Suc -` A) = set_encode A div 2"
+apply (cases "finite A")
+apply (erule finite_induct, simp)
+apply (case_tac x)
+apply (simp add: even_nat_Suc_div_2 even_set_encode_iff vimage_Suc_insert_0)
+apply (simp add: finite_vimageI add_commute vimage_Suc_insert_Suc)
+apply (simp add: set_encode_def finite_vimage_Suc_iff)
+done
+
+lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric]
+
+subsubsection {* From naturals to sets *}
+
+definition
+ set_decode :: "nat \<Rightarrow> nat set"
+where
+ "set_decode x = {n. odd (x div 2 ^ n)}"
+
+lemma set_decode_0 [simp]: "0 \<in> set_decode x \<longleftrightarrow> odd x"
+by (simp add: set_decode_def)
+
+lemma set_decode_Suc [simp]:
+ "Suc n \<in> set_decode x \<longleftrightarrow> n \<in> set_decode (x div 2)"
+by (simp add: set_decode_def div_mult2_eq)
+
+lemma set_decode_zero [simp]: "set_decode 0 = {}"
+by (simp add: set_decode_def)
+
+lemma set_decode_div_2: "set_decode (x div 2) = Suc -` set_decode x"
+by auto
+
+lemma set_decode_plus_power_2:
+ "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
+ apply (induct n arbitrary: z, simp_all)
+ apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2)
+ apply (rule set_ext, induct_tac x, simp, simp add: add_commute)
+done
+
+lemma finite_set_decode [simp]: "finite (set_decode n)"
+apply (induct n rule: nat_less_induct)
+apply (case_tac "n = 0", simp)
+apply (drule_tac x="n div 2" in spec, simp)
+apply (simp add: set_decode_div_2)
+apply (simp add: finite_vimage_Suc_iff)
+done
+
+subsubsection {* Proof of isomorphism *}
+
+lemma set_decode_inverse [simp]: "set_encode (set_decode n) = n"
+apply (induct n rule: nat_less_induct)
+apply (case_tac "n = 0", simp)
+apply (drule_tac x="n div 2" in spec, simp)
+apply (simp add: set_decode_div_2 set_encode_vimage_Suc)
+apply (erule div2_even_ext_nat)
+apply (simp add: even_set_encode_iff)
+done
+
+lemma set_encode_inverse [simp]: "finite A \<Longrightarrow> set_decode (set_encode A) = A"
+apply (erule finite_induct, simp_all)
+apply (simp add: set_decode_plus_power_2)
+done
+
+lemma inj_on_set_encode: "inj_on set_encode (Collect finite)"
+by (rule inj_on_inverseI [where g="set_decode"], simp)
+
+lemma set_encode_eq:
+ "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set_encode A = set_encode B \<longleftrightarrow> A = B"
+by (rule iffI, simp add: inj_onD [OF inj_on_set_encode], simp)
+
+end
--- a/src/HOL/Library/Nat_Int_Bij.thy Thu Mar 11 09:09:43 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-(* Title: HOL/Nat_Int_Bij.thy
- Author: Stefan Richter, Tobias Nipkow
-*)
-
-header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
-
-theory Nat_Int_Bij
-imports Main
-begin
-
-subsection{* A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
-
-text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}
-
-definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
-"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
-definition nat_to_nat2:: "nat \<Rightarrow> (nat * nat)" where
-"nat_to_nat2 = inv nat2_to_nat"
-
-lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
-proof (cases "2 dvd a")
- case True
- then show ?thesis by (rule dvd_mult2)
-next
- case False
- then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
- then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
- then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
- then show ?thesis by (rule dvd_mult)
-qed
-
-lemma
- assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
- shows nat2_to_nat_help: "u+v \<le> x+y"
-proof (rule classical)
- assume "\<not> ?thesis"
- then have contrapos: "x+y < u+v"
- by simp
- have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
- by (unfold nat2_to_nat_def) (simp add: Let_def)
- also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
- by (simp only: div_mult_self1_is_m)
- also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
- + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
- proof -
- have "2 dvd (x+y)*Suc(x+y)"
- by (rule dvd2_a_x_suc_a)
- then have "(x+y)*Suc(x+y) mod 2 = 0"
- by (simp only: dvd_eq_mod_eq_0)
- also
- have "2 * Suc(x+y) mod 2 = 0"
- by (rule mod_mult_self1_is_0)
- ultimately have
- "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
- by simp
- then show ?thesis
- by simp
- qed
- also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
- by (rule div_add1_eq [symmetric])
- also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
- by (simp only: add_mult_distrib [symmetric])
- also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
- by (simp only: mult_le_mono div_le_mono)
- also have "\<dots> \<le> nat2_to_nat (u,v)"
- by (unfold nat2_to_nat_def) (simp add: Let_def)
- finally show ?thesis
- by (simp only: eq)
-qed
-
-theorem nat2_to_nat_inj: "inj nat2_to_nat"
-proof -
- {
- fix u v x y
- assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
- then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
- also from eq1 [symmetric] have "x+y \<le> u+v"
- by (rule nat2_to_nat_help)
- finally have eq2: "u+v = x+y" .
- with eq1 have ux: "u=x"
- by (simp add: nat2_to_nat_def Let_def)
- with eq2 have vy: "v=y" by simp
- with ux have "(u,v) = (x,y)" by simp
- }
- then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
- then show ?thesis unfolding inj_on_def by simp
-qed
-
-lemma nat_to_nat2_surj: "surj nat_to_nat2"
-by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)
-
-
-lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"
-using gauss_sum[where 'a = nat]
-by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)
-
-lemma nat2_to_nat_surj: "surj nat2_to_nat"
-proof (unfold surj_def)
- {
- fix z::nat
- def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}"
- def x \<equiv> "z - (\<Sum>i\<le>r. i)"
-
- hence "finite {r. (\<Sum>i\<le>r. i) \<le> z}"
- by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
- also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}" by simp
- hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}" by fast
- ultimately have a: "r \<in> {r. (\<Sum>i\<le>r. i) \<le> z} \<and> (\<forall>s \<in> {r. (\<Sum>i\<le>r. i) \<le> z}. s \<le> r)"
- by (simp add: r_def del:mem_Collect_eq)
- {
- assume "r<x"
- hence "r+1\<le>x" by simp
- hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z" using x_def by arith
- hence "(r+1) \<in> {r. (\<Sum>i\<le>r. i) \<le> z}" by simp
- with a have "(r+1)\<le>r" by simp
- }
- hence b: "x\<le>r" by force
-
- def y \<equiv> "r-x"
- have "2*z=2*(\<Sum>i\<le>r. i)+2*x" using x_def a by simp arith
- also have "\<dots> = r * (r+1) + 2*x" using gauss_sum_nat_upto by simp
- also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
- also { have "2 dvd ((x+y)*(x+y+1))" using dvd2_a_x_suc_a by simp }
- hence "\<dots> = 2 * nat2_to_nat(x,y)"
- using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)
- finally have "z=nat2_to_nat (x, y)" by simp
- }
- thus "\<forall>y. \<exists>x. y = nat2_to_nat x" by fast
-qed
-
-lemma nat_to_nat2_inj: "inj nat_to_nat2"
- by (simp add: nat_to_nat2_def surj_imp_inj_inv nat2_to_nat_surj)
-
-
-subsection{* A bijection between @{text "\<nat>"} and @{text "\<int>"} *}
-
-definition nat_to_int_bij :: "nat \<Rightarrow> int" where
-"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"
-
-definition int_to_nat_bij :: "int \<Rightarrow> nat" where
-"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"
-
-lemma i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"
-by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger
-
-lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"
-proof -
- have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger
- thus ?thesis
- by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)
-qed
-
-lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"
-by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
-
-lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"
-by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
-
-lemma surj_nat_to_int_bij: "surj nat_to_int_bij"
-by (blast intro: n2i_i2n_id surjI)
-
-lemma surj_int_to_nat_bij: "surj int_to_nat_bij"
-by (blast intro: i2n_n2i_id surjI)
-
-lemma inj_nat_to_int_bij: "inj nat_to_int_bij"
-by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)
-
-lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
-by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
-
-lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
-by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
-
-lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
-by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
-
-
-end
--- a/src/HOL/Nitpick.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Nitpick.thy Thu Mar 11 09:09:51 2010 +0100
@@ -96,10 +96,10 @@
else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
-"card' X \<equiv> length (SOME xs. set xs = X \<and> distinct xs)"
+"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
-"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
+"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
"fold_graph' f z {} z" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Mar 11 09:09:51 2010 +0100
@@ -206,4 +206,39 @@
nitpick [binary_ints, expect = none]
sorry
+datatype tree = Null | Node nat tree tree
+
+primrec labels where
+"labels Null = {}" |
+"labels (Node x t u) = {x} \<union> labels t \<union> labels u"
+
+lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "labels (Node x t u) \<noteq> {}"
+nitpick [expect = none]
+oops
+
+lemma "card (labels t) > 0"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
+nitpick [expect = none]
+nitpick [dont_finitize, expect = none]
+sorry
+
+lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = none]
+oops
+
end
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Thu Mar 11 09:09:51 2010 +0100
@@ -24,8 +24,6 @@
fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
*}
-ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
-
ML {* genuine 1 @{prop "x = Not"} *}
ML {* none 1 @{prop "\<exists>x. x = Not"} *}
ML {* none 1 @{prop "\<not> False"} *}
--- a/src/HOL/Probability/Borel.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Probability/Borel.thy Thu Mar 11 09:09:51 2010 +0100
@@ -15,11 +15,6 @@
definition indicator_fn where
"indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
-definition mono_convergent where
- "mono_convergent u f s \<equiv>
- (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
- (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
-
lemma in_borel_measurable:
"f \<in> borel_measurable M \<longleftrightarrow>
sigma_algebra M \<and>
@@ -191,20 +186,20 @@
definition
nat_to_rat_surj :: "nat \<Rightarrow> rat" where
- "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n
- in Fract (nat_to_int_bij i) (nat_to_int_bij j))"
+ "nat_to_rat_surj n = (let (i,j) = prod_decode n
+ in Fract (int_decode i) (int_decode j))"
lemma nat_to_rat_surj: "surj nat_to_rat_surj"
proof (auto simp add: surj_def nat_to_rat_surj_def)
fix y
- show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)"
+ show "\<exists>x. y = (\<lambda>(i, j). Fract (int_decode i) (int_decode j)) (prod_decode x)"
proof (cases y)
case (Fract a b)
- obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij
+ obtain i where i: "int_decode i = a" using surj_int_decode
by (metis surj_def)
- obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij
+ obtain j where j: "int_decode j = b" using surj_int_decode
by (metis surj_def)
- obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj
+ obtain n where n: "prod_decode n = (i,j)" using surj_prod_decode
by (metis surj_def)
from Fract i j n show ?thesis
@@ -375,6 +370,95 @@
by (fast intro: borel_measurable_add_borel_measurable
borel_measurable_uminus_borel_measurable f g)
+lemma (in measure_space) borel_measurable_setsum_borel_measurable:
+ assumes s: "finite s"
+ shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
+proof (induct s)
+ case empty
+ thus ?case
+ by (simp add: borel_measurable_const)
+next
+ case (insert x s)
+ thus ?case
+ by (auto simp add: borel_measurable_add_borel_measurable)
+qed
+
+lemma (in measure_space) borel_measurable_cong:
+ assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
+ shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
+using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
+
+lemma (in measure_space) borel_measurable_inverse:
+ assumes "f \<in> borel_measurable M"
+ shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
+ unfolding borel_measurable_ge_iff
+proof (safe, rule linorder_cases)
+ fix a :: real assume "0 < a"
+ { fix w
+ from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
+ by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
+ linorder_not_le real_le_refl real_le_trans real_less_def
+ xt1(7) zero_less_divide_1_iff) }
+ hence "{w \<in> space M. a \<le> inverse (f w)} =
+ {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
+ with Int assms[unfolded borel_measurable_gr_iff]
+ assms[unfolded borel_measurable_le_iff]
+ show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+next
+ fix a :: real assume "0 = a"
+ { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
+ unfolding `0 = a`[symmetric] by auto }
+ thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
+ using assms[unfolded borel_measurable_ge_iff] by simp
+next
+ fix a :: real assume "a < 0"
+ { fix w
+ from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
+ apply (cases "0 \<le> f w")
+ apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
+ zero_le_divide_1_iff)
+ apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
+ linorder_not_le real_le_refl real_le_trans)
+ done }
+ hence "{w \<in> space M. a \<le> inverse (f w)} =
+ {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
+ with Un assms[unfolded borel_measurable_ge_iff]
+ assms[unfolded borel_measurable_le_iff]
+ show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+qed
+
+lemma (in measure_space) borel_measurable_divide:
+ assumes "f \<in> borel_measurable M"
+ and "g \<in> borel_measurable M"
+ shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
+ unfolding field_divide_inverse
+ by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
+
+
+section "Monotone convergence"
+
+definition mono_convergent where
+ "mono_convergent u f s \<equiv>
+ (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
+ (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+
+definition "upclose f g x = max (f x) (g x)"
+
+primrec mon_upclose where
+"mon_upclose 0 u = u 0" |
+"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
+
+lemma mono_convergentD:
+ assumes "mono_convergent u f s" and "x \<in> s"
+ shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
+ using assms unfolding mono_convergent_def by auto
+
+lemma mono_convergentI:
+ assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
+ assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
+ shows "mono_convergent u f s"
+ using assms unfolding mono_convergent_def by auto
+
lemma (in measure_space) mono_convergent_borel_measurable:
assumes u: "!!n. u n \<in> borel_measurable M"
assumes mc: "mono_convergent u f (space M)"
@@ -409,44 +493,11 @@
by (auto simp add: borel_measurable_le_iff)
qed
-lemma (in measure_space) borel_measurable_setsum_borel_measurable:
- assumes s: "finite s"
- shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
-proof (induct s)
- case empty
- thus ?case
- by (simp add: borel_measurable_const)
-next
- case (insert x s)
- thus ?case
- by (auto simp add: borel_measurable_add_borel_measurable)
-qed
-
-section "Monotone convergence"
-
-lemma mono_convergentD:
- assumes "mono_convergent u f s" and "x \<in> s"
- shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
- using assms unfolding mono_convergent_def by auto
-
-
-lemma mono_convergentI:
- assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
- assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
- shows "mono_convergent u f s"
- using assms unfolding mono_convergent_def by auto
-
lemma mono_convergent_le:
assumes "mono_convergent u f s" and "t \<in> s"
shows "u n t \<le> f t"
using mono_convergentD[OF assms] by (auto intro!: incseq_le)
-definition "upclose f g x = max (f x) (g x)"
-
-primrec mon_upclose where
-"mon_upclose 0 u = u 0" |
-"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
-
lemma mon_upclose_ex:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
shows "\<exists>n \<le> m. mon_upclose m u x = u n x"
@@ -561,4 +612,19 @@
qed
qed
+lemma mono_conv_outgrow:
+ assumes "incseq x" "x ----> y" "z < y"
+ shows "\<exists>b. \<forall> a \<ge> b. z < x a"
+using assms
+proof -
+ from assms have "y - z > 0" by simp
+ hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
+ unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
+ by simp
+ have "\<forall>m. x m \<le> y" using incseq_le assms by auto
+ hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
+ by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
+ from A B show ?thesis by auto
+qed
+
end
--- a/src/HOL/Probability/Caratheodory.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Thu Mar 11 09:09:51 2010 +0100
@@ -816,9 +816,9 @@
by (simp add: eqe)
finally show ?thesis using Series.summable_le2 [OF 1 2] by auto
qed
- def C \<equiv> "(split BB) o nat_to_nat2"
+ def C \<equiv> "(split BB) o prod_decode"
have C: "!!n. C n \<in> sets M"
- apply (rule_tac p="nat_to_nat2 n" in PairE)
+ apply (rule_tac p="prod_decode n" in PairE)
apply (simp add: C_def)
apply (metis BB subsetD rangeI)
done
@@ -828,11 +828,10 @@
assume x: "x \<in> A i"
with sbBB [of i] obtain j where "x \<in> BB i j"
by blast
- thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
- by (metis nat_to_nat2_surj internal_split_def prod.cases
- prod_case_split surj_f_inv_f)
+ thus "\<exists>i. x \<in> split BB (prod_decode i)"
+ by (metis prod_encode_inverse prod.cases prod_case_split)
qed
- have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
+ have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
by (rule ext) (auto simp add: C_def)
also have "... sums suminf ll"
proof (rule suminf_2dimen)
--- a/src/HOL/Probability/Lebesgue.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy Thu Mar 11 09:09:51 2010 +0100
@@ -25,9 +25,58 @@
shows "nonneg (neg_part f)"
unfolding nonneg_def neg_part_def min_def by auto
+lemma (in measure_space)
+ assumes "f \<in> borel_measurable M"
+ shows pos_part_borel_measurable: "pos_part f \<in> borel_measurable M"
+ and neg_part_borel_measurable: "neg_part f \<in> borel_measurable M"
+using assms
+proof -
+ { fix a :: real
+ { assume asm: "0 \<le> a"
+ from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
+ have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
+ unfolding pos_part_def using assms borel_measurable_le_iff by auto
+ hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
+ moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
+ unfolding pos_part_def using empty_sets by auto
+ ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
+ using le_less_linear by auto
+ } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+ { fix a :: real
+ { assume asm: "0 \<le> a"
+ from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
+ have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
+ unfolding neg_part_def using assms borel_measurable_ge_iff by auto
+ hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
+ moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
+ moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
+ ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
+ using le_less_linear by auto
+ } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+ from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
+qed
+
+lemma (in measure_space) pos_part_neg_part_borel_measurable_iff:
+ "f \<in> borel_measurable M \<longleftrightarrow>
+ pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
+proof -
+ { fix x
+ have "f x = pos_part f x - neg_part f x"
+ unfolding pos_part_def neg_part_def unfolding max_def min_def
+ by auto }
+ hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
+ hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
+ from pos_part_borel_measurable[of f] neg_part_borel_measurable[of f]
+ borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
+ this
+ show ?thesis by auto
+qed
+
context measure_space
begin
+section "Simple discrete step function"
+
definition
"pos_simple f =
{ (s :: nat set, a, x).
@@ -40,29 +89,6 @@
definition
"psfis f = pos_simple_integral ` (pos_simple f)"
-definition
- "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
- (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
-
-definition
- "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
-
-definition
- "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
-
-definition
- "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
-
-definition
- "countable_space_integral f \<equiv>
- let e = enumerate (f ` space M) in
- suminf (\<lambda>r. e r * measure M (f -` {e r} \<inter> space M))"
-
-definition
- "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
- f \<in> borel_measurable M \<and>
- (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
-
lemma pos_simpleE[consumes 1]:
assumes ps: "(s, a, x) \<in> pos_simple f"
obtains "finite s" and "nonneg f" and "nonneg x"
@@ -105,6 +131,11 @@
shows "psfis f = psfis g"
unfolding psfis_def using pos_simple_cong[OF assms] by simp
+lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
+ unfolding psfis_def pos_simple_def pos_simple_integral_def
+ by (auto simp: nonneg_def
+ intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
+
lemma pos_simple_setsum_indicator_fn:
assumes ps: "(s, a, x) \<in> pos_simple f"
and "t \<in> space M"
@@ -121,28 +152,7 @@
using `i \<in> s` by simp
qed
-lemma (in measure_space) measure_setsum_split:
- assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
- assumes "(\<Union>i \<in> r. b i) = space M"
- assumes "disjoint_family_on b r"
- shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
-proof -
- have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
- using assms by auto
- show ?thesis unfolding *
- proof (rule measure_finitely_additive''[symmetric])
- show "finite r" using `finite r` by auto
- { fix i assume "i \<in> r"
- hence "b i \<in> sets M" using br_in_M by auto
- thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
- }
- show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
- using `disjoint_family_on b r`
- unfolding disjoint_family_on_def by auto
- qed
-qed
-
-lemma (in measure_space) pos_simple_common_partition:
+lemma pos_simple_common_partition:
assumes psf: "(s, a, x) \<in> pos_simple f"
assumes psg: "(s', b, y) \<in> pos_simple g"
obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
@@ -229,7 +239,7 @@
qed
qed
-lemma (in measure_space) pos_simple_integral_equal:
+lemma pos_simple_integral_equal:
assumes psx: "(s, a, x) \<in> pos_simple f"
assumes psy: "(s', b, y) \<in> pos_simple f"
shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
@@ -269,7 +279,7 @@
finally show "?left = ?right" .
qed
-lemma (in measure_space)psfis_present:
+lemma psfis_present:
assumes "A \<in> psfis f"
assumes "B \<in> psfis g"
obtains z z' c k where
@@ -295,7 +305,7 @@
qed
qed
-lemma (in measure_space) pos_simple_integral_add:
+lemma pos_simple_integral_add:
assumes "(s, a, x) \<in> pos_simple f"
assumes "(s', b, y) \<in> pos_simple g"
obtains s'' c z where
@@ -468,70 +478,6 @@
thus ?thesis using r unfolding psfis_def image_def by auto
qed
-lemma pos_simple_integral_setsum_image:
- assumes "finite P"
- assumes "\<And> i. i \<in> P \<Longrightarrow> (s i, a i, x i) \<in> pos_simple (f i)"
- obtains s' a' x' where
- "(s', a', x') \<in> pos_simple (\<lambda>t. (\<Sum> i \<in> P. f i t))"
- "pos_simple_integral (s', a', x') = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))"
-using assms that
-proof (induct P arbitrary:thesis rule:finite.induct)
- case emptyI note asms = this
- def s' == "{0 :: nat}"
- def a' == "\<lambda> x. if x = (0 :: nat) then space M else {}"
- def x' == "\<lambda> x :: nat. (0 :: real)"
- have "(s', a', x') \<in> pos_simple (\<lambda> t. 0)"
- unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto
- moreover have "pos_simple_integral (s', a', x') = 0"
- unfolding s'_def a'_def x'_def pos_simple_integral_def by auto
- ultimately show ?case using asms by auto
-next
-
- case (insertI P c) note asms = this
- then obtain s' a' x' where
- sax: "(s', a', x') \<in> pos_simple (\<lambda>t. \<Sum>i\<in>P. f i t)"
- "pos_simple_integral (s', a', x') =
- (\<Sum>i\<in>P. pos_simple_integral (s i, a i, x i))"
- by auto
-
- { assume "c \<in> P"
- hence "P = insert c P" by auto
- hence thesis using asms sax by auto
- }
- moreover
- { assume "c \<notin> P"
- from asms obtain s'' a'' x'' where
- sax': "s'' = s c" "a'' = a c" "x'' = x c"
- "(s'', a'', x'') \<in> pos_simple (f c)" by auto
- from sax sax' obtain k :: "nat \<Rightarrow> bool" and b :: "nat \<Rightarrow> 'a \<Rightarrow> bool" and z :: "nat \<Rightarrow> real" where
- tybbie:
- "(k, b, z) \<in> pos_simple (\<lambda>t. ((\<Sum>i\<in>P. f i t) + f c t))"
- "(pos_simple_integral (s', a', x') +
- pos_simple_integral (s'', a'', x'') =
- pos_simple_integral (k, b, z))"
- using pos_simple_integral_add by blast
-
- from tybbie have
- "pos_simple_integral (k, b, z) =
- pos_simple_integral (s', a', x') +
- pos_simple_integral (s'', a'', x'')" by simp
- also have "\<dots> = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))
- + pos_simple_integral (s c, a c, x c)"
- using sax sax' by auto
- also have "\<dots> = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
- using asms `c \<notin> P` by auto
- finally have A: "pos_simple_integral (k, b, z) = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
- by simp
-
- have "\<And> t. (\<Sum> i \<in> P. f i t) + f c t = (\<Sum> i \<in> insert c P. f i t)"
- using `c \<notin> P` `finite P` by auto
- hence B: "(k, b, z) \<in> pos_simple (\<lambda> t. (\<Sum> i \<in> insert c P. f i t))"
- using tybbie by simp
-
- from A B have thesis using asms by auto
- } ultimately show thesis by blast
-qed
-
lemma psfis_setsum_image:
assumes "finite P"
assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
@@ -577,57 +523,6 @@
unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
-lemma pos_part_neg_part_borel_measurable:
- assumes "f \<in> borel_measurable M"
- shows "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M"
-using assms
-proof -
- { fix a :: real
- { assume asm: "0 \<le> a"
- from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
- have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
- unfolding pos_part_def using assms borel_measurable_le_iff by auto
- hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
- moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
- unfolding pos_part_def using empty_sets by auto
- ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
- using le_less_linear by auto
- } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
- { fix a :: real
- { assume asm: "0 \<le> a"
- from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
- have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
- unfolding neg_part_def using assms borel_measurable_ge_iff by auto
- hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
- moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
- moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
- ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
- using le_less_linear by auto
- } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
- from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
-qed
-
-lemma pos_part_neg_part_borel_measurable_iff:
- "f \<in> borel_measurable M \<longleftrightarrow>
- pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
-proof -
- { fix x
- have "f x = pos_part f x - neg_part f x"
- unfolding pos_part_def neg_part_def unfolding max_def min_def
- by auto }
- hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
- hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
- from pos_part_neg_part_borel_measurable[of f]
- borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
- this
- show ?thesis by auto
-qed
-
-lemma borel_measurable_cong:
- assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
- shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
-using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
-
lemma psfis_borel_measurable:
assumes "a \<in> psfis f"
shows "f \<in> borel_measurable M"
@@ -654,21 +549,6 @@
show ?thesis by simp
qed
-lemma mono_conv_outgrow:
- assumes "incseq x" "x ----> y" "z < y"
- shows "\<exists>b. \<forall> a \<ge> b. z < x a"
-using assms
-proof -
- from assms have "y - z > 0" by simp
- hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
- unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
- by simp
- have "\<forall>m. x m \<le> y" using incseq_le assms by auto
- hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
- by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
- from A B show ?thesis by auto
-qed
-
lemma psfis_mono_conv_mono:
assumes mono: "mono_convergent u f (space M)"
and ps_u: "\<And>n. x n \<in> psfis (u n)"
@@ -679,7 +559,6 @@
proof (rule field_le_mult_one_interval)
fix z :: real assume "0 < z" and "z < 1"
hence "0 \<le> z" by auto
-(* def B' \<equiv> "\<lambda>n. {w \<in> space M. z * s w <= u n w}" *)
let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
have "incseq x" unfolding incseq_def
@@ -783,6 +662,12 @@
qed
qed
+section "Continuous posititve integration"
+
+definition
+ "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
+ (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
+
lemma psfis_nnfis:
"a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
unfolding nnfis_def mono_convergent_def incseq_def
@@ -1136,11 +1021,6 @@
show ?thesis unfolding nnfis_def by auto
qed
-lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
- unfolding psfis_def pos_simple_def pos_simple_integral_def
- by (auto simp: nonneg_def
- intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
-
lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
by (auto intro: the_equality nnfis_unique)
@@ -1158,6 +1038,14 @@
show ?thesis by safe
qed
+section "Lebesgue Integral"
+
+definition
+ "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
+
+definition
+ "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
+
lemma integral_cong:
assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
shows "integral f = integral g"
@@ -1203,7 +1091,7 @@
(is "\<exists>x. x \<in> nnfis ?pp \<and> _")
proof (rule nnfis_dom_conv)
show "?pp \<in> borel_measurable M"
- using borel by (rule pos_part_neg_part_borel_measurable)
+ using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
fix t assume "t \<in> space M"
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
@@ -1217,7 +1105,7 @@
(is "\<exists>x. x \<in> nnfis ?np \<and> _")
proof (rule nnfis_dom_conv)
show "?np \<in> borel_measurable M"
- using borel by (rule pos_part_neg_part_borel_measurable)
+ using borel by (rule pos_part_borel_measurable neg_part_borel_measurable)
show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
fix t assume "t \<in> space M"
with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
@@ -1419,6 +1307,8 @@
by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
qed
+section "Lebesgue integration on finite space"
+
lemma integral_finite_on_sets:
assumes "f \<in> borel_measurable M" and "finite (space M)" and "a \<in> sets M"
shows "integral (\<lambda>x. f x * indicator_fn a x) =
@@ -1489,51 +1379,12 @@
qed (auto intro!: image_eqI inj_onI)
qed
-lemma borel_measurable_inverse:
- assumes "f \<in> borel_measurable M"
- shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
- unfolding borel_measurable_ge_iff
-proof (safe, rule linorder_cases)
- fix a :: real assume "0 < a"
- { fix w
- from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
- by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
- linorder_not_le real_le_refl real_le_trans real_less_def
- xt1(7) zero_less_divide_1_iff) }
- hence "{w \<in> space M. a \<le> inverse (f w)} =
- {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
- with Int assms[unfolded borel_measurable_gr_iff]
- assms[unfolded borel_measurable_le_iff]
- show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
-next
- fix a :: real assume "0 = a"
- { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
- unfolding `0 = a`[symmetric] by auto }
- thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
- using assms[unfolded borel_measurable_ge_iff] by simp
-next
- fix a :: real assume "a < 0"
- { fix w
- from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
- apply (cases "0 \<le> f w")
- apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
- zero_le_divide_1_iff)
- apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
- linorder_not_le real_le_refl real_le_trans)
- done }
- hence "{w \<in> space M. a \<le> inverse (f w)} =
- {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
- with Un assms[unfolded borel_measurable_ge_iff]
- assms[unfolded borel_measurable_le_iff]
- show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
-qed
+section "Radon–Nikodym derivative"
-lemma borel_measurable_divide:
- assumes "f \<in> borel_measurable M"
- and "g \<in> borel_measurable M"
- shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
- unfolding field_divide_inverse
- by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
+definition
+ "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
+ f \<in> borel_measurable M \<and>
+ (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
lemma RN_deriv_finite_singleton:
fixes v :: "'a set \<Rightarrow> real"
@@ -1577,6 +1428,11 @@
using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
qed fact
+section "Lebesgue integration on countable spaces"
+
+definition
+ "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
+
lemma countable_space_integral_reduce:
assumes "positive M (measure M)" and "f \<in> borel_measurable M"
and "countable (f ` space M)"
--- a/src/HOL/Probability/Measure.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Probability/Measure.thy Thu Mar 11 09:09:51 2010 +0100
@@ -997,4 +997,25 @@
\<Longrightarrow> measure_space M"
by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto)
+lemma (in measure_space) measure_setsum_split:
+ assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
+ assumes "(\<Union>i \<in> r. b i) = space M"
+ assumes "disjoint_family_on b r"
+ shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
+proof -
+ have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
+ using assms by auto
+ show ?thesis unfolding *
+ proof (rule measure_finitely_additive''[symmetric])
+ show "finite r" using `finite r` by auto
+ { fix i assume "i \<in> r"
+ hence "b i \<in> sets M" using br_in_M by auto
+ thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
+ }
+ show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
+ using `disjoint_family_on b r`
+ unfolding disjoint_family_on_def by auto
+ qed
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Probability/SeriesPlus.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Probability/SeriesPlus.thy Thu Mar 11 09:09:51 2010 +0100
@@ -1,5 +1,5 @@
theory SeriesPlus
- imports Complex_Main Nat_Int_Bij
+ imports Complex_Main Nat_Bijection
begin
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -16,7 +16,7 @@
assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)"
and sumg: "summable g"
- shows "(f o nat_to_nat2) sums suminf g"
+ shows "(f o prod_decode) sums suminf g"
proof (simp add: sums_def)
{
fix x
@@ -31,18 +31,18 @@
thus "0 \<le> g m" using fsums [of m]
by (auto simp add: sums_iff)
qed
- show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
+ show "(\<lambda>n. \<Sum>x = 0..<n. f (prod_decode x)) ----> suminf g"
proof (rule increasing_LIMSEQ, simp add: f_nneg)
fix n
- def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
- def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
- have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})"
+ def i \<equiv> "Max (Domain (prod_decode ` {0..<n}))"
+ def j \<equiv> "Max (Range (prod_decode ` {0..<n}))"
+ have ij: "prod_decode ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})"
by (force simp add: i_def j_def
intro: finite_imageI Max_ge finite_Domain finite_Range)
- have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})"
- using setsum_reindex [of nat_to_nat2 "{0..<n}" f]
+ have "(\<Sum>x = 0..<n. f (prod_decode x)) = setsum f (prod_decode ` {0..<n})"
+ using setsum_reindex [of prod_decode "{0..<n}" f]
by (simp add: o_def)
- (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj)
+ (metis inj_prod_decode inj_prod_decode)
also have "... \<le> setsum f ({0..i} \<times> {0..j})"
by (rule setsum_mono2) (auto simp add: ij)
also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
@@ -56,10 +56,10 @@
by (auto simp add: sums_iff)
(metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg)
qed
- finally have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
+ finally have "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> setsum g {0..<Suc i}" .
also have "... \<le> suminf g"
by (rule series_pos_le [OF sumg]) (simp add: g_nneg)
- finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
+ finally show "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> suminf g" .
next
fix e :: real
assume e: "0 < e"
@@ -99,26 +99,25 @@
by auto
have finite_IJ: "finite IJ"
by (simp add: IJ_def)
- def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
- have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
+ def NIJ \<equiv> "Max (prod_decode -` IJ)"
+ have IJsb: "IJ \<subseteq> prod_decode ` {0..NIJ}"
proof (auto simp add: NIJ_def)
fix i j
assume ij:"(i,j) \<in> IJ"
- hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
- by (metis nat_to_nat2_surj surj_f_inv_f)
- thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
+ hence "(i,j) = prod_decode (prod_encode (i,j))"
+ by simp
+ thus "(i,j) \<in> prod_decode ` {0..Max (prod_decode -` IJ)}"
by (rule image_eqI)
- (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
- nat_to_nat2_surj surj_f_inv_f)
+ (simp add: ij finite_vimageI [OF finite_IJ inj_prod_decode])
qed
- have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
+ have "setsum f IJ \<le> setsum f (prod_decode `{0..NIJ})"
by (rule setsum_mono2) (auto simp add: IJsb)
- also have "... = (\<Sum>k = 0..NIJ. f (nat_to_nat2 k))"
- by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV])
- also have "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
+ also have "... = (\<Sum>k = 0..NIJ. f (prod_decode k))"
+ by (simp add: setsum_reindex inj_prod_decode)
+ also have "... = (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))"
by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
- finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
- thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
+ finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))" .
+ thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (prod_decode x)) + e" using glessf
by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
qed
qed
--- a/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 11 09:09:51 2010 +0100
@@ -7,7 +7,7 @@
header{*The Message Theory, Modified for SET*}
theory Message_SET
-imports Main Nat_Int_Bij
+imports Main Nat_Bijection
begin
subsection{*General Lemmas*}
@@ -81,17 +81,16 @@
definition nat_of_agent :: "agent => nat" where
- "nat_of_agent == agent_case (curry nat2_to_nat 0)
- (curry nat2_to_nat 1)
- (curry nat2_to_nat 2)
- (curry nat2_to_nat 3)
- (nat2_to_nat (4,0))"
+ "nat_of_agent == agent_case (curry prod_encode 0)
+ (curry prod_encode 1)
+ (curry prod_encode 2)
+ (curry prod_encode 3)
+ (prod_encode (4,0))"
--{*maps each agent to a unique natural number, for specifications*}
text{*The function is indeed injective*}
lemma inj_nat_of_agent: "inj nat_of_agent"
-by (simp add: nat_of_agent_def inj_on_def curry_def
- nat2_to_nat_inj [THEN inj_eq] split: agent.split)
+by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split)
constdefs
--- a/src/HOL/SET_Protocol/Purchase.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy Thu Mar 11 09:09:51 2010 +0100
@@ -280,9 +280,9 @@
inj_PANSecret: "inj PANSecret"
CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"
--{*No CardSecret equals any PANSecret*}
- apply (rule_tac x="curry nat2_to_nat 0" in exI)
- apply (rule_tac x="curry nat2_to_nat 1" in exI)
- apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def)
+ apply (rule_tac x="curry prod_encode 0" in exI)
+ apply (rule_tac x="curry prod_encode 1" in exI)
+ apply (simp add: prod_encode_eq inj_on_def)
done
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
--- a/src/HOL/SET_Protocol/ROOT.ML Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/SET_Protocol/ROOT.ML Thu Mar 11 09:09:51 2010 +0100
@@ -5,5 +5,5 @@
Root file for the SET protocol proofs.
*)
-no_document use_thys ["Nat_Int_Bij"];
+no_document use_thys ["Nat_Bijection"];
use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
--- a/src/HOL/Tools/Nitpick/HISTORY Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Thu Mar 11 09:09:51 2010 +0100
@@ -11,6 +11,7 @@
* Improved efficiency of "destroy_constrs" optimization
* Fixed soundness bugs related to "destroy_constrs" optimization and record
getters
+ * Fixed soundness bug related to higher-order constructors
* Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 09:09:51 2010 +0100
@@ -157,7 +157,8 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
- NotInstalled |
+ JavaNotInstalled |
+ KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Interrupted of int list option |
@@ -303,7 +304,8 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
- NotInstalled |
+ JavaNotInstalled |
+ KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Interrupted of int list option |
@@ -893,7 +895,7 @@
map (fn b => (out_assign b; out ";")) expr_assigns;
out "solve "; out_outmost_f formula; out ";\n")
in
- out ("// This file was generated by Isabelle (probably Nitpick)\n" ^
+ out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
"// " ^ Date.fmt "%Y-%m-%d %H:%M:%S"
(Date.fromTimeLocal (Time.now ())) ^ "\n");
map out_problem problems
@@ -1083,8 +1085,11 @@
||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
val js = triv_js @ nontriv_js
val first_error =
- File.fold_lines (fn line => fn "" => line | s => s) err_path ""
- handle IO.Io _ => "" | OS.SysErr _ => ""
+ (File.fold_lines (fn line => fn "" => line | s => s) err_path ""
+ handle IO.Io _ => "" | OS.SysErr _ => "")
+ |> perhaps (try (unsuffix "\r"))
+ |> perhaps (try (unsuffix "."))
+ |> perhaps (try (unprefix "Error: "))
in
if null ps then
if code = 2 then
@@ -1092,12 +1097,15 @@
else if code = 0 then
Normal ([], js, first_error)
else if first_error |> Substring.full
+ |> Substring.position "exec: java" |> snd
+ |> Substring.isEmpty |> not then
+ JavaNotInstalled
+ else if first_error |> Substring.full
|> Substring.position "NoClassDefFoundError" |> snd
|> Substring.isEmpty |> not then
- NotInstalled
+ KodkodiNotInstalled
else if first_error <> "" then
- Error (first_error |> perhaps (try (unsuffix "."))
- |> perhaps (try (unprefix "Error: ")), js)
+ Error (first_error, js)
else if io_error then
Error ("I/O error", js)
else
--- a/src/HOL/Tools/Nitpick/minipick.ML Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Thu Mar 11 09:09:51 2010 +0100
@@ -336,7 +336,8 @@
val max_solutions = 1
in
case solve_any_problem overlord NONE max_threads max_solutions problems of
- NotInstalled => "unknown"
+ JavaNotInstalled => "unknown"
+ | KodkodiNotInstalled => "unknown"
| Normal ([], _, _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 11 09:09:51 2010 +0100
@@ -149,6 +149,9 @@
(length ts downto 1) ts))]
(* unit -> string *)
+fun install_java_message () =
+ "Nitpick requires a Java 1.5 virtual machine called \"java\"."
+(* unit -> string *)
fun install_kodkodi_message () =
"Nitpick requires the external Java program Kodkodi. To install it, download \
\the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
@@ -726,7 +729,10 @@
else
case KK.solve_any_problem overlord deadline max_threads max_solutions
(map fst problems) of
- KK.NotInstalled =>
+ KK.JavaNotInstalled =>
+ (print_m install_java_message;
+ (found_really_genuine, max_potential, max_genuine, donno + 1))
+ | KK.KodkodiNotInstalled =>
(print_m install_kodkodi_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.Normal ([], unsat_js, s) =>
@@ -911,8 +917,7 @@
in
"Nitpick " ^ did_so_and_so ^
(if is_some (!checked_problems) andalso total > 0 then
- " after checking " ^
- string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
+ " " ^ string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
string_of_int total ^ " scope" ^ plural_s total
else
"") ^ "."
@@ -922,7 +927,7 @@
fun run_batches _ _ []
(found_really_genuine, max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
- (print_m (fn () => excipit "ran out of some resource"); "unknown")
+ (print_m (fn () => excipit "checked"); "unknown")
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_m (fn () =>
@@ -966,10 +971,11 @@
(false, max_potential, max_genuine, 0)
handle Exn.Interrupt => do_interrupted ())
handle TimeLimit.TimeOut =>
- (print_m (fn () => excipit "ran out of time");
+ (print_m (fn () => excipit "ran out of time after checking");
if !met_potential > 0 then "potential" else "unknown")
- | Exn.Interrupt => if auto orelse debug then raise Interrupt
- else error (excipit "was interrupted")
+ | Exn.Interrupt =>
+ if auto orelse debug then raise Interrupt
+ else error (excipit "was interrupted after checking")
val _ = print_v (fn () => "Total time: " ^
signed_string_of_int (Time.toMilliseconds
(Timer.checkRealTimer timer)) ^ " ms.")
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 11 09:09:51 2010 +0100
@@ -1653,6 +1653,7 @@
else
kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)]
(kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)
+ |> is_opt_rep (rep_of arg_u) ? to_guard [arg_u] R1
end) sel_us arg_us
in fold1 kk_intersect set_rs end
| BoundRel (x, _, _, _) => KK.Var x
@@ -1723,10 +1724,8 @@
map2 (kk_not oo kk_n_ary_function kk)
(map (unopt_rep o rep_of) func_guard_us) func_guard_rs
in
- if null guard_fs then
- r
- else
- kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
+ if null guard_fs then r
+ else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
end
(* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *)
and to_project new_R old_R r j0 =
--- a/src/HOLCF/IsaMakefile Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOLCF/IsaMakefile Thu Mar 11 09:09:51 2010 +0100
@@ -47,7 +47,6 @@
HOLCF.thy \
Lift.thy \
LowerPD.thy \
- NatIso.thy \
One.thy \
Pcpodef.thy \
Pcpo.thy \
--- a/src/HOLCF/NatIso.thy Thu Mar 11 09:09:43 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,241 +0,0 @@
-(* Title: HOLCF/NatIso.thy
- Author: Brian Huffman
-*)
-
-header {* Isomorphisms of the Natural Numbers *}
-
-theory NatIso
-imports Parity
-begin
-
-subsection {* Isomorphism between naturals and sums of naturals *}
-
-primrec
- sum2nat :: "nat + nat \<Rightarrow> nat"
-where
- "sum2nat (Inl a) = a + a"
-| "sum2nat (Inr b) = Suc (b + b)"
-
-primrec
- nat2sum :: "nat \<Rightarrow> nat + nat"
-where
- "nat2sum 0 = Inl 0"
-| "nat2sum (Suc n) = (case nat2sum n of
- Inl a \<Rightarrow> Inr a | Inr b \<Rightarrow> Inl (Suc b))"
-
-lemma nat2sum_sum2nat [simp]: "nat2sum (sum2nat x) = x"
-by (induct x, rule_tac [!] nat.induct, simp_all)
-
-lemma sum2nat_nat2sum [simp]: "sum2nat (nat2sum n) = n"
-by (induct n, auto split: sum.split)
-
-lemma inj_sum2nat: "inj sum2nat"
-by (rule inj_on_inverseI, rule nat2sum_sum2nat)
-
-lemma sum2nat_eq_iff [simp]: "sum2nat x = sum2nat y \<longleftrightarrow> x = y"
-by (rule inj_sum2nat [THEN inj_eq])
-
-lemma inj_nat2sum: "inj nat2sum"
-by (rule inj_on_inverseI, rule sum2nat_nat2sum)
-
-lemma nat2sum_eq_iff [simp]: "nat2sum x = nat2sum y \<longleftrightarrow> x = y"
-by (rule inj_nat2sum [THEN inj_eq])
-
-declare sum2nat.simps [simp del]
-declare nat2sum.simps [simp del]
-
-
-subsection {* Isomorphism between naturals and pairs of naturals *}
-
-function
- prod2nat :: "nat \<times> nat \<Rightarrow> nat"
-where
- "prod2nat (0, 0) = 0"
-| "prod2nat (0, Suc n) = Suc (prod2nat (n, 0))"
-| "prod2nat (Suc m, n) = Suc (prod2nat (m, Suc n))"
-by pat_completeness auto
-
-termination by (relation
- "inv_image (measure id <*lex*> measure id) (\<lambda>(x, y). (x+y, x))") auto
-
-primrec
- nat2prod :: "nat \<Rightarrow> nat \<times> nat"
-where
- "nat2prod 0 = (0, 0)"
-| "nat2prod (Suc x) =
- (case nat2prod x of (m, n) \<Rightarrow>
- (case n of 0 \<Rightarrow> (0, Suc m) | Suc n \<Rightarrow> (Suc m, n)))"
-
-lemma nat2prod_prod2nat [simp]: "nat2prod (prod2nat x) = x"
-by (induct x, rule prod2nat.induct, simp_all)
-
-lemma prod2nat_nat2prod [simp]: "prod2nat (nat2prod n) = n"
-by (induct n, auto split: prod.split nat.split)
-
-lemma inj_prod2nat: "inj prod2nat"
-by (rule inj_on_inverseI, rule nat2prod_prod2nat)
-
-lemma prod2nat_eq_iff [simp]: "prod2nat x = prod2nat y \<longleftrightarrow> x = y"
-by (rule inj_prod2nat [THEN inj_eq])
-
-lemma inj_nat2prod: "inj nat2prod"
-by (rule inj_on_inverseI, rule prod2nat_nat2prod)
-
-lemma nat2prod_eq_iff [simp]: "nat2prod x = nat2prod y \<longleftrightarrow> x = y"
-by (rule inj_nat2prod [THEN inj_eq])
-
-subsubsection {* Ordering properties *}
-
-lemma fst_snd_le_prod2nat: "fst x \<le> prod2nat x \<and> snd x \<le> prod2nat x"
-by (induct x rule: prod2nat.induct) auto
-
-lemma fst_le_prod2nat: "fst x \<le> prod2nat x"
-by (rule fst_snd_le_prod2nat [THEN conjunct1])
-
-lemma snd_le_prod2nat: "snd x \<le> prod2nat x"
-by (rule fst_snd_le_prod2nat [THEN conjunct2])
-
-lemma le_prod2nat_1: "a \<le> prod2nat (a, b)"
-using fst_le_prod2nat [where x="(a, b)"] by simp
-
-lemma le_prod2nat_2: "b \<le> prod2nat (a, b)"
-using snd_le_prod2nat [where x="(a, b)"] by simp
-
-declare prod2nat.simps [simp del]
-declare nat2prod.simps [simp del]
-
-
-subsection {* Isomorphism between naturals and finite sets of naturals *}
-
-subsubsection {* Preliminaries *}
-
-lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
-apply (safe intro!: finite_vimageI inj_Suc)
-apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
-apply (rule subsetI, case_tac x, simp, simp)
-apply (rule finite_insert [THEN iffD2])
-apply (erule finite_imageI)
-done
-
-lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
-by auto
-
-lemma vimage_Suc_insert_Suc:
- "Suc -` insert (Suc n) A = insert n (Suc -` A)"
-by auto
-
-lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
-by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
-
-lemma div2_even_ext_nat:
- "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
-apply (rule mod_div_equality [of x 2, THEN subst])
-apply (rule mod_div_equality [of y 2, THEN subst])
-apply (case_tac "even x")
-apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
-apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
-done
-
-subsubsection {* From sets to naturals *}
-
-definition
- set2nat :: "nat set \<Rightarrow> nat" where
- "set2nat = setsum (op ^ 2)"
-
-lemma set2nat_empty [simp]: "set2nat {} = 0"
-by (simp add: set2nat_def)
-
-lemma set2nat_insert [simp]:
- "\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set2nat (insert n A) = 2^n + set2nat A"
-by (simp add: set2nat_def)
-
-lemma even_set2nat_iff: "finite A \<Longrightarrow> even (set2nat A) = (0 \<notin> A)"
-by (unfold set2nat_def, erule finite_induct, auto)
-
-lemma set2nat_vimage_Suc: "set2nat (Suc -` A) = set2nat A div 2"
-apply (case_tac "finite A")
-apply (erule finite_induct, simp)
-apply (case_tac x)
-apply (simp add: even_nat_Suc_div_2 even_set2nat_iff vimage_Suc_insert_0)
-apply (simp add: finite_vimageI add_commute vimage_Suc_insert_Suc)
-apply (simp add: set2nat_def finite_vimage_Suc_iff)
-done
-
-lemmas set2nat_div_2 = set2nat_vimage_Suc [symmetric]
-
-subsubsection {* From naturals to sets *}
-
-definition
- nat2set :: "nat \<Rightarrow> nat set" where
- "nat2set x = {n. odd (x div 2 ^ n)}"
-
-lemma nat2set_0 [simp]: "0 \<in> nat2set x \<longleftrightarrow> odd x"
-by (simp add: nat2set_def)
-
-lemma nat2set_Suc [simp]:
- "Suc n \<in> nat2set x \<longleftrightarrow> n \<in> nat2set (x div 2)"
-by (simp add: nat2set_def div_mult2_eq)
-
-lemma nat2set_zero [simp]: "nat2set 0 = {}"
-by (simp add: nat2set_def)
-
-lemma nat2set_div_2: "nat2set (x div 2) = Suc -` nat2set x"
-by auto
-
-lemma nat2set_plus_power_2:
- "n \<notin> nat2set z \<Longrightarrow> nat2set (2 ^ n + z) = insert n (nat2set z)"
- apply (induct n arbitrary: z, simp_all)
- apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2)
- apply (rule set_ext, induct_tac x, simp, simp add: add_commute)
-done
-
-lemma finite_nat2set [simp]: "finite (nat2set n)"
-apply (induct n rule: nat_less_induct)
-apply (case_tac "n = 0", simp)
-apply (drule_tac x="n div 2" in spec, simp)
-apply (simp add: nat2set_div_2)
-apply (simp add: finite_vimage_Suc_iff)
-done
-
-subsubsection {* Proof of isomorphism *}
-
-lemma set2nat_nat2set [simp]: "set2nat (nat2set n) = n"
-apply (induct n rule: nat_less_induct)
-apply (case_tac "n = 0", simp)
-apply (drule_tac x="n div 2" in spec, simp)
-apply (simp add: nat2set_div_2 set2nat_vimage_Suc)
-apply (erule div2_even_ext_nat)
-apply (simp add: even_set2nat_iff)
-done
-
-lemma nat2set_set2nat [simp]: "finite A \<Longrightarrow> nat2set (set2nat A) = A"
-apply (erule finite_induct, simp_all)
-apply (simp add: nat2set_plus_power_2)
-done
-
-lemma inj_nat2set: "inj nat2set"
-by (rule inj_on_inverseI, rule set2nat_nat2set)
-
-lemma nat2set_eq_iff [simp]: "nat2set x = nat2set y \<longleftrightarrow> x = y"
-by (rule inj_eq [OF inj_nat2set])
-
-lemma inj_on_set2nat: "inj_on set2nat (Collect finite)"
-by (rule inj_on_inverseI [where g="nat2set"], simp)
-
-lemma set2nat_eq_iff [simp]:
- "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set2nat A = set2nat B \<longleftrightarrow> A = B"
-by (rule iffI, simp add: inj_onD [OF inj_on_set2nat], simp)
-
-subsubsection {* Ordering properties *}
-
-lemma nat_less_power2: "n < 2^n"
-by (induct n) simp_all
-
-lemma less_set2nat: "\<lbrakk>finite A; x \<in> A\<rbrakk> \<Longrightarrow> x < set2nat A"
-unfolding set2nat_def
-apply (rule order_less_le_trans [where y="setsum (op ^ 2) {x}"])
-apply (simp add: nat_less_power2)
-apply (erule setsum_mono2, simp, simp)
-done
-
-end
\ No newline at end of file
--- a/src/HOLCF/ROOT.ML Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOLCF/ROOT.ML Thu Mar 11 09:09:51 2010 +0100
@@ -4,6 +4,6 @@
HOLCF -- a semantic extension of HOL by the LCF logic.
*)
-no_document use_thys ["Nat_Int_Bij"];
+no_document use_thys ["Nat_Bijection"];
use_thys ["HOLCF"];
--- a/src/HOLCF/Universal.thy Thu Mar 11 09:09:43 2010 +0100
+++ b/src/HOLCF/Universal.thy Thu Mar 11 09:09:51 2010 +0100
@@ -3,7 +3,7 @@
*)
theory Universal
-imports CompactBasis NatIso
+imports CompactBasis Nat_Bijection
begin
subsection {* Basis datatype *}
@@ -13,7 +13,7 @@
definition
node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis"
where
- "node i a S = Suc (prod2nat (i, prod2nat (a, set2nat S)))"
+ "node i a S = Suc (prod_encode (i, prod_encode (a, set_encode S)))"
lemma node_not_0 [simp]: "node i a S \<noteq> 0"
unfolding node_def by simp
@@ -24,30 +24,30 @@
lemma node_inject [simp]:
"\<lbrakk>finite S; finite T\<rbrakk>
\<Longrightarrow> node i a S = node j b T \<longleftrightarrow> i = j \<and> a = b \<and> S = T"
-unfolding node_def by simp
+unfolding node_def by (simp add: prod_encode_eq set_encode_eq)
lemma node_gt0: "i < node i a S"
unfolding node_def less_Suc_eq_le
-by (rule le_prod2nat_1)
+by (rule le_prod_encode_1)
lemma node_gt1: "a < node i a S"
unfolding node_def less_Suc_eq_le
-by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2])
+by (rule order_trans [OF le_prod_encode_1 le_prod_encode_2])
lemma nat_less_power2: "n < 2^n"
by (induct n) simp_all
lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S"
-unfolding node_def less_Suc_eq_le set2nat_def
-apply (rule order_trans [OF _ le_prod2nat_2])
-apply (rule order_trans [OF _ le_prod2nat_2])
+unfolding node_def less_Suc_eq_le set_encode_def
+apply (rule order_trans [OF _ le_prod_encode_2])
+apply (rule order_trans [OF _ le_prod_encode_2])
apply (rule order_trans [where y="setsum (op ^ 2) {b}"])
apply (simp add: nat_less_power2 [THEN order_less_imp_le])
apply (erule setsum_mono2, simp, simp)
done
-lemma eq_prod2nat_pairI:
- "\<lbrakk>fst (nat2prod x) = a; snd (nat2prod x) = b\<rbrakk> \<Longrightarrow> x = prod2nat (a, b)"
+lemma eq_prod_encode_pairI:
+ "\<lbrakk>fst (prod_decode x) = a; snd (prod_decode x) = b\<rbrakk> \<Longrightarrow> x = prod_encode (a, b)"
by (erule subst, erule subst, simp)
lemma node_cases:
@@ -57,10 +57,10 @@
apply (cases x)
apply (erule 1)
apply (rule 2)
- apply (rule finite_nat2set)
+ apply (rule finite_set_decode)
apply (simp add: node_def)
- apply (rule eq_prod2nat_pairI [OF refl])
- apply (rule eq_prod2nat_pairI [OF refl refl])
+ apply (rule eq_prod_encode_pairI [OF refl])
+ apply (rule eq_prod_encode_pairI [OF refl refl])
done
lemma node_induct:
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Mar 11 09:09:43 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Mar 11 09:09:51 2010 +0100
@@ -849,17 +849,20 @@
fun splitasms ctxt (asms : thm list) : splittree =
let val {neqE, ...} = get_data ctxt
- fun elim_neq (asms', []) = Tip (rev asms')
- | elim_neq (asms', asm::asms) =
- (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
+ fun elim_neq [] (asms', []) = Tip (rev asms')
+ | elim_neq [] (asms', asms) = Tip (rev asms' @ asms)
+ | elim_neq (neq :: neqs) (asms', []) = elim_neq neqs ([],rev asms')
+ | elim_neq (neqs as (neq :: _)) (asms', asm::asms) =
+ (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of
SOME spl =>
let val (ct1, ct2) = extract (cprop_of spl)
val thm1 = assume ct1
val thm2 = assume ct2
- in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2]))
+ in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]),
+ ct2, elim_neq neqs (asms', asms@[thm2]))
end
- | NONE => elim_neq (asm::asms', asms))
-in elim_neq ([], asms) end;
+ | NONE => elim_neq neqs (asm::asms', asms))
+in elim_neq neqE ([], asms) end;
fun fwdproof ss (Tip asms : splittree) (j::js : injust list) = (mkthm ss asms j, js)
| fwdproof ss (Spl (thm, ct1, tree1, ct2, tree2)) js =