author nipkow Fri, 09 Aug 2002 11:22:18 +0200 changeset 13489 79d117a158bd parent 13488 a246d390f033 child 13490 44bdc150211b
*** empty log message ***
--- 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)