# HG changeset patch
# User haftmann
# Date 1172846597 -3600
# Node ID 4ebe883b02ff020ea2853526a127e1ac27ce4467
# Parent  cc2be3315e728f47c81ec5b048e6ceebc775f1b3
new code theorems

diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -1,24 +1,15 @@
 structure ROOT = 
 struct
 
-structure HOL = 
-struct
-
-fun nota false = true
-  | nota true = false;
-
-end; (*struct HOL*)
-
 structure Nat = 
 struct
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
+fun less_nat n (Suc m) = less_eq_nat n m
   | 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);
+and less_eq_nat (Suc n) m = less_nat n m
+  | less_eq_nat Zero_nat m = true;
 
 end; (*struct Nat*)
 
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -6,9 +6,6 @@
 
 datatype boola = True | False;
 
-fun nota False = True
-  | nota True = False;
-
 fun op_conj y True = y
   | op_conj x False = False
   | op_conj True y = y
@@ -21,11 +18,10 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = HOL.True
+fun less_nat n (Suc m) = less_eq_nat n m
   | 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);
+and less_eq_nat (Suc n) m = less_nat n m
+  | less_eq_nat Zero_nat m = HOL.True;
 
 end; (*struct Nat*)
 
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -1,24 +1,15 @@
 structure ROOT = 
 struct
 
-structure HOL = 
-struct
-
-fun nota false = true
-  | nota true = false;
-
-end; (*struct HOL*)
-
 structure Nat = 
 struct
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
+fun less_nat n (Suc m) = less_eq_nat n m
   | 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);
+and less_eq_nat (Suc n) m = less_nat n m
+  | less_eq_nat Zero_nat m = true;
 
 end; (*struct Nat*)
 
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -11,15 +11,15 @@
 structure Codegen = 
 struct
 
-type 'a null = {Codegen__null : 'a};
-fun null (A_:'a null) = #Codegen__null A_;
+type 'a null = {null : 'a};
+fun null (A_:'a null) = #null A_;
 
 fun head A_ (y :: xs) = y
   | head A_ [] = null A_;
 
 val null_option : 'a option = NONE;
 
-fun null_optiona () = {Codegen__null = null_option} : ('b option) null;
+fun null_optiona () = {null = null_option} : ('b option) null;
 
 val dummy : Nat.nat option =
   head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -4,8 +4,8 @@
 structure Code_Generator = 
 struct
 
-type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
+type 'a eq = {op_eq : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq A_;
 
 end; (*struct Code_Generator*)
 
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -8,6 +8,17 @@
 
 end; (*struct Nat*)
 
+structure Integer = 
+struct
+
+fun nat_aux n i =
+  (if IntInf.<= (i, (0 : IntInf.int)) then n
+    else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
+
+fun nat i = nat_aux Nat.Zero_nat i;
+
+end; (*struct Integer*)
+
 structure Codegen = 
 struct
 
@@ -15,7 +26,7 @@
 
 val foobar_set : Nat.nat list =
   Nat.Zero_nat ::
-    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+    (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: []));
 
 end; (*struct Codegen*)
 
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -4,19 +4,17 @@
 structure Orderings = 
 struct
 
-type 'a ord =
-  {Orderings__less_eq : 'a -> 'a -> bool,
-    Orderings__less : 'a -> 'a -> bool};
-fun less_eq (A_:'a ord) = #Orderings__less_eq A_;
-fun less (A_:'a ord) = #Orderings__less A_;
+type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
+fun less_eq (A_:'a ord) = #less_eq A_;
+fun less (A_:'a ord) = #less A_;
 
 end; (*struct Orderings*)
 
 structure Code_Generator = 
 struct
 
-type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
+type 'a eq = {op_eq : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq A_;
 
 end; (*struct Code_Generator*)
 
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -6,9 +6,10 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
+fun less_nat n (Suc m) = less_eq_nat n m
   | less_nat n Zero_nat = false
-  | less_nat (Suc m) (Suc n) = less_nat m n;
+and less_eq_nat (Suc n) m = less_nat n m
+  | less_eq_nat Zero_nat m = true;
 
 fun minus_nat (Suc m) (Suc n) = minus_nat m n
   | minus_nat Zero_nat n = Zero_nat
diff -r cc2be3315e72 -r 4ebe883b02ff doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Fri Mar 02 15:43:17 2007 +0100
@@ -6,9 +6,10 @@
 
 datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Suc n) = true
+fun less_nat n (Suc m) = less_eq_nat n m
   | less_nat n Zero_nat = false
-  | less_nat (Suc m) (Suc n) = less_nat m n;
+and less_eq_nat (Suc n) m = less_nat n m
+  | less_eq_nat Zero_nat m = true;
 
 fun minus_nat (Suc m) (Suc n) = minus_nat m n
   | minus_nat Zero_nat n = Zero_nat