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*}