--- a/doc-src/TutorialI/Advanced/WFrec.thy Sat Oct 06 00:02:46 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Mon Oct 08 12:13:34 2001 +0200
@@ -67,8 +67,8 @@
*}
consts f :: "nat \<Rightarrow> nat"
-recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
-"f i = (if #10 \<le> i then 0 else i * f(Suc i))"
+recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (10::nat)}"
+"f i = (if 10 \<le> i then 0 else i * f(Suc i))"
text{*\noindent
Since \isacommand{recdef} is not prepared for the relation supplied above,
@@ -111,13 +111,13 @@
*}
(*<*)
consts g :: "nat \<Rightarrow> nat"
-recdef g "{(i,j). j<i \<and> i \<le> (#10::nat)}"
-"g i = (if #10 \<le> i then 0 else i * g(Suc i))"
+recdef g "{(i,j). j<i \<and> i \<le> (10::nat)}"
+"g i = (if 10 \<le> i then 0 else i * g(Suc i))"
(*>*)
(hints recdef_wf: wf_greater)
text{*\noindent
-Alternatively, we could have given @{text "measure (\<lambda>k::nat. #10-k)"} for the
+Alternatively, we could have given @{text "measure (\<lambda>k::nat. 10-k)"} for the
well-founded relation in our \isacommand{recdef}. However, the arithmetic
goal in the lemma above would have arisen instead in the \isacommand{recdef}
termination proof, where we have less control. A tailor-made termination
--- a/doc-src/TutorialI/CTL/CTL.thy Sat Oct 06 00:02:46 2001 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Mon Oct 08 12:13:34 2001 +0200
@@ -203,7 +203,7 @@
both the path property and the fact that @{term Q} holds:
*};
-apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> Q(p i))");
+apply(subgoal_tac "\<exists>p. s = p (0::nat) \<and> (\<forall>i. (p i, p(i+1)) \<in> M \<and> Q(p i))");
txt{*\noindent
From this proposition the original goal follows easily:
--- a/doc-src/TutorialI/Inductive/AB.thy Sat Oct 06 00:02:46 2001 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Mon Oct 08 12:13:34 2001 +0200
@@ -23,13 +23,13 @@
and~@{term b}'s:
*}
-datatype alfa = a | b;
+datatype alfa = a | b
text{*\noindent
For convenience we include the following easy lemmas as simplification rules:
*}
-lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";
+lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)"
by (case_tac x, auto)
text{*\noindent
@@ -39,7 +39,7 @@
consts S :: "alfa list set"
A :: "alfa list set"
- B :: "alfa list set";
+ B :: "alfa list set"
text{*\noindent
The productions above are recast as a \emph{mutual} inductive
@@ -57,7 +57,7 @@
"\<lbrakk> v\<in>A; w\<in>A \<rbrakk> \<Longrightarrow> b#v@w \<in> A"
"w \<in> S \<Longrightarrow> b#w \<in> B"
- "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B";
+ "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B"
text{*\noindent
First we show that all words in @{term S} contain the same number of @{term
@@ -105,7 +105,7 @@
where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
@{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
-syntax.}, and @{term"#1::int"} is the integer 1 (see \S\ref{sec:numbers}).
+syntax.}, and @{term"1::int"} is the integer 1 (see \S\ref{sec:numbers}).
First we show that our specific function, the difference between the
numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
@@ -117,7 +117,7 @@
lemma step1: "\<forall>i < size w.
\<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
- - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> #1"
+ - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> Numeral1"
txt{*\noindent
The lemma is a bit hard to read because of the coercion function
@@ -132,9 +132,9 @@
discuss it.
*}
-apply(induct w);
- apply(simp);
-by(force simp add:zabs_def take_Cons split:nat.split if_splits);
+apply(induct w)
+ apply(simp)
+by(force simp add: zabs_def take_Cons split: nat.split if_splits)
text{*
Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:
@@ -142,7 +142,7 @@
lemma part1:
"size[x\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
- \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1";
+ \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1"
txt{*\noindent
This is proved by @{text force} with the help of the intermediate value theorem,
@@ -150,8 +150,8 @@
@{thm[source]step1}:
*}
-apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);
-by force;
+apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "Numeral1"])
+by force
text{*\noindent
@@ -164,8 +164,8 @@
"\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
size[x\<in>take i w @ drop i w. \<not>P x]+2;
size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
- \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1";
-by(simp del:append_take_drop_id);
+ \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1"
+by(simp del:append_take_drop_id)
text{*\noindent
In the proof we have disabled the normally useful lemma
@@ -180,7 +180,7 @@
definition are declared simplification rules:
*}
-declare S_A_B.intros[simp];
+declare S_A_B.intros[simp]
text{*\noindent
This could have been done earlier but was not necessary so far.
@@ -193,7 +193,7 @@
theorem completeness:
"(size[x\<in>w. x=a] = size[x\<in>w. x=b] \<longrightarrow> w \<in> S) \<and>
(size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
- (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)";
+ (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)"
txt{*\noindent
The proof is by induction on @{term w}. Structural induction would fail here
@@ -202,7 +202,7 @@
of @{term w}, using the induction rule @{thm[source]length_induct}:
*}
-apply(induct_tac w rule: length_induct);
+apply(induct_tac w rule: length_induct)
(*<*)apply(rename_tac w)(*>*)
txt{*\noindent
@@ -215,8 +215,8 @@
on whether @{term w} is empty or not.
*}
-apply(case_tac w);
- apply(simp_all);
+apply(case_tac w)
+ apply(simp_all)
(*<*)apply(rename_tac x v)(*>*)
txt{*\noindent
--- a/doc-src/TutorialI/Inductive/Even.thy Sat Oct 06 00:02:46 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy Mon Oct 08 12:13:34 2001 +0200
@@ -20,7 +20,7 @@
specified as \isa{intro!}
Our first lemma states that numbers of the form $2\times k$ are even. *}
-lemma two_times_even[intro!]: "#2*k \<in> even"
+lemma two_times_even[intro!]: "2*k \<in> even"
apply (induct "k")
txt{*
The first step is induction on the natural number \isa{k}, which leaves
@@ -36,11 +36,11 @@
this equivalence is trivial using the lemma just proved, whose \isa{intro!}
attribute ensures it will be applied automatically. *}
-lemma dvd_imp_even: "#2 dvd n \<Longrightarrow> n \<in> even"
+lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even"
by (auto simp add: dvd_def)
text{*our first rule induction!*}
-lemma even_imp_dvd: "n \<in> even \<Longrightarrow> #2 dvd n"
+lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
apply (erule even.induct)
txt{*
@{subgoals[display,indent=0,margin=65]}
@@ -58,7 +58,7 @@
text{*no iff-attribute because we don't always want to use it*}
-theorem even_iff_dvd: "(n \<in> even) = (#2 dvd n)"
+theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)"
by (blast intro: dvd_imp_even even_imp_dvd)
text{*this result ISN'T inductive...*}
@@ -70,7 +70,7 @@
oops
text{*...so we need an inductive lemma...*}
-lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n-#2 \<in> even"
+lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n - 2 \<in> even"
apply (erule even.induct)
txt{*
@{subgoals[display,indent=0,margin=65]}
--- a/doc-src/TutorialI/Recdef/examples.thy Sat Oct 06 00:02:46 2001 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Mon Oct 08 12:13:34 2001 +0200
@@ -9,7 +9,7 @@
consts fib :: "nat \<Rightarrow> nat";
recdef fib "measure(\<lambda>n. n)"
"fib 0 = 0"
- "fib 1' = 1"
+ "fib (Suc 0) = 1"
"fib (Suc(Suc x)) = fib x + fib (Suc x)";
text{*\noindent