# HG changeset patch
# User nipkow
# Date 1025082434 -7200
# Node ID 4b3de63701841df832ce4e1e30fb487c5ae38d2e
# Parent  ae66c22ed52ebff3de8ea773f9eb79d4c5233c1f
*** empty log message ***

diff -r ae66c22ed52e -r 4b3de6370184 doc-src/TutorialI/Overview/Ind.thy
--- 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(*>*)
diff -r ae66c22ed52e -r 4b3de6370184 doc-src/TutorialI/Overview/Isar.thy
--- 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
diff -r ae66c22ed52e -r 4b3de6370184 doc-src/TutorialI/Overview/RECDEF.thy
--- 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
diff -r ae66c22ed52e -r 4b3de6370184 doc-src/TutorialI/Overview/Sets.thy
--- 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}
diff -r ae66c22ed52e -r 4b3de6370184 doc-src/TutorialI/Overview/document/root.tex
--- 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