author wenzelm Thu, 20 Feb 2014 23:46:40 +0100 changeset 55640 abc140f21caa parent 55639 e4e8cbd9d780 child 55641 5b466efedd2c
tuned proofs; more symbols;
 src/HOL/Isar_Examples/Basic_Logic.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Cantor.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Expr_Compiler.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Fibonacci.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Peirce.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Summation.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -18,33 +18,33 @@
@{text K}, and @{text S}.  The following (rather explicit) proofs
should require little extra explanations. *}

-lemma I: "A --> A"
+lemma I: "A \<longrightarrow> A"
proof
assume A
show A by fact
qed

-lemma K: "A --> B --> A"
+lemma K: "A \<longrightarrow> B \<longrightarrow> A"
proof
assume A
-  show "B --> A"
+  show "B \<longrightarrow> A"
proof
show A by fact
qed
qed

-lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
+lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
proof
-  assume "A --> B --> C"
-  show "(A --> B) --> A --> C"
+  assume "A \<longrightarrow> B \<longrightarrow> C"
+  show "(A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
proof
-    assume "A --> B"
-    show "A --> C"
+    assume "A \<longrightarrow> B"
+    show "A \<longrightarrow> C"
proof
assume A
show C
proof (rule mp)
-        show "B --> C" by (rule mp) fact+
+        show "B \<longrightarrow> C" by (rule mp) fact+
show B by (rule mp) fact+
qed
qed
@@ -60,7 +60,7 @@
First of all, proof by assumption may be abbreviated as a single
dot. *}

-lemma "A --> A"
+lemma "A \<longrightarrow> A"
proof
assume A
show A by fact+
@@ -72,7 +72,7 @@
higher-order unification.}.  Thus we may skip the rather vacuous
body of the above proof as well. *}

-lemma "A --> A"
+lemma "A \<longrightarrow> A"
proof
qed

@@ -82,12 +82,12 @@
statements involved.  The \isacommand{by} command abbreviates any
proof with empty body, so the proof may be further pruned. *}

-lemma "A --> A"
+lemma "A \<longrightarrow> A"
by rule

text {* Proof by a single rule may be abbreviated as double-dot. *}

-lemma "A --> A" ..
+lemma "A \<longrightarrow> A" ..

text {* Thus we have arrived at an adequate representation of the
proof of a tautology that holds by a single standard
@@ -103,7 +103,7 @@
conclusion.\footnote{The dual method is @{text elim}, acting on a
goal's premises.} *}

-lemma "A --> B --> A"
+lemma "A \<longrightarrow> B \<longrightarrow> A"
proof (intro impI)
assume A
show A by fact
@@ -111,7 +111,7 @@

text {* Again, the body may be collapsed. *}

-lemma "A --> B --> A"
+lemma "A \<longrightarrow> B \<longrightarrow> A"
by (intro impI)

text {* Just like @{text rule}, the @{text intro} and @{text elim}
@@ -140,10 +140,10 @@

The first version is purely backward. *}

-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
-  assume "A & B"
-  show "B & A"
+  assume "A \<and> B"
+  show "B \<and> A"
proof
show B by (rule conjunct2) fact
show A by (rule conjunct1) fact
@@ -158,13 +158,13 @@
\isacommand{from} already does forward-chaining, involving the
@{text conjE} rule here. *}

-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
-  assume "A & B"
-  show "B & A"
+  assume "A \<and> B"
+  show "B \<and> A"
proof
-    from A & B show B ..
-    from A & B show A ..
+    from A \<and> B show B ..
+    from A \<and> B show A ..
qed
qed

@@ -176,10 +176,10 @@
that of the @{text conjE} rule, including the repeated goal
proposition that is abbreviated as @{text ?thesis} below. *}

-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
-  assume "A & B"
-  then show "B & A"
+  assume "A \<and> B"
+  then show "B \<and> A"
proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
assume B A
then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
@@ -190,25 +190,25 @@
body by doing forward reasoning all the time.  Only the outermost
decomposition step is left as backward. *}

-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
-  assume "A & B"
-  from A & B have A ..
-  from A & B have B ..
-  from B A show "B & A" ..
+  assume "A \<and> B"
+  from A \<and> B have A ..
+  from A \<and> B have B ..
+  from B A show "B \<and> A" ..
qed

