1.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy Sat Oct 06 00:02:46 2001 +0200
1.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Mon Oct 08 12:13:34 2001 +0200
1.3 @@ -67,8 +67,8 @@
1.4 *}
1.5
1.6 consts f :: "nat \<Rightarrow> nat"
1.7 -recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
1.8 -"f i = (if #10 \<le> i then 0 else i * f(Suc i))"
1.9 +recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (10::nat)}"
1.10 +"f i = (if 10 \<le> i then 0 else i * f(Suc i))"
1.11
1.12 text{*\noindent
1.13 Since \isacommand{recdef} is not prepared for the relation supplied above,
1.14 @@ -111,13 +111,13 @@
1.15 *}
1.16 (*<*)
1.17 consts g :: "nat \<Rightarrow> nat"
1.18 -recdef g "{(i,j). j<i \<and> i \<le> (#10::nat)}"
1.19 -"g i = (if #10 \<le> i then 0 else i * g(Suc i))"
1.20 +recdef g "{(i,j). j<i \<and> i \<le> (10::nat)}"
1.21 +"g i = (if 10 \<le> i then 0 else i * g(Suc i))"
1.22 (*>*)
1.23 (hints recdef_wf: wf_greater)
1.24
1.25 text{*\noindent
1.26 -Alternatively, we could have given @{text "measure (\<lambda>k::nat. #10-k)"} for the
1.27 +Alternatively, we could have given @{text "measure (\<lambda>k::nat. 10-k)"} for the
1.28 well-founded relation in our \isacommand{recdef}. However, the arithmetic
1.29 goal in the lemma above would have arisen instead in the \isacommand{recdef}
1.30 termination proof, where we have less control. A tailor-made termination
2.1 --- a/doc-src/TutorialI/CTL/CTL.thy Sat Oct 06 00:02:46 2001 +0200
2.2 +++ b/doc-src/TutorialI/CTL/CTL.thy Mon Oct 08 12:13:34 2001 +0200
2.3 @@ -203,7 +203,7 @@
2.4 both the path property and the fact that @{term Q} holds:
2.5 *};
2.6
2.7 -apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> Q(p i))");
2.8 +apply(subgoal_tac "\<exists>p. s = p (0::nat) \<and> (\<forall>i. (p i, p(i+1)) \<in> M \<and> Q(p i))");
2.9
2.10 txt{*\noindent
2.11 From this proposition the original goal follows easily:
3.1 --- a/doc-src/TutorialI/Inductive/AB.thy Sat Oct 06 00:02:46 2001 +0200
3.2 +++ b/doc-src/TutorialI/Inductive/AB.thy Mon Oct 08 12:13:34 2001 +0200
3.3 @@ -23,13 +23,13 @@
3.4 and~@{term b}'s:
3.5 *}
3.6
3.7 -datatype alfa = a | b;
3.8 +datatype alfa = a | b
3.9
3.10 text{*\noindent
3.11 For convenience we include the following easy lemmas as simplification rules:
3.12 *}
3.13
3.14 -lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";
3.15 +lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)"
3.16 by (case_tac x, auto)
3.17
3.18 text{*\noindent
3.19 @@ -39,7 +39,7 @@
3.20
3.21 consts S :: "alfa list set"
3.22 A :: "alfa list set"
3.23 - B :: "alfa list set";
3.24 + B :: "alfa list set"
3.25
3.26 text{*\noindent
3.27 The productions above are recast as a \emph{mutual} inductive
3.28 @@ -57,7 +57,7 @@
3.29 "\<lbrakk> v\<in>A; w\<in>A \<rbrakk> \<Longrightarrow> b#v@w \<in> A"
3.30
3.31 "w \<in> S \<Longrightarrow> b#w \<in> B"
3.32 - "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B";
3.33 + "\<lbrakk> v \<in> B; w \<in> B \<rbrakk> \<Longrightarrow> a#v@w \<in> B"
3.34
3.35 text{*\noindent
3.36 First we show that all words in @{term S} contain the same number of @{term
3.37 @@ -105,7 +105,7 @@
3.38 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
3.39 @{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
3.40 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
3.41 -syntax.}, and @{term"#1::int"} is the integer 1 (see \S\ref{sec:numbers}).
3.42 +syntax.}, and @{term"1::int"} is the integer 1 (see \S\ref{sec:numbers}).
3.43
3.44 First we show that our specific function, the difference between the
3.45 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
3.46 @@ -117,7 +117,7 @@
3.47
3.48 lemma step1: "\<forall>i < size w.
3.49 \<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
3.50 - - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> #1"
3.51 + - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> Numeral1"
3.52
3.53 txt{*\noindent
3.54 The lemma is a bit hard to read because of the coercion function
3.55 @@ -132,9 +132,9 @@
3.56 discuss it.
3.57 *}
3.58
3.59 -apply(induct w);
3.60 - apply(simp);
3.61 -by(force simp add:zabs_def take_Cons split:nat.split if_splits);
3.62 +apply(induct w)
3.63 + apply(simp)
3.64 +by(force simp add: zabs_def take_Cons split: nat.split if_splits)
3.65
3.66 text{*
3.67 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:
3.68 @@ -142,7 +142,7 @@
3.69
3.70 lemma part1:
3.71 "size[x\<in>w. P x] = size[x\<in>w. \<not>P x]+2 \<Longrightarrow>
3.72 - \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1";
3.73 + \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1"
3.74
3.75 txt{*\noindent
3.76 This is proved by @{text force} with the help of the intermediate value theorem,
3.77 @@ -150,8 +150,8 @@
3.78 @{thm[source]step1}:
3.79 *}
3.80
3.81 -apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);
3.82 -by force;
3.83 +apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "Numeral1"])
3.84 +by force
3.85
3.86 text{*\noindent
3.87
3.88 @@ -164,8 +164,8 @@
3.89 "\<lbrakk>size[x\<in>take i w @ drop i w. P x] =
3.90 size[x\<in>take i w @ drop i w. \<not>P x]+2;
3.91 size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
3.92 - \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1";
3.93 -by(simp del:append_take_drop_id);
3.94 + \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1"
3.95 +by(simp del:append_take_drop_id)
3.96
3.97 text{*\noindent
3.98 In the proof we have disabled the normally useful lemma
3.99 @@ -180,7 +180,7 @@
3.100 definition are declared simplification rules:
3.101 *}
3.102
3.103 -declare S_A_B.intros[simp];
3.104 +declare S_A_B.intros[simp]
3.105
3.106 text{*\noindent
3.107 This could have been done earlier but was not necessary so far.
3.108 @@ -193,7 +193,7 @@
3.109 theorem completeness:
3.110 "(size[x\<in>w. x=a] = size[x\<in>w. x=b] \<longrightarrow> w \<in> S) \<and>
3.111 (size[x\<in>w. x=a] = size[x\<in>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
3.112 - (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)";
3.113 + (size[x\<in>w. x=b] = size[x\<in>w. x=a] + 1 \<longrightarrow> w \<in> B)"
3.114
3.115 txt{*\noindent
3.116 The proof is by induction on @{term w}. Structural induction would fail here
3.117 @@ -202,7 +202,7 @@
3.118 of @{term w}, using the induction rule @{thm[source]length_induct}:
3.119 *}
3.120
3.121 -apply(induct_tac w rule: length_induct);
3.122 +apply(induct_tac w rule: length_induct)
3.123 (*<*)apply(rename_tac w)(*>*)
3.124
3.125 txt{*\noindent
3.126 @@ -215,8 +215,8 @@
3.127 on whether @{term w} is empty or not.
3.128 *}
3.129
3.130 -apply(case_tac w);
3.131 - apply(simp_all);
3.132 +apply(case_tac w)
3.133 + apply(simp_all)
3.134 (*<*)apply(rename_tac x v)(*>*)
3.135
3.136 txt{*\noindent
4.1 --- a/doc-src/TutorialI/Inductive/Even.thy Sat Oct 06 00:02:46 2001 +0200
4.2 +++ b/doc-src/TutorialI/Inductive/Even.thy Mon Oct 08 12:13:34 2001 +0200
4.3 @@ -20,7 +20,7 @@
4.4 specified as \isa{intro!}
4.5
4.6 Our first lemma states that numbers of the form $2\times k$ are even. *}
4.7 -lemma two_times_even[intro!]: "#2*k \<in> even"
4.8 +lemma two_times_even[intro!]: "2*k \<in> even"
4.9 apply (induct "k")
4.10 txt{*
4.11 The first step is induction on the natural number \isa{k}, which leaves
4.12 @@ -36,11 +36,11 @@
4.13 this equivalence is trivial using the lemma just proved, whose \isa{intro!}
4.14 attribute ensures it will be applied automatically. *}
4.15
4.16 -lemma dvd_imp_even: "#2 dvd n \<Longrightarrow> n \<in> even"
4.17 +lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even"
4.18 by (auto simp add: dvd_def)
4.19
4.20 text{*our first rule induction!*}
4.21 -lemma even_imp_dvd: "n \<in> even \<Longrightarrow> #2 dvd n"
4.22 +lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
4.23 apply (erule even.induct)
4.24 txt{*
4.25 @{subgoals[display,indent=0,margin=65]}
4.26 @@ -58,7 +58,7 @@
4.27
4.28
4.29 text{*no iff-attribute because we don't always want to use it*}
4.30 -theorem even_iff_dvd: "(n \<in> even) = (#2 dvd n)"
4.31 +theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)"
4.32 by (blast intro: dvd_imp_even even_imp_dvd)
4.33
4.34 text{*this result ISN'T inductive...*}
4.35 @@ -70,7 +70,7 @@
4.36 oops
4.37
4.38 text{*...so we need an inductive lemma...*}
4.39 -lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n-#2 \<in> even"
4.40 +lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n - 2 \<in> even"
4.41 apply (erule even.induct)
4.42 txt{*
4.43 @{subgoals[display,indent=0,margin=65]}
5.1 --- a/doc-src/TutorialI/Recdef/examples.thy Sat Oct 06 00:02:46 2001 +0200
5.2 +++ b/doc-src/TutorialI/Recdef/examples.thy Mon Oct 08 12:13:34 2001 +0200
5.3 @@ -9,7 +9,7 @@
5.4 consts fib :: "nat \<Rightarrow> nat";
5.5 recdef fib "measure(\<lambda>n. n)"
5.6 "fib 0 = 0"
5.7 - "fib 1' = 1"
5.8 + "fib (Suc 0) = 1"
5.9 "fib (Suc(Suc x)) = fib x + fib (Suc x)";
5.10
5.11 text{*\noindent