--- 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.
--- /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
--- 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"
--- 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 \<open>
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]
\<open>#!/usr/bin/env isabelle_scala_script
@@ -89,8 +85,12 @@
Console.println("browser_info = " + options.bool("browser_info"))
Console.println("document = " + options.string("document"))\<close>}
- 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.
\<close>
end
--- 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 \<open>Sylow's Theorem\<close>
-subsection \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
+text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
+
+
+subsection\<open>Prime Theorems\<close>
+
+lemma prime_dvd_cases:
+ assumes pk: "p*k dvd m*n" and p: "prime p"
+ shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> 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 "\<exists>x. k dvd x * n \<and> 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 "\<exists>y. k dvd m*y \<and> 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 "\<exists>a b. a+b = c \<and> p^a dvd m \<and> 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 "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
+ by force
+ next
+ case (2 y)
+ with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
+ by force
+ qed
+qed
+
+lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
+ by arith
+
+lemma prime_power_dvd_cases:
+ "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
+ using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
+
+text\<open>needed in this form to prove Sylow's theorem\<close>
+corollary div_combine: "\<lbrakk>prime p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
+ by (metis add_Suc_right mult.commute prime_power_dvd_cases)
+
+
+subsection\<open>The Exponent Function\<close>
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]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
+ by (simp add: exponent_def)
-text\<open>Prime Theorems\<close>
+lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n"
+ by (induct n) (auto simp: Suc_le_eq le_less_trans)
+
+text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close>
+lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a"
+ by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans)
-lemma prime_iff:
- "prime p \<longleftrightarrow> Suc 0 < p \<and> (\<forall>a b. p dvd a * b \<longrightarrow> p dvd a \<or> 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 \<le> exponent p n"
+proof -
+ have "Suc 0 < p"
+ using \<open>prime p\<close> by (simp add: prime_def)
+ with assms show ?thesis
+ by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound)
+qed
-lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 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:
+ "\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0"
+ by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc)
+lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> 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 |]
- ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>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:
+ "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> 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 \<le> exponent p (a * b)"
+ by (rule exponent_ge) (auto simp: mult_dvd_mono power_add power_exponent_dvd \<open>prime p\<close> 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) \<le> exponent p a + exponent p b" by (blast intro: leI)
+ qed
+qed
+
+lemma not_divides_exponent_0: "~ (p dvd n) \<Longrightarrow> 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
- ==> \<forall>m n. p^c dvd m*n -->
- (\<forall>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\<open>Exponent Theorems\<close>
+subsection\<open>The Main Combinatorial Argument\<close>
-lemma exponent_ge [rule_format]:
- "[|p^k dvd n; prime p; 0<n|] ==> 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 \<noteq> 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 \<le> p ^ a * m" using assms
+ by (meson nat_dvd_not_less dvd_triv_left leI mult_pos_pos order.strict_trans)
+ then have "r \<le> a"
+ by (meson "*" \<open>0 < k\<close> \<open>k < p^a\<close> 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 \<open>k \<le> p ^ a * m\<close> \<open>r \<le> a\<close> * dvd_diffD1 dvd_diff_nat le_imp_power_dvd)
+ qed
+next
+ fix r
+ assume *: "p ^ r dvd p ^ a - k"
+ with assms have "r \<le> 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: \<open>r \<le> a\<close> le_imp_power_dvd)
+ then show ?thesis
+ by (meson assms * dvd_diffD1 dvd_diff_nat le_imp_power_dvd less_imp_le_nat \<open>r \<le> a\<close>)
+ 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]: "\<not> prime p ==> exponent p s = 0"
-by (simp (no_asm_simp) add: exponent_def)
-
+lemma p_not_div_choose_lemma:
+ assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> 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 \<open>k < K\<close>
+ 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 \<in> 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\<open>The lemma above, with two changes of variables\<close>
+lemma p_not_div_choose:
+ assumes "k < K" and "k \<le> n"
+ and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> 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\<open>Main Combinatorial Argument\<close>
-
-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)\<noteq>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)\<noteq>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\<open>Suc rules that we have to delete from the simpset\<close>
-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]:
- "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
- ==> k<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\<open>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.\<close>
- 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:
- "[| k<K; k<=n;
- \<forall>j. 0<j & j<K --> 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 "0<p")
- prefer 2 apply (force dest!: prime_gt_Suc_0_nat)
-apply (subst exponent_p_a_m_k_equation, auto)
-done
-
-lemma const_p_fac:
- "m>0 ==> 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\<open>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}.\<close>
-apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
- a + exponent p m")
- apply (simp add: exponent_mult_add)
-txt\<open>one subgoal left!\<close>
-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 \<le> 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
--- 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\<open>The combinatorial argument is in theory Exponent\<close>
+lemma le_extend_mult:
+ fixes c::nat shows "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> 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 \<subseteq> carrier(G) & card(s) = p^a}"
and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
(\<exists>g \<in> 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 \<in> calM"
@@ -35,19 +40,20 @@
thus "\<exists>g'\<in>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' \<in> calM // RelM ==> M' \<subseteq> calM"
+lemma M_subset_calM_prep: "M' \<in> calM // RelM ==> M' \<subseteq> calM"
apply (unfold RelM_def)
apply (blast elim!: quotientE)
done
+end
subsection\<open>Main Part of the Proof\<close>
@@ -58,102 +64,87 @@
and M1_in_M: "M1 \<in> M"
defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
-lemma (in sylow_central) M_subset_calM: "M \<subseteq> 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 \<subseteq> calM"
+ by (rule M_in_quot [THEN M_subset_calM_prep])
-lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
-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: "\<exists>x. x \<in> 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: "\<exists>x. x\<in>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 \<subseteq> 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 \<subseteq> 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: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
- proof -
- from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
- have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
- show ?thesis
- proof
- show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
- by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
- show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
- proof (rule restrictI)
- fix z assume zH: "z \<in> H"
- show "m1 \<otimes> z \<in> M1"
- proof -
- from zH
- have zG: "z \<in> 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: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
+proof -
+ from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
+ have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
+ show ?thesis
+ proof
+ show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
+ by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
+ show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
+ proof (rule restrictI)
+ fix z assume zH: "z \<in> H"
+ show "m1 \<otimes> z \<in> M1"
+ proof -
+ from zH
+ have zG: "z \<in> 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\<open>Discharging the Assumptions of @{text sylow_central}\<close>
-lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
+context sylow
+begin
+
+lemma EmptyNotInEquivSet: "{} \<notin> calM // RelM"
by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
-lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
-apply (subgoal_tac "M \<noteq> {}")
- apply blast
-apply (cut_tac EmptyNotInEquivSet, blast)
-done
+lemma existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> 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:
"\<exists>M \<in> 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\<open>Introduction and Destruct Rules for @{term H}\<close>
@@ -196,11 +187,7 @@
by (rule finite_subset [OF M1_subset_G finite_G])
lemma (in sylow_central) finite_rcosetGM1g: "g\<in>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 \<in> carrier G ==> card(M1 #> g) = card(M1)"
@@ -242,7 +229,7 @@
"(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset)
-lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M"
+lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
apply (rule bexI)
apply (rule_tac [2] M_funcset_rcosets_H)
apply (rule inj_onI, simp)
--- 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 \<in> A" "y \<in> 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) \<le> (1 - t) * f x + t * f y"
+ by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
qed
lemma convex_onD:
--- 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 \<open>Primes\<close>
lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> 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 \<Longrightarrow> p > 0"
unfolding prime_def by auto