# HG changeset patch
# User haftmann
# Date 1167927468 -3600
# Node ID dfa5133dbe73125d3a1e559c34e4152f25e986dd
# Parent  4b802a9e0738c5cbb43041988656a5ea23b582c5
updated manual

diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Jan 04 17:17:48 2007 +0100
@@ -984,7 +984,7 @@
 \ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
 This merely introduces a class \isa{eq} with corresponding
-  operation \isa{foo{\isachardot}op\ {\isacharequal}};
+  operation \isa{op\ {\isacharequal}};
   the preprocessing framework does the rest.%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Jan 04 17:17:48 2007 +0100
@@ -6,6 +6,7 @@
 
 heada :: (Codegen.Null a) => ([a] -> a)
 heada (y : xs) = y
+heada [] = Codegen.nulla
 
 null_option :: Maybe b
 null_option = Nothing
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -6,7 +6,8 @@
 
 val arbitrary_option : 'a option = NONE;
 
-fun dummy_option [] = arbitrary_option;
+fun dummy_option [] = arbitrary_option
+  | dummy_option (x :: xs) = SOME x;
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -4,7 +4,8 @@
 structure HOL = 
 struct
 
-fun nota false = true;
+fun nota false = true
+  | nota true = false;
 
 end; (*struct HOL*)
 
@@ -13,7 +14,9 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+  | less_nat n Zero_nat = false
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 
@@ -22,9 +25,8 @@
 structure Codegen = 
 struct
 
-fun in_interval (k, l) n = (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l)
-  | in_interval (k, l) n =
-    (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
+fun in_interval (k, l) n =
+  (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -6,9 +6,13 @@
 
 datatype boola = True | False;
 
-fun nota False = True;
+fun nota False = True
+  | nota True = False;
 
-fun op_conj y True = y;
+fun op_conj y True = y
+  | op_conj x False = False
+  | op_conj True y = y
+  | op_conj False x = False;
 
 end; (*struct HOL*)
 
@@ -17,7 +21,9 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = HOL.True;
+fun less_nat Zero_nat (Suc n) = HOL.True
+  | less_nat n Zero_nat = HOL.False
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 
@@ -27,9 +33,7 @@
 struct
 
 fun in_interval (k, l) n =
-  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l)
-  | in_interval (k, l) n =
-    HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
+  HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -4,7 +4,8 @@
 structure HOL = 
 struct
 
-fun nota false = true;
+fun nota false = true
+  | nota true = false;
 
 end; (*struct HOL*)
 
@@ -13,7 +14,9 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+  | less_nat n Zero_nat = false
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 
@@ -23,9 +26,7 @@
 struct
 
 fun in_interval (k, l) n =
-  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l)
-  | in_interval (k, l) n =
-    (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
+  (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -14,7 +14,8 @@
 type 'a null = {null_ : 'a};
 fun null (A_:'a null) = #null_ A_;
 
-fun head (A_:'a null) (y :: xs) = y;
+fun head (A_:'a null) (y :: xs) = y
+  | head (A_:'a null) [] = null A_;
 
 val null_option : 'b option = NONE;
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -13,7 +13,8 @@
 struct
 
 fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
-  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys);
+  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys)
+  | memberl (A_:'a Code_Generator.eq) x [] = false;
 
 end; (*struct List*)
 
@@ -24,7 +25,8 @@
   (if List.memberl A_ z xs
     then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
            else collect_duplicates A_ xs (z :: ys) zs)
-    else collect_duplicates A_ (z :: xs) (z :: ys) zs);
+    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
+  | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -7,16 +7,18 @@
 datatype nat = Zero_nat | Suc of nat;
 
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
-  | plus_nat (Suc m) n = Suc (plus_nat m n);
+  | plus_nat Zero_nat y = y;
 
-fun times_nat (Suc m) n = plus_nat n (times_nat m n);
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
+  | times_nat Zero_nat n = Zero_nat;
 
 end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
-fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
+fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
+  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -7,9 +7,10 @@
 datatype nat = Zero_nat | Suc of nat;
 
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
-  | plus_nat (Suc m) n = Suc (plus_nat m n);
+  | plus_nat Zero_nat y = y;
 
-fun times_nat (Suc m) n = plus_nat n (times_nat m n);
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
+  | times_nat Zero_nat n = Zero_nat;
 
 end; (*struct Nat*)
 
@@ -18,8 +19,7 @@
 
 fun fac n =
   (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
-     | Nat.Suc m => Nat.times_nat n (fac m))
-  | fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
+     | Nat.Suc m => Nat.times_nat n (fac m));
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -5,7 +5,8 @@
 struct
 
 fun lookup ((k, v) :: xs) l =
-  (if ((k : string) = l) then SOME v else lookup xs l);
+  (if ((k : string) = l) then SOME v else lookup xs l)
+  | lookup [] l = NONE;
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -6,9 +6,13 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+  | less_nat n Zero_nat = false
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
-fun minus_nat (Suc m) (Suc n) = minus_nat m n;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
+  | minus_nat Zero_nat n = Zero_nat
+  | minus_nat y Zero_nat = y;
 
 end; (*struct Nat*)
 
@@ -16,7 +20,13 @@
 struct
 
 fun pick ((k, v) :: xs) n =
-  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
+  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
+  | pick (x :: xs) n =
+    let
+      val (k, v) = x;
+    in
+      (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
+    end;
 
 end; (*struct Codegen*)
 
diff -r 4b802a9e0738 -r dfa5133dbe73 doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 17:11:09 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Thu Jan 04 17:17:48 2007 +0100
@@ -6,9 +6,13 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true;
+fun less_nat Zero_nat (Suc n) = true
+  | less_nat n Zero_nat = false
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
-fun minus_nat (Suc m) (Suc n) = minus_nat m n;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
+  | minus_nat Zero_nat n = Zero_nat
+  | minus_nat y Zero_nat = y;
 
 end; (*struct Nat*)