--- a/doc-src/TutorialI/Overview/LNCS/FP1.thy Thu Aug 08 23:53:22 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP1.thy Fri Aug 09 11:22:18 2002 +0200
@@ -35,7 +35,6 @@
by(arith)
text{*Not proved automatically because it involves multiplication:*}
-
lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)"
(*<*)oops(*>*)
@@ -46,7 +45,6 @@
by auto
-
subsection{*Definitions*}
consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
@@ -92,13 +90,6 @@
apply (simp del: rev_rev_ident)
(*<*)oops(*>*)
-subsubsection{*Assumptions*}
-
-lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
-by simp
-
-lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"
-by(simp (no_asm))
subsubsection{*Rewriting with Definitions*}
@@ -110,10 +101,9 @@
subsubsection{*Conditional Equations*}
-lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
-by(case_tac xs, simp_all)
-
-lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"
+(*<*)thm hd_Cons_tl(*>*)
+text{*A pre-proved simplification rule: @{thm hd_Cons_tl[no_vars]}*}
+lemma "hd(xs @ [x]) # tl(xs @ [x]) = xs @ [x]"
by simp
@@ -121,24 +111,16 @@
lemma "\<forall>xs. if xs = [] then A else B"
apply simp
-(*<*)oops(*>*)text_raw{* \isanewline\isanewline *}
-
-lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y"
-apply simp
-apply(simp split: list.split)
(*<*)oops(*>*)
+text{*Case-expressions are only split on demand.*}
subsubsection{*Arithmetic*}
-text{*Is simple enough for the default arithmetic:*}
+text{*Only simple arithmetic:*}
lemma "\<lbrakk> \<not> m < n; m < n+(1::nat) \<rbrakk> \<Longrightarrow> m = n"
by simp
-
-text{*Contains boolean combinations and needs full arithmetic:*}
-lemma "\<not> m < n \<and> m < n+(1::nat) \<Longrightarrow> m = n"
-apply simp
-by(arith)
+text{*\noindent Complex goals need @{text arith}-method.*}
(*<*)
subsubsection{*Tracing*}
--- a/doc-src/TutorialI/Overview/LNCS/Rules.thy Thu Aug 08 23:53:22 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Rules.thy Fri Aug 09 11:22:18 2002 +0200
@@ -55,29 +55,30 @@
done
-subsection{*Destruction Rules*}
+subsection{*Negation*}
-text{* Destruction rules for propositional logic:
+text{*
\begin{center}
\begin{tabular}{ll}
-@{thm[source]conjunct1} & @{thm conjunct1[no_vars]} \\
-@{thm[source]conjunct2} & @{thm conjunct2[no_vars]} \\
-@{thm[source]iffD1} & @{thm iffD1[no_vars]} \\
-@{thm[source]iffD2} & @{thm iffD2[no_vars]}
+@{thm[source]notI} & @{thm notI[no_vars]} \\
+@{thm[source]notE} & @{thm notE[no_vars]} \\
+@{thm[source]ccontr} & @{thm ccontr[no_vars]}
\end{tabular}
\end{center}
*}
-(*<*)thm conjunct1 conjunct1 iffD1 iffD2(*>*)
+(*<*)thm notI notE ccontr(*>*)
-lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"
-apply (rule conjI)
- apply (drule conjunct2)
- apply assumption
-apply (drule conjunct1)
+lemma "\<not>\<not>P \<Longrightarrow> P"
+apply (rule ccontr)
+apply (erule notE)
apply assumption
done
+text{*A simple exercise:*}
+lemma "\<not>P \<or> \<not>Q \<Longrightarrow> \<not>(P \<and> Q)"
+(*<*)oops(*>*)
+
subsection{*Quantifiers*}
@@ -97,9 +98,11 @@
thm allE exE
thm spec
(*>*)
+text{*Another classic exercise:*}
lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
(*<*)oops(*>*)
+
subsection{*Instantiation*}
lemma "\<exists>xs. xs @ xs = xs"
--- a/doc-src/TutorialI/Overview/LNCS/Sets.thy Thu Aug 08 23:53:22 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Sets.thy Fri Aug 09 11:22:18 2002 +0200
@@ -18,6 +18,7 @@
term "{a,b}" term "{x. P x}"
term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*)
+
subsection{*Some Functions*}
text{*
@@ -29,6 +30,7 @@
\end{tabular}*}
(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)
+
subsection{*Some Relations*}
text{*
@@ -47,6 +49,7 @@
thm rtrancl.intros[no_vars]
thm trancl_def[no_vars](*>*)
+
subsection{*Wellfoundedness*}
text{*
@@ -57,6 +60,7 @@
(*<*)thm wf_def[no_vars]
thm wf_iff_no_infinite_down_chain[no_vars](*>*)
+
subsection{*Fixed Point Operators*}
text{*
@@ -69,9 +73,9 @@
thm lfp_unfold
thm lfp_induct(*>*)
+
subsection{*Case Study: Verified Model Checking*}
-
typedecl state
consts M :: "(state \<times> state)set"
@@ -81,10 +85,10 @@
consts L :: "state \<Rightarrow> atom set"
datatype formula = Atom atom
- | Neg formula
- | And formula formula
- | AX formula
- | EF formula
+ | Neg formula
+ | And formula formula
+ | AX formula
+ | EF formula
consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)