# HG changeset patch
# User nipkow
# Date 1059652864 -7200
# Node ID ca5029d391d1e7632fe0bfbd16fcc35b15dc884f
# Parent  c57ec95e7763439dd7d77265d0c04496d0a37407
*** empty log message ***

diff -r c57ec95e7763 -r ca5029d391d1 doc-src/TutorialI/Overview/LNCS/FP1.thy
--- 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(*>*)
diff -r c57ec95e7763 -r ca5029d391d1 doc-src/TutorialI/Overview/LNCS/Sets.thy
--- 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}