# HG changeset patch
# User nipkow
# Date 1028884938 -7200
# Node ID 79d117a158bd8b522831da3a32c85dbe6b62cbc6
# Parent  a246d390f0330f39ab0145925f1ea51283560d3c
*** empty log message ***

diff -r a246d390f033 -r 79d117a158bd doc-src/TutorialI/Overview/LNCS/FP1.thy
--- 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*}
diff -r a246d390f033 -r 79d117a158bd doc-src/TutorialI/Overview/LNCS/Rules.thy
--- 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"
diff -r a246d390f033 -r 79d117a158bd doc-src/TutorialI/Overview/LNCS/Sets.thy
--- 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)