text {* We can still push forward-reasoning a bit further, even at the
risk of getting ridiculous.  Note that we force the initial proof
step to do nothing here, by referring to the -'' proof method. *}

-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
proof -
{
-    assume "A & B"
-    from A & B have A ..
-    from A & B have B ..
-    from B A have "B & A" ..
+    assume "A \<and> B"
+    from A \<and> B have A ..
+    from A \<and> B have B ..
+    from B A have "B \<and> A" ..
}
then show ?thesis ..         -- {* rule @{text impI} *}
qed
@@ -232,10 +232,10 @@
probably the middle one, with conjunction introduction done after
elimination. *}

-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
-  assume "A & B"
-  then show "B & A"
+  assume "A \<and> B"
+  then show "B \<and> A"
proof
assume B A
then show ?thesis ..
@@ -256,9 +256,9 @@
below involves forward-chaining from @{text "P \<or> P"}, followed by an
explicit case-analysis on the two \emph{identical} cases. *}

-lemma "P | P --> P"
+lemma "P \<or> P \<longrightarrow> P"
proof
-  assume "P | P"
+  assume "P \<or> P"
then show P
proof                    -- {*
rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
@@ -291,9 +291,9 @@
cases actually coincide.  Consequently the proof may be rephrased as
follows. *}

-lemma "P | P --> P"
+lemma "P \<or> P --> P"
proof
-  assume "P | P"
+  assume "P \<or> P"
then show P
proof
assume P
@@ -307,9 +307,9 @@
are implicitly performed when concluding the single rule step of the
double-dot proof as follows. *}

-lemma "P | P --> P"
+lemma "P \<or> P --> P"
proof
-  assume "P | P"
+  assume "P \<or> P"
then show P ..
qed

@@ -328,10 +328,10 @@
arbitrary, but fixed'' element; the \isacommand{is} annotation
binds term abbreviations by higher-order pattern matching. *}

-lemma "(EX x. P (f x)) --> (EX y. P y)"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
+  assume "\<exists>x. P (f x)"
+  then show "\<exists>y. P y"
proof (rule exE)             -- {*
rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
*}
@@ -348,10 +348,10 @@
instances (by higher-order unification).  Thus we may as well prune
the text as follows. *}

-lemma "(EX x. P (f x)) --> (EX y. P y)"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
+  assume "\<exists>x. P (f x)"
+  then show "\<exists>y. P y"
proof
fix a
assume "P (f a)"
@@ -364,11 +364,11 @@
\isakeyword{obtain}'' provides a more handsome way to do
generalized existence reasoning. *}

-lemma "(EX x. P (f x)) --> (EX y. P y)"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
proof
-  assume "EX x. P (f x)"
+  assume "\<exists>x. P (f x)"
then obtain a where "P (f a)" ..
-  then show "EX y. P y" ..
+  then show "\<exists>y. P y" ..
qed

text {* Technically, \isakeyword{obtain} is similar to
@@ -387,10 +387,10 @@
since Isabelle/Isar supports non-atomic goals and assumptions fully
transparently. *}

-theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
+theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
proof -
-  assume "A & B"
-  assume r: "A ==> B ==> C"
+  assume "A \<and> B"
+  assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
show C
proof (rule r)
show A by (rule conjunct1) fact
--- a/src/HOL/Isar_Examples/Cantor.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -24,22 +24,24 @@
with the type $\alpha \ap \idt{set}$ and the operator
$\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}

-theorem "EX S. S ~: range (f :: 'a => 'a set)"
+theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
proof
-  let ?S = "{x. x ~: f x}"
-  show "?S ~: range f"
+  let ?S = "{x. x \<notin> f x}"
+  show "?S \<notin> range f"
proof
-    assume "?S : range f"
+    assume "?S \<in> range f"
then obtain y where "?S = f y" ..
then show False
proof (rule equalityCE)
-      assume "y : f y"
-      assume "y : ?S" then have "y ~: f y" ..
+      assume "y \<in> f y"
+      assume "y \<in> ?S"
+      then have "y \<notin> f y" ..
with y : f y show ?thesis by contradiction
next
-      assume "y ~: ?S"
-      assume "y ~: f y" then have "y : ?S" ..
-      with y ~: ?S show ?thesis by contradiction
+      assume "y \<notin> ?S"
+      assume "y \<notin> f y"
+      then have "y \<in> ?S" ..
+      with y \<notin> ?S show ?thesis by contradiction
qed
qed
qed
@@ -51,7 +53,7 @@
classical prover contains rules for the relevant constructs of HOL's
set theory.  *}

