# HG changeset patch
# User wenzelm
# Date 1461663499 -7200
# Node ID 1b237d147cc4c4982a26d142004d33388c43b85f
# Parent  2cc4e85b46d450dcb8032c37eb1e0f8eee3d4090
misc tuning and modernization;

diff -r 2cc4e85b46d4 -r 1b237d147cc4 src/HOL/ex/Abstract_NAT.thy
--- 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)
diff -r 2cc4e85b46d4 -r 1b237d147cc4 src/HOL/ex/CTL.thy
--- 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)
diff -r 2cc4e85b46d4 -r 1b237d147cc4 src/HOL/ex/Cartouche_Examples.thy
--- 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"
diff -r 2cc4e85b46d4 -r 1b237d147cc4 src/HOL/ex/Coherent.thy
--- 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
 
diff -r 2cc4e85b46d4 -r 1b237d147cc4 src/HOL/ex/Cubic_Quartic.thy
--- 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