1.1 --- a/doc-src/TutorialI/Overview/Ind.thy Wed Jun 26 10:26:46 2002 +0200
1.2 +++ b/doc-src/TutorialI/Overview/Ind.thy Wed Jun 26 11:07:14 2002 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -theory Ind = Main:
1.5 +(*<*)theory Ind = Main:(*>*)
1.6
1.7 section{*Inductive Definitions*}
1.8
1.9 @@ -21,7 +21,10 @@
1.10
1.11 subsubsection{*Rule Induction*}
1.12
1.13 -thm even.induct
1.14 +text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
1.15 +@{thm[display] even.induct[no_vars]}
1.16 +*}
1.17 +(*<*)thm even.induct[no_vars](*>*)
1.18
1.19 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
1.20 apply (erule even.induct)
1.21 @@ -31,7 +34,8 @@
1.22 subsubsection{*Rule Inversion*}
1.23
1.24 inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even"
1.25 -thm Suc_Suc_case
1.26 +text{* @{thm[display] Suc_Suc_case[no_vars]} *}
1.27 +(*<*)thm Suc_Suc_case(*>*)
1.28
1.29 lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even"
1.30 by blast
1.31 @@ -84,8 +88,7 @@
1.32
1.33 subsection{*The accessible part of a relation*}
1.34
1.35 -consts
1.36 - acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
1.37 +consts acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
1.38 inductive "acc r"
1.39 intros
1.40 "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
1.41 @@ -99,11 +102,10 @@
1.42 apply(erule acc.induct)
1.43 by blast
1.44
1.45 -consts
1.46 - accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
1.47 +consts accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
1.48 inductive "accs r"
1.49 intros
1.50 "r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r"
1.51 monos Pow_mono
1.52
1.53 -end
1.54 +(*<*)end(*>*)
2.1 --- a/doc-src/TutorialI/Overview/Isar.thy Wed Jun 26 10:26:46 2002 +0200
2.2 +++ b/doc-src/TutorialI/Overview/Isar.thy Wed Jun 26 11:07:14 2002 +0200
2.3 @@ -10,7 +10,7 @@
2.4 proof
2.5 show "lfp ?F \<subseteq> ?toA"
2.6 by (blast intro!: lfp_lowerbound intro: rtrancl_trans)
2.7 -
2.8 +next
2.9 show "?toA \<subseteq> lfp ?F"
2.10 proof
2.11 fix s assume "s \<in> ?toA"
2.12 @@ -20,6 +20,7 @@
2.13 proof (rule converse_rtrancl_induct)
2.14 from tA have "t \<in> ?F (lfp ?F)" by blast
2.15 with mono_ef show "t \<in> lfp ?F" ..
2.16 + next
2.17 fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*"
2.18 and "s' \<in> lfp ?F"
2.19 then have "s \<in> ?F (lfp ?F)" by blast
3.1 --- a/doc-src/TutorialI/Overview/RECDEF.thy Wed Jun 26 10:26:46 2002 +0200
3.2 +++ b/doc-src/TutorialI/Overview/RECDEF.thy Wed Jun 26 11:07:14 2002 +0200
3.3 @@ -61,8 +61,14 @@
3.4
3.5 subsubsection{*Induction*}
3.6
3.7 +text{*
3.8 +Every recursive definition provides an induction theorem, for example
3.9 +@{thm[source]sep.induct}:
3.10 +@{thm[display,margin=70] sep.induct[no_vars]}
3.11 +*}
3.12 +(*<*)thm sep.induct[no_vars](*>*)
3.13 +
3.14 lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
3.15 -thm sep.induct
3.16 apply(induct_tac x xs rule: sep.induct)
3.17 apply simp_all
3.18 done
4.1 --- a/doc-src/TutorialI/Overview/Sets.thy Wed Jun 26 10:26:46 2002 +0200
4.2 +++ b/doc-src/TutorialI/Overview/Sets.thy Wed Jun 26 11:07:14 2002 +0200
4.3 @@ -15,6 +15,10 @@
4.4 \end{tabular}
4.5 \end{center}
4.6 *}
4.7 +(*<*)term "A \<union> B" term "A \<inter> B" term "A - B"
4.8 +term "a \<in> A" term "b \<notin> A"
4.9 +term "{a,b}" term "{x. P x}"
4.10 +term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*)
4.11
4.12 subsection{*Some Functions*}
4.13
4.14 @@ -26,41 +30,63 @@
4.15 @{thm vimage_def[no_vars]}
4.16 \end{tabular}
4.17 *}
4.18 -(*<*)
4.19 -thm id_def
4.20 -thm o_def[no_vars]
4.21 -thm image_def[no_vars]
4.22 -thm vimage_def[no_vars]
4.23 -(*>*)
4.24 +(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)
4.25
4.26 subsection{*Some Relations*}
4.27
4.28 +text{*
4.29 +\begin{tabular}{l}
4.30 +@{thm Id_def}\\
4.31 +@{thm converse_def[no_vars]}\\
4.32 +@{thm Image_def[no_vars]}\\
4.33 +@{thm rtrancl_refl[no_vars]}\\
4.34 +@{thm rtrancl_into_rtrancl[no_vars]}\\
4.35 +@{thm trancl_def[no_vars]}
4.36 +\end{tabular}
4.37 +*}
4.38 +(*<*)
4.39 thm Id_def
4.40 -thm converse_def
4.41 -thm Image_def
4.42 -thm relpow.simps
4.43 -thm rtrancl_idemp
4.44 -thm trancl_converse
4.45 +thm converse_def[no_vars]
4.46 +thm Image_def[no_vars]
4.47 +thm relpow.simps[no_vars]
4.48 +thm rtrancl.intros[no_vars]
4.49 +thm trancl_def[no_vars]
4.50 +(*>*)
4.51
4.52 subsection{*Wellfoundedness*}
4.53
4.54 -thm wf_def
4.55 -thm wf_iff_no_infinite_down_chain
4.56 -
4.57 +text{*
4.58 +\begin{tabular}{l}
4.59 +@{thm wf_def[no_vars]}\\
4.60 +@{thm wf_iff_no_infinite_down_chain[no_vars]}
4.61 +\end{tabular}
4.62 +*}
4.63 +(*<*)
4.64 +thm wf_def[no_vars]
4.65 +thm wf_iff_no_infinite_down_chain[no_vars]
4.66 +(*>*)
4.67
4.68 subsection{*Fixed Point Operators*}
4.69
4.70 +text{*
4.71 +\begin{tabular}{l}
4.72 +@{thm lfp_def[no_vars]}\\
4.73 +@{thm lfp_unfold[no_vars]}\\
4.74 +@{thm lfp_induct[no_vars]}
4.75 +\end{tabular}
4.76 +*}
4.77 +(*<*)
4.78 thm lfp_def gfp_def
4.79 thm lfp_unfold
4.80 thm lfp_induct
4.81 -
4.82 +(*>*)
4.83
4.84 subsection{*Case Study: Verified Model Checking*}
4.85
4.86
4.87 typedecl state
4.88
4.89 -consts M :: "(state \<times> state)set";
4.90 +consts M :: "(state \<times> state)set"
4.91
4.92 typedecl atom
4.93
4.94 @@ -79,9 +105,9 @@
4.95 "s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))"
4.96 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
4.97 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
4.98 -"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)";
4.99 +"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
4.100
4.101 -consts mc :: "formula \<Rightarrow> state set";
4.102 +consts mc :: "formula \<Rightarrow> state set"
4.103 primrec
4.104 "mc(Atom a) = {s. a \<in> L s}"
4.105 "mc(Neg f) = -mc f"
4.106 @@ -99,9 +125,9 @@
4.107 apply(rule equalityI)
4.108 thm lfp_lowerbound
4.109 apply(rule lfp_lowerbound)
4.110 - apply(blast intro: rtrancl_trans);
4.111 + apply(blast intro: rtrancl_trans)
4.112 apply(rule subsetI)
4.113 -apply(simp, clarify)
4.114 +apply clarsimp
4.115 apply(erule converse_rtrancl_induct)
4.116 thm lfp_unfold[OF mono_ef]
4.117 apply(subst lfp_unfold[OF mono_ef])
4.118 @@ -110,10 +136,10 @@
4.119 apply(blast)
4.120 done
4.121
4.122 -theorem "mc f = {s. s \<Turnstile> f}";
4.123 -apply(induct_tac f);
4.124 -apply(auto simp add: EF_lemma);
4.125 -done;
4.126 +theorem "mc f = {s. s \<Turnstile> f}"
4.127 +apply(induct_tac f)
4.128 +apply(auto simp add: EF_lemma)
4.129 +done
4.130
4.131 text{*
4.132 \begin{exercise}
5.1 --- a/doc-src/TutorialI/Overview/document/root.tex Wed Jun 26 10:26:46 2002 +0200
5.2 +++ b/doc-src/TutorialI/Overview/document/root.tex Wed Jun 26 11:07:14 2002 +0200
5.3 @@ -39,7 +39,7 @@
5.4
5.5 \input{Ind.tex}
5.6
5.7 -\input{Isar.tex}
5.8 +%\input{Isar.tex}
5.9
5.10 %%% Local Variables:
5.11 %%% mode: latex