# HG changeset patch
# User nipkow
# Date 910885540 -3600
# Node ID 15ce4c1c83134e3a77dbf2df67a9cc3b5012f096
# Parent  9712294e60b938aa75e6220dfae7921b24af7002
New section on advanced datatypes.

diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/ABexp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/ABexp.thy	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,35 @@
+ABexp = Main +
+datatype
+    'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
+            | Sum ('a aexp) ('a aexp)
+            | Diff ('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 => nat) => 'a aexp => nat
+        evalb :: ('a => nat) => 'a bexp => bool
+primrec
+  "evala env (IF b a1 a2) =
+     (if evalb env b then evala env a1 else evala env a2)"
+  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
+  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
+  "evala env (Var v) = env v"
+  "evala env (Num n) = n"
+  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
+  "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
+  "evalb env (Neg b) = (~ evalb env b)"
+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 (Diff a1 a2) = Diff (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)"
+end
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/ROOT.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,25 @@
+use_thy "ABexp";
+use"abgoalind.ML";
+use"autotac.ML";
+result();
+
+use_thy "Term";
+use"tidproof.ML";
+result();
+use"appmap.ML";
+by(induct_tac "ts" 1);
+by(Auto_tac);
+qed"subst_App_map";
+Addsimps [subst_App_map];
+result();
+
+use_thy"Trie";
+use"lookupempty.ML";
+qed "lookup_empty";
+Addsimps [lookup_empty];
+use"trieAdds.ML";
+use"triemain.ML";
+use"trieinduct.ML";
+use"trieexhaust.ML";
+by(Auto_tac);
+result();
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/Term.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/Term.thy	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,16 @@
+Term = Main +
+datatype 'a t = A | B "'a * ('a t list)"
+datatype expr = Var string | Lam string expr | App expr expr
+              | Data data
+and      data = Bool bool | Num nat
+              | Closure string expr "(string * data)list"
+datatype ('a,'b)term = Var 'a | App 'b ((('a,'b)term)list)
+consts
+   subst  :: ('a => ('a,'b)term) => ('a,'b)term      => ('a,'b)term
+   substs :: ('a => ('a,'b)term) => ('a,'b)term list => ('a,'b)term list
+primrec
+  "subst s (Var x) = s x"
+  "subst s (App f ts) = App f (substs s ts)"
+  "substs s [] = []"
+  "substs s (t # ts) = subst s t # substs s ts"
+end
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/Trie.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/Trie.thy	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,23 @@
+Trie = Main +
+consts   assoc :: "('key * 'val)list => 'key => 'val option"
+primrec "assoc [] x = None"
+        "assoc (p#ps) x =
+           (let (a,b) = p in if a=x then Some b else assoc ps x)"
+datatype ('a,'v)trie = Trie ('v option) "('a * ('a,'v)trie)list"
+consts value :: ('a,'v)trie => 'v option
+       alist :: "('a,'v)trie => ('a * ('a,'v)trie)list"
+primrec "value(Trie ov al) = ov"
+primrec "alist(Trie ov al) = al"
+consts   lookup :: ('a,'v)trie => 'a list => 'v option
+primrec "lookup t [] = value t"
+        "lookup t (a#as) = (case assoc (alist t) a of
+                              None => None
+                            | Some at => lookup at as)"
+consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie
+
+primrec
+  "update t []     v = Trie (Some v) (alist t)"
+  "update t (a#as) v = (let tt = (case assoc (alist t) a of
+                                    None => Trie None [] | Some at => at)
+                        in Trie (value t) ((a,update tt as v)#alist t))"
+end
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abconstseval
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abconstseval	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,2 @@
+consts  evala :: ('a => nat) => 'a aexp => nat
+        evalb :: ('a => nat) => 'a bexp => bool
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abconstssubst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abconstssubst	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,2 @@
+consts substa :: ('a => 'b aexp) => 'a aexp => 'b aexp
+       substb :: ('a => 'b aexp) => 'a bexp => 'b bexp
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abdata
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abdata	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,9 @@
+datatype
+    'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
+            | Sum ('a aexp) ('a aexp)
+            | Diff ('a aexp) ('a aexp)
+            | Var 'a
+            | Num nat
+and 'a bexp = Less ('a aexp) ('a aexp)
+            | And ('a bexp) ('a bexp)
+            | Neg ('a bexp)
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abevala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abevala	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,7 @@
+primrec
+  "evala env (IF b a1 a2) =
+     (if evalb env b then evala env a1 else evala env a2)"
+  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
+  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
+  "evala env (Var v) = env v"
+  "evala env (Num n) = n"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abevalb
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abevalb	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,3 @@
+  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
+  "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
+  "evalb env (Neg b) = (~ evalb env b)"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abgoalfind.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abgoalfind.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,4 @@
+Goal
+ "evala env (substa s a) = evala (%x. evala env (s x)) a & \
+\ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
+by(mutual_induct_tac ["a","b"] 1);
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abgoalind.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abgoalind.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,4 @@
+Goal
+ "evala env (substa s a) = evala (%x. evala env (s x)) a & \
+\ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
+by(mutual_induct_tac ["a","b"] 1);
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/abprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/abprolog	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+ABexp = Main +
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/absubsta
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/absubsta	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,7 @@
+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 (Diff a1 a2) = Diff (substa s a1) (substa s a2)"
+  "substa s (Var v) = s v"
+  "substa s (Num n) = Num n"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/absubstb
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/absubstb	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,3 @@
+  "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)"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/appmap
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/appmap	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+"subst s (App f ts) = App f (map (subst s) ts)"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/appmap.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/appmap.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,3 @@
+Goal
+"subst s (App f ts) = App f (map (subst s) ts)"
+;
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/assoc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/assoc	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,4 @@
+consts   assoc :: "('key * 'val)list => 'key => 'val option"
+primrec "assoc [] x = None"
+        "assoc (p#ps) x =
+           (let (a,b) = p in if a=x then Some b else assoc ps x)"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/autotac.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/autotac.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+by(Auto_tac);
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/end	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+end
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/goal
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/goal	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+Goal
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/lookup
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/lookup	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,5 @@
+consts   lookup :: ('a,'v)trie => 'a list => 'v option
+primrec "lookup t [] = value t"
+        "lookup t (a#as) = (case assoc (alist t) a of
+                              None => None
+                            | Some at => lookup at as)"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/lookupempty.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/lookupempty.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,3 @@
+Goal "lookup (Trie None []) as = None";
+by(exhaust_tac "as" 1);
+by(Auto_tac);
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/mutnested
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/mutnested	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,4 @@
+datatype expr = Var string | Lam string expr | App expr expr
+              | Data data
+and      data = Bool bool | Num nat
+              | Closure string expr "(string * data)list"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/semi
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/semi	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+;
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/tconstssubst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/tconstssubst	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,3 @@
+consts
+   subst  :: ('a => ('a,'b)term) => ('a,'b)term      => ('a,'b)term
+   substs :: ('a => ('a,'b)term) => ('a,'b)term list => ('a,'b)term list
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/tdata
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/tdata	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+datatype ('a,'b)term = Var 'a | App 'b ((('a,'b)term)list)
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/tidproof.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/tidproof.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,4 @@
+Goal "subst  Var t  = (t ::('a,'b)term)  & \
+\     substs Var ts = (ts::('a,'b)term list)";
+by(mutual_induct_tac ["t", "ts"] 1);
+by(Auto_tac);
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/tprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/tprolog	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+Term = Main +
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/trie
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/trie	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+datatype ('a,'v)trie = Trie ('v option) "('a * ('a,'v)trie)list"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/trieAdds.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/trieAdds.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,2 @@
+Addsimps [Let_def];
+Addsplits [option.split];
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/trieexhaust.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/trieexhaust.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+by(ALLGOALS (exhaust_tac "bs"));
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/trieinduct.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/trieinduct.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,2 @@
+by(induct_tac "as" 1);
+by(Auto_tac);
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/triemain.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/triemain.ML	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,2 @@
+Goal "!t v bs. lookup (update t as v) bs = \
+\              (if as=bs then Some v else lookup t bs)";
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/trieprolog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/trieprolog	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,1 @@
+Trie = Main +
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/triesels
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/triesels	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,4 @@
+consts value :: ('a,'v)trie => 'v option
+       alist :: "('a,'v)trie => ('a * ('a,'v)trie)list"
+primrec "value(Trie ov al) = ov"
+primrec "alist(Trie ov al) = al"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/tsubst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/tsubst	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,3 @@
+primrec
+  "subst s (Var x) = s x"
+  "subst s (App f ts) = App f (substs s ts)"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/tsubsts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/tsubsts	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,2 @@
+  "substs s [] = []"
+  "substs s (t # ts) = subst s t # substs s ts"
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/tunfoldeddata
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/tunfoldeddata	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,2 @@
+datatype ('a,'b)term = Var 'a | App 'b (('a,'b)term_list)
+and ('a,'b)term_list = Nil | Cons (('a,'b)term) (('a,'b)term_list)
diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/update
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/update	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,7 @@
+consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie
+
+primrec
+  "update t []     v = Trie (Some v) (alist t)"
+  "update t (a#as) v = (let tt = (case assoc (alist t) a of
+                                    None => Trie None [] | Some at => at)
+                        in Trie (value t) ((a,update tt as v)#alist t))"