--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGen.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,26 @@
+CodeGen = Main +
+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) => ('a,'v)expr => 'v
+primrec
+"value env (Cex v) = v"
+"value env (Vex a) = env a"
+"value env (Bex f e1 e2) = f (value env e1) (value env e2)"
+datatype ('a,'v) instr = Const 'v
+ | Load 'a
+ | Apply ('v binop)
+consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list
+primrec
+"exec s vs [] = vs"
+"exec s vs (i#is) = (case i of
+ Const v => exec s (v#vs) is
+ | Load a => exec s ((s a)#vs) is
+ | Apply f => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"
+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]"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGenIf.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,39 @@
+Addsimps exec.rules;
+Addsimps [Let_def,drop_all];
+Addsplits [split_instr_case];
+
+Goal "!xs. wf xs --> wf(drop n xs)";
+by(induct_tac "n" 1);
+by(Simp_tac 1);
+by(Clarify_tac 1);
+by(exhaust_tac "xs" 1);
+by(Asm_simp_tac 1);
+by(Asm_full_simp_tac 1);
+qed_spec_mp "wf_drop";
+Addsimps [wf_drop];
+
+Goal "wf xs --> wf ys --> wf(xs@ys)";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [trans_le_add1]) 1);
+qed_spec_mp "wf_append";
+Addsimps [wf_append];
+
+Goal "!vs ys. wf xs --> exec(s,vs,xs@ys) = exec(s,exec(s,vs,xs),ys)";
+by(res_inst_tac [("xs","xs")] length_induct 1);
+by(exhaust_tac "xs" 1);
+by(Asm_full_simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [less_imp_diff_is_0,diff_less_Suc,le_imp_less_Suc]) 1);
+qed_spec_mp "exec_append";
+Addsimps [exec_append];
+
+Goal "wf(comp e)";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "wf_comp";
+Addsimps [wf_comp];
+
+Goal "!vs. exec(s, vs, comp e) = (value s e) # vs";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "exec_comp";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/CodeGenIf.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,46 @@
+CodeGenIf = List +
+types 'v binop = 'v => 'v => 'v
+ 'v test = 'v => bool
+datatype ('a,'v) expr = Vex 'a
+ | Cex 'v
+ | Bex ('v binop) (('a,'v) expr) (('a,'v) expr)
+ | Ifex ('v test) (('a,'v)expr) (('a,'v)expr) (('a,'v)expr)
+consts value :: ('a => 'v) => ('a,'v)expr => 'v
+primrec value expr
+"value env (Vex a) = env a"
+"value env (Cex v) = v"
+"value env (Bex f e1 e2) = f (value env e1) (value env e2)"
+"value env (Ifex t b e1 e2) =
+ (if t(value env b) then value env e1 else value env e2)"
+datatype ('a,'v) instr = Load 'a
+ | Const 'v
+ | Apply ('v binop)
+ | Jump nat
+ | Test ('v test) nat
+consts exec :: "('a => 'v) * 'v list * (('a,'v) instr) list => 'v list"
+recdef exec "measure(%(s,vs,is).length is)"
+simpset "simpset() addsimps [diff_less_Suc]"
+"exec(s, vs, []) = vs"
+"exec(s, vs, i#is) = (case i of
+ Load a => exec(s,(s a)#vs,is)
+ | Const v => exec(s,v#vs,is)
+ | Apply f => exec(s, (f (hd vs) (hd(tl vs)))#(tl(tl vs)), is)
+ | Jump n => exec(s, vs, drop n is)
+ | Test t n => (if t(hd vs) then exec(s,tl vs, drop n is)
+ else exec(s,tl vs, is)))"
+consts comp :: ('a,'v) expr => (('a,'v) instr) list
+primrec comp expr
+"comp (Vex a) = [Load a]"
+"comp (Cex v) = [Const v]"
+"comp (Bex f e1 e2) = (comp e2)@(comp e1)@[Apply f]"
+"comp (Ifex t b e1 e2) = (let is1 = comp e1; is2 = comp e2
+ in comp b @ [Test t (Suc(length is2))] @
+ is2 @ [Jump (length is1)] @ is1)"
+
+consts wf :: ('a,'v)instr list => bool
+primrec wf list
+"wf [] = True"
+"wf (i#is) = (wf is & (case i of Load a => True | Const v => True
+ | Apply f => True | Jump n => n <= length is | Test t n => n <= length is))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/Lemma.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Lemma = List
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/ROOT.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,13 @@
+use_thy"CodeGen";
+
+use"goal1.ML";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+use"simpsplit.ML";
+qed "exec_append";
+Addsimps [exec_append];
+
+use"goal2.ML";
+by(induct_tac "e" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "exec_comp";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/comp Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+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]"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/end Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/exec Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list
+primrec
+"exec s vs [] = vs"
+"exec s vs (i#is) = (case i of
+ Const v => exec s (v#vs) is
+ | Load a => exec s ((s a)#vs) is
+ | Apply f => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/expr Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+types 'v binop = 'v => 'v => 'v
+datatype ('a,'v) expr = Cex 'v
+ | Vex 'a
+ | Bex ('v binop) (('a,'v) expr) (('a,'v) expr)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/goal1.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/goal2.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!vs. exec s vs (comp e) = (value s e) # vs";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/instr Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+datatype ('a,'v) instr = Const 'v
+ | Load 'a
+ | Apply ('v binop)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/prolog Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+CodeGen = Main +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/simpsplit.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(asm_simp_tac (simpset() addsplits [instr.split]) 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/CodeGen/value Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts value :: ('a => 'v) => ('a,'v)expr => 'v
+primrec
+"value env (Cex v) = v"
+"value env (Vex a) = env a"
+"value env (Bex f e1 e2) = f (value env e1) (value env e2)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Exercise.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,17 @@
+use "normif.ML";
+use "proof.ML";
+qed_spec_mp "normif_correct";
+Addsimps [normif_correct];
+
+use "norm.ML";
+use "proof.ML";
+qed "norm_correct";
+
+Goal "!t e. normal t & normal e --> normal(normif b t e)";
+use "proof.ML";
+qed_spec_mp "normal_normif";
+Addsimps [normal_normif];
+
+use "normal_norm.ML";
+use "proof.ML";
+qed "normal_norm";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Exercise.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,25 @@
+Exercise = Main +
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
+consts valif :: ifex => (nat => bool) => bool
+primrec valif ifex
+"valif (CIF b) env = b"
+"valif (VIF x) env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+ else valif e env)"
+consts normif :: ifex => ifex => ifex => ifex
+primrec normif ifex
+"normif (CIF b) t e = (if b then t else e)"
+"normif (VIF x) t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
+consts norm :: ifex => ifex
+primrec norm ifex
+"norm (CIF b) = CIF b"
+"norm (VIF x) = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)"
+consts normal :: ifex => bool
+primrec normal ifex
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t & normal e &
+ (case b of CIF b => False | VIF x => True | IF x y z => False))"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Ifexpr.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,21 @@
+use "bool2if.ML";
+use "proof.ML";
+qed "bool2if_correct";
+
+use "normif.ML";
+use "proof.ML";
+qed_spec_mp "normif_correct";
+Addsimps [normif_correct];
+
+use "norm.ML";
+use "proof.ML";
+qed "norm_correct";
+
+use "normal_normif.ML";
+use "proof.ML";
+qed_spec_mp "normal_normif";
+Addsimps [normal_normif];
+
+use "normal_norm.ML";
+use "proof.ML";
+qed "normal_norm";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Ifexpr.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,39 @@
+Ifexpr = Main +
+datatype boolex = Const bool | Var nat
+ | Neg boolex | And boolex boolex
+consts value :: boolex => (nat => bool) => bool
+primrec
+"value (Const b) env = b"
+"value (Var x) env = env x"
+"value (Neg b) env = (~ value b env)"
+"value (And b c) env = (value b env & value c env)"
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
+consts valif :: ifex => (nat => bool) => bool
+primrec
+"valif (CIF b) env = b"
+"valif (VIF x) env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+ else valif e env)"
+consts bool2if :: boolex => ifex
+primrec
+"bool2if (Const b) = CIF b"
+"bool2if (Var x) = VIF x"
+"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"
+"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
+consts normif :: ifex => ifex => ifex => ifex
+primrec
+"normif (CIF b) t e = IF (CIF b) t e"
+"normif (VIF x) t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
+consts norm :: ifex => ifex
+primrec
+"norm (CIF b) = CIF b"
+"norm (VIF x) = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)"
+consts normal :: ifex => bool
+primrec
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t & normal e &
+ (case b of CIF b => True | VIF x => True | IF x y z => False))"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/Makefile Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+
+Ifexpr.thy: prolog boolex value ifex valif bool2if normif norm normal end
+ cat prolog boolex value ifex valif bool2if normif norm normal end > Ifexpr.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/ROOT.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+use_thy "Ifexpr";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/bool2if Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts bool2if :: boolex => ifex
+primrec
+"bool2if (Const b) = CIF b"
+"bool2if (Var x) = VIF x"
+"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"
+"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/bool2if.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "valif (bool2if b) env = value b env";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/boolex Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+datatype boolex = Const bool | Var nat
+ | Neg boolex | And boolex boolex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/end Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/ifex Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/norm Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts norm :: ifex => ifex
+primrec
+"norm (CIF b) = CIF b"
+"norm (VIF x) = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/norm.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "valif (norm b) env = valif b env";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normal Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts normal :: ifex => bool
+primrec
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t & normal e &
+ (case b of CIF b => True | VIF x => True | IF x y z => False))"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normal_norm.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "normal(norm b)";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normal_normif.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!t e. normal(normif b t e) = (normal t & normal e)";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normif Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+consts normif :: ifex => ifex => ifex => ifex
+primrec
+"normif (CIF b) t e = IF (CIF b) t e"
+"normif (VIF x) t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/normif.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!t e. valif (normif b t e) env = valif (IF b t e) env";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/prolog Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Ifexpr = Main +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/proof.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+by(induct_tac "b" 1);
+by(Auto_tac);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/valif Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts valif :: ifex => (nat => bool) => bool
+primrec
+"valif (CIF b) env = b"
+"valif (VIF x) env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+ else valif e env)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Ifexpr/value Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+consts value :: boolex => (nat => bool) => bool
+primrec
+"value (Const b) env = b"
+"value (Var x) env = env x"
+"value (Neg b) env = (~ value b env)"
+"value (And b c) env = (value b env & value c env)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Ackermann.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+Ackermann = WF_Rel +
+consts ack :: "nat * nat => nat"
+recdef ack "measure(%m. m) ** 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))"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Chain.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+Chain = List +
+consts chain :: "('a => 'a => bool) * 'a list => bool"
+recdef chain "measure (%(r,xs). length xs)"
+ "chain(r, []) = True"
+ "chain(r, [x]) = True"
+ "chain(r, x#y#zs) = (r x y & chain(r, y#zs))"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/ConstDefs.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+ConstDefs = Types +
+constdefs nand :: gate
+ "nand A B == ~(A & B)"
+ exor :: gate
+ "exor A B == A & ~B | ~A & B"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Defs.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+Defs = Types +
+consts nand, exor :: gate
+defs nand_def "nand A B == ~(A & B)"
+ exor_def "exor A B == A & ~B | ~A & B"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Exor.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+Exor = Main +
+constdefs
+ exor :: bool => bool => bool
+"exor A B == (A & ~B) | (~A & B)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Fib.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+Fib = WF_Rel +
+consts fib :: nat => nat
+recdef fib "measure(%n. n)"
+ "fib 0 = 0"
+ "fib 1 = 1"
+ "fib (Suc(Suc x)) = fib x + fib (Suc x)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/GCD.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,14 @@
+Goal "gcd(m,0) = m";
+by(resolve_tac [trans] 1);
+by(resolve_tac gcd.rules 1);
+by(Simp_tac 1);
+qed "gcd_0";
+Addsimps [gcd_0];
+
+Goal "!!n. n ~= 0 ==> gcd(m,n) = gcd(n, m mod n)";
+by(resolve_tac [trans] 1);
+by(resolve_tac gcd.rules 1);
+by(Asm_simp_tac 1);
+qed "gcd_not_0";
+Addsimps [gcd_not_0];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/GCD.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+GCD = WF_Rel +
+consts gcd :: "nat*nat => nat"
+recdef gcd "measure ((%(m,n).n))"
+ simpset "simpset() addsimps [mod_less_divisor]"
+ "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/InfixTree.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+Goal "!xs. linInfixList t xs = infixList t @ xs";
+by(induct_tac "t" 1);
+by(Simp_tac 1);
+by(Asm_simp_tac 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Itrev.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+Itrev = Main +
+consts itrev :: 'a list => 'a list => 'a list
+primrec
+"itrev [] ys = ys"
+"itrev (x#xs) ys = itrev xs (x#ys)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Itrev.thy~ Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+Itrev = Main +
+consts itrev :: 'a list => 'a list => 'a list
+primrec itrev list
+"itrev [] ys = ys"
+"itrev (x#xs) ys = itrev xs (x#ys)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Last.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+Last = List +
+consts last :: 'a list => 'a
+recdef last "measure (%xs. length xs)"
+ "last [x] = x"
+ "last (x#y#zs) = last (y#zs)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/NatSum.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+Goal "sum n + sum n = n*(Suc n)";
+by(induct_tac "n" 1);
+by(Auto_tac);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/NatSum.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+NatSum = Main +
+consts sum :: nat => nat
+primrec
+"sum 0 = 0"
+"sum (Suc n) = Suc n + sum n"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/ROOT.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,27 @@
+use_thy "Tree";
+
+context Main.thy;
+use"exhaust.ML";
+use"autotac.ML";
+result();
+
+use_thy"NatSum";
+result();
+
+use_thy"Types";
+use_thy"Defs";
+use_thy"ConstDefs";
+
+context Main.thy;
+Goal "! xs. if xs = [] then rev xs = [] else rev xs ~= []";
+use"splitif.ML";
+
+Goal "(case xs of [] => zs | y#ys => y#(ys@zs)) = xs@zs";
+use"splitlist.ML";
+
+use_thy "Itrev";
+use "itrev1.ML";
+use "itrev2.ML";
+use "itrev3.ML";
+use "induct_auto.ML";
+result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Sep.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,7 @@
+Sep = List +
+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)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Sep2.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,6 @@
+Sep2 = List +
+consts sep :: "'a * 'a list => 'a list"
+recdef sep "measure (%(a,xs). length xs)"
+ "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
+ "sep(a, xs) = xs"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Tree.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+Tree = Main +
+datatype 'a tree = Tip | Node ('a tree) 'a ('a tree)
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/Types.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,5 @@
+Types = Main +
+types number = nat
+ gate = bool => bool => bool
+ ('a,'b)alist = "('a * 'b)list"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/autotac.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(Auto_tac);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/constdefs Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+constdefs nand :: gate
+ "nand A B == ~(A & B)"
+ exor :: gate
+ "exor A B == A & ~B | ~A & B"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/constdefsprolog Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+ConstDefs = Types +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/consts Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+consts nand, exor :: gate
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/defs Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+defs nand_def "nand A B == ~(A & B)"
+ exor_def "exor A B == A & ~B | ~A & B"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/defsprolog Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Defs = Types +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/end Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/exhaust.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+Goal "(case xs of [] => [] | y#ys => xs) = xs";
+by(exhaust_tac "xs" 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/exorgoal.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goalw [exor_def] "exor A (~A)";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/exorproof.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(simp_tac (simpset() addsimps [exor_def]) 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/induct_auto.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+by(induct_tac "xs" 1);
+by(Auto_tac);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/itrev1.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "itrev xs [] = rev xs";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/itrev2.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "itrev xs ys = rev xs @ ys";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/itrev3.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "!ys. itrev xs ys = rev xs @ ys";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/natsum Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,4 @@
+consts sum :: nat => nat
+primrec
+"sum 0 = 0"
+"sum (Suc n) = Suc n + sum n"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/natsumprolog Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+NatSum = Main +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/splitif.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(split_tac [split_if] 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/splitlist.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(split_tac [list.split] 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/tree Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+datatype 'a tree = Tip | Node ('a tree) 'a ('a tree)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/treeprolog Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Tree = Main +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/types Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+types number = nat
+ gate = bool => bool => bool
+ ('a,'b)alist = "('a * 'b)list"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Misc/typesprolog Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Types = Main +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/ROOT.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+use_thy "ToyList";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/ToyList.ML Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,19 @@
+Goal "xs @ [] = xs";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "app_Nil2";
+Addsimps [app_Nil2];
+Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "app_assoc";
+Addsimps [app_assoc];
+Goal "rev(xs @ ys) = (rev ys) @ (rev xs)";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "rev_app";
+Addsimps [rev_app];
+Goal "rev(rev xs) = xs";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "rev_rev";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/ToyList.thy Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,17 @@
+ToyList = Datatype +
+
+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 # [])"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/addsimps2 Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Addsimps [app_Nil2];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/autotac Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(Auto_tac);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/inductxs Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+by(induct_tac "xs" 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/lemma1 Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "rev(xs @ ys) = (rev ys) @ (rev xs)";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/lemma2 Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "xs @ [] = xs";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/lemma3 Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,3 @@
+Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
+by(induct_tac "xs" 1);
+by(Auto_tac);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+qed "rev_rev";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed1 Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+qed "rev_app";
+Addsimps [rev_app];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed2 Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+qed "app_Nil2";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/qed3 Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,2 @@
+qed "app_assoc";
+Addsimps [app_assoc];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/ToyList/thm Wed Aug 26 17:27:27 1998 +0200
@@ -0,0 +1,1 @@
+Goal "rev(rev xs) = xs";