summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 20 Feb 2014 23:46:40 +0100 | |

changeset 55640 | abc140f21caa |

parent 55639 | e4e8cbd9d780 |

child 55641 | 5b466efedd2c |

tuned proofs;
more symbols;

--- 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