# HG changeset patch
# User wenzelm
# Date 1002536014 -7200
# Node ID ac8ca15c556cad0e552e513ccf16e7682ade9e7d
# Parent  3c50a2cd6f00e303d92da90d0213ace3d376cad2
fixed numerals;

diff -r 3c50a2cd6f00 -r ac8ca15c556c doc-src/TutorialI/Advanced/WFrec.thy
--- 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
diff -r 3c50a2cd6f00 -r ac8ca15c556c doc-src/TutorialI/CTL/CTL.thy
--- 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:
diff -r 3c50a2cd6f00 -r ac8ca15c556c doc-src/TutorialI/Inductive/AB.thy
--- 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
diff -r 3c50a2cd6f00 -r ac8ca15c556c doc-src/TutorialI/Inductive/Even.thy
--- 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]}
diff -r 3c50a2cd6f00 -r ac8ca15c556c doc-src/TutorialI/Recdef/examples.thy
--- 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