1.1 --- a/src/HOL/Isar_Examples/Basic_Logic.thy Thu Feb 20 23:16:33 2014 +0100
1.2 +++ b/src/HOL/Isar_Examples/Basic_Logic.thy Thu Feb 20 23:46:40 2014 +0100
1.3 @@ -18,33 +18,33 @@
1.4 @{text K}, and @{text S}. The following (rather explicit) proofs
1.5 should require little extra explanations. *}
1.6
1.7 -lemma I: "A --> A"
1.8 +lemma I: "A \<longrightarrow> A"
1.9 proof
1.10 assume A
1.11 show A by fact
1.12 qed
1.13
1.14 -lemma K: "A --> B --> A"
1.15 +lemma K: "A \<longrightarrow> B \<longrightarrow> A"
1.16 proof
1.17 assume A
1.18 - show "B --> A"
1.19 + show "B \<longrightarrow> A"
1.20 proof
1.21 show A by fact
1.22 qed
1.23 qed
1.24
1.25 -lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
1.26 +lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
1.27 proof
1.28 - assume "A --> B --> C"
1.29 - show "(A --> B) --> A --> C"
1.30 + assume "A \<longrightarrow> B \<longrightarrow> C"
1.31 + show "(A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
1.32 proof
1.33 - assume "A --> B"
1.34 - show "A --> C"
1.35 + assume "A \<longrightarrow> B"
1.36 + show "A \<longrightarrow> C"
1.37 proof
1.38 assume A
1.39 show C
1.40 proof (rule mp)
1.41 - show "B --> C" by (rule mp) fact+
1.42 + show "B \<longrightarrow> C" by (rule mp) fact+
1.43 show B by (rule mp) fact+
1.44 qed
1.45 qed
1.46 @@ -60,7 +60,7 @@
1.47 First of all, proof by assumption may be abbreviated as a single
1.48 dot. *}
1.49
1.50 -lemma "A --> A"
1.51 +lemma "A \<longrightarrow> A"
1.52 proof
1.53 assume A
1.54 show A by fact+
1.55 @@ -72,7 +72,7 @@
1.56 higher-order unification.}. Thus we may skip the rather vacuous
1.57 body of the above proof as well. *}
1.58
1.59 -lemma "A --> A"
1.60 +lemma "A \<longrightarrow> A"
1.61 proof
1.62 qed
1.63
1.64 @@ -82,12 +82,12 @@
1.65 statements involved. The \isacommand{by} command abbreviates any
1.66 proof with empty body, so the proof may be further pruned. *}
1.67
1.68 -lemma "A --> A"
1.69 +lemma "A \<longrightarrow> A"
1.70 by rule
1.71
1.72 text {* Proof by a single rule may be abbreviated as double-dot. *}
1.73
1.74 -lemma "A --> A" ..
1.75 +lemma "A \<longrightarrow> A" ..
1.76
1.77 text {* Thus we have arrived at an adequate representation of the
1.78 proof of a tautology that holds by a single standard
1.79 @@ -103,7 +103,7 @@
1.80 conclusion.\footnote{The dual method is @{text elim}, acting on a
1.81 goal's premises.} *}
1.82
1.83 -lemma "A --> B --> A"
1.84 +lemma "A \<longrightarrow> B \<longrightarrow> A"
1.85 proof (intro impI)
1.86 assume A
1.87 show A by fact
1.88 @@ -111,7 +111,7 @@
1.89
1.90 text {* Again, the body may be collapsed. *}
1.91
1.92 -lemma "A --> B --> A"
1.93 +lemma "A \<longrightarrow> B \<longrightarrow> A"
1.94 by (intro impI)
1.95
1.96 text {* Just like @{text rule}, the @{text intro} and @{text elim}
1.97 @@ -140,10 +140,10 @@
1.98
1.99 The first version is purely backward. *}
1.100
1.101 -lemma "A & B --> B & A"
1.102 +lemma "A \<and> B \<longrightarrow> B \<and> A"
1.103 proof
1.104 - assume "A & B"
1.105 - show "B & A"
1.106 + assume "A \<and> B"
1.107 + show "B \<and> A"
1.108 proof
1.109 show B by (rule conjunct2) fact
1.110 show A by (rule conjunct1) fact
1.111 @@ -158,13 +158,13 @@
1.112 \isacommand{from} already does forward-chaining, involving the
1.113 @{text conjE} rule here. *}
1.114
1.115 -lemma "A & B --> B & A"
1.116 +lemma "A \<and> B \<longrightarrow> B \<and> A"
1.117 proof
1.118 - assume "A & B"
1.119 - show "B & A"
1.120 + assume "A \<and> B"
1.121 + show "B \<and> A"
1.122 proof
1.123 - from `A & B` show B ..
1.124 - from `A & B` show A ..
1.125 + from `A \<and> B` show B ..
1.126 + from `A \<and> B` show A ..
1.127 qed
1.128 qed
1.129
1.130 @@ -176,10 +176,10 @@
1.131 that of the @{text conjE} rule, including the repeated goal
1.132 proposition that is abbreviated as @{text ?thesis} below. *}
1.133
1.134 -lemma "A & B --> B & A"
1.135 +lemma "A \<and> B \<longrightarrow> B \<and> A"
1.136 proof
1.137 - assume "A & B"
1.138 - then show "B & A"
1.139 + assume "A \<and> B"
1.140 + then show "B \<and> A"
1.141 proof -- {* rule @{text conjE} of @{text "A \<and> B"} *}
1.142 assume B A
1.143 then show ?thesis .. -- {* rule @{text conjI} of @{text "B \<and> A"} *}
1.144 @@ -190,25 +190,25 @@
1.145 body by doing forward reasoning all the time. Only the outermost
1.146 decomposition step is left as backward. *}
1.147
1.148 -lemma "A & B --> B & A"
1.149 +lemma "A \<and> B \<longrightarrow> B \<and> A"
1.150 proof
1.151 - assume "A & B"
1.152 - from `A & B` have A ..
1.153 - from `A & B` have B ..
1.154 - from `B` `A` show "B & A" ..
1.155 + assume "A \<and> B"
1.156 + from `A \<and> B` have A ..
1.157 + from `A \<and> B` have B ..
1.158 + from `B` `A` show "B \<and> A" ..
1.159 qed
1.160
1.161 text {* We can still push forward-reasoning a bit further, even at the
1.162 risk of getting ridiculous. Note that we force the initial proof
1.163 step to do nothing here, by referring to the ``-'' proof method. *}
1.164
1.165 -lemma "A & B --> B & A"
1.166 +lemma "A \<and> B \<longrightarrow> B \<and> A"
1.167 proof -
1.168 {
1.169 - assume "A & B"
1.170 - from `A & B` have A ..
1.171 - from `A & B` have B ..
1.172 - from `B` `A` have "B & A" ..
1.173 + assume "A \<and> B"
1.174 + from `A \<and> B` have A ..
1.175 + from `A \<and> B` have B ..
1.176 + from `B` `A` have "B \<and> A" ..
1.177 }
1.178 then show ?thesis .. -- {* rule @{text impI} *}
1.179 qed
1.180 @@ -232,10 +232,10 @@
1.181 probably the middle one, with conjunction introduction done after
1.182 elimination. *}
1.183
1.184 -lemma "A & B --> B & A"
1.185 +lemma "A \<and> B \<longrightarrow> B \<and> A"
1.186 proof
1.187 - assume "A & B"
1.188 - then show "B & A"
1.189 + assume "A \<and> B"
1.190 + then show "B \<and> A"
1.191 proof
1.192 assume B A
1.193 then show ?thesis ..
1.194 @@ -256,9 +256,9 @@
1.195 below involves forward-chaining from @{text "P \<or> P"}, followed by an
1.196 explicit case-analysis on the two \emph{identical} cases. *}
1.197
1.198 -lemma "P | P --> P"
1.199 +lemma "P \<or> P \<longrightarrow> P"
1.200 proof
1.201 - assume "P | P"
1.202 + assume "P \<or> P"
1.203 then show P
1.204 proof -- {*
1.205 rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
1.206 @@ -291,9 +291,9 @@
1.207 cases actually coincide. Consequently the proof may be rephrased as
1.208 follows. *}
1.209
1.210 -lemma "P | P --> P"
1.211 +lemma "P \<or> P --> P"
1.212 proof
1.213 - assume "P | P"
1.214 + assume "P \<or> P"
1.215 then show P
1.216 proof
1.217 assume P
1.218 @@ -307,9 +307,9 @@
1.219 are implicitly performed when concluding the single rule step of the
1.220 double-dot proof as follows. *}
1.221
1.222 -lemma "P | P --> P"
1.223 +lemma "P \<or> P --> P"
1.224 proof
1.225 - assume "P | P"
1.226 + assume "P \<or> P"
1.227 then show P ..
1.228 qed
1.229
1.230 @@ -328,10 +328,10 @@
1.231 ``arbitrary, but fixed'' element; the \isacommand{is} annotation
1.232 binds term abbreviations by higher-order pattern matching. *}
1.233
1.234 -lemma "(EX x. P (f x)) --> (EX y. P y)"
1.235 +lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
1.236 proof
1.237 - assume "EX x. P (f x)"
1.238 - then show "EX y. P y"
1.239 + assume "\<exists>x. P (f x)"
1.240 + then show "\<exists>y. P y"
1.241 proof (rule exE) -- {*
1.242 rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
1.243 *}
1.244 @@ -348,10 +348,10 @@
1.245 instances (by higher-order unification). Thus we may as well prune
1.246 the text as follows. *}
1.247
1.248 -lemma "(EX x. P (f x)) --> (EX y. P y)"
1.249 +lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
1.250 proof
1.251 - assume "EX x. P (f x)"
1.252 - then show "EX y. P y"
1.253 + assume "\<exists>x. P (f x)"
1.254 + then show "\<exists>y. P y"
1.255 proof
1.256 fix a
1.257 assume "P (f a)"
1.258 @@ -364,11 +364,11 @@
1.259 ``\isakeyword{obtain}'' provides a more handsome way to do
1.260 generalized existence reasoning. *}
1.261
1.262 -lemma "(EX x. P (f x)) --> (EX y. P y)"
1.263 +lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
1.264 proof
1.265 - assume "EX x. P (f x)"
1.266 + assume "\<exists>x. P (f x)"
1.267 then obtain a where "P (f a)" ..
1.268 - then show "EX y. P y" ..
1.269 + then show "\<exists>y. P y" ..
1.270 qed
1.271
1.272 text {* Technically, \isakeyword{obtain} is similar to
1.273 @@ -387,10 +387,10 @@
1.274 since Isabelle/Isar supports non-atomic goals and assumptions fully
1.275 transparently. *}
1.276
1.277 -theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
1.278 +theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
1.279 proof -
1.280 - assume "A & B"
1.281 - assume r: "A ==> B ==> C"
1.282 + assume "A \<and> B"
1.283 + assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
1.284 show C
1.285 proof (rule r)
1.286 show A by (rule conjunct1) fact
2.1 --- a/src/HOL/Isar_Examples/Cantor.thy Thu Feb 20 23:16:33 2014 +0100
2.2 +++ b/src/HOL/Isar_Examples/Cantor.thy Thu Feb 20 23:46:40 2014 +0100
2.3 @@ -24,22 +24,24 @@
2.4 with the type $\alpha \ap \idt{set}$ and the operator
2.5 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}
2.6
2.7 -theorem "EX S. S ~: range (f :: 'a => 'a set)"
2.8 +theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
2.9 proof
2.10 - let ?S = "{x. x ~: f x}"
2.11 - show "?S ~: range f"
2.12 + let ?S = "{x. x \<notin> f x}"
2.13 + show "?S \<notin> range f"
2.14 proof
2.15 - assume "?S : range f"
2.16 + assume "?S \<in> range f"
2.17 then obtain y where "?S = f y" ..
2.18 then show False
2.19 proof (rule equalityCE)
2.20 - assume "y : f y"
2.21 - assume "y : ?S" then have "y ~: f y" ..
2.22 + assume "y \<in> f y"
2.23 + assume "y \<in> ?S"
2.24 + then have "y \<notin> f y" ..
2.25 with `y : f y` show ?thesis by contradiction
2.26 next
2.27 - assume "y ~: ?S"
2.28 - assume "y ~: f y" then have "y : ?S" ..
2.29 - with `y ~: ?S` show ?thesis by contradiction
2.30 + assume "y \<notin> ?S"
2.31 + assume "y \<notin> f y"
2.32 + then have "y \<in> ?S" ..
2.33 + with `y \<notin> ?S` show ?thesis by contradiction
2.34 qed
2.35 qed
2.36 qed
2.37 @@ -51,7 +53,7 @@
2.38 classical prover contains rules for the relevant constructs of HOL's
2.39 set theory. *}
2.40
2.41 -theorem "EX S. S ~: range (f :: 'a => 'a set)"
2.42 +theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
2.43 by best
2.44
2.45 text {* While this establishes the same theorem internally, we do not
3.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy Thu Feb 20 23:16:33 2014 +0100
3.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Thu Feb 20 23:46:40 2014 +0100
3.3 @@ -22,7 +22,7 @@
3.4 This is both for abstract syntax and semantics, i.e.\ we use a
3.5 ``shallow embedding'' here. *}
3.6
3.7 -type_synonym 'val binop = "'val => 'val => 'val"
3.8 +type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
3.9
3.10
3.11 subsection {* Expressions *}
3.12 @@ -39,7 +39,7 @@
3.13 text {* Evaluation (wrt.\ some environment of variable assignments) is
3.14 defined by primitive recursion over the structure of expressions. *}
3.15
3.16 -primrec eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
3.17 +primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
3.18 where
3.19 "eval (Variable x) env = env x"
3.20 | "eval (Constant c) env = c"
3.21 @@ -59,17 +59,17 @@
3.22 text {* Execution of a list of stack machine instructions is easily
3.23 defined as follows. *}
3.24
3.25 -primrec exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"
3.26 +primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
3.27 where
3.28 "exec [] stack env = stack"
3.29 | "exec (instr # instrs) stack env =
3.30 (case instr of
3.31 - Const c => exec instrs (c # stack) env
3.32 - | Load x => exec instrs (env x # stack) env
3.33 - | Apply f => exec instrs (f (hd stack) (hd (tl stack))
3.34 + Const c \<Rightarrow> exec instrs (c # stack) env
3.35 + | Load x \<Rightarrow> exec instrs (env x # stack) env
3.36 + | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))
3.37 # (tl (tl stack))) env)"
3.38
3.39 -definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
3.40 +definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
3.41 where "execute instrs env = hd (exec instrs [] env)"
3.42
3.43
3.44 @@ -78,7 +78,7 @@
3.45 text {* We are ready to define the compilation function of expressions
3.46 to lists of stack machine instructions. *}
3.47
3.48 -primrec compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
3.49 +primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
3.50 where
3.51 "compile (Variable x) = [Load x]"
3.52 | "compile (Constant c) = [Const c]"
3.53 @@ -114,11 +114,14 @@
3.54 proof -
3.55 have "\<And>stack. exec (compile e) stack env = eval e env # stack"
3.56 proof (induct e)
3.57 - case Variable show ?case by simp
3.58 + case Variable
3.59 + show ?case by simp
3.60 next
3.61 - case Constant show ?case by simp
3.62 + case Constant
3.63 + show ?case by simp
3.64 next
3.65 - case Binop then show ?case by (simp add: exec_append)
3.66 + case Binop
3.67 + then show ?case by (simp add: exec_append)
3.68 qed
3.69 then show ?thesis by (simp add: execute_def)
3.70 qed
3.71 @@ -134,8 +137,10 @@
3.72 "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
3.73 proof (induct xs arbitrary: stack)
3.74 case (Nil s)
3.75 - have "exec ([] @ ys) s env = exec ys s env" by simp
3.76 - also have "... = exec ys (exec [] s env) env" by simp
3.77 + have "exec ([] @ ys) s env = exec ys s env"
3.78 + by simp
3.79 + also have "\<dots> = exec ys (exec [] s env) env"
3.80 + by simp
3.81 finally show ?case .
3.82 next
3.83 case (Cons x xs s)
3.84 @@ -144,22 +149,27 @@
3.85 case (Const val)
3.86 have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
3.87 by simp
3.88 - also have "... = exec (xs @ ys) (val # s) env" by simp
3.89 - also from Cons have "... = exec ys (exec xs (val # s) env) env" .
3.90 - also have "... = exec ys (exec (Const val # xs) s env) env" by simp
3.91 + also have "\<dots> = exec (xs @ ys) (val # s) env"
3.92 + by simp
3.93 + also from Cons have "\<dots> = exec ys (exec xs (val # s) env) env" .
3.94 + also have "\<dots> = exec ys (exec (Const val # xs) s env) env"
3.95 + by simp
3.96 finally show ?case .
3.97 next
3.98 case (Load adr)
3.99 - from Cons show ?case by simp -- {* same as above *}
3.100 + from Cons show ?case
3.101 + by simp -- {* same as above *}
3.102 next
3.103 case (Apply fn)
3.104 have "exec ((Apply fn # xs) @ ys) s env =
3.105 exec (Apply fn # xs @ ys) s env" by simp
3.106 - also have "... =
3.107 - exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
3.108 - also from Cons have "... =
3.109 + also have "\<dots> =
3.110 + exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env"
3.111 + by simp
3.112 + also from Cons have "\<dots> =
3.113 exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
3.114 - also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
3.115 + also have "\<dots> = exec ys (exec (Apply fn # xs) s env) env"
3.116 + by simp
3.117 finally show ?case .
3.118 qed
3.119 qed
3.120 @@ -171,8 +181,10 @@
3.121 case (Variable adr s)
3.122 have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
3.123 by simp
3.124 - also have "... = env adr # s" by simp
3.125 - also have "env adr = eval (Variable adr) env" by simp
3.126 + also have "\<dots> = env adr # s"
3.127 + by simp
3.128 + also have "env adr = eval (Variable adr) env"
3.129 + by simp
3.130 finally show ?case .
3.131 next
3.132 case (Constant val s)
3.133 @@ -180,15 +192,20 @@
3.134 next
3.135 case (Binop fn e1 e2 s)
3.136 have "exec (compile (Binop fn e1 e2)) s env =
3.137 - exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
3.138 - also have "... = exec [Apply fn]
3.139 + exec (compile e2 @ compile e1 @ [Apply fn]) s env"
3.140 + by simp
3.141 + also have "\<dots> = exec [Apply fn]
3.142 (exec (compile e1) (exec (compile e2) s env) env) env"
3.143 by (simp only: exec_append)
3.144 - also have "exec (compile e2) s env = eval e2 env # s" by fact
3.145 - also have "exec (compile e1) ... env = eval e1 env # ..." by fact
3.146 - also have "exec [Apply fn] ... env =
3.147 - fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
3.148 - also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
3.149 + also have "exec (compile e2) s env = eval e2 env # s"
3.150 + by fact
3.151 + also have "exec (compile e1) \<dots> env = eval e1 env # \<dots>"
3.152 + by fact
3.153 + also have "exec [Apply fn] \<dots> env =
3.154 + fn (hd \<dots>) (hd (tl \<dots>)) # (tl (tl \<dots>))"
3.155 + by simp
3.156 + also have "\<dots> = fn (eval e1 env) (eval e2 env) # s"
3.157 + by simp
3.158 also have "fn (eval e1 env) (eval e2 env) =
3.159 eval (Binop fn e1 e2) env"
3.160 by simp
3.161 @@ -198,7 +215,8 @@
3.162 have "execute (compile e) env = hd (exec (compile e) [] env)"
3.163 by (simp add: execute_def)
3.164 also from exec_compile have "exec (compile e) [] env = [eval e env]" .
3.165 - also have "hd ... = eval e env" by simp
3.166 + also have "hd \<dots> = eval e env"
3.167 + by simp
3.168 finally show ?thesis .
3.169 qed
3.170
4.1 --- a/src/HOL/Isar_Examples/Fibonacci.thy Thu Feb 20 23:16:33 2014 +0100
4.2 +++ b/src/HOL/Isar_Examples/Fibonacci.thy Thu Feb 20 23:46:40 2014 +0100
4.3 @@ -40,7 +40,8 @@
4.4 text {* Alternative induction rule. *}
4.5
4.6 theorem fib_induct:
4.7 - "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
4.8 + fixes n :: nat
4.9 + shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
4.10 by (induct rule: fib.induct) simp_all
4.11
4.12
4.13 @@ -77,21 +78,23 @@
4.14 fix n
4.15 have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
4.16 by simp
4.17 - also have "... = fib (n + 2) + fib (n + 1)" by simp
4.18 - also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
4.19 + also have "\<dots> = fib (n + 2) + fib (n + 1)"
4.20 + by simp
4.21 + also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
4.22 by (rule gcd_add2_nat)
4.23 - also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
4.24 + also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
4.25 by (simp add: gcd_commute_nat)
4.26 - also assume "... = 1"
4.27 + also assume "\<dots> = 1"
4.28 finally show "?P (n + 2)" .
4.29 qed
4.30
4.31 -lemma gcd_mult_add: "(0::nat) < n ==> gcd (n * k + m) n = gcd m n"
4.32 +lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
4.33 proof -
4.34 assume "0 < n"
4.35 then have "gcd (n * k + m) n = gcd n (m mod n)"
4.36 by (simp add: gcd_non_0_nat add_commute)
4.37 - also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat)
4.38 + also from `0 < n` have "\<dots> = gcd m n"
4.39 + by (simp add: gcd_non_0_nat)
4.40 finally show ?thesis .
4.41 qed
4.42
4.43 @@ -106,22 +109,23 @@
4.44 also have "fib (n + k + 1)
4.45 = fib (k + 1) * fib (n + 1) + fib k * fib n"
4.46 by (rule fib_add)
4.47 - also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
4.48 + also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
4.49 by (simp add: gcd_mult_add)
4.50 - also have "... = gcd (fib n) (fib (k + 1))"
4.51 + also have "\<dots> = gcd (fib n) (fib (k + 1))"
4.52 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
4.53 - also have "... = gcd (fib m) (fib n)"
4.54 + also have "\<dots> = gcd (fib m) (fib n)"
4.55 using Suc by (simp add: gcd_commute_nat)
4.56 finally show ?thesis .
4.57 qed
4.58
4.59 lemma gcd_fib_diff:
4.60 - assumes "m <= n"
4.61 + assumes "m \<le> n"
4.62 shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
4.63 proof -
4.64 have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
4.65 by (simp add: gcd_fib_add)
4.66 - also from `m <= n` have "n - m + m = n" by simp
4.67 + also from `m \<le> n` have "n - m + m = n"
4.68 + by simp
4.69 finally show ?thesis .
4.70 qed
4.71
4.72 @@ -134,15 +138,18 @@
4.73 proof -
4.74 have "n mod m = (if n < m then n else (n - m) mod m)"
4.75 by (rule mod_if)
4.76 - also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
4.77 + also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
4.78 proof (cases "n < m")
4.79 - case True then show ?thesis by simp
4.80 + case True
4.81 + then show ?thesis by simp
4.82 next
4.83 - case False then have "m <= n" by simp
4.84 - from `0 < m` and False have "n - m < n" by simp
4.85 + case False
4.86 + then have "m \<le> n" by simp
4.87 + from `0 < m` and False have "n - m < n"
4.88 + by simp
4.89 with hyp have "gcd (fib m) (fib ((n - m) mod m))
4.90 = gcd (fib m) (fib (n - m))" by simp
4.91 - also have "... = gcd (fib m) (fib n)"
4.92 + also have "\<dots> = gcd (fib m) (fib n)"
4.93 using `m <= n` by (rule gcd_fib_diff)
4.94 finally have "gcd (fib m) (fib ((n - m) mod m)) =
4.95 gcd (fib m) (fib n)" .
4.96 @@ -154,12 +161,18 @@
4.97
4.98 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
4.99 proof (induct m n rule: gcd_nat_induct)
4.100 - fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
4.101 - fix n :: nat assume n: "0 < n"
4.102 - then have "gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat)
4.103 - also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
4.104 - also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
4.105 - also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat)
4.106 + fix m
4.107 + show "fib (gcd m 0) = gcd (fib m) (fib 0)"
4.108 + by simp
4.109 + fix n :: nat
4.110 + assume n: "0 < n"
4.111 + then have "gcd m n = gcd n (m mod n)"
4.112 + by (simp add: gcd_non_0_nat)
4.113 + also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
4.114 + also from n have "\<dots> = gcd (fib n) (fib m)"
4.115 + by (rule gcd_fib_mod)
4.116 + also have "\<dots> = gcd (fib m) (fib n)"
4.117 + by (rule gcd_commute_nat)
4.118 finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
4.119 qed
4.120
5.1 --- a/src/HOL/Isar_Examples/Peirce.thy Thu Feb 20 23:16:33 2014 +0100
5.2 +++ b/src/HOL/Isar_Examples/Peirce.thy Thu Feb 20 23:46:40 2014 +0100
5.3 @@ -19,18 +19,18 @@
5.4 there is negation elimination; it holds in intuitionistic logic as
5.5 well.} *}
5.6
5.7 -theorem "((A --> B) --> A) --> A"
5.8 +theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
5.9 proof
5.10 - assume "(A --> B) --> A"
5.11 + assume "(A \<longrightarrow> B) \<longrightarrow> A"
5.12 show A
5.13 proof (rule classical)
5.14 - assume "~ A"
5.15 - have "A --> B"
5.16 + assume "\<not> A"
5.17 + have "A \<longrightarrow> B"
5.18 proof
5.19 assume A
5.20 - with `~ A` show B by contradiction
5.21 + with `\<not> A` show B by contradiction
5.22 qed
5.23 - with `(A --> B) --> A` show A ..
5.24 + with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
5.25 qed
5.26 qed
5.27
5.28 @@ -48,19 +48,19 @@
5.29 contrast, strong assumptions (as introduced by \isacommand{assume})
5.30 are solved immediately. *}
5.31
5.32 -theorem "((A --> B) --> A) --> A"
5.33 +theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
5.34 proof
5.35 - assume "(A --> B) --> A"
5.36 + assume "(A \<longrightarrow> B) \<longrightarrow> A"
5.37 show A
5.38 proof (rule classical)
5.39 - presume "A --> B"
5.40 - with `(A --> B) --> A` show A ..
5.41 + presume "A \<longrightarrow> B"
5.42 + with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
5.43 next
5.44 - assume "~ A"
5.45 - show "A --> B"
5.46 + assume "\<not> A"
5.47 + show "A \<longrightarrow> B"
5.48 proof
5.49 assume A
5.50 - with `~ A` show B by contradiction
5.51 + with `\<not> A` show B by contradiction
5.52 qed
5.53 qed
5.54 qed
6.1 --- a/src/HOL/Isar_Examples/Summation.thy Thu Feb 20 23:16:33 2014 +0100
6.2 +++ b/src/HOL/Isar_Examples/Summation.thy Thu Feb 20 23:46:40 2014 +0100
6.3 @@ -26,10 +26,13 @@
6.4 proof (induct n)
6.5 show "?P 0" by simp
6.6 next
6.7 - fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
6.8 + fix n have "?S (n + 1) = ?S n + 2 * (n + 1)"
6.9 + by simp
6.10 also assume "?S n = n * (n + 1)"
6.11 - also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
6.12 - finally show "?P (Suc n)" by simp
6.13 + also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)"
6.14 + by simp
6.15 + finally show "?P (Suc n)"
6.16 + by simp
6.17 qed
6.18
6.19 text {* The above proof is a typical instance of mathematical
6.20 @@ -80,10 +83,14 @@
6.21 proof (induct n)
6.22 show "?P 0" by simp
6.23 next
6.24 - fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
6.25 + fix n
6.26 + have "?S (n + 1) = ?S n + 2 * n + 1"
6.27 + by simp
6.28 also assume "?S n = n^Suc (Suc 0)"
6.29 - also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
6.30 - finally show "?P (Suc n)" by simp
6.31 + also have "\<dots> + 2 * n + 1 = (n + 1)^Suc (Suc 0)"
6.32 + by simp
6.33 + finally show "?P (Suc n)"
6.34 + by simp
6.35 qed
6.36
6.37 text {* Subsequently we require some additional tweaking of Isabelle
6.38 @@ -98,12 +105,15 @@
6.39 proof (induct n)
6.40 show "?P 0" by simp
6.41 next
6.42 - fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
6.43 + fix n
6.44 + have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
6.45 by (simp add: distrib)
6.46 also assume "?S n = n * (n + 1) * (2 * n + 1)"
6.47 - also have "... + 6 * (n + 1)^Suc (Suc 0) =
6.48 - (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
6.49 - finally show "?P (Suc n)" by simp
6.50 + also have "\<dots> + 6 * (n + 1)^Suc (Suc 0) =
6.51 + (n + 1) * (n + 2) * (2 * (n + 1) + 1)"
6.52 + by (simp add: distrib)
6.53 + finally show "?P (Suc n)"
6.54 + by simp
6.55 qed
6.56
6.57 theorem sum_of_cubes:
6.58 @@ -112,12 +122,14 @@
6.59 proof (induct n)
6.60 show "?P 0" by (simp add: power_eq_if)
6.61 next
6.62 - fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
6.63 + fix n
6.64 + have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
6.65 by (simp add: power_eq_if distrib)
6.66 also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
6.67 - also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
6.68 + also have "\<dots> + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
6.69 by (simp add: power_eq_if distrib)
6.70 - finally show "?P (Suc n)" by simp
6.71 + finally show "?P (Suc n)"
6.72 + by simp
6.73 qed
6.74
6.75 text {* Note that in contrast to older traditions of tactical proof