--- a/doc-src/TutorialI/Overview/Ind.thy Wed Jun 26 10:26:46 2002 +0200
+++ b/doc-src/TutorialI/Overview/Ind.thy Wed Jun 26 11:07:14 2002 +0200
@@ -1,4 +1,4 @@
-theory Ind = Main:
+(*<*)theory Ind = Main:(*>*)
section{*Inductive Definitions*}
@@ -21,7 +21,10 @@
subsubsection{*Rule Induction*}
-thm even.induct
+text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
+@{thm[display] even.induct[no_vars]}
+*}
+(*<*)thm even.induct[no_vars](*>*)
lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
apply (erule even.induct)
@@ -31,7 +34,8 @@
subsubsection{*Rule Inversion*}
inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even"
-thm Suc_Suc_case
+text{* @{thm[display] Suc_Suc_case[no_vars]} *}
+(*<*)thm Suc_Suc_case(*>*)
lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even"
by blast
@@ -84,8 +88,7 @@
subsection{*The accessible part of a relation*}
-consts
- acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
+consts acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
inductive "acc r"
intros
"(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
@@ -99,11 +102,10 @@
apply(erule acc.induct)
by blast
-consts
- accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
+consts accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
inductive "accs r"
intros
"r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r"
monos Pow_mono
-end
+(*<*)end(*>*)
--- a/doc-src/TutorialI/Overview/Isar.thy Wed Jun 26 10:26:46 2002 +0200
+++ b/doc-src/TutorialI/Overview/Isar.thy Wed Jun 26 11:07:14 2002 +0200
@@ -10,7 +10,7 @@
proof
show "lfp ?F \<subseteq> ?toA"
by (blast intro!: lfp_lowerbound intro: rtrancl_trans)
-
+next
show "?toA \<subseteq> lfp ?F"
proof
fix s assume "s \<in> ?toA"
@@ -20,6 +20,7 @@
proof (rule converse_rtrancl_induct)
from tA have "t \<in> ?F (lfp ?F)" by blast
with mono_ef show "t \<in> lfp ?F" ..
+ next
fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*"
and "s' \<in> lfp ?F"
then have "s \<in> ?F (lfp ?F)" by blast
--- a/doc-src/TutorialI/Overview/RECDEF.thy Wed Jun 26 10:26:46 2002 +0200
+++ b/doc-src/TutorialI/Overview/RECDEF.thy Wed Jun 26 11:07:14 2002 +0200
@@ -61,8 +61,14 @@
subsubsection{*Induction*}
+text{*
+Every recursive definition provides an induction theorem, for example
+@{thm[source]sep.induct}:
+@{thm[display,margin=70] sep.induct[no_vars]}
+*}
+(*<*)thm sep.induct[no_vars](*>*)
+
lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
-thm sep.induct
apply(induct_tac x xs rule: sep.induct)
apply simp_all
done
--- a/doc-src/TutorialI/Overview/Sets.thy Wed Jun 26 10:26:46 2002 +0200
+++ b/doc-src/TutorialI/Overview/Sets.thy Wed Jun 26 11:07:14 2002 +0200
@@ -15,6 +15,10 @@
\end{tabular}
\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}"
+term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*)
subsection{*Some Functions*}
@@ -26,41 +30,63 @@
@{thm vimage_def[no_vars]}
\end{tabular}
*}
-(*<*)
-thm id_def
-thm o_def[no_vars]
-thm image_def[no_vars]
-thm vimage_def[no_vars]
-(*>*)
+(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)
subsection{*Some Relations*}
+text{*
+\begin{tabular}{l}
+@{thm Id_def}\\
+@{thm converse_def[no_vars]}\\
+@{thm Image_def[no_vars]}\\
+@{thm rtrancl_refl[no_vars]}\\
+@{thm rtrancl_into_rtrancl[no_vars]}\\
+@{thm trancl_def[no_vars]}
+\end{tabular}
+*}
+(*<*)
thm Id_def
-thm converse_def
-thm Image_def
-thm relpow.simps
-thm rtrancl_idemp
-thm trancl_converse
+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]
+(*>*)
subsection{*Wellfoundedness*}
-thm wf_def
-thm wf_iff_no_infinite_down_chain
-
+text{*
+\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]
+(*>*)
subsection{*Fixed Point Operators*}
+text{*
+\begin{tabular}{l}
+@{thm lfp_def[no_vars]}\\
+@{thm lfp_unfold[no_vars]}\\
+@{thm lfp_induct[no_vars]}
+\end{tabular}
+*}
+(*<*)
thm lfp_def gfp_def
thm lfp_unfold
thm lfp_induct
-
+(*>*)
subsection{*Case Study: Verified Model Checking*}
typedecl state
-consts M :: "(state \<times> state)set";
+consts M :: "(state \<times> state)set"
typedecl atom
@@ -79,9 +105,9 @@
"s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))"
"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
-"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)";
+"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
-consts mc :: "formula \<Rightarrow> state set";
+consts mc :: "formula \<Rightarrow> state set"
primrec
"mc(Atom a) = {s. a \<in> L s}"
"mc(Neg f) = -mc f"
@@ -99,9 +125,9 @@
apply(rule equalityI)
thm lfp_lowerbound
apply(rule lfp_lowerbound)
- apply(blast intro: rtrancl_trans);
+ apply(blast intro: rtrancl_trans)
apply(rule subsetI)
-apply(simp, clarify)
+apply clarsimp
apply(erule converse_rtrancl_induct)
thm lfp_unfold[OF mono_ef]
apply(subst lfp_unfold[OF mono_ef])
@@ -110,10 +136,10 @@
apply(blast)
done
-theorem "mc f = {s. s \<Turnstile> f}";
-apply(induct_tac f);
-apply(auto simp add: EF_lemma);
-done;
+theorem "mc f = {s. s \<Turnstile> f}"
+apply(induct_tac f)
+apply(auto simp add: EF_lemma)
+done
text{*
\begin{exercise}
--- a/doc-src/TutorialI/Overview/document/root.tex Wed Jun 26 10:26:46 2002 +0200
+++ b/doc-src/TutorialI/Overview/document/root.tex Wed Jun 26 11:07:14 2002 +0200
@@ -39,7 +39,7 @@
\input{Ind.tex}
-\input{Isar.tex}
+%\input{Isar.tex}
%%% Local Variables:
%%% mode: latex