# HG changeset patch # User haftmann # Date 1268294991 -3600 # Node ID 267e15230a318936a207af6b3548402abb219e53 # Parent 44936737902dfe4a7d1c7b69ab765ac79f7c6b38# Parent 5e5925871d6f137ea50cecff0f283bbaf00b4248 merged diff -r 5e5925871d6f -r 267e15230a31 doc-src/Nitpick/nitpick.tex --- 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: diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Auth/TLS.thy --- 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 diff -r 5e5925871d6f -r 267e15230a31 src/HOL/IsaMakefile --- 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 \ diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Library/Countable.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 \ 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 \ m \ sum n \ sum m" - by (induct n m rule: diff_induct) auto - -definition - "pair_encode = (\(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 \ a + b \ Suc (c + d) \ c + d \ 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 \ Suc (c + d)" - from sum_mono[OF this] eq - show ?thesis by auto - next - assume "c + d \ Suc (a + b)" - from sum_mono[OF this] eq - show ?thesis by auto - qed -qed - instance "*" :: (countable, countable) countable -by (rule countable_classI [of "\(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 "\(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 "(\x. case x of Inl a \ to_nat (False, to_nat a) | Inr b \ to_nat (True, to_nat b))"]) - (auto split:sum.splits) + (simp split: sum.split_asm) text {* Integers *} -lemma int_cases: "(i::int) = 0 \ i < 0 \ 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 "(\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 "\x. case x of None \ 0 - | Some y \ Suc (to_nat y)"]) - (auto split:option.splits) + by (rule countable_classI [of "option_case 0 (Suc \ 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\countable list \ 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 \ 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 \ 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 "\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 "\n. r = nat_to_rat_surj n" by(auto simp:Let_def) qed qed diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Library/Nat_Bijection.thy --- /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 \ nat"} *} + +text "Triangle numbers: 0, 1, 3, 6, 10, 15, ..." + +definition + triangle :: "nat \ 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 \ nat \ nat" +where + "prod_encode = (\(m, n). triangle (m + n) + m)" + +text {* In this auxiliary function, @{term "triangle k + m"} is an invariant. *} + +fun + prod_decode_aux :: "nat \ nat \ nat \ nat" +where + "prod_decode_aux k m = + (if m \ 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 \ nat \ 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 \ x = y" +by (rule inj_prod_encode [THEN inj_eq]) + +lemma prod_decode_eq: "prod_decode x = prod_decode y \ x = y" +by (rule inj_prod_decode [THEN inj_eq]) + +text {* Ordering properties *} + +lemma le_prod_encode_1: "a \ prod_encode (a, b)" +unfolding prod_encode_def by simp + +lemma le_prod_encode_2: "b \ prod_encode (a, b)" +unfolding prod_encode_def by (induct b, simp_all) + + +subsection {* Type @{typ "nat + nat"} *} + +definition + sum_encode :: "nat + nat \ nat" +where + "sum_encode x = (case x of Inl a \ 2 * a | Inr b \ Suc (2 * b))" + +definition + sum_decode :: "nat \ 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 \ x = y" +by (rule inj_sum_encode [THEN inj_eq]) + +lemma sum_decode_eq: "sum_decode x = sum_decode y \ x = y" +by (rule inj_sum_decode [THEN inj_eq]) + + +subsection {* Type @{typ "int"} *} + +definition + int_encode :: "int \ nat" +where + "int_encode i = sum_encode (if 0 \ i then Inl (nat i) else Inr (nat (- i - 1)))" + +definition + int_decode :: "nat \ int" +where + "int_decode n = (case sum_decode n of Inl a \ int a | Inr b \ - 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 \ x = y" +by (rule inj_int_encode [THEN inj_eq]) + +lemma int_decode_eq: "int_decode x = int_decode y \ x = y" +by (rule inj_int_decode [THEN inj_eq]) + + +subsection {* Type @{typ "nat list"} *} + +fun + list_encode :: "nat list \ nat" +where + "list_encode [] = 0" +| "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))" + +function + list_decode :: "nat \ nat list" +where + "list_decode 0 = []" +| "list_decode (Suc n) = (case prod_decode n of (x, y) \ 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 \ x = y" +by (rule inj_list_encode [THEN inj_eq]) + +lemma list_decode_eq: "list_decode x = list_decode y \ 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) \ 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 \ 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: + "\x div 2 = y div 2; even x = even y\ \ (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 \ 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]: + "\finite A; n \ A\ \ set_encode (insert n A) = 2^n + set_encode A" +by (simp add: set_encode_def) + +lemma even_set_encode_iff: "finite A \ even (set_encode A) \ 0 \ 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 \ nat set" +where + "set_decode x = {n. odd (x div 2 ^ n)}" + +lemma set_decode_0 [simp]: "0 \ set_decode x \ odd x" +by (simp add: set_decode_def) + +lemma set_decode_Suc [simp]: + "Suc n \ set_decode x \ n \ 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 \ set_decode z \ 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 \ 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: + "\finite A; finite B\ \ set_encode A = set_encode B \ A = B" +by (rule iffI, simp add: inj_onD [OF inj_on_set_encode], simp) + +end diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Library/Nat_Int_Bij.thy --- 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 "\"} and @{text "\\"} *} - -text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *} - -definition nat2_to_nat:: "(nat * nat) \ nat" where -"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)" -definition nat_to_nat2:: "nat \ (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 \ x+y" -proof (rule classical) - assume "\ ?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 "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" - by (simp only: div_mult_self1_is_m) - also have "\ = (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 "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" - by (rule div_add1_eq [symmetric]) - also have "\ = ((x+y+2)*Suc(x+y)) div 2" - by (simp only: add_mult_distrib [symmetric]) - also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2" - by (simp only: mult_le_mono div_le_mono) - also have "\ \ 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 \ x+y" by (rule nat2_to_nat_help) - also from eq1 [symmetric] have "x+y \ 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 "\x y. nat2_to_nat x = nat2_to_nat y \ 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 * (\i\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 \ "Max {r. (\i\r. i) \ z}" - def x \ "z - (\i\r. i)" - - hence "finite {r. (\i\r. i) \ z}" - by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub) - also have "0 \ {r. (\i\r. i) \ z}" by simp - hence "{r::nat. (\i\r. i) \ z} \ {}" by fast - ultimately have a: "r \ {r. (\i\r. i) \ z} \ (\s \ {r. (\i\r. i) \ z}. s \ r)" - by (simp add: r_def del:mem_Collect_eq) - { - assume "rx" by simp - hence "(\i\r. i)+(r+1)\z" using x_def by arith - hence "(r+1) \ {r. (\i\r. i) \ z}" by simp - with a have "(r+1)\r" by simp - } - hence b: "x\r" by force - - def y \ "r-x" - have "2*z=2*(\i\r. i)+2*x" using x_def a by simp arith - also have "\ = r * (r+1) + 2*x" using gauss_sum_nat_upto by simp - also have "\ = (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 "\ = 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 "\y. \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 "\"} and @{text "\"} *} - -definition nat_to_int_bij :: "nat \ 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 \ 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 \ 2 * m - Suc 0 \ 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 diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Nitpick.thy --- 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 \ bool) \ nat" where -"card' X \ length (SOME xs. set xs = X \ distinct xs)" +"card' A \ if finite A then length (safe_Eps (\xs. set xs = A \ distinct xs)) else 0" definition setsum' :: "('a \ 'b\comm_monoid_add) \ ('a \ bool) \ 'b" where -"setsum' f A \ if finite A then listsum (map f (SOME xs. set xs = A \ distinct xs)) else 0" +"setsum' f A \ if finite A then listsum (map f (safe_Eps (\xs. set xs = A \ distinct xs))) else 0" inductive fold_graph' :: "('a \ 'b \ 'b) \ 'b \ ('a \ bool) \ 'b \ bool" where "fold_graph' f z {} z" | diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Nitpick_Examples/Integer_Nits.thy --- 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} \ labels t \ labels u" + +lemma "labels (Node x t u) \ labels (Node y v w)" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = potential] +oops + +lemma "labels (Node x t u) \ {}" +nitpick [expect = none] +oops + +lemma "card (labels t) > 0" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = potential] +oops + +lemma "(\n \ labels t. n + 2) \ 2" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = potential] +oops + +lemma "t \ Null \ (\n \ labels t. n + 2) \ 2" +nitpick [expect = none] +nitpick [dont_finitize, expect = none] +sorry + +lemma "(\i \ labels (Node x t u). f i\nat) = f x + (\i \ labels t. f i) + (\i \ labels u. f i)" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = none] +oops + end diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Nitpick_Examples/Mini_Nits.thy --- 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 "\x\'a. \y\'b. f x = y"} *} - ML {* genuine 1 @{prop "x = Not"} *} ML {* none 1 @{prop "\x. x = Not"} *} ML {* none 1 @{prop "\ False"} *} diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Probability/Borel.thy --- 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 = (\x. if x \ s then 1 else (0::real))" -definition mono_convergent where - "mono_convergent u f s \ - (\x\s. incseq (\n. u n x)) \ - (\x \ s. (\i. u i x) ----> f x)" - lemma in_borel_measurable: "f \ borel_measurable M \ sigma_algebra M \ @@ -191,20 +186,20 @@ definition nat_to_rat_surj :: "nat \ 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 "\x. y = (\(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)" + show "\x. y = (\(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 \ s ==> f i \ borel_measurable M) \ (\x. setsum (\i. f i x) s) \ 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 "\ w. w \ space M \ f w = g w" + shows "f \ borel_measurable M \ g \ borel_measurable M" +using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong) + +lemma (in measure_space) borel_measurable_inverse: + assumes "f \ borel_measurable M" + shows "(\x. inverse (f x)) \ 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 \ inverse (f w) \ 0 < f w \ f w \ 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 \ space M. a \ inverse (f w)} = + {w \ space M. 0 < f w} \ {w \ space M. f w \ 1 / a}" by auto + with Int assms[unfolded borel_measurable_gr_iff] + assms[unfolded borel_measurable_le_iff] + show "{w \ space M. a \ inverse (f w)} \ sets M" by simp +next + fix a :: real assume "0 = a" + { fix w have "a \ inverse (f w) \ 0 \ f w" + unfolding `0 = a`[symmetric] by auto } + thus "{w \ space M. a \ inverse (f w)} \ 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 \ inverse (f w) \ f w \ 1 / a \ 0 \ f w" + apply (cases "0 \ 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 \ space M. a \ inverse (f w)} = + {w \ space M. f w \ 1 / a} \ {w \ space M. 0 \ f w}" by auto + with Un assms[unfolded borel_measurable_ge_iff] + assms[unfolded borel_measurable_le_iff] + show "{w \ space M. a \ inverse (f w)} \ sets M" by simp +qed + +lemma (in measure_space) borel_measurable_divide: + assumes "f \ borel_measurable M" + and "g \ borel_measurable M" + shows "(\x. f x / g x) \ 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 \ + (\x\s. incseq (\n. u n x)) \ + (\x \ s. (\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 \ s" + shows "incseq (\n. u n x)" and "(\i. u i x) ----> f x" + using assms unfolding mono_convergent_def by auto + +lemma mono_convergentI: + assumes "\x. x \ s \ incseq (\n. u n x)" + assumes "\x. x \ s \ (\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 \ 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 \ s ==> f i \ borel_measurable M) \ (\x. setsum (\i. f i x) s) \ 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 \ s" - shows "incseq (\n. u n x)" and "(\i. u i x) ----> f x" - using assms unfolding mono_convergent_def by auto - - -lemma mono_convergentI: - assumes "\x. x \ s \ incseq (\n. u n x)" - assumes "\x. x \ s \ (\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 \ s" shows "u n t \ 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 \ 'a \ ('b\linorder)" shows "\n \ 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 "\b. \ a \ b. z < x a" +using assms +proof - + from assms have "y - z > 0" by simp + hence A: "\n. (\ m \ n. \ x m + - y \ < y - z)" using assms + unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def + by simp + have "\m. x m \ y" using incseq_le assms by auto + hence B: "\m. \ x m + - y \ = 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 diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Probability/Caratheodory.thy --- 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 \ "(split BB) o nat_to_nat2" + def C \ "(split BB) o prod_decode" have C: "!!n. C n \ 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 \ A i" with sbBB [of i] obtain j where "x \ BB i j" by blast - thus "\i. x \ 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 "\i. x \ split BB (prod_decode i)" + by (metis prod_encode_inverse prod.cases prod_case_split) qed - have "(f \ C) = (f \ (\(x, y). BB x y)) \ nat_to_nat2" + have "(f \ C) = (f \ (\(x, y). BB x y)) \ prod_decode" by (rule ext) (auto simp add: C_def) also have "... sums suminf ll" proof (rule suminf_2dimen) diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Probability/Lebesgue.thy --- 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 \ borel_measurable M" + shows pos_part_borel_measurable: "pos_part f \ borel_measurable M" + and neg_part_borel_measurable: "neg_part f \ borel_measurable M" +using assms +proof - + { fix a :: real + { assume asm: "0 \ a" + from asm have pp: "\ w. (pos_part f w \ a) = (f w \ a)" unfolding pos_part_def by auto + have "{w | w. w \ space M \ f w \ a} \ sets M" + unfolding pos_part_def using assms borel_measurable_le_iff by auto + hence "{w . w \ space M \ pos_part f w \ a} \ sets M" using pp by auto } + moreover have "a < 0 \ {w \ space M. pos_part f w \ a} \ sets M" + unfolding pos_part_def using empty_sets by auto + ultimately have "{w . w \ space M \ pos_part f w \ a} \ sets M" + using le_less_linear by auto + } hence pos: "pos_part f \ borel_measurable M" using borel_measurable_le_iff by auto + { fix a :: real + { assume asm: "0 \ a" + from asm have pp: "\ w. (neg_part f w \ a) = (f w \ - a)" unfolding neg_part_def by auto + have "{w | w. w \ space M \ f w \ - a} \ sets M" + unfolding neg_part_def using assms borel_measurable_ge_iff by auto + hence "{w . w \ space M \ neg_part f w \ a} \ sets M" using pp by auto } + moreover have "a < 0 \ {w \ space M. neg_part f w \ a} = {}" unfolding neg_part_def by auto + moreover hence "a < 0 \ {w \ space M. neg_part f w \ a} \ sets M" by (simp only: empty_sets) + ultimately have "{w . w \ space M \ neg_part f w \ a} \ sets M" + using le_less_linear by auto + } hence neg: "neg_part f \ borel_measurable M" using borel_measurable_le_iff by auto + from pos neg show "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" by auto +qed + +lemma (in measure_space) pos_part_neg_part_borel_measurable_iff: + "f \ borel_measurable M \ + pos_part f \ borel_measurable M \ neg_part f \ 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 "(\ x. f x) = (\ x. pos_part f x - neg_part f x)" by auto + hence "f = (\ 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. \u x. mono_convergent u f (space M) \ - (\n. x n \ psfis (u n)) \ x ----> y }" - -definition - "integrable f \ (\x. x \ nnfis (pos_part f)) \ (\y. y \ nnfis (neg_part f))" - -definition - "integral f = (THE i :: real. i \ nnfis (pos_part f)) - (THE j. j \ nnfis (neg_part f))" - -definition - "enumerate s \ SOME f. bij_betw f UNIV s" - -definition - "countable_space_integral f \ - let e = enumerate (f ` space M) in - suminf (\r. e r * measure M (f -` {e r} \ space M))" - -definition - "RN_deriv v \ SOME f. measure_space (M\measure := v\) \ - f \ borel_measurable M \ - (\a \ sets M. (integral (\x. f x * indicator_fn a x) = v a))" - lemma pos_simpleE[consumes 1]: assumes ps: "(s, a, x) \ 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 \ psfis (\x. 0)" + unfolding psfis_def pos_simple_def pos_simple_integral_def + by (auto simp: nonneg_def + intro: image_eqI[where x="({0}, (\i. space M), (\i. 0))"]) + lemma pos_simple_setsum_indicator_fn: assumes ps: "(s, a, x) \ pos_simple f" and "t \ space M" @@ -121,28 +152,7 @@ using `i \ s` by simp qed -lemma (in measure_space) measure_setsum_split: - assumes "finite r" and "a \ sets M" and br_in_M: "b ` r \ sets M" - assumes "(\i \ r. b i) = space M" - assumes "disjoint_family_on b r" - shows "(measure M) a = (\ i \ r. measure M (a \ (b i)))" -proof - - have *: "measure M a = measure M (\i \ r. a \ 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 \ r" - hence "b i \ sets M" using br_in_M by auto - thus "a \ b i \ sets M" using `a \ sets M` by auto - } - show "disjoint_family_on (\i. a \ 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) \ pos_simple f" assumes psg: "(s', b, y) \ pos_simple g" obtains z z' c k where "(k, c, z) \ pos_simple f" "(k, c, z') \ 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) \ pos_simple f" assumes psy: "(s', b, y) \ 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 \ psfis f" assumes "B \ 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) \ pos_simple f" assumes "(s', b, y) \ 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 "\ i. i \ P \ (s i, a i, x i) \ pos_simple (f i)" - obtains s' a' x' where - "(s', a', x') \ pos_simple (\t. (\ i \ P. f i t))" - "pos_simple_integral (s', a', x') = (\ i \ 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' == "\ x. if x = (0 :: nat) then space M else {}" - def x' == "\ x :: nat. (0 :: real)" - have "(s', a', x') \ pos_simple (\ 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') \ pos_simple (\t. \i\P. f i t)" - "pos_simple_integral (s', a', x') = - (\i\P. pos_simple_integral (s i, a i, x i))" - by auto - - { assume "c \ P" - hence "P = insert c P" by auto - hence thesis using asms sax by auto - } - moreover - { assume "c \ P" - from asms obtain s'' a'' x'' where - sax': "s'' = s c" "a'' = a c" "x'' = x c" - "(s'', a'', x'') \ pos_simple (f c)" by auto - from sax sax' obtain k :: "nat \ bool" and b :: "nat \ 'a \ bool" and z :: "nat \ real" where - tybbie: - "(k, b, z) \ pos_simple (\t. ((\i\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 "\ = (\ i \ 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 "\ = (\ i \ insert c P. pos_simple_integral (s i, a i, x i))" - using asms `c \ P` by auto - finally have A: "pos_simple_integral (k, b, z) = (\ i \ insert c P. pos_simple_integral (s i, a i, x i))" - by simp - - have "\ t. (\ i \ P. f i t) + f c t = (\ i \ insert c P. f i t)" - using `c \ P` `finite P` by auto - hence B: "(k, b, z) \ pos_simple (\ t. (\ i \ 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 "\i. i \ P \ a i \ 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 \ borel_measurable M" - shows "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" -using assms -proof - - { fix a :: real - { assume asm: "0 \ a" - from asm have pp: "\ w. (pos_part f w \ a) = (f w \ a)" unfolding pos_part_def by auto - have "{w | w. w \ space M \ f w \ a} \ sets M" - unfolding pos_part_def using assms borel_measurable_le_iff by auto - hence "{w . w \ space M \ pos_part f w \ a} \ sets M" using pp by auto } - moreover have "a < 0 \ {w \ space M. pos_part f w \ a} \ sets M" - unfolding pos_part_def using empty_sets by auto - ultimately have "{w . w \ space M \ pos_part f w \ a} \ sets M" - using le_less_linear by auto - } hence pos: "pos_part f \ borel_measurable M" using borel_measurable_le_iff by auto - { fix a :: real - { assume asm: "0 \ a" - from asm have pp: "\ w. (neg_part f w \ a) = (f w \ - a)" unfolding neg_part_def by auto - have "{w | w. w \ space M \ f w \ - a} \ sets M" - unfolding neg_part_def using assms borel_measurable_ge_iff by auto - hence "{w . w \ space M \ neg_part f w \ a} \ sets M" using pp by auto } - moreover have "a < 0 \ {w \ space M. neg_part f w \ a} = {}" unfolding neg_part_def by auto - moreover hence "a < 0 \ {w \ space M. neg_part f w \ a} \ sets M" by (simp only: empty_sets) - ultimately have "{w . w \ space M \ neg_part f w \ a} \ sets M" - using le_less_linear by auto - } hence neg: "neg_part f \ borel_measurable M" using borel_measurable_le_iff by auto - from pos neg show "pos_part f \ borel_measurable M" and "neg_part f \ borel_measurable M" by auto -qed - -lemma pos_part_neg_part_borel_measurable_iff: - "f \ borel_measurable M \ - pos_part f \ borel_measurable M \ neg_part f \ 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 "(\ x. f x) = (\ x. pos_part f x - neg_part f x)" by auto - hence "f = (\ 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 "\ w. w \ space M \ f w = g w" - shows "f \ borel_measurable M \ g \ borel_measurable M" -using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong) - lemma psfis_borel_measurable: assumes "a \ psfis f" shows "f \ borel_measurable M" @@ -654,21 +549,6 @@ show ?thesis by simp qed -lemma mono_conv_outgrow: - assumes "incseq x" "x ----> y" "z < y" - shows "\b. \ a \ b. z < x a" -using assms -proof - - from assms have "y - z > 0" by simp - hence A: "\n. (\ m \ n. \ x m + - y \ < y - z)" using assms - unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def - by simp - have "\m. x m \ y" using incseq_le assms by auto - hence B: "\m. \ x m + - y \ = 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: "\n. x n \ 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 \ z" by auto -(* def B' \ "\n. {w \ space M. z * s w <= u n w}" *) let "?B' n" = "{w \ 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. \u x. mono_convergent u f (space M) \ + (\n. x n \ psfis (u n)) \ x ----> y }" + lemma psfis_nnfis: "a \ psfis f \ a \ 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 \ psfis (\x. 0)" - unfolding psfis_def pos_simple_def pos_simple_integral_def - by (auto simp: nonneg_def - intro: image_eqI[where x="({0}, (\i. space M), (\i. 0))"]) - lemma the_nnfis[simp]: "a \ nnfis f \ (THE a. a \ 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 \ (\x. x \ nnfis (pos_part f)) \ (\y. y \ nnfis (neg_part f))" + +definition + "integral f = (THE i :: real. i \ nnfis (pos_part f)) - (THE j. j \ nnfis (neg_part f))" + lemma integral_cong: assumes cong: "\x. x \ space M \ f x = g x" shows "integral f = integral g" @@ -1203,7 +1091,7 @@ (is "\x. x \ nnfis ?pp \ _") proof (rule nnfis_dom_conv) show "?pp \ 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 \ nnfis (\t. f t + g t)" using assms by (rule nnfis_add) fix t assume "t \ space M" with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]] @@ -1217,7 +1105,7 @@ (is "\x. x \ nnfis ?np \ _") proof (rule nnfis_dom_conv) show "?np \ 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 \ nnfis (\t. f t + g t)" using assms by (rule nnfis_add) fix t assume "t \ 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 \ borel_measurable M" and "finite (space M)" and "a \ sets M" shows "integral (\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 \ borel_measurable M" - shows "(\x. inverse (f x)) \ 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 \ inverse (f w) \ 0 < f w \ f w \ 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 \ space M. a \ inverse (f w)} = - {w \ space M. 0 < f w} \ {w \ space M. f w \ 1 / a}" by auto - with Int assms[unfolded borel_measurable_gr_iff] - assms[unfolded borel_measurable_le_iff] - show "{w \ space M. a \ inverse (f w)} \ sets M" by simp -next - fix a :: real assume "0 = a" - { fix w have "a \ inverse (f w) \ 0 \ f w" - unfolding `0 = a`[symmetric] by auto } - thus "{w \ space M. a \ inverse (f w)} \ 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 \ inverse (f w) \ f w \ 1 / a \ 0 \ f w" - apply (cases "0 \ 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 \ space M. a \ inverse (f w)} = - {w \ space M. f w \ 1 / a} \ {w \ space M. 0 \ f w}" by auto - with Un assms[unfolded borel_measurable_ge_iff] - assms[unfolded borel_measurable_le_iff] - show "{w \ space M. a \ inverse (f w)} \ sets M" by simp -qed +section "Radon–Nikodym derivative" -lemma borel_measurable_divide: - assumes "f \ borel_measurable M" - and "g \ borel_measurable M" - shows "(\x. f x / g x) \ borel_measurable M" - unfolding field_divide_inverse - by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+ +definition + "RN_deriv v \ SOME f. measure_space (M\measure := v\) \ + f \ borel_measurable M \ + (\a \ sets M. (integral (\x. f x * indicator_fn a x) = v a))" lemma RN_deriv_finite_singleton: fixes v :: "'a set \ real" @@ -1577,6 +1428,11 @@ using `measure M {x} \ 0` by (simp add: eq_divide_eq) qed fact +section "Lebesgue integration on countable spaces" + +definition + "enumerate s \ SOME f. bij_betw f UNIV s" + lemma countable_space_integral_reduce: assumes "positive M (measure M)" and "f \ borel_measurable M" and "countable (f ` space M)" diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Probability/Measure.thy --- 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 @@ \ 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 \ sets M" and br_in_M: "b ` r \ sets M" + assumes "(\i \ r. b i) = space M" + assumes "disjoint_family_on b r" + shows "(measure M) a = (\ i \ r. measure M (a \ (b i)))" +proof - + have *: "measure M a = measure M (\i \ r. a \ 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 \ r" + hence "b i \ sets M" using br_in_M by auto + thus "a \ b i \ sets M" using `a \ sets M` by auto + } + show "disjoint_family_on (\i. a \ 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 diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Probability/SeriesPlus.thy --- 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 \ f(m,n)" and fsums: "!!m. (\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 \ g m" using fsums [of m] by (auto simp add: sums_iff) qed - show "(\n. \x = 0.. suminf g" + show "(\n. \x = 0.. suminf g" proof (rule increasing_LIMSEQ, simp add: f_nneg) fix n - def i \ "Max (Domain (nat_to_nat2 ` {0.. "Max (Range (nat_to_nat2 ` {0.. ({0..i} \ {0..j})" + def i \ "Max (Domain (prod_decode ` {0.. "Max (Range (prod_decode ` {0.. ({0..i} \ {0..j})" by (force simp add: i_def j_def intro: finite_imageI Max_ge finite_Domain finite_Range) - have "(\x = 0..x = 0.. setsum f ({0..i} \ {0..j})" by (rule setsum_mono2) (auto simp add: ij) also have "... = setsum (\m. setsum (\n. f (m,n)) {0..j}) {0..x = 0.. setsum g {0..x = 0.. setsum g {0.. suminf g" by (rule series_pos_le [OF sumg]) (simp add: g_nneg) - finally show "(\x = 0.. suminf g" . + finally show "(\x = 0.. 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 \ "Max (nat_to_nat2 -` IJ)" - have IJsb: "IJ \ nat_to_nat2 ` {0..NIJ}" + def NIJ \ "Max (prod_decode -` IJ)" + have IJsb: "IJ \ prod_decode ` {0..NIJ}" proof (auto simp add: NIJ_def) fix i j assume ij:"(i,j) \ 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) \ nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}" + hence "(i,j) = prod_decode (prod_encode (i,j))" + by simp + thus "(i,j) \ 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 \ setsum f (nat_to_nat2 `{0..NIJ})" + have "setsum f IJ \ setsum f (prod_decode `{0..NIJ})" by (rule setsum_mono2) (auto simp add: IJsb) - also have "... = (\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 "... = (\k = 0..k = 0..NIJ. f (prod_decode k))" + by (simp add: setsum_reindex inj_prod_decode) + also have "... = (\k = 0.. (\k = 0..n. suminf g \ (\x = 0.. (\k = 0..n. suminf g \ (\x = 0.. 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 diff -r 5e5925871d6f -r 267e15230a31 src/HOL/SET_Protocol/Purchase.thy --- 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 \ 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] diff -r 5e5925871d6f -r 267e15230a31 src/HOL/SET_Protocol/ROOT.ML --- 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"]; diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Tools/Nitpick/HISTORY --- 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" diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Tools/Nitpick/kodkod.ML --- 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 diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Tools/Nitpick/minipick.ML --- 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" diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Tools/Nitpick/nitpick.ML --- 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.") diff -r 5e5925871d6f -r 267e15230a31 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 = diff -r 5e5925871d6f -r 267e15230a31 src/HOLCF/IsaMakefile --- 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 \ diff -r 5e5925871d6f -r 267e15230a31 src/HOLCF/NatIso.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 \ nat" -where - "sum2nat (Inl a) = a + a" -| "sum2nat (Inr b) = Suc (b + b)" - -primrec - nat2sum :: "nat \ nat + nat" -where - "nat2sum 0 = Inl 0" -| "nat2sum (Suc n) = (case nat2sum n of - Inl a \ Inr a | Inr b \ 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 \ 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 \ 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 \ nat \ 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) (\(x, y). (x+y, x))") auto - -primrec - nat2prod :: "nat \ nat \ nat" -where - "nat2prod 0 = (0, 0)" -| "nat2prod (Suc x) = - (case nat2prod x of (m, n) \ - (case n of 0 \ (0, Suc m) | Suc n \ (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 \ 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 \ x = y" -by (rule inj_nat2prod [THEN inj_eq]) - -subsubsection {* Ordering properties *} - -lemma fst_snd_le_prod2nat: "fst x \ prod2nat x \ snd x \ prod2nat x" -by (induct x rule: prod2nat.induct) auto - -lemma fst_le_prod2nat: "fst x \ prod2nat x" -by (rule fst_snd_le_prod2nat [THEN conjunct1]) - -lemma snd_le_prod2nat: "snd x \ prod2nat x" -by (rule fst_snd_le_prod2nat [THEN conjunct2]) - -lemma le_prod2nat_1: "a \ prod2nat (a, b)" -using fst_le_prod2nat [where x="(a, b)"] by simp - -lemma le_prod2nat_2: "b \ 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) \ 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 \ 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: - "\x div 2 = y div 2; even x = even y\ \ (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 \ nat" where - "set2nat = setsum (op ^ 2)" - -lemma set2nat_empty [simp]: "set2nat {} = 0" -by (simp add: set2nat_def) - -lemma set2nat_insert [simp]: - "\finite A; n \ A\ \ set2nat (insert n A) = 2^n + set2nat A" -by (simp add: set2nat_def) - -lemma even_set2nat_iff: "finite A \ even (set2nat A) = (0 \ 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 \ nat set" where - "nat2set x = {n. odd (x div 2 ^ n)}" - -lemma nat2set_0 [simp]: "0 \ nat2set x \ odd x" -by (simp add: nat2set_def) - -lemma nat2set_Suc [simp]: - "Suc n \ nat2set x \ n \ 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 \ nat2set z \ 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 \ 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 \ 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]: - "\finite A; finite B\ \ set2nat A = set2nat B \ 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: "\finite A; x \ A\ \ 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 diff -r 5e5925871d6f -r 267e15230a31 src/HOLCF/ROOT.ML --- 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"]; diff -r 5e5925871d6f -r 267e15230a31 src/HOLCF/Universal.thy --- 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 \ ubasis \ ubasis set \ 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 \ 0" unfolding node_def by simp @@ -24,30 +24,30 @@ lemma node_inject [simp]: "\finite S; finite T\ \ node i a S = node j b T \ i = j \ a = b \ 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: "\finite S; b \ S\ \ 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: - "\fst (nat2prod x) = a; snd (nat2prod x) = b\ \ x = prod2nat (a, b)" +lemma eq_prod_encode_pairI: + "\fst (prod_decode x) = a; snd (prod_decode x) = b\ \ 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: diff -r 5e5925871d6f -r 267e15230a31 src/Provers/Arith/fast_lin_arith.ML --- 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 =