author nipkow Wed, 26 Jun 2002 12:17:21 +0200 changeset 13250 efd5db7dc7cc parent 13249 4b3de6370184 child 13251 74cb2af8811e
*** empty log message ***
 doc-src/TutorialI/Overview/FP0.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/FP1.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/Ind.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/Ordinal.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/Rules.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/Sets.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/delete-verbatim file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/Overview/FP0.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP0.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -17,7 +17,6 @@
theorem rev_rev [simp]: "rev(rev xs) = xs"
(*<*)oops(*>*)

-
text{*
\begin{exercise}
Define a datatype of binary trees and a function @{term mirror}
@@ -29,5 +28,4 @@
@{prop"flatten(mirror t) = rev(flatten t)"}.
\end{exercise}
*}
-
end
--- a/doc-src/TutorialI/Overview/FP1.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP1.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -1,6 +1,4 @@
-(*<*)
-theory FP1 = Main:
-(*>*)
+(*<*)theory FP1 = Main:(*>*)

lemma "if xs = ys
then rev xs = rev ys
@@ -28,9 +26,7 @@
apply(auto)
done

-text{*
-Some examples of linear arithmetic:
-*}
+text{*Some examples of linear arithmetic:*}

lemma "\<lbrakk> \<not> m < n; m < n+(1::int) \<rbrakk> \<Longrightarrow> m = n"
by(auto)
@@ -38,9 +34,7 @@
lemma "min i (max j k) = max (min k i) (min i (j::nat))"
by(arith)

-text{*
-Not proved automatically because it involves multiplication:
-*}
+text{*Not proved automatically because it involves multiplication:*}

lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)"
(*<*)oops(*>*)
@@ -75,9 +69,7 @@
lemma fst_conv[simp]: "fst(x,y) = x"
by auto

-text{*
-Setting and resetting the @{text simp} attribute:
-*}
+text{*Setting and resetting the @{text simp} attribute:*}

declare fst_conv[simp]
declare fst_conv[simp del]
@@ -94,7 +86,7 @@

lemma "\<forall>x::nat. x*(y+z) = r"
-(*<*)oops(*>*)text_raw {* \isanewline\isanewline *}
+(*<*)oops(*>*)text_raw{* \isanewline\isanewline *}

lemma "rev(rev(xs @ [])) = xs"
apply (simp del: rev_rev_ident)
@@ -129,7 +121,7 @@

lemma "\<forall>xs. if xs = [] then A else B"
apply simp
-(*<*)oops(*>*)text_raw {* \isanewline\isanewline *}
+(*<*)oops(*>*)text_raw{* \isanewline\isanewline *}

lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y"
apply simp
@@ -139,15 +131,11 @@

subsubsection{*Arithmetic*}

-text{*
-Is simple enough for the default arithmetic:
-*}
+text{*Is simple enough for the default arithmetic:*}
lemma "\<lbrakk> \<not> m < n; m < n+(1::nat) \<rbrakk> \<Longrightarrow> m = n"
by simp

-text{*
-Contains boolean combinations and needs full arithmetic:
-*}
+text{*Contains boolean combinations and needs full arithmetic:*}
lemma "\<not> m < n \<and> m < n+(1::nat) \<Longrightarrow> m = n"
apply simp
by(arith)
@@ -161,7 +149,6 @@
(*>*)

-
subsection{*Case Study: Compiling Expressions*}

@@ -262,7 +249,6 @@
datatype tree = C "tree list"

text{*Some trees:*}
-
term "C []"
term "C [C [C []], C []]"

@@ -287,7 +273,6 @@
\end{exercise}
*}

-
subsubsection{*Datatypes Involving Functions*}

datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
@@ -309,13 +294,9 @@
\begin{verbatim}
datatype lambda = C "lambda => lambda"
\end{verbatim}
-*}

