# HG changeset patch
# User wenzelm
# Date 901295757 -7200
# Node ID be986f7a6def4ef56d36ef108fd4139e6ae4894d
# Parent  b1adae4f8b90285ce7b9497c059b3af56d034f35
added ex/MonoidGroups (record example);
moved Bin and String examples to ex;

diff -r b1adae4f8b90 -r be986f7a6def src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Jul 24 17:54:58 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Jul 24 17:55:57 1998 +0200
@@ -279,70 +279,3 @@
 Addsimps [zdiff_def, iob_eq_eq_diff_0, iob_less_eq_diff_lt_0, 
           iob_le_diff_lt_0_or_eq_0, iob_Plus_eq_0, iob_Minus_not_eq_0, 
           iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0];
-
-
-(*** Examples of performing binary arithmetic by simplification ***)
-
-Goal "#13  +  #19 = #32";
-by (Simp_tac 1);
-result();
-
-Goal "#1234  +  #5678 = #6912";
-by (Simp_tac 1);
-result();
-
-Goal "#1359  +  #~2468 = #~1109";
-by (Simp_tac 1);
-result();
-
-Goal "#93746 +  #~46375 = #47371";
-by (Simp_tac 1);
-result();
-
-Goal "$~ #65745 = #~65745";
-by (Simp_tac 1);
-result();
-
-Goal "$~ #~54321 = #54321";
-by (Simp_tac 1);
-result();
-
-Goal "#13  *  #19 = #247";
-by (Simp_tac 1);
-result();
-
-Goal "#~84  *  #51 = #~4284";
-by (Simp_tac 1);
-result();
-
-Goal "#255  *  #255 = #65025";
-by (Simp_tac 1);
-result();
-
-Goal "#1359  *  #~2468 = #~3354012";
-by (Simp_tac 1);
-result();
-
-Goal "#89 * #10 ~= #889";  
-by (Simp_tac 1); 
-result();
-
-Goal "#13 < #18 - #4";  
-by (Simp_tac 1); 
-result();
-
-Goal "#~345 < #~242 + #~100";  
-by (Simp_tac 1); 
-result();
-
-Goal "#13557456 < #18678654";  
-by (Simp_tac 1); 
-result();
-
-Goal "#999999 <= (#1000001 + #1)-#2";  
-by (Simp_tac 1); 
-result();
-
-Goal "#1234567 <= #1234567";  
-by (Simp_tac 1); 
-result();
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jul 24 17:54:58 1998 +0200
+++ b/src/HOL/IsaMakefile	Fri Jul 24 17:55:57 1998 +0200
@@ -47,7 +47,7 @@
   Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
   Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
   RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
-  String.ML String.thy Sum.ML Sum.thy \
+  String.thy Sum.ML Sum.thy \
   Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
   Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
@@ -283,13 +283,13 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/BT.ML ex/BT.thy ex/Fib.ML ex/Fib.thy \
   ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
