# HG changeset patch # User wenzelm # Date 1481560806 -3600 # Node ID 628b271c5b8bc8843cf43b6a36cac870ff4be167 # Parent 134ae7da2ccf29c1a6cb4008163868bc3d4ccb52# Parent 5d2cef77373c064ea204a15799e2e46be04eed3b merged diff -r 5d2cef77373c -r 628b271c5b8b Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon Dec 12 16:54:15 2016 +0100 +++ b/Admin/components/components.sha1 Mon Dec 12 17:40:06 2016 +0100 @@ -138,6 +138,7 @@ 5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz 5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz 853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz +c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz 8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz 8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz diff -r 5d2cef77373c -r 628b271c5b8b Admin/cronjob/self_update --- a/Admin/cronjob/self_update Mon Dec 12 16:54:15 2016 +0100 +++ b/Admin/cronjob/self_update Mon Dec 12 17:40:06 2016 +0100 @@ -10,5 +10,5 @@ cd "$HOME/cronjob" mkdir -p run log -hg -R isabelle pull "http://bitbucket.org/isabelle_project/isabelle-release" -q || echo "self_update pull failed" +hg -R isabelle pull "http://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed" hg -R isabelle update -C -q || echo "self_update update failed" diff -r 5d2cef77373c -r 628b271c5b8b Admin/polyml/README --- a/Admin/polyml/README Mon Dec 12 16:54:15 2016 +0100 +++ b/Admin/polyml/README Mon Dec 12 17:40:06 2016 +0100 @@ -1,32 +1,27 @@ Poly/ML for Isabelle ==================== -This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source -distribution from https://github.com/polyml/polyml/releases/tag/v5.6/. +This compilation of Poly/ML (http://www.polyml.org) is based on the repository +version https://github.com/polyml/polyml/commit/8529546198aa -On Linux the sources have changed as follows, in order to evade a -potential conflict of /bin/bash versus /bin/sh -> dash (notably on -Ubuntu and Debian): +The Isabelle repository provides the administrative tool "build_polyml", which +can be used in the polyml component directory as follows. -diff -r src-orig/libpolyml/process_env.cpp src/libpolyml/process_env.cpp -228c228 -< execve("/bin/sh", argv, environ); ---- -> execvp("bash", argv); +* Linux: + isabelle build_polyml -m32 -s sha1 src --with-gmp + isabelle build_polyml -m64 -s sha1 src --with-gmp -The included build script is used like this: +* Mac OS X: - ./build src x86-linux --with-gmp - ./build src x86_64-linux --with-gmp - ./build src x86-darwin --without-gmp - ./build src x86_64-darwin --without-gmp - ./build src x86-windows --with-gmp - ./build src x86_64-windows --with-gmp + isabelle build_polyml -m32 -s sha1 src --without-gmp + isabelle build_polyml -m64 -s sha1 src --without-gmp -Also note that the separate "sha1" library module is required for -efficient digestion of strings according to SHA-1. +* Windows (Cygwin shell) + + isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src --with-gmp + isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src --with-gmp Makarius - 11-Feb-2016 + 10-Dec-2016 diff -r 5d2cef77373c -r 628b271c5b8b Admin/polyml/build --- a/Admin/polyml/build Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -#!/usr/bin/env bash -# -# Multi-platform build script for Poly/ML - -THIS="$(cd "$(dirname "$0")"; pwd)" -PRG="$(basename "$0")" - - -# diagnostics - -function usage() -{ - echo - echo "Usage: $PRG SOURCE TARGET [OPTIONS]" - echo - echo " Build Poly/ML in SOURCE directory for given platform in TARGET," - echo " using the usual Isabelle platform identifiers." - echo - echo " Additional options for ./configure may be given, e.g. --with-gmp" - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -# command line args - -[ "$#" -eq 0 ] && usage -SOURCE="$1"; shift - -[ "$#" -eq 0 ] && usage -TARGET="$1"; shift - -USER_OPTIONS=("$@") - - -# main - -[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\"" - -case "$TARGET" in - x86-linux) - OPTIONS=() - ;; - x86_64-linux) - OPTIONS=() - ;; - x86-darwin) - OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3 -I../libffi/include' - CXXFLAGS='-arch i686 -O3 -I../libffi/include' CCASFLAGS='-arch i686 -O3' - LDFLAGS='-segprot POLY rwx rwx') - ;; - x86_64-darwin) - OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3 -I../libffi/include' - CXXFLAGS='-arch x86_64 -O3 -I../libffi/include' CCASFLAGS='-arch x86_64' - LDFLAGS='-segprot POLY rwx rwx') - ;; - x86-cygwin) - OPTIONS=() - ;; - x86-windows) - OPTIONS=(--host=i686-w32-mingw32 CPPFLAGS='-I/mingw32/include' --disable-windows-gui) - PATH="/mingw32/bin:$PATH" - ;; - x86_64-windows) - OPTIONS=(--host=x86_64-w64-mingw32 CPPFLAGS='-I/mingw64/include' --disable-windows-gui) - PATH="/mingw64/bin:$PATH" - ;; - *) - fail "Bad platform identifier: \"$TARGET\"" - ;; -esac - -( - cd "$SOURCE" - make distclean - - { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" --enable-intinf-as-int "${USER_OPTIONS[@]}" && \ - make compiler && \ - make compiler && \ - make install; } || fail "Build failed" -) - -mkdir -p "$TARGET" -for X in "$TARGET"/* -do - [ -d "$X" ] && rm -rf "$X" -done -rm -rf "$TARGET/polyml" -cp -a "$THIS/polyi" "$TARGET/" -mv "$SOURCE/$TARGET/bin/"* "$TARGET/" -mv "$SOURCE/$TARGET/lib/"* "$TARGET/" -rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib" -rm -rf "$SOURCE/$TARGET/share" - -case "$TARGET" in - x86-cygwin) - peflags -x8192000 -z500 "$TARGET/poly.exe" - ;; - x86-windows) - for X in libgcc_s_dw2-1.dll libgmp-10.dll libstdc++-6.dll - do - cp "/mingw32/bin/$X" "$TARGET/." - done - ;; - x86_64-windows) - for X in libgcc_s_seh-1.dll libgmp-10.dll libstdc++-6.dll - do - cp "/mingw64/bin/$X" "$TARGET/." - done - ;; -esac diff -r 5d2cef77373c -r 628b271c5b8b Admin/polyml/settings --- a/Admin/polyml/settings Mon Dec 12 16:54:15 2016 +0100 +++ b/Admin/polyml/settings Mon Dec 12 17:40:06 2016 +0100 @@ -36,12 +36,12 @@ do if [ -z "$ML_HOME" ] then - if "$POLYML_HOME/$PLATFORM/polyml" -v /dev/null 2>/dev/null + if "$POLYML_HOME/$PLATFORM/polyi" -v /dev/null 2>/dev/null then # ML settings - ML_SYSTEM=polyml-5.6 + ML_SYSTEM=polyml-5.7 ML_PLATFORM="$PLATFORM" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_SOURCES="$POLYML_HOME/src" diff -r 5d2cef77373c -r 628b271c5b8b CONTRIBUTORS --- a/CONTRIBUTORS Mon Dec 12 16:54:15 2016 +0100 +++ b/CONTRIBUTORS Mon Dec 12 17:40:06 2016 +0100 @@ -3,6 +3,10 @@ listed as an author in one of the source files of this Isabelle distribution. +Contributions to this Isabelle version +-------------------------------------- + + Contributions to Isabelle2016-1 ------------------------------- diff -r 5d2cef77373c -r 628b271c5b8b NEWS --- a/NEWS Mon Dec 12 16:54:15 2016 +0100 +++ b/NEWS Mon Dec 12 17:40:06 2016 +0100 @@ -3,6 +3,17 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) +New in this Isabelle version +---------------------------- + +* (Co)datatype package: + - The 'size_gen_o_map' lemma is no longer generated for datatypes + with type class annotations. As a result, the tactic that derives + it no longer fails on nested datatypes. Slight INCOMPATIBILITY. + +* The theorem in Permutations has been renamed: + bij_swap_ompose_bij ~> bij_swap_compose_bij + New in Isabelle2016-1 (December 2016) ------------------------------------- diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Analysis/Summation_Tests.thy --- a/src/HOL/Analysis/Summation_Tests.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Analysis/Summation_Tests.thy Mon Dec 12 17:40:06 2016 +0100 @@ -7,6 +7,7 @@ theory Summation_Tests imports Complex_Main + "~~/src/HOL/Library/Discrete" "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Liminf_Limsup" begin @@ -16,89 +17,6 @@ various summability tests, lemmas to compute the radius of convergence etc. \ -subsection \Rounded dual logarithm\ - -(* This is required for the Cauchy condensation criterion *) - -definition "natlog2 n = (if n = 0 then 0 else nat \log 2 (real_of_nat n)\)" - -lemma natlog2_0 [simp]: "natlog2 0 = 0" by (simp add: natlog2_def) -lemma natlog2_1 [simp]: "natlog2 1 = 0" by (simp add: natlog2_def) -lemma natlog2_eq_0_iff: "natlog2 n = 0 \ n < 2" by (simp add: natlog2_def) - -lemma natlog2_power_of_two [simp]: "natlog2 (2 ^ n) = n" - by (simp add: natlog2_def log_nat_power) - -lemma natlog2_mono: "m \ n \ natlog2 m \ natlog2 n" - unfolding natlog2_def by (simp_all add: nat_mono floor_mono) - -lemma pow_natlog2_le: "n > 0 \ 2 ^ natlog2 n \ n" -proof - - assume n: "n > 0" - from n have "of_nat (2 ^ natlog2 n) = 2 powr real_of_nat (nat \log 2 (real_of_nat n)\)" - by (subst powr_realpow) (simp_all add: natlog2_def) - also have "\ = 2 powr of_int \log 2 (real_of_nat n)\" using n by simp - also have "\ \ 2 powr log 2 (real_of_nat n)" by (intro powr_mono) (linarith, simp_all) - also have "\ = of_nat n" using n by simp - finally show ?thesis by simp -qed - -lemma pow_natlog2_gt: "n > 0 \ 2 * 2 ^ natlog2 n > n" - and pow_natlog2_ge: "n > 0 \ 2 * 2 ^ natlog2 n \ n" -proof - - assume n: "n > 0" - from n have "of_nat n = 2 powr log 2 (real_of_nat n)" by simp - also have "\ < 2 powr (1 + of_int \log 2 (real_of_nat n)\)" - by (intro powr_less_mono) (linarith, simp_all) - also from n have "\ = 2 powr (1 + real_of_nat (nat \log 2 (real_of_nat n)\))" by simp - also from n have "\ = of_nat (2 * 2 ^ natlog2 n)" - by (simp_all add: natlog2_def powr_real_of_int powr_add) - finally show "2 * 2 ^ natlog2 n > n" by (rule of_nat_less_imp_less) - thus "2 * 2 ^ natlog2 n \ n" by simp -qed - -lemma natlog2_eqI: - assumes "n > 0" "2^k \ n" "n < 2 * 2^k" - shows "natlog2 n = k" -proof - - from assms have "of_nat (2 ^ k) \ real_of_nat n" by (subst of_nat_le_iff) simp_all - hence "real_of_int (int k) \ log (of_nat 2) (real_of_nat n)" - by (subst le_log_iff) (simp_all add: powr_realpow assms del: of_nat_le_iff) - moreover from assms have "real_of_nat n < of_nat (2 ^ Suc k)" by (subst of_nat_less_iff) simp_all - hence "log 2 (real_of_nat n) < of_nat k + 1" - by (subst log_less_iff) (simp_all add: assms powr_realpow powr_add) - ultimately have "\log 2 (real_of_nat n)\ = of_nat k" by (intro floor_unique) simp_all - with assms show ?thesis by (simp add: natlog2_def) -qed - -lemma natlog2_rec: - assumes "n \ 2" - shows "natlog2 n = 1 + natlog2 (n div 2)" -proof (rule natlog2_eqI) - from assms have "2 ^ (1 + natlog2 (n div 2)) \ 2 * (n div 2)" - by (simp add: pow_natlog2_le) - also have "\ \ n" by simp - finally show "2 ^ (1 + natlog2 (n div 2)) \ n" . -next - from assms have "n < 2 * (n div 2 + 1)" by simp - also from assms have "(n div 2) < 2 ^ (1 + natlog2 (n div 2))" - by (simp add: pow_natlog2_gt) - hence "2 * (n div 2 + 1) \ 2 * (2 ^ (1 + natlog2 (n div 2)))" - by (intro mult_left_mono) simp_all - finally show "n < 2 * 2 ^ (1 + natlog2 (n div 2))" . -qed (insert assms, simp_all) - -fun natlog2_aux where - "natlog2_aux n acc = (if (n::nat) < 2 then acc else natlog2_aux (n div 2) (acc + 1))" - -lemma natlog2_aux_correct: - "natlog2_aux n acc = acc + natlog2 n" - by (induction n acc rule: natlog2_aux.induct) (auto simp: natlog2_rec natlog2_eq_0_iff) - -lemma natlog2_code [code]: "natlog2 n = natlog2_aux n 0" - by (subst natlog2_aux_correct) simp - - subsection \Convergence tests for infinite sums\ subsubsection \Root test\ @@ -216,33 +134,33 @@ private lemma condensation_inequality: assumes mono: "\m n. 0 < m \ m \ n \ f n \ f m" - shows "(\k=1.. (\k=1..k=1.. (\k=1..k=1.. (\k=1..k=1.. (\k=1..k=1..<2^n. f (2 ^ natlog2 k)) = (\kk=1..<2^n. f (2 ^ Discrete.log k)) = (\k {2^n..<(2^Suc n :: nat)}" by auto - also have "(\k\\. f (2 ^ natlog2 k)) = - (\kk = 2^n..<2^Suc n. f (2^natlog2 k))" + also have "(\k\\. f (2 ^ Discrete.log k)) = + (\kk = 2^n..<2^Suc n. f (2^Discrete.log k))" by (subst sum.union_disjoint) (insert Suc, auto) - also have "natlog2 k = n" if "k \ {2^n..<2^Suc n}" for k using that by (intro natlog2_eqI) simp_all - hence "(\k = 2^n..<2^Suc n. f (2^natlog2 k)) = (\(_::nat) = 2^n..<2^Suc n. f (2^n))" + also have "Discrete.log k = n" if "k \ {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all + hence "(\k = 2^n..<2^Suc n. f (2^Discrete.log k)) = (\(_::nat) = 2^n..<2^Suc n. f (2^n))" by (intro sum.cong) simp_all also have "\ = 2^n * f (2^n)" by (simp add: of_nat_power) finally show ?case by simp qed simp -private lemma condensation_condense2: "(\k=1..<2^n. f (2 * 2 ^ natlog2 k)) = (\kk=1..<2^n. f (2 * 2 ^ Discrete.log k)) = (\k {2^n..<(2^Suc n :: nat)}" by auto - also have "(\k\\. f (2 * 2 ^ natlog2 k)) = - (\kk = 2^n..<2^Suc n. f (2 * 2^natlog2 k))" + also have "(\k\\. f (2 * 2 ^ Discrete.log k)) = + (\kk = 2^n..<2^Suc n. f (2 * 2^Discrete.log k))" by (subst sum.union_disjoint) (insert Suc, auto) - also have "natlog2 k = n" if "k \ {2^n..<2^Suc n}" for k using that by (intro natlog2_eqI) simp_all - hence "(\k = 2^n..<2^Suc n. f (2*2^natlog2 k)) = (\(_::nat) = 2^n..<2^Suc n. f (2^Suc n))" + also have "Discrete.log k = n" if "k \ {2^n..<2^Suc n}" for k using that by (intro Discrete.log_eqI) simp_all + hence "(\k = 2^n..<2^Suc n. f (2*2^Discrete.log k)) = (\(_::nat) = 2^n..<2^Suc n. f (2^Suc n))" by (intro sum.cong) simp_all also have "\ = 2^n * f (2^Suc n)" by (simp add: of_nat_power) finally show ?case by simp diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Dec 12 17:40:06 2016 +0100 @@ -29,8 +29,7 @@ by auto definition (in monoid_add) support_on :: "'b set \ ('b \ 'a) \ 'b set" -where - "support_on s f = {x\s. f x \ 0}" + where "support_on s f = {x\s. f x \ 0}" lemma in_support_on: "x \ support_on s f \ x \ s \ f x \ 0" by (simp add: support_on_def) @@ -60,8 +59,7 @@ (* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) definition (in comm_monoid_add) supp_sum :: "('b \ 'a) \ 'b set \ 'a" -where - "supp_sum f s = (\x\support_on s f. f x)" + where "supp_sum f s = (\x\support_on s f. f x)" lemma supp_sum_empty[simp]: "supp_sum f {} = 0" unfolding supp_sum_def by auto @@ -1029,33 +1027,27 @@ lemma sphere_trivial [simp]: "sphere x 0 = {x}" by (simp add: sphere_def) -lemma mem_ball_0 [simp]: - fixes x :: "'a::real_normed_vector" - shows "x \ ball 0 e \ norm x < e" +lemma mem_ball_0 [simp]: "x \ ball 0 e \ norm x < e" + for x :: "'a::real_normed_vector" by (simp add: dist_norm) -lemma mem_cball_0 [simp]: - fixes x :: "'a::real_normed_vector" - shows "x \ cball 0 e \ norm x \ e" +lemma mem_cball_0 [simp]: "x \ cball 0 e \ norm x \ e" + for x :: "'a::real_normed_vector" by (simp add: dist_norm) -lemma disjoint_ballI: - shows "dist x y \ r+s \ ball x r \ ball y s = {}" +lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}" using dist_triangle_less_add not_le by fastforce -lemma disjoint_cballI: - shows "dist x y > r+s \ cball x r \ cball y s = {}" +lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}" by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball) -lemma mem_sphere_0 [simp]: - fixes x :: "'a::real_normed_vector" - shows "x \ sphere 0 e \ norm x = e" +lemma mem_sphere_0 [simp]: "x \ sphere 0 e \ norm x = e" + for x :: "'a::real_normed_vector" by (simp add: dist_norm) -lemma sphere_empty [simp]: - fixes a :: "'a::metric_space" - shows "r < 0 \ sphere a r = {}" -by auto +lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}" + for a :: "'a::metric_space" + by auto lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e" by simp @@ -1063,7 +1055,7 @@ lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e" by simp -lemma ball_subset_cball [simp,intro]: "ball x e \ cball x e" +lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e" by (simp add: subset_eq) lemma sphere_cball [simp,intro]: "sphere z r \ cball z r" @@ -1407,10 +1399,10 @@ lemma subset_box: fixes a :: "'a::euclidean_space" - shows "cbox c d \ cbox a b \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th1) - and "cbox c d \ box a b \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i < c\i \ d\i < b\i)" (is ?th2) - and "box c d \ cbox a b \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th3) - and "box c d \ box a b \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th4) + shows "cbox c d \ cbox a b \ (\i\Basis. c\i \ d\i) \ (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th1) + and "cbox c d \ box a b \ (\i\Basis. c\i \ d\i) \ (\i\Basis. a\i < c\i \ d\i < b\i)" (is ?th2) + and "box c d \ cbox a b \ (\i\Basis. c\i < d\i) \ (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th3) + and "box c d \ box a b \ (\i\Basis. c\i < d\i) \ (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th4) proof - show ?th1 unfolding subset_eq and Ball_def and mem_box @@ -1523,7 +1515,7 @@ qed lemma eq_cbox_box [simp]: "cbox a b = box c d \ cbox a b = {} \ box c d = {}" - (is "?lhs = ?rhs") + (is "?lhs \ ?rhs") proof assume ?lhs then have "cbox a b \ box c d" "box c d \cbox a b" @@ -1543,7 +1535,7 @@ by (metis eq_cbox_box) lemma eq_box: "box a b = box c d \ box a b = {} \ box c d = {} \ a = c \ b = d" - (is "?lhs = ?rhs") + (is "?lhs \ ?rhs") proof assume ?lhs then have "box a b \ box c d" "box c d \ box a b" @@ -1624,16 +1616,16 @@ lemma mem_is_intervalI: assumes "is_interval s" - assumes "a \ s" "b \ s" - assumes "\i. i \ Basis \ a \ i \ x \ i \ x \ i \ b \ i \ b \ i \ x \ i \ x \ i \ a \ i" + and "a \ s" "b \ s" + and "\i. i \ Basis \ a \ i \ x \ i \ x \ i \ b \ i \ b \ i \ x \ i \ x \ i \ a \ i" shows "x \ s" by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)]) lemma interval_subst: fixes S::"'a::euclidean_space set" assumes "is_interval S" - assumes "x \ S" "y j \ S" - assumes "j \ Basis" + and "x \ S" "y j \ S" + and "j \ Basis" shows "(\i\Basis. (if i = j then y i \ i else x \ i) *\<^sub>R i) \ S" by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms) @@ -1645,11 +1637,12 @@ proof - from assms have "\i \ Basis. \s \ S. x \ i = s \ i" by auto - with finite_Basis obtain s and bs::"'a list" where - s: "\i. i \ Basis \ x \ i = s i \ i" "\i. i \ Basis \ s i \ S" and - bs: "set bs = Basis" "distinct bs" + with finite_Basis obtain s and bs::"'a list" + where s: "\i. i \ Basis \ x \ i = s i \ i" "\i. i \ Basis \ s i \ S" + and bs: "set bs = Basis" "distinct bs" by (metis finite_distinct_list) - from nonempty_Basis s obtain j where j: "j \ Basis" "s j \ S" by blast + from nonempty_Basis s obtain j where j: "j \ Basis" "s j \ S" + by blast define y where "y = rec_list (s j) (\j _ Y. (\i\Basis. (if i = j then s i \ i else Y \ i) *\<^sub>R i))" have "x = (\i\Basis. (if i \ set bs then s i \ i else s j \ i) *\<^sub>R i)" @@ -1660,9 +1653,9 @@ also have "y bs \ S" using bs(1)[THEN equalityD1] apply (induct bs) - apply (auto simp: y_def j) + apply (auto simp: y_def j) apply (rule interval_subst[OF assms(1)]) - apply (auto simp: s) + apply (auto simp: s) done finally show ?thesis . qed @@ -1674,7 +1667,7 @@ by (simp add: box_ne_empty inner_Basis inner_sum_left) (simp add: sum.remove) -subsection\Connectedness\ +subsection \Connectedness\ lemma connected_local: "connected S \ @@ -1690,19 +1683,16 @@ lemma exists_diff: fixes P :: "'a set \ bool" - shows "(\S. P (- S)) \ (\S. P S)" (is "?lhs \ ?rhs") -proof - - { - assume "?lhs" - then have ?rhs by blast - } - moreover - { - fix S - assume H: "P S" - have "S = - (- S)" by auto - with H have "P (- (- S))" by metis - } + shows "(\S. P (- S)) \ (\S. P S)" + (is "?lhs \ ?rhs") +proof - + have ?rhs if ?lhs + using that by blast + moreover have "P (- (- S))" if "P S" for S + proof - + have "S = - (- S)" by simp + with that show ?thesis by metis + qed ultimately show ?thesis by metis qed @@ -1717,29 +1707,25 @@ then have th0: "connected S \ \ (\e2 e1. closed e2 \ open e1 \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})" (is " _ \ \ (\e2 e1. ?P e2 e1)") - apply (simp add: closed_def) - apply metis - done + by (simp add: closed_def) metis have th1: "?rhs \ \ (\t' t. closed t'\t = S\t' \ t\{} \ t\S \ (\t'. open t' \ t = S \ t'))" (is "_ \ \ (\t' t. ?Q t' t)") unfolding connected_def openin_open closedin_closed by auto - { - fix e2 - { - fix e1 - have "?P e2 e1 \ (\t. closed e2 \ t = S\e2 \ open e1 \ t = S\e1 \ t\{} \ t \ S)" - by auto - } - then have "(\e1. ?P e2 e1) \ (\t. ?Q e2 t)" + have "(\e1. ?P e2 e1) \ (\t. ?Q e2 t)" for e2 + proof - + have "?P e2 e1 \ (\t. closed e2 \ t = S\e2 \ open e1 \ t = S\e1 \ t\{} \ t \ S)" for e1 + by auto + then show ?thesis by metis - } + qed then have "\e2. (\e1. ?P e2 e1) \ (\t. ?Q e2 t)" by blast then show ?thesis - unfolding th0 th1 by simp -qed - -subsection\Limit points\ + by (simp add: th0 th1) +qed + + +subsection \Limit points\ definition (in topological_space) islimpt:: "'a \ 'a set \ bool" (infixr "islimpt" 60) where "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" @@ -1765,9 +1751,8 @@ shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" unfolding islimpt_iff_eventually eventually_at by fast -lemma islimpt_approachable_le: - fixes x :: "'a::metric_space" - shows "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" +lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" + for x :: "'a::metric_space" unfolding islimpt_approachable using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x", THEN arg_cong [where f=Not]] @@ -1781,14 +1766,13 @@ text \A perfect space has no isolated points.\ -lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV" +lemma islimpt_UNIV [simp, intro]: "x islimpt UNIV" + for x :: "'a::perfect_space" unfolding islimpt_UNIV_iff by (rule not_open_singleton) -lemma perfect_choose_dist: - fixes x :: "'a::{perfect_space, metric_space}" - shows "0 < r \ \a. a \ x \ dist a x < r" - using islimpt_UNIV [of x] - by (simp add: islimpt_approachable) +lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r" + for x :: "'a::{perfect_space,metric_space}" + using islimpt_UNIV [of x] by (simp add: islimpt_approachable) lemma closed_limpt: "closed S \ (\x. x islimpt S \ x \ S)" unfolding closed_def @@ -1798,12 +1782,12 @@ done lemma islimpt_EMPTY[simp]: "\ x islimpt {}" - unfolding islimpt_def by auto + by (auto simp add: islimpt_def) lemma finite_set_avoid: fixes a :: "'a::metric_space" assumes fS: "finite S" - shows "\d>0. \x\S. x \ a \ d \ dist a x" + shows "\d>0. \x\S. x \ a \ d \ dist a x" proof (induct rule: finite_induct[OF fS]) case 1 then show ?case by (auto intro: zero_less_one) @@ -1814,12 +1798,12 @@ show ?case proof (cases "x = a") case True - then show ?thesis using d by auto + with d show ?thesis by auto next case False let ?d = "min d (dist a x)" - have dp: "?d > 0" - using False d(1) by auto + from False d(1) have dp: "?d > 0" + by auto from d have d': "\x\F. x \ a \ ?d \ dist a x" by auto with dp False show ?thesis @@ -1836,9 +1820,8 @@ and d: "\x \ S. \y \ S. dist y x < e \ y = x" shows "closed S" proof - - { - fix x - assume C: "\e>0. \x'\S. x' \ x \ dist x' x < e" + have False if C: "\e>0. \x'\S. x' \ x \ dist x' x < e" for x + proof - from e have e2: "e/2 > 0" by arith from C[rule_format, OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2" by blast @@ -1847,18 +1830,19 @@ by simp from C[rule_format, OF mp] obtain z where z: "z \ S" "z \ x" "dist z x < ?m" by blast - have th: "dist z y < e" using z y - by (intro dist_triangle_lt [where z=x], simp) - from d[rule_format, OF y(1) z(1) th] y z - have False by (auto simp add: dist_commute)} + from z y have "dist z y < e" + by (intro dist_triangle_lt [where z=x]) simp + from d[rule_format, OF y(1) z(1) this] y z show ?thesis + by (auto simp add: dist_commute) + qed then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) qed -lemma closed_of_nat_image: "closed (of_nat ` A :: 'a :: real_normed_algebra_1 set)" +lemma closed_of_nat_image: "closed (of_nat ` A :: 'a::real_normed_algebra_1 set)" by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat) -lemma closed_of_int_image: "closed (of_int ` A :: 'a :: real_normed_algebra_1 set)" +lemma closed_of_int_image: "closed (of_int ` A :: 'a::real_normed_algebra_1 set)" by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int) lemma closed_Nats [simp]: "closed (\ :: 'a :: real_normed_algebra_1 set)" @@ -1918,10 +1902,13 @@ shows "interior S = T" by (intro equalityI assms interior_subset open_interior interior_maximal) -lemma interior_singleton [simp]: - fixes a :: "'a::perfect_space" shows "interior {a} = {}" - apply (rule interior_unique, simp_all) - using not_open_singleton subset_singletonD by fastforce +lemma interior_singleton [simp]: "interior {a} = {}" + for a :: "'a::perfect_space" + apply (rule interior_unique) + apply simp_all + using not_open_singleton subset_singletonD + apply fastforce + done lemma interior_Int [simp]: "interior (S \ T) = interior S \ interior T" by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 @@ -1994,11 +1981,12 @@ qed lemma interior_Ici: - fixes x :: "'a :: {dense_linorder, linorder_topology}" + fixes x :: "'a :: {dense_linorder,linorder_topology}" assumes "b < x" - shows "interior { x ..} = { x <..}" + shows "interior {x ..} = {x <..}" proof (rule interior_unique) - fix T assume "T \ {x ..}" "open T" + fix T + assume "T \ {x ..}" "open T" moreover have "x \ T" proof assume "x \ T" @@ -2013,11 +2001,12 @@ qed auto lemma interior_Iic: - fixes x :: "'a :: {dense_linorder, linorder_topology}" + fixes x :: "'a ::{dense_linorder,linorder_topology}" assumes "x < b" shows "interior {.. x} = {..< x}" proof (rule interior_unique) - fix T assume "T \ {.. x}" "open T" + fix T + assume "T \ {.. x}" "open T" moreover have "x \ T" proof assume "x \ T" @@ -2031,30 +2020,31 @@ by (auto simp: subset_eq less_le) qed auto + subsection \Closure of a Set\ definition "closure S = S \ {x | x. x islimpt S}" lemma interior_closure: "interior S = - (closure (- S))" - unfolding interior_def closure_def islimpt_def by auto + by (auto simp add: interior_def closure_def islimpt_def) lemma closure_interior: "closure S = - interior (- S)" - unfolding interior_closure by simp + by (simp add: interior_closure) lemma closed_closure[simp, intro]: "closed (closure S)" - unfolding closure_interior by (simp add: closed_Compl) + by (simp add: closure_interior closed_Compl) lemma closure_subset: "S \ closure S" - unfolding closure_def by simp + by (simp add: closure_def) lemma closure_hull: "closure S = closed hull S" - unfolding hull_def closure_interior interior_def by auto + by (auto simp add: hull_def closure_interior interior_def) lemma closure_eq: "closure S = S \ closed S" unfolding closure_hull using closed_Inter by (rule hull_eq) lemma closure_closed [simp]: "closed S \ closure S = S" - unfolding closure_eq . + by (simp only: closure_eq) lemma closure_closure [simp]: "closure (closure S) = closure S" unfolding closure_hull by (rule hull_hull) @@ -2079,53 +2069,44 @@ using closed_UNIV by (rule closure_closed) lemma closure_Un [simp]: "closure (S \ T) = closure S \ closure T" - unfolding closure_interior by simp + by (simp add: closure_interior) lemma closure_eq_empty [iff]: "closure S = {} \ S = {}" - using closure_empty closure_subset[of S] - by blast + using closure_empty closure_subset[of S] by blast lemma closure_subset_eq: "closure S \ S \ closed S" - using closure_eq[of S] closure_subset[of S] - by simp - -lemma open_Int_closure_eq_empty: - "open S \ (S \ closure T) = {} \ S \ T = {}" + using closure_eq[of S] closure_subset[of S] by simp + +lemma open_Int_closure_eq_empty: "open S \ (S \ closure T) = {} \ S \ T = {}" using open_subset_interior[of S "- T"] using interior_subset[of "- T"] - unfolding closure_interior - by auto - -lemma open_Int_closure_subset: - "open S \ (S \ (closure T)) \ closure(S \ T)" + by (auto simp: closure_interior) + +lemma open_Int_closure_subset: "open S \ S \ closure T \ closure (S \ T)" proof fix x - assume as: "open S" "x \ S \ closure T" - { - assume *: "x islimpt T" - have "x islimpt (S \ T)" - proof (rule islimptI) - fix A - assume "x \ A" "open A" - with as have "x \ A \ S" "open (A \ S)" - by (simp_all add: open_Int) - with * obtain y where "y \ T" "y \ A \ S" "y \ x" - by (rule islimptE) - then have "y \ S \ T" "y \ A \ y \ x" - by simp_all - then show "\y\(S \ T). y \ A \ y \ x" .. - qed - } - then show "x \ closure (S \ T)" using as - unfolding closure_def - by blast + assume *: "open S" "x \ S \ closure T" + have "x islimpt (S \ T)" if **: "x islimpt T" + proof (rule islimptI) + fix A + assume "x \ A" "open A" + with * have "x \ A \ S" "open (A \ S)" + by (simp_all add: open_Int) + with ** obtain y where "y \ T" "y \ A \ S" "y \ x" + by (rule islimptE) + then have "y \ S \ T" "y \ A \ y \ x" + by simp_all + then show "\y\(S \ T). y \ A \ y \ x" .. + qed + with * show "x \ closure (S \ T)" + unfolding closure_def by blast qed lemma closure_complement: "closure (- S) = - interior S" - unfolding closure_interior by simp + by (simp add: closure_interior) lemma interior_complement: "interior (- S) = - closure S" - unfolding closure_interior by simp + by (simp add: closure_interior) lemma closure_Times: "closure (A \ B) = closure A \ closure B" proof (rule closure_unique) @@ -2136,7 +2117,8 @@ fix T assume "A \ B \ T" and "closed T" then show "closure A \ closure B \ T" - apply (simp add: closed_def open_prod_def, clarify) + apply (simp add: closed_def open_prod_def) + apply clarify apply (rule ccontr) apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D) apply (simp add: closure_interior interior_def) @@ -2150,63 +2132,61 @@ unfolding closure_def using islimpt_punctured by blast lemma connected_imp_connected_closure: "connected S \ connected (closure S)" - by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD) - -lemma limpt_of_limpts: - fixes x :: "'a::metric_space" - shows "x islimpt {y. y islimpt S} \ x islimpt S" + by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD) + +lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S" + for x :: "'a::metric_space" apply (clarsimp simp add: islimpt_approachable) apply (drule_tac x="e/2" in spec) apply (auto simp: simp del: less_divide_eq_numeral1) apply (drule_tac x="dist x' x" in spec) apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1) apply (erule rev_bexI) - by (metis dist_commute dist_triangle_half_r less_trans less_irrefl) + apply (metis dist_commute dist_triangle_half_r less_trans less_irrefl) + done lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}" using closed_limpt limpt_of_limpts by blast -lemma limpt_of_closure: - fixes x :: "'a::metric_space" - shows "x islimpt closure S \ x islimpt S" +lemma limpt_of_closure: "x islimpt closure S \ x islimpt S" + for x :: "'a::metric_space" by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts) lemma closedin_limpt: - "closedin (subtopology euclidean T) S \ S \ T \ (\x. x islimpt S \ x \ T \ x \ S)" + "closedin (subtopology euclidean T) S \ S \ T \ (\x. x islimpt S \ x \ T \ x \ S)" apply (simp add: closedin_closed, safe) - apply (simp add: closed_limpt islimpt_subset) + apply (simp add: closed_limpt islimpt_subset) apply (rule_tac x="closure S" in exI) apply simp apply (force simp: closure_def) done -lemma closedin_closed_eq: - "closed S \ (closedin (subtopology euclidean S) T \ closed T \ T \ S)" +lemma closedin_closed_eq: "closed S \ closedin (subtopology euclidean S) T \ closed T \ T \ S" by (meson closedin_limpt closed_subset closedin_closed_trans) lemma closedin_subset_trans: - "\closedin (subtopology euclidean U) S; S \ T; T \ U\ - \ closedin (subtopology euclidean T) S" -by (meson closedin_limpt subset_iff) + "closedin (subtopology euclidean U) S \ S \ T \ T \ U \ + closedin (subtopology euclidean T) S" + by (meson closedin_limpt subset_iff) lemma openin_subset_trans: - "\openin (subtopology euclidean U) S; S \ T; T \ U\ - \ openin (subtopology euclidean T) S" + "openin (subtopology euclidean U) S \ S \ T \ T \ U \ + openin (subtopology euclidean T) S" by (auto simp: openin_open) lemma openin_Times: - "\openin (subtopology euclidean S) S'; openin (subtopology euclidean T) T'\ - \ openin (subtopology euclidean (S \ T)) (S' \ T')" + "openin (subtopology euclidean S) S' \ openin (subtopology euclidean T) T' \ + openin (subtopology euclidean (S \ T)) (S' \ T')" unfolding openin_open using open_Times by blast lemma Times_in_interior_subtopology: - fixes U :: "('a::metric_space * 'b::metric_space) set" + fixes U :: "('a::metric_space \ 'b::metric_space) set" assumes "(x, y) \ U" "openin (subtopology euclidean (S \ T)) U" obtains V W where "openin (subtopology euclidean S) V" "x \ V" "openin (subtopology euclidean T) W" "y \ W" "(V \ W) \ U" proof - from assms obtain e where "e > 0" and "U \ S \ T" - and e: "\x' y'. \x'\S; y'\T; dist (x', y') (x, y) < e\ \ (x', y') \ U" + and e: "\x' y'. \x'\S; y'\T; dist (x', y') (x, y) < e\ \ (x', y') \ U" by (force simp: openin_euclidean_subtopology_iff) with assms have "x \ S" "y \ T" by auto @@ -2228,9 +2208,8 @@ lemma openin_Times_eq: fixes S :: "'a::metric_space set" and T :: "'b::metric_space set" shows - "openin (subtopology euclidean (S \ T)) (S' \ T') \ - (S' = {} \ T' = {} \ - openin (subtopology euclidean S) S' \ openin (subtopology euclidean T) T')" + "openin (subtopology euclidean (S \ T)) (S' \ T') \ + S' = {} \ T' = {} \ openin (subtopology euclidean S) S' \ openin (subtopology euclidean T) T'" (is "?lhs = ?rhs") proof (cases "S' = {} \ T' = {}") case True @@ -2241,15 +2220,19 @@ by blast show ?thesis proof - assume L: ?lhs + assume ?lhs have "openin (subtopology euclidean S) S'" apply (subst openin_subopen, clarify) - apply (rule Times_in_interior_subtopology [OF _ L]) - using \y \ T'\ by auto + apply (rule Times_in_interior_subtopology [OF _ \?lhs\]) + using \y \ T'\ + apply auto + done moreover have "openin (subtopology euclidean T) T'" apply (subst openin_subopen, clarify) - apply (rule Times_in_interior_subtopology [OF _ L]) - using \x \ S'\ by auto + apply (rule Times_in_interior_subtopology [OF _ \?lhs\]) + using \x \ S'\ + apply auto + done ultimately show ?rhs by simp next @@ -2260,39 +2243,40 @@ qed lemma closedin_Times: - "\closedin (subtopology euclidean S) S'; closedin (subtopology euclidean T) T'\ - \ closedin (subtopology euclidean (S \ T)) (S' \ T')" -unfolding closedin_closed using closed_Times by blast + "closedin (subtopology euclidean S) S' \ closedin (subtopology euclidean T) T' \ + closedin (subtopology euclidean (S \ T)) (S' \ T')" + unfolding closedin_closed using closed_Times by blast lemma bdd_below_closure: fixes A :: "real set" assumes "bdd_below A" shows "bdd_below (closure A)" proof - - from assms obtain m where "\x. x \ A \ m \ x" unfolding bdd_below_def by auto - hence "A \ {m..}" by auto - hence "closure A \ {m..}" using closed_real_atLeast by (rule closure_minimal) - thus ?thesis unfolding bdd_below_def by auto -qed - -subsection\Connected components, considered as a connectedness relation or a set\ - -definition - "connected_component s x y \ \t. connected t \ t \ s \ x \ t \ y \ t" - -abbreviation - "connected_component_set s x \ Collect (connected_component s x)" + from assms obtain m where "\x. x \ A \ m \ x" + by (auto simp: bdd_below_def) + then have "A \ {m..}" by auto + then have "closure A \ {m..}" + using closed_real_atLeast by (rule closure_minimal) + then show ?thesis + by (auto simp: bdd_below_def) +qed + + +subsection \Connected components, considered as a connectedness relation or a set\ + +definition "connected_component s x y \ \t. connected t \ t \ s \ x \ t \ y \ t" + +abbreviation "connected_component_set s x \ Collect (connected_component s x)" lemma connected_componentI: - "\connected t; t \ s; x \ t; y \ t\ \ connected_component s x y" + "connected t \ t \ s \ x \ t \ y \ t \ connected_component s x y" by (auto simp: connected_component_def) lemma connected_component_in: "connected_component s x y \ x \ s \ y \ s" by (auto simp: connected_component_def) lemma connected_component_refl: "x \ s \ connected_component s x x" - apply (auto simp: connected_component_def) - using connected_sing by blast + by (auto simp: connected_component_def) (use connected_sing in blast) lemma connected_component_refl_eq [simp]: "connected_component s x x \ x \ s" by (auto simp: connected_component_refl) (auto simp: connected_component_def) @@ -2301,11 +2285,12 @@ by (auto simp: connected_component_def) lemma connected_component_trans: - "\connected_component s x y; connected_component s y z\ \ connected_component s x z" + "connected_component s x y \ connected_component s y z \ connected_component s x z" unfolding connected_component_def by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un) -lemma connected_component_of_subset: "\connected_component s x y; s \ t\ \ connected_component t x y" +lemma connected_component_of_subset: + "connected_component s x y \ s \ t \ connected_component t x y" by (auto simp: connected_component_def) lemma connected_component_Union: "connected_component_set s x = \{t. connected t \ x \ t \ t \ s}" @@ -2314,9 +2299,11 @@ lemma connected_connected_component [iff]: "connected (connected_component_set s x)" by (auto simp: connected_component_Union intro: connected_Union) -lemma connected_iff_eq_connected_component_set: "connected s \ (\x \ s. connected_component_set s x = s)" -proof (cases "s={}") - case True then show ?thesis by simp +lemma connected_iff_eq_connected_component_set: + "connected s \ (\x \ s. connected_component_set s x = s)" +proof (cases "s = {}") + case True + then show ?thesis by simp next case False then obtain x where "x \ s" by auto @@ -2335,98 +2322,106 @@ lemma connected_component_subset: "connected_component_set s x \ s" using connected_component_in by blast -lemma connected_component_eq_self: "\connected s; x \ s\ \ connected_component_set s x = s" +lemma connected_component_eq_self: "connected s \ x \ s \ connected_component_set s x = s" by (simp add: connected_iff_eq_connected_component_set) lemma connected_iff_connected_component: - "connected s \ (\x \ s. \y \ s. connected_component s x y)" + "connected s \ (\x \ s. \y \ s. connected_component s x y)" using connected_component_in by (auto simp: connected_iff_eq_connected_component_set) lemma connected_component_maximal: - "\x \ t; connected t; t \ s\ \ t \ (connected_component_set s x)" + "x \ t \ connected t \ t \ s \ t \ (connected_component_set s x)" using connected_component_eq_self connected_component_of_subset by blast lemma connected_component_mono: - "s \ t \ (connected_component_set s x) \ (connected_component_set t x)" + "s \ t \ connected_component_set s x \ connected_component_set t x" by (simp add: Collect_mono connected_component_of_subset) -lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \ (x \ s)" +lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \ x \ s" using connected_component_refl by (fastforce simp: connected_component_in) lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}" using connected_component_eq_empty by blast lemma connected_component_eq: - "y \ connected_component_set s x - \ (connected_component_set s y = connected_component_set s x)" - by (metis (no_types, lifting) Collect_cong connected_component_sym connected_component_trans mem_Collect_eq) + "y \ connected_component_set s x \ (connected_component_set s y = connected_component_set s x)" + by (metis (no_types, lifting) + Collect_cong connected_component_sym connected_component_trans mem_Collect_eq) lemma closed_connected_component: - assumes s: "closed s" shows "closed (connected_component_set s x)" + assumes s: "closed s" + shows "closed (connected_component_set s x)" proof (cases "x \ s") - case False then show ?thesis + case False + then show ?thesis by (metis connected_component_eq_empty closed_empty) next case True show ?thesis unfolding closure_eq [symmetric] - proof - show "closure (connected_component_set s x) \ connected_component_set s x" - apply (rule connected_component_maximal) + proof + show "closure (connected_component_set s x) \ connected_component_set s x" + apply (rule connected_component_maximal) apply (simp add: closure_def True) - apply (simp add: connected_imp_connected_closure) - apply (simp add: s closure_minimal connected_component_subset) - done - next - show "connected_component_set s x \ closure (connected_component_set s x)" - by (simp add: closure_subset) + apply (simp add: connected_imp_connected_closure) + apply (simp add: s closure_minimal connected_component_subset) + done + next + show "connected_component_set s x \ closure (connected_component_set s x)" + by (simp add: closure_subset) qed qed lemma connected_component_disjoint: - "(connected_component_set s a) \ (connected_component_set s b) = {} \ - a \ connected_component_set s b" -apply (auto simp: connected_component_eq) -using connected_component_eq connected_component_sym by blast + "connected_component_set s a \ connected_component_set s b = {} \ + a \ connected_component_set s b" + apply (auto simp: connected_component_eq) + using connected_component_eq connected_component_sym + apply blast + done lemma connected_component_nonoverlap: - "(connected_component_set s a) \ (connected_component_set s b) = {} \ - (a \ s \ b \ s \ connected_component_set s a \ connected_component_set s b)" + "connected_component_set s a \ connected_component_set s b = {} \ + a \ s \ b \ s \ connected_component_set s a \ connected_component_set s b" apply (auto simp: connected_component_in) - using connected_component_refl_eq apply blast - apply (metis connected_component_eq mem_Collect_eq) + using connected_component_refl_eq + apply blast + apply (metis connected_component_eq mem_Collect_eq) apply (metis connected_component_eq mem_Collect_eq) done lemma connected_component_overlap: - "(connected_component_set s a \ connected_component_set s b \ {}) = - (a \ s \ b \ s \ connected_component_set s a = connected_component_set s b)" + "connected_component_set s a \ connected_component_set s b \ {} \ + a \ s \ b \ s \ connected_component_set s a = connected_component_set s b" by (auto simp: connected_component_nonoverlap) lemma connected_component_sym_eq: "connected_component s x y \ connected_component s y x" using connected_component_sym by blast lemma connected_component_eq_eq: - "connected_component_set s x = connected_component_set s y \ - x \ s \ y \ s \ x \ s \ y \ s \ connected_component s x y" - apply (case_tac "y \ s") + "connected_component_set s x = connected_component_set s y \ + x \ s \ y \ s \ x \ s \ y \ s \ connected_component s x y" + apply (cases "y \ s") apply (simp add:) apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq) - apply (case_tac "x \ s") + apply (cases "x \ s") apply (simp add:) apply (metis connected_component_eq_empty) - using connected_component_eq_empty by blast + using connected_component_eq_empty + apply blast + done lemma connected_iff_connected_component_eq: - "connected s \ - (\x \ s. \y \ s. connected_component_set s x = connected_component_set s y)" + "connected s \ (\x \ s. \y \ s. connected_component_set s x = connected_component_set s y)" by (simp add: connected_component_eq_eq connected_iff_connected_component) lemma connected_component_idemp: - "connected_component_set (connected_component_set s x) x = connected_component_set s x" -apply (rule subset_antisym) -apply (simp add: connected_component_subset) -by (metis connected_component_eq_empty connected_component_maximal connected_component_refl_eq connected_connected_component mem_Collect_eq set_eq_subset) + "connected_component_set (connected_component_set s x) x = connected_component_set s x" + apply (rule subset_antisym) + apply (simp add: connected_component_subset) + apply (metis connected_component_eq_empty connected_component_maximal + connected_component_refl_eq connected_connected_component mem_Collect_eq set_eq_subset) + done lemma connected_component_unique: "\x \ c; c \ s; connected c; @@ -2468,10 +2463,11 @@ apply (simp add: connected_component_maximal connected_component_mono subset_antisym) using connected_component_eq_empty by blast -subsection\The set of connected components of a set\ - -definition components:: "'a::topological_space set \ 'a set set" where - "components s \ connected_component_set s ` s" + +subsection \The set of connected components of a set\ + +definition components:: "'a::topological_space set \ 'a set set" + where "components s \ connected_component_set s ` s" lemma components_iff: "s \ components u \ (\x. x \ u \ s = connected_component_set u x)" by (auto simp: components_def) @@ -2506,15 +2502,16 @@ by (metis components_iff connected_connected_component) lemma in_components_maximal: - "c \ components s \ - (c \ {} \ c \ s \ connected c \ (\d. d \ {} \ c \ d \ d \ s \ connected d \ d = c))" + "c \ components s \ + c \ {} \ c \ s \ connected c \ (\d. d \ {} \ c \ d \ d \ s \ connected d \ d = c)" apply (rule iffI) - apply (simp add: in_components_nonempty in_components_connected) - apply (metis (full_types) components_iff connected_component_eq_self connected_component_intermediate_subset connected_component_refl in_components_subset mem_Collect_eq rev_subsetD) - by (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI) + apply (simp add: in_components_nonempty in_components_connected) + apply (metis (full_types) components_iff connected_component_eq_self connected_component_intermediate_subset connected_component_refl in_components_subset mem_Collect_eq rev_subsetD) + apply (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI) + done lemma joinable_components_eq: - "connected t \ t \ s \ c1 \ components s \ c2 \ components s \ c1 \ t \ {} \ c2 \ t \ {} \ c1 = c2" + "connected t \ t \ s \ c1 \ components s \ c2 \ components s \ c1 \ t \ {} \ c2 \ t \ {} \ c1 = c2" by (metis (full_types) components_iff joinable_connected_component_eq) lemma closed_components: "\closed s; c \ components s\ \ closed c" @@ -2541,16 +2538,19 @@ lemma components_eq_sing_iff: "components s = {s} \ connected s \ s \ {}" apply (rule iffI) - using in_components_connected apply fastforce + using in_components_connected apply fastforce apply safe - using Union_components apply fastforce + using Union_components apply fastforce apply (metis components_iff connected_component_eq_self) - using in_components_maximal by auto + using in_components_maximal + apply auto + done lemma components_eq_sing_exists: "(\a. components s = {a}) \ connected s \ s \ {}" apply (rule iffI) - using connected_eq_connected_components_eq apply fastforce - by (metis components_eq_sing_iff) + using connected_eq_connected_components_eq apply fastforce + apply (metis components_eq_sing_iff) + done lemma connected_eq_components_subset_sing: "connected s \ components s \ {s}" by (metis Union_components components_empty components_eq_sing_iff connected_empty insert_subset order_refl subset_singletonD) @@ -2566,24 +2566,26 @@ by (meson connected_component_def connected_component_trans) lemma exists_component_superset: "\t \ s; s \ {}; connected t\ \ \c. c \ components s \ t \ c" - apply (case_tac "t = {}") + apply (cases "t = {}") apply force - by (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI) + apply (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI) + done lemma components_intermediate_subset: "\s \ components u; s \ t; t \ u\ \ s \ components t" apply (auto simp: components_iff) - by (metis connected_component_eq_empty connected_component_intermediate_subset) + apply (metis connected_component_eq_empty connected_component_intermediate_subset) + done lemma in_components_unions_complement: "c \ components s \ s - c = \(components s - {c})" by (metis complement_connected_component_unions components_def components_iff) lemma connected_intermediate_closure: assumes cs: "connected s" and st: "s \ t" and ts: "t \ closure s" - shows "connected t" + shows "connected t" proof (rule connectedI) fix A B assume A: "open A" and B: "open B" and Alap: "A \ t \ {}" and Blap: "B \ t \ {}" - and disj: "A \ B \ t = {}" and cover: "t \ A \ B" + and disj: "A \ B \ t = {}" and cover: "t \ A \ B" have disjs: "A \ B \ s = {}" using disj st by auto have "A \ closure s \ {}" @@ -2601,33 +2603,34 @@ lemma closedin_connected_component: "closedin (subtopology euclidean s) (connected_component_set s x)" proof (cases "connected_component_set s x = {}") - case True then show ?thesis + case True + then show ?thesis by (metis closedin_empty) next case False then obtain y where y: "connected_component s x y" by blast - have 1: "connected_component_set s x \ s \ closure (connected_component_set s x)" + have *: "connected_component_set s x \ s \ closure (connected_component_set s x)" by (auto simp: closure_def connected_component_in) - have 2: "connected_component s x y \ s \ closure (connected_component_set s x) \ connected_component_set s x" + have "connected_component s x y \ s \ closure (connected_component_set s x) \ connected_component_set s x" apply (rule connected_component_maximal) - apply (simp add:) + apply simp using closure_subset connected_component_in apply fastforce - using "1" connected_intermediate_closure apply blast+ + using * connected_intermediate_closure apply blast+ done - show ?thesis using y - apply (simp add: Topology_Euclidean_Space.closedin_closed) - using 1 2 by auto -qed - -subsection \Frontier (aka boundary)\ + with y * show ?thesis + by (auto simp add: Topology_Euclidean_Space.closedin_closed) +qed + + +subsection \Frontier (also known as boundary)\ definition "frontier S = closure S - interior S" lemma frontier_closed [iff]: "closed (frontier S)" by (simp add: frontier_def closed_Diff) -lemma frontier_closures: "frontier S = (closure S) \ (closure(- S))" +lemma frontier_closures: "frontier S = closure S \ closure (- S)" by (auto simp add: frontier_def interior_closure) lemma frontier_straddle: @@ -2667,8 +2670,7 @@ subsection \Filters and the ``eventually true'' quantifier\ -definition indirection :: "'a::real_normed_vector \ 'a \ 'a filter" - (infixr "indirection" 70) +definition indirection :: "'a::real_normed_vector \ 'a \ 'a filter" (infixr "indirection" 70) where "a indirection v = at a within {b. \c\0. b - a = scaleR c v}" text \Identify Trivial limits, where we can't approach arbitrarily closely.\ @@ -2694,9 +2696,8 @@ lemma trivial_limit_at_iff: "trivial_limit (at a) \ \ a islimpt UNIV" using trivial_limit_within [of a UNIV] by simp -lemma trivial_limit_at: - fixes a :: "'a::perfect_space" - shows "\ trivial_limit (at a)" +lemma trivial_limit_at: "\ trivial_limit (at a)" + for a :: "'a::perfect_space" by (rule at_neq_bot) lemma trivial_limit_at_infinity: @@ -2710,10 +2711,9 @@ done lemma not_trivial_limit_within: "\ trivial_limit (at x within S) = (x \ closure (S - {x}))" - using islimpt_in_closure - by (metis trivial_limit_within) - -lemma at_within_eq_bot_iff: "(at c within A = bot) \ (c \ closure (A - {c}))" + using islimpt_in_closure by (metis trivial_limit_within) + +lemma at_within_eq_bot_iff: "at c within A = bot \ c \ closure (A - {c})" using not_trivial_limit_within[of c A] by blast text \Some property holds "sufficiently close" to the limit point.\ @@ -2727,13 +2727,10 @@ subsection \Limits\ -lemma Lim: - "(f \ l) net \ - trivial_limit net \ - (\e>0. eventually (\x. dist (f x) l < e) net)" - unfolding tendsto_iff trivial_limit_eq by auto - -text\Show that they yield usual definitions in the various cases.\ +lemma Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" + by (auto simp: tendsto_iff trivial_limit_eq) + +text \Show that they yield usual definitions in the various cases.\ lemma Lim_within_le: "(f \ l)(at a within S) \ (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" @@ -2746,27 +2743,28 @@ corollary Lim_withinI [intro?]: assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e" shows "(f \ l) (at a within S)" -apply (simp add: Lim_within, clarify) -apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) -done + apply (simp add: Lim_within, clarify) + apply (rule ex_forward [OF assms [OF half_gt_zero]]) + apply auto + done lemma Lim_at: "(f \ l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at) -lemma Lim_at_infinity: - "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" +lemma Lim_at_infinity: "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at_infinity) corollary Lim_at_infinityI [intro?]: assumes "\e. e > 0 \ \B. \x. norm x \ B \ dist (f x) l \ e" shows "(f \ l) at_infinity" -apply (simp add: Lim_at_infinity, clarify) -apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) -done + apply (simp add: Lim_at_infinity, clarify) + apply (rule ex_forward [OF assms [OF half_gt_zero]]) + apply auto + done lemma Lim_eventually: "eventually (\x. f x = l) net \ (f \ l) net" - by (rule topological_tendstoI, auto elim: eventually_mono) + by (rule topological_tendstoI) (auto elim: eventually_mono) lemma Lim_transform_within_set: fixes a :: "'a::metric_space" and l :: "'b::metric_space" @@ -2782,34 +2780,32 @@ fixes a l :: "'a::real_normed_vector" shows "eventually (\x. x \ s \ x \ t) (at a) \ ((f \ l) (at a within s) \ (f \ l) (at a within t))" -by (force intro: Lim_transform_within_set elim: eventually_mono) + by (force intro: Lim_transform_within_set elim: eventually_mono) lemma Lim_transform_within_openin: fixes a :: "'a::metric_space" assumes f: "(f \ l) (at a within T)" - and "openin (subtopology euclidean T) S" "a \ S" - and eq: "\x. \x \ S; x \ a\ \ f x = g x" + and "openin (subtopology euclidean T) S" "a \ S" + and eq: "\x. \x \ S; x \ a\ \ f x = g x" shows "(g \ l) (at a within T)" proof - obtain \ where "0 < \" and \: "ball a \ \ T \ S" using assms by (force simp: openin_contains_ball) then have "a \ ball a \" - by force + by simp show ?thesis - apply (rule Lim_transform_within [OF f \0 < \\ eq]) - using \ apply (auto simp: dist_commute subset_iff) - done + by (rule Lim_transform_within [OF f \0 < \\ eq]) (use \ in \auto simp: dist_commute subset_iff\) qed lemma continuous_transform_within_openin: fixes a :: "'a::metric_space" assumes "continuous (at a within T) f" - and "openin (subtopology euclidean T) S" "a \ S" - and eq: "\x. x \ S \ f x = g x" + and "openin (subtopology euclidean T) S" "a \ S" + and eq: "\x. x \ S \ f x = g x" shows "continuous (at a within T) g" -using assms by (simp add: Lim_transform_within_openin continuous_within) - -text\The expected monotonicity property.\ + using assms by (simp add: Lim_transform_within_openin continuous_within) + +text \The expected monotonicity property.\ lemma Lim_Un: assumes "(f \ l) (at x within S)" "(f \ l) (at x within T)" @@ -2821,10 +2817,9 @@ S \ T = UNIV \ (f \ l) (at x)" by (metis Lim_Un) -text\Interrelations between restricted and unrestricted limits.\ - -lemma Lim_at_imp_Lim_at_within: - "(f \ l) (at x) \ (f \ l) (at x within S)" +text \Interrelations between restricted and unrestricted limits.\ + +lemma Lim_at_imp_Lim_at_within: "(f \ l) (at x) \ (f \ l) (at x within S)" by (metis order_refl filterlim_mono subset_UNIV at_le) lemma eventually_within_interior: @@ -2834,23 +2829,21 @@ proof from assms obtain T where T: "open T" "x \ T" "T \ S" .. { - assume "?lhs" + assume ?lhs then obtain A where "open A" and "x \ A" and "\y\A. y \ x \ y \ S \ P y" - unfolding eventually_at_topological - by auto + by (auto simp: eventually_at_topological) with T have "open (A \ T)" and "x \ A \ T" and "\y \ A \ T. y \ x \ P y" by auto - then show "?rhs" - unfolding eventually_at_topological by auto + then show ?rhs + by (auto simp: eventually_at_topological) next - assume "?rhs" - then show "?lhs" + assume ?rhs + then show ?lhs by (auto elim: eventually_mono simp: eventually_at_filter) } qed -lemma at_within_interior: - "x \ interior S \ at x within S = at x" +lemma at_within_interior: "x \ interior S \ at x within S = at x" unfolding filter_eq_iff by (intro allI eventually_within_interior) lemma Lim_within_LIMSEQ: @@ -2897,7 +2890,7 @@ qed qed -text\Another limit point characterization.\ +text \Another limit point characterization.\ lemma limpt_sequential_inj: fixes x :: "'a::metric_space" @@ -4867,12 +4860,13 @@ lemma bolzano_weierstrass_imp_seq_compact: fixes s :: "'a::{t1_space, first_countable_topology} set" - shows "\t. infinite t \ t \ s --> (\x \ s. x islimpt t) \ seq_compact s" + shows "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ seq_compact s" by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point) + subsubsection\Totally bounded\ -lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N --> dist(s m)(s n) < e)" +lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (s m) (s n) < e)" unfolding Cauchy_def by metis lemma seq_compact_imp_totally_bounded: @@ -9001,82 +8995,69 @@ lemma continuous_on_inverse_open_map: assumes contf: "continuous_on S f" - and imf: "f ` S = T" - and injf: "\x. x \ S \ g(f x) = x" - and oo: "\U. openin (subtopology euclidean S) U - \ openin (subtopology euclidean T) (f ` U)" - shows "continuous_on T g" -proof - - have gTS: "g ` T = S" - using imf injf by force - have fU: "U \ S \ (f ` U) = {x \ T. g x \ U}" for U - using imf injf by force + and imf: "f ` S = T" + and injf: "\x. x \ S \ g (f x) = x" + and oo: "\U. openin (subtopology euclidean S) U \ openin (subtopology euclidean T) (f ` U)" + shows "continuous_on T g" +proof - + from imf injf have gTS: "g ` T = S" + by force + from imf injf have fU: "U \ S \ (f ` U) = {x \ T. g x \ U}" for U + by force show ?thesis - apply (simp add: continuous_on_open [of T g] gTS) - apply (metis openin_imp_subset fU oo) - done + by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo) qed lemma continuous_on_inverse_closed_map: assumes contf: "continuous_on S f" - and imf: "f ` S = T" - and injf: "\x. x \ S \ g(f x) = x" - and oo: "\U. closedin (subtopology euclidean S) U - \ closedin (subtopology euclidean T) (f ` U)" - shows "continuous_on T g" -proof - - have gTS: "g ` T = S" - using imf injf by force - have fU: "U \ S \ (f ` U) = {x \ T. g x \ U}" for U - using imf injf by force + and imf: "f ` S = T" + and injf: "\x. x \ S \ g(f x) = x" + and oo: "\U. closedin (subtopology euclidean S) U \ closedin (subtopology euclidean T) (f ` U)" + shows "continuous_on T g" +proof - + from imf injf have gTS: "g ` T = S" + by force + from imf injf have fU: "U \ S \ (f ` U) = {x \ T. g x \ U}" for U + by force show ?thesis - apply (simp add: continuous_on_closed [of T g] gTS) - apply (metis closedin_imp_subset fU oo) - done + by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo) qed lemma homeomorphism_injective_open_map: assumes contf: "continuous_on S f" - and imf: "f ` S = T" - and injf: "inj_on f S" - and oo: "\U. openin (subtopology euclidean S) U - \ openin (subtopology euclidean T) (f ` U)" + and imf: "f ` S = T" + and injf: "inj_on f S" + and oo: "\U. openin (subtopology euclidean S) U \ openin (subtopology euclidean T) (f ` U)" obtains g where "homeomorphism S T f g" -proof - +proof have "continuous_on T (inv_into S f)" by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo) - then show ?thesis - apply (rule_tac g = "inv_into S f" in that) - using imf injf contf apply (auto simp: homeomorphism_def) - done + with imf injf contf show "homeomorphism S T f (inv_into S f)" + by (auto simp: homeomorphism_def) qed lemma homeomorphism_injective_closed_map: assumes contf: "continuous_on S f" - and imf: "f ` S = T" - and injf: "inj_on f S" - and oo: "\U. closedin (subtopology euclidean S) U - \ closedin (subtopology euclidean T) (f ` U)" + and imf: "f ` S = T" + and injf: "inj_on f S" + and oo: "\U. closedin (subtopology euclidean S) U \ closedin (subtopology euclidean T) (f ` U)" obtains g where "homeomorphism S T f g" -proof - +proof have "continuous_on T (inv_into S f)" by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo) - then show ?thesis - apply (rule_tac g = "inv_into S f" in that) - using imf injf contf apply (auto simp: homeomorphism_def) - done + with imf injf contf show "homeomorphism S T f (inv_into S f)" + by (auto simp: homeomorphism_def) qed lemma homeomorphism_imp_open_map: assumes hom: "homeomorphism S T f g" - and oo: "openin (subtopology euclidean S) U" - shows "openin (subtopology euclidean T) (f ` U)" -proof - - have [simp]: "f ` U = {y. y \ T \ g y \ U}" - using assms openin_subset - by (fastforce simp: homeomorphism_def rev_image_eqI) - have "continuous_on T g" - using hom homeomorphism_def by blast + and oo: "openin (subtopology euclidean S) U" + shows "openin (subtopology euclidean T) (f ` U)" +proof - + from hom oo have [simp]: "f ` U = {y. y \ T \ g y \ U}" + using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) + from hom have "continuous_on T g" + unfolding homeomorphism_def by blast moreover have "g ` T = S" by (metis hom homeomorphism_def) ultimately show ?thesis @@ -9085,21 +9066,21 @@ lemma homeomorphism_imp_closed_map: assumes hom: "homeomorphism S T f g" - and oo: "closedin (subtopology euclidean S) U" - shows "closedin (subtopology euclidean T) (f ` U)" -proof - - have [simp]: "f ` U = {y. y \ T \ g y \ U}" - using assms closedin_subset - by (fastforce simp: homeomorphism_def rev_image_eqI) - have "continuous_on T g" - using hom homeomorphism_def by blast + and oo: "closedin (subtopology euclidean S) U" + shows "closedin (subtopology euclidean T) (f ` U)" +proof - + from hom oo have [simp]: "f ` U = {y. y \ T \ g y \ U}" + using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI) + from hom have "continuous_on T g" + unfolding homeomorphism_def by blast moreover have "g ` T = S" by (metis hom homeomorphism_def) ultimately show ?thesis by (simp add: continuous_on_closed oo) qed -subsection\"Isometry" (up to constant bounds) of injective linear map etc.\ + +subsection \"Isometry" (up to constant bounds) of injective linear map etc.\ lemma cauchy_isometric: assumes e: "e > 0" @@ -9111,15 +9092,13 @@ shows "Cauchy x" proof - interpret f: bounded_linear f by fact - { - fix d :: real - assume "d > 0" - then obtain N where N:"\n\N. norm (f (x n) - f (x N)) < e * d" + have "\N. \n\N. norm (x n - x N) < d" if "d > 0" for d :: real + proof - + from that obtain N where N: "\n\N. norm (f (x n) - f (x N)) < e * d" using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] e by auto - { - fix n - assume "n\N" + have "norm (x n - x N) < d" if "n \ N" for n + proof - have "e * norm (x n - x N) \ norm (f (x n - x N))" using subspace_diff[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]] @@ -9127,11 +9106,13 @@ by auto also have "norm (f (x n - x N)) < e * d" using \N \ n\ N unfolding f.diff[symmetric] by auto - finally have "norm (x n - x N) < d" using \e>0\ by simp - } - then have "\N. \n\N. norm (x n - x N) < d" by auto - } - then show ?thesis unfolding cauchy and dist_norm by auto + finally show ?thesis + using \e>0\ by simp + qed + then show ?thesis by auto + qed + then show ?thesis + by (simp add: cauchy dist_norm) qed lemma complete_isometric_image: @@ -9142,26 +9123,21 @@ and cs: "complete s" shows "complete (f ` s)" proof - - { - fix g - assume as:"\n::nat. g n \ f ` s" and cfg:"Cauchy g" - then obtain x where "\n. x n \ s \ g n = f (x n)" - using choice[of "\ n xa. xa \ s \ g n = f xa"] - by auto - then have x:"\n. x n \ s" "\n. g n = f (x n)" - by auto - then have "f \ x = g" - unfolding fun_eq_iff - by auto + have "\l\f ` s. (g \ l) sequentially" + if as:"\n::nat. g n \ f ` s" and cfg:"Cauchy g" for g + proof - + from that obtain x where "\n. x n \ s \ g n = f (x n)" + using choice[of "\ n xa. xa \ s \ g n = f xa"] by auto + then have x: "\n. x n \ s" "\n. g n = f (x n)" by auto + then have "f \ x = g" by (simp add: fun_eq_iff) then obtain l where "l\s" and l:"(x \ l) sequentially" using cs[unfolded complete_def, THEN spec[where x="x"]] using cauchy_isometric[OF \0 < e\ s f normf] and cfg and x(1) by auto - then have "\l\f ` s. (g \ l) sequentially" + then show ?thesis using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l] - unfolding \f \ x = g\ - by auto - } + by (auto simp: \f \ x = g\) + qed then show ?thesis unfolding complete_def by auto qed @@ -9173,25 +9149,25 @@ shows "\e>0. \x\s. norm (f x) \ e * norm x" proof (cases "s \ {0::'a}") case True - { - fix x - assume "x \ s" - then have "x = 0" using True by auto - then have "norm x \ norm (f x)" by auto - } - then show ?thesis by (auto intro!: exI[where x=1]) + have "norm x \ norm (f x)" if "x \ s" for x + proof - + from True that have "x = 0" by auto + then show ?thesis by simp + qed + then show ?thesis + by (auto intro!: exI[where x=1]) next + case False interpret f: bounded_linear f by fact - case False - then obtain a where a: "a \ 0" "a \ s" + from False obtain a where a: "a \ 0" "a \ s" by auto from False have "s \ {}" by auto - let ?S = "{f x| x. (x \ s \ norm x = norm a)}" + let ?S = "{f x| x. x \ s \ norm x = norm a}" let ?S' = "{x::'a. x\s \ norm x = norm a}" let ?S'' = "{x::'a. norm x = norm a}" - have "?S'' = frontier(cball 0 (norm a))" + have "?S'' = frontier (cball 0 (norm a))" by (simp add: sphere_def dist_norm) then have "compact ?S''" by (metis compact_cball compact_frontier) moreover have "?S' = s \ ?S''" by auto @@ -9200,8 +9176,9 @@ moreover have *:"f ` ?S' = ?S" by auto ultimately have "compact ?S" using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto - then have "closed ?S" using compact_imp_closed by auto - moreover have "?S \ {}" using a by auto + then have "closed ?S" + using compact_imp_closed by auto + moreover from a have "?S \ {}" by auto ultimately obtain b' where "b'\?S" "\y\?S. norm b' \ norm y" using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto then obtain b where "b\s" @@ -9210,36 +9187,31 @@ unfolding *[symmetric] unfolding image_iff by auto let ?e = "norm (f b) / norm b" - have "norm b > 0" using ba and a and norm_ge_zero by auto + have "norm b > 0" + using ba and a and norm_ge_zero by auto moreover have "norm (f b) > 0" using f(2)[THEN bspec[where x=b], OF \b\s\] - using \norm b >0\ - unfolding zero_less_norm_iff - by auto + using \norm b >0\ by simp ultimately have "0 < norm (f b) / norm b" by simp moreover - { - fix x - assume "x\s" - then have "norm (f b) / norm b * norm x \ norm (f x)" - proof (cases "x=0") - case True - then show "norm (f b) / norm b * norm x \ norm (f x)" by auto - next - case False - then have *: "0 < norm a / norm x" - using \a\0\ - unfolding zero_less_norm_iff[symmetric] by simp - have "\c. \x\s. c *\<^sub>R x \ s" - using s[unfolded subspace_def] by auto - then have "(norm a / norm x) *\<^sub>R x \ {x \ s. norm x = norm a}" - using \x\s\ and \x\0\ by auto - then show "norm (f b) / norm b * norm x \ norm (f x)" - using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]] - unfolding f.scaleR and ba using \x\0\ \a\0\ - by (auto simp add: mult.commute pos_le_divide_eq pos_divide_le_eq) - qed - } + have "norm (f b) / norm b * norm x \ norm (f x)" if "x\s" for x + proof (cases "x = 0") + case True + then show "norm (f b) / norm b * norm x \ norm (f x)" + by auto + next + case False + with \a \ 0\ have *: "0 < norm a / norm x" + unfolding zero_less_norm_iff[symmetric] by simp + have "\x\s. c *\<^sub>R x \ s" for c + using s[unfolded subspace_def] by simp + with \x \ s\ \x \ 0\ have "(norm a / norm x) *\<^sub>R x \ {x \ s. norm x = norm a}" + by simp + with \x \ 0\ \a \ 0\ show "norm (f b) / norm b * norm x \ norm (f x)" + using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]] + unfolding f.scaleR and ba + by (auto simp: mult.commute pos_le_divide_eq pos_divide_le_eq) + qed ultimately show ?thesis by auto qed @@ -9258,16 +9230,16 @@ subsection \Some properties of a canonical subspace\ -lemma subspace_substandard: - "subspace {x::'a::euclidean_space. (\i\Basis. P i \ x\i = 0)}" - unfolding subspace_def by (auto simp: inner_add_left) - -lemma closed_substandard: - "closed {x::'a::euclidean_space. \i\Basis. P i --> x\i = 0}" (is "closed ?A") +lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\i\Basis. P i \ x\i = 0)}" + by (auto simp: subspace_def inner_add_left) + +lemma closed_substandard: "closed {x::'a::euclidean_space. \i\Basis. P i \ x\i = 0}" + (is "closed ?A") proof - let ?D = "{i\Basis. P i}" have "closed (\i\?D. {x::'a. x\i = 0})" - by (simp add: closed_INT closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id) + by (simp add: closed_INT closed_Collect_eq continuous_on_inner + continuous_on_const continuous_on_id) also have "(\i\?D. {x::'a. x\i = 0}) = ?A" by auto finally show "closed ?A" . @@ -9277,31 +9249,30 @@ assumes d: "d \ Basis" shows "dim {x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0} = card d" (is "dim ?A = _") proof (rule dim_unique) - show "d \ ?A" - using d by (auto simp: inner_Basis) - show "independent d" - using independent_mono [OF independent_Basis d] . - show "?A \ span d" - proof (clarify) - fix x assume x: "\i\Basis. i \ d \ x \ i = 0" + from d show "d \ ?A" + by (auto simp: inner_Basis) + from d show "independent d" + by (rule independent_mono [OF independent_Basis]) + have "x \ span d" if "\i\Basis. i \ d \ x \ i = 0" for x + proof - have "finite d" - using finite_subset [OF d finite_Basis] . + by (rule finite_subset [OF d finite_Basis]) then have "(\i\d. (x \ i) *\<^sub>R i) \ span d" by (simp add: span_sum span_clauses) also have "(\i\d. (x \ i) *\<^sub>R i) = (\i\Basis. (x \ i) *\<^sub>R i)" - by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp add: x) + by (rule sum.mono_neutral_cong_left [OF finite_Basis d]) (auto simp: that) finally show "x \ span d" - unfolding euclidean_representation . + by (simp only: euclidean_representation) qed + then show "?A \ span d" by auto qed simp -text\Hence closure and completeness of all subspaces.\ - +text \Hence closure and completeness of all subspaces.\ lemma ex_card: assumes "n \ card A" shows "\S\A. card S = n" -proof cases - assume "finite A" +proof (cases "finite A") + case True from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..n \ card A\ have "{..< n} \ {..< card A}" "inj_on f {..< n}" by (auto simp: bij_betw_def intro: subset_inj_on) @@ -9309,7 +9280,7 @@ by (auto simp: bij_betw_def card_image) then show ?thesis by blast next - assume "\ finite A" + case False with \n \ card A\ show ?thesis by force qed @@ -9333,201 +9304,169 @@ "inj_on f {x. \i\Basis. i \ d \ x \ i = 0}" by blast interpret f: bounded_linear f - using f unfolding linear_conv_bounded_linear by auto - { - fix x - have "x\?t \ f x = 0 \ x = 0" - using f.zero d f(3)[THEN inj_onD, of x 0] by auto - } - moreover have "closed ?t" using closed_substandard . - moreover have "subspace ?t" using subspace_substandard . + using f by (simp add: linear_conv_bounded_linear) + have "x \ ?t \ f x = 0 \ x = 0" for x + using f.zero d f(3)[THEN inj_onD, of x 0] by auto + moreover have "closed ?t" by (rule closed_substandard) + moreover have "subspace ?t" by (rule subspace_substandard) ultimately show ?thesis using closed_injective_image_subspace[of ?t f] unfolding f(2) using f(1) unfolding linear_conv_bounded_linear by auto qed -lemma complete_subspace: - fixes s :: "('a::euclidean_space) set" - shows "subspace s \ complete s" +lemma complete_subspace: "subspace s \ complete s" + for s :: "'a::euclidean_space set" using complete_eq_closed closed_subspace by auto -lemma closed_span [iff]: - fixes s :: "'a::euclidean_space set" - shows "closed (span s)" -by (simp add: closed_subspace subspace_span) - -lemma dim_closure [simp]: - fixes s :: "('a::euclidean_space) set" - shows "dim(closure s) = dim s" (is "?dc = ?d") -proof - - have "?dc \ ?d" using closure_minimal[OF span_inc, of s] +lemma closed_span [iff]: "closed (span s)" + for s :: "'a::euclidean_space set" + by (simp add: closed_subspace) + +lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d") + for s :: "'a::euclidean_space set" +proof - + have "?dc \ ?d" + using closure_minimal[OF span_inc, of s] using closed_subspace[OF subspace_span, of s] using dim_subset[of "closure s" "span s"] - unfolding dim_span - by auto - then show ?thesis using dim_subset[OF closure_subset, of s] - by auto + by simp + then show ?thesis + using dim_subset[OF closure_subset, of s] + by simp qed subsection \Affine transformations of intervals\ -lemma real_affinity_le: - "0 < (m::'a::linordered_field) \ (m * x + c \ y \ x \ inverse(m) * y + -(c / m))" +lemma real_affinity_le: "0 < m \ m * x + c \ y \ x \ inverse m * y + - (c / m)" + for m :: "'a::linordered_field" by (simp add: field_simps) -lemma real_le_affinity: - "0 < (m::'a::linordered_field) \ (y \ m * x + c \ inverse(m) * y + -(c / m) \ x)" +lemma real_le_affinity: "0 < m \ y \ m * x + c \ inverse m * y + - (c / m) \ x" + for m :: "'a::linordered_field" by (simp add: field_simps) -lemma real_affinity_lt: - "0 < (m::'a::linordered_field) \ (m * x + c < y \ x < inverse(m) * y + -(c / m))" +lemma real_affinity_lt: "0 < m \ m * x + c < y \ x < inverse m * y + - (c / m)" + for m :: "'a::linordered_field" by (simp add: field_simps) -lemma real_lt_affinity: - "0 < (m::'a::linordered_field) \ (y < m * x + c \ inverse(m) * y + -(c / m) < x)" +lemma real_lt_affinity: "0 < m \ y < m * x + c \ inverse m * y + - (c / m) < x" + for m :: "'a::linordered_field" by (simp add: field_simps) -lemma real_affinity_eq: - "(m::'a::linordered_field) \ 0 \ (m * x + c = y \ x = inverse(m) * y + -(c / m))" +lemma real_affinity_eq: "m \ 0 \ m * x + c = y \ x = inverse m * y + - (c / m)" + for m :: "'a::linordered_field" by (simp add: field_simps) -lemma real_eq_affinity: - "(m::'a::linordered_field) \ 0 \ (y = m * x + c \ inverse(m) * y + -(c / m) = x)" +lemma real_eq_affinity: "m \ 0 \ y = m * x + c \ inverse m * y + - (c / m) = x" + for m :: "'a::linordered_field" by (simp add: field_simps) -subsection \Banach fixed point theorem (not really topological...)\ +subsection \Banach fixed point theorem (not really topological ...)\ theorem banach_fix: assumes s: "complete s" "s \ {}" and c: "0 \ c" "c < 1" - and f: "(f ` s) \ s" + and f: "f ` s \ s" and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y" shows "\!x\s. f x = x" proof - - have "1 - c > 0" using c by auto - - from s(2) obtain z0 where "z0 \ s" by auto + from c have "1 - c > 0" by simp + + from s(2) obtain z0 where z0: "z0 \ s" by blast define z where "z n = (f ^^ n) z0" for n - { - fix n :: nat - have "z n \ s" unfolding z_def - proof (induct n) - case 0 - then show ?case using \z0 \ s\ by auto - next - case Suc - then show ?case using f by auto qed - } note z_in_s = this - + with f z0 have z_in_s: "z n \ s" for n :: nat + by (induct n) auto define d where "d = dist (z 0) (z 1)" - have fzn:"\n. f (z n) = z (Suc n)" unfolding z_def by auto - { - fix n :: nat - have "dist (z n) (z (Suc n)) \ (c ^ n) * d" - proof (induct n) - case 0 - then show ?case - unfolding d_def by auto - next - case (Suc m) - then have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * d" - using \0 \ c\ - using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] - by auto - then show ?case - using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s] - unfolding fzn and mult_le_cancel_left - by auto + have fzn: "f (z n) = z (Suc n)" for n + by (simp add: z_def) + have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * d" for n :: nat + proof (induct n) + case 0 + then show ?case + by (simp add: d_def) + next + case (Suc m) + with \0 \ c\ have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * d" + using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp + then show ?case + using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s] + by (simp add: fzn mult_le_cancel_left) + qed + + have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * d * (1 - c ^ n)" for n m :: nat + proof (induct n) + case 0 + show ?case by simp + next + case (Suc k) + from c have "(1 - c) * dist (z m) (z (m + Suc k)) \ + (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))" + by (simp add: dist_triangle) + also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)" + by simp + also from Suc have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d" + by (simp add: field_simps) + also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)" + by (simp add: power_add field_simps) + also from c have "\ \ (c ^ m) * d * (1 - c ^ Suc k)" + by (simp add: field_simps) + finally show ?case by simp + qed + + have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" if "e > 0" for e + proof (cases "d = 0") + case True + from \1 - c > 0\ have "(1 - c) * x \ 0 \ x \ 0" for x + by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1) + with c cf_z2[of 0] True have "z n = z0" for n + by (simp add: z_def) + with \e > 0\ show ?thesis by simp + next + case False + with zero_le_dist[of "z 0" "z 1"] have "d > 0" + by (metis d_def less_le) + with \1 - c > 0\ \e > 0\ have "0 < e * (1 - c) / d" + by simp + with c obtain N where N: "c ^ N < e * (1 - c) / d" + using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto + have *: "dist (z m) (z n) < e" if "m > n" and as: "m \ N" "n \ N" for m n :: nat + proof - + from c \n \ N\ have *: "c ^ n \ c ^ N" + using power_decreasing[OF \n\N\, of c] by simp + from c \m > n\ have "1 - c ^ (m - n) > 0" + using power_strict_mono[of c 1 "m - n"] by simp + with \d > 0\ \0 < 1 - c\ have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0" + by simp + from cf_z2[of n "m - n"] \m > n\ + have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)" + by (simp add: pos_le_divide_eq[OF \1 - c > 0\] mult.commute dist_commute) + also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)" + using mult_right_mono[OF * order_less_imp_le[OF **]] + by (simp add: mult.assoc) + also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)" + using mult_strict_right_mono[OF N **] by (auto simp add: mult.assoc) + also from c \d > 0\ \1 - c > 0\ have "\ = e * (1 - c ^ (m - n))" + by simp + also from c \1 - c ^ (m - n) > 0\ \e > 0\ have "\ \ e" + using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto + finally show ?thesis by simp qed - } note cf_z = this - - { - fix n m :: nat - have "(1 - c) * dist (z m) (z (m+n)) \ (c ^ m) * d * (1 - c ^ n)" - proof (induct n) - case 0 - show ?case by auto - next - case (Suc k) - have "(1 - c) * dist (z m) (z (m + Suc k)) \ - (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))" - using dist_triangle and c by (auto simp add: dist_triangle) - also have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)" - using cf_z[of "m + k"] and c by auto - also have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d" - using Suc by (auto simp add: field_simps) - also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)" - unfolding power_add by (auto simp add: field_simps) - also have "\ \ (c ^ m) * d * (1 - c ^ Suc k)" - using c by (auto simp add: field_simps) - finally show ?case by auto - qed - } note cf_z2 = this - { - fix e :: real - assume "e > 0" - then have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" - proof (cases "d = 0") + have "dist (z n) (z m) < e" if "N \ m" "N \ n" for m n :: nat + proof (cases "n = m") case True - have *: "\x. ((1 - c) * x \ 0) = (x \ 0)" using \1 - c > 0\ - by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1) - from True have "\n. z n = z0" using cf_z2[of 0] and c unfolding z_def - by (simp add: *) - then show ?thesis using \e>0\ by auto + with \e > 0\ show ?thesis by simp next case False - then have "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"] - by (metis False d_def less_le) - hence "0 < e * (1 - c) / d" - using \e>0\ and \1-c>0\ by auto - then obtain N where N:"c ^ N < e * (1 - c) / d" - using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto - { - fix m n::nat - assume "m>n" and as:"m\N" "n\N" - have *:"c ^ n \ c ^ N" using \n\N\ and c - using power_decreasing[OF \n\N\, of c] by auto - have "1 - c ^ (m - n) > 0" - using c and power_strict_mono[of c 1 "m - n"] using \m>n\ by auto - hence **: "d * (1 - c ^ (m - n)) / (1 - c) > 0" - using \d>0\ \0 < 1 - c\ by auto - - have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)" - using cf_z2[of n "m - n"] and \m>n\ - unfolding pos_le_divide_eq[OF \1-c>0\] - by (auto simp add: mult.commute dist_commute) - also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)" - using mult_right_mono[OF * order_less_imp_le[OF **]] - unfolding mult.assoc by auto - also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)" - using mult_strict_right_mono[OF N **] unfolding mult.assoc by auto - also have "\ = e * (1 - c ^ (m - n))" - using c and \d>0\ and \1 - c > 0\ by auto - also have "\ \ e" using c and \1 - c ^ (m - n) > 0\ and \e>0\ - using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto - finally have "dist (z m) (z n) < e" by auto - } note * = this - { - fix m n :: nat - assume as: "N \ m" "N \ n" - then have "dist (z n) (z m) < e" - proof (cases "n = m") - case True - then show ?thesis using \e>0\ by auto - next - case False - then show ?thesis using as and *[of n m] *[of m n] - unfolding nat_neq_iff by (auto simp add: dist_commute) - qed - } - then show ?thesis by auto + with *[of n m] *[of m n] and that show ?thesis + by (auto simp add: dist_commute nat_neq_iff) qed - } + then show ?thesis by auto + qed then have "Cauchy z" - unfolding cauchy_def by auto + by (simp add: cauchy_def) then obtain x where "x\s" and x:"(z \ x) sequentially" using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto @@ -9541,7 +9480,6 @@ then obtain N where N:"\n\N. dist (z n) x < e / 2" using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto then have N':"dist (z N) x < e / 2" by auto - have *: "c * dist (z N) x \ dist (z N) x" unfolding mult_le_cancel_right2 using zero_le_dist[of "z N" x] and c @@ -9559,22 +9497,17 @@ unfolding e_def by auto qed - then have "f x = x" unfolding e_def by auto - moreover - { - fix y - assume "f y = y" "y\s" - then have "dist x y \ c * dist x y" - using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] - using \x\s\ and \f x = x\ - by auto - then have "dist x y = 0" - unfolding mult_le_cancel_right1 - using c and zero_le_dist[of x y] - by auto - then have "y = x" by auto - } - ultimately show ?thesis using \x\s\ by blast+ + then have "f x = x" by (auto simp: e_def) + moreover have "y = x" if "f y = y" "y \ s" for y + proof - + from \x \ s\ \f x = x\ that have "dist x y \ c * dist x y" + using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp + with c and zero_le_dist[of x y] have "dist x y = 0" + by (simp add: mult_le_cancel_right1) + then show ?thesis by simp + qed + ultimately show ?thesis + using \x\s\ by blast qed @@ -9595,7 +9528,7 @@ have "\x y e. x \ s \ y \ s \ 0 < e \ dist y x < e \ dist (g y) (g x) < e" using dist by fastforce then have "continuous_on s g" - unfolding continuous_on_iff by auto + by (auto simp: continuous_on_iff) then have cont: "continuous_on ?D (\x. dist ((g \ fst) x) (snd x))" unfolding continuous_on_eq_continuous_within by (intro continuous_dist ballI continuous_within_compose) @@ -9615,26 +9548,29 @@ qed moreover have "\x. x \ s \ g x = x \ x = a" using dist[THEN bspec[where x=a]] \g a = a\ and \a\s\ by auto - ultimately show "\!x\s. g x = x" using \a \ s\ by blast + ultimately show "\!x\s. g x = x" + using \a \ s\ by blast qed lemma cball_subset_cball_iff: fixes a :: "'a :: euclidean_space" shows "cball a r \ cball a' r' \ dist a a' + r \ r' \ r < 0" - (is "?lhs = ?rhs") + (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs proof (cases "r < 0") - case True then show ?rhs by simp + case True + then show ?rhs by simp next case False then have [simp]: "r \ 0" by simp have "norm (a - a') + r \ r'" proof (cases "a = a'") - case True then show ?thesis - using subsetD [where c = "a + r *\<^sub>R (SOME i. i \ Basis)", OF \?lhs\] subsetD [where c = "a", OF \?lhs\] + case True + then show ?thesis + using subsetD [where c = "a + r *\<^sub>R (SOME i. i \ Basis)", OF \?lhs\] subsetD [where c = "a", OF \?lhs\] by (force simp add: SOME_Basis dist_norm) next case False @@ -9642,79 +9578,84 @@ by (simp add: algebra_simps) also have "... = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))" by (simp add: algebra_simps) - also have "... = \- norm (a - a') - r\" - using \a \ a'\ by (simp add: abs_mult_pos field_simps) - finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \norm (a - a') + r\" by linarith - show ?thesis - using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \?lhs\] \a \ a'\ + also from \a \ a'\ have "... = \- norm (a - a') - r\" + by (simp add: abs_mult_pos field_simps) + finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \norm (a - a') + r\" + by linarith + from \a \ a'\ show ?thesis + using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \?lhs\] by (simp add: dist_norm scaleR_add_left) qed - then show ?rhs by (simp add: dist_norm) + then show ?rhs + by (simp add: dist_norm) qed next - assume ?rhs then show ?lhs - apply (auto simp: ball_def dist_norm) - apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans) - done -qed - -lemma cball_subset_ball_iff: - fixes a :: "'a :: euclidean_space" - shows "cball a r \ ball a' r' \ dist a a' + r < r' \ r < 0" - (is "?lhs = ?rhs") + assume ?rhs + then show ?lhs + by (auto simp: ball_def dist_norm) + (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans) +qed + +lemma cball_subset_ball_iff: "cball a r \ ball a' r' \ dist a a' + r < r' \ r < 0" + (is "?lhs \ ?rhs") + for a :: "'a::euclidean_space" proof assume ?lhs then show ?rhs proof (cases "r < 0") - case True then show ?rhs by simp + case True then + show ?rhs by simp next case False then have [simp]: "r \ 0" by simp have "norm (a - a') + r < r'" proof (cases "a = a'") - case True then show ?thesis - using subsetD [where c = "a + r *\<^sub>R (SOME i. i \ Basis)", OF \?lhs\] subsetD [where c = "a", OF \?lhs\] + case True + then show ?thesis + using subsetD [where c = "a + r *\<^sub>R (SOME i. i \ Basis)", OF \?lhs\] subsetD [where c = "a", OF \?lhs\] by (force simp add: SOME_Basis dist_norm) next case False - { assume "norm (a - a') + r \ r'" - then have "\r' - norm (a - a')\ \ r" - apply (simp split: abs_split) - by (metis \0 \ r\ \?lhs\ centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq) - then have False - using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \?lhs\] \a \ a'\ - apply (simp add: dist_norm field_simps) - apply (simp add: diff_divide_distrib scaleR_left_diff_distrib) - done - } + have False if "norm (a - a') + r \ r'" + proof - + from that have "\r' - norm (a - a')\ \ r" + by (simp split: abs_split) + (metis \0 \ r\ \?lhs\ centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq) + then show ?thesis + using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \?lhs\] \a \ a'\ + by (simp add: dist_norm field_simps) + (simp add: diff_divide_distrib scaleR_left_diff_distrib) + qed then show ?thesis by force qed then show ?rhs by (simp add: dist_norm) qed next - assume ?rhs then show ?lhs - apply (auto simp: ball_def dist_norm ) - apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans) - done -qed - -lemma ball_subset_cball_iff: - fixes a :: "'a :: euclidean_space" - shows "ball a r \ cball a' r' \ dist a a' + r \ r' \ r \ 0" - (is "?lhs = ?rhs") + assume ?rhs + then show ?lhs + by (auto simp: ball_def dist_norm) + (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans) +qed + +lemma ball_subset_cball_iff: "ball a r \ cball a' r' \ dist a a' + r \ r' \ r \ 0" + (is "?lhs = ?rhs") + for a :: "'a::euclidean_space" proof (cases "r \ 0") - case True then show ?thesis + case True + then show ?thesis using dist_not_less_zero less_le_trans by force next - case False show ?thesis + case False + show ?thesis proof assume ?lhs then have "(cball a r \ cball a' r')" by (metis False closed_cball closure_ball closure_closed closure_mono not_less) - then show ?rhs - using False cball_subset_cball_iff by fastforce + with False show ?rhs + by (fastforce iff: cball_subset_cball_iff) next - assume ?rhs with False show ?lhs + assume ?rhs + with False show ?lhs using ball_subset_cball cball_subset_cball_iff by blast qed qed diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Data_Structures/Balance.thy --- a/src/HOL/Data_Structures/Balance.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Data_Structures/Balance.thy Mon Dec 12 17:40:06 2016 +0100 @@ -8,6 +8,63 @@ "~~/src/HOL/Library/Tree" begin +(* The following two lemmas should go into theory \Tree\, except that that +theory would then depend on \Complex_Main\. *) + +lemma min_height_balanced: assumes "balanced t" +shows "min_height t = nat(floor(log 2 (size1 t)))" +proof cases + assume *: "complete t" + hence "size1 t = 2 ^ min_height t" + by (simp add: complete_iff_height size1_if_complete) + hence "size1 t = 2 powr min_height t" + using * by (simp add: powr_realpow) + hence "min_height t = log 2 (size1 t)" + by simp + thus ?thesis + by linarith +next + assume *: "\ complete t" + hence "height t = min_height t + 1" + using assms min_height_le_height[of t] + by(auto simp add: balanced_def complete_iff_height) + hence "2 ^ min_height t \ size1 t \ size1 t < 2 ^ (min_height t + 1)" + by (metis * min_height_size1 size1_height_if_incomplete) + hence "2 powr min_height t \ size1 t \ size1 t < 2 powr (min_height t + 1)" + by(simp only: powr_realpow) + (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power) + hence "min_height t \ log 2 (size1 t) \ log 2 (size1 t) < min_height t + 1" + by(simp add: log_less_iff le_log_iff) + thus ?thesis by linarith +qed + +lemma height_balanced: assumes "balanced t" +shows "height t = nat(ceiling(log 2 (size1 t)))" +proof cases + assume *: "complete t" + hence "size1 t = 2 ^ height t" + by (simp add: size1_if_complete) + hence "size1 t = 2 powr height t" + using * by (simp add: powr_realpow) + hence "height t = log 2 (size1 t)" + by simp + thus ?thesis + by linarith +next + assume *: "\ complete t" + hence **: "height t = min_height t + 1" + using assms min_height_le_height[of t] + by(auto simp add: balanced_def complete_iff_height) + hence 0: "2 ^ min_height t < size1 t \ size1 t \ 2 ^ (min_height t + 1)" + by (metis "*" min_height_size1_if_incomplete size1_height) + hence "2 powr min_height t < size1 t \ size1 t \ 2 powr (min_height t + 1)" + by(simp only: powr_realpow) + (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power) + hence "min_height t < log 2 (size1 t) \ log 2 (size1 t) \ min_height t + 1" + by(simp add: log_le_iff less_log_iff) + thus ?thesis using ** by linarith +qed + (* mv *) text \The lemmas about \floor\ and \ceiling\ of \log 2\ should be generalized @@ -94,57 +151,116 @@ show ?thesis by simp qed +lemma balanced_Node_if_wbal1: +assumes "balanced l" "balanced r" "size l = size r + 1" +shows "balanced \l, x, r\" +proof - + from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_def) + have "nat \log 2 (1 + size1 r)\ \ nat \log 2 (size1 r)\" + by(rule nat_mono[OF ceiling_mono]) simp + hence 1: "height(Node l x r) = nat \log 2 (1 + size1 r)\ + 1" + using height_balanced[OF assms(1)] height_balanced[OF assms(2)] + by (simp del: nat_ceiling_le_eq add: max_def) + have "nat \log 2 (1 + size1 r)\ \ nat \log 2 (size1 r)\" + by(rule nat_mono[OF floor_mono]) simp + hence 2: "min_height(Node l x r) = nat \log 2 (size1 r)\ + 1" + using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)] + by (simp) + have "size1 r \ 1" by(simp add: size1_def) + then obtain i where i: "2 ^ i \ size1 r" "size1 r < 2 ^ (i + 1)" + using ex_power_ivl1[of 2 "size1 r"] by auto + hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \ 2 ^ (i + 1)" by auto + from 1 2 floor_log_nat_ivl[OF _ i] ceil_log_nat_ivl[OF _ i1] + show ?thesis by(simp add:balanced_def) +qed + +lemma balanced_sym: "balanced \l, x, r\ \ balanced \r, y, l\" +by(auto simp: balanced_def) + +lemma balanced_Node_if_wbal2: +assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \ 1" +shows "balanced \l, x, r\" +proof - + have "size l = size r \ (size l = size r + 1 \ size r = size l + 1)" (is "?A \ ?B") + using assms(3) by linarith + thus ?thesis + proof + assume "?A" + thus ?thesis using assms(1,2) + apply(simp add: balanced_def min_def max_def) + by (metis assms(1,2) balanced_optimal le_antisym le_less) + next + assume "?B" + thus ?thesis + by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1) + qed +qed + +lemma balanced_if_wbalanced: "wbalanced t \ balanced t" +proof(induction t) + case Leaf show ?case by (simp add: balanced_def) +next + case (Node l x r) + thus ?case by(simp add: balanced_Node_if_wbal2) +qed + (* end of mv *) -fun bal :: "'a list \ nat \ 'a tree * 'a list" where -"bal xs n = (if n=0 then (Leaf,xs) else +fun bal :: "nat \ 'a list \ 'a tree * 'a list" where +"bal n xs = (if n=0 then (Leaf,xs) else (let m = n div 2; - (l, ys) = bal xs m; - (r, zs) = bal (tl ys) (n-1-m) + (l, ys) = bal m xs; + (r, zs) = bal (n-1-m) (tl ys) in (Node l (hd ys) r, zs)))" declare bal.simps[simp del] +definition bal_list :: "nat \ 'a list \ 'a tree" where +"bal_list n xs = fst (bal n xs)" + definition balance_list :: "'a list \ 'a tree" where -"balance_list xs = fst (bal xs (length xs))" +"balance_list xs = bal_list (length xs) xs" + +definition bal_tree :: "nat \ 'a tree \ 'a tree" where +"bal_tree n t = bal_list n (inorder t)" definition balance_tree :: "'a tree \ 'a tree" where -"balance_tree = balance_list o inorder" +"balance_tree t = bal_tree (size t) t" lemma bal_simps: - "bal xs 0 = (Leaf, xs)" + "bal 0 xs = (Leaf, xs)" "n > 0 \ - bal xs n = + bal n xs = (let m = n div 2; - (l, ys) = bal xs m; - (r, zs) = bal (tl ys) (n-1-m) + (l, ys) = bal m xs; + (r, zs) = bal (n-1-m) (tl ys) in (Node l (hd ys) r, zs))" by(simp_all add: bal.simps) -text\The following lemmas take advantage of the fact +text\Some of the following lemmas take advantage of the fact that \bal xs n\ yields a result even if \n > length xs\.\ -lemma size_bal: "bal xs n = (t,ys) \ size t = n" -proof(induction xs n arbitrary: t ys rule: bal.induct) - case (1 xs n) +lemma size_bal: "bal n xs = (t,ys) \ size t = n" +proof(induction n xs arbitrary: t ys rule: bal.induct) + case (1 n xs) thus ?case by(cases "n=0") (auto simp add: bal_simps Let_def split: prod.splits) qed lemma bal_inorder: - "\ bal xs n = (t,ys); n \ length xs \ + "\ bal n xs = (t,ys); n \ length xs \ \ inorder t = take n xs \ ys = drop n xs" -proof(induction xs n arbitrary: t ys rule: bal.induct) - case (1 xs n) show ?case +proof(induction n xs arbitrary: t ys rule: bal.induct) + case (1 n xs) show ?case proof cases assume "n = 0" thus ?thesis using 1 by (simp add: bal_simps) next assume [arith]: "n \ 0" let ?n1 = "n div 2" let ?n2 = "n - 1 - ?n1" from "1.prems" obtain l r xs' where - b1: "bal xs ?n1 = (l,xs')" and - b2: "bal (tl xs') ?n2 = (r,ys)" and + b1: "bal ?n1 xs = (l,xs')" and + b2: "bal ?n2 (tl xs') = (r,ys)" and t: "t = \l, hd xs', r\" by(auto simp: Let_def bal_simps split: prod.splits) have IH1: "inorder l = take ?n1 xs \ xs' = drop ?n1 xs" @@ -162,31 +278,44 @@ qed qed -corollary inorder_balance_list: "inorder(balance_list xs) = xs" -using bal_inorder[of xs "length xs"] -by (metis balance_list_def order_refl prod.collapse take_all) +corollary inorder_bal_list[simp]: + "n \ length xs \ inorder(bal_list n xs) = take n xs" +unfolding bal_list_def by (metis bal_inorder eq_fst_iff) + +corollary inorder_balance_list[simp]: "inorder(balance_list xs) = xs" +by(simp add: balance_list_def) + +corollary inorder_bal_tree: + "n \ size t \ inorder(bal_tree n t) = take n (inorder t)" +by(simp add: bal_tree_def) corollary inorder_balance_tree[simp]: "inorder(balance_tree t) = inorder t" -by(simp add: balance_tree_def inorder_balance_list) +by(simp add: balance_tree_def inorder_bal_tree) + +corollary size_bal_list[simp]: "size(bal_list n xs) = n" +unfolding bal_list_def by (metis prod.collapse size_bal) corollary size_balance_list[simp]: "size(balance_list xs) = length xs" -by (metis inorder_balance_list length_inorder) +by (simp add: balance_list_def) + +corollary size_bal_tree[simp]: "size(bal_tree n t) = n" +by(simp add: bal_tree_def) corollary size_balance_tree[simp]: "size(balance_tree t) = size t" -by(simp add: balance_tree_def inorder_balance_list) +by(simp add: balance_tree_def) lemma min_height_bal: - "bal xs n = (t,ys) \ min_height t = nat(floor(log 2 (n + 1)))" -proof(induction xs n arbitrary: t ys rule: bal.induct) - case (1 xs n) show ?case + "bal n xs = (t,ys) \ min_height t = nat(floor(log 2 (n + 1)))" +proof(induction n xs arbitrary: t ys rule: bal.induct) + case (1 n xs) show ?case proof cases assume "n = 0" thus ?thesis using "1.prems" by (simp add: bal_simps) next assume [arith]: "n \ 0" from "1.prems" obtain l r xs' where - b1: "bal xs (n div 2) = (l,xs')" and - b2: "bal (tl xs') (n - 1 - n div 2) = (r,ys)" and + b1: "bal (n div 2) xs = (l,xs')" and + b2: "bal (n - 1 - n div 2) (tl xs') = (r,ys)" and t: "t = \l, hd xs', r\" by(auto simp: bal_simps Let_def split: prod.splits) let ?log1 = "nat (floor(log 2 (n div 2 + 1)))" @@ -211,17 +340,17 @@ qed lemma height_bal: - "bal xs n = (t,ys) \ height t = nat \log 2 (n + 1)\" -proof(induction xs n arbitrary: t ys rule: bal.induct) - case (1 xs n) show ?case + "bal n xs = (t,ys) \ height t = nat \log 2 (n + 1)\" +proof(induction n xs arbitrary: t ys rule: bal.induct) + case (1 n xs) show ?case proof cases assume "n = 0" thus ?thesis using "1.prems" by (simp add: bal_simps) next assume [arith]: "n \ 0" from "1.prems" obtain l r xs' where - b1: "bal xs (n div 2) = (l,xs')" and - b2: "bal (tl xs') (n - 1 - n div 2) = (r,ys)" and + b1: "bal (n div 2) xs = (l,xs')" and + b2: "bal (n - 1 - n div 2) (tl xs') = (r,ys)" and t: "t = \l, hd xs', r\" by(auto simp: bal_simps Let_def split: prod.splits) let ?log1 = "nat \log 2 (n div 2 + 1)\" @@ -242,28 +371,43 @@ qed lemma balanced_bal: - assumes "bal xs n = (t,ys)" shows "balanced t" + assumes "bal n xs = (t,ys)" shows "balanced t" unfolding balanced_def using height_bal[OF assms] min_height_bal[OF assms] by linarith +lemma height_bal_list: + "n \ length xs \ height (bal_list n xs) = nat \log 2 (n + 1)\" +unfolding bal_list_def by (metis height_bal prod.collapse) + lemma height_balance_list: "height (balance_list xs) = nat \log 2 (length xs + 1)\" -by (metis balance_list_def height_bal prod.collapse) +by (simp add: balance_list_def height_bal_list) + +corollary height_bal_tree: + "n \ length xs \ height (bal_tree n t) = nat(ceiling(log 2 (n + 1)))" +unfolding bal_list_def bal_tree_def +using height_bal prod.exhaust_sel by blast corollary height_balance_tree: "height (balance_tree t) = nat(ceiling(log 2 (size t + 1)))" -by(simp add: balance_tree_def height_balance_list) +by (simp add: bal_tree_def balance_tree_def height_bal_list) + +corollary balanced_bal_list[simp]: "balanced (bal_list n xs)" +unfolding bal_list_def by (metis balanced_bal prod.collapse) corollary balanced_balance_list[simp]: "balanced (balance_list xs)" -by (metis balance_list_def balanced_bal prod.collapse) +by (simp add: balance_list_def) + +corollary balanced_bal_tree[simp]: "balanced (bal_tree n t)" +by (simp add: bal_tree_def) corollary balanced_balance_tree[simp]: "balanced (balance_tree t)" by (simp add: balance_tree_def) -lemma wbalanced_bal: "bal xs n = (t,ys) \ wbalanced t" -proof(induction xs n arbitrary: t ys rule: bal.induct) - case (1 xs n) +lemma wbalanced_bal: "bal n xs = (t,ys) \ wbalanced t" +proof(induction n xs arbitrary: t ys rule: bal.induct) + case (1 n xs) show ?case proof cases assume "n = 0" @@ -272,8 +416,8 @@ next assume "n \ 0" with "1.prems" obtain l ys r zs where - rec1: "bal xs (n div 2) = (l, ys)" and - rec2: "bal (tl ys) (n - 1 - n div 2) = (r, zs)" and + rec1: "bal (n div 2) xs = (l, ys)" and + rec2: "bal (n - 1 - n div 2) (tl ys) = (r, zs)" and t: "t = \l, hd ys, r\" by(auto simp add: bal_simps Let_def split: prod.splits) have l: "wbalanced l" using "1.IH"(1)[OF \n\0\ refl rec1] . @@ -283,9 +427,21 @@ qed qed +text\An alternative proof via @{thm balanced_if_wbalanced}:\ +lemma "bal n xs = (t,ys) \ balanced t" +by(rule balanced_if_wbalanced[OF wbalanced_bal]) + +lemma wbalanced_bal_list[simp]: "wbalanced (bal_list n xs)" +by(simp add: bal_list_def) (metis prod.collapse wbalanced_bal) + +lemma wbalanced_balance_list[simp]: "wbalanced (balance_list xs)" +by(simp add: balance_list_def) + +lemma wbalanced_bal_tree[simp]: "wbalanced (bal_tree n t)" +by(simp add: bal_tree_def) + lemma wbalanced_balance_tree: "wbalanced (balance_tree t)" -by(simp add: balance_tree_def balance_list_def) - (metis prod.collapse wbalanced_bal) +by (simp add: balance_tree_def) hide_const (open) bal diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,125 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory ACom_ITP -imports "../Com" -begin - -subsection "Annotated Commands" - -datatype 'a acom = - SKIP 'a ("SKIP {_}" 61) | - Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | - Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) | - If bexp "('a acom)" "('a acom)" 'a - ("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) | - While 'a bexp "('a acom)" 'a - ("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61) - -fun post :: "'a acom \'a" where -"post (SKIP {P}) = P" | -"post (x ::= e {P}) = P" | -"post (c1;; c2) = post c2" | -"post (IF b THEN c1 ELSE c2 {P}) = P" | -"post ({Inv} WHILE b DO c {P}) = P" - -fun strip :: "'a acom \ com" where -"strip (SKIP {P}) = com.SKIP" | -"strip (x ::= e {P}) = (x ::= e)" | -"strip (c1;;c2) = (strip c1;; strip c2)" | -"strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" | -"strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)" - -fun anno :: "'a \ com \ 'a acom" where -"anno a com.SKIP = SKIP {a}" | -"anno a (x ::= e) = (x ::= e {a})" | -"anno a (c1;;c2) = (anno a c1;; anno a c2)" | -"anno a (IF b THEN c1 ELSE c2) = - (IF b THEN anno a c1 ELSE anno a c2 {a})" | -"anno a (WHILE b DO c) = - ({a} WHILE b DO anno a c {a})" - -fun annos :: "'a acom \ 'a list" where -"annos (SKIP {a}) = [a]" | -"annos (x::=e {a}) = [a]" | -"annos (C1;;C2) = annos C1 @ annos C2" | -"annos (IF b THEN C1 ELSE C2 {a}) = a # annos C1 @ annos C2" | -"annos ({i} WHILE b DO C {a}) = i # a # annos C" - -fun map_acom :: "('a \ 'b) \ 'a acom \ 'b acom" where -"map_acom f (SKIP {P}) = SKIP {f P}" | -"map_acom f (x ::= e {P}) = (x ::= e {f P})" | -"map_acom f (c1;;c2) = (map_acom f c1;; map_acom f c2)" | -"map_acom f (IF b THEN c1 ELSE c2 {P}) = - (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" | -"map_acom f ({Inv} WHILE b DO c {P}) = - ({f Inv} WHILE b DO map_acom f c {f P})" - - -lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)" -by (induction c) simp_all - -lemma strip_acom[simp]: "strip (map_acom f c) = strip c" -by (induction c) auto - -lemma map_acom_SKIP: - "map_acom f c = SKIP {S'} \ (\S. c = SKIP {S} \ S' = f S)" -by (cases c) auto - -lemma map_acom_Assign: - "map_acom f c = x ::= e {S'} \ (\S. c = x::=e {S} \ S' = f S)" -by (cases c) auto - -lemma map_acom_Seq: - "map_acom f c = c1';;c2' \ - (\c1 c2. c = c1;;c2 \ map_acom f c1 = c1' \ map_acom f c2 = c2')" -by (cases c) auto - -lemma map_acom_If: - "map_acom f c = IF b THEN c1' ELSE c2' {S'} \ - (\S c1 c2. c = IF b THEN c1 ELSE c2 {S} \ map_acom f c1 = c1' \ map_acom f c2 = c2' \ S' = f S)" -by (cases c) auto - -lemma map_acom_While: - "map_acom f w = {I'} WHILE b DO c' {P'} \ - (\I P c. w = {I} WHILE b DO c {P} \ map_acom f c = c' \ I' = f I \ P' = f P)" -by (cases w) auto - - -lemma strip_anno[simp]: "strip (anno a c) = c" -by(induct c) simp_all - -lemma strip_eq_SKIP: - "strip c = com.SKIP \ (EX P. c = SKIP {P})" -by (cases c) simp_all - -lemma strip_eq_Assign: - "strip c = x::=e \ (EX P. c = x::=e {P})" -by (cases c) simp_all - -lemma strip_eq_Seq: - "strip c = c1;;c2 \ (EX d1 d2. c = d1;;d2 & strip d1 = c1 & strip d2 = c2)" -by (cases c) simp_all - -lemma strip_eq_If: - "strip c = IF b THEN c1 ELSE c2 \ - (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)" -by (cases c) simp_all - -lemma strip_eq_While: - "strip c = WHILE b DO c1 \ - (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)" -by (cases c) simp_all - - -lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}" -by(induction C)(auto) - -lemma size_annos_same: "strip C1 = strip C2 \ size(annos C1) = size(annos C2)" -apply(induct C2 arbitrary: C1) -apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While) -done - -lemmas size_annos_same2 = eqTrueI[OF size_annos_same] - - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,397 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_Int0_ITP -imports - "~~/src/HOL/Library/While_Combinator" - Collecting_ITP -begin - -subsection "Orderings" - -class preord = -fixes le :: "'a \ 'a \ bool" (infix "\" 50) -assumes le_refl[simp]: "x \ x" -and le_trans: "x \ y \ y \ z \ x \ z" -begin - -definition mono where "mono f = (\x y. x \ y \ f x \ f y)" - -lemma monoD: "mono f \ x \ y \ f x \ f y" by(simp add: mono_def) - -lemma mono_comp: "mono f \ mono g \ mono (g o f)" -by(simp add: mono_def) - -declare le_trans[trans] - -end - -text{* Note: no antisymmetry. Allows implementations where some abstract -element is implemented by two different values @{prop "x \ y"} -such that @{prop"x \ y"} and @{prop"y \ x"}. Antisymmetry is not -needed because we never compare elements for equality but only for @{text"\"}. -*} - -class SL_top = preord + -fixes join :: "'a \ 'a \ 'a" (infixl "\" 65) -fixes Top :: "'a" ("\") -assumes join_ge1 [simp]: "x \ x \ y" -and join_ge2 [simp]: "y \ x \ y" -and join_least: "x \ z \ y \ z \ x \ y \ z" -and top[simp]: "x \ \" -begin - -lemma join_le_iff[simp]: "x \ y \ z \ x \ z \ y \ z" -by (metis join_ge1 join_ge2 join_least le_trans) - -lemma le_join_disj: "x \ y \ x \ z \ x \ y \ z" -by (metis join_ge1 join_ge2 le_trans) - -end - -instantiation "fun" :: (type, SL_top) SL_top -begin - -definition "f \ g = (ALL x. f x \ g x)" -definition "f \ g = (\x. f x \ g x)" -definition "\ = (\x. \)" - -lemma join_apply[simp]: "(f \ g) x = f x \ g x" -by (simp add: join_fun_def) - -instance -proof - case goal2 thus ?case by (metis le_fun_def preord_class.le_trans) -qed (simp_all add: le_fun_def Top_fun_def) - -end - - -instantiation acom :: (preord) preord -begin - -fun le_acom :: "('a::preord)acom \ 'a acom \ bool" where -"le_acom (SKIP {S}) (SKIP {S'}) = (S \ S')" | -"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \ e=e' \ S \ S')" | -"le_acom (c1;;c2) (c1';;c2') = (le_acom c1 c1' \ le_acom c2 c2')" | -"le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) = - (b=b' \ le_acom c1 c1' \ le_acom c2 c2' \ S \ S')" | -"le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) = - (b=b' \ le_acom c c' \ Inv \ Inv' \ P \ P')" | -"le_acom _ _ = False" - -lemma [simp]: "SKIP {S} \ c \ (\S'. c = SKIP {S'} \ S \ S')" -by (cases c) auto - -lemma [simp]: "x ::= e {S} \ c \ (\S'. c = x ::= e {S'} \ S \ S')" -by (cases c) auto - -lemma [simp]: "c1;;c2 \ c \ (\c1' c2'. c = c1';;c2' \ c1 \ c1' \ c2 \ c2')" -by (cases c) auto - -lemma [simp]: "IF b THEN c1 ELSE c2 {S} \ c \ - (\c1' c2' S'. c = IF b THEN c1' ELSE c2' {S'} \ c1 \ c1' \ c2 \ c2' \ S \ S')" -by (cases c) auto - -lemma [simp]: "{Inv} WHILE b DO c {P} \ w \ - (\Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \ c \ c' \ Inv \ Inv' \ P \ P')" -by (cases w) auto - -instance -proof - case goal1 thus ?case by (induct x) auto -next - case goal2 thus ?case - apply(induct x y arbitrary: z rule: le_acom.induct) - apply (auto intro: le_trans) - done -qed - -end - - -subsubsection "Lifting" - -instantiation option :: (preord)preord -begin - -fun le_option where -"Some x \ Some y = (x \ y)" | -"None \ y = True" | -"Some _ \ None = False" - -lemma [simp]: "(x \ None) = (x = None)" -by (cases x) simp_all - -lemma [simp]: "(Some x \ u) = (\y. u = Some y & x \ y)" -by (cases u) auto - -instance proof - case goal1 show ?case by(cases x, simp_all) -next - case goal2 thus ?case - by(cases z, simp, cases y, simp, cases x, auto intro: le_trans) -qed - -end - -instantiation option :: (SL_top)SL_top -begin - -fun join_option where -"Some x \ Some y = Some(x \ y)" | -"None \ y = y" | -"x \ None = x" - -lemma join_None2[simp]: "x \ None = x" -by (cases x) simp_all - -definition "\ = Some \" - -instance proof - case goal1 thus ?case by(cases x, simp, cases y, simp_all) -next - case goal2 thus ?case by(cases y, simp, cases x, simp_all) -next - case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all) -next - case goal4 thus ?case by(cases x, simp_all add: Top_option_def) -qed - -end - -definition bot_acom :: "com \ ('a::SL_top)option acom" ("\\<^sub>c") where -"\\<^sub>c = anno None" - -lemma strip_bot_acom[simp]: "strip(\\<^sub>c c) = c" -by(simp add: bot_acom_def) - -lemma bot_acom[rule_format]: "strip c' = c \ \\<^sub>c c \ c'" -apply(induct c arbitrary: c') -apply (simp_all add: bot_acom_def) - apply(induct_tac c') - apply simp_all - apply(induct_tac c') - apply simp_all - apply(induct_tac c') - apply simp_all - apply(induct_tac c') - apply simp_all - apply(induct_tac c') - apply simp_all -done - - -subsubsection "Post-fixed point iteration" - -definition - pfp :: "(('a::preord) \ 'a) \ 'a \ 'a option" where -"pfp f = while_option (\x. \ f x \ x) f" - -lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \ x" -using while_option_stop[OF assms[simplified pfp_def]] by simp - -lemma pfp_least: -assumes mono: "\x y. x \ y \ f x \ f y" -and "f p \ p" and "x0 \ p" and "pfp f x0 = Some x" shows "x \ p" -proof- - { fix x assume "x \ p" - hence "f x \ f p" by(rule mono) - from this `f p \ p` have "f x \ p" by(rule le_trans) - } - thus "x \ p" using assms(2-) while_option_rule[where P = "%x. x \ p"] - unfolding pfp_def by blast -qed - -definition - lpfp\<^sub>c :: "(('a::SL_top)option acom \ 'a option acom) \ com \ 'a option acom option" where -"lpfp\<^sub>c f c = pfp f (\\<^sub>c c)" - -lemma lpfpc_pfp: "lpfp\<^sub>c f c0 = Some c \ f c \ c" -by(simp add: pfp_pfp lpfp\<^sub>c_def) - -lemma strip_pfp: -assumes "\x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" -using assms while_option_rule[where P = "%x. g x = g x0" and c = f] -unfolding pfp_def by metis - -lemma strip_lpfpc: assumes "\c. strip(f c) = strip c" and "lpfp\<^sub>c f c = Some c'" -shows "strip c' = c" -using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp\<^sub>c_def]] -by(metis strip_bot_acom) - -lemma lpfpc_least: -assumes mono: "\x y. x \ y \ f x \ f y" -and "strip p = c0" and "f p \ p" and lp: "lpfp\<^sub>c f c0 = Some c" shows "c \ p" -using pfp_least[OF _ _ bot_acom[OF `strip p = c0`] lp[simplified lpfp\<^sub>c_def]] - mono `f p \ p` -by blast - - -subsection "Abstract Interpretation" - -definition \_fun :: "('a \ 'b set) \ ('c \ 'a) \ ('c \ 'b)set" where -"\_fun \ F = {f. \x. f x \ \(F x)}" - -fun \_option :: "('a \ 'b set) \ 'a option \ 'b set" where -"\_option \ None = {}" | -"\_option \ (Some a) = \ a" - -text{* The interface for abstract values: *} - -locale Val_abs = -fixes \ :: "'av::SL_top \ val set" - assumes mono_gamma: "a \ b \ \ a \ \ b" - and gamma_Top[simp]: "\ \ = UNIV" -fixes num' :: "val \ 'av" -and plus' :: "'av \ 'av \ 'av" - assumes gamma_num': "n : \(num' n)" - and gamma_plus': - "n1 : \ a1 \ n2 : \ a2 \ n1+n2 : \(plus' a1 a2)" - -type_synonym 'av st = "(vname \ 'av)" - -locale Abs_Int_Fun = Val_abs \ for \ :: "'av::SL_top \ val set" -begin - -fun aval' :: "aexp \ 'av st \ 'av" where -"aval' (N n) S = num' n" | -"aval' (V x) S = S x" | -"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" - -fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" - where -"step' S (SKIP {P}) = (SKIP {S})" | -"step' S (x ::= e {P}) = - x ::= e {case S of None \ None | Some S \ Some(S(x := aval' e S))}" | -"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" | -"step' S (IF b THEN c1 ELSE c2 {P}) = - IF b THEN step' S c1 ELSE step' S c2 {post c1 \ post c2}" | -"step' S ({Inv} WHILE b DO c {P}) = - {S \ post c} WHILE b DO (step' Inv c) {Inv}" - -definition AI :: "com \ 'av st option acom option" where -"AI = lpfp\<^sub>c (step' \)" - - -lemma strip_step'[simp]: "strip(step' S c) = strip c" -by(induct c arbitrary: S) (simp_all add: Let_def) - - -abbreviation \\<^sub>f :: "'av st \ state set" -where "\\<^sub>f == \_fun \" - -abbreviation \\<^sub>o :: "'av st option \ state set" -where "\\<^sub>o == \_option \\<^sub>f" - -abbreviation \\<^sub>c :: "'av st option acom \ state set acom" -where "\\<^sub>c == map_acom \\<^sub>o" - -lemma gamma_f_Top[simp]: "\\<^sub>f Top = UNIV" -by(simp add: Top_fun_def \_fun_def) - -lemma gamma_o_Top[simp]: "\\<^sub>o Top = UNIV" -by (simp add: Top_option_def) - -(* FIXME (maybe also le \ sqle?) *) - -lemma mono_gamma_f: "f \ g \ \\<^sub>f f \ \\<^sub>f g" -by(auto simp: le_fun_def \_fun_def dest: mono_gamma) - -lemma mono_gamma_o: - "sa \ sa' \ \\<^sub>o sa \ \\<^sub>o sa'" -by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) - -lemma mono_gamma_c: "ca \ ca' \ \\<^sub>c ca \ \\<^sub>c ca'" -by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) - -text{* Soundness: *} - -lemma aval'_sound: "s : \\<^sub>f S \ aval a s : \(aval' a S)" -by (induct a) (auto simp: gamma_num' gamma_plus' \_fun_def) - -lemma in_gamma_update: - "\ s : \\<^sub>f S; i : \ a \ \ s(x := i) : \\<^sub>f(S(x := a))" -by(simp add: \_fun_def) - -lemma step_preserves_le: - "\ S \ \\<^sub>o S'; c \ \\<^sub>c c' \ \ step S c \ \\<^sub>c (step' S' c')" -proof(induction c arbitrary: c' S S') - case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP) -next - case Assign thus ?case - by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update - split: option.splits del:subsetD) -next - case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) - by (metis le_post post_map_acom) -next - case (If b c1 c2 P) - then obtain c1' c2' P' where - "c' = IF b THEN c1' ELSE c2' {P'}" - "P \ \\<^sub>o P'" "c1 \ \\<^sub>c c1'" "c2 \ \\<^sub>c c2'" - by (fastforce simp: If_le map_acom_If) - moreover have "post c1 \ \\<^sub>o(post c1' \ post c2')" - by (metis (no_types) `c1 \ \\<^sub>c c1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom) - moreover have "post c2 \ \\<^sub>o(post c1' \ post c2')" - by (metis (no_types) `c2 \ \\<^sub>c c2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom) - ultimately show ?case using `S \ \\<^sub>o S'` by (simp add: If.IH subset_iff) -next - case (While I b c1 P) - then obtain c1' I' P' where - "c' = {I'} WHILE b DO c1' {P'}" - "I \ \\<^sub>o I'" "P \ \\<^sub>o P'" "c1 \ \\<^sub>c c1'" - by (fastforce simp: map_acom_While While_le) - moreover have "S \ post c1 \ \\<^sub>o (S' \ post c1')" - using `S \ \\<^sub>o S'` le_post[OF `c1 \ \\<^sub>c c1'`, simplified] - by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) - ultimately show ?case by (simp add: While.IH subset_iff) -qed - -lemma AI_sound: "AI c = Some c' \ CS c \ \\<^sub>c c'" -proof(simp add: CS_def AI_def) - assume 1: "lpfp\<^sub>c (step' \) c = Some c'" - have 2: "step' \ c' \ c'" by(rule lpfpc_pfp[OF 1]) - have 3: "strip (\\<^sub>c (step' \ c')) = c" - by(simp add: strip_lpfpc[OF _ 1]) - have "lfp (step UNIV) c \ \\<^sub>c (step' \ c')" - proof(rule lfp_lowerbound[simplified,OF 3]) - show "step UNIV (\\<^sub>c (step' \ c')) \ \\<^sub>c (step' \ c')" - proof(rule step_preserves_le[OF _ _]) - show "UNIV \ \\<^sub>o \" by simp - show "\\<^sub>c (step' \ c') \ \\<^sub>c c'" by(rule mono_gamma_c[OF 2]) - qed - qed - with 2 show "lfp (step UNIV) c \ \\<^sub>c c'" - by (blast intro: mono_gamma_c order_trans) -qed - -end - - -subsubsection "Monotonicity" - -lemma mono_post: "c \ c' \ post c \ post c'" -by(induction c c' rule: le_acom.induct) (auto) - -locale Abs_Int_Fun_mono = Abs_Int_Fun + -assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" -begin - -lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" -by(induction e)(auto simp: le_fun_def mono_plus') - -lemma mono_update: "a \ a' \ S \ S' \ S(x := a) \ S'(x := a')" -by(simp add: le_fun_def) - -lemma mono_step': "S \ S' \ c \ c' \ step' S c \ step' S' c'" -apply(induction c c' arbitrary: S S' rule: le_acom.induct) -apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj - split: option.split) -done - -end - -text{* Problem: not executable because of the comparison of abstract states, -i.e. functions, in the post-fixedpoint computation. *} - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,372 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_Int1_ITP -imports Abs_State_ITP -begin - -subsection "Computable Abstract Interpretation" - -text{* Abstract interpretation over type @{text st} instead of -functions. *} - -context Gamma -begin - -fun aval' :: "aexp \ 'av st \ 'av" where -"aval' (N n) S = num' n" | -"aval' (V x) S = lookup S x" | -"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" - -lemma aval'_sound: "s : \\<^sub>f S \ aval a s : \(aval' a S)" -by (induction a) (auto simp: gamma_num' gamma_plus' \_st_def lookup_def) - -end - -text{* The for-clause (here and elsewhere) only serves the purpose of fixing -the name of the type parameter @{typ 'av} which would otherwise be renamed to -@{typ 'a}. *} - -locale Abs_Int = Gamma where \=\ for \ :: "'av::SL_top \ val set" -begin - -fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" where -"step' S (SKIP {P}) = (SKIP {S})" | -"step' S (x ::= e {P}) = - x ::= e {case S of None \ None | Some S \ Some(update S x (aval' e S))}" | -"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" | -"step' S (IF b THEN c1 ELSE c2 {P}) = - (let c1' = step' S c1; c2' = step' S c2 - in IF b THEN c1' ELSE c2' {post c1 \ post c2})" | -"step' S ({Inv} WHILE b DO c {P}) = - {S \ post c} WHILE b DO step' Inv c {Inv}" - -definition AI :: "com \ 'av st option acom option" where -"AI = lpfp\<^sub>c (step' \)" - - -lemma strip_step'[simp]: "strip(step' S c) = strip c" -by(induct c arbitrary: S) (simp_all add: Let_def) - - -text{* Soundness: *} - -lemma in_gamma_update: - "\ s : \\<^sub>f S; i : \ a \ \ s(x := i) : \\<^sub>f(update S x a)" -by(simp add: \_st_def lookup_update) - -text{* The soundness proofs are textually identical to the ones for the step -function operating on states as functions. *} - -lemma step_preserves_le: - "\ S \ \\<^sub>o S'; c \ \\<^sub>c c' \ \ step S c \ \\<^sub>c (step' S' c')" -proof(induction c arbitrary: c' S S') - case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP) -next - case Assign thus ?case - by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update - split: option.splits del:subsetD) -next - case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) - by (metis le_post post_map_acom) -next - case (If b c1 c2 P) - then obtain c1' c2' P' where - "c' = IF b THEN c1' ELSE c2' {P'}" - "P \ \\<^sub>o P'" "c1 \ \\<^sub>c c1'" "c2 \ \\<^sub>c c2'" - by (fastforce simp: If_le map_acom_If) - moreover have "post c1 \ \\<^sub>o(post c1' \ post c2')" - by (metis (no_types) `c1 \ \\<^sub>c c1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom) - moreover have "post c2 \ \\<^sub>o(post c1' \ post c2')" - by (metis (no_types) `c2 \ \\<^sub>c c2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom) - ultimately show ?case using `S \ \\<^sub>o S'` by (simp add: If.IH subset_iff) -next - case (While I b c1 P) - then obtain c1' I' P' where - "c' = {I'} WHILE b DO c1' {P'}" - "I \ \\<^sub>o I'" "P \ \\<^sub>o P'" "c1 \ \\<^sub>c c1'" - by (fastforce simp: map_acom_While While_le) - moreover have "S \ post c1 \ \\<^sub>o (S' \ post c1')" - using `S \ \\<^sub>o S'` le_post[OF `c1 \ \\<^sub>c c1'`, simplified] - by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) - ultimately show ?case by (simp add: While.IH subset_iff) -qed - -lemma AI_sound: "AI c = Some c' \ CS c \ \\<^sub>c c'" -proof(simp add: CS_def AI_def) - assume 1: "lpfp\<^sub>c (step' \) c = Some c'" - have 2: "step' \ c' \ c'" by(rule lpfpc_pfp[OF 1]) - have 3: "strip (\\<^sub>c (step' \ c')) = c" - by(simp add: strip_lpfpc[OF _ 1]) - have "lfp (step UNIV) c \ \\<^sub>c (step' \ c')" - proof(rule lfp_lowerbound[simplified,OF 3]) - show "step UNIV (\\<^sub>c (step' \ c')) \ \\<^sub>c (step' \ c')" - proof(rule step_preserves_le[OF _ _]) - show "UNIV \ \\<^sub>o \" by simp - show "\\<^sub>c (step' \ c') \ \\<^sub>c c'" by(rule mono_gamma_c[OF 2]) - qed - qed - from this 2 show "lfp (step UNIV) c \ \\<^sub>c c'" - by (blast intro: mono_gamma_c order_trans) -qed - -end - - -subsubsection "Monotonicity" - -locale Abs_Int_mono = Abs_Int + -assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" -begin - -lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" -by(induction e) (auto simp: le_st_def lookup_def mono_plus') - -lemma mono_update: "a \ a' \ S \ S' \ update S x a \ update S' x a'" -by(auto simp add: le_st_def lookup_def update_def) - -lemma mono_step': "S \ S' \ c \ c' \ step' S c \ step' S' c'" -apply(induction c c' arbitrary: S S' rule: le_acom.induct) -apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj - split: option.split) -done - -end - - -subsubsection "Ascending Chain Condition" - -abbreviation "strict r == r \ -(r^-1)" -abbreviation "acc r == wf((strict r)^-1)" - -lemma strict_inv_image: "strict(inv_image r f) = inv_image (strict r) f" -by(auto simp: inv_image_def) - -lemma acc_inv_image: - "acc r \ acc (inv_image r f)" -by (metis converse_inv_image strict_inv_image wf_inv_image) - -text{* ACC for option type: *} - -lemma acc_option: assumes "acc {(x,y::'a::preord). x \ y}" -shows "acc {(x,y::'a::preord option). x \ y}" -proof(auto simp: wf_eq_minimal) - fix xo :: "'a option" and Qo assume "xo : Qo" - let ?Q = "{x. Some x \ Qo}" - show "\yo\Qo. \zo. yo \ zo \ ~ zo \ yo \ zo \ Qo" (is "\zo\Qo. ?P zo") - proof cases - assume "?Q = {}" - hence "?P None" by auto - moreover have "None \ Qo" using `?Q = {}` `xo : Qo` - by auto (metis not_Some_eq) - ultimately show ?thesis by blast - next - assume "?Q \ {}" - with assms show ?thesis - apply(auto simp: wf_eq_minimal) - apply(erule_tac x="?Q" in allE) - apply auto - apply(rule_tac x = "Some z" in bexI) - by auto - qed -qed - -text{* ACC for abstract states, via measure functions. *} - -lemma measure_st: assumes "(strict{(x,y::'a::SL_top). x \ y})^-1 <= measure m" -and "\x y::'a::SL_top. x \ y \ y \ x \ m x = m y" -shows "(strict{(S,S'::'a::SL_top st). S \ S'})^-1 \ - measure(%fd. \x| x\set(dom fd) \ ~ \ \ fun fd x. m(fun fd x)+1)" -proof- - { fix S S' :: "'a st" assume "S \ S'" "~ S' \ S" - let ?X = "set(dom S)" let ?Y = "set(dom S')" - let ?f = "fun S" let ?g = "fun S'" - let ?X' = "{x:?X. ~ \ \ ?f x}" let ?Y' = "{y:?Y. ~ \ \ ?g y}" - from `S \ S'` have "ALL y:?Y'\?X. ?f y \ ?g y" - by(auto simp: le_st_def lookup_def) - hence 1: "ALL y:?Y'\?X. m(?g y)+1 \ m(?f y)+1" - using assms(1,2) by(fastforce) - from `~ S' \ S` obtain u where u: "u : ?X" "~ lookup S' u \ ?f u" - by(auto simp: le_st_def) - hence "u : ?X'" by simp (metis preord_class.le_trans top) - have "?Y'-?X = {}" using `S \ S'` by(fastforce simp: le_st_def lookup_def) - have "?Y'\?X <= ?X'" apply auto - apply (metis `S \ S'` le_st_def lookup_def preord_class.le_trans) - done - have "(\y\?Y'. m(?g y)+1) = (\y\(?Y'-?X) \ (?Y'\?X). m(?g y)+1)" - by (metis Un_Diff_Int) - also have "\ = (\y\?Y'\?X. m(?g y)+1)" - using `?Y'-?X = {}` by (metis Un_empty_left) - also have "\ < (\x\?X'. m(?f x)+1)" - proof cases - assume "u \ ?Y'" - hence "m(?g u) < m(?f u)" using assms(1) `S \ S'` u - by (fastforce simp: le_st_def lookup_def) - have "(\y\?Y'\?X. m(?g y)+1) < (\y\?Y'\?X. m(?f y)+1)" - using `u:?X` `u:?Y'` `m(?g u) < m(?f u)` - by(fastforce intro!: sum_strict_mono_ex1[OF _ 1]) - also have "\ \ (\y\?X'. m(?f y)+1)" - by(simp add: sum_mono3[OF _ `?Y'\?X <= ?X'`]) - finally show ?thesis . - next - assume "u \ ?Y'" - with `?Y'\?X <= ?X'` have "?Y'\?X - {u} <= ?X' - {u}" by blast - have "(\y\?Y'\?X. m(?g y)+1) = (\y\?Y'\?X - {u}. m(?g y)+1)" - proof- - have "?Y'\?X = ?Y'\?X - {u}" using `u \ ?Y'` by auto - thus ?thesis by metis - qed - also have "\ < (\y\?Y'\?X-{u}. m(?g y)+1) + (\y\{u}. m(?f y)+1)" by simp - also have "(\y\?Y'\?X-{u}. m(?g y)+1) \ (\y\?Y'\?X-{u}. m(?f y)+1)" - using 1 by(blast intro: sum_mono) - also have "\ \ (\y\?X'-{u}. m(?f y)+1)" - by(simp add: sum_mono3[OF _ `?Y'\?X-{u} <= ?X'-{u}`]) - also have "\ + (\y\{u}. m(?f y)+1)= (\y\(?X'-{u}) \ {u}. m(?f y)+1)" - using `u:?X'` by(subst sum.union_disjoint[symmetric]) auto - also have "\ = (\x\?X'. m(?f x)+1)" - using `u : ?X'` by(simp add:insert_absorb) - finally show ?thesis by (blast intro: add_right_mono) - qed - finally have "(\y\?Y'. m(?g y)+1) < (\x\?X'. m(?f x)+1)" . - } thus ?thesis by(auto simp add: measure_def inv_image_def) -qed - -text{* ACC for acom. First the ordering on acom is related to an ordering on -lists of annotations. *} - -(* FIXME mv and add [simp] *) -lemma listrel_Cons_iff: - "(x#xs, y#ys) : listrel r \ (x,y) \ r \ (xs,ys) \ listrel r" -by (blast intro:listrel.Cons) - -lemma listrel_app: "(xs1,ys1) : listrel r \ (xs2,ys2) : listrel r - \ (xs1@xs2, ys1@ys2) : listrel r" -by(auto simp add: listrel_iff_zip) - -lemma listrel_app_same_size: "size xs1 = size ys1 \ size xs2 = size ys2 \ - (xs1@xs2, ys1@ys2) : listrel r \ - (xs1,ys1) : listrel r \ (xs2,ys2) : listrel r" -by(auto simp add: listrel_iff_zip) - -lemma listrel_converse: "listrel(r^-1) = (listrel r)^-1" -proof- - { fix xs ys - have "(xs,ys) : listrel(r^-1) \ (ys,xs) : listrel r" - apply(induct xs arbitrary: ys) - apply (fastforce simp: listrel.Nil) - apply (fastforce simp: listrel_Cons_iff) - done - } thus ?thesis by auto -qed - -(* It would be nice to get rid of refl & trans and build them into the proof *) -lemma acc_listrel: fixes r :: "('a*'a)set" assumes "refl r" and "trans r" -and "acc r" shows "acc (listrel r - {([],[])})" -proof- - have refl: "!!x. (x,x) : r" using `refl r` unfolding refl_on_def by blast - have trans: "!!x y z. (x,y) : r \ (y,z) : r \ (x,z) : r" - using `trans r` unfolding trans_def by blast - from assms(3) obtain mx :: "'a set \ 'a" where - mx: "!!S x. x:S \ mx S : S \ (\y. (mx S,y) : strict r \ y \ S)" - by(simp add: wf_eq_minimal) metis - let ?R = "listrel r - {([], [])}" - { fix Q and xs :: "'a list" - have "xs \ Q \ \ys. ys\Q \ (\zs. (ys, zs) \ strict ?R \ zs \ Q)" - (is "_ \ \ys. ?P Q ys") - proof(induction xs arbitrary: Q rule: length_induct) - case (1 xs) - { have "!!ys Q. size ys < size xs \ ys : Q \ EX ms. ?P Q ms" - using "1.IH" by blast - } note IH = this - show ?case - proof(cases xs) - case Nil with `xs : Q` have "?P Q []" by auto - thus ?thesis by blast - next - case (Cons x ys) - let ?Q1 = "{a. \bs. size bs = size ys \ a#bs : Q}" - have "x : ?Q1" using `xs : Q` Cons by auto - from mx[OF this] obtain m1 where - 1: "m1 \ ?Q1 \ (\y. (m1,y) \ strict r \ y \ ?Q1)" by blast - then obtain ms1 where "size ms1 = size ys" "m1#ms1 : Q" by blast+ - hence "size ms1 < size xs" using Cons by auto - let ?Q2 = "{bs. \m1'. (m1',m1):r \ (m1,m1'):r \ m1'#bs : Q \ size bs = size ms1}" - have "ms1 : ?Q2" using `m1#ms1 : Q` by(blast intro: refl) - from IH[OF `size ms1 < size xs` this] - obtain ms where 2: "?P ?Q2 ms" by auto - then obtain m1' where m1': "(m1',m1) : r \ (m1,m1') : r \ m1'#ms : Q" - by blast - hence "\ab. (m1'#ms,ab) : strict ?R \ ab \ Q" using 1 2 - apply (auto simp: listrel_Cons_iff) - apply (metis `length ms1 = length ys` listrel_eq_len trans) - by (metis `length ms1 = length ys` listrel_eq_len trans) - with m1' show ?thesis by blast - qed - qed - } - thus ?thesis unfolding wf_eq_minimal by (metis converse_iff) -qed - - -lemma le_iff_le_annos: "c1 \ c2 \ - (annos c1, annos c2) : listrel{(x,y). x \ y} \ strip c1 = strip c2" -apply(induct c1 c2 rule: le_acom.induct) -apply (auto simp: listrel.Nil listrel_Cons_iff listrel_app size_annos_same2) -apply (metis listrel_app_same_size size_annos_same)+ -done - -lemma le_acom_subset_same_annos: - "(strict{(c,c'::'a::preord acom). c \ c'})^-1 \ - (strict(inv_image (listrel{(a,a'::'a). a \ a'} - {([],[])}) annos))^-1" -by(auto simp: le_iff_le_annos) - -lemma acc_acom: "acc {(a,a'::'a::preord). a \ a'} \ - acc {(c,c'::'a acom). c \ c'}" -apply(rule wf_subset[OF _ le_acom_subset_same_annos]) -apply(rule acc_inv_image[OF acc_listrel]) -apply(auto simp: refl_on_def trans_def intro: le_trans) -done - -text{* Termination of the fixed-point finders, assuming monotone functions: *} - -lemma pfp_termination: -fixes x0 :: "'a::preord" -assumes mono: "\x y. x \ y \ f x \ f y" and "acc {(x::'a,y). x \ y}" -and "x0 \ f x0" shows "EX x. pfp f x0 = Some x" -proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. x \ f x"]) - show "wf {(x, s). (s \ f s \ \ f s \ s) \ x = f s}" - by(rule wf_subset[OF assms(2)]) auto -next - show "x0 \ f x0" by(rule assms) -next - fix x assume "x \ f x" thus "f x \ f(f x)" by(rule mono) -qed - -lemma lpfpc_termination: - fixes f :: "(('a::SL_top)option acom \ 'a option acom)" - assumes "acc {(x::'a,y). x \ y}" and "\x y. x \ y \ f x \ f y" - and "\c. strip(f c) = strip c" - shows "\c'. lpfp\<^sub>c f c = Some c'" -unfolding lpfp\<^sub>c_def -apply(rule pfp_termination) - apply(erule assms(2)) - apply(rule acc_acom[OF acc_option[OF assms(1)]]) -apply(simp add: bot_acom assms(3)) -done - -context Abs_Int_mono -begin - -lemma AI_Some_measure: -assumes "(strict{(x,y::'a). x \ y})^-1 <= measure m" -and "\x y::'a. x \ y \ y \ x \ m x = m y" -shows "\c'. AI c = Some c'" -unfolding AI_def -apply(rule lpfpc_termination) -apply(rule wf_subset[OF wf_measure measure_st[OF assms]]) -apply(erule mono_step'[OF le_refl]) -apply(rule strip_step') -done - -end - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,139 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_Int1_const_ITP -imports Abs_Int1_ITP "../Abs_Int_Tests" -begin - -subsection "Constant Propagation" - -datatype const = Const val | Any - -fun \_const where -"\_const (Const n) = {n}" | -"\_const (Any) = UNIV" - -fun plus_const where -"plus_const (Const m) (Const n) = Const(m+n)" | -"plus_const _ _ = Any" - -lemma plus_const_cases: "plus_const a1 a2 = - (case (a1,a2) of (Const m, Const n) \ Const(m+n) | _ \ Any)" -by(auto split: prod.split const.split) - -instantiation const :: SL_top -begin - -fun le_const where -"_ \ Any = True" | -"Const n \ Const m = (n=m)" | -"Any \ Const _ = False" - -fun join_const where -"Const m \ Const n = (if n=m then Const m else Any)" | -"_ \ _ = Any" - -definition "\ = Any" - -instance -proof - case goal1 thus ?case by (cases x) simp_all -next - case goal2 thus ?case by(cases z, cases y, cases x, simp_all) -next - case goal3 thus ?case by(cases x, cases y, simp_all) -next - case goal4 thus ?case by(cases y, cases x, simp_all) -next - case goal5 thus ?case by(cases z, cases y, cases x, simp_all) -next - case goal6 thus ?case by(simp add: Top_const_def) -qed - -end - - -global_interpretation Val_abs -where \ = \_const and num' = Const and plus' = plus_const -proof - case goal1 thus ?case - by(cases a, cases b, simp, simp, cases b, simp, simp) -next - case goal2 show ?case by(simp add: Top_const_def) -next - case goal3 show ?case by simp -next - case goal4 thus ?case - by(auto simp: plus_const_cases split: const.split) -qed - -global_interpretation Abs_Int -where \ = \_const and num' = Const and plus' = plus_const -defines AI_const = AI and step_const = step' and aval'_const = aval' -.. - - -subsubsection "Tests" - -value "show_acom (((step_const \)^^0) (\\<^sub>c test1_const))" -value "show_acom (((step_const \)^^1) (\\<^sub>c test1_const))" -value "show_acom (((step_const \)^^2) (\\<^sub>c test1_const))" -value "show_acom (((step_const \)^^3) (\\<^sub>c test1_const))" -value "show_acom_opt (AI_const test1_const)" - -value "show_acom_opt (AI_const test2_const)" -value "show_acom_opt (AI_const test3_const)" - -value "show_acom (((step_const \)^^0) (\\<^sub>c test4_const))" -value "show_acom (((step_const \)^^1) (\\<^sub>c test4_const))" -value "show_acom (((step_const \)^^2) (\\<^sub>c test4_const))" -value "show_acom (((step_const \)^^3) (\\<^sub>c test4_const))" -value "show_acom_opt (AI_const test4_const)" - -value "show_acom (((step_const \)^^0) (\\<^sub>c test5_const))" -value "show_acom (((step_const \)^^1) (\\<^sub>c test5_const))" -value "show_acom (((step_const \)^^2) (\\<^sub>c test5_const))" -value "show_acom (((step_const \)^^3) (\\<^sub>c test5_const))" -value "show_acom (((step_const \)^^4) (\\<^sub>c test5_const))" -value "show_acom (((step_const \)^^5) (\\<^sub>c test5_const))" -value "show_acom_opt (AI_const test5_const)" - -value "show_acom (((step_const \)^^0) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^1) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^2) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^3) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^4) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^5) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^6) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^7) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^8) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^9) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^10) (\\<^sub>c test6_const))" -value "show_acom (((step_const \)^^11) (\\<^sub>c test6_const))" -value "show_acom_opt (AI_const test6_const)" - - -text{* Monotonicity: *} - -global_interpretation Abs_Int_mono -where \ = \_const and num' = Const and plus' = plus_const -proof - case goal1 thus ?case - by(auto simp: plus_const_cases split: const.split) -qed - -text{* Termination: *} - -definition "m_const x = (case x of Const _ \ 1 | Any \ 0)" - -lemma measure_const: - "(strict{(x::const,y). x \ y})^-1 \ measure m_const" -by(auto simp: m_const_def split: const.splits) - -lemma measure_const_eq: - "\ x y::const. x \ y \ y \ x \ m_const x = m_const y" -by(auto simp: m_const_def split: const.splits) - -lemma "EX c'. AI_const c = Some c'" -by(rule AI_Some_measure[OF measure_const measure_const_eq]) - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,168 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_Int1_parity_ITP -imports Abs_Int1_ITP -begin - -subsection "Parity Analysis" - -datatype parity = Even | Odd | Either - -text{* Instantiation of class @{class preord} with type @{typ parity}: *} - -instantiation parity :: preord -begin - -text{* First the definition of the interface function @{text"\"}. Note that -the header of the definition must refer to the ascii name @{const le} of the -constants as @{text le_parity} and the definition is named @{text -le_parity_def}. Inside the definition the symbolic names can be used. *} - -definition le_parity where -"x \ y = (y = Either \ x=y)" - -text{* Now the instance proof, i.e.\ the proof that the definition fulfills -the axioms (assumptions) of the class. The initial proof-step generates the -necessary proof obligations. *} - -instance -proof - fix x::parity show "x \ x" by(auto simp: le_parity_def) -next - fix x y z :: parity assume "x \ y" "y \ z" thus "x \ z" - by(auto simp: le_parity_def) -qed - -end - -text{* Instantiation of class @{class SL_top} with type @{typ parity}: *} - -instantiation parity :: SL_top -begin - - -definition join_parity where -"x \ y = (if x \ y then y else if y \ x then x else Either)" - -definition Top_parity where -"\ = Either" - -text{* Now the instance proof. This time we take a lazy shortcut: we do not -write out the proof obligations but use the @{text goali} primitive to refer -to the assumptions of subgoal i and @{text "case?"} to refer to the -conclusion of subgoal i. The class axioms are presented in the same order as -in the class definition. *} - -instance -proof - case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def) -next - case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def) -next - case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def) -next - case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def) -qed - -end - - -text{* Now we define the functions used for instantiating the abstract -interpretation locales. Note that the Isabelle terminology is -\emph{interpretation}, not \emph{instantiation} of locales, but we use -instantiation to avoid confusion with abstract interpretation. *} - -fun \_parity :: "parity \ val set" where -"\_parity Even = {i. i mod 2 = 0}" | -"\_parity Odd = {i. i mod 2 = 1}" | -"\_parity Either = UNIV" - -fun num_parity :: "val \ parity" where -"num_parity i = (if i mod 2 = 0 then Even else Odd)" - -fun plus_parity :: "parity \ parity \ parity" where -"plus_parity Even Even = Even" | -"plus_parity Odd Odd = Even" | -"plus_parity Even Odd = Odd" | -"plus_parity Odd Even = Odd" | -"plus_parity Either y = Either" | -"plus_parity x Either = Either" - -text{* First we instantiate the abstract value interface and prove that the -functions on type @{typ parity} have all the necessary properties: *} - -interpretation Val_abs -where \ = \_parity and num' = num_parity and plus' = plus_parity -proof txt{* of the locale axioms *} - fix a b :: parity - assume "a \ b" thus "\_parity a \ \_parity b" - by(auto simp: le_parity_def) -next txt{* The rest in the lazy, implicit way *} - case goal2 show ?case by(auto simp: Top_parity_def) -next - case goal3 show ?case by auto -next - txt{* Warning: this subproof refers to the names @{text a1} and @{text a2} - from the statement of the axiom. *} - case goal4 thus ?case - proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust]) - qed (auto simp add:mod_add_eq) -qed - -text{* Instantiating the abstract interpretation locale requires no more -proofs (they happened in the instatiation above) but delivers the -instantiated abstract interpreter which we call AI: *} - -global_interpretation Abs_Int -where \ = \_parity and num' = num_parity and plus' = plus_parity -defines aval_parity = aval' and step_parity = step' and AI_parity = AI -.. - - -subsubsection "Tests" - -definition "test1_parity = - ''x'' ::= N 1;; - WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" - -value "show_acom_opt (AI_parity test1_parity)" - -definition "test2_parity = - ''x'' ::= N 1;; - WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)" - -value "show_acom ((step_parity \ ^^1) (anno None test2_parity))" -value "show_acom ((step_parity \ ^^2) (anno None test2_parity))" -value "show_acom ((step_parity \ ^^3) (anno None test2_parity))" -value "show_acom ((step_parity \ ^^4) (anno None test2_parity))" -value "show_acom ((step_parity \ ^^5) (anno None test2_parity))" -value "show_acom_opt (AI_parity test2_parity)" - - -subsubsection "Termination" - -global_interpretation Abs_Int_mono -where \ = \_parity and num' = num_parity and plus' = plus_parity -proof - case goal1 thus ?case - proof(cases a1 a2 b1 b2 - rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *) - qed (auto simp add:le_parity_def) -qed - - -definition m_parity :: "parity \ nat" where -"m_parity x = (if x=Either then 0 else 1)" - -lemma measure_parity: - "(strict{(x::parity,y). x \ y})^-1 \ measure m_parity" -by(auto simp add: m_parity_def le_parity_def) - -lemma measure_parity_eq: - "\x y::parity. x \ y \ y \ x \ m_parity x = m_parity y" -by(auto simp add: m_parity_def le_parity_def) - -lemma AI_parity_Some: "\c'. AI_parity c = Some c'" -by(rule AI_Some_measure[OF measure_parity measure_parity_eq]) - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,340 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_Int2_ITP -imports Abs_Int1_ITP "../Vars" -begin - -instantiation prod :: (preord,preord) preord -begin - -definition "le_prod p1 p2 = (fst p1 \ fst p2 \ snd p1 \ snd p2)" - -instance -proof - case goal1 show ?case by(simp add: le_prod_def) -next - case goal2 thus ?case unfolding le_prod_def by(metis le_trans) -qed - -end - - -subsection "Backward Analysis of Expressions" - -hide_const bot - -class L_top_bot = SL_top + -fixes meet :: "'a \ 'a \ 'a" (infixl "\" 65) -and bot :: "'a" ("\") -assumes meet_le1 [simp]: "x \ y \ x" -and meet_le2 [simp]: "x \ y \ y" -and meet_greatest: "x \ y \ x \ z \ x \ y \ z" -assumes bot[simp]: "\ \ x" -begin - -lemma mono_meet: "x \ x' \ y \ y' \ x \ y \ x' \ y'" -by (metis meet_greatest meet_le1 meet_le2 le_trans) - -end - -locale Val_abs1_gamma = - Gamma where \ = \ for \ :: "'av::L_top_bot \ val set" + -assumes inter_gamma_subset_gamma_meet: - "\ a1 \ \ a2 \ \(a1 \ a2)" -and gamma_Bot[simp]: "\ \ = {}" -begin - -lemma in_gamma_meet: "x : \ a1 \ x : \ a2 \ x : \(a1 \ a2)" -by (metis IntI inter_gamma_subset_gamma_meet set_mp) - -lemma gamma_meet[simp]: "\(a1 \ a2) = \ a1 \ \ a2" -by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2) - -end - - -locale Val_abs1 = - Val_abs1_gamma where \ = \ - for \ :: "'av::L_top_bot \ val set" + -fixes test_num' :: "val \ 'av \ bool" -and filter_plus' :: "'av \ 'av \ 'av \ 'av * 'av" -and filter_less' :: "bool \ 'av \ 'av \ 'av * 'av" -assumes test_num': "test_num' n a = (n : \ a)" -and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \ - n1 : \ a1 \ n2 : \ a2 \ n1+n2 : \ a \ n1 : \ b1 \ n2 : \ b2" -and filter_less': "filter_less' (n1 - n1 : \ a1 \ n2 : \ a2 \ n1 : \ b1 \ n2 : \ b2" - - -locale Abs_Int1 = - Val_abs1 where \ = \ for \ :: "'av::L_top_bot \ val set" -begin - -lemma in_gamma_join_UpI: "s : \\<^sub>o S1 \ s : \\<^sub>o S2 \ s : \\<^sub>o(S1 \ S2)" -by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp) - -fun aval'' :: "aexp \ 'av st option \ 'av" where -"aval'' e None = \" | -"aval'' e (Some sa) = aval' e sa" - -lemma aval''_sound: "s : \\<^sub>o S \ aval a s : \(aval'' a S)" -by(cases S)(simp add: aval'_sound)+ - -subsubsection "Backward analysis" - -fun afilter :: "aexp \ 'av \ 'av st option \ 'av st option" where -"afilter (N n) a S = (if test_num' n a then S else None)" | -"afilter (V x) a S = (case S of None \ None | Some S \ - let a' = lookup S x \ a in - if a' \ \ then None else Some(update S x a'))" | -"afilter (Plus e1 e2) a S = - (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S) - in afilter e1 a1 (afilter e2 a2 S))" - -text{* The test for @{const bot} in the @{const V}-case is important: @{const -bot} indicates that a variable has no possible values, i.e.\ that the current -program point is unreachable. But then the abstract state should collapse to -@{const None}. Put differently, we maintain the invariant that in an abstract -state of the form @{term"Some s"}, all variables are mapped to non-@{const -bot} values. Otherwise the (pointwise) join of two abstract states, one of -which contains @{const bot} values, may produce too large a result, thus -making the analysis less precise. *} - - -fun bfilter :: "bexp \ bool \ 'av st option \ 'av st option" where -"bfilter (Bc v) res S = (if v=res then S else None)" | -"bfilter (Not b) res S = bfilter b (\ res) S" | -"bfilter (And b1 b2) res S = - (if res then bfilter b1 True (bfilter b2 True S) - else bfilter b1 False S \ bfilter b2 False S)" | -"bfilter (Less e1 e2) res S = - (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S) - in afilter e1 res1 (afilter e2 res2 S))" - -lemma afilter_sound: "s : \\<^sub>o S \ aval e s : \ a \ s : \\<^sub>o (afilter e a S)" -proof(induction e arbitrary: a S) - case N thus ?case by simp (metis test_num') -next - case (V x) - obtain S' where "S = Some S'" and "s : \\<^sub>f S'" using `s : \\<^sub>o S` - by(auto simp: in_gamma_option_iff) - moreover hence "s x : \ (lookup S' x)" by(simp add: \_st_def) - moreover have "s x : \ a" using V by simp - ultimately show ?case using V(1) - by(simp add: lookup_update Let_def \_st_def) - (metis mono_gamma emptyE in_gamma_meet gamma_Bot subset_empty) -next - case (Plus e1 e2) thus ?case - using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]] - by (auto split: prod.split) -qed - -lemma bfilter_sound: "s : \\<^sub>o S \ bv = bval b s \ s : \\<^sub>o(bfilter b bv S)" -proof(induction b arbitrary: S bv) - case Bc thus ?case by simp -next - case (Not b) thus ?case by simp -next - case (And b1 b2) thus ?case - apply hypsubst_thin - apply (fastforce simp: in_gamma_join_UpI) - done -next - case (Less e1 e2) thus ?case - apply hypsubst_thin - apply (auto split: prod.split) - apply (metis afilter_sound filter_less' aval''_sound Less) - done -qed - - -fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" - where -"step' S (SKIP {P}) = (SKIP {S})" | -"step' S (x ::= e {P}) = - x ::= e {case S of None \ None | Some S \ Some(update S x (aval' e S))}" | -"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" | -"step' S (IF b THEN c1 ELSE c2 {P}) = - (let c1' = step' (bfilter b True S) c1; c2' = step' (bfilter b False S) c2 - in IF b THEN c1' ELSE c2' {post c1 \ post c2})" | -"step' S ({Inv} WHILE b DO c {P}) = - {S \ post c} - WHILE b DO step' (bfilter b True Inv) c - {bfilter b False Inv}" - -definition AI :: "com \ 'av st option acom option" where -"AI = lpfp\<^sub>c (step' \)" - -lemma strip_step'[simp]: "strip(step' S c) = strip c" -by(induct c arbitrary: S) (simp_all add: Let_def) - - -subsubsection "Soundness" - -lemma in_gamma_update: - "\ s : \\<^sub>f S; i : \ a \ \ s(x := i) : \\<^sub>f(update S x a)" -by(simp add: \_st_def lookup_update) - -lemma step_preserves_le: - "\ S \ \\<^sub>o S'; cs \ \\<^sub>c ca \ \ step S cs \ \\<^sub>c (step' S' ca)" -proof(induction cs arbitrary: ca S S') - case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP) -next - case Assign thus ?case - by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update - split: option.splits del:subsetD) -next - case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) - by (metis le_post post_map_acom) -next - case (If b cs1 cs2 P) - then obtain ca1 ca2 Pa where - "ca= IF b THEN ca1 ELSE ca2 {Pa}" - "P \ \\<^sub>o Pa" "cs1 \ \\<^sub>c ca1" "cs2 \ \\<^sub>c ca2" - by (fastforce simp: If_le map_acom_If) - moreover have "post cs1 \ \\<^sub>o(post ca1 \ post ca2)" - by (metis (no_types) `cs1 \ \\<^sub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom) - moreover have "post cs2 \ \\<^sub>o(post ca1 \ post ca2)" - by (metis (no_types) `cs2 \ \\<^sub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom) - ultimately show ?case using `S \ \\<^sub>o S'` - by (simp add: If.IH subset_iff bfilter_sound) -next - case (While I b cs1 P) - then obtain ca1 Ia Pa where - "ca = {Ia} WHILE b DO ca1 {Pa}" - "I \ \\<^sub>o Ia" "P \ \\<^sub>o Pa" "cs1 \ \\<^sub>c ca1" - by (fastforce simp: map_acom_While While_le) - moreover have "S \ post cs1 \ \\<^sub>o (S' \ post ca1)" - using `S \ \\<^sub>o S'` le_post[OF `cs1 \ \\<^sub>c ca1`, simplified] - by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) - ultimately show ?case by (simp add: While.IH subset_iff bfilter_sound) -qed - -lemma AI_sound: "AI c = Some c' \ CS c \ \\<^sub>c c'" -proof(simp add: CS_def AI_def) - assume 1: "lpfp\<^sub>c (step' \) c = Some c'" - have 2: "step' \ c' \ c'" by(rule lpfpc_pfp[OF 1]) - have 3: "strip (\\<^sub>c (step' \ c')) = c" - by(simp add: strip_lpfpc[OF _ 1]) - have "lfp (step UNIV) c \ \\<^sub>c (step' \ c')" - proof(rule lfp_lowerbound[simplified,OF 3]) - show "step UNIV (\\<^sub>c (step' \ c')) \ \\<^sub>c (step' \ c')" - proof(rule step_preserves_le[OF _ _]) - show "UNIV \ \\<^sub>o \" by simp - show "\\<^sub>c (step' \ c') \ \\<^sub>c c'" by(rule mono_gamma_c[OF 2]) - qed - qed - from this 2 show "lfp (step UNIV) c \ \\<^sub>c c'" - by (blast intro: mono_gamma_c order_trans) -qed - - -subsubsection "Commands over a set of variables" - -text{* Key invariant: the domains of all abstract states are subsets of the -set of variables of the program. *} - -definition "domo S = (case S of None \ {} | Some S' \ set(dom S'))" - -definition Com :: "vname set \ 'a st option acom set" where -"Com X = {c. \S \ set(annos c). domo S \ X}" - -lemma domo_Top[simp]: "domo \ = {}" -by(simp add: domo_def Top_st_def Top_option_def) - -lemma bot_acom_Com[simp]: "\\<^sub>c c \ Com X" -by(simp add: bot_acom_def Com_def domo_def set_annos_anno) - -lemma post_in_annos: "post c : set(annos c)" -by(induction c) simp_all - -lemma domo_join: "domo (S \ T) \ domo S \ domo T" -by(auto simp: domo_def join_st_def split: option.split) - -lemma domo_afilter: "vars a \ X \ domo S \ X \ domo(afilter a i S) \ X" -apply(induction a arbitrary: i S) -apply(simp add: domo_def) -apply(simp add: domo_def Let_def update_def lookup_def split: option.splits) -apply blast -apply(simp split: prod.split) -done - -lemma domo_bfilter: "vars b \ X \ domo S \ X \ domo(bfilter b bv S) \ X" -apply(induction b arbitrary: bv S) -apply(simp add: domo_def) -apply(simp) -apply(simp) -apply rule -apply (metis le_sup_iff subset_trans[OF domo_join]) -apply(simp split: prod.split) -by (metis domo_afilter) - -lemma step'_Com: - "domo S \ X \ vars(strip c) \ X \ c : Com X \ step' S c : Com X" -apply(induction c arbitrary: S) -apply(simp add: Com_def) -apply(simp add: Com_def domo_def update_def split: option.splits) -apply(simp (no_asm_use) add: Com_def ball_Un) -apply (metis post_in_annos) -apply(simp (no_asm_use) add: Com_def ball_Un) -apply rule -apply (metis Un_assoc domo_join order_trans post_in_annos subset_Un_eq) -apply (metis domo_bfilter) -apply(simp (no_asm_use) add: Com_def) -apply rule -apply (metis domo_join le_sup_iff post_in_annos subset_trans) -apply rule -apply (metis domo_bfilter) -by (metis domo_bfilter) - -end - - -subsubsection "Monotonicity" - -locale Abs_Int1_mono = Abs_Int1 + -assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" -and mono_filter_plus': "a1 \ b1 \ a2 \ b2 \ r \ r' \ - filter_plus' r a1 a2 \ filter_plus' r' b1 b2" -and mono_filter_less': "a1 \ b1 \ a2 \ b2 \ - filter_less' bv a1 a2 \ filter_less' bv b1 b2" -begin - -lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" -by(induction e) (auto simp: le_st_def lookup_def mono_plus') - -lemma mono_aval'': "S \ S' \ aval'' e S \ aval'' e S'" -apply(cases S) - apply simp -apply(cases S') - apply simp -by (simp add: mono_aval') - -lemma mono_afilter: "r \ r' \ S \ S' \ afilter e r S \ afilter e r' S'" -apply(induction e arbitrary: r r' S S') -apply(auto simp: test_num' Let_def split: option.splits prod.splits) -apply (metis mono_gamma subsetD) -apply(rename_tac list a b c d, drule_tac x = "list" in mono_lookup) -apply (metis mono_meet le_trans) -apply (metis mono_meet mono_lookup mono_update) -apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv) -done - -lemma mono_bfilter: "S \ S' \ bfilter b r S \ bfilter b r S'" -apply(induction b arbitrary: r S S') -apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits) -apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv) -done - -lemma mono_step': "S \ S' \ c \ c' \ step' S c \ step' S' c'" -apply(induction c c' arbitrary: S S' rule: le_acom.induct) -apply (auto simp: mono_post mono_bfilter mono_update mono_aval' Let_def le_join_disj - split: option.split) -done - -lemma mono_step'2: "mono (step' S)" -by(simp add: mono_def mono_step'[OF le_refl]) - -end - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,285 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_Int2_ivl_ITP -imports Abs_Int2_ITP "../Abs_Int_Tests" -begin - -subsection "Interval Analysis" - -datatype ivl = I "int option" "int option" - -definition "\_ivl i = (case i of - I (Some l) (Some h) \ {l..h} | - I (Some l) None \ {l..} | - I None (Some h) \ {..h} | - I None None \ UNIV)" - -abbreviation I_Some_Some :: "int \ int \ ivl" ("{_\_}") where -"{lo\hi} == I (Some lo) (Some hi)" -abbreviation I_Some_None :: "int \ ivl" ("{_\}") where -"{lo\} == I (Some lo) None" -abbreviation I_None_Some :: "int \ ivl" ("{\_}") where -"{\hi} == I None (Some hi)" -abbreviation I_None_None :: "ivl" ("{\}") where -"{\} == I None None" - -definition "num_ivl n = {n\n}" - -fun in_ivl :: "int \ ivl \ bool" where -"in_ivl k (I (Some l) (Some h)) \ l \ k \ k \ h" | -"in_ivl k (I (Some l) None) \ l \ k" | -"in_ivl k (I None (Some h)) \ k \ h" | -"in_ivl k (I None None) \ True" - -instantiation option :: (plus)plus -begin - -fun plus_option where -"Some x + Some y = Some(x+y)" | -"_ + _ = None" - -instance .. - -end - -definition empty where "empty = {1\0}" - -fun is_empty where -"is_empty {l\h} = (h (case h of Some h \ h False) | None \ False)" -by(auto split:option.split) - -lemma [simp]: "is_empty i \ \_ivl i = {}" -by(auto simp add: \_ivl_def split: ivl.split option.split) - -definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else - case (i1,i2) of (I l1 h1, I l2 h2) \ I (l1+l2) (h1+h2))" - -instantiation ivl :: SL_top -begin - -definition le_option :: "bool \ int option \ int option \ bool" where -"le_option pos x y = - (case x of (Some i) \ (case y of Some j \ i\j | None \ pos) - | None \ (case y of Some j \ \pos | None \ True))" - -fun le_aux where -"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)" - -definition le_ivl where -"i1 \ i2 = - (if is_empty i1 then True else - if is_empty i2 then False else le_aux i1 i2)" - -definition min_option :: "bool \ int option \ int option \ int option" where -"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)" - -definition max_option :: "bool \ int option \ int option \ int option" where -"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)" - -definition "i1 \ i2 = - (if is_empty i1 then i2 else if is_empty i2 then i1 - else case (i1,i2) of (I l1 h1, I l2 h2) \ - I (min_option False l1 l2) (max_option True h1 h2))" - -definition "\ = {\}" - -instance -proof - case goal1 thus ?case - by(cases x, simp add: le_ivl_def le_option_def split: option.split) -next - case goal2 thus ?case - by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits) -next - case goal3 thus ?case - by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits) -next - case goal4 thus ?case - by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits) -next - case goal5 thus ?case - by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits) -next - case goal6 thus ?case - by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split) -qed - -end - - -instantiation ivl :: L_top_bot -begin - -definition "i1 \ i2 = (if is_empty i1 \ is_empty i2 then empty else - case (i1,i2) of (I l1 h1, I l2 h2) \ - I (max_option False l1 l2) (min_option True h1 h2))" - -definition "\ = empty" - -instance -proof - case goal1 thus ?case - by (simp add:meet_ivl_def empty_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits) -next - case goal2 thus ?case - by (simp add: empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits) -next - case goal3 thus ?case - by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits) -next - case goal4 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def) -qed - -end - -instantiation option :: (minus)minus -begin - -fun minus_option where -"Some x - Some y = Some(x-y)" | -"_ - _ = None" - -instance .. - -end - -definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else - case (i1,i2) of (I l1 h1, I l2 h2) \ I (l1-h2) (h1-l2))" - -lemma gamma_minus_ivl: - "n1 : \_ivl i1 \ n2 : \_ivl i2 \ n1-n2 : \_ivl(minus_ivl i1 i2)" -by(auto simp add: minus_ivl_def \_ivl_def split: ivl.splits option.splits) - -definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*) - i1 \ minus_ivl i i2, i2 \ minus_ivl i i1)" - -fun filter_less_ivl :: "bool \ ivl \ ivl \ ivl * ivl" where -"filter_less_ivl res (I l1 h1) (I l2 h2) = - (if is_empty(I l1 h1) \ is_empty(I l2 h2) then (empty, empty) else - if res - then (I l1 (min_option True h1 (h2 - Some 1)), - I (max_option False (l1 + Some 1) l2) h2) - else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" - -global_interpretation Val_abs -where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -proof - case goal1 thus ?case - by(auto simp: \_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits) -next - case goal2 show ?case by(simp add: \_ivl_def Top_ivl_def) -next - case goal3 thus ?case by(simp add: \_ivl_def num_ivl_def) -next - case goal4 thus ?case - by(auto simp add: \_ivl_def plus_ivl_def split: ivl.split option.splits) -qed - -global_interpretation Val_abs1_gamma -where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -defines aval_ivl = aval' -proof - case goal1 thus ?case - by(auto simp add: \_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) -next - case goal2 show ?case by(auto simp add: bot_ivl_def \_ivl_def empty_def) -qed - -lemma mono_minus_ivl: - "i1 \ i1' \ i2 \ i2' \ minus_ivl i1 i2 \ minus_ivl i1' i2'" -apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits) - apply(simp split: option.splits) - apply(simp split: option.splits) -apply(simp split: option.splits) -done - - -global_interpretation Val_abs1 -where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -and test_num' = in_ivl -and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -proof - case goal1 thus ?case - by (simp add: \_ivl_def split: ivl.split option.split) -next - case goal2 thus ?case - by(auto simp add: filter_plus_ivl_def) - (metis gamma_minus_ivl add_diff_cancel add.commute)+ -next - case goal3 thus ?case - by(cases a1, cases a2, - auto simp: \_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) -qed - -global_interpretation Abs_Int1 -where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -and test_num' = in_ivl -and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -defines afilter_ivl = afilter -and bfilter_ivl = bfilter -and step_ivl = step' -and AI_ivl = AI -and aval_ivl' = aval'' -.. - - -text{* Monotonicity: *} - -global_interpretation Abs_Int1_mono -where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -and test_num' = in_ivl -and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -proof - case goal1 thus ?case - by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits) -next - case goal2 thus ?case - by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl) -next - case goal3 thus ?case - apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def) - by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits) -qed - - -subsubsection "Tests" - -value "show_acom_opt (AI_ivl test1_ivl)" - -text{* Better than @{text AI_const}: *} -value "show_acom_opt (AI_ivl test3_const)" -value "show_acom_opt (AI_ivl test4_const)" -value "show_acom_opt (AI_ivl test6_const)" - -value "show_acom_opt (AI_ivl test2_ivl)" -value "show_acom (((step_ivl \)^^0) (\\<^sub>c test2_ivl))" -value "show_acom (((step_ivl \)^^1) (\\<^sub>c test2_ivl))" -value "show_acom (((step_ivl \)^^2) (\\<^sub>c test2_ivl))" - -text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *} - -value "show_acom_opt (AI_ivl test3_ivl)" -value "show_acom (((step_ivl \)^^0) (\\<^sub>c test3_ivl))" -value "show_acom (((step_ivl \)^^1) (\\<^sub>c test3_ivl))" -value "show_acom (((step_ivl \)^^2) (\\<^sub>c test3_ivl))" -value "show_acom (((step_ivl \)^^3) (\\<^sub>c test3_ivl))" -value "show_acom (((step_ivl \)^^4) (\\<^sub>c test3_ivl))" - -text{* Takes as many iterations as the actual execution. Would diverge if -loop did not terminate. Worse still, as the following example shows: even if -the actual execution terminates, the analysis may not. The value of y keeps -decreasing as the analysis is iterated, no matter how long: *} - -value "show_acom (((step_ivl \)^^50) (\\<^sub>c test4_ivl))" - -text{* Relationships between variables are NOT captured: *} -value "show_acom_opt (AI_ivl test5_ivl)" - -text{* Again, the analysis would not terminate: *} -value "show_acom (((step_ivl \)^^50) (\\<^sub>c test6_ivl))" - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,683 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_Int3_ITP -imports Abs_Int2_ivl_ITP -begin - -subsection "Widening and Narrowing" - -class WN = SL_top + -fixes widen :: "'a \ 'a \ 'a" (infix "\" 65) -assumes widen1: "x \ x \ y" -assumes widen2: "y \ x \ y" -fixes narrow :: "'a \ 'a \ 'a" (infix "\" 65) -assumes narrow1: "y \ x \ y \ x \ y" -assumes narrow2: "y \ x \ x \ y \ x" - - -subsubsection "Intervals" - -instantiation ivl :: WN -begin - -definition "widen_ivl ivl1 ivl2 = - ((*if is_empty ivl1 then ivl2 else - if is_empty ivl2 then ivl1 else*) - case (ivl1,ivl2) of (I l1 h1, I l2 h2) \ - I (if le_option False l2 l1 \ l2 \ l1 then None else l1) - (if le_option True h1 h2 \ h1 \ h2 then None else h1))" - -definition "narrow_ivl ivl1 ivl2 = - ((*if is_empty ivl1 \ is_empty ivl2 then empty else*) - case (ivl1,ivl2) of (I l1 h1, I l2 h2) \ - I (if l1 = None then l2 else l1) - (if h1 = None then h2 else h1))" - -instance -proof qed - (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits) - -end - - -subsubsection "Abstract State" - -instantiation st :: (WN)WN -begin - -definition "widen_st F1 F2 = - FunDom (\x. fun F1 x \ fun F2 x) (inter_list (dom F1) (dom F2))" - -definition "narrow_st F1 F2 = - FunDom (\x. fun F1 x \ fun F2 x) (inter_list (dom F1) (dom F2))" - -instance -proof - case goal1 thus ?case - by(simp add: widen_st_def le_st_def lookup_def widen1) -next - case goal2 thus ?case - by(simp add: widen_st_def le_st_def lookup_def widen2) -next - case goal3 thus ?case - by(auto simp: narrow_st_def le_st_def lookup_def narrow1) -next - case goal4 thus ?case - by(auto simp: narrow_st_def le_st_def lookup_def narrow2) -qed - -end - - -subsubsection "Option" - -instantiation option :: (WN)WN -begin - -fun widen_option where -"None \ x = x" | -"x \ None = x" | -"(Some x) \ (Some y) = Some(x \ y)" - -fun narrow_option where -"None \ x = None" | -"x \ None = None" | -"(Some x) \ (Some y) = Some(x \ y)" - -instance -proof - case goal1 show ?case - by(induct x y rule: widen_option.induct) (simp_all add: widen1) -next - case goal2 show ?case - by(induct x y rule: widen_option.induct) (simp_all add: widen2) -next - case goal3 thus ?case - by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) -next - case goal4 thus ?case - by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) -qed - -end - - -subsubsection "Annotated commands" - -fun map2_acom :: "('a \ 'a \ 'a) \ 'a acom \ 'a acom \ 'a acom" where -"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" | -"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" | -"map2_acom f (c1;;c2) (c1';;c2') = (map2_acom f c1 c1';; map2_acom f c2 c2')" | -"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) = - (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" | -"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) = - ({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})" - -abbreviation widen_acom :: "('a::WN)acom \ 'a acom \ 'a acom" (infix "\\<^sub>c" 65) -where "widen_acom == map2_acom (op \)" - -abbreviation narrow_acom :: "('a::WN)acom \ 'a acom \ 'a acom" (infix "\\<^sub>c" 65) -where "narrow_acom == map2_acom (op \)" - -lemma widen1_acom: "strip c = strip c' \ c \ c \\<^sub>c c'" -by(induct c c' rule: le_acom.induct)(simp_all add: widen1) - -lemma widen2_acom: "strip c = strip c' \ c' \ c \\<^sub>c c'" -by(induct c c' rule: le_acom.induct)(simp_all add: widen2) - -lemma narrow1_acom: "y \ x \ y \ x \\<^sub>c y" -by(induct y x rule: le_acom.induct) (simp_all add: narrow1) - -lemma narrow2_acom: "y \ x \ x \\<^sub>c y \ x" -by(induct y x rule: le_acom.induct) (simp_all add: narrow2) - - -subsubsection "Post-fixed point computation" - -definition iter_widen :: "('a acom \ 'a acom) \ 'a acom \ ('a::WN)acom option" -where "iter_widen f = while_option (\c. \ f c \ c) (\c. c \\<^sub>c f c)" - -definition iter_narrow :: "('a acom \ 'a acom) \ 'a acom \ 'a::WN acom option" -where "iter_narrow f = while_option (\c. \ c \ c \\<^sub>c f c) (\c. c \\<^sub>c f c)" - -definition pfp_wn :: - "(('a::WN)option acom \ 'a option acom) \ com \ 'a option acom option" -where "pfp_wn f c = (case iter_widen f (\\<^sub>c c) of None \ None - | Some c' \ iter_narrow f c')" - -lemma strip_map2_acom: - "strip c1 = strip c2 \ strip(map2_acom f c1 c2) = strip c1" -by(induct f c1 c2 rule: map2_acom.induct) simp_all - -lemma iter_widen_pfp: "iter_widen f c = Some c' \ f c' \ c'" -by(auto simp add: iter_widen_def dest: while_option_stop) - -lemma strip_while: fixes f :: "'a acom \ 'a acom" -assumes "\c. strip (f c) = strip c" and "while_option P f c = Some c'" -shows "strip c' = strip c" -using while_option_rule[where P = "\c'. strip c' = strip c", OF _ assms(2)] -by (metis assms(1)) - -lemma strip_iter_widen: fixes f :: "'a::WN acom \ 'a acom" -assumes "\c. strip (f c) = strip c" and "iter_widen f c = Some c'" -shows "strip c' = strip c" -proof- - have "\c. strip(c \\<^sub>c f c) = strip c" by (metis assms(1) strip_map2_acom) - from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def) -qed - -lemma iter_narrow_pfp: assumes "mono f" and "f c0 \ c0" -and "iter_narrow f c0 = Some c" -shows "f c \ c \ c \ c0" (is "?P c") -proof- - { fix c assume "?P c" - note 1 = conjunct1[OF this] and 2 = conjunct2[OF this] - let ?c' = "c \\<^sub>c f c" - have "?P ?c'" - proof - have "f ?c' \ f c" by(rule monoD[OF `mono f` narrow2_acom[OF 1]]) - also have "\ \ ?c'" by(rule narrow1_acom[OF 1]) - finally show "f ?c' \ ?c'" . - have "?c' \ c" by (rule narrow2_acom[OF 1]) - also have "c \ c0" by(rule 2) - finally show "?c' \ c0" . - qed - } - with while_option_rule[where P = ?P, OF _ assms(3)[simplified iter_narrow_def]] - assms(2) le_refl - show ?thesis by blast -qed - -lemma pfp_wn_pfp: - "\ mono f; pfp_wn f c = Some c' \ \ f c' \ c'" -unfolding pfp_wn_def -by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits) - -lemma strip_pfp_wn: - "\ \c. strip(f c) = strip c; pfp_wn f c = Some c' \ \ strip c' = c" -apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) -by (metis (mono_tags) strip_map2_acom strip_while strip_bot_acom strip_iter_widen) - -locale Abs_Int2 = Abs_Int1_mono -where \=\ for \ :: "'av::{WN,L_top_bot} \ val set" -begin - -definition AI_wn :: "com \ 'av st option acom option" where -"AI_wn = pfp_wn (step' \)" - -lemma AI_wn_sound: "AI_wn c = Some c' \ CS c \ \\<^sub>c c'" -proof(simp add: CS_def AI_wn_def) - assume 1: "pfp_wn (step' \) c = Some c'" - from pfp_wn_pfp[OF mono_step'2 1] - have 2: "step' \ c' \ c'" . - have 3: "strip (\\<^sub>c (step' \ c')) = c" by(simp add: strip_pfp_wn[OF _ 1]) - have "lfp (step UNIV) c \ \\<^sub>c (step' \ c')" - proof(rule lfp_lowerbound[simplified,OF 3]) - show "step UNIV (\\<^sub>c (step' \ c')) \ \\<^sub>c (step' \ c')" - proof(rule step_preserves_le[OF _ _]) - show "UNIV \ \\<^sub>o \" by simp - show "\\<^sub>c (step' \ c') \ \\<^sub>c c'" by(rule mono_gamma_c[OF 2]) - qed - qed - from this 2 show "lfp (step UNIV) c \ \\<^sub>c c'" - by (blast intro: mono_gamma_c order_trans) -qed - -end - -global_interpretation Abs_Int2 -where \ = \_ivl and num' = num_ivl and plus' = plus_ivl -and test_num' = in_ivl -and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl -defines AI_ivl' = AI_wn -.. - - -subsubsection "Tests" - -definition "step_up_ivl n = ((\c. c \\<^sub>c step_ivl \ c)^^n)" -definition "step_down_ivl n = ((\c. c \\<^sub>c step_ivl \ c)^^n)" - -text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as -the loop took to execute. In contrast, @{const AI_ivl'} converges in a -constant number of steps: *} - -value "show_acom (step_up_ivl 1 (\\<^sub>c test3_ivl))" -value "show_acom (step_up_ivl 2 (\\<^sub>c test3_ivl))" -value "show_acom (step_up_ivl 3 (\\<^sub>c test3_ivl))" -value "show_acom (step_up_ivl 4 (\\<^sub>c test3_ivl))" -value "show_acom (step_up_ivl 5 (\\<^sub>c test3_ivl))" -value "show_acom (step_down_ivl 1 (step_up_ivl 5 (\\<^sub>c test3_ivl)))" -value "show_acom (step_down_ivl 2 (step_up_ivl 5 (\\<^sub>c test3_ivl)))" -value "show_acom (step_down_ivl 3 (step_up_ivl 5 (\\<^sub>c test3_ivl)))" - -text{* Now all the analyses terminate: *} - -value "show_acom_opt (AI_ivl' test4_ivl)" -value "show_acom_opt (AI_ivl' test5_ivl)" -value "show_acom_opt (AI_ivl' test6_ivl)" - - -subsubsection "Termination: Intervals" - -definition m_ivl :: "ivl \ nat" where -"m_ivl ivl = (case ivl of I l h \ - (case l of None \ 0 | Some _ \ 1) + (case h of None \ 0 | Some _ \ 1))" - -lemma m_ivl_height: "m_ivl ivl \ 2" -by(simp add: m_ivl_def split: ivl.split option.split) - -lemma m_ivl_anti_mono: "(y::ivl) \ x \ m_ivl x \ m_ivl y" -by(auto simp: m_ivl_def le_option_def le_ivl_def - split: ivl.split option.split if_splits) - -lemma m_ivl_widen: - "~ y \ x \ m_ivl(x \ y) < m_ivl x" -by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def - split: ivl.splits option.splits if_splits) - -lemma Top_less_ivl: "\ \ x \ m_ivl x = 0" -by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def - split: ivl.split option.split if_splits) - - -definition n_ivl :: "ivl \ nat" where -"n_ivl ivl = 2 - m_ivl ivl" - -lemma n_ivl_mono: "(x::ivl) \ y \ n_ivl x \ n_ivl y" -unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono) - -lemma n_ivl_narrow: - "~ x \ x \ y \ n_ivl(x \ y) < n_ivl x" -by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def - split: ivl.splits option.splits if_splits) - - -subsubsection "Termination: Abstract State" - -definition "m_st m st = (\x\set(dom st). m(fun st x))" - -lemma m_st_height: assumes "finite X" and "set (dom S) \ X" -shows "m_st m_ivl S \ 2 * card X" -proof(auto simp: m_st_def) - have "(\x\set(dom S). m_ivl (fun S x)) \ (\x\set(dom S). 2)" (is "?L \ _") - by(rule sum_mono)(simp add:m_ivl_height) - also have "\ \ (\x\X. 2)" - by(rule sum_mono3[OF assms]) simp - also have "\ = 2 * card X" by(simp add: sum_constant) - finally show "?L \ \" . -qed - -lemma m_st_anti_mono: - "S1 \ S2 \ m_st m_ivl S2 \ m_st m_ivl S1" -proof(auto simp: m_st_def le_st_def lookup_def split: if_splits) - let ?X = "set(dom S1)" let ?Y = "set(dom S2)" - let ?f = "fun S1" let ?g = "fun S2" - assume asm: "\x\?Y. (x \ ?X \ ?f x \ ?g x) \ (x \ ?X \ \ \ ?g x)" - hence 1: "\y\?Y\?X. m_ivl(?g y) \ m_ivl(?f y)" by(simp add: m_ivl_anti_mono) - have 0: "\x\?Y-?X. m_ivl(?g x) = 0" using asm by (auto simp: Top_less_ivl) - have "(\y\?Y. m_ivl(?g y)) = (\y\(?Y-?X) \ (?Y\?X). m_ivl(?g y))" - by (metis Un_Diff_Int) - also have "\ = (\y\?Y-?X. m_ivl(?g y)) + (\y\?Y\?X. m_ivl(?g y))" - by(subst sum.union_disjoint) auto - also have "(\y\?Y-?X. m_ivl(?g y)) = 0" using 0 by simp - also have "0 + (\y\?Y\?X. m_ivl(?g y)) = (\y\?Y\?X. m_ivl(?g y))" by simp - also have "\ \ (\y\?Y\?X. m_ivl(?f y))" - by(rule sum_mono)(simp add: 1) - also have "\ \ (\y\?X. m_ivl(?f y))" - by(simp add: sum_mono3[of "?X" "?Y Int ?X", OF _ Int_lower2]) - finally show "(\y\?Y. m_ivl(?g y)) \ (\x\?X. m_ivl(?f x))" - by (metis add_less_cancel_left) -qed - -lemma m_st_widen: -assumes "\ S2 \ S1" shows "m_st m_ivl (S1 \ S2) < m_st m_ivl S1" -proof- - { let ?X = "set(dom S1)" let ?Y = "set(dom S2)" - let ?f = "fun S1" let ?g = "fun S2" - fix x assume "x \ ?X" "\ lookup S2 x \ ?f x" - have "(\x\?X\?Y. m_ivl(?f x \ ?g x)) < (\x\?X. m_ivl(?f x))" (is "?L < ?R") - proof cases - assume "x : ?Y" - have "?L < (\x\?X\?Y. m_ivl(?f x))" - proof(rule sum_strict_mono_ex1, simp) - show "\x\?X\?Y. m_ivl(?f x \ ?g x) \ m_ivl (?f x)" - by (metis m_ivl_anti_mono widen1) - next - show "\x\?X\?Y. m_ivl(?f x \ ?g x) < m_ivl(?f x)" - using `x:?X` `x:?Y` `\ lookup S2 x \ ?f x` - by (metis IntI m_ivl_widen lookup_def) - qed - also have "\ \ ?R" by(simp add: sum_mono3[OF _ Int_lower1]) - finally show ?thesis . - next - assume "x ~: ?Y" - have "?L \ (\x\?X\?Y. m_ivl(?f x))" - proof(rule sum_mono, simp) - fix x assume "x:?X \ x:?Y" show "m_ivl(?f x \ ?g x) \ m_ivl (?f x)" - by (metis m_ivl_anti_mono widen1) - qed - also have "\ < m_ivl(?f x) + \" - using m_ivl_widen[OF `\ lookup S2 x \ ?f x`] - by (metis Nat.le_refl add_strict_increasing gr0I not_less0) - also have "\ = (\y\insert x (?X\?Y). m_ivl(?f y))" - using `x ~: ?Y` by simp - also have "\ \ (\x\?X. m_ivl(?f x))" - by(rule sum_mono3)(insert `x:?X`, auto) - finally show ?thesis . - qed - } with assms show ?thesis - by(auto simp: le_st_def widen_st_def m_st_def Int_def) -qed - -definition "n_st m X st = (\x\X. m(lookup st x))" - -lemma n_st_mono: assumes "set(dom S1) \ X" "set(dom S2) \ X" "S1 \ S2" -shows "n_st n_ivl X S1 \ n_st n_ivl X S2" -proof- - have "(\x\X. n_ivl(lookup S1 x)) \ (\x\X. n_ivl(lookup S2 x))" - apply(rule sum_mono) using assms - by(auto simp: le_st_def lookup_def n_ivl_mono split: if_splits) - thus ?thesis by(simp add: n_st_def) -qed - -lemma n_st_narrow: -assumes "finite X" and "set(dom S1) \ X" "set(dom S2) \ X" -and "S2 \ S1" "\ S1 \ S1 \ S2" -shows "n_st n_ivl X (S1 \ S2) < n_st n_ivl X S1" -proof- - have 1: "\x\X. n_ivl (lookup (S1 \ S2) x) \ n_ivl (lookup S1 x)" - using assms(2-4) - by(auto simp: le_st_def narrow_st_def lookup_def n_ivl_mono narrow2 - split: if_splits) - have 2: "\x\X. n_ivl (lookup (S1 \ S2) x) < n_ivl (lookup S1 x)" - using assms(2-5) - by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow - split: if_splits) - have "(\x\X. n_ivl(lookup (S1 \ S2) x)) < (\x\X. n_ivl(lookup S1 x))" - apply(rule sum_strict_mono_ex1[OF `finite X`]) using 1 2 by blast+ - thus ?thesis by(simp add: n_st_def) -qed - - -subsubsection "Termination: Option" - -definition "m_o m n opt = (case opt of None \ n+1 | Some x \ m x)" - -lemma m_o_anti_mono: "finite X \ domo S2 \ X \ S1 \ S2 \ - m_o (m_st m_ivl) (2 * card X) S2 \ m_o (m_st m_ivl) (2 * card X) S1" -apply(induction S1 S2 rule: le_option.induct) -apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height - split: option.splits) -done - -lemma m_o_widen: "\ finite X; domo S2 \ X; \ S2 \ S1 \ \ - m_o (m_st m_ivl) (2 * card X) (S1 \ S2) < m_o (m_st m_ivl) (2 * card X) S1" -by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le m_st_widen - split: option.split) - -definition "n_o n opt = (case opt of None \ 0 | Some x \ n x + 1)" - -lemma n_o_mono: "domo S1 \ X \ domo S2 \ X \ S1 \ S2 \ - n_o (n_st n_ivl X) S1 \ n_o (n_st n_ivl X) S2" -apply(induction S1 S2 rule: le_option.induct) -apply(auto simp: domo_def n_o_def n_st_mono - split: option.splits) -done - -lemma n_o_narrow: - "\ finite X; domo S1 \ X; domo S2 \ X; S2 \ S1; \ S1 \ S1 \ S2 \ - \ n_o (n_st n_ivl X) (S1 \ S2) < n_o (n_st n_ivl X) S1" -apply(induction S1 S2 rule: narrow_option.induct) -apply(auto simp: n_o_def domo_def n_st_narrow) -done - -lemma domo_widen_subset: "domo (S1 \ S2) \ domo S1 \ domo S2" -apply(induction S1 S2 rule: widen_option.induct) -apply (auto simp: domo_def widen_st_def) -done - -lemma domo_narrow_subset: "domo (S1 \ S2) \ domo S1 \ domo S2" -apply(induction S1 S2 rule: narrow_option.induct) -apply (auto simp: domo_def narrow_st_def) -done - -subsubsection "Termination: Commands" - -lemma strip_widen_acom[simp]: - "strip c' = strip (c::'a::WN acom) \ strip (c \\<^sub>c c') = strip c" -by(induction "widen::'a\'a\'a" c c' rule: map2_acom.induct) simp_all - -lemma strip_narrow_acom[simp]: - "strip c' = strip (c::'a::WN acom) \ strip (c \\<^sub>c c') = strip c" -by(induction "narrow::'a\'a\'a" c c' rule: map2_acom.induct) simp_all - -lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \ - annos(c1 \\<^sub>c c2) = map (%(x,y).x\y) (zip (annos c1) (annos(c2::'a::WN acom)))" -by(induction "widen::'a\'a\'a" c1 c2 rule: map2_acom.induct) - (simp_all add: size_annos_same2) - -lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \ - annos(c1 \\<^sub>c c2) = map (%(x,y).x\y) (zip (annos c1) (annos(c2::'a::WN acom)))" -by(induction "narrow::'a\'a\'a" c1 c2 rule: map2_acom.induct) - (simp_all add: size_annos_same2) - -lemma widen_acom_Com[simp]: "strip c2 = strip c1 \ - c1 : Com X \ c2 : Com X \ (c1 \\<^sub>c c2) : Com X" -apply(auto simp add: Com_def) -apply(rename_tac S S' x) -apply(erule in_set_zipE) -apply(auto simp: domo_def split: option.splits) -apply(case_tac S) -apply(case_tac S') -apply simp -apply fastforce -apply(case_tac S') -apply fastforce -apply (fastforce simp: widen_st_def) -done - -lemma narrow_acom_Com[simp]: "strip c2 = strip c1 \ - c1 : Com X \ c2 : Com X \ (c1 \\<^sub>c c2) : Com X" -apply(auto simp add: Com_def) -apply(rename_tac S S' x) -apply(erule in_set_zipE) -apply(auto simp: domo_def split: option.splits) -apply(case_tac S) -apply(case_tac S') -apply simp -apply fastforce -apply(case_tac S') -apply fastforce -apply (fastforce simp: narrow_st_def) -done - -definition "m_c m c = (let as = annos c in \i=0.. {(c, c \\<^sub>c c') |c c'::ivl st option acom. - strip c' = strip c \ c : Com X \ c' : Com X \ \ c' \ c}\ - \ measure(m_c(m_o (m_st m_ivl) (2*card(X))))" -apply(auto simp: m_c_def Let_def Com_def) -apply(subgoal_tac "length(annos c') = length(annos c)") -prefer 2 apply (simp add: size_annos_same2) -apply (auto) -apply(rule sum_strict_mono_ex1) -apply simp -apply (clarsimp) -apply(erule m_o_anti_mono) -apply(rule subset_trans[OF domo_widen_subset]) -apply fastforce -apply(rule widen1) -apply(auto simp: le_iff_le_annos listrel_iff_nth) -apply(rule_tac x=n in bexI) -prefer 2 apply simp -apply(erule m_o_widen) -apply (simp)+ -done - -lemma measure_n_c: "finite X \ {(c, c \\<^sub>c c') |c c'. - strip c = strip c' \ c \ Com X \ c' \ Com X \ c' \ c \ \ c \ c \\<^sub>c c'}\ - \ measure(m_c(n_o (n_st n_ivl X)))" -apply(auto simp: m_c_def Let_def Com_def) -apply(subgoal_tac "length(annos c') = length(annos c)") -prefer 2 apply (simp add: size_annos_same2) -apply (auto) -apply(rule sum_strict_mono_ex1) -apply simp -apply (clarsimp) -apply(rule n_o_mono) -using domo_narrow_subset apply fastforce -apply fastforce -apply(rule narrow2) -apply(fastforce simp: le_iff_le_annos listrel_iff_nth) -apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom) -apply(rule_tac x=n in bexI) -prefer 2 apply simp -apply(erule n_o_narrow) -apply (simp)+ -done - - -subsubsection "Termination: Post-Fixed Point Iterations" - -lemma iter_widen_termination: -fixes c0 :: "'a::WN acom" -assumes P_f: "\c. P c \ P(f c)" -assumes P_widen: "\c c'. P c \ P c' \ P(c \\<^sub>c c')" -and "wf({(c::'a acom,c \\<^sub>c c')|c c'. P c \ P c' \ ~ c' \ c}^-1)" -and "P c0" and "c0 \ f c0" shows "EX c. iter_widen f c0 = Some c" -proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"]) - show "wf {(cc', c). (P c \ \ f c \ c) \ cc' = c \\<^sub>c f c}" - apply(rule wf_subset[OF assms(3)]) by(blast intro: P_f) -next - show "P c0" by(rule `P c0`) -next - fix c assume "P c" thus "P (c \\<^sub>c f c)" by(simp add: P_f P_widen) -qed - -lemma iter_narrow_termination: -assumes P_f: "\c. P c \ P(c \\<^sub>c f c)" -and wf: "wf({(c, c \\<^sub>c f c)|c c'. P c \ ~ c \ c \\<^sub>c f c}^-1)" -and "P c0" shows "EX c. iter_narrow f c0 = Some c" -proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "P"]) - show "wf {(c', c). (P c \ \ c \ c \\<^sub>c f c) \ c' = c \\<^sub>c f c}" - apply(rule wf_subset[OF wf]) by(blast intro: P_f) -next - show "P c0" by(rule `P c0`) -next - fix c assume "P c" thus "P (c \\<^sub>c f c)" by(simp add: P_f) -qed - -lemma iter_winden_step_ivl_termination: - "EX c. iter_widen (step_ivl \) (\\<^sub>c c0) = Some c" -apply(rule iter_widen_termination[where - P = "%c. strip c = c0 \ c : Com(vars c0)"]) -apply (simp_all add: step'_Com bot_acom) -apply(rule wf_subset) -apply(rule wf_measure) -apply(rule subset_trans) -prefer 2 -apply(rule measure_m_c[where X = "vars c0", OF finite_cvars]) -apply blast -done - -lemma iter_narrow_step_ivl_termination: - "c0 \ Com (vars(strip c0)) \ step_ivl \ c0 \ c0 \ - EX c. iter_narrow (step_ivl \) c0 = Some c" -apply(rule iter_narrow_termination[where - P = "%c. strip c = strip c0 \ c : Com(vars(strip c0)) \ step_ivl \ c \ c"]) -apply (simp_all add: step'_Com) -apply(clarify) -apply(frule narrow2_acom, drule mono_step'[OF le_refl], erule le_trans[OF _ narrow1_acom]) -apply assumption -apply(rule wf_subset) -apply(rule wf_measure) -apply(rule subset_trans) -prefer 2 -apply(rule measure_n_c[where X = "vars(strip c0)", OF finite_cvars]) -apply auto -by (metis bot_least domo_Top order_refl step'_Com strip_step') - -(* FIXME: simplify type system: Combine Com(X) and vars <= X?? *) -lemma while_Com: -fixes c :: "'a st option acom" -assumes "while_option P f c = Some c'" -and "!!c. strip(f c) = strip c" -and "\c::'a st option acom. c : Com(X) \ vars(strip c) \ X \ f c : Com(X)" -and "c : Com(X)" and "vars(strip c) \ X" shows "c' : Com(X)" -using while_option_rule[where P = "\c'. c' : Com(X) \ vars(strip c') \ X", OF _ assms(1)] -by(simp add: assms(2-)) - -lemma iter_widen_Com: fixes f :: "'a::WN st option acom \ 'a st option acom" -assumes "iter_widen f c = Some c'" -and "\c. c : Com(X) \ vars(strip c) \ X \ f c : Com(X)" -and "!!c. strip(f c) = strip c" -and "c : Com(X)" and "vars (strip c) \ X" shows "c' : Com(X)" -proof- - have "\c. c : Com(X) \ vars(strip c) \ X \ c \\<^sub>c f c : Com(X)" - by (metis (full_types) widen_acom_Com assms(2,3)) - from while_Com[OF assms(1)[simplified iter_widen_def] _ this assms(4,5)] - show ?thesis using assms(3) by(simp) -qed - - -context Abs_Int2 -begin - -lemma iter_widen_step'_Com: - "iter_widen (step' \) c = Some c' \ vars(strip c) \ X \ c : Com(X) - \ c' : Com(X)" -apply(subgoal_tac "strip c'= strip c") -prefer 2 apply (metis strip_iter_widen strip_step') -apply(drule iter_widen_Com) -prefer 3 apply assumption -prefer 3 apply assumption -apply (auto simp: step'_Com) -done - -end - -theorem AI_ivl'_termination: - "EX c'. AI_ivl' c = Some c'" -apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split) -apply(rule iter_narrow_step_ivl_termination) -apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step') -apply(erule iter_widen_pfp) -done - -end - - -(* interesting(?) relic -lemma widen_assoc: - "~ (y::ivl) \ x \ ~ z \ x \ y \ ((x::ivl) \ y) \ z = x \ (y \ z)" -apply(cases x) -apply(cases y) -apply(cases z) -apply(rename_tac x1 x2 y1 y2 z1 z2) -apply(simp add: le_ivl_def) -apply(case_tac x1) -apply(case_tac x2) -apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) -apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) -apply(case_tac x2) -apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) -apply(case_tac y1) -apply(case_tac y2) -apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) -apply(case_tac z1) -apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] -apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] -apply(case_tac y2) -apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] -apply(case_tac z1) -apply(auto simp add:le_option_def widen_ivl_def split: if_splits ivl.splits option.splits)[1] -apply(case_tac z2) -apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1] -apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1] -done - -lemma widen_step_trans: - "~ (y::ivl) \ x \ ~ z \ x \ y \ EX u. (x \ y) \ z = x \ u \ ~ u \ x" -by (metis widen_assoc preord_class.le_trans widen1) -*) diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,98 +0,0 @@ -(* Author: Tobias Nipkow *) - -theory Abs_State_ITP -imports Abs_Int0_ITP - "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord" - (* Library import merely to allow string lists to be sorted for output *) -begin - -subsection "Abstract State with Computable Ordering" - -text{* A concrete type of state with computable @{text"\"}: *} - -datatype 'a st = FunDom "vname \ 'a" "vname list" - -fun "fun" where "fun (FunDom f xs) = f" -fun dom where "dom (FunDom f xs) = xs" - -definition [simp]: "inter_list xs ys = [x\xs. x \ set ys]" - -definition "show_st S = [(x,fun S x). x \ sort(dom S)]" - -definition "show_acom = map_acom (map_option show_st)" -definition "show_acom_opt = map_option show_acom" - -definition "lookup F x = (if x : set(dom F) then fun F x else \)" - -definition "update F x y = - FunDom ((fun F)(x:=y)) (if x \ set(dom F) then dom F else x # dom F)" - -lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)" -by(rule ext)(auto simp: lookup_def update_def) - -definition "\_st \ F = {f. \x. f x \ \(lookup F x)}" - -instantiation st :: (SL_top) SL_top -begin - -definition "le_st F G = (ALL x : set(dom G). lookup F x \ fun G x)" - -definition -"join_st F G = - FunDom (\x. fun F x \ fun G x) (inter_list (dom F) (dom G))" - -definition "\ = FunDom (\x. \) []" - -instance -proof - case goal2 thus ?case - apply(auto simp: le_st_def) - by (metis lookup_def preord_class.le_trans top) -qed (auto simp: le_st_def lookup_def join_st_def Top_st_def) - -end - -lemma mono_lookup: "F \ F' \ lookup F x \ lookup F' x" -by(auto simp add: lookup_def le_st_def) - -lemma mono_update: "a \ a' \ S \ S' \ update S x a \ update S' x a'" -by(auto simp add: le_st_def lookup_def update_def) - -locale Gamma = Val_abs where \=\ for \ :: "'av::SL_top \ val set" -begin - -abbreviation \\<^sub>f :: "'av st \ state set" -where "\\<^sub>f == \_st \" - -abbreviation \\<^sub>o :: "'av st option \ state set" -where "\\<^sub>o == \_option \\<^sub>f" - -abbreviation \\<^sub>c :: "'av st option acom \ state set acom" -where "\\<^sub>c == map_acom \\<^sub>o" - -lemma gamma_f_Top[simp]: "\\<^sub>f Top = UNIV" -by(auto simp: Top_st_def \_st_def lookup_def) - -lemma gamma_o_Top[simp]: "\\<^sub>o Top = UNIV" -by (simp add: Top_option_def) - -(* FIXME (maybe also le \ sqle?) *) - -lemma mono_gamma_f: "f \ g \ \\<^sub>f f \ \\<^sub>f g" -apply(simp add:\_st_def subset_iff lookup_def le_st_def split: if_splits) -by (metis UNIV_I mono_gamma gamma_Top subsetD) - -lemma mono_gamma_o: - "sa \ sa' \ \\<^sub>o sa \ \\<^sub>o sa'" -by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) - -lemma mono_gamma_c: "ca \ ca' \ \\<^sub>c ca \ \\<^sub>c ca'" -by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) - -lemma in_gamma_option_iff: - "x : \_option r u \ (\u'. u = Some u' \ x : r u')" -by (cases u) auto - -end - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,183 +0,0 @@ -theory Collecting_ITP -imports Complete_Lattice_ix "ACom_ITP" -begin - -subsection "Collecting Semantics of Commands" - -subsubsection "Annotated commands as a complete lattice" - -(* Orderings could also be lifted generically (thus subsuming the -instantiation for preord and order), but then less_eq_acom would need to -become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would -need to unfold this defn first. *) - -instantiation acom :: (order) order -begin - -fun less_eq_acom :: "('a::order)acom \ 'a acom \ bool" where -"(SKIP {S}) \ (SKIP {S'}) = (S \ S')" | -"(x ::= e {S}) \ (x' ::= e' {S'}) = (x=x' \ e=e' \ S \ S')" | -"(c1;;c2) \ (c1';;c2') = (c1 \ c1' \ c2 \ c2')" | -"(IF b THEN c1 ELSE c2 {S}) \ (IF b' THEN c1' ELSE c2' {S'}) = - (b=b' \ c1 \ c1' \ c2 \ c2' \ S \ S')" | -"({Inv} WHILE b DO c {P}) \ ({Inv'} WHILE b' DO c' {P'}) = - (b=b' \ c \ c' \ Inv \ Inv' \ P \ P')" | -"less_eq_acom _ _ = False" - -lemma SKIP_le: "SKIP {S} \ c \ (\S'. c = SKIP {S'} \ S \ S')" -by (cases c) auto - -lemma Assign_le: "x ::= e {S} \ c \ (\S'. c = x ::= e {S'} \ S \ S')" -by (cases c) auto - -lemma Seq_le: "c1;;c2 \ c \ (\c1' c2'. c = c1';;c2' \ c1 \ c1' \ c2 \ c2')" -by (cases c) auto - -lemma If_le: "IF b THEN c1 ELSE c2 {S} \ c \ - (\c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} \ c1 \ c1' \ c2 \ c2' \ S \ S')" -by (cases c) auto - -lemma While_le: "{Inv} WHILE b DO c {P} \ w \ - (\Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \ c \ c' \ Inv \ Inv' \ P \ P')" -by (cases w) auto - -definition less_acom :: "'a acom \ 'a acom \ bool" where -"less_acom x y = (x \ y \ \ y \ x)" - -instance -proof - case goal1 show ?case by(simp add: less_acom_def) -next - case goal2 thus ?case by (induct x) auto -next - case goal3 thus ?case - apply(induct x y arbitrary: z rule: less_eq_acom.induct) - apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le) - done -next - case goal4 thus ?case - apply(induct x y rule: less_eq_acom.induct) - apply (auto intro: le_antisym) - done -qed - -end - -fun sub\<^sub>1 :: "'a acom \ 'a acom" where -"sub\<^sub>1(c1;;c2) = c1" | -"sub\<^sub>1(IF b THEN c1 ELSE c2 {S}) = c1" | -"sub\<^sub>1({I} WHILE b DO c {P}) = c" - -fun sub\<^sub>2 :: "'a acom \ 'a acom" where -"sub\<^sub>2(c1;;c2) = c2" | -"sub\<^sub>2(IF b THEN c1 ELSE c2 {S}) = c2" - -fun invar :: "'a acom \ 'a" where -"invar({I} WHILE b DO c {P}) = I" - -fun lift :: "('a set \ 'b) \ com \ 'a acom set \ 'b acom" -where -"lift F com.SKIP M = (SKIP {F (post ` M)})" | -"lift F (x ::= a) M = (x ::= a {F (post ` M)})" | -"lift F (c1;;c2) M = - lift F c1 (sub\<^sub>1 ` M);; lift F c2 (sub\<^sub>2 ` M)" | -"lift F (IF b THEN c1 ELSE c2) M = - IF b THEN lift F c1 (sub\<^sub>1 ` M) ELSE lift F c2 (sub\<^sub>2 ` M) - {F (post ` M)}" | -"lift F (WHILE b DO c) M = - {F (invar ` M)} - WHILE b DO lift F c (sub\<^sub>1 ` M) - {F (post ` M)}" - -global_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter" -proof - case goal1 - have "a:A \ lift Inter (strip a) A \ a" - proof(induction a arbitrary: A) - case Seq from Seq.prems show ?case by(force intro!: Seq.IH) - next - case If from If.prems show ?case by(force intro!: If.IH) - next - case While from While.prems show ?case by(force intro!: While.IH) - qed force+ - with goal1 show ?case by auto -next - case goal2 - thus ?case - proof(induction b arbitrary: i A) - case SKIP thus ?case by (force simp:SKIP_le) - next - case Assign thus ?case by (force simp:Assign_le) - next - case Seq from Seq.prems show ?case - by (force intro!: Seq.IH simp:Seq_le) - next - case If from If.prems show ?case by (force simp: If_le intro!: If.IH) - next - case While from While.prems show ?case - by(fastforce simp: While_le intro: While.IH) - qed -next - case goal3 - have "strip(lift Inter i A) = i" - proof(induction i arbitrary: A) - case Seq from Seq.prems show ?case - by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH) - next - case If from If.prems show ?case - by (fastforce intro!: If.IH simp: strip_eq_If) - next - case While from While.prems show ?case - by(fastforce intro: While.IH simp: strip_eq_While) - qed auto - thus ?case by auto -qed - -lemma le_post: "c \ d \ post c \ post d" -by(induction c d rule: less_eq_acom.induct) auto - -subsubsection "Collecting semantics" - -fun step :: "state set \ state set acom \ state set acom" where -"step S (SKIP {P}) = (SKIP {S})" | -"step S (x ::= e {P}) = - (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" | -"step S (c1;; c2) = step S c1;; step (post c1) c2" | -"step S (IF b THEN c1 ELSE c2 {P}) = - IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \ bval b s} c2 - {post c1 \ post c2}" | -"step S ({Inv} WHILE b DO c {P}) = - {S \ post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \ bval b s}}" - -definition CS :: "com \ state set acom" where -"CS c = lfp (step UNIV) c" - -lemma mono2_step: "c1 \ c2 \ S1 \ S2 \ step S1 c1 \ step S2 c2" -proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct) - case 2 thus ?case by fastforce -next - case 3 thus ?case by(simp add: le_post) -next - case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+ -next - case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp) -qed auto - -lemma mono_step: "mono (step S)" -by(blast intro: monoI mono2_step) - -lemma strip_step: "strip(step S c) = strip c" -by (induction c arbitrary: S) auto - -lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)" -apply(rule lfp_unfold[OF _ mono_step]) -apply(simp add: strip_step) -done - -lemma CS_unfold: "CS c = step UNIV (CS c)" -by (metis CS_def lfp_cs_unfold) - -lemma strip_CS[simp]: "strip(CS c) = c" -by(simp add: CS_def index_lfp[simplified]) - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy --- a/src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy Mon Dec 12 16:54:15 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,61 +0,0 @@ -(* Author: Tobias Nipkow *) - -section "Abstract Interpretation (ITP)" - -theory Complete_Lattice_ix -imports Main -begin - -subsection "Complete Lattice (indexed)" - -text{* A complete lattice is an ordered type where every set of elements has -a greatest lower (and thus also a leats upper) bound. Sets are the -prototypical complete lattice where the greatest lower bound is -intersection. Sometimes that set of all elements of a type is not a complete -lattice although all elements of the same shape form a complete lattice, for -example lists of the same length, where the list elements come from a -complete lattice. We will have exactly this situation with annotated -commands. This theory introduces a slightly generalised version of complete -lattices where elements have an ``index'' and only the set of elements with -the same index form a complete lattice; the type as a whole is a disjoint -union of complete lattices. Because sets are not types, this requires a -special treatment. *} - -locale Complete_Lattice_ix = -fixes L :: "'i \ 'a::order set" -and Glb :: "'i \ 'a set \ 'a" -assumes Glb_lower: "A \ L i \ a \ A \ (Glb i A) \ a" -and Glb_greatest: "b : L i \ \a\A. b \ a \ b \ (Glb i A)" -and Glb_in_L: "A \ L i \ Glb i A : L i" -begin - -definition lfp :: "('a \ 'a) \ 'i \ 'a" where -"lfp f i = Glb i {a : L i. f a \ a}" - -lemma index_lfp: "lfp f i : L i" -by(auto simp: lfp_def intro: Glb_in_L) - -lemma lfp_lowerbound: - "\ a : L i; f a \ a \ \ lfp f i \ a" -by (auto simp add: lfp_def intro: Glb_lower) - -lemma lfp_greatest: - "\ a : L i; \u. \ u : L i; f u \ u\ \ a \ u \ \ a \ lfp f i" -by (auto simp add: lfp_def intro: Glb_greatest) - -lemma lfp_unfold: assumes "\x i. f x : L i \ x : L i" -and mono: "mono f" shows "lfp f i = f (lfp f i)" -proof- - note assms(1)[simp] index_lfp[simp] - have 1: "f (lfp f i) \ lfp f i" - apply(rule lfp_greatest) - apply simp - by (blast intro: lfp_lowerbound monoD[OF mono] order_trans) - have "lfp f i \ f (lfp f i)" - by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound) - with 1 show ?thesis by(blast intro: order_antisym) -qed - -end - -end diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/IMP/Big_Step.thy --- a/src/HOL/IMP/Big_Step.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/IMP/Big_Step.thy Mon Dec 12 17:40:06 2016 +0100 @@ -179,52 +179,39 @@ -- "to show the equivalence, we look at the derivation tree for" -- "each side and from that construct a derivation tree for the other side" { fix s t assume "(?w, s) \ t" - -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s}," - -- "then both statements do nothing:" - { assume "\bval b s" - hence "t = s" using `(?w,s) \ t` by blast - hence "(?iw, s) \ t" using `\bval b s` by blast - } - moreover - -- "on the other hand, if @{text b} is @{text True} in state @{text s}," - -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \ t"} *} - { assume "bval b s" - with `(?w, s) \ t` obtain s' where + hence "(?iw, s) \ t" + proof cases --"rule inversion on \(?w, s) \ t\" + case WhileFalse + thus ?thesis by blast + next + case WhileTrue + from `bval b s` `(?w, s) \ t` obtain s' where "(c, s) \ s'" and "(?w, s') \ t" by auto -- "now we can build a derivation tree for the @{text IF}" -- "first, the body of the True-branch:" hence "(c;; ?w, s) \ t" by (rule Seq) -- "then the whole @{text IF}" - with `bval b s` have "(?iw, s) \ t" by (rule IfTrue) - } - ultimately - -- "both cases together give us what we want:" - have "(?iw, s) \ t" by blast + with `bval b s` show ?thesis by (rule IfTrue) + qed } moreover -- "now the other direction:" { fix s t assume "(?iw, s) \ t" - -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch" - -- "of the @{text IF} is executed, and both statements do nothing:" - { assume "\bval b s" + hence "(?w, s) \ t" + proof cases --"rule inversion on \(?iw, s) \ t\" + case IfFalse hence "s = t" using `(?iw, s) \ t` by blast - hence "(?w, s) \ t" using `\bval b s` by blast - } - moreover - -- "on the other hand, if @{text b} is @{text True} in state @{text s}," - -- {* then this time only the @{text IfTrue} rule can have be used *} - { assume "bval b s" + thus ?thesis using `\bval b s` by blast + next + case IfTrue with `(?iw, s) \ t` have "(c;; ?w, s) \ t" by auto -- "and for this, only the Seq-rule is applicable:" then obtain s' where "(c, s) \ s'" and "(?w, s') \ t" by auto -- "with this information, we can build a derivation tree for the @{text WHILE}" with `bval b s` - have "(?w, s) \ t" by (rule WhileTrue) - } - ultimately - -- "both cases together again give us what we want:" - have "(?w, s) \ t" by blast + show ?thesis by (rule WhileTrue) + qed } ultimately show ?thesis by blast diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Library/Discrete.thy --- a/src/HOL/Library/Discrete.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Library/Discrete.thy Mon Dec 12 17:40:06 2016 +0100 @@ -3,7 +3,7 @@ section \Common discrete functions\ theory Discrete -imports Main +imports Complex_Main begin subsection \Discrete logarithm\ @@ -111,6 +111,62 @@ finally show ?case . qed +lemma log_exp2_gt: "2 * 2 ^ log n > n" +proof (cases "n > 0") + case True + thus ?thesis + proof (induct n rule: log_induct) + case (double n) + thus ?case + by (cases "even n") (auto elim!: evenE oddE simp: field_simps log.simps) + qed simp_all +qed simp_all + +lemma log_exp2_ge: "2 * 2 ^ log n \ n" + using log_exp2_gt[of n] by simp + +lemma log_le_iff: "m \ n \ log m \ log n" + by (rule monoD [OF log_mono]) + +lemma log_eqI: + assumes "n > 0" "2^k \ n" "n < 2 * 2^k" + shows "log n = k" +proof (rule antisym) + from \n > 0\ have "2 ^ log n \ n" by (rule log_exp2_le) + also have "\ < 2 ^ Suc k" using assms by simp + finally have "log n < Suc k" by (subst (asm) power_strict_increasing_iff) simp_all + thus "log n \ k" by simp +next + have "2^k \ n" by fact + also have "\ < 2^(Suc (log n))" by (simp add: log_exp2_gt) + finally have "k < Suc (log n)" by (subst (asm) power_strict_increasing_iff) simp_all + thus "k \ log n" by simp +qed + +lemma log_altdef: "log n = (if n = 0 then 0 else nat \Transcendental.log 2 (real_of_nat n)\)" +proof (cases "n = 0") + case False + have "\Transcendental.log 2 (real_of_nat n)\ = int (log n)" + proof (rule floor_unique) + from False have "2 powr (real (log n)) \ real n" + by (simp add: powr_realpow log_exp2_le) + hence "Transcendental.log 2 (2 powr (real (log n))) \ Transcendental.log 2 (real n)" + using False by (subst Transcendental.log_le_cancel_iff) simp_all + also have "Transcendental.log 2 (2 powr (real (log n))) = real (log n)" by simp + finally show "real_of_int (int (log n)) \ Transcendental.log 2 (real n)" by simp + next + have "real n < real (2 * 2 ^ log n)" + by (subst of_nat_less_iff) (rule log_exp2_gt) + also have "\ = 2 powr (real (log n) + 1)" + by (simp add: powr_add powr_realpow) + finally have "Transcendental.log 2 (real n) < Transcendental.log 2 \" + using False by (subst Transcendental.log_less_cancel_iff) simp_all + also have "\ = real (log n) + 1" by simp + finally show "Transcendental.log 2 (real n) < real_of_int (int (log n)) + 1" by simp + qed + thus ?thesis by simp +qed simp_all + subsection \Discrete square root\ diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Dec 12 17:40:06 2016 +0100 @@ -2825,6 +2825,9 @@ thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps) qed +lemmas mult_cancel_add_mset = + mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral] + lemma mult_cancel_max: assumes "trans s" and "irrefl s" shows "(X, Y) \ mult s \ (X - X \# Y, Y - X \# Y) \ mult s" (is "?L \ ?R") diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Library/Permutations.thy Mon Dec 12 17:40:06 2016 +0100 @@ -31,7 +31,7 @@ using surj_f_inv_f[OF bij_is_surj[OF bp]] by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp]) -lemma bij_swap_ompose_bij: "bij p \ bij (Fun.swap a b id \ p)" +lemma bij_swap_compose_bij: "bij p \ bij (Fun.swap a b id \ p)" proof - assume H: "bij p" show ?thesis @@ -756,18 +756,10 @@ let ?q = "Fun.swap a (p a) id \ ?r" have raa: "?r a = a" by (simp add: Fun.swap_def) - from bij_swap_ompose_bij[OF insert(4)] - have br: "bij ?r" . - + from bij_swap_compose_bij[OF insert(4)] have br: "bij ?r" . from insert raa have th: "\x. x \ F \ ?r x = x" - apply (clarsimp simp add: Fun.swap_def) - apply (erule_tac x="x" in allE) - apply auto - unfolding bij_iff - apply metis - done - from insert(3)[OF br th] - have rp: "permutation ?r" . + by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3)) + from insert(3)[OF br th] have rp: "permutation ?r" . have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp) then show ?case @@ -926,7 +918,7 @@ using permutes_in_image[OF assms] by auto have "count (mset (permute_list f xs)) y = card ((\i. xs ! f i) -` {y} \ {..i. xs ! f i) -` {y} \ {.. y = xs ! i}" by auto also from assms have "card \ = card {i. i < length xs \ y = xs ! i}" diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Library/Tree.thy --- a/src/HOL/Library/Tree.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Library/Tree.thy Mon Dec 12 17:40:06 2016 +0100 @@ -144,46 +144,46 @@ lemma height_le_size_tree: "height t \ size (t::'a tree)" by (induction t) auto -lemma size1_height: "size t + 1 \ 2 ^ height (t::'a tree)" +lemma size1_height: "size1 t \ 2 ^ height (t::'a tree)" proof(induction t) case (Node l a r) show ?case proof (cases "height l \ height r") case True - have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp - also have "size l + 1 \ 2 ^ height l" by(rule Node.IH(1)) - also have "size r + 1 \ 2 ^ height r" by(rule Node.IH(2)) + have "size1(Node l a r) = size1 l + size1 r" by simp + also have "size1 l \ 2 ^ height l" by(rule Node.IH(1)) + also have "size1 r \ 2 ^ height r" by(rule Node.IH(2)) also have "(2::nat) ^ height l \ 2 ^ height r" using True by simp finally show ?thesis using True by (auto simp: max_def mult_2) next case False - have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp - also have "size l + 1 \ 2 ^ height l" by(rule Node.IH(1)) - also have "size r + 1 \ 2 ^ height r" by(rule Node.IH(2)) + have "size1(Node l a r) = size1 l + size1 r" by simp + also have "size1 l \ 2 ^ height l" by(rule Node.IH(1)) + also have "size1 r \ 2 ^ height r" by(rule Node.IH(2)) also have "(2::nat) ^ height r \ 2 ^ height l" using False by simp finally show ?thesis using False by (auto simp: max_def mult_2) qed qed simp corollary size_height: "size t \ 2 ^ height (t::'a tree) - 1" -using size1_height[of t] by(arith) +using size1_height[of t, unfolded size1_def] by(arith) lemma height_subtrees: "s \ subtrees t \ height s \ height t" by (induction t) auto -lemma min_hight_le_height: "min_height t \ height t" +lemma min_height_le_height: "min_height t \ height t" by(induction t) auto lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t" by (induction t) auto -lemma min_height_le_size1: "2 ^ min_height t \ size t + 1" +lemma min_height_size1: "2 ^ min_height t \ size1 t" proof(induction t) case (Node l a r) have "(2::nat) ^ min_height (Node l a r) \ 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def) - also have "\ \ size(Node l a r) + 1" using Node.IH by simp + also have "\ \ size1(Node l a r)" using Node.IH by simp finally show ?case . qed simp @@ -194,7 +194,7 @@ apply(induction t) apply simp apply (simp add: min_def max_def) -by (metis le_antisym le_trans min_hight_le_height) +by (metis le_antisym le_trans min_height_le_height) lemma size1_if_complete: "complete t \ size1 t = 2 ^ height t" by (induction t) auto @@ -202,102 +202,106 @@ lemma size_if_complete: "complete t \ size t = 2 ^ height t - 1" using size1_if_complete[simplified size1_def] by fastforce -lemma complete_if_size: "size t = 2 ^ height t - 1 \ complete t" +lemma complete_if_size1_height: "size1 t = 2 ^ height t \ complete t" proof (induct "height t" arbitrary: t) - case 0 thus ?case by (simp add: size_0_iff_Leaf) + case 0 thus ?case by (simp add: height_0_iff_Leaf) next case (Suc h) hence "t \ Leaf" by auto then obtain l a r where [simp]: "t = Node l a r" by (auto simp: neq_Leaf_iff) have 1: "height l \ h" and 2: "height r \ h" using Suc(2) by(auto) - have 3: "~ height l < h" + have 3: "\ height l < h" proof assume 0: "height l < h" - have "size t = size l + (size r + 1)" by simp - also note size_height[of l] + have "size1 t = size1 l + size1 r" by simp + also note size1_height[of l] also note size1_height[of r] - also have "(2::nat) ^ height l - 1 < 2 ^ h - 1" + also have "(2::nat) ^ height l < 2 ^ h" using 0 by (simp add: diff_less_mono) also have "(2::nat) ^ height r \ 2 ^ h" using 2 by simp - also have "(2::nat) ^ h - 1 + 2 ^ h = 2 ^ (Suc h) - 1" by (simp) - also have "\ = size t" using Suc(2,3) by simp + also have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp) + also have "\ = size1 t" using Suc(2,3) by simp finally show False by (simp add: diff_le_mono) qed have 4: "~ height r < h" proof assume 0: "height r < h" - have "size t = (size l + 1) + size r" by simp - also note size_height[of r] + have "size1 t = size1 l + size1 r" by simp + also note size1_height[of r] also note size1_height[of l] - also have "(2::nat) ^ height r - 1 < 2 ^ h - 1" + also have "(2::nat) ^ height r < 2 ^ h" using 0 by (simp add: diff_less_mono) also have "(2::nat) ^ height l \ 2 ^ h" using 1 by simp - also have "(2::nat) ^ h + (2 ^ h - 1) = 2 ^ (Suc h) - 1" by (simp) - also have "\ = size t" using Suc(2,3) by simp + also have "(2::nat) ^ h +2 ^ h = 2 ^ (Suc h)" by (simp) + also have "\ = size1 t" using Suc(2,3) by simp finally show False by (simp add: diff_le_mono) qed from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+ - hence "size l = 2 ^ height l - 1" "size r = 2 ^ height r - 1" - using Suc(3) size_height[of l] size_height[of r] by (auto) + hence "size1 l = 2 ^ height l" "size1 r = 2 ^ height r" + using Suc(3) size1_height[of l] size1_height[of r] by (auto) with * Suc(1) show ?case by simp qed -lemma complete_iff_size: "complete t \ size t = 2 ^ height t - 1" -using complete_if_size size_if_complete by blast - -text\A better lower bound for incomplete trees:\ +text\The following proof involves \\\/\>\ chains rather than the standard +\\\/\<\ chains. To chain the elements together the transitivity rules \xtrans\ +are used.\ -lemma min_height_le_size_if_incomplete: - "\ complete t \ 2 ^ min_height t \ size t" -proof(induction t) - case Leaf thus ?case by simp +lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \ complete t" +proof (induct "min_height t" arbitrary: t) + case 0 thus ?case by (simp add: size_0_iff_Leaf size1_def) next - case (Node l a r) - show ?case (is "?l \ ?r") - proof (cases "complete l") - case l: True thus ?thesis - proof (cases "complete r") - case r: True - have "height l \ height r" using Node.prems l r by simp - hence "?l < 2 ^ min_height l + 2 ^ min_height r" - using l r by (simp add: min_def complete_iff_height) - also have "\ = (size l + 1) + (size r + 1)" - using l r size_if_complete[where ?'a = 'a] - by (simp add: complete_iff_height) - also have "\ \ ?r + 1" by simp - finally show ?thesis by arith - next - case r: False - have "?l \ 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def) - also have "\ \ size l + 1 + size r" - using Node.IH(2)[OF r] l size_if_complete[where ?'a = 'a] - by (simp add: complete_iff_height) - also have "\ = ?r" by simp - finally show ?thesis . - qed - next - case l: False thus ?thesis - proof (cases "complete r") - case r: True - have "?l \ 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def) - also have "\ \ size l + (size r + 1)" - using Node.IH(1)[OF l] r size_if_complete[where ?'a = 'a] - by (simp add: complete_iff_height) - also have "\ = ?r" by simp - finally show ?thesis . - next - case r: False - have "?l \ 2 ^ min_height l + 2 ^ min_height r" - by (simp add: min_def) - also have "\ \ size l + size r" - using Node.IH(1)[OF l] Node.IH(2)[OF r] by (simp) - also have "\ \ ?r" by simp - finally show ?thesis . - qed + case (Suc h) + hence "t \ Leaf" by auto + then obtain l a r where [simp]: "t = Node l a r" + by (auto simp: neq_Leaf_iff) + have 1: "h \ min_height l" and 2: "h \ min_height r" using Suc(2) by(auto) + have 3: "\ h < min_height l" + proof + assume 0: "h < min_height l" + have "size1 t = size1 l + size1 r" by simp + also note min_height_size1[of l] + also(xtrans) note min_height_size1[of r] + also(xtrans) have "(2::nat) ^ min_height l > 2 ^ h" + using 0 by (simp add: diff_less_mono) + also(xtrans) have "(2::nat) ^ min_height r \ 2 ^ h" using 2 by simp + also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp) + also have "\ = size1 t" using Suc(2,3) by simp + finally show False by (simp add: diff_le_mono) qed + have 4: "\ h < min_height r" + proof + assume 0: "h < min_height r" + have "size1 t = size1 l + size1 r" by simp + also note min_height_size1[of l] + also(xtrans) note min_height_size1[of r] + also(xtrans) have "(2::nat) ^ min_height r > 2 ^ h" + using 0 by (simp add: diff_less_mono) + also(xtrans) have "(2::nat) ^ min_height l \ 2 ^ h" using 1 by simp + also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp) + also have "\ = size1 t" using Suc(2,3) by simp + finally show False by (simp add: diff_le_mono) + qed + from 1 2 3 4 have *: "min_height l = h" "min_height r = h" by linarith+ + hence "size1 l = 2 ^ min_height l" "size1 r = 2 ^ min_height r" + using Suc(3) min_height_size1[of l] min_height_size1[of r] by (auto) + with * Suc(1) show ?case + by (simp add: complete_iff_height) qed +lemma complete_iff_size1: "complete t \ size1 t = 2 ^ height t" +using complete_if_size1_height size1_if_complete by blast + +text\Better bounds for incomplete trees:\ + +lemma size1_height_if_incomplete: + "\ complete t \ size1 t < 2 ^ height t" +by (meson antisym_conv complete_iff_size1 not_le size1_height) + +lemma min_height_size1_if_incomplete: + "\ complete t \ 2 ^ min_height t < size1 t" +by (metis complete_if_size1_min_height le_less min_height_size1) + subsection \@{const balanced}\ @@ -332,16 +336,16 @@ case False have "(2::nat) ^ min_height t < 2 ^ height t'" proof - - have "(2::nat) ^ min_height t \ size t" - by(rule min_height_le_size_if_incomplete[OF False]) - also note assms(2) - also have "size t' \ 2 ^ height t' - 1" by(rule size_height) + have "(2::nat) ^ min_height t < size1 t" + by(rule min_height_size1_if_incomplete[OF False]) + also have "size1 t \ size1 t'" using assms(2) by (simp add: size1_def) + also have "size1 t' \ 2 ^ height t'" by(rule size1_height) finally show ?thesis using power_eq_0_iff[of "2::nat" "height t'"] by linarith qed hence *: "min_height t < height t'" by simp have "min_height t + 1 = height t" - using min_hight_le_height[of t] assms(1) False + using min_height_le_height[of t] assms(1) False by (simp add: complete_iff_height balanced_def) with * show ?thesis by arith qed diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Nat.thy Mon Dec 12 17:40:06 2016 +0100 @@ -10,7 +10,7 @@ section \Natural numbers\ theory Nat - imports Inductive Typedef Fun Rings +imports Inductive Typedef Fun Rings begin named_theorems arith "arith facts -- only ground formulas" @@ -742,6 +742,8 @@ lemma less_Suc_eq_0_disj: "m < Suc n \ m = 0 \ (\j. m = Suc j \ j < n)" by (cases m) simp_all +lemma All_less_Suc: "(\i < Suc n. P i) = (P n \ (\i < n. P i))" +by (auto simp: less_Suc_eq) subsubsection \Monotonicity of Addition\ diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Dec 12 17:40:06 2016 +0100 @@ -125,6 +125,14 @@ code_pred predicate_where_argument_is_neg_condition_and_in_equation . +text {* Another related example that required slight adjustment of the proof procedure *} + +inductive if_as_predicate :: "bool \ 'a \ 'a \ 'a \ bool" +where + "condition \ if_as_predicate condition then_value else_value then_value" +| "\ condition \ if_as_predicate condition then_value else_value else_value" + +code_pred [show_proof_trace] if_as_predicate . inductive zerozero :: "nat * nat => bool" where diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/ROOT --- a/src/HOL/ROOT Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/ROOT Mon Dec 12 17:40:06 2016 +0100 @@ -152,9 +152,6 @@ Abs_Int1_parity Abs_Int1_const Abs_Int3 - "Abs_Int_ITP/Abs_Int1_parity_ITP" - "Abs_Int_ITP/Abs_Int1_const_ITP" - "Abs_Int_ITP/Abs_Int3_ITP" Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Mon Dec 12 17:40:06 2016 +0100 @@ -185,7 +185,7 @@ val thy = Proof_Context.theory_of ctxt val assm_ths0 = map (Skip_Proof.make_thm thy) assms val ((assm_name, _), ctxt) = ctxt - |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 2 else 0) + |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0) |> Local_Theory.note ((@{binding thms}, []), assm_ths0) fun ref_of th = (Facts.named (Thm.derivation_name th), []) diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Dec 12 17:40:06 2016 +0100 @@ -1529,7 +1529,7 @@ val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, []) fun predicatify completish tm = - if completish > 0 then + if completish > 1 then IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm), fTrue_iconst) else IApp (predicator_iconst, tm) @@ -1733,14 +1733,14 @@ fold (fn ((helper_s, needs_sound), ths) => if (needs_sound andalso not sound) orelse (helper_s <> unmangled_s andalso - (completish < 2 orelse could_specialize)) then + (completish < 3 orelse could_specialize)) then I else ths ~~ (1 upto length ths) |> maps (dub_and_inst needs_sound o apfst (apsnd Thm.prop_of)) |> make_facts |> union (op = o apply2 #iformula)) - (if completish >= 2 then completish_helper_table else helper_table) + (if completish >= 3 then completish_helper_table else helper_table) end | NONE => I) fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab = @@ -2168,7 +2168,7 @@ fun default_mono level completish = {maybe_finite_Ts = [@{typ bool}], surely_infinite_Ts = (case level of Nonmono_Types (Strict, _) => [] | _ => known_infinite_types), - maybe_nonmono_Ts = [if completish >= 2 then tvar_a else @{typ bool}]} + maybe_nonmono_Ts = [if completish >= 3 then tvar_a else @{typ bool}]} (* This inference is described in section 4 of Blanchette et al., "Encoding monomorphic and polymorphic types", TACAS 2013. *) diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Dec 12 17:40:06 2016 +0100 @@ -14,6 +14,7 @@ val morph_bnf: morphism -> bnf -> bnf val morph_bnf_defs: morphism -> bnf -> bnf + val permute_deads: (typ list -> typ list) -> bnf -> bnf val transfer_bnf: theory -> bnf -> bnf val bnf_of: Proof.context -> string -> bnf option val bnf_of_global: theory -> string -> bnf option @@ -660,6 +661,8 @@ fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I I; +fun permute_deads perm = map_bnf I I I I I I perm I I I I I I I I I I; + val transfer_bnf = morph_bnf o Morphism.transfer_morphism; structure Data = Generic_Data diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Dec 12 17:40:06 2016 +0100 @@ -341,7 +341,8 @@ fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars []; val size_gen_o_map_thmss = - if nested_size_gen_o_maps_complete then + if nested_size_gen_o_maps_complete + andalso forall (fn TFree (_, S) => S = @{sort type}) As then @{map 3} (fn goal => fn size_def => fn rec_o_map => Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Dec 12 17:40:06 2016 +0100 @@ -152,6 +152,7 @@ THEN TRY ( let val prems' = maps dest_conjunct_prem (take nargs prems) + |> filter is_equationlike in rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 diff -r 5d2cef77373c -r 628b271c5b8b src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Dec 12 16:54:15 2016 +0100 +++ b/src/HOL/Transcendental.thy Mon Dec 12 17:40:06 2016 +0100 @@ -2634,6 +2634,10 @@ and less_powr_iff = log_less_iff[symmetric] and le_powr_iff = log_le_iff[symmetric] +lemma gr_one_powr[simp]: + fixes x y :: real shows "\ x > 1; y > 0 \ \ 1 < x powr y" +by(simp add: less_powr_iff) + lemma floor_log_eq_powr_iff: "x > 0 \ b > 1 \ \log b x\ = k \ b powr k \ x \ x < b powr (k + 1)" by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff) @@ -2712,6 +2716,7 @@ lemma log_powr: "x \ 0 \ log b (x powr y) = y * log b x" by (simp add: log_def ln_powr) +(* [simp] is not worth it, interferes with some proofs *) lemma log_nat_power: "0 < x \ log b (x^n) = real n * log b x" by (simp add: log_powr powr_realpow [symmetric]) diff -r 5d2cef77373c -r 628b271c5b8b src/Pure/Admin/ci_api.scala --- a/src/Pure/Admin/ci_api.scala Mon Dec 12 16:54:15 2016 +0100 +++ b/src/Pure/Admin/ci_api.scala Mon Dec 12 17:40:06 2016 +0100 @@ -32,7 +32,7 @@ def build_jobs(): List[String] = for { - job <- JSON.array(invoke(root()), "jobs") + job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil) _class <- JSON.string(job, "_class") if _class == "hudson.model.FreeStyleProject" name <- JSON.string(job, "name") @@ -56,7 +56,8 @@ for { build <- JSON.array( - invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds") + invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds") + .getOrElse(Nil) number <- JSON.int(build, "number") timestamp <- JSON.long(build, "timestamp") } yield { @@ -64,7 +65,7 @@ val output = Url(job_prefix + "/consoleText") val session_logs = for { - artifact <- JSON.array(build, "artifacts") + artifact <- JSON.array(build, "artifacts").getOrElse(Nil) log_path <- JSON.string(artifact, "relativePath") session <- (log_path match { case Log_Session(name) => Some(name) case _ => None }) } yield (session -> Url(job_prefix + "/artifact/" + log_path)) diff -r 5d2cef77373c -r 628b271c5b8b src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Mon Dec 12 16:54:15 2016 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Dec 12 17:40:06 2016 +0100 @@ -97,7 +97,7 @@ private val remote_builds = List( List(Remote_Build("lxbroy8", - options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-7a7b742897e9'", + options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-8529546198aa'", args = "-N -g timing")), List(Remote_Build("lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")), List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), @@ -126,7 +126,7 @@ Build_History.remote_build_history(ssh, isabelle_repos, isabelle_repos.ext(r.host), - isabelle_repos_source = isabelle_release_source, + isabelle_repos_source = isabelle_dev_source, self_update = self_update, push_isabelle_home = push_isabelle_home, options = diff -r 5d2cef77373c -r 628b271c5b8b src/Pure/General/json.scala --- a/src/Pure/General/json.scala Mon Dec 12 16:54:15 2016 +0100 +++ b/src/Pure/General/json.scala Mon Dec 12 17:40:06 2016 +0100 @@ -7,48 +7,163 @@ package isabelle +import scala.util.parsing.json.{JSONObject, JSONArray} + object JSON { - /* parse */ - - def parse(text: String): Any = - scala.util.parsing.json.JSON.parseFull(text) getOrElse error("Malformed JSON") + type T = Any + type S = String - /* field access */ + /* standard format */ + + def parse(s: S): T = Format.unapply(s) getOrElse error("Malformed JSON") + + object Format + { + def unapply(s: S): Option[T] = + try { scala.util.parsing.json.JSON.parseFull(s) } + catch { case ERROR(_) => None } + + def apply(json: T): S = + { + val result = new StringBuilder + + def string(s: String) + { + result += '"' + result ++= scala.util.parsing.json.JSONFormat.quoteString(s) + result += '"' + } + + def array(list: List[T]) + { + result += '[' + Library.separate(None, list.map(Some(_))).foreach({ + case None => result += ',' + case Some(x) => json_format(x) + }) + result += ']' + } + + def object_(obj: Map[String, T]) + { + result += '{' + Library.separate(None, obj.toList.map(Some(_))).foreach({ + case None => result += ',' + case Some((x, y)) => + string(x) + result += ':' + json_format(y) + }) + result += '}' + } - def any(obj: Any, name: String): Option[Any] = + def json_format(x: T) + { + x match { + case null => result ++= "null" + case _: Int | _: Long | _: Boolean => result ++= x.toString + case n: Double => + val i = n.toLong + result ++= (if (i.toDouble == n) i.toString else n.toString) + case s: String => string(s) + case JSONObject(obj) => object_(obj) + case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) => + object_(obj.asInstanceOf[Map[String, T]]) + case JSONArray(list) => array(list) + case list: List[T] => array(list) + case _ => error("Bad JSON value: " + x.toString) + } + } + + json_format(json) + result.toString + } + } + + + /* numbers */ + + object Number + { + object Double { + def unapply(json: T): Option[scala.Double] = + json match { + case x: scala.Double => Some(x) + case x: scala.Long => Some(x.toDouble) + case x: scala.Int => Some(x.toDouble) + case _ => None + } + } + + object Long { + def unapply(json: T): Option[scala.Long] = + json match { + case x: scala.Double if x.toLong.toDouble == x => Some(x.toLong) + case x: scala.Long => Some(x) + case x: scala.Int => Some(x.toLong) + case _ => None + } + } + + object Int { + def unapply(json: T): Option[scala.Int] = + json match { + case x: scala.Double if x.toInt.toDouble == x => Some(x.toInt) + case x: scala.Long if x.toInt.toLong == x => Some(x.toInt) + case x: scala.Int => Some(x) + case _ => None + } + } + } + + + /* object values */ + + def value(obj: T, name: String): Option[T] = obj match { - case m: Map[String, Any] => m.get(name) + case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) => + m.asInstanceOf[Map[String, T]].get(name) case _ => None } - def array(obj: Any, name: String): List[Any] = - any(obj, name) match { - case Some(a: List[Any]) => a - case _ => Nil + def value[A](obj: T, name: String, unapply: T => Option[A]): Option[A] = + for { + json <- value(obj, name) + x <- unapply(json) + } yield x + + def array(obj: T, name: String): Option[List[T]] = + value(obj, name) match { + case Some(a: List[T]) => Some(a) + case _ => None } - def string(obj: Any, name: String): Option[String] = - any(obj, name) match { + def array[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] = + for { + a0 <- array(obj, name) + a = a0.map(unapply(_)) + if a.forall(_.isDefined) + } yield a.map(_.get) + + def string(obj: T, name: String): Option[String] = + value(obj, name) match { case Some(x: String) => Some(x) case _ => None } - def double(obj: Any, name: String): Option[Double] = - any(obj, name) match { - case Some(x: Double) => Some(x) - case _ => None - } + def double(obj: T, name: String): Option[Double] = + value(obj, name, Number.Double.unapply) + + def long(obj: T, name: String): Option[Long] = + value(obj, name, Number.Long.unapply) - def long(obj: Any, name: String): Option[Long] = - double(obj, name).map(_.toLong) + def int(obj: T, name: String): Option[Int] = + value(obj, name, Number.Int.unapply) - def int(obj: Any, name: String): Option[Int] = - double(obj, name).map(_.toInt) - - def bool(obj: Any, name: String): Option[Boolean] = - any(obj, name) match { + def bool(obj: T, name: String): Option[Boolean] = + value(obj, name) match { case Some(x: Boolean) => Some(x) case _ => None } diff -r 5d2cef77373c -r 628b271c5b8b src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Mon Dec 12 16:54:15 2016 +0100 +++ b/src/Pure/PIDE/text.scala Mon Dec 12 17:40:06 2016 +0100 @@ -37,9 +37,9 @@ { // denotation: {start} Un {i. start < i & i < stop} if (start > stop) - error("Bad range: [" + start.toString + ":" + stop.toString + "]") + error("Bad range: [" + start.toString + ".." + stop.toString + "]") - override def toString: String = "[" + start.toString + ":" + stop.toString + "]" + override def toString: String = "[" + start.toString + ".." + stop.toString + "]" def length: Int = stop - start