-theorem "EX S. S ~: range (f :: 'a => 'a set)"
+theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
by best

text {* While this establishes the same theorem internally, we do not
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -22,7 +22,7 @@
This is both for abstract syntax and semantics, i.e.\ we use a
shallow embedding'' here. *}

-type_synonym 'val binop = "'val => 'val => 'val"
+type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"

subsection {* Expressions *}
@@ -39,7 +39,7 @@
text {* Evaluation (wrt.\ some environment of variable assignments) is
defined by primitive recursion over the structure of expressions. *}

-primrec eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
+primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
where
"eval (Variable x) env = env x"
| "eval (Constant c) env = c"
@@ -59,17 +59,17 @@
text {* Execution of a list of stack machine instructions is easily
defined as follows. *}

-primrec exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"
+primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
where
"exec [] stack env = stack"
| "exec (instr # instrs) stack env =
(case instr of
-      Const c => exec instrs (c # stack) env
-    | Load x => exec instrs (env x # stack) env
-    | Apply f => exec instrs (f (hd stack) (hd (tl stack))
+      Const c \<Rightarrow> exec instrs (c # stack) env
+    | Load x \<Rightarrow> exec instrs (env x # stack) env
+    | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))
# (tl (tl stack))) env)"

-definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
+definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
where "execute instrs env = hd (exec instrs [] env)"

@@ -78,7 +78,7 @@
text {* We are ready to define the compilation function of expressions
to lists of stack machine instructions. *}

where
"compile (Variable x) = [Load x]"
| "compile (Constant c) = [Const c]"
@@ -114,11 +114,14 @@
proof -
have "\<And>stack. exec (compile e) stack env = eval e env # stack"
proof (induct e)
-    case Variable show ?case by simp
+    case Variable
+    show ?case by simp
next
-    case Constant show ?case by simp
+    case Constant
+    show ?case by simp
next
-    case Binop then show ?case by (simp add: exec_append)
+    case Binop
+    then show ?case by (simp add: exec_append)
qed
then show ?thesis by (simp add: execute_def)
qed
@@ -134,8 +137,10 @@
"exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
proof (induct xs arbitrary: stack)
case (Nil s)
-  have "exec ([] @ ys) s env = exec ys s env" by simp
-  also have "... = exec ys (exec [] s env) env" by simp
+  have "exec ([] @ ys) s env = exec ys s env"
+    by simp
+  also have "\<dots> = exec ys (exec [] s env) env"
+    by simp
finally show ?case .
next
case (Cons x xs s)
@@ -144,22 +149,27 @@
case (Const val)
have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
by simp
-    also have "... = exec (xs @ ys) (val # s) env" by simp
-    also from Cons have "... = exec ys (exec xs (val # s) env) env" .
-    also have "... = exec ys (exec (Const val # xs) s env) env" by simp
+    also have "\<dots> = exec (xs @ ys) (val # s) env"
+      by simp
+    also from Cons have "\<dots> = exec ys (exec xs (val # s) env) env" .
+    also have "\<dots> = exec ys (exec (Const val # xs) s env) env"
+      by simp
finally show ?case .
next
-    from Cons show ?case by simp -- {* same as above *}
+    from Cons show ?case
+      by simp -- {* same as above *}
next
case (Apply fn)
have "exec ((Apply fn # xs) @ ys) s env =
exec (Apply fn # xs @ ys) s env" by simp
-    also have "... =
-        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
-    also from Cons have "... =
+    also have "\<dots> =
+        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env"
+      by simp
+    also from Cons have "\<dots> =
exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
-    also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
+    also have "\<dots> = exec ys (exec (Apply fn # xs) s env) env"
+      by simp
finally show ?case .
qed
qed
@@ -171,8 +181,10 @@
by simp
-    also have "... = env adr # s" by simp
-    also have "env adr = eval (Variable adr) env" by simp
+    also have "\<dots> = env adr # s"
+      by simp
+      by simp
finally show ?case .
next
case (Constant val s)
@@ -180,15 +192,20 @@
next
case (Binop fn e1 e2 s)
have "exec (compile (Binop fn e1 e2)) s env =
-        exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
-    also have "... = exec [Apply fn]
+        exec (compile e2 @ compile e1 @ [Apply fn]) s env"
+      by simp
+    also have "\<dots> = exec [Apply fn]
(exec (compile e1) (exec (compile e2) s env) env) env"
by (simp only: exec_append)
-    also have "exec (compile e2) s env = eval e2 env # s" by fact
-    also have "exec (compile e1) ... env = eval e1 env # ..." by fact
-    also have "exec [Apply fn] ... env =
-        fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
-    also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
+    also have "exec (compile e2) s env = eval e2 env # s"
+      by fact
+    also have "exec (compile e1) \<dots> env = eval e1 env # \<dots>"
+      by fact
+    also have "exec [Apply fn] \<dots> env =
+        fn (hd \<dots>) (hd (tl \<dots>)) # (tl (tl \<dots>))"
+      by simp
+    also have "\<dots> = fn (eval e1 env) (eval e2 env) # s"
+      by simp
also have "fn (eval e1 env) (eval e2 env) =
eval (Binop fn e1 e2) env"
by simp
@@ -198,7 +215,8 @@
have "execute (compile e) env = hd (exec (compile e) [] env)"
also from exec_compile have "exec (compile e) [] env = [eval e env]" .
-  also have "hd ... = eval e env" by simp
+  also have "hd \<dots> = eval e env"
+    by simp
finally show ?thesis .
qed

--- a/src/HOL/Isar_Examples/Fibonacci.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -40,7 +40,8 @@
text {* Alternative induction rule. *}

theorem fib_induct:
-    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
+  fixes n :: nat
+  shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
by (induct rule: fib.induct) simp_all

@@ -77,21 +78,23 @@
fix n
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
by simp
-  also have "... = fib (n + 2) + fib (n + 1)" by simp
-  also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
+  also have "\<dots> = fib (n + 2) + fib (n + 1)"
+    by simp
+  also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
-  also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
+  also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
-  also assume "... = 1"
+  also assume "\<dots> = 1"
finally show "?P (n + 2)" .
qed

-lemma gcd_mult_add: "(0::nat) < n ==> gcd (n * k + m) n = gcd m n"
+lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
proof -
assume "0 < n"
then have "gcd (n * k + m) n = gcd n (m mod n)"
-  also from 0 < n have "... = gcd m n" by (simp add: gcd_non_0_nat)
+  also from 0 < n have "\<dots> = gcd m n"
finally show ?thesis .
qed

@@ -106,22 +109,23 @@
also have "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
-  also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
+  also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
-  also have "... = gcd (fib n) (fib (k + 1))"
+  also have "\<dots> = gcd (fib n) (fib (k + 1))"
by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
-  also have "... = gcd (fib m) (fib n)"
+  also have "\<dots> = gcd (fib m) (fib n)"
using Suc by (simp add: gcd_commute_nat)
finally show ?thesis .
qed

lemma gcd_fib_diff:
-  assumes "m <= n"
+  assumes "m \<le> n"
shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
proof -
have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
-  also from m <= n have "n - m + m = n" by simp
+  also from m \<le> n have "n - m + m = n"
+    by simp
finally show ?thesis .
qed

@@ -134,15 +138,18 @@
proof -
have "n mod m = (if n < m then n else (n - m) mod m)"
by (rule mod_if)
-    also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
+    also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
proof (cases "n < m")
-      case True then show ?thesis by simp
+      case True
+      then show ?thesis by simp
next
-      case False then have "m <= n" by simp
-      from 0 < m and False have "n - m < n" by simp
+      case False
+      then have "m \<le> n" by simp
+      from 0 < m and False have "n - m < n"
+        by simp
with hyp have "gcd (fib m) (fib ((n - m) mod m))
= gcd (fib m) (fib (n - m))" by simp
-      also have "... = gcd (fib m) (fib n)"
+      also have "\<dots> = gcd (fib m) (fib n)"
using m <= n by (rule gcd_fib_diff)
finally have "gcd (fib m) (fib ((n - m) mod m)) =
gcd (fib m) (fib n)" .
@@ -154,12 +161,18 @@

theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
proof (induct m n rule: gcd_nat_induct)
-  fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
-  fix n :: nat assume n: "0 < n"
-  then have "gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat)
-  also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
-  also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
-  also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat)
+  fix m
+  show "fib (gcd m 0) = gcd (fib m) (fib 0)"
+    by simp
+  fix n :: nat
+  assume n: "0 < n"
+  then have "gcd m n = gcd n (m mod n)"
+  also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
+  also from n have "\<dots> = gcd (fib n) (fib m)"
+    by (rule gcd_fib_mod)
+  also have "\<dots> = gcd (fib m) (fib n)"
+    by (rule gcd_commute_nat)
finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
qed

--- a/src/HOL/Isar_Examples/Peirce.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Peirce.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -19,18 +19,18 @@
there is negation elimination; it holds in intuitionistic logic as
well.} *}

-theorem "((A --> B) --> A) --> A"
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
-  assume "(A --> B) --> A"
+  assume "(A \<longrightarrow> B) \<longrightarrow> A"
show A
proof (rule classical)
-    assume "~ A"
-    have "A --> B"
+    assume "\<not> A"
+    have "A \<longrightarrow> B"
proof
assume A
-      with ~ A show B by contradiction
+      with \<not> A show B by contradiction
qed
-    with (A --> B) --> A show A ..
+    with (A \<longrightarrow> B) \<longrightarrow> A show A ..
qed
qed

@@ -48,19 +48,19 @@
contrast, strong assumptions (as introduced by \isacommand{assume})
are solved immediately. *}

-theorem "((A --> B) --> A) --> A"
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
-  assume "(A --> B) --> A"
+  assume "(A \<longrightarrow> B) \<longrightarrow> A"
show A
proof (rule classical)
-    presume "A --> B"
-    with (A --> B) --> A show A ..
+    presume "A \<longrightarrow> B"
+    with (A \<longrightarrow> B) \<longrightarrow> A show A ..
next
-    assume "~ A"
-    show "A --> B"
+    assume "\<not> A"
+    show "A \<longrightarrow> B"
proof
assume A
-      with ~ A show B by contradiction
+      with \<not> A show B by contradiction
qed
qed
qed
--- a/src/HOL/Isar_Examples/Summation.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -26,10 +26,13 @@
proof (induct n)
show "?P 0" by simp
next
-  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
+  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)"
+    by simp
also assume "?S n = n * (n + 1)"
-  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
-  finally show "?P (Suc n)" by simp
+  also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)"
+    by simp
+  finally show "?P (Suc n)"
+    by simp
qed