-  ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML ex/Primrec.thy \
-  ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML \
-  ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML \
-  ex/meson.ML ex/mesontest.ML ex/set.ML \
-  ex/Group.ML ex/Group.thy  ex/IntRing.ML ex/IntRing.thy \
-  ex/IntRingDefs.ML ex/IntRingDefs.thy \
-  ex/Lagrange.ML ex/Lagrange.thy ex/Ring.ML ex/Ring.thy
+  ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML \
+  ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
+  ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML ex/meson.ML \
+  ex/mesontest.ML ex/set.ML ex/Group.ML ex/Group.thy ex/IntRing.ML \
+  ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
+  ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
+  ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/String.ML
--- a/src/HOL/String.ML	Fri Jul 24 17:54:58 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-Goal "hd(''ABCD'') = CHR ''A''";
-by (Simp_tac 1);
-result();
-
-Goal "hd(''ABCD'') ~= CHR ''B''";
-by (Simp_tac 1);
-result();
-
-Goal "''ABCD'' ~= ''ABCX''";
-by (Simp_tac 1);
-result();
-
-Goal "''ABCD'' = ''ABCD''";
-by (Simp_tac 1);
-result();
-
-Goal
-  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
-by (Simp_tac 1);
-result();
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/ex/BinEx.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/BinEx.ML	Fri Jul 24 17:55:57 1998 +0200
@@ -0,0 +1,66 @@
+
+(*** Examples of performing binary arithmetic by simplification ***)
+
+Goal "#13  +  #19 = #32";
+by (Simp_tac 1);
+result();
+
+Goal "#1234  +  #5678 = #6912";
+by (Simp_tac 1);
+result();
+
+Goal "#1359  +  #~2468 = #~1109";
+by (Simp_tac 1);
+result();
+
+Goal "#93746 +  #~46375 = #47371";
+by (Simp_tac 1);
+result();
+
+Goal "$~ #65745 = #~65745";
+by (Simp_tac 1);
+result();
+
+Goal "$~ #~54321 = #54321";
+by (Simp_tac 1);
+result();
+
+Goal "#13  *  #19 = #247";
+by (Simp_tac 1);
+result();
+
+Goal "#~84  *  #51 = #~4284";
+by (Simp_tac 1);
+result();
+
+Goal "#255  *  #255 = #65025";
+by (Simp_tac 1);
+result();
+
+Goal "#1359  *  #~2468 = #~3354012";
+by (Simp_tac 1);
+result();
+
+Goal "#89 * #10 ~= #889";  
+by (Simp_tac 1); 
+result();
+
+Goal "#13 < #18 - #4";  
+by (Simp_tac 1); 
+result();
+
+Goal "#~345 < #~242 + #~100";  
+by (Simp_tac 1); 
+result();
+
+Goal "#13557456 < #18678654";  
+by (Simp_tac 1); 
+result();
+
+Goal "#999999 <= (#1000001 + #1)-#2";  
+by (Simp_tac 1); 
+result();
+
+Goal "#1234567 <= #1234567";  
+by (Simp_tac 1); 
+result();
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/ex/BinEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/BinEx.thy	Fri Jul 24 17:55:57 1998 +0200
@@ -0,0 +1,2 @@
+
+BinEx = Bin
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/ex/MonoidGroup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/MonoidGroup.thy	Fri Jul 24 17:55:57 1998 +0200
@@ -0,0 +1,33 @@
+(*  Title:      HOL/ex/MonoidGroup.thy
+    ID:         $Id$
+    Author:     Markus Wenzel
+    Copyright   1996 TU Muenchen
+
+Monoids and Groups as predicates over record schemes.
+*)
+
+MonoidGroup = HOL + Record +
+
+
+record 'a monoid_sig =
+  times :: "['a, 'a] => 'a"
+  one :: 'a
+
+record 'a group_sig = 'a monoid_sig +
+  inv :: "'a => 'a"
+
+constdefs
+  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) => bool"
+  "monoid M == ALL x y z.
+    times M (times M x y) z = times M x (times M y z) &
+    times M (one M) x & times M x (one M) = x"
+
+  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
+  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
+
+  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
+    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
+  "reverse M == M (| times := %x y. times M y x |)"
+
+
+end
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Jul 24 17:54:58 1998 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Jul 24 17:55:57 1998 +0200
@@ -32,4 +32,11 @@
 time_use     "set.ML";
 time_use_thy "MT";
 
+time_use_thy "StringEx";
+time_use_thy "BinEx";
+
+(*Monoids and Groups as predicates over record schemes*)
+time_use_thy "MonoidGroup";
+
+
 writeln "END: Root file for HOL examples";
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/ex/StringEx.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/StringEx.ML	Fri Jul 24 17:55:57 1998 +0200
@@ -0,0 +1,21 @@
+
+Goal "hd(''ABCD'') = CHR ''A''";
+by (Simp_tac 1);
+result();
+
+Goal "hd(''ABCD'') ~= CHR ''B''";
+by (Simp_tac 1);
+result();
+
+Goal "''ABCD'' ~= ''ABCX''";
+by (Simp_tac 1);
+result();
+
+Goal "''ABCD'' = ''ABCD''";
+by (Simp_tac 1);
+result();
+
+Goal
+  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
+by (Simp_tac 1);
+result();
diff -r b1adae4f8b90 -r be986f7a6def src/HOL/ex/StringEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/StringEx.thy	Fri Jul 24 17:55:57 1998 +0200
@@ -0,0 +1,2 @@
+
+StringEx = String