# HG changeset patch # User eberlm # Date 1456484256 -3600 # Node ID 8c47e7fcdb8d1263f47999427699af2bc2395079 # Parent 2497c966ba2bc2b345dde6f5d62d544a42e6f963# Parent f1b0908028cfed1a6f5967e6fff2d0a806b64302 Merged diff -r 2497c966ba2b -r 8c47e7fcdb8d NEWS --- a/NEWS Thu Feb 25 16:54:24 2016 +0100 +++ b/NEWS Fri Feb 26 11:57:36 2016 +0100 @@ -156,6 +156,10 @@ *** System *** +* The Isabelle system environment always ensures that the main +executables are found within the PATH: isabelle, isabelle_process, +isabelle_scala_script. + * SML/NJ is no longer supported. diff -r 2497c966ba2b -r 8c47e7fcdb8d lib/scripts/getfunctions --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/getfunctions Fri Feb 26 11:57:36 2016 +0100 @@ -0,0 +1,206 @@ +# -*- shell-script -*- :mode=shellscript: +# +# Author: Makarius +# +# Isabelle shell functions, with on-demand re-initialization for +# non-interactive bash processess. NB: bash shell functions are not portable +# and may be dropped by aggressively POSIX-conformant versions of /bin/sh. + +if type splitarray >/dev/null 2>/dev/null +then + : +else + +if [ "$OSTYPE" = cygwin ]; then + function platform_path() { cygpath -i -C UTF8 -w -p "$@"; } +else + function platform_path() { echo "$@"; } +fi +export -f platform_path + +#GNU tar (notably on Mac OS X) +if [ -x /usr/bin/gnutar ]; then + function tar() { /usr/bin/gnutar "$@"; } + export -f tar +fi + +#shared library convenience +function librarypath () +{ + for X in "$@" + do + case "$ISABELLE_PLATFORM" in + *-darwin) + if [ -z "$DYLD_LIBRARY_PATH" ]; then + DYLD_LIBRARY_PATH="$X" + else + DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH" + fi + export DYLD_LIBRARY_PATH + ;; + *) + if [ -z "$LD_LIBRARY_PATH" ]; then + LD_LIBRARY_PATH="$X" + else + LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH" + fi + export LD_LIBRARY_PATH + ;; + esac + done +} +export -f librarypath + +#robust invocation via ISABELLE_JDK_HOME +function isabelle_jdk () +{ + if [ -z "$ISABELLE_JDK_HOME" ]; then + echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2 + return 127 + else + local PRG="$1"; shift + "$ISABELLE_JDK_HOME/bin/$PRG" "$@" + fi +} +export -f isabelle_jdk + +#robust invocation via JAVA_HOME +function isabelle_java () +{ + if [ -z "$JAVA_HOME" ]; then + echo "Unknown JAVA_HOME -- Java unavailable" >&2 + return 127 + else + local PRG="$1"; shift + "$JAVA_HOME/bin/$PRG" "$@" + fi +} +export -f isabelle_java + +#robust invocation via SCALA_HOME +function isabelle_scala () +{ + if [ -z "$JAVA_HOME" ]; then + echo "Unknown JAVA_HOME -- Java unavailable" >&2 + return 127 + elif [ -z "$SCALA_HOME" ]; then + echo "Unknown SCALA_HOME -- Scala unavailable" >&2 + return 127 + else + local PRG="$1"; shift + "$SCALA_HOME/bin/$PRG" "$@" + fi +} +export -f isabelle_scala + +#classpath +function classpath () +{ + for X in "$@" + do + if [ -z "$ISABELLE_CLASSPATH" ]; then + ISABELLE_CLASSPATH="$X" + else + ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" + fi + done + export ISABELLE_CLASSPATH +} +export -f classpath + +#administrative build +if [ -e "$ISABELLE_HOME/Admin/build" ]; then + function isabelle_admin_build () + { + "$ISABELLE_HOME/Admin/build" "$@" + } +else + function isabelle_admin_build () { return 0; } +fi +export -f isabelle_admin_build + +#arrays +function splitarray () +{ + SPLITARRAY=() + local IFS="$1"; shift + for X in $* + do + SPLITARRAY["${#SPLITARRAY[@]}"]="$X" + done +} +export -f splitarray + +#init component tree +function init_component () +{ + local COMPONENT="$1" + case "$COMPONENT" in + /*) ;; + *) + echo >&2 "Absolute component path required: \"$COMPONENT\"" + exit 2 + ;; + esac + + if [ -d "$COMPONENT" ]; then + if [ -z "$ISABELLE_COMPONENTS" ]; then + ISABELLE_COMPONENTS="$COMPONENT" + else + ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" + fi + else + echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" + if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then + ISABELLE_COMPONENTS_MISSING="$COMPONENT" + else + ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" + fi + fi + + if [ -f "$COMPONENT/etc/settings" ]; then + source "$COMPONENT/etc/settings" + local RC="$?" + if [ "$RC" -ne 0 ]; then + echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" + exit 2 + fi + fi + if [ -f "$COMPONENT/etc/components" ]; then + init_components "$COMPONENT" "$COMPONENT/etc/components" + fi +} +export -f init_component + +#init component forest +function init_components () +{ + local BASE="$1" + local CATALOG="$2" + local COMPONENT="" + local -a COMPONENTS=() + + if [ ! -f "$CATALOG" ]; then + echo >&2 "Bad component catalog file: \"$CATALOG\"" + exit 2 + fi + + { + while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } + do + case "$REPLY" in + \#* | "") ;; + /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;; + *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;; + esac + done + } < "$CATALOG" + + for COMPONENT in "${COMPONENTS[@]}" + do + init_component "$COMPONENT" + done +} +export -f init_components + +fi diff -r 2497c966ba2b -r 8c47e7fcdb8d lib/scripts/getsettings --- a/lib/scripts/getsettings Thu Feb 25 16:54:24 2016 +0100 +++ b/lib/scripts/getsettings Fri Feb 26 11:57:36 2016 +0100 @@ -1,20 +1,21 @@ # -*- shell-script -*- :mode=shellscript: # -# Author: Markus Wenzel, TU Muenchen +# Author: Makarius # -# getsettings - bash source script to augment current env. +# Static Isabelle environment for root of process tree. + +export ISABELLE_HOME + +export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions" +source "$BASH_ENV" + if [ -z "$ISABELLE_SETTINGS_PRESENT" ] then -set -o allexport - -ISABELLE_SETTINGS_PRESENT=true +export ISABELLE_SETTINGS_PRESENT=true -#GNU tar (notably on Mac OS X) -if [ -x /usr/bin/gnutar ]; then - function tar() { /usr/bin/gnutar "$@"; } -fi +set -o allexport #sane environment defaults (notably on Mac OS X) if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then @@ -36,7 +37,6 @@ USER_HOME="$(cygpath -u "$USERPROFILE")" fi - function platform_path() { cygpath -i -C UTF8 -w -p "$@"; } CYGWIN_ROOT="$(platform_path "/")" ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")" @@ -49,33 +49,15 @@ ISABELLE_ROOT="$ISABELLE_HOME" - function platform_path() { echo "$@"; } - ISABELLE_CLASSPATH="$CLASSPATH" unset CLASSPATH fi -export ISABELLE_HOME - -#key executables +#main executables ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process" ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script" - -function isabelle () -{ - "$ISABELLE_TOOL" "$@" -} - -function isabelle_process () -{ - "$ISABELLE_PROCESS" "$@" -} - -function isabelle_scala_script () -{ - "$ISABELLE_SCALA_SCRIPT" "$@" -} +PATH="$ISABELLE_HOME/bin:$PATH" #platform source "$ISABELLE_HOME/lib/scripts/isabelle-platform" @@ -88,186 +70,12 @@ ISABELLE_ID="" [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="" -#sometimes users put strange things in here ... -unset ENV -unset BASH_ENV - -#shared library convenience -function librarypath () -{ - for X in "$@" - do - case "$ISABELLE_PLATFORM" in - *-darwin) - if [ -z "$DYLD_LIBRARY_PATH" ]; then - DYLD_LIBRARY_PATH="$X" - else - DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH" - fi - export DYLD_LIBRARY_PATH - ;; - *) - if [ -z "$LD_LIBRARY_PATH" ]; then - LD_LIBRARY_PATH="$X" - else - LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH" - fi - export LD_LIBRARY_PATH - ;; - esac - done -} - -#robust invocation via ISABELLE_JDK_HOME -function isabelle_jdk () -{ - if [ -z "$ISABELLE_JDK_HOME" ]; then - echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2 - return 127 - else - local PRG="$1"; shift - "$ISABELLE_JDK_HOME/bin/$PRG" "$@" - fi -} - -#robust invocation via JAVA_HOME -function isabelle_java () -{ - if [ -z "$JAVA_HOME" ]; then - echo "Unknown JAVA_HOME -- Java unavailable" >&2 - return 127 - else - local PRG="$1"; shift - "$JAVA_HOME/bin/$PRG" "$@" - fi -} - -#robust invocation via SCALA_HOME -function isabelle_scala () -{ - if [ -z "$JAVA_HOME" ]; then - echo "Unknown JAVA_HOME -- Java unavailable" >&2 - return 127 - elif [ -z "$SCALA_HOME" ]; then - echo "Unknown SCALA_HOME -- Scala unavailable" >&2 - return 127 - else - local PRG="$1"; shift - "$SCALA_HOME/bin/$PRG" "$@" - fi -} - -#administrative build -if [ -e "$ISABELLE_HOME/Admin/build" ]; then - function isabelle_admin_build () - { - "$ISABELLE_HOME/Admin/build" "$@" - } -else - function isabelle_admin_build () { return 0; } -fi - -#classpath -function classpath () -{ - for X in "$@" - do - if [ -z "$ISABELLE_CLASSPATH" ]; then - ISABELLE_CLASSPATH="$X" - else - ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X" - fi - done - export ISABELLE_CLASSPATH -} - -#arrays -function splitarray () -{ - SPLITARRAY=() - local IFS="$1"; shift - for X in $* - do - SPLITARRAY["${#SPLITARRAY[@]}"]="$X" - done -} - # components ISABELLE_COMPONENTS="" ISABELLE_COMPONENTS_MISSING="" -#init component tree -function init_component () -{ - local COMPONENT="$1" - case "$COMPONENT" in - /*) ;; - *) - echo >&2 "Absolute component path required: \"$COMPONENT\"" - exit 2 - ;; - esac - - if [ -d "$COMPONENT" ]; then - if [ -z "$ISABELLE_COMPONENTS" ]; then - ISABELLE_COMPONENTS="$COMPONENT" - else - ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT" - fi - else - echo >&2 "### Missing Isabelle component: \"$COMPONENT\"" - if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then - ISABELLE_COMPONENTS_MISSING="$COMPONENT" - else - ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT" - fi - fi - - if [ -f "$COMPONENT/etc/settings" ]; then - source "$COMPONENT/etc/settings" - local RC="$?" - if [ "$RC" -ne 0 ]; then - echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\"" - exit 2 - fi - fi - if [ -f "$COMPONENT/etc/components" ]; then - init_components "$COMPONENT" "$COMPONENT/etc/components" - fi -} - -#init component forest -function init_components () -{ - local BASE="$1" - local CATALOG="$2" - local COMPONENT="" - local -a COMPONENTS=() - - if [ ! -f "$CATALOG" ]; then - echo >&2 "Bad component catalog file: \"$CATALOG\"" - exit 2 - fi - - { - while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } - do - case "$REPLY" in - \#* | "") ;; - /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;; - *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;; - esac - done - } < "$CATALOG" - - for COMPONENT in "${COMPONENTS[@]}" - do - init_component "$COMPONENT" - done -} - #main components init_component "$ISABELLE_HOME" [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" diff -r 2497c966ba2b -r 8c47e7fcdb8d src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy Thu Feb 25 16:54:24 2016 +0100 +++ b/src/Doc/System/Scala.thy Fri Feb 26 11:57:36 2016 +0100 @@ -77,11 +77,7 @@ text \ The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run Isabelle/Scala source files stand-alone programs, by using a - suitable ``hash-bang'' line and executable file permissions. - - The subsequent example assumes that the main Isabelle binaries have been - installed in some directory that is included in @{setting PATH} (see also - @{tool "install"}): + suitable ``hash-bang'' line and executable file permissions. For example: @{verbatim [display] \#!/usr/bin/env isabelle_scala_script @@ -89,8 +85,12 @@ Console.println("browser_info = " + options.bool("browser_info")) Console.println("document = " + options.string("document"))\} - Alternatively the full @{file "$ISABELLE_HOME/bin/isabelle_scala_script"} - may be specified in expanded form. + This assumes that the executable may be found via the @{setting PATH} from + the process environment: this is the case when Isabelle settings are active, + e.g.\ in the context of the main Isabelle tool wrapper + \secref{sec:isabelle-tool}. Alternatively, the full @{file + "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in expanded + form. \ end diff -r 2497c966ba2b -r 8c47e7fcdb8d src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Thu Feb 25 16:54:24 2016 +0100 +++ b/src/HOL/Algebra/Exponent.thy Fri Feb 26 11:57:36 2016 +0100 @@ -11,304 +11,237 @@ section \Sylow's Theorem\ -subsection \The Combinatorial Argument Underlying the First Sylow Theorem\ +text \The Combinatorial Argument Underlying the First Sylow Theorem\ + + +subsection\Prime Theorems\ + +lemma prime_dvd_cases: + assumes pk: "p*k dvd m*n" and p: "prime p" + shows "(\x. k dvd x*n \ m = p*x) \ (\y. k dvd m*y \ n = p*y)" +proof - + have "p dvd m*n" using dvd_mult_left pk by blast + then consider "p dvd m" | "p dvd n" + using p prime_dvd_mult_eq_nat by blast + then show ?thesis + proof cases + case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) + then have "\x. k dvd x * n \ m = p * x" + using p pk by auto + then show ?thesis .. + next + case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) + then have "\y. k dvd m*y \ n = p*y" + using p pk by auto + then show ?thesis .. + qed +qed + +lemma prime_power_dvd_prod: + assumes pc: "p^c dvd m*n" and p: "prime p" + shows "\a b. a+b = c \ p^a dvd m \ p^b dvd n" +using pc +proof (induct c arbitrary: m n) + case 0 show ?case by simp +next + case (Suc c) + consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y" + using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force + then show ?case + proof cases + case (1 x) + with Suc.hyps [of x n] show "\a b. a + b = Suc c \ p ^ a dvd m \ p ^ b dvd n" + by force + next + case (2 y) + with Suc.hyps [of m y] show "\a b. a + b = Suc c \ p ^ a dvd m \ p ^ b dvd n" + by force + qed +qed + +lemma add_eq_Suc_lem: "a+b = Suc (x+y) \ a \ x \ b \ y" + by arith + +lemma prime_power_dvd_cases: + "\p^c dvd m * n; a + b = Suc c; prime p\ \ p ^ a dvd m \ p ^ b dvd n" + using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem) + +text\needed in this form to prove Sylow's theorem\ +corollary div_combine: "\prime p; \ p ^ Suc r dvd n; p ^ (a + r) dvd n * k\ \ p ^ a dvd k" + by (metis add_Suc_right mult.commute prime_power_dvd_cases) + + +subsection\The Exponent Function\ definition exponent :: "nat => nat => nat" where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)" +lemma exponent_eq_0 [simp]: "\ prime p \ exponent p s = 0" + by (simp add: exponent_def) -text\Prime Theorems\ +lemma Suc_le_power: "Suc 0 < p \ Suc n \ p ^ n" + by (induct n) (auto simp: Suc_le_eq le_less_trans) + +text\An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\ +lemma power_dvd_bound: "\p ^ n dvd a; Suc 0 < p; 0 < a\ \ n < a" + by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans) -lemma prime_iff: - "prime p \ Suc 0 < p \ (\a b. p dvd a * b \ p dvd a \ p dvd b)" - by (auto simp add: prime_gt_Suc_0_nat) - (metis One_nat_def Suc_lessD dvd_refl nat_dvd_not_less not_prime_eq_prod_nat) - -lemma zero_less_prime_power: - fixes p::nat shows "prime p ==> 0 < p^a" -by (force simp add: prime_iff) +lemma exponent_ge: + assumes "p ^ k dvd n" "prime p" "0 < n" + shows "k \ exponent p n" +proof - + have "Suc 0 < p" + using \prime p\ by (simp add: prime_def) + with assms show ?thesis + by (simp add: \prime p\ exponent_def) (meson Greatest_le power_dvd_bound) +qed -lemma zero_less_card_empty: "[| finite S; S \ {} |] ==> 0 < card(S)" -by (rule ccontr, simp) +lemma power_exponent_dvd: "p ^ exponent p s dvd s" +proof (cases "s = 0") + case True then show ?thesis by simp +next + case False then show ?thesis + apply (simp add: exponent_def, clarify) + apply (rule GreatestI [where k = 0]) + apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound) + done +qed + +lemma power_Suc_exponent_Not_dvd: + "\p * p ^ exponent p s dvd s; prime p\ \ s = 0" + by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc) +lemma exponent_power_eq [simp]: "prime p \ exponent p (p ^ a) = a" + apply (simp add: exponent_def) + apply (rule Greatest_equality, simp) + apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le) + done -lemma prime_dvd_cases: - fixes p::nat - shows "[| p*k dvd m*n; prime p |] - ==> (\x. k dvd x*n & m = p*x) | (\y. k dvd m*y & n = p*y)" -apply (simp add: prime_iff) -apply (frule dvd_mult_left) -apply (subgoal_tac "p dvd m | p dvd n") - prefer 2 apply blast -apply (erule disjE) -apply (rule disjI1) -apply (rule_tac [2] disjI2) -apply (auto elim!: dvdE) -done +lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0" + apply (case_tac "prime p") + apply (metis exponent_power_eq nat_power_eq_Suc_0_iff) + apply simp + done + +lemma exponent_equalityI: + "(\r. p ^ r dvd a \ p ^ r dvd b) \ exponent p a = exponent p b" + by (simp add: exponent_def) + +lemma exponent_mult_add: + assumes "a > 0" "b > 0" + shows "exponent p (a * b) = (exponent p a) + (exponent p b)" +proof (cases "prime p") + case False then show ?thesis by simp +next + case True show ?thesis + proof (rule order_antisym) + show "exponent p a + exponent p b \ exponent p (a * b)" + by (rule exponent_ge) (auto simp: mult_dvd_mono power_add power_exponent_dvd \prime p\ assms) + next + { assume "exponent p a + exponent p b < exponent p (a * b)" + then have "p ^ (Suc (exponent p a + exponent p b)) dvd a * b" + by (meson Suc_le_eq power_exponent_dvd power_le_dvd) + with prime_power_dvd_cases [where a = "Suc (exponent p a)" and b = "Suc (exponent p b)"] + have False + by (metis Suc_n_not_le_n True add_Suc add_Suc_right assms exponent_ge) + } + then show "exponent p (a * b) \ exponent p a + exponent p b" by (blast intro: leI) + qed +qed + +lemma not_divides_exponent_0: "~ (p dvd n) \ exponent p n = 0" + apply (case_tac "exponent p n", simp) + by (metis dvd_mult_left power_Suc power_exponent_dvd) -lemma prime_power_dvd_cases [rule_format (no_asm)]: -fixes p::nat - shows "prime p - ==> \m n. p^c dvd m*n --> - (\a b. a+b = Suc c --> p^a dvd m | p^b dvd n)" -apply (induct c) -apply (metis dvd_1_left nat_power_eq_Suc_0_iff one_is_add) -(*inductive step*) -apply simp -apply clarify -apply (erule prime_dvd_cases [THEN disjE], assumption, auto) -(*case 1: p dvd m*) - apply (case_tac "a") - apply simp - apply clarify - apply (drule spec, drule spec, erule (1) notE impE) - apply (drule_tac x = nat in spec) - apply (drule_tac x = b in spec) - apply simp -(*case 2: p dvd n*) -apply (case_tac "b") - apply simp -apply clarify -apply (drule spec, drule spec, erule (1) notE impE) -apply (drule_tac x = a in spec) -apply (drule_tac x = nat in spec, simp) -done - -(*needed in this form in Sylow.ML*) -lemma div_combine: - fixes p::nat - shows "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] ==> p ^ a dvd k" -by (metis add_Suc add.commute prime_power_dvd_cases) - -(*Lemma for power_dvd_bound*) -lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n" -apply (induct n) -apply (simp (no_asm_simp)) -apply simp -apply (subgoal_tac "2 * n + 2 <= p * p^n", simp) -apply (subgoal_tac "2 * p^n <= p * p^n") -apply arith -apply (drule_tac k = 2 in mult_le_mono2, simp) -done - -(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*) -lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; a > 0|] ==> n < a" -apply (drule dvd_imp_le) -apply (drule_tac [2] n = n in Suc_le_power, auto) -done - - -text\Exponent Theorems\ +subsection\The Main Combinatorial Argument\ -lemma exponent_ge [rule_format]: - "[|p^k dvd n; prime p; 0 k <= exponent p n" -apply (simp add: exponent_def) -apply (erule Greatest_le) -apply (blast dest: prime_gt_Suc_0_nat power_dvd_bound) -done - -lemma power_exponent_dvd: "s>0 ==> (p ^ exponent p s) dvd s" -apply (simp add: exponent_def) -apply clarify -apply (rule_tac k = 0 in GreatestI) -prefer 2 apply (blast dest: prime_gt_Suc_0_nat power_dvd_bound, simp) -done - -lemma power_Suc_exponent_Not_dvd: - "[|(p * p ^ exponent p s) dvd s; prime p |] ==> s=0" -apply (subgoal_tac "p ^ Suc (exponent p s) dvd s") - prefer 2 apply simp -apply (rule ccontr) -apply (drule exponent_ge, auto) -done - -lemma exponent_power_eq [simp]: "prime p ==> exponent p (p^a) = a" -apply (simp add: exponent_def) -apply (rule Greatest_equality, simp) -apply (simp (no_asm_simp) add: prime_gt_Suc_0_nat power_dvd_imp_le) -done +lemma exponent_p_a_m_k_equation: + assumes "0 < m" "0 < k" "p \ 0" "k < p^a" + shows "exponent p (p^a * m - k) = exponent p (p^a - k)" +proof (rule exponent_equalityI [OF iffI]) + fix r + assume *: "p ^ r dvd p ^ a * m - k" + show "p ^ r dvd p ^ a - k" + proof - + have "k \ p ^ a * m" using assms + by (meson nat_dvd_not_less dvd_triv_left leI mult_pos_pos order.strict_trans) + then have "r \ a" + by (meson "*" \0 < k\ \k < p^a\ dvd_diffD1 dvd_triv_left leI less_imp_le_nat nat_dvd_not_less power_le_dvd) + then have "p^r dvd p^a * m" by (simp add: le_imp_power_dvd) + thus ?thesis + by (meson \k \ p ^ a * m\ \r \ a\ * dvd_diffD1 dvd_diff_nat le_imp_power_dvd) + qed +next + fix r + assume *: "p ^ r dvd p ^ a - k" + with assms have "r \ a" + by (metis diff_diff_cancel less_imp_le_nat nat_dvd_not_less nat_le_linear power_le_dvd zero_less_diff) + show "p ^ r dvd p ^ a * m - k" + proof - + have "p^r dvd p^a*m" + by (simp add: \r \ a\ le_imp_power_dvd) + then show ?thesis + by (meson assms * dvd_diffD1 dvd_diff_nat le_imp_power_dvd less_imp_le_nat \r \ a\) + qed +qed -lemma exponent_equalityI: - "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b" -by (simp (no_asm_simp) add: exponent_def) - -lemma exponent_eq_0 [simp]: "\ prime p ==> exponent p s = 0" -by (simp (no_asm_simp) add: exponent_def) - +lemma p_not_div_choose_lemma: + assumes eeq: "\i. Suc i < K \ exponent p (Suc i) = exponent p (Suc (j + i))" + and "k < K" + shows "exponent p (j + k choose k) = 0" +proof (cases "prime p") + case False then show ?thesis by simp +next + case True show ?thesis using \k < K\ + proof (induction k) + case 0 then show ?case by simp + next + case (Suc k) + then have *: "(Suc (j+k) choose Suc k) > 0" by simp + then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)" + by (metis Suc.IH Suc.prems Suc_lessD Suc_times_binomial_eq add.comm_neutral eeq exponent_mult_add + mult_pos_pos zero_less_Suc zero_less_mult_pos) + then show ?case + by (metis * add.commute add_Suc_right add_eq_self_zero exponent_mult_add zero_less_Suc) + qed +qed -(* exponent_mult_add, easy inclusion. Could weaken p \ prime to Suc 0 < p *) -lemma exponent_mult_add1: "[| a > 0; b > 0 |] - ==> (exponent p a) + (exponent p b) <= exponent p (a * b)" -apply (case_tac "prime p") -apply (rule exponent_ge) -apply (auto simp add: power_add) -by (metis mult_dvd_mono power_exponent_dvd) - -(* exponent_mult_add, opposite inclusion *) -lemma exponent_mult_add2: "[| a > 0; b > 0 |] - ==> exponent p (a * b) <= (exponent p a) + (exponent p b)" -apply (case_tac "prime p") -apply (rule leI, clarify) -apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto) -apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b") -apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans]) - prefer 3 apply assumption - prefer 2 apply simp -apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases) - apply (assumption, force, simp) -apply (blast dest: power_Suc_exponent_Not_dvd) +text\The lemma above, with two changes of variables\ +lemma p_not_div_choose: + assumes "k < K" and "k \ n" + and eeq: "\j. \0 \ exponent p (n - k + (K - j)) = exponent p (K - j)" + shows "exponent p (n choose k) = 0" +apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1]) +apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff) +apply (rule TrueI) done -lemma exponent_mult_add: "[| a > 0; b > 0 |] - ==> exponent p (a * b) = (exponent p a) + (exponent p b)" -by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym) - - -lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0" -apply (case_tac "exponent p n", simp) -apply (case_tac "n", simp) -apply (cut_tac s = n and p = p in power_exponent_dvd) -apply (auto dest: dvd_mult_left) -done - -lemma exponent_1_eq_0 [simp]: - fixes p::nat - shows "exponent p (Suc 0) = 0" -apply (case_tac "prime p") -apply (metis exponent_power_eq nat_power_eq_Suc_0_iff) -apply (simp add: prime_iff not_divides_exponent_0) -done - - -text\Main Combinatorial Argument\ - -lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b" -by (simp add: mult.commute[of a b]) - -lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)" -apply (rule_tac P = "%x. x <= b * c" in subst) -apply (rule mult_1_right) -apply (rule mult_le_mono, auto) -done - -lemma p_fac_forw_lemma: - "[| (m::nat) > 0; k > 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a" -apply (rule notnotD) -apply (rule notI) -apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption) -apply (drule less_imp_le [of a]) -apply (drule le_imp_power_dvd) -apply (drule_tac b = "p ^ r" in dvd_trans, assumption) -apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2 gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less mult.commute not_add_less2 xt1(10)) -done - -lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |] - ==> (p^r) dvd (p^a) - k" -apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto) -apply (subgoal_tac "p^r dvd p^a*m") - prefer 2 apply (blast intro: dvd_mult2) -apply (drule dvd_diffD1) - apply assumption - prefer 2 apply (blast intro: dvd_diff_nat) -apply (drule gr0_implies_Suc, auto) -done - - -lemma r_le_a_forw: - "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a" -by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto) - -lemma p_fac_backw: "[| m>0; k>0; (p::nat)\0; k < p^a; (p^r) dvd p^a - k |] - ==> (p^r) dvd (p^a)*m - k" -apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto) -apply (subgoal_tac "p^r dvd p^a*m") - prefer 2 apply (blast intro: dvd_mult2) -apply (drule dvd_diffD1) - apply assumption - prefer 2 apply (blast intro: dvd_diff_nat) -apply (drule less_imp_Suc_add, auto) -done - -lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\0; k < p^a |] - ==> exponent p (p^a * m - k) = exponent p (p^a - k)" -apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw) -done - -text\Suc rules that we have to delete from the simpset\ -lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right - -(*The bound K is needed; otherwise it's too weak to be used.*) -lemma p_not_div_choose_lemma [rule_format]: - "[| \i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] - ==> k exponent p ((j+k) choose k) = 0" -apply (cases "prime p") - prefer 2 apply simp -apply (induct k) -apply (simp (no_asm)) -(*induction step*) -apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0") - prefer 2 apply (simp, clarify) -apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) = - exponent p (Suc k)") - txt\First, use the assumed equation. We simplify the LHS to - @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"} - the common terms cancel, proving the conclusion.\ - apply (simp del: bad_Sucs add: exponent_mult_add) -apply (simp del: bad_Sucs add: mult_ac Suc_times_binomial exponent_mult_add) - -done - -(*The lemma above, with two changes of variables*) -lemma p_not_div_choose: - "[| kj. 0 exponent p (n - k + (K - j)) = exponent p (K - j)|] - ==> exponent p (n choose k) = 0" -apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma) - prefer 3 apply simp - prefer 2 apply assumption -apply (drule_tac x = "K - Suc i" in spec) -apply (simp add: Suc_diff_le) -done - - -lemma const_p_fac_right: - "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0" -apply (case_tac "prime p") - prefer 2 apply simp -apply (frule_tac a = a in zero_less_prime_power) -apply (rule_tac K = "p^a" in p_not_div_choose) - apply simp - apply simp - apply (case_tac "m") - apply (case_tac [2] "p^a") - apply auto -(*now the hard case, simplified to - exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *) -apply (subgoal_tac "00 ==> exponent p (((p^a) * m) choose p^a) = exponent p m" -apply (case_tac "prime p") - prefer 2 apply simp -apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m") - prefer 2 apply (force simp add: prime_iff) -txt\A similar trick to the one used in @{text p_not_div_choose_lemma}: - insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS, - first - transform the binomial coefficient, then use @{text exponent_mult_add}.\ -apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = - a + exponent p m") - apply (simp add: exponent_mult_add) -txt\one subgoal left!\ -apply (auto simp: mult_ac) -apply (subst times_binomial_minus1_eq, simp) -apply (simp add: diff_le_mono exponent_mult_add) -apply (metis const_p_fac_right mult.commute) -done +proposition const_p_fac: + assumes "m>0" + shows "exponent p (p^a * m choose p^a) = exponent p m" +proof (cases "prime p") + case False then show ?thesis by auto +next + case True + with assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \ p^a * m" + by (auto simp: prime_gt_0_nat) + have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0" + apply (rule p_not_div_choose [where K = "p^a"]) + using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono) + have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m" + proof - + have "p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1)) = p ^ a * (p ^ a * m choose p ^ a)" + using p One_nat_def times_binomial_minus1_eq by presburger + moreover have "exponent p (p ^ a) = a" + by (meson True exponent_power_eq) + ultimately show ?thesis + using * p + by (metis (no_types, lifting) One_nat_def exponent_1_eq_0 exponent_mult_add mult.commute mult.right_neutral nat_0_less_mult_iff zero_less_binomial) + qed + then show ?thesis + using True p exponent_mult_add by auto +qed end diff -r 2497c966ba2b -r 8c47e7fcdb8d src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Thu Feb 25 16:54:24 2016 +0100 +++ b/src/HOL/Algebra/Sylow.thy Fri Feb 26 11:57:36 2016 +0100 @@ -12,6 +12,10 @@ text\The combinatorial argument is in theory Exponent\ +lemma le_extend_mult: + fixes c::nat shows "\0 < c; a \ b\ \ a \ b * c" +by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero) + locale sylow = group + fixes p and a and m and calM and RelM assumes prime_p: "prime p" @@ -20,13 +24,14 @@ defines "calM == {s. s \ carrier(G) & card(s) = p^a}" and "RelM == {(N1,N2). N1 \ calM & N2 \ calM & (\g \ carrier(G). N1 = (N2 #> g) )}" +begin -lemma (in sylow) RelM_refl_on: "refl_on calM RelM" +lemma RelM_refl_on: "refl_on calM RelM" apply (auto simp add: refl_on_def RelM_def calM_def) apply (blast intro!: coset_mult_one [symmetric]) done -lemma (in sylow) RelM_sym: "sym RelM" +lemma RelM_sym: "sym RelM" proof (unfold sym_def RelM_def, clarify) fix y g assume "y \ calM" @@ -35,19 +40,20 @@ thus "\g'\carrier G. y = y #> g #> g'" by (blast intro: g) qed -lemma (in sylow) RelM_trans: "trans RelM" +lemma RelM_trans: "trans RelM" by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc) -lemma (in sylow) RelM_equiv: "equiv calM RelM" +lemma RelM_equiv: "equiv calM RelM" apply (unfold equiv_def) apply (blast intro: RelM_refl_on RelM_sym RelM_trans) done -lemma (in sylow) M_subset_calM_prep: "M' \ calM // RelM ==> M' \ calM" +lemma M_subset_calM_prep: "M' \ calM // RelM ==> M' \ calM" apply (unfold RelM_def) apply (blast elim!: quotientE) done +end subsection\Main Part of the Proof\ @@ -58,102 +64,87 @@ and M1_in_M: "M1 \ M" defines "H == {g. g\carrier G & M1 #> g = M1}" -lemma (in sylow_central) M_subset_calM: "M \ calM" -by (rule M_in_quot [THEN M_subset_calM_prep]) +begin -lemma (in sylow_central) card_M1: "card(M1) = p^a" -apply (cut_tac M_subset_calM M1_in_M) -apply (simp add: calM_def, blast) -done +lemma M_subset_calM: "M \ calM" + by (rule M_in_quot [THEN M_subset_calM_prep]) -lemma card_nonempty: "0 < card(S) ==> S \ {}" -by force +lemma card_M1: "card(M1) = p^a" + using M1_in_M M_subset_calM calM_def by blast + +lemma exists_x_in_M1: "\x. x \ M1" +using prime_p [THEN prime_gt_Suc_0_nat] card_M1 +by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI) -lemma (in sylow_central) exists_x_in_M1: "\x. x\M1" -apply (subgoal_tac "0 < card M1") - apply (blast dest: card_nonempty) -apply (cut_tac prime_p [THEN prime_gt_Suc_0_nat]) -apply (simp (no_asm_simp) add: card_M1) -done +lemma M1_subset_G [simp]: "M1 \ carrier G" + using M1_in_M M_subset_calM calM_def mem_Collect_eq subsetCE by blast -lemma (in sylow_central) M1_subset_G [simp]: "M1 \ carrier G" -apply (rule subsetD [THEN PowD]) -apply (rule_tac [2] M1_in_M) -apply (rule M_subset_calM [THEN subset_trans]) -apply (auto simp add: calM_def) -done - -lemma (in sylow_central) M1_inj_H: "\f \ H\M1. inj_on f H" - proof - - from exists_x_in_M1 obtain m1 where m1M: "m1 \ M1".. - have m1G: "m1 \ carrier G" by (simp add: m1M M1_subset_G [THEN subsetD]) - show ?thesis - proof - show "inj_on (\z\H. m1 \ z) H" - by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G) - show "restrict (op \ m1) H \ H \ M1" - proof (rule restrictI) - fix z assume zH: "z \ H" - show "m1 \ z \ M1" - proof - - from zH - have zG: "z \ carrier G" and M1zeq: "M1 #> z = M1" - by (auto simp add: H_def) - show ?thesis - by (rule subst [OF M1zeq], simp add: m1M zG rcosI) - qed +lemma M1_inj_H: "\f \ H\M1. inj_on f H" +proof - + from exists_x_in_M1 obtain m1 where m1M: "m1 \ M1".. + have m1G: "m1 \ carrier G" by (simp add: m1M M1_subset_G [THEN subsetD]) + show ?thesis + proof + show "inj_on (\z\H. m1 \ z) H" + by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G) + show "restrict (op \ m1) H \ H \ M1" + proof (rule restrictI) + fix z assume zH: "z \ H" + show "m1 \ z \ M1" + proof - + from zH + have zG: "z \ carrier G" and M1zeq: "M1 #> z = M1" + by (auto simp add: H_def) + show ?thesis + by (rule subst [OF M1zeq], simp add: m1M zG rcosI) qed qed qed +qed +end subsection\Discharging the Assumptions of @{text sylow_central}\ -lemma (in sylow) EmptyNotInEquivSet: "{} \ calM // RelM" +context sylow +begin + +lemma EmptyNotInEquivSet: "{} \ calM // RelM" by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self]) -lemma (in sylow) existsM1inM: "M \ calM // RelM ==> \M1. M1 \ M" -apply (subgoal_tac "M \ {}") - apply blast -apply (cut_tac EmptyNotInEquivSet, blast) -done +lemma existsM1inM: "M \ calM // RelM ==> \M1. M1 \ M" + using RelM_equiv equiv_Eps_in by blast -lemma (in sylow) zero_less_o_G: "0 < order(G)" -apply (unfold order_def) -apply (blast intro: zero_less_card_empty) -done +lemma zero_less_o_G: "0 < order(G)" + by (simp add: order_def card_gt_0_iff carrier_not_empty) -lemma (in sylow) zero_less_m: "m > 0" -apply (cut_tac zero_less_o_G) -apply (simp add: order_G) -done +lemma zero_less_m: "m > 0" + using zero_less_o_G by (simp add: order_G) -lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a" +lemma card_calM: "card(calM) = (p^a) * m choose p^a" by (simp add: calM_def n_subsets order_G [symmetric] order_def) -lemma (in sylow) zero_less_card_calM: "card calM > 0" +lemma zero_less_card_calM: "card calM > 0" by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m) -lemma (in sylow) max_p_div_calM: +lemma max_p_div_calM: "~ (p ^ Suc(exponent p m) dvd card(calM))" -apply (subgoal_tac "exponent p m = exponent p (card calM) ") - apply (cut_tac zero_less_card_calM prime_p) - apply (force dest: power_Suc_exponent_Not_dvd) -apply (simp add: card_calM zero_less_m [THEN const_p_fac]) -done +proof - + have "exponent p m = exponent p (card calM)" + by (simp add: card_calM const_p_fac zero_less_m) + then show ?thesis + by (metis Suc_n_not_le_n exponent_ge prime_p zero_less_card_calM) +qed -lemma (in sylow) finite_calM: "finite calM" -apply (unfold calM_def) -apply (rule_tac B = "Pow (carrier G) " in finite_subset) -apply auto -done +lemma finite_calM: "finite calM" + unfolding calM_def + by (rule_tac B = "Pow (carrier G) " in finite_subset) auto -lemma (in sylow) lemma_A1: +lemma lemma_A1: "\M \ calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))" -apply (rule max_p_div_calM [THEN contrapos_np]) -apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv]) -done + using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast +end subsubsection\Introduction and Destruct Rules for @{term H}\ @@ -196,11 +187,7 @@ by (rule finite_subset [OF M1_subset_G finite_G]) lemma (in sylow_central) finite_rcosetGM1g: "g\carrier G ==> finite (M1 #> g)" -apply (rule finite_subset) -apply (rule subsetI) -apply (erule rcosetGM1g_subset_G, assumption) -apply (rule finite_G) -done + using rcosetGM1g_subset_G finite_G M1_subset_G cosets_finite rcosetsI by blast lemma (in sylow_central) M1_cardeq_rcosetGM1g: "g \ carrier G ==> card(M1 #> g) = card(M1)" @@ -242,7 +229,7 @@ "(%x:M. H #> (SOME g. g \ carrier G & M1 #> g = x)) \ M \ rcosets H" by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset) -lemma (in sylow_central) inj_M_GmodH: "\f \ M\rcosets H. inj_on f M" +lemma (in sylow_central) inj_M_GmodH: "\f \ M \ rcosets H. inj_on f M" apply (rule bexI) apply (rule_tac [2] M_funcset_rcosets_H) apply (rule inj_onI, simp) diff -r 2497c966ba2b -r 8c47e7fcdb8d src/HOL/Library/Convex.thy --- a/src/HOL/Library/Convex.thy Thu Feb 25 16:54:24 2016 +0100 +++ b/src/HOL/Library/Convex.thy Fri Feb 26 11:57:36 2016 +0100 @@ -323,9 +323,9 @@ shows "convex_on A f" proof fix t x y assume A: "x \ A" "y \ A" "(t::real) > 0" "t < 1" - case (goal1 t x y) - with goal1 assms[of t x y] assms[of "1 - t" y x] - show ?case by (cases x y rule: linorder_cases) (auto simp: algebra_simps) + with assms[of t x y] assms[of "1 - t" y x] + show "f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y" + by (cases x y rule: linorder_cases) (auto simp: algebra_simps) qed lemma convex_onD: diff -r 2497c966ba2b -r 8c47e7fcdb8d src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Thu Feb 25 16:54:24 2016 +0100 +++ b/src/HOL/Number_Theory/Primes.thy Fri Feb 26 11:57:36 2016 +0100 @@ -40,9 +40,7 @@ subsection \Primes\ lemma prime_odd_nat: "prime p \ p > 2 \ odd p" - apply (auto simp add: prime_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0) - apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral) - done + using nat_dvd_1_iff_1 odd_one prime_def by blast lemma prime_gt_0_nat: "prime p \ p > 0" unfolding prime_def by auto