# HG changeset patch
# User nipkow
# Date 985961577 -7200
# Node ID 860c65c7388a0e3710d1a6c3dcc7d075f52aa301
# Parent  6902638af59e72edf8a4c02875f39ac5c193a838
*** empty log message ***

diff -r 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/FP0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/FP0.thy	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,37 @@
+theory FP0 = PreList:
+
+section{*Functional Programming/Modelling*}
+
+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 # [])"
+
+subsection{*An Introductory Proof*}
+
+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 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/FP1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/FP1.thy	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,306 @@
+theory FP1 = Main:
+
+subsection{*More Constructs*}
+
+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
+
+lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
+by(auto)
+
+lemma "min i (max j k) = max (min k i) (min i (j::nat))";
+by(arith)
+
+lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1"
+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
+
+declare fst_conv[simp]
+declare fst_conv[simp del]
+
+
+subsubsection{*The Simplification Method*}
+
+lemma "x*(y+1) = y*(x+1)"
+apply simp
+oops
+
+
+subsubsection{*Adding and Deleting Simplification Rules*}
+
+lemma "\<forall>x::nat. x*(y+z) = r"
+apply (simp add: add_mult_distrib2)
+oops
+
+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";
+apply simp;
+done
+
+lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
+apply(simp (no_asm));
+done
+
+
+subsubsection{*Rewriting with Definitions*}
+
+lemma "xor A (\<not>A)";
+apply(simp only:xor_def);
+by simp
+
+
+subsubsection{*Conditional Equations*}
+
+lemma hd_Cons_tl[simp]: "xs \<noteq> []  \<Longrightarrow>  hd xs # tl xs = xs"
+apply(case_tac xs, simp, simp)
+done
+
+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
+
+lemma "case xs @ [] of [] \<Rightarrow> A | y#ys \<Rightarrow> B";
+apply simp
+apply(simp split: list.split)
+oops
+
+
+subsubsection{*Arithmetic*}
+
+lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
+by simp
+
+lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
+apply simp
+by(arith)
+
+
+subsubsection{*Tracing*}
+
+ML "set trace_simp"
+lemma "rev [a] = []"
+apply(simp)
+oops
+ML "reset trace_simp"
+
+
+
+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
+
+theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
+oops
+
+lemma exec_app[simp]:
+  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
+apply(induct_tac xs)
+apply(simp)
+apply(simp split: instr.split)
+done
+
+theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
+by(induct_tac e, auto)
+
+
+
+subsection{*Advanced Datatupes*}
+
+
+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"
+
+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
+
+lemma "mirrors ts = rev(map mirror ts)"
+by(induct ts, simp_all)
+
+
+subsubsection{*Datatypes Involving Functions*}
+
+datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
+
+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
+
+(* This is NOT allowed:
+datatype lambda = C "lambda \<Rightarrow> lambda"
+*)
+
+end
diff -r 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/Ind.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/Ind.thy	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,101 @@
+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*}
+
+thm even.induct
+
+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"
+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. (x,y) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
+
+
+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 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/Isar.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/Isar.thy	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,30 @@
+theory Isar = Sets:
+
+section{*A Taste of Structured Proofs in Isar*}
+
+lemma [intro?]: "mono f \<Longrightarrow> x \<in> f (lfp f) \<Longrightarrow> x \<in> lfp f"
+  by(simp only: lfp_unfold [symmetric])
+
+lemma "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
+      (is "lfp ?F = ?toA")
+proof
+  show "lfp ?F \<subseteq> ?toA"
+  by (blast intro!: lfp_lowerbound intro:rtrancl_trans)
+
+  show "?toA \<subseteq> lfp ?F"
+  proof
+    fix s assume "s \<in> ?toA"
+    then obtain t where stM: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" by blast
+    from stM show "s \<in> lfp ?F"
+    proof (rule converse_rtrancl_induct)
+      from tA have "t \<in> ?F (lfp ?F)" by blast
+      with mono_ef show "t \<in> lfp ?F" ..
+      fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*" and "s' \<in> lfp ?F"
+      then have "s \<in> ?F (lfp ?F)" by blast
+      with mono_ef show "s \<in> lfp ?F" ..
+    qed
+  qed
+qed
+
+end
+
diff -r 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/RECDEF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/RECDEF.thy	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,78 @@
+theory RECDEF = Main:
+
+subsection{*Wellfounded Recursion*}
+
+subsubsection{*Examples*}
+
+consts fib :: "nat \<Rightarrow> nat";
+recdef fib "measure(\<lambda>n. n)"
+  "fib 0 = 0"
+  "fib 1 = 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";
+
+thm sep1.simps
+
+
+consts swap12 :: "'a list \<Rightarrow> 'a list";
+recdef swap12 "{}"
+  "swap12 (x#y#zs) = y#x#zs"
+  "swap12 zs       = zs";
+
+
+subsubsection{*Beyond Measure*}
+
+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*}
+
+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
+
+end
diff -r 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/ROOT.ML	Fri Mar 30 16:12:57 2001 +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 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/Rules.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/Rules.thy	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,126 @@
+theory Rules = Main:
+
+section{*The  Rules of the Game*}
+
+
+subsection{*Introduction Rules*}
+
+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*}
+
+thm impE mp
+thm conjE
+thm disjE
+
+lemma disj_swap: "P | Q \<Longrightarrow> Q | P"
+apply (erule disjE)
+ apply (rule disjI2)
+ apply assumption
+apply (rule disjI1)
+apply assumption
+done
+
+
+subsection{*Destruction Rules*}
+
+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*}
+
+
+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{*Hilbert's epsilon Operator*}
+
+theorem axiom_of_choice:
+     "\<forall>x. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
+by (fast elim!: someI)
+
+
+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*}
+
+thm rev_rev_ident
+thm rev_rev_ident[of "[]"]
+thm sym
+thm sym[OF rev_rev_ident]
+thm rev_rev_ident[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
+
+
+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 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/Sets.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/Sets.thy	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,123 @@
+theory Sets = Main:
+
+section{*Sets, Functions and Relations*}
+
+subsection{*Set Notation*}
+
+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 "{x+y+eps |x y. x < y}"
+term "\<Union> M"
+term "\<Union>a \<in> A. F a"
+
+subsection{*Functions*}
+
+thm id_def
+thm o_assoc
+thm image_Int
+thm vimage_Compl
+
+
+subsection{*Relations*}
+
+thm Id_def
+thm converse_comp
+thm Image_def
+thm relpow.simps
+thm rtrancl_idemp
+thm trancl_converse
+
+subsection{*Wellfoundedness*}
+
+thm wf_def
+thm wf_iff_no_infinite_down_chain
+
+
+subsection{*Fixed Point Operators*}
+
+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(simp, clarify)
+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 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/document/root.tex	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,20 @@
+\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{Overview}\maketitle
+
+\input{session}
+
+%\bibliographystyle{plain}
+%\bibliography{root}
+
+\end{document}
diff -r 6902638af59e -r 860c65c7388a doc-src/TutorialI/Overview/document/session.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/document/session.tex	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,18 @@
+\input{FP0.tex}
+
+\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:
diff -r 6902638af59e -r 860c65c7388a doc-src/TutorialI/OverviewMakefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/OverviewMakefile	Fri Mar 30 16:12:57 2001 +0200
@@ -0,0 +1,31 @@
+
+## targets
+
+default: Overview
+images: 
+test: Overview
+
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+USEDIR = $(ISATOOL) usedir -i true -d dvi -D document
+
+
+## Overview
+
+Overview: $(LOG)/HOL-Overview.gz
+
+$(LOG)/HOL-Overview.gz: Overview/ROOT.ML Overview/document/root.tex Overview/*.thy
+	@$(USEDIR) HOL Overview
+
+
+## clean
+
+clean:
+	@rm -f $(LOG)/HOL-Overview.gz
+
diff -r 6902638af59e -r 860c65c7388a doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Fri Mar 30 13:29:16 2001 +0200
+++ b/doc-src/TutorialI/todo.tobias	Fri Mar 30 16:12:57 2001 +0200
@@ -81,6 +81,8 @@
 
 Appendix with list functions.
 
+All theory sources on the web?
+
 
 Minor additions to the tutorial, unclear where
 ==============================================