--- a/doc-src/TutorialI/Overview/LNCS/FP1.thy Thu Jul 31 00:01:47 2003 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP1.thy Thu Jul 31 14:01:04 2003 +0200
@@ -1,5 +1,13 @@
(*<*)theory FP1 = Main:(*>*)
+subsection{*Quickcheck*}
+
+lemma "rev(xs @ ys) = rev xs @ rev ys"
+quickcheck
+oops
+
+subsection{*More Syntax*}
+
lemma "if xs = ys
then rev xs = rev ys
else rev xs \<noteq> rev ys"
@@ -34,6 +42,10 @@
lemma "min i (max j k) = max (min k i) (min i (j::nat))"
by(arith)
+text{*Full Presburger arithmetic:*}
+lemma "8 \<le> (n::int) \<Longrightarrow> \<exists>i j. 0\<le>i \<and> 0\<le>j \<and> n = 3*i + 5*j"
+by(arith)
+
text{*Not proved automatically because it involves multiplication:*}
lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)"
(*<*)oops(*>*)
@@ -166,13 +178,13 @@
subsubsection{*The Compiler*}
-consts comp :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list"
+consts compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list"
primrec
-"comp (Cex v) = [Const v]"
-"comp (Vex a) = [Load a]"
-"comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]"
+"compile (Cex v) = [Const v]"
+"compile (Vex a) = [Load a]"
+"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"
-theorem "exec (comp e) s [] = [value e s]"
+theorem "exec (compile e) s [] = [value e s]"
(*<*)oops(*>*)
@@ -228,18 +240,18 @@
subsubsection{*Nested Recursion*}
-datatype tree = C "tree list"
+datatype tree = Tree "tree list"
text{*Some trees:*}
-term "C []"
-term "C [C [C []], C []]"
+term "Tree []"
+term "Tree [Tree [Tree []], Tree []]"
consts
mirror :: "tree \<Rightarrow> tree"
mirrors:: "tree list \<Rightarrow> tree list"
primrec
- "mirror(C ts) = C(mirrors ts)"
+ "mirror(Tree ts) = Tree(mirrors ts)"
"mirrors [] = []"
"mirrors (t # ts) = mirrors ts @ [mirror t]"
@@ -272,13 +284,48 @@
apply simp_all
done
+text{*The ordinals:*}
+datatype ord = Zero | Succ ord | Lim "nat \<Rightarrow> ord"
+
+thm ord.induct[no_vars]
+
+instance ord :: plus ..
+instance ord :: times ..
+
+primrec
+"a + Zero = a"
+"a + Succ b = Succ(a+b)"
+"a + Lim F = Lim(\<lambda>n. a + F n)"
+
+primrec
+"a * Zero = Zero"
+"a * Succ b = a*b + a"
+"a * Lim F = Lim(\<lambda>n. a * F n)"
+
+text{*An example provided by Stan Wainer:*}
+consts H :: "ord \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat)"
+primrec
+"H Zero f n = n"
+"H (Succ b) f n = H b f (f n)"
+"H (Lim F) f n = H (F n) f n"
+
+lemma [simp]: "H (a+b) f = H a f \<circ> H b f"
+apply(induct b)
+apply auto
+done
+
+lemma [simp]: "H (a*b) = H b \<circ> H a"
+apply(induct b)
+apply auto
+done
+
text{* This is \emph{not} allowed:
\begin{verbatim}
datatype lambda = C "lambda => lambda"
\end{verbatim}
\begin{exercise}
-Define a datatype of ordinals and the ordinal $\Gamma_0$.
+Define the ordinal $\Gamma_0$.
\end{exercise}
*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Overview/LNCS/Sets.thy Thu Jul 31 00:01:47 2003 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Sets.thy Thu Jul 31 14:01:04 2003 +0200
@@ -39,15 +39,12 @@
@{thm converse_def[no_vars]}\\
@{thm Image_def[no_vars]}\\
@{thm rtrancl_refl[no_vars]}\\
-@{thm rtrancl_into_rtrancl[no_vars]}\\
-@{thm trancl_def[no_vars]}
+@{thm rtrancl_into_rtrancl[no_vars]}
\end{tabular}*}
(*<*)thm Id_def
-thm converse_def[no_vars]
-thm Image_def[no_vars]
+thm converse_def[no_vars] Image_def[no_vars]
thm relpow.simps[no_vars]
-thm rtrancl.intros[no_vars]
-thm trancl_def[no_vars](*>*)
+thm rtrancl.intros[no_vars](*>*)
subsection{*Wellfoundedness*}
@@ -69,9 +66,9 @@
@{thm lfp_unfold[no_vars]}\\
@{thm lfp_induct[no_vars]}
\end{tabular}*}
-(*<*)thm lfp_def gfp_def
-thm lfp_unfold
-thm lfp_induct(*>*)
+(*<*)thm lfp_def[no_vars] gfp_def[no_vars]
+thm lfp_unfold[no_vars]
+thm lfp_induct[no_vars](*>*)
subsection{*Case Study: Verified Model Checking*}
@@ -133,6 +130,39 @@
apply(auto simp add: EF_lemma)
done
+text{*Preview of coming attractions: a structured proof of the
+@{thm[source]EF_lemma}.*}
+lemma EF_lemma:
+ "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
+ (is "lfp ?F = ?R")
+proof
+ show "lfp ?F \<subseteq> ?R"
+ proof (rule lfp_lowerbound)
+ show "?F ?R \<subseteq> ?R" by(blast intro: rtrancl_trans)
+ qed
+next
+ show "?R \<subseteq> lfp ?F"
+ proof
+ fix s assume "s \<in> ?R"
+ then obtain t where st: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" by blast
+ from st show "s \<in> lfp ?F"
+ proof (rule converse_rtrancl_induct)
+ show "t \<in> lfp ?F"
+ proof (subst lfp_unfold[OF mono_ef])
+ show "t \<in> ?F(lfp ?F)" using tA by blast
+ qed
+ next
+ fix s s'
+ assume ss': "(s,s') \<in> M" and s't: "(s',t) \<in> M\<^sup>*"
+ and IH: "s' \<in> lfp ?F"
+ show "s \<in> lfp ?F"
+ proof (subst lfp_unfold[OF mono_ef])
+ show "s \<in> ?F(lfp ?F)" using prems by blast
+ qed
+ qed
+ qed
+qed
+
text{*
\begin{exercise}
@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}