# HG changeset patch
# User nipkow
# Date 1025530383 -7200
# Node ID bbfc360db011a4781048a0da8e70c8fe5a0b3a56
# Parent  a0460a450cf9e5c7bf2da3c591ef29b93104aee0
*** empty log message ***

diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/FP0.thy
--- 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
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/FP1.thy
--- 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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/Ind.thy
--- 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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/Isar0.thy
--- 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
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/FP0.thy
--- /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
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/FP1.thy
--- /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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/Ind.thy
--- /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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/Ordinal.thy
--- /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
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/RECDEF.thy
--- /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
+(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/ROOT.ML
--- /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";
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/Rules.thy
--- /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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/Sets.thy
--- /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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/document/root.bib
--- /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}
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/document/root.tex
--- /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}
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/LNCS/makeDemo
--- /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"; }
+}
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/Ordinal.thy
--- 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
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/RECDEF.thy
--- 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
-(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/ROOT.ML
--- 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";
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/Rules.thy
--- 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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/Sets.thy
--- 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(*>*)
diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/makeDemo
--- 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"; }
-}