# 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 \ 'a list \ 'a list" (infixr "@" 65) + rev :: "'a list \ '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 \ rev ys" +by auto + +lemma "case xs of + [] \ tl xs = xs + | y#ys \ tl xs \ xs" +apply(case_tac xs) +by auto + + +subsection{*More Types*} + + +subsubsection{*Natural Numbers*} + +consts sum :: "nat \ 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 "\ \ m < n; m < n+1 \ \ m = n" +by(auto) + +lemma "min i (max j k) = max (min k i) (min i (j::nat))"; +by(arith) + +lemma "n*n = n \ n=0 \ n=1" +oops + + +subsubsection{*Pairs*} + +lemma "fst(x,y) = snd(z,x)" +by auto + + + +subsection{*Definitions*} + +consts xor :: "bool \ bool \ bool" +defs xor_def: "xor x y \ x \ \y \ \x \ y" + +constdefs nand :: "bool \ bool \ bool" + "nand x y \ \(x \ y)" + +lemma "\ 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 "\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 "\ xs @ zs = ys @ xs; [] @ xs = [] @ [] \ \ ys = zs"; +apply simp; +done + +lemma "\x. f x = g (f (g x)) \ f [] = f [] @ []"; +apply(simp (no_asm)); +done + + +subsubsection{*Rewriting with Definitions*} + +lemma "xor A (\A)"; +apply(simp only:xor_def); +by simp + + +subsubsection{*Conditional Equations*} + +lemma hd_Cons_tl[simp]: "xs \ [] \ hd xs # tl xs = xs" +apply(case_tac xs, simp, simp) +done + +lemma "xs \ [] \ hd(rev xs) # tl(rev xs) = rev xs" +by(simp) + + +subsubsection{*Automatic Case Splits*} + +lemma "\xs. if xs = [] then A else B"; +apply simp +oops + +lemma "case xs @ [] of [] \ A | y#ys \ B"; +apply simp +apply(simp split: list.split) +oops + + +subsubsection{*Arithmetic*} + +lemma "\ \ m < n; m < n+1 \ \ m = n" +by simp + +lemma "\ m < n \ m < n+1 \ 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 \ 'v \ 'v"; + +datatype ('a,'v)expr = Cex 'v + | Vex 'a + | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"; + +consts value :: "('a,'v)expr \ ('a \ 'v) \ '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 \ ('a\'v) \ 'v list \ 'v list"; +primrec +"exec [] s vs = vs" +"exec (i#is) s vs = (case i of + Const v \ exec is s (v#vs) + | Load a \ exec is s ((s a)#vs) + | Apply f \ exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"; + + +subsubsection{*The Compiler*} + +consts comp :: "('a,'v)expr \ ('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 "\vs. exec (comp e) s vs = (value e s) # vs"; +oops + +lemma exec_app[simp]: + "\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 "\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 \ ('a \ nat) \ nat" + evalb :: "'a bexp \ ('a \ nat) \ 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 \ evalb b2 env)" + "evalb (Neg b) env = (\ evalb b env)" + +consts substa :: "('a \ 'b aexp) \ 'a aexp \ 'b aexp" + substb :: "('a \ 'b aexp) \ 'a bexp \ '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 (\x. evala (s x) env) \ + evalb (substb s b) env = evalb b (\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 \ tree" +mirrors:: "tree list \ tree list"; + +primrec + "mirror(C ts) = C(mirrors ts)" + + "mirrors [] = []" + "mirrors (t # ts) = mirrors ts @ [mirror t]" + +lemma "mirror(mirror t) = t \ 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 \ ('a,'i)bigtree" + +term "Br 0 (\i. Br i (\n. Tip))" + +consts map_bt :: "('a \ 'b) \ ('a,'i)bigtree \ ('b,'i)bigtree" +primrec +"map_bt f Tip = Tip" +"map_bt f (Br a F) = Br (f a) (\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 \ 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 \ even" +step[intro!]: "n \ even \ Suc(Suc n) \ even" + +lemma [simp,intro!]: "2 dvd n \ 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 \ even \ 2 dvd n" +apply (erule even.induct) +apply simp_all +done + +subsubsection{*Rule Inversion*} + +inductive_cases Suc_Suc_case [elim!]: "Suc(Suc n) \ even" +thm Suc_Suc_case + +lemma "Suc(Suc n) \ even \ n \ even" +by blast + + +subsection{*Mutually Inductive Definitions*} + +consts evn :: "nat set" + odd :: "nat set" + +inductive evn odd +intros +zero: "0 \ evn" +evnI: "n \ odd \ Suc n \ evn" +oddI: "n \ evn \ Suc n \ odd" + +lemma "(m \ evn \ 2 dvd m) \ (n \ odd \ 2 dvd (Suc n))" +apply(rule evn_odd.induct) +by simp_all + + +subsection{*The Reflexive Transitive Closure*} + +consts rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) +inductive "r*" +intros +rtc_refl[iff]: "(x,x) \ r*" +rtc_step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" + +lemma [intro]: "(x,y) : r \ (x,y) \ r*" +by(blast intro: rtc_step); + +lemma rtc_trans: "\ (x,y) \ r*; (y,z) \ r* \ \ (x,z) \ r*" +apply(erule rtc.induct) +oops + +lemma rtc_trans[rule_format]: + "(x,y) \ r* \ (y,z) \ r* \ (x,z) \ 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 \ 'a) set \ 'a set" +inductive "acc r" +intros + "(\y. (x,y) \ r \ y \ acc r) \ x \ acc r" + + +consts + accs :: "('a \ 'a) set \ 'a set" +inductive "accs r" +intros + "r``{x} \ Pow(accs r) \ x \ 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 \ x \ f (lfp f) \ x \ lfp f" + by(simp only: lfp_unfold [symmetric]) + +lemma "lfp(\T. A \ M\ `` T) = {s. \t. (s,t) \ M\<^sup>* \ t \ A}" + (is "lfp ?F = ?toA") +proof + show "lfp ?F \ ?toA" + by (blast intro!: lfp_lowerbound intro:rtrancl_trans) + + show "?toA \ lfp ?F" + proof + fix s assume "s \ ?toA" + then obtain t where stM: "(s,t) \ M\<^sup>*" and tA: "t \ A" by blast + from stM show "s \ lfp ?F" + proof (rule converse_rtrancl_induct) + from tA have "t \ ?F (lfp ?F)" by blast + with mono_ef show "t \ lfp ?F" .. + fix s s' assume "(s,s') \ M" and "(s',t) \ M\<^sup>*" and "s' \ lfp ?F" + then have "s \ ?F (lfp ?F)" by blast + with mono_ef show "s \ 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 \ nat"; +recdef fib "measure(\n. n)" + "fib 0 = 0" + "fib 1 = 1" + "fib (Suc(Suc x)) = fib x + fib (Suc x)"; + +consts sep :: "'a \ 'a list \ 'a list"; +recdef sep "measure (\(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 \ 'a"; +recdef last "measure (\xs. length xs)" + "last [x] = x" + "last (x#y#zs) = last (y#zs)"; + + +consts sep1 :: "'a \ 'a list \ 'a list"; +recdef sep1 "measure (\(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 \ 'a list"; +recdef swap12 "{}" + "swap12 (x#y#zs) = y#x#zs" + "swap12 zs = zs"; + + +subsubsection{*Beyond Measure*} + +consts ack :: "nat\nat \ nat"; +recdef ack "measure(\m. m) <*lex*> measure(\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 \ set ts \ size t < Suc(tree_list_size ts)" +by(induct_tac ts, auto) + +consts mirror :: "tree \ 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 \ B \ A \ (B \ 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 \ 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 \ Q \ Q \ 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 "\x.\y. P x y \ \y.\x. P x y" +oops + +subsection{*Instantiation*} + +lemma "\xs. xs @ xs = xs" +apply(rule_tac x = "[]" in exI) +by simp + +lemma "\xs. f(xs @ xs) = xs \ f [] = []" +apply(erule_tac x = "[]" in allE) +by simp + + +subsection{*Hilbert's epsilon Operator*} + +theorem axiom_of_choice: + "\x. \y. P x y \ \f. \x. P x (f x)" +by (fast elim!: someI) + + +subsection{*Automation*} + +lemma "(\x. honest(x) \ industrious(x) \ healthy(x)) \ + \ (\x. grocer(x) \ healthy(x)) \ + (\x. industrious(x) \ grocer(x) \ honest(x)) \ + (\x. cyclist(x) \ industrious(x)) \ + (\x. \healthy(x) \ cyclist(x) \ \honest(x)) + \ (\x. grocer(x) \ \cyclist(x))"; +by blast + +lemma "(\i\I. A(i)) \ (\j\J. B(j)) = + (\i\I. \j\J. A(i) \ B(j))" +by fast + +lemma "\x.\y. P x y \ \y.\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 \ 1 \ n \ 0 \ n^n = n" +apply(subgoal_tac "n=1") + apply simp +apply arith +done + + +lemma "\ 2 \ Q; sqrt 2 \ Q; + \x y z. sqrt x * sqrt x = x \ + x ^ 2 = x * x \ + (x ^ y) ^ z = x ^ (y*z) + \ \ \a b. a \ Q \ b \ Q \ a ^ b \ 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 \ B" +term "A \ B" +term "A - B" +term "a \ A" +term "b \ A" +term "{a,b}" +term "{x. P x}" +term "{x+y+eps |x y. x < y}" +term "\ M" +term "\a \ 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 \ state)set"; + +typedecl atom + +consts L :: "state \ atom set" + +datatype formula = Atom atom + | Neg formula + | And formula formula + | AX formula + | EF formula + +consts valid :: "state \ formula \ bool" ("(_ \ _)" [80,80] 80) + +primrec +"s \ Atom a = (a \ L s)" +"s \ Neg f = (\(s \ f))" +"s \ And f g = (s \ f \ s \ g)" +"s \ AX f = (\t. (s,t) \ M \ t \ f)" +"s \ EF f = (\t. (s,t) \ M\<^sup>* \ t \ f)"; + +consts mc :: "formula \ state set"; +primrec +"mc(Atom a) = {s. a \ L s}" +"mc(Neg f) = -mc f" +"mc(And f g) = mc f \ mc g" +"mc(AX f) = {s. \t. (s,t) \ M \ t \ mc f}" +"mc(EF f) = lfp(\T. mc f \ (M\ `` T))" + +lemma mono_ef: "mono(\T. A \ (M\ `` T))" +apply(rule monoI) +apply blast +done + +lemma EF_lemma: + "lfp(\T. A \ (M\ `` T)) = {s. \t. (s,t) \ M\<^sup>* \ t \ 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 \ 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"\"}} +(``there exists a next state such that'') with the intended semantics +@{prop[display]"(s \ EN f) = (EX t. (s,t) : M & t \ 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 \ EF f) = (s \ f | s \ 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 ==============================================