--- 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"
apply (simp add: add_mult_distrib2)
-(*<*)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"; }
+}