-text{*
\begin{exercise}
Define a datatype of ordinals and the ordinal $\Gamma_0$.
\end{exercise}
*}
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
--- a/doc-src/TutorialI/Overview/Ind.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/Ind.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -22,8 +22,7 @@
subsubsection{*Rule Induction*}

text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
-@{thm[display] even.induct[no_vars]}
-*}
+@{thm[display] even.induct[no_vars]}*}
(*<*)thm even.induct[no_vars](*>*)

lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
@@ -83,8 +82,7 @@
\begin{exercise}
Show that the converse of @{thm[source]rtc_step} also holds:
@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
-\end{exercise}
-*}
+\end{exercise}*}

subsection{*The accessible part of a relation*}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/Ordinal.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -0,0 +1,52 @@
+theory Ordinal = Main:
+
+datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"
+
+consts
+  pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option"
+primrec
+  "pred Zero n = None"
+  "pred (Succ a) n = Some a"
+  "pred (Limit f) n = Some (f n)"
+
+constdefs
+  OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+  "OpLim F a \<equiv> Limit (\<lambda>n. F n a)"
+  OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<Squnion>")
+  "\<Squnion>f \<equiv> OpLim (power f)"
+
+consts
+  cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
+primrec
+  "cantor a Zero = Succ a"
+  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
+  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
+
+consts
+  Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<nabla>")
+primrec
+  "\<nabla>f Zero = f Zero"
+  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
+  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
+
+constdefs
+  deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+  "deriv f \<equiv> \<nabla>(\<Squnion>f)"
+
+consts
+  veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
+primrec
+  "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))"
+  "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
+  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
+
+constdefs
+  veb :: "ordinal \<Rightarrow> ordinal"
+  "veb a \<equiv> veblen a Zero"
+  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
+  "\<epsilon>\<^sub>0 \<equiv> veb Zero"
+  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
+  "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
+thm Gamma0_def
+
+end
--- a/doc-src/TutorialI/Overview/Rules.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/Rules.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -1,6 +1,4 @@
-(*<*)
-theory Rules = Main:
-(*>*)
+(*<*)theory Rules = Main:(*>*)

section{*The Rules of the Game*}

@@ -19,9 +17,7 @@
\end{center}
*}

-(*<*)
-thm impI conjI disjI1 disjI2 iffI
-(*>*)
+(*<*)thm impI conjI disjI1 disjI2 iffI(*>*)

lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)"
apply(rule impI)
@@ -45,13 +41,11 @@
\end{tabular}
\end{center}
*}
-
(*<*)
thm impE mp
thm conjE
thm disjE
(*>*)
-
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
apply (erule disjE)
apply (rule disjI2)
@@ -74,9 +68,7 @@
\end{center}
*}

-(*<*)
-thm conjunct1 conjunct1 iffD1 iffD2
-(*>*)
+(*<*)thm conjunct1 conjunct1 iffD1 iffD2(*>*)

lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"
apply (rule conjI)
@@ -100,13 +92,11 @@
\end{tabular}
\end{center}
*}
-
(*<*)
thm allI exI
thm allE exE
thm spec
(*>*)
-
lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
(*<*)oops(*>*)

@@ -160,7 +150,6 @@
\end{tabular}
\end{center}
*}
-
(*<*)
thm append_self_conv
thm append_self_conv[of _ "[]"]
@@ -168,7 +157,6 @@
thm sym[OF append_self_conv]
thm append_self_conv[THEN sym]
(*>*)
-
subsection{*Further Useful Methods*}

lemma "n \<le> 1 \<and> n \<noteq> 0 \<Longrightarrow> n^n = n"
@@ -178,7 +166,6 @@
done

text{* And a cute example: *}
-
lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q;
\<forall>x y z. sqrt x * sqrt x = x \<and>
x ^ 2 = x * x \<and>
@@ -192,7 +179,6 @@
apply simp
done
*)
-(*<*)
-oops
-end
-(*>*)
+(*<*)oops
+
+end(*>*)
--- a/doc-src/TutorialI/Overview/Sets.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/Sets.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -1,6 +1,5 @@
-(*<*)
-theory Sets = Main:
-(*>*)
+(*<*)theory Sets = Main:(*>*)
+
section{*Sets, Functions and Relations*}

subsection{*Set Notation*}
@@ -13,8 +12,7 @@
@{term "{a,b}"} & @{text "{x. P x}"} \\
@{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"}
\end{tabular}
-\end{center}
-*}
+\end{center}*}
(*<*)term "A \<union> B" term "A \<inter> B" term "A - B"
term "a \<in> A" term "b \<notin> A"
term "{a,b}" term "{x. P x}"
@@ -28,8 +26,7 @@
@{thm o_def[no_vars]}\\
@{thm image_def[no_vars]}\\
@{thm vimage_def[no_vars]}
-\end{tabular}
-*}
+\end{tabular}*}
(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)

subsection{*Some Relations*}
@@ -42,16 +39,13 @@
@{thm rtrancl_refl[no_vars]}\\
@{thm rtrancl_into_rtrancl[no_vars]}\\
@{thm trancl_def[no_vars]}
-\end{tabular}
-*}
-(*<*)
-thm Id_def
+\end{tabular}*}
+(*<*)thm Id_def
thm converse_def[no_vars]
thm Image_def[no_vars]
thm relpow.simps[no_vars]
thm rtrancl.intros[no_vars]
-thm trancl_def[no_vars]
-(*>*)
+thm trancl_def[no_vars](*>*)

subsection{*Wellfoundedness*}

@@ -59,12 +53,9 @@
\begin{tabular}{l}
@{thm wf_def[no_vars]}\\
@{thm wf_iff_no_infinite_down_chain[no_vars]}
-\end{tabular}
-*}
-(*<*)
-thm wf_def[no_vars]
-thm wf_iff_no_infinite_down_chain[no_vars]
-(*>*)
+\end{tabular}*}
+(*<*)thm wf_def[no_vars]
+thm wf_iff_no_infinite_down_chain[no_vars](*>*)

subsection{*Fixed Point Operators*}

@@ -73,13 +64,10 @@
@{thm lfp_def[no_vars]}\\
@{thm lfp_unfold[no_vars]}\\
@{thm lfp_induct[no_vars]}
-\end{tabular}
-*}
-(*<*)
-thm lfp_def gfp_def
+\end{tabular}*}
+(*<*)thm lfp_def gfp_def
thm lfp_unfold
-thm lfp_induct
-(*>*)
+thm lfp_induct(*>*)

subsection{*Case Study: Verified Model Checking*}

@@ -151,8 +139,5 @@

Show that the semantics for @{term EF} satisfies the following recursion equation:
@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
-\end{exercise}
-*}
-(*<*)
-end
-(*>*)
+\end{exercise}*}
+(*<*)end(*>*)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/delete-verbatim	Wed Jun 26 12:17:21 2002 +0200
@@ -0,0 +1,34 @@
+#!/usr/bin/perl -w
+
+sub doit {
+    my ($file) = @_; + + open (FILE,$file) || die $!; + undef$/; $text = <FILE>;$/ = "\n";
+    close FILE || die $!; + +$_ = $text; + + s/text_raw\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here + s/text\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here + s/$$\*<\*$$//sg; + s/$$\*>\*$$//sg; + +$result = $_; + + if ($text ne $result) { + print STDERR "fixing$file\n";
+#        if (! -f "$file~~") { +# rename$file, "$file~~" || die$!;
+#        }
+        open (FILE, "> Demo/$file") || die$!;
+        print FILE $result; + close FILE || die$!;
+    }
+}
+
+
+foreach $file (@ARGV) { + eval { &doit($file); };
+  if ($@) { print STDERR "*** doit$file: ", \$@, "\n"; }
+}