--- a/doc-src/TutorialI/Overview/FP0.thy Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-theory FP0 = PreList:
-
-datatype 'a list = Nil ("[]")
- | Cons 'a "'a list" (infixr "#" 65)
-
-consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
- rev :: "'a list \<Rightarrow> 'a list"
-
-primrec
-"[] @ ys = ys"
-"(x # xs) @ ys = x # (xs @ ys)"
-
-primrec
-"rev [] = []"
-"rev (x # xs) = (rev xs) @ (x # [])"
-
-theorem rev_rev [simp]: "rev(rev xs) = xs"
-(*<*)oops(*>*)
-
-text{*
-\begin{exercise}
-Define a datatype of binary trees and a function @{term mirror}
-that mirrors a binary tree by swapping subtrees recursively. Prove
-@{prop"mirror(mirror t) = t"}.
-
-Define a function @{term flatten} that flattens a tree into a list
-by traversing it in infix order. Prove
-@{prop"flatten(mirror t) = rev(flatten t)"}.
-\end{exercise}
-*}
-end
--- a/doc-src/TutorialI/Overview/FP1.thy Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,302 +0,0 @@
-(*<*)theory FP1 = Main:(*>*)
-
-lemma "if xs = ys
- then rev xs = rev ys
- else rev xs \<noteq> rev ys"
-by auto
-
-lemma "case xs of
- [] \<Rightarrow> tl xs = xs
- | y#ys \<Rightarrow> tl xs \<noteq> xs"
-apply(case_tac xs)
-by auto
-
-
-subsection{*More Types*}
-
-
-subsubsection{*Natural Numbers*}
-
-consts sum :: "nat \<Rightarrow> nat"
-primrec "sum 0 = 0"
- "sum (Suc n) = Suc n + sum n"
-
-lemma "sum n + sum n = n*(Suc n)"
-apply(induct_tac n)
-apply(auto)
-done
-
-text{*Some examples of linear arithmetic:*}
-
-lemma "\<lbrakk> \<not> m < n; m < n+(1::int) \<rbrakk> \<Longrightarrow> m = n"
-by(auto)
-
-lemma "min i (max j k) = max (min k i) (min i (j::nat))"
-by(arith)
-
-text{*Not proved automatically because it involves multiplication:*}
-
-lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)"
-(*<*)oops(*>*)
-
-
-subsubsection{*Pairs*}
-
-lemma "fst(x,y) = snd(z,x)"
-by auto
-
-
-
-subsection{*Definitions*}
-
-consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
-defs xor_def: "xor x y \<equiv> x \<and> \<not>y \<or> \<not>x \<and> y"
-
-constdefs nand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
- "nand x y \<equiv> \<not>(x \<and> y)"
-
-lemma "\<not> xor x x"
-apply(unfold xor_def)
-by auto
-
-
-
-subsection{*Simplification*}
-
-
-subsubsection{*Simplification Rules*}
-
-lemma fst_conv[simp]: "fst(x,y) = x"
-by auto
-
-text{*Setting and resetting the @{text simp} attribute:*}
-
-declare fst_conv[simp]
-declare fst_conv[simp del]
-
-
-subsubsection{*The Simplification Method*}
-
-lemma "x*(y+1) = y*(x+1::nat)"
-apply simp
-(*<*)oops(*>*)
-
-
-subsubsection{*Adding and Deleting Simplification Rules*}
-
-lemma "\<forall>x::nat. x*(y+z) = r"
-apply (simp add: add_mult_distrib2)
-(*<*)oops(*>*)text_raw{* \isanewline\isanewline *}
-
-lemma "rev(rev(xs @ [])) = xs"
-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*}
-
-lemma "xor A (\<not>A)"
-apply(simp only: xor_def)
-apply simp
-done
-
-
-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"
-by simp
-
-
-subsubsection{*Automatic Case Splits*}
-
-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(*>*)
-
-
-subsubsection{*Arithmetic*}
-
-text{*Is simple enough for the default 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)
-
-(*<*)
-subsubsection{*Tracing*}
-
-lemma "rev [a] = []"
-apply(simp)
-oops
-(*>*)
-
-
-subsection{*Case Study: Compiling Expressions*}
-
-
-subsubsection{*Expressions*}
-
-types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
-
-datatype ('a,'v)expr = Cex 'v
- | Vex 'a
- | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"
-
-consts value :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v"
-primrec
-"value (Cex v) env = v"
-"value (Vex a) env = env a"
-"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
-
-
-subsubsection{*The Stack Machine*}
-
-datatype ('a,'v) instr = Const 'v
- | Load 'a
- | Apply "'v binop"
-
-consts exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list"
-primrec
-"exec [] s vs = vs"
-"exec (i#is) s vs = (case i of
- Const v \<Rightarrow> exec is s (v#vs)
- | Load a \<Rightarrow> exec is s ((s a)#vs)
- | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"
-
-
-subsubsection{*The Compiler*}
-
-consts comp :: "('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]"
-
-theorem "exec (comp e) s [] = [value e s]"
-(*<*)oops(*>*)
-
-
-
-subsection{*Advanced Datatypes*}
-
-
-subsubsection{*Mutual Recursion*}
-
-datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp"
- | Sum "'a aexp" "'a aexp"
- | Var 'a
- | Num nat
-and 'a bexp = Less "'a aexp" "'a aexp"
- | And "'a bexp" "'a bexp"
- | Neg "'a bexp"
-
-
-consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
- evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
-
-primrec
- "evala (IF b a1 a2) env =
- (if evalb b env then evala a1 env else evala a2 env)"
- "evala (Sum a1 a2) env = evala a1 env + evala a2 env"
- "evala (Var v) env = env v"
- "evala (Num n) env = n"
-
- "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
- "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
- "evalb (Neg b) env = (\<not> evalb b env)"
-
-consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
- substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
-
-primrec
- "substa s (IF b a1 a2) =
- IF (substb s b) (substa s a1) (substa s a2)"
- "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
- "substa s (Var v) = s v"
- "substa s (Num n) = Num n"
-
- "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
- "substb s (And b1 b2) = And (substb s b1) (substb s b2)"
- "substb s (Neg b) = Neg (substb s b)"
-
-lemma substitution_lemma:
- "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
- evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"
-apply(induct_tac a and b)
-by simp_all
-
-
-subsubsection{*Nested Recursion*}
-
-datatype tree = C "tree list"
-
-text{*Some trees:*}
-term "C []"
-term "C [C [C []], C []]"
-
-consts
-mirror :: "tree \<Rightarrow> tree"
-mirrors:: "tree list \<Rightarrow> tree list"
-
-primrec
- "mirror(C ts) = C(mirrors ts)"
-
- "mirrors [] = []"
- "mirrors (t # ts) = mirrors ts @ [mirror t]"
-
-lemma "mirror(mirror t) = t \<and> mirrors(mirrors ts) = ts"
-apply(induct_tac t and ts)
-apply simp_all
-(*<*)oops(*>*)
-
-text{*
-\begin{exercise}
-Complete the above proof.
-\end{exercise}
-*}
-
-subsubsection{*Datatypes Involving Functions*}
-
-datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
-
-text{*A big tree:*}
-term "Br 0 (\<lambda>i. Br i (\<lambda>n. Tip))"
-
-consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
-primrec
-"map_bt f Tip = Tip"
-"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
-
-lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
-apply(induct_tac T, rename_tac[2] F)
-apply simp_all
-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$.
-\end{exercise}
-*}
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Overview/Ind.thy Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(*<*)theory Ind = Main:(*>*)
-
-section{*Inductive Definitions*}
-
-
-subsection{*Even Numbers*}
-
-subsubsection{*The Definition*}
-
-consts even :: "nat set"
-inductive even
-intros
-zero[intro!]: "0 \<in> even"
-step[intro!]: "n \<in> even \<Longrightarrow> Suc(Suc n) \<in> even"
-
-lemma [simp,intro!]: "2 dvd n \<Longrightarrow> 2 dvd Suc(Suc n)"
-apply (unfold dvd_def)
-apply clarify
-apply (rule_tac x = "Suc k" in exI, simp)
-done
-
-subsubsection{*Rule Induction*}
-
-text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
-@{thm[display] even.induct[no_vars]}*}
-(*<*)thm even.induct[no_vars](*>*)
-
-lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
-apply (erule even.induct)
-apply simp_all
-done
-
-subsubsection{*Rule Inversion*}
-
-inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even"
-text{* @{thm[display] Suc_Suc_case[no_vars]} *}
-(*<*)thm Suc_Suc_case(*>*)
-
-lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even"
-by blast
-
-
-subsection{*Mutually Inductive Definitions*}
-
-consts evn :: "nat set"
- odd :: "nat set"
-
-inductive evn odd
-intros
-zero: "0 \<in> evn"
-evnI: "n \<in> odd \<Longrightarrow> Suc n \<in> evn"
-oddI: "n \<in> evn \<Longrightarrow> Suc n \<in> odd"
-
-lemma "(m \<in> evn \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 2 dvd (Suc n))"
-apply(rule evn_odd.induct)
-by simp_all
-
-
-subsection{*The Reflexive Transitive Closure*}
-
-consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
-inductive "r*"
-intros
-rtc_refl[iff]: "(x,x) \<in> r*"
-rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
-
-lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
-by(blast intro: rtc_step);
-
-lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
-apply(erule rtc.induct)
-oops
-
-lemma rtc_trans[rule_format]:
- "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
-apply(erule rtc.induct)
- apply(blast);
-apply(blast intro: rtc_step);
-done
-
-text{*
-\begin{exercise}
-Show that the converse of @{thm[source]rtc_step} also holds:
-@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
-\end{exercise}*}
-
-subsection{*The accessible part of a relation*}
-
-consts acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
-inductive "acc r"
-intros
- "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
-
-lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}"
-thm wfI
-apply(rule_tac A = "acc r" in wfI)
- apply (blast elim: acc.elims)
-apply(simp(no_asm_use))
-thm acc.induct
-apply(erule acc.induct)
-by blast
-
-consts accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
-inductive "accs r"
-intros
- "r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r"
-monos Pow_mono
-
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Overview/Isar0.thy Mon Jul 01 12:50:35 2002 +0200
+++ b/doc-src/TutorialI/Overview/Isar0.thy Mon Jul 01 15:33:03 2002 +0200
@@ -305,4 +305,22 @@
theorem "EX S. S ~: range (f :: 'a => 'a set)"
by best
+(* Finally, whole scripts may appear in the leaves of the proof tree,
+although this is best avoided. Here is a contrived example. *)
+
+lemma "A \<longrightarrow> (A \<longrightarrow>B) \<longrightarrow> B"
+proof
+ assume A: A
+ show "(A \<longrightarrow>B) \<longrightarrow> B"
+ apply(rule impI)
+ apply(erule impE)
+ apply(rule A)
+ apply assumption
+ done
+qed
+
+
+(* You may need to resort to this technique if an automatic step fails to
+prove the desired proposition. *)
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/FP0.thy Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,31 @@
+theory FP0 = PreList:
+
+datatype 'a list = Nil ("[]")
+ | Cons 'a "'a list" (infixr "#" 65)
+
+consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
+ rev :: "'a list \<Rightarrow> 'a list"
+
+primrec
+"[] @ ys = ys"
+"(x # xs) @ ys = x # (xs @ ys)"
+
+primrec
+"rev [] = []"
+"rev (x # xs) = (rev xs) @ (x # [])"
+
+theorem rev_rev [simp]: "rev(rev xs) = xs"
+(*<*)oops(*>*)
+
+text{*
+\begin{exercise}
+Define a datatype of binary trees and a function @{term mirror}
+that mirrors a binary tree by swapping subtrees recursively. Prove
+@{prop"mirror(mirror t) = t"}.
+
+Define a function @{term flatten} that flattens a tree into a list
+by traversing it in infix order. Prove
+@{prop"flatten(mirror t) = rev(flatten t)"}.
+\end{exercise}
+*}
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/FP1.thy Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,302 @@
+(*<*)theory FP1 = Main:(*>*)
+
+lemma "if xs = ys
+ then rev xs = rev ys
+ else rev xs \<noteq> rev ys"
+by auto
+
+lemma "case xs of
+ [] \<Rightarrow> tl xs = xs
+ | y#ys \<Rightarrow> tl xs \<noteq> xs"
+apply(case_tac xs)
+by auto
+
+
+subsection{*More Types*}
+
+
+subsubsection{*Natural Numbers*}
+
+consts sum :: "nat \<Rightarrow> nat"
+primrec "sum 0 = 0"
+ "sum (Suc n) = Suc n + sum n"
+
+lemma "sum n + sum n = n*(Suc n)"
+apply(induct_tac n)
+apply(auto)
+done
+
+text{*Some examples of linear arithmetic:*}
+
+lemma "\<lbrakk> \<not> m < n; m < n+(1::int) \<rbrakk> \<Longrightarrow> m = n"
+by(auto)
+
+lemma "min i (max j k) = max (min k i) (min i (j::nat))"
+by(arith)
+
+text{*Not proved automatically because it involves multiplication:*}
+
+lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)"
+(*<*)oops(*>*)
+
+
+subsubsection{*Pairs*}
+
+lemma "fst(x,y) = snd(z,x)"
+by auto
+
+
+
+subsection{*Definitions*}
+
+consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+defs xor_def: "xor x y \<equiv> x \<and> \<not>y \<or> \<not>x \<and> y"
+
+constdefs nand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+ "nand x y \<equiv> \<not>(x \<and> y)"
+
+lemma "\<not> xor x x"
+apply(unfold xor_def)
+by auto
+
+
+
+subsection{*Simplification*}
+
+
+subsubsection{*Simplification Rules*}
+
+lemma fst_conv[simp]: "fst(x,y) = x"
+by auto
+
+text{*Setting and resetting the @{text simp} attribute:*}
+
+declare fst_conv[simp]
+declare fst_conv[simp del]
+
+
+subsubsection{*The Simplification Method*}
+
+lemma "x*(y+1) = y*(x+1::nat)"
+apply simp
+(*<*)oops(*>*)
+
+
+subsubsection{*Adding and Deleting Simplification Rules*}
+
+lemma "\<forall>x::nat. x*(y+z) = r"
+apply (simp add: add_mult_distrib2)
+(*<*)oops(*>*)text_raw{* \isanewline\isanewline *}
+
+lemma "rev(rev(xs @ [])) = xs"
+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*}
+
+lemma "xor A (\<not>A)"
+apply(simp only: xor_def)
+apply simp
+done
+
+
+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"
+by simp
+
+
+subsubsection{*Automatic Case Splits*}
+
+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(*>*)
+
+
+subsubsection{*Arithmetic*}
+
+text{*Is simple enough for the default 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)
+
+(*<*)
+subsubsection{*Tracing*}
+
+lemma "rev [a] = []"
+apply(simp)
+oops
+(*>*)
+
+
+subsection{*Case Study: Compiling Expressions*}
+
+
+subsubsection{*Expressions*}
+
+types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
+
+datatype ('a,'v)expr = Cex 'v
+ | Vex 'a
+ | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"
+
+consts value :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v"
+primrec
+"value (Cex v) env = v"
+"value (Vex a) env = env a"
+"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
+
+
+subsubsection{*The Stack Machine*}
+
+datatype ('a,'v) instr = Const 'v
+ | Load 'a
+ | Apply "'v binop"
+
+consts exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list"
+primrec
+"exec [] s vs = vs"
+"exec (i#is) s vs = (case i of
+ Const v \<Rightarrow> exec is s (v#vs)
+ | Load a \<Rightarrow> exec is s ((s a)#vs)
+ | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"
+
+
+subsubsection{*The Compiler*}
+
+consts comp :: "('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]"
+
+theorem "exec (comp e) s [] = [value e s]"
+(*<*)oops(*>*)
+
+
+
+subsection{*Advanced Datatypes*}
+
+
+subsubsection{*Mutual Recursion*}
+
+datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp"
+ | Sum "'a aexp" "'a aexp"
+ | Var 'a
+ | Num nat
+and 'a bexp = Less "'a aexp" "'a aexp"
+ | And "'a bexp" "'a bexp"
+ | Neg "'a bexp"
+
+
+consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
+ evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
+
+primrec
+ "evala (IF b a1 a2) env =
+ (if evalb b env then evala a1 env else evala a2 env)"
+ "evala (Sum a1 a2) env = evala a1 env + evala a2 env"
+ "evala (Var v) env = env v"
+ "evala (Num n) env = n"
+
+ "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
+ "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
+ "evalb (Neg b) env = (\<not> evalb b env)"
+
+consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
+ substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
+
+primrec
+ "substa s (IF b a1 a2) =
+ IF (substb s b) (substa s a1) (substa s a2)"
+ "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
+ "substa s (Var v) = s v"
+ "substa s (Num n) = Num n"
+
+ "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
+ "substb s (And b1 b2) = And (substb s b1) (substb s b2)"
+ "substb s (Neg b) = Neg (substb s b)"
+
+lemma substitution_lemma:
+ "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
+ evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"
+apply(induct_tac a and b)
+by simp_all
+
+
+subsubsection{*Nested Recursion*}
+
+datatype tree = C "tree list"
+
+text{*Some trees:*}
+term "C []"
+term "C [C [C []], C []]"
+
+consts
+mirror :: "tree \<Rightarrow> tree"
+mirrors:: "tree list \<Rightarrow> tree list"
+
+primrec
+ "mirror(C ts) = C(mirrors ts)"
+
+ "mirrors [] = []"
+ "mirrors (t # ts) = mirrors ts @ [mirror t]"
+
+lemma "mirror(mirror t) = t \<and> mirrors(mirrors ts) = ts"
+apply(induct_tac t and ts)
+apply simp_all
+(*<*)oops(*>*)
+
+text{*
+\begin{exercise}
+Complete the above proof.
+\end{exercise}
+*}
+
+subsubsection{*Datatypes Involving Functions*}
+
+datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
+
+text{*A big tree:*}
+term "Br 0 (\<lambda>i. Br i (\<lambda>n. Tip))"
+
+consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
+primrec
+"map_bt f Tip = Tip"
+"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
+
+lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
+apply(induct_tac T, rename_tac[2] F)
+apply simp_all
+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$.
+\end{exercise}
+*}
+(*<*)end(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,109 @@
+(*<*)theory Ind = Main:(*>*)
+
+section{*Inductive Definitions*}
+
+
+subsection{*Even Numbers*}
+
+subsubsection{*The Definition*}
+
+consts even :: "nat set"
+inductive even
+intros
+zero[intro!]: "0 \<in> even"
+step[intro!]: "n \<in> even \<Longrightarrow> Suc(Suc n) \<in> even"
+
+lemma [simp,intro!]: "2 dvd n \<Longrightarrow> 2 dvd Suc(Suc n)"
+apply (unfold dvd_def)
+apply clarify
+apply (rule_tac x = "Suc k" in exI, simp)
+done
+
+subsubsection{*Rule Induction*}
+
+text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
+@{thm[display] even.induct[no_vars]}*}
+(*<*)thm even.induct[no_vars](*>*)
+
+lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
+apply (erule even.induct)
+apply simp_all
+done
+
+subsubsection{*Rule Inversion*}
+
+inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \<in> even"
+text{* @{thm[display] Suc_Suc_case[no_vars]} *}
+(*<*)thm Suc_Suc_case(*>*)
+
+lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even"
+by blast
+
+
+subsection{*Mutually Inductive Definitions*}
+
+consts evn :: "nat set"
+ odd :: "nat set"
+
+inductive evn odd
+intros
+zero: "0 \<in> evn"
+evnI: "n \<in> odd \<Longrightarrow> Suc n \<in> evn"
+oddI: "n \<in> evn \<Longrightarrow> Suc n \<in> odd"
+
+lemma "(m \<in> evn \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 2 dvd (Suc n))"
+apply(rule evn_odd.induct)
+by simp_all
+
+
+subsection{*The Reflexive Transitive Closure*}
+
+consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
+inductive "r*"
+intros
+rtc_refl[iff]: "(x,x) \<in> r*"
+rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+
+lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
+by(blast intro: rtc_step);
+
+lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+apply(erule rtc.induct)
+oops
+
+lemma rtc_trans[rule_format]:
+ "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
+apply(erule rtc.induct)
+ apply(blast);
+apply(blast intro: rtc_step);
+done
+
+text{*
+\begin{exercise}
+Show that the converse of @{thm[source]rtc_step} also holds:
+@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
+\end{exercise}*}
+
+subsection{*The accessible part of a relation*}
+
+consts acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
+inductive "acc r"
+intros
+ "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
+
+lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}"
+thm wfI
+apply(rule_tac A = "acc r" in wfI)
+ apply (blast elim: acc.elims)
+apply(simp(no_asm_use))
+thm acc.induct
+apply(erule acc.induct)
+by blast
+
+consts accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
+inductive "accs r"
+intros
+ "r``{x} \<in> Pow(accs r) \<Longrightarrow> x \<in> accs r"
+monos Pow_mono
+
+(*<*)end(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/Ordinal.thy Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,52 @@
+theory Ordinal = Main:
+
+datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"
+
+consts
+ pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option"
+primrec
+ "pred Zero n = None"
+ "pred (Succ a) n = Some a"
+ "pred (Limit f) n = Some (f n)"
+
+constdefs
+ OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+ "OpLim F a \<equiv> Limit (\<lambda>n. F n a)"
+ OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>")
+ "\<Squnion>f \<equiv> OpLim (power f)"
+
+consts
+ cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
+primrec
+ "cantor a Zero = Succ a"
+ "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
+ "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
+
+consts
+ Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<nabla>")
+primrec
+ "\<nabla>f Zero = f Zero"
+ "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
+ "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
+
+constdefs
+ deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+ "deriv f \<equiv> \<nabla>(\<Squnion>f)"
+
+consts
+ veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
+primrec
+ "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))"
+ "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
+ "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
+
+constdefs
+ veb :: "ordinal \<Rightarrow> ordinal"
+ "veb a \<equiv> veblen a Zero"
+ epsilon0 :: ordinal ("\<epsilon>\<^sub>0")
+ "\<epsilon>\<^sub>0 \<equiv> veb Zero"
+ Gamma0 :: ordinal ("\<Gamma>\<^sub>0")
+ "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
+thm Gamma0_def
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/RECDEF.thy Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,109 @@
+(*<*)
+theory RECDEF = Main:
+(*>*)
+
+subsection{*Wellfounded Recursion*}
+
+subsubsection{*Examples*}
+
+consts fib :: "nat \<Rightarrow> nat";
+recdef fib "measure(\<lambda>n. n)"
+ "fib 0 = 0"
+ "fib (Suc 0) = 1"
+ "fib (Suc(Suc x)) = fib x + fib (Suc x)";
+
+consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
+recdef sep "measure (\<lambda>(a,xs). length xs)"
+ "sep(a, []) = []"
+ "sep(a, [x]) = [x]"
+ "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
+
+consts last :: "'a list \<Rightarrow> 'a";
+recdef last "measure (\<lambda>xs. length xs)"
+ "last [x] = x"
+ "last (x#y#zs) = last (y#zs)";
+
+consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
+recdef sep1 "measure (\<lambda>(a,xs). length xs)"
+ "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
+ "sep1(a, xs) = xs";
+
+text{*
+This is what the rules for @{term sep1} are turned into:
+@{thm[display,indent=5] sep1.simps[no_vars]}
+*}
+(*<*)
+thm sep1.simps
+(*>*)
+
+text{*
+Pattern matching is also useful for nonrecursive functions:
+*}
+
+consts swap12 :: "'a list \<Rightarrow> 'a list";
+recdef swap12 "{}"
+ "swap12 (x#y#zs) = y#x#zs"
+ "swap12 zs = zs";
+
+
+subsubsection{*Beyond Measure*}
+
+text{*
+The lexicographic product of two relations:
+*}
+
+consts ack :: "nat\<times>nat \<Rightarrow> nat";
+recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
+ "ack(0,n) = Suc n"
+ "ack(Suc m,0) = ack(m, 1)"
+ "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
+
+
+subsubsection{*Induction*}
+
+text{*
+Every recursive definition provides an induction theorem, for example
+@{thm[source]sep.induct}:
+@{thm[display,margin=70] sep.induct[no_vars]}
+*}
+(*<*)thm sep.induct[no_vars](*>*)
+
+lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
+apply(induct_tac x xs rule: sep.induct)
+apply simp_all
+done
+
+lemma ack_incr2: "n < ack(m,n)"
+apply(induct_tac m n rule: ack.induct)
+apply simp_all
+done
+
+
+subsubsection{*Recursion Over Nested Datatypes*}
+
+datatype tree = C "tree list"
+
+lemma termi_lem: "t \<in> set ts \<longrightarrow> size t < Suc(tree_list_size ts)"
+by(induct_tac ts, auto)
+
+consts mirror :: "tree \<Rightarrow> tree"
+recdef mirror "measure size"
+ "mirror(C ts) = C(rev(map mirror ts))"
+(hints recdef_simp: termi_lem)
+
+lemma "mirror(mirror t) = t"
+apply(induct_tac t rule: mirror.induct)
+apply(simp add: rev_map sym[OF map_compose] cong: map_cong)
+done
+
+text{*
+Figure out how that proof worked!
+
+\begin{exercise}
+Define a function for merging two ordered lists (of natural numbers) and
+show that if the two input lists are ordered, so is the output.
+\end{exercise}
+*}
+(*<*)
+end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/ROOT.ML Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,7 @@
+use_thy "FP0";
+use_thy "FP1";
+use_thy "RECDEF";
+use_thy "Rules";
+use_thy "Sets";
+use_thy "Ind";
+use_thy "Isar";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/Rules.thy Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,184 @@
+(*<*)theory Rules = Main:(*>*)
+
+section{*The Rules of the Game*}
+
+
+subsection{*Introduction Rules*}
+
+text{* Introduction rules for propositional logic:
+\begin{center}
+\begin{tabular}{ll}
+@{thm[source]impI} & @{thm impI[no_vars]} \\
+@{thm[source]conjI} & @{thm conjI[no_vars]} \\
+@{thm[source]disjI1} & @{thm disjI1[no_vars]} \\
+@{thm[source]disjI2} & @{thm disjI2[no_vars]} \\
+@{thm[source]iffI} & @{thm iffI[no_vars]}
+\end{tabular}
+\end{center}
+*}
+
+(*<*)thm impI conjI disjI1 disjI2 iffI(*>*)
+
+lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)"
+apply(rule impI)
+apply(rule conjI)
+ apply assumption
+apply(rule conjI)
+ apply assumption
+apply assumption
+done
+
+
+subsection{*Elimination Rules*}
+
+text{* Elimination rules for propositional logic:
+\begin{center}
+\begin{tabular}{ll}
+@{thm[source]impE} & @{thm impE[no_vars]} \\
+@{thm[source]mp} & @{thm mp[no_vars]} \\
+@{thm[source]conjE} & @{thm conjE[no_vars]} \\
+@{thm[source]disjE} & @{thm disjE[no_vars]}
+\end{tabular}
+\end{center}
+*}
+(*<*)
+thm impE mp
+thm conjE
+thm disjE
+(*>*)
+lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
+apply (erule disjE)
+ apply (rule disjI2)
+ apply assumption
+apply (rule disjI1)
+apply assumption
+done
+
+
+subsection{*Destruction Rules*}
+
+text{* Destruction rules for propositional logic:
+\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]}
+\end{tabular}
+\end{center}
+*}
+
+(*<*)thm conjunct1 conjunct1 iffD1 iffD2(*>*)
+
+lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"
+apply (rule conjI)
+ apply (drule conjunct2)
+ apply assumption
+apply (drule conjunct1)
+apply assumption
+done
+
+
+subsection{*Quantifiers*}
+
+text{* Quantifier rules:
+\begin{center}
+\begin{tabular}{ll}
+@{thm[source]allI} & @{thm allI[no_vars]} \\
+@{thm[source]exI} & @{thm exI[no_vars]} \\
+@{thm[source]allE} & @{thm allE[no_vars]} \\
+@{thm[source]exE} & @{thm exE[no_vars]} \\
+@{thm[source]spec} & @{thm spec[no_vars]}
+\end{tabular}
+\end{center}
+*}
+(*<*)
+thm allI exI
+thm allE exE
+thm spec
+(*>*)
+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"
+apply(rule_tac x = "[]" in exI)
+by simp
+
+lemma "\<forall>xs. f(xs @ xs) = xs \<Longrightarrow> f [] = []"
+apply(erule_tac x = "[]" in allE)
+by simp
+
+
+subsection{*Automation*}
+
+lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>
+ \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
+ (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
+ (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
+ (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
+ \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
+by blast
+
+lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
+ (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
+by fast
+
+lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
+apply(clarify)
+by blast
+
+
+subsection{*Forward Proof*}
+
+text{*
+Instantiation of unknowns (in left-to-right order):
+\begin{center}
+\begin{tabular}{@ {}ll@ {}}
+@{thm[source]append_self_conv} & @{thm append_self_conv} \\
+@{thm[source]append_self_conv[of _ "[]"]} & @{thm append_self_conv[of _ "[]"]}
+\end{tabular}
+\end{center}
+Applying one theorem to another
+by unifying the premise of one theorem with the conclusion of another:
+\begin{center}
+\begin{tabular}{@ {}ll@ {}}
+@{thm[source]sym} & @{thm sym} \\
+@{thm[source]sym[OF append_self_conv]} & @{thm sym[OF append_self_conv]}\\
+@{thm[source]append_self_conv[THEN sym]} & @{thm append_self_conv[THEN sym]}
+\end{tabular}
+\end{center}
+*}
+(*<*)
+thm append_self_conv
+thm append_self_conv[of _ "[]"]
+thm sym
+thm sym[OF append_self_conv]
+thm append_self_conv[THEN sym]
+(*>*)
+subsection{*Further Useful Methods*}
+
+lemma "n \<le> 1 \<and> n \<noteq> 0 \<Longrightarrow> n^n = n"
+apply(subgoal_tac "n=1")
+ apply simp
+apply arith
+done
+
+text{* And a cute example: *}
+lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q;
+ \<forall>x y z. sqrt x * sqrt x = x \<and>
+ x ^ 2 = x * x \<and>
+ (x ^ y) ^ z = x ^ (y*z)
+ \<rbrakk> \<Longrightarrow> \<exists>a b. a \<notin> Q \<and> b \<notin> Q \<and> a ^ b \<in> Q"
+(*
+apply(case_tac "")
+ apply blast
+apply(rule_tac x = "" in exI)
+apply(rule_tac x = "" in exI)
+apply simp
+done
+*)
+(*<*)oops
+
+end(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/Sets.thy Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,143 @@
+(*<*)theory Sets = Main:(*>*)
+
+section{*Sets, Functions and Relations*}
+
+subsection{*Set Notation*}
+
+text{*
+\begin{center}
+\begin{tabular}{ccc}
+@{term "A \<union> B"} & @{term "A \<inter> B"} & @{term "A - B"} \\
+@{term "a \<in> A"} & @{term "b \<notin> A"} \\
+@{term "{a,b}"} & @{text "{x. P x}"} \\
+@{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"}
+\end{tabular}
+\end{center}*}
+(*<*)term "A \<union> B" term "A \<inter> B" term "A - B"
+term "a \<in> A" term "b \<notin> A"
+term "{a,b}" term "{x. P x}"
+term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*)
+
+subsection{*Some Functions*}
+
+text{*
+\begin{tabular}{l}
+@{thm id_def}\\
+@{thm o_def[no_vars]}\\
+@{thm image_def[no_vars]}\\
+@{thm vimage_def[no_vars]}
+\end{tabular}*}
+(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)
+
+subsection{*Some Relations*}
+
+text{*
+\begin{tabular}{l}
+@{thm Id_def}\\
+@{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]}
+\end{tabular}*}
+(*<*)thm Id_def
+thm converse_def[no_vars]
+thm Image_def[no_vars]
+thm relpow.simps[no_vars]
+thm rtrancl.intros[no_vars]
+thm trancl_def[no_vars](*>*)
+
+subsection{*Wellfoundedness*}
+
+text{*
+\begin{tabular}{l}
+@{thm wf_def[no_vars]}\\
+@{thm wf_iff_no_infinite_down_chain[no_vars]}
+\end{tabular}*}
+(*<*)thm wf_def[no_vars]
+thm wf_iff_no_infinite_down_chain[no_vars](*>*)
+
+subsection{*Fixed Point Operators*}
+
+text{*
+\begin{tabular}{l}
+@{thm lfp_def[no_vars]}\\
+@{thm lfp_unfold[no_vars]}\\
+@{thm lfp_induct[no_vars]}
+\end{tabular}*}
+(*<*)thm lfp_def gfp_def
+thm lfp_unfold
+thm lfp_induct(*>*)
+
+subsection{*Case Study: Verified Model Checking*}
+
+
+typedecl state
+
+consts M :: "(state \<times> state)set"
+
+typedecl atom
+
+consts L :: "state \<Rightarrow> atom set"
+
+datatype formula = Atom atom
+ | Neg formula
+ | And formula formula
+ | AX formula
+ | EF formula
+
+consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
+
+primrec
+"s \<Turnstile> Atom a = (a \<in> L s)"
+"s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))"
+"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
+"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
+"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
+
+consts mc :: "formula \<Rightarrow> state set"
+primrec
+"mc(Atom a) = {s. a \<in> L s}"
+"mc(Neg f) = -mc f"
+"mc(And f g) = mc f \<inter> mc g"
+"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
+"mc(EF f) = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))"
+
+lemma mono_ef: "mono(\<lambda>T. A \<union> (M\<inverse> `` T))"
+apply(rule monoI)
+apply blast
+done
+
+lemma EF_lemma:
+ "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
+apply(rule equalityI)
+ thm lfp_lowerbound
+ apply(rule lfp_lowerbound)
+ apply(blast intro: rtrancl_trans)
+apply(rule subsetI)
+apply clarsimp
+apply(erule converse_rtrancl_induct)
+thm lfp_unfold[OF mono_ef]
+ apply(subst lfp_unfold[OF mono_ef])
+ apply(blast)
+apply(subst lfp_unfold[OF mono_ef])
+apply(blast)
+done
+
+theorem "mc f = {s. s \<Turnstile> f}"
+apply(induct_tac f)
+apply(auto simp add: EF_lemma)
+done
+
+text{*
+\begin{exercise}
+@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
+as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
+(``there exists a next state such that'') with the intended semantics
+@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
+Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
+
+Show that the semantics for @{term EF} satisfies the following recursion equation:
+@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
+\end{exercise}*}
+(*<*)end(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/document/root.bib Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,6 @@
+@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
+@string{Springer="Springer-Verlag"}
+
+@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
+title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
+publisher=Springer,series=LNCS,volume=2283,year=2002}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/document/root.tex Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,53 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym,pdfsetup}
+
+%for best-style documents ...
+\urlstyle{rm}
+%\isabellestyle{it}
+
+\newtheorem{Exercise}{Exercise}[section]
+\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
+
+\begin{document}
+
+\title{A Compact Overview of Isabelle/HOL}
+\author{Tobias Nipkow}
+\date{}
+\maketitle
+
+\noindent
+This document is a very compact introduction to the proof assistant
+Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283}
+where full explanations and a wealth of additional material can be found.
+
+While reading this document it is recommended to single-step through the
+corresponding theories using Isabelle/HOL to follow the proofs.
+
+\section{Functional Programming/Modelling}
+
+\subsection{An Introductory Theory}
+\input{FP0.tex}
+
+\subsection{More Constructs}
+\input{FP1.tex}
+
+\input{RECDEF.tex}
+
+\input{Rules.tex}
+
+\input{Sets.tex}
+
+\input{Ind.tex}
+
+%\input{Isar.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
+
+
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/LNCS/makeDemo Mon Jul 01 15:33:03 2002 +0200
@@ -0,0 +1,34 @@
+#!/usr/bin/perl -w
+
+sub doit {
+ my ($file) = @_;
+
+ open (FILE, $file) || die $!;
+ undef $/; $text = <FILE>; $/ = "\n";
+ close FILE || die $!;
+
+ $_ = $text;
+
+ s/text_raw\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here
+ s/text\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here
+ s/\(\*<\*\)//sg;
+ s/\(\*>\*\)//sg;
+
+ $result = $_;
+
+ if ($text ne $result) {
+ print STDERR "fixing $file\n";
+# if (! -f "$file~~") {
+# rename $file, "$file~~" || die $!;
+# }
+ open (FILE, "> Demo/$file") || die $!;
+ print FILE $result;
+ close FILE || die $!;
+ }
+}
+
+
+foreach $file (@ARGV) {
+ eval { &doit($file); };
+ if ($@) { print STDERR "*** doit $file: ", $@, "\n"; }
+}
--- a/doc-src/TutorialI/Overview/Ordinal.thy Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-theory Ordinal = Main:
-
-datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"
-
-consts
- pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option"
-primrec
- "pred Zero n = None"
- "pred (Succ a) n = Some a"
- "pred (Limit f) n = Some (f n)"
-
-constdefs
- OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
- "OpLim F a \<equiv> Limit (\<lambda>n. F n a)"
- OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>")
- "\<Squnion>f \<equiv> OpLim (power f)"
-
-consts
- cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
-primrec
- "cantor a Zero = Succ a"
- "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
- "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
-
-consts
- Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<nabla>")
-primrec
- "\<nabla>f Zero = f Zero"
- "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
- "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
-
-constdefs
- deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
- "deriv f \<equiv> \<nabla>(\<Squnion>f)"
-
-consts
- veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
-primrec
- "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))"
- "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
- "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
-
-constdefs
- veb :: "ordinal \<Rightarrow> ordinal"
- "veb a \<equiv> veblen a Zero"
- epsilon0 :: ordinal ("\<epsilon>\<^sub>0")
- "\<epsilon>\<^sub>0 \<equiv> veb Zero"
- Gamma0 :: ordinal ("\<Gamma>\<^sub>0")
- "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
-thm Gamma0_def
-
-end
--- a/doc-src/TutorialI/Overview/RECDEF.thy Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(*<*)
-theory RECDEF = Main:
-(*>*)
-
-subsection{*Wellfounded Recursion*}
-
-subsubsection{*Examples*}
-
-consts fib :: "nat \<Rightarrow> nat";
-recdef fib "measure(\<lambda>n. n)"
- "fib 0 = 0"
- "fib (Suc 0) = 1"
- "fib (Suc(Suc x)) = fib x + fib (Suc x)";
-
-consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
-recdef sep "measure (\<lambda>(a,xs). length xs)"
- "sep(a, []) = []"
- "sep(a, [x]) = [x]"
- "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
-
-consts last :: "'a list \<Rightarrow> 'a";
-recdef last "measure (\<lambda>xs. length xs)"
- "last [x] = x"
- "last (x#y#zs) = last (y#zs)";
-
-consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
-recdef sep1 "measure (\<lambda>(a,xs). length xs)"
- "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
- "sep1(a, xs) = xs";
-
-text{*
-This is what the rules for @{term sep1} are turned into:
-@{thm[display,indent=5] sep1.simps[no_vars]}
-*}
-(*<*)
-thm sep1.simps
-(*>*)
-
-text{*
-Pattern matching is also useful for nonrecursive functions:
-*}
-
-consts swap12 :: "'a list \<Rightarrow> 'a list";
-recdef swap12 "{}"
- "swap12 (x#y#zs) = y#x#zs"
- "swap12 zs = zs";
-
-
-subsubsection{*Beyond Measure*}
-
-text{*
-The lexicographic product of two relations:
-*}
-
-consts ack :: "nat\<times>nat \<Rightarrow> nat";
-recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
- "ack(0,n) = Suc n"
- "ack(Suc m,0) = ack(m, 1)"
- "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
-
-
-subsubsection{*Induction*}
-
-text{*
-Every recursive definition provides an induction theorem, for example
-@{thm[source]sep.induct}:
-@{thm[display,margin=70] sep.induct[no_vars]}
-*}
-(*<*)thm sep.induct[no_vars](*>*)
-
-lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
-apply(induct_tac x xs rule: sep.induct)
-apply simp_all
-done
-
-lemma ack_incr2: "n < ack(m,n)"
-apply(induct_tac m n rule: ack.induct)
-apply simp_all
-done
-
-
-subsubsection{*Recursion Over Nested Datatypes*}
-
-datatype tree = C "tree list"
-
-lemma termi_lem: "t \<in> set ts \<longrightarrow> size t < Suc(tree_list_size ts)"
-by(induct_tac ts, auto)
-
-consts mirror :: "tree \<Rightarrow> tree"
-recdef mirror "measure size"
- "mirror(C ts) = C(rev(map mirror ts))"
-(hints recdef_simp: termi_lem)
-
-lemma "mirror(mirror t) = t"
-apply(induct_tac t rule: mirror.induct)
-apply(simp add: rev_map sym[OF map_compose] cong: map_cong)
-done
-
-text{*
-Figure out how that proof worked!
-
-\begin{exercise}
-Define a function for merging two ordered lists (of natural numbers) and
-show that if the two input lists are ordered, so is the output.
-\end{exercise}
-*}
-(*<*)
-end
-(*>*)
--- a/doc-src/TutorialI/Overview/ROOT.ML Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-use_thy "FP0";
-use_thy "FP1";
-use_thy "RECDEF";
-use_thy "Rules";
-use_thy "Sets";
-use_thy "Ind";
-use_thy "Isar";
--- a/doc-src/TutorialI/Overview/Rules.thy Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,184 +0,0 @@
-(*<*)theory Rules = Main:(*>*)
-
-section{*The Rules of the Game*}
-
-
-subsection{*Introduction Rules*}
-
-text{* Introduction rules for propositional logic:
-\begin{center}
-\begin{tabular}{ll}
-@{thm[source]impI} & @{thm impI[no_vars]} \\
-@{thm[source]conjI} & @{thm conjI[no_vars]} \\
-@{thm[source]disjI1} & @{thm disjI1[no_vars]} \\
-@{thm[source]disjI2} & @{thm disjI2[no_vars]} \\
-@{thm[source]iffI} & @{thm iffI[no_vars]}
-\end{tabular}
-\end{center}
-*}
-
-(*<*)thm impI conjI disjI1 disjI2 iffI(*>*)
-
-lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)"
-apply(rule impI)
-apply(rule conjI)
- apply assumption
-apply(rule conjI)
- apply assumption
-apply assumption
-done
-
-
-subsection{*Elimination Rules*}
-
-text{* Elimination rules for propositional logic:
-\begin{center}
-\begin{tabular}{ll}
-@{thm[source]impE} & @{thm impE[no_vars]} \\
-@{thm[source]mp} & @{thm mp[no_vars]} \\
-@{thm[source]conjE} & @{thm conjE[no_vars]} \\
-@{thm[source]disjE} & @{thm disjE[no_vars]}
-\end{tabular}
-\end{center}
-*}
-(*<*)
-thm impE mp
-thm conjE
-thm disjE
-(*>*)
-lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
-apply (erule disjE)
- apply (rule disjI2)
- apply assumption
-apply (rule disjI1)
-apply assumption
-done
-
-
-subsection{*Destruction Rules*}
-
-text{* Destruction rules for propositional logic:
-\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]}
-\end{tabular}
-\end{center}
-*}
-
-(*<*)thm conjunct1 conjunct1 iffD1 iffD2(*>*)
-
-lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"
-apply (rule conjI)
- apply (drule conjunct2)
- apply assumption
-apply (drule conjunct1)
-apply assumption
-done
-
-
-subsection{*Quantifiers*}
-
-text{* Quantifier rules:
-\begin{center}
-\begin{tabular}{ll}
-@{thm[source]allI} & @{thm allI[no_vars]} \\
-@{thm[source]exI} & @{thm exI[no_vars]} \\
-@{thm[source]allE} & @{thm allE[no_vars]} \\
-@{thm[source]exE} & @{thm exE[no_vars]} \\
-@{thm[source]spec} & @{thm spec[no_vars]}
-\end{tabular}
-\end{center}
-*}
-(*<*)
-thm allI exI
-thm allE exE
-thm spec
-(*>*)
-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"
-apply(rule_tac x = "[]" in exI)
-by simp
-
-lemma "\<forall>xs. f(xs @ xs) = xs \<Longrightarrow> f [] = []"
-apply(erule_tac x = "[]" in allE)
-by simp
-
-
-subsection{*Automation*}
-
-lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>
- \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
- (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
- (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
- (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
- \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
-by blast
-
-lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
- (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
-by fast
-
-lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
-apply(clarify)
-by blast
-
-
-subsection{*Forward Proof*}
-
-text{*
-Instantiation of unknowns (in left-to-right order):
-\begin{center}
-\begin{tabular}{@ {}ll@ {}}
-@{thm[source]append_self_conv} & @{thm append_self_conv} \\
-@{thm[source]append_self_conv[of _ "[]"]} & @{thm append_self_conv[of _ "[]"]}
-\end{tabular}
-\end{center}
-Applying one theorem to another
-by unifying the premise of one theorem with the conclusion of another:
-\begin{center}
-\begin{tabular}{@ {}ll@ {}}
-@{thm[source]sym} & @{thm sym} \\
-@{thm[source]sym[OF append_self_conv]} & @{thm sym[OF append_self_conv]}\\
-@{thm[source]append_self_conv[THEN sym]} & @{thm append_self_conv[THEN sym]}
-\end{tabular}
-\end{center}
-*}
-(*<*)
-thm append_self_conv
-thm append_self_conv[of _ "[]"]
-thm sym
-thm sym[OF append_self_conv]
-thm append_self_conv[THEN sym]
-(*>*)
-subsection{*Further Useful Methods*}
-
-lemma "n \<le> 1 \<and> n \<noteq> 0 \<Longrightarrow> n^n = n"
-apply(subgoal_tac "n=1")
- apply simp
-apply arith
-done
-
-text{* And a cute example: *}
-lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q;
- \<forall>x y z. sqrt x * sqrt x = x \<and>
- x ^ 2 = x * x \<and>
- (x ^ y) ^ z = x ^ (y*z)
- \<rbrakk> \<Longrightarrow> \<exists>a b. a \<notin> Q \<and> b \<notin> Q \<and> a ^ b \<in> Q"
-(*
-apply(case_tac "")
- apply blast
-apply(rule_tac x = "" in exI)
-apply(rule_tac x = "" in exI)
-apply simp
-done
-*)
-(*<*)oops
-
-end(*>*)
--- a/doc-src/TutorialI/Overview/Sets.thy Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,143 +0,0 @@
-(*<*)theory Sets = Main:(*>*)
-
-section{*Sets, Functions and Relations*}
-
-subsection{*Set Notation*}
-
-text{*
-\begin{center}
-\begin{tabular}{ccc}
-@{term "A \<union> B"} & @{term "A \<inter> B"} & @{term "A - B"} \\
-@{term "a \<in> A"} & @{term "b \<notin> A"} \\
-@{term "{a,b}"} & @{text "{x. P x}"} \\
-@{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"}
-\end{tabular}
-\end{center}*}
-(*<*)term "A \<union> B" term "A \<inter> B" term "A - B"
-term "a \<in> A" term "b \<notin> A"
-term "{a,b}" term "{x. P x}"
-term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*)
-
-subsection{*Some Functions*}
-
-text{*
-\begin{tabular}{l}
-@{thm id_def}\\
-@{thm o_def[no_vars]}\\
-@{thm image_def[no_vars]}\\
-@{thm vimage_def[no_vars]}
-\end{tabular}*}
-(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)
-
-subsection{*Some Relations*}
-
-text{*
-\begin{tabular}{l}
-@{thm Id_def}\\
-@{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]}
-\end{tabular}*}
-(*<*)thm Id_def
-thm converse_def[no_vars]
-thm Image_def[no_vars]
-thm relpow.simps[no_vars]
-thm rtrancl.intros[no_vars]
-thm trancl_def[no_vars](*>*)
-
-subsection{*Wellfoundedness*}
-
-text{*
-\begin{tabular}{l}
-@{thm wf_def[no_vars]}\\
-@{thm wf_iff_no_infinite_down_chain[no_vars]}
-\end{tabular}*}
-(*<*)thm wf_def[no_vars]
-thm wf_iff_no_infinite_down_chain[no_vars](*>*)
-
-subsection{*Fixed Point Operators*}
-
-text{*
-\begin{tabular}{l}
-@{thm lfp_def[no_vars]}\\
-@{thm lfp_unfold[no_vars]}\\
-@{thm lfp_induct[no_vars]}
-\end{tabular}*}
-(*<*)thm lfp_def gfp_def
-thm lfp_unfold
-thm lfp_induct(*>*)
-
-subsection{*Case Study: Verified Model Checking*}
-
-
-typedecl state
-
-consts M :: "(state \<times> state)set"
-
-typedecl atom
-
-consts L :: "state \<Rightarrow> atom set"
-
-datatype formula = Atom atom
- | Neg formula
- | And formula formula
- | AX formula
- | EF formula
-
-consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
-
-primrec
-"s \<Turnstile> Atom a = (a \<in> L s)"
-"s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))"
-"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
-"s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
-"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
-
-consts mc :: "formula \<Rightarrow> state set"
-primrec
-"mc(Atom a) = {s. a \<in> L s}"
-"mc(Neg f) = -mc f"
-"mc(And f g) = mc f \<inter> mc g"
-"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
-"mc(EF f) = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))"
-
-lemma mono_ef: "mono(\<lambda>T. A \<union> (M\<inverse> `` T))"
-apply(rule monoI)
-apply blast
-done
-
-lemma EF_lemma:
- "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
-apply(rule equalityI)
- thm lfp_lowerbound
- apply(rule lfp_lowerbound)
- apply(blast intro: rtrancl_trans)
-apply(rule subsetI)
-apply clarsimp
-apply(erule converse_rtrancl_induct)
-thm lfp_unfold[OF mono_ef]
- apply(subst lfp_unfold[OF mono_ef])
- apply(blast)
-apply(subst lfp_unfold[OF mono_ef])
-apply(blast)
-done
-
-theorem "mc f = {s. s \<Turnstile> f}"
-apply(induct_tac f)
-apply(auto simp add: EF_lemma)
-done
-
-text{*
-\begin{exercise}
-@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
-as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
-(``there exists a next state such that'') with the intended semantics
-@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
-Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
-
-Show that the semantics for @{term EF} satisfies the following recursion equation:
-@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
-\end{exercise}*}
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Overview/makeDemo Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-#!/usr/bin/perl -w
-
-sub doit {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n";
- close FILE || die $!;
-
- $_ = $text;
-
- s/text_raw\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here
- s/text\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here
- s/\(\*<\*\)//sg;
- s/\(\*>\*\)//sg;
-
- $result = $_;
-
- if ($text ne $result) {
- print STDERR "fixing $file\n";
-# if (! -f "$file~~") {
-# rename $file, "$file~~" || die $!;
-# }
- open (FILE, "> Demo/$file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-foreach $file (@ARGV) {
- eval { &doit($file); };
- if ($@) { print STDERR "*** doit $file: ", $@, "\n"; }
-}