text {* The above proof is a typical instance of mathematical
@@ -80,10 +83,14 @@
proof (induct n)
show "?P 0" by simp
next
-  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
+  fix n
+  have "?S (n + 1) = ?S n + 2 * n + 1"
+    by simp
also assume "?S n = n^Suc (Suc 0)"
-  also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
-  finally show "?P (Suc n)" by simp
+  also have "\<dots> + 2 * n + 1 = (n + 1)^Suc (Suc 0)"
+    by simp
+  finally show "?P (Suc n)"
+    by simp
qed

text {* Subsequently we require some additional tweaking of Isabelle
@@ -98,12 +105,15 @@
proof (induct n)
show "?P 0" by simp
next
-  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
+  fix n
+  have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
also assume "?S n = n * (n + 1) * (2 * n + 1)"
-  also have "... + 6 * (n + 1)^Suc (Suc 0) =
-      (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
-  finally show "?P (Suc n)" by simp
+  also have "\<dots> + 6 * (n + 1)^Suc (Suc 0) =
+      (n + 1) * (n + 2) * (2 * (n + 1) + 1)"
+  finally show "?P (Suc n)"
+    by simp
qed

theorem sum_of_cubes:
@@ -112,12 +122,14 @@
proof (induct n)
show "?P 0" by (simp add: power_eq_if)
next
-  fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
+  fix n
+  have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
-  also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
+  also have "\<dots> + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
-  finally show "?P (Suc n)" by simp
+  finally show "?P (Suc n)"
+    by simp
qed

text {* Note that in contrast to older traditions of tactical proof