--- a/src/HOL/ex/Abstract_NAT.thy Mon Apr 25 22:59:53 2016 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy Tue Apr 26 11:38:19 2016 +0200
@@ -23,13 +23,13 @@
by (rule succ_neq_zero [symmetric])
-text \<open>\medskip Primitive recursion as a (functional) relation -- polymorphic!\<close>
+text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>
inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
where
- Rec_zero: "Rec e r zero e"
- | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
+ Rec_zero: "Rec e r zero e"
+| Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
lemma Rec_functional:
fixes x :: 'n
@@ -42,26 +42,30 @@
show "\<exists>!y. ?R zero y"
proof
show "?R zero e" ..
- fix y assume "?R zero y"
- then show "y = e" by cases simp_all
+ show "y = e" if "?R zero y" for y
+ using that by cases simp_all
qed
next
case (succ m)
from \<open>\<exists>!y. ?R m y\<close>
- obtain y where y: "?R m y"
- and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
+ obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'"
+ by blast
show "\<exists>!z. ?R (succ m) z"
proof
from y show "?R (succ m) (r m y)" ..
- fix z assume "?R (succ m) z"
- then obtain u where "z = r m u" and "?R m u" by cases simp_all
- with yy' show "z = r m y" by (simp only:)
+ next
+ fix z
+ assume "?R (succ m) z"
+ then obtain u where "z = r m u" and "?R m u"
+ by cases simp_all
+ with yy' show "z = r m y"
+ by (simp only:)
qed
qed
qed
-text \<open>\medskip The recursion operator -- polymorphic!\<close>
+text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
where "rec e r x = (THE y. Rec e r x y)"
@@ -86,7 +90,7 @@
qed
-text \<open>\medskip Example: addition (monomorphic)\<close>
+text \<open>\<^medskip> Example: addition (monomorphic)\<close>
definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
where "add m n = rec n (\<lambda>_ k. succ k) m"
@@ -109,7 +113,7 @@
by simp
-text \<open>\medskip Example: replication (polymorphic)\<close>
+text \<open>\<^medskip> Example: replication (polymorphic)\<close>
definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
@@ -124,17 +128,17 @@
end
-text \<open>\medskip Just see that our abstract specification makes sense \dots\<close>
+text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
interpretation NAT 0 Suc
proof (rule NAT.intro)
fix m n
show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
show "Suc m \<noteq> 0" by simp
- fix P
- assume zero: "P 0"
+ show "P n"
+ if zero: "P 0"
and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
- show "P n"
+ for P
proof (induct n)
case 0
show ?case by (rule zero)
--- a/src/HOL/ex/CTL.thy Mon Apr 25 22:59:53 2016 +0200
+++ b/src/HOL/ex/CTL.thy Tue Apr 26 11:38:19 2016 +0200
@@ -25,9 +25,8 @@
type_synonym 'a ctl = "'a set"
-definition
- imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75) where
- "p \<rightarrow> q = - p \<union> q"
+definition imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
+ where "p \<rightarrow> q = - p \<union> q"
lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
@@ -86,8 +85,7 @@
proof
show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
proof
- fix x assume l: "x \<in> lfp f"
- show "x \<in> - gfp (\<lambda>s. - f (- s))"
+ show "x \<in> - gfp (\<lambda>s. - f (- s))" if l: "x \<in> lfp f" for x
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
@@ -100,7 +98,8 @@
qed
show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
proof (rule lfp_greatest)
- fix u assume "f u \<subseteq> u"
+ fix u
+ assume "f u \<subseteq> u"
then have "- u \<subseteq> - f u" by auto
then have "- u \<subseteq> - f (- (- u))" by simp
then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
--- a/src/HOL/ex/Cartouche_Examples.thy Mon Apr 25 22:59:53 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue Apr 26 11:38:19 2016 +0200
@@ -13,14 +13,14 @@
subsection \<open>Regular outer syntax\<close>
-text \<open>Text cartouches may be used in the outer syntax category "text",
- as alternative to the traditional "verbatim" tokens. An example is
+text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>,
+ as alternative to the traditional \<open>verbatim\<close> tokens. An example is
this text block.\<close> \<comment> \<open>The same works for small side-comments.\<close>
notepad
begin
txt \<open>Moreover, cartouches work as additional syntax in the
- "altstring" category, for literal fact references. For example:\<close>
+ \<open>altstring\<close> category, for literal fact references. For example:\<close>
fix x y :: 'a
assume "x = y"
--- a/src/HOL/ex/Coherent.thy Mon Apr 25 22:59:53 2016 +0200
+++ b/src/HOL/ex/Coherent.thy Tue Apr 26 11:38:19 2016 +0200
@@ -16,65 +16,63 @@
relcomp (infixr "O" 75)
lemma p1p2:
- assumes
- "col a b c l \<and> col d e f m"
- "col b f g n \<and> col c e g o"
- "col b d h p \<and> col a e h q"
- "col c d i r \<and> col a f i s"
- "el n o \<Longrightarrow> goal"
- "el p q \<Longrightarrow> goal"
- "el s r \<Longrightarrow> goal"
- "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
- "\<And>A B. pl A B \<Longrightarrow> ep A A"
- "\<And>A B. ep A B \<Longrightarrow> ep B A"
- "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
- "\<And>A B. pl A B \<Longrightarrow> el B B"
- "\<And>A B. el A B \<Longrightarrow> el B A"
- "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
- "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
- "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
- "\<And>A B C D E F G H I J K L M N O P Q.
- col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
- col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
- (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
- "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
- "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+ assumes "col a b c l \<and> col d e f m"
+ and "col b f g n \<and> col c e g o"
+ and "col b d h p \<and> col a e h q"
+ and "col c d i r \<and> col a f i s"
+ and "el n o \<Longrightarrow> goal"
+ and "el p q \<Longrightarrow> goal"
+ and "el s r \<Longrightarrow> goal"
+ and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+ and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+ and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+ and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+ and "\<And>A B. pl A B \<Longrightarrow> el B B"
+ and "\<And>A B. el A B \<Longrightarrow> el B A"
+ and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+ and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+ and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+ and "\<And>A B C D E F G H I J K L M N O P Q.
+ col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
+ col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
+ (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
+ and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
+ and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
shows goal using assms
by coherent
lemma p2p1:
- assumes
- "col a b c l \<and> col d e f m"
- "col b f g n \<and> col c e g o"
- "col b d h p \<and> col a e h q"
- "col c d i r \<and> col a f i s"
- "pl a m \<Longrightarrow> goal"
- "pl b m \<Longrightarrow> goal"
- "pl c m \<Longrightarrow> goal"
- "pl d l \<Longrightarrow> goal"
- "pl e l \<Longrightarrow> goal"
- "pl f l \<Longrightarrow> goal"
- "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
- "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
- "\<And>A B. pl A B \<Longrightarrow> ep A A"
- "\<And>A B. ep A B \<Longrightarrow> ep B A"
- "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
- "\<And>A B. pl A B \<Longrightarrow> el B B"
- "\<And>A B. el A B \<Longrightarrow> el B A"
- "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
- "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
- "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
- "\<And>A B C D E F G H I J K L M N O P Q.
- col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
- col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
- (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
- "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
- "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+ assumes "col a b c l \<and> col d e f m"
+ and "col b f g n \<and> col c e g o"
+ and "col b d h p \<and> col a e h q"
+ and "col c d i r \<and> col a f i s"
+ and "pl a m \<Longrightarrow> goal"
+ and "pl b m \<Longrightarrow> goal"
+ and "pl c m \<Longrightarrow> goal"
+ and "pl d l \<Longrightarrow> goal"
+ and "pl e l \<Longrightarrow> goal"
+ and "pl f l \<Longrightarrow> goal"
+ and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+ and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+ and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+ and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+ and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+ and "\<And>A B. pl A B \<Longrightarrow> el B B"
+ and "\<And>A B. el A B \<Longrightarrow> el B A"
+ and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+ and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+ and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+ and "\<And>A B C D E F G H I J K L M N O P Q.
+ col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
+ col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
+ (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
+ and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
+ and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
shows goal using assms
by coherent
@@ -82,16 +80,15 @@
subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
lemma diamond:
- assumes
- "reflexive_rewrite a b" "reflexive_rewrite a c"
- "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
- "\<And>A. equalish A A"
- "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
- "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
- "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
- "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
- "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
- "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
+ assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
+ and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
+ and "\<And>A. equalish A A"
+ and "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
+ and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
+ and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
+ and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
+ and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
+ and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
shows goal using assms
by coherent
--- a/src/HOL/ex/Cubic_Quartic.thy Mon Apr 25 22:59:53 2016 +0200
+++ b/src/HOL/ex/Cubic_Quartic.thy Tue Apr 26 11:38:19 2016 +0200
@@ -2,144 +2,160 @@
Author: Amine Chaieb
*)
-section "The Cubic and Quartic Root Formulas"
+section \<open>The Cubic and Quartic Root Formulas\<close>
theory Cubic_Quartic
imports Complex_Main
begin
-section "The Cubic Formula"
+section \<open>The Cubic Formula\<close>
definition "ccbrt z = (SOME (w::complex). w^3 = z)"
lemma ccbrt: "(ccbrt z) ^ 3 = z"
-proof-
- from rcis_Ex obtain r a where ra: "z = rcis r a" by blast
+proof -
+ from rcis_Ex obtain r a where ra: "z = rcis r a"
+ by blast
let ?r' = "if r < 0 then - root 3 (-r) else root 3 r"
let ?a' = "a/3"
- have "rcis ?r' ?a' ^ 3 = rcis r a" by (cases "r<0", simp_all add: DeMoivre2)
- hence th: "\<exists>w. w^3 = z" unfolding ra by blast
- from someI_ex[OF th] show ?thesis unfolding ccbrt_def by blast
+ have "rcis ?r' ?a' ^ 3 = rcis r a"
+ by (cases "r < 0") (simp_all add: DeMoivre2)
+ then have *: "\<exists>w. w^3 = z"
+ unfolding ra by blast
+ from someI_ex [OF *] show ?thesis
+ unfolding ccbrt_def by blast
qed
-text "The reduction to a simpler form:"
+
+text \<open>The reduction to a simpler form:\<close>
lemma cubic_reduction:
fixes a :: complex
- assumes H: "a \<noteq> 0 \<and> x = y - b / (3 * a) \<and> p = (3* a * c - b^2) / (9 * a^2) \<and>
- q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
+ assumes
+ "a \<noteq> 0 \<and> x = y - b / (3 * a) \<and> p = (3* a * c - b^2) / (9 * a^2) \<and>
+ q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
shows "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> y^3 + 3 * p * y - 2 * q = 0"
-proof-
- from H have "3*a \<noteq> 0" "9*a^2 \<noteq> 0" "54*a^3 \<noteq> 0" by auto
- hence th: "x = y - b / (3 * a) \<longleftrightarrow> (3*a) * x = (3*a) * y - b"
- "p = (3* a * c - b^2) / (9 * a^2) \<longleftrightarrow> (9 * a^2) * p = (3* a * c - b^2)"
- "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \<longleftrightarrow>
- (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)"
+proof -
+ from assms have "3 * a \<noteq> 0" "9 * a^2 \<noteq> 0" "54 * a^3 \<noteq> 0" by auto
+ then have *:
+ "x = y - b / (3 * a) \<longleftrightarrow> (3*a) * x = (3*a) * y - b"
+ "p = (3* a * c - b^2) / (9 * a^2) \<longleftrightarrow> (9 * a^2) * p = (3* a * c - b^2)"
+ "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \<longleftrightarrow>
+ (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)"
by (simp_all add: field_simps)
- from H[unfolded th] show ?thesis by algebra
+ from assms [unfolded *] show ?thesis
+ by algebra
qed
-text "The solutions of the special form:"
-lemma cubic_basic:
+text \<open>The solutions of the special form:\<close>
+
+lemma cubic_basic:
fixes s :: complex
- assumes H: "s^2 = q^2 + p^3 \<and>
- s1^3 = (if p = 0 then 2 * q else q + s) \<and>
- s2 = -s1 * (1 + i * t) / 2 \<and>
- s3 = -s1 * (1 - i * t) / 2 \<and>
- i^2 + 1 = 0 \<and>
- t^2 = 3"
- shows
+ assumes
+ "s^2 = q^2 + p^3 \<and>
+ s1^3 = (if p = 0 then 2 * q else q + s) \<and>
+ s2 = -s1 * (1 + i * t) / 2 \<and>
+ s3 = -s1 * (1 - i * t) / 2 \<and>
+ i^2 + 1 = 0 \<and>
+ t^2 = 3"
+ shows
"if p = 0
then y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> y = s1 \<or> y = s2 \<or> y = s3
else s1 \<noteq> 0 \<and>
- (y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> (y = s1 - p / s1 \<or> y = s2 - p / s2 \<or> y = s3 - p / s3))"
-proof-
- { assume p0: "p = 0"
- with H have ?thesis by (simp add: field_simps) algebra
- }
- moreover
- { assume p0: "p \<noteq> 0"
- with H have th1: "s1 \<noteq> 0" by (simp add: field_simps) algebra
- from p0 H th1 have th0: "s2 \<noteq> 0" "s3 \<noteq>0"
- by (simp_all add: field_simps) algebra+
- from th1 th0
- have th: "y = s1 - p / s1 \<longleftrightarrow> s1*y = s1^2 - p"
- "y = s2 - p / s2 \<longleftrightarrow> s2*y = s2^2 - p"
- "y = s3 - p / s3 \<longleftrightarrow> s3*y = s3^2 - p"
- by (simp_all add: field_simps power2_eq_square)
- from p0 H have ?thesis unfolding th by (simp add: field_simps) algebra
- }
- ultimately show ?thesis by blast
+ (y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> (y = s1 - p / s1 \<or> y = s2 - p / s2 \<or> y = s3 - p / s3))"
+proof (cases "p = 0")
+ case True
+ with assms show ?thesis
+ by (simp add: field_simps) algebra
+next
+ case False
+ with assms have *: "s1 \<noteq> 0" by (simp add: field_simps) algebra
+ with assms False have "s2 \<noteq> 0" "s3 \<noteq> 0"
+ by (simp_all add: field_simps) algebra+
+ with * have **:
+ "y = s1 - p / s1 \<longleftrightarrow> s1 * y = s1^2 - p"
+ "y = s2 - p / s2 \<longleftrightarrow> s2 * y = s2^2 - p"
+ "y = s3 - p / s3 \<longleftrightarrow> s3 * y = s3^2 - p"
+ by (simp_all add: field_simps power2_eq_square)
+ from assms False show ?thesis
+ unfolding ** by (simp add: field_simps) algebra
qed
-text "Explicit formula for the roots:"
+
+text \<open>Explicit formula for the roots:\<close>
lemma cubic:
assumes a0: "a \<noteq> 0"
- shows "
- let p = (3 * a * c - b^2) / (9 * a^2) ;
+ shows
+ "let
+ p = (3 * a * c - b^2) / (9 * a^2);
q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3);
s = csqrt(q^2 + p^3);
s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s));
s2 = -s1 * (1 + ii * csqrt 3) / 2;
s3 = -s1 * (1 - ii * csqrt 3) / 2
- in if p = 0 then
- a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
- x = s1 - b / (3 * a) \<or>
- x = s2 - b / (3 * a) \<or>
- x = s3 - b / (3 * a)
+ in
+ if p = 0 then
+ a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
+ x = s1 - b / (3 * a) \<or>
+ x = s2 - b / (3 * a) \<or>
+ x = s3 - b / (3 * a)
else
s1 \<noteq> 0 \<and>
- (a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
+ (a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
x = s1 - p / s1 - b / (3 * a) \<or>
x = s2 - p / s2 - b / (3 * a) \<or>
x = s3 - p / s3 - b / (3 * a))"
-proof-
+proof -
let ?p = "(3 * a * c - b^2) / (9 * a^2)"
let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
- let ?s = "csqrt(?q^2 + ?p^3)"
+ let ?s = "csqrt (?q^2 + ?p^3)"
let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)"
let ?s2 = "- ?s1 * (1 + ii * csqrt 3) / 2"
let ?s3 = "- ?s1 * (1 - ii * csqrt 3) / 2"
let ?y = "x + b / (3 * a)"
- from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a*3)\<noteq> 0" by auto
- have eq:"a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> ?y^3 + 3 * ?p * ?y - 2 * ?q = 0"
+ from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a * 3) \<noteq> 0"
+ by auto
+ have eq: "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> ?y^3 + 3 * ?p * ?y - 2 * ?q = 0"
by (rule cubic_reduction) (auto simp add: field_simps zero a0)
have "csqrt 3^2 = 3" by (rule power2_csqrt)
- hence th0: "?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and>
- ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \<and>
- ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and>
- ii^2 + 1 = 0 \<and> csqrt 3^2 = 3"
+ then have th0:
+ "?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and>
+ ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \<and>
+ ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and>
+ ii^2 + 1 = 0 \<and> csqrt 3^2 = 3"
using zero by (simp add: field_simps ccbrt)
from cubic_basic[OF th0, of ?y]
- show ?thesis
+ show ?thesis
apply (simp only: Let_def eq)
using zero apply (simp add: field_simps ccbrt)
using zero
- apply (cases "a * (c * 3) = b^2", simp_all add: field_simps)
+ apply (cases "a * (c * 3) = b^2")
+ apply (simp_all add: field_simps)
done
qed
-section "The Quartic Formula"
+section \<open>The Quartic Formula\<close>
lemma quartic:
- "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \<and>
- R^2 = a^2 / 4 - b + y \<and>
- s^2 = y^2 - 4 * d \<and>
- (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
- else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \<and>
- (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
- else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
+ "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \<and>
+ R^2 = a^2 / 4 - b + y \<and>
+ s^2 = y^2 - 4 * d \<and>
+ (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
+ else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \<and>
+ (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
+ else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
\<Longrightarrow> x^4 + a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
x = -a / 4 + R / 2 + D / 2 \<or>
x = -a / 4 + R / 2 - D / 2 \<or>
x = -a / 4 - R / 2 + E / 2 \<or>
x = -a / 4 - R / 2 - E / 2"
-apply (cases "R=0", simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left)
- apply algebra
-apply algebra
-done
+ apply (cases "R = 0")
+ apply (simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left)
+ apply algebra
+ apply algebra
+ done
end