# HG changeset patch
# User haftmann
# Date 1248179786 -7200
# Node ID a853099fd9ca52010f84a34c63cde3255952ebdc
# Parent  0762b9ad83df00c46c702b79e0660307ae60088f
moved abstract algebra section to the end

diff -r 0762b9ad83df -r a853099fd9ca src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jul 21 11:09:50 2009 +0200
+++ b/src/HOL/HOL.thy	Tue Jul 21 14:36:26 2009 +0200
@@ -107,7 +107,6 @@
 notation (xsymbols)
   iff  (infixr "\<longleftrightarrow>" 25)
 
-
 nonterminals
   letbinds  letbind
   case_syn  cases_syn
@@ -198,96 +197,9 @@
 axiomatization
   undefined :: 'a
 
-
-subsubsection {* Generic classes and algebraic operations *}
-
 class default =
   fixes default :: 'a
 
-class zero = 
-  fixes zero :: 'a  ("0")
-
-class one =
-  fixes one  :: 'a  ("1")
-
-hide (open) const zero one
-
-class plus =
-  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
-
-class minus =
-  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
-
-class uminus =
-  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
-
-class times =
-  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
-
-class inverse =
-  fixes inverse :: "'a \<Rightarrow> 'a"
-    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
-
-class abs =
-  fixes abs :: "'a \<Rightarrow> 'a"
-begin
-
-notation (xsymbols)
-  abs  ("\<bar>_\<bar>")
-
-notation (HTML output)
-  abs  ("\<bar>_\<bar>")
-
-end
-
-class sgn =
-  fixes sgn :: "'a \<Rightarrow> 'a"
-
-class ord =
-  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-begin
-
-notation
-  less_eq  ("op <=") and
-  less_eq  ("(_/ <= _)" [51, 51] 50) and
-  less  ("op <") and
-  less  ("(_/ < _)"  [51, 51] 50)
-  
-notation (xsymbols)
-  less_eq  ("op \<le>") and
-  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
-
-notation (HTML output)
-  less_eq  ("op \<le>") and
-  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
-
-abbreviation (input)
-  greater_eq  (infix ">=" 50) where
-  "x >= y \<equiv> y <= x"
-
-notation (input)
-  greater_eq  (infix "\<ge>" 50)
-
-abbreviation (input)
-  greater  (infix ">" 50) where
-  "x > y \<equiv> y < x"
-
-end
-
-syntax
-  "_index1"  :: index    ("\<^sub>1")
-translations
-  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
-typed_print_translation {*
-let
-  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
-    if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
-    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
-in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
-*} -- {* show types that are presumably too general *}
-
 
 subsection {* Fundamental rules *}
 
@@ -1605,25 +1517,9 @@
 
 setup ReorientProc.init
 
-setup {*
-  ReorientProc.add
-    (fn Const(@{const_name HOL.zero}, _) => true
-      | Const(@{const_name HOL.one}, _) => true
-      | _ => false)
-*}
-
-simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
-simproc_setup reorient_one ("1 = x") = ReorientProc.proc
-
 
 subsection {* Other simple lemmas and lemma duplicates *}
 
-lemma Let_0 [simp]: "Let 0 f = f 0"
-  unfolding Let_def ..
-
-lemma Let_1 [simp]: "Let 1 f = f 1"
-  unfolding Let_def ..
-
 lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
   by blast+
 
@@ -1643,13 +1539,6 @@
   apply (drule_tac [3] x = x in fun_cong, simp_all)
   done
 
-lemma mk_left_commute:
-  fixes f (infix "\<otimes>" 60)
-  assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
-          c: "\<And>x y. x \<otimes> y = y \<otimes> x"
-  shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
-  by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
-
 lemmas eq_sym_conv = eq_commute
 
 lemma nnf_simps:
@@ -1659,6 +1548,118 @@
 by blast+
 
 
+subsection {* Generic classes and algebraic operations *}
+
+class zero = 
+  fixes zero :: 'a  ("0")
+
+class one =
+  fixes one  :: 'a  ("1")
+
+lemma Let_0 [simp]: "Let 0 f = f 0"
+  unfolding Let_def ..
+
+lemma Let_1 [simp]: "Let 1 f = f 1"
+  unfolding Let_def ..
+
+setup {*
+  ReorientProc.add
+    (fn Const(@{const_name HOL.zero}, _) => true
+      | Const(@{const_name HOL.one}, _) => true
+      | _ => false)
+*}
+
+simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
+simproc_setup reorient_one ("1 = x") = ReorientProc.proc
+
+typed_print_translation {*
+let
+  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
+    if (not o null) ts orelse T = dummyT
+      orelse not (! show_types) andalso can Term.dest_Type T
+    then raise Match
+    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
+in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
+*} -- {* show types that are presumably too general *}
+
+hide (open) const zero one
+
+class plus =
+  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
+
+class minus =
+  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
+
+class uminus =
+  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
+
+class times =
+  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
+
+class inverse =
+  fixes inverse :: "'a \<Rightarrow> 'a"
+    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
+
+class abs =
+  fixes abs :: "'a \<Rightarrow> 'a"
+begin
+
+notation (xsymbols)
+  abs  ("\<bar>_\<bar>")
+
+notation (HTML output)
+  abs  ("\<bar>_\<bar>")
+
+end
+
+class sgn =
+  fixes sgn :: "'a \<Rightarrow> 'a"
+
+class ord =
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+
+notation
+  less_eq  ("op <=") and
+  less_eq  ("(_/ <= _)" [51, 51] 50) and
+  less  ("op <") and
+  less  ("(_/ < _)"  [51, 51] 50)
+  
+notation (xsymbols)
+  less_eq  ("op \<le>") and
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
+
+notation (HTML output)
+  less_eq  ("op \<le>") and
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
+
+abbreviation (input)
+  greater_eq  (infix ">=" 50) where
+  "x >= y \<equiv> y <= x"
+
+notation (input)
+  greater_eq  (infix "\<ge>" 50)
+
+abbreviation (input)
+  greater  (infix ">" 50) where
+  "x > y \<equiv> y < x"
+
+end
+
+syntax
+  "_index1"  :: index    ("\<^sub>1")
+translations
+  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
+
+lemma mk_left_commute:
+  fixes f (infix "\<otimes>" 60)
+  assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
+          c: "\<And>x y. x \<otimes> y = y \<otimes> x"
+  shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
+  by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
+
+
 subsection {* Basic ML bindings *}
 
 ML {*