--- 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. *}
-primrec compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
+primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
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
case (Load adr)
- 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 @@
case (Variable adr s)
have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
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
+ also have "env adr = eval (Variable adr) env"
+ 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)"
by (simp add: execute_def)
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))"
by (rule gcd_add2_nat)
- also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
+ also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
by (simp add: gcd_commute_nat)
- 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)"
by (simp add: gcd_non_0_nat add_commute)
- also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat)
+ also from `0 < n` have "\<dots> = gcd m n"
+ by (simp add: gcd_non_0_nat)
finally show ?thesis .
qed
@@ -106,22 +109,23 @@
also have "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
- 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))"
by (simp add: gcd_mult_add)
- 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))"
by (simp add: gcd_fib_add)
- 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)"
+ by (simp add: gcd_non_0_nat)
+ 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)"
by (simp add: distrib)
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)"
+ by (simp add: distrib)
+ 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"
by (simp add: power_eq_if distrib)
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)"
by (simp add: power_eq_if distrib)
- 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