# HG changeset patch
# User haftmann
# Date 1168931217 -3600
# Node ID 00bed5ac98843ab03ef205d0f25edbb74bcd442a
# Parent  39d5d42116c4dfc0f3327ca78641c5d33519bcab
renamed locale partial_order to order

diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/Lattices.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -16,12 +16,12 @@
 Finite_Set}. In the longer term it may be better to define arbitrary
 sups and infs via @{text THE}. *}
 
-locale lower_semilattice = partial_order +
+locale lower_semilattice = order +
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
   assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
 
-locale upper_semilattice = partial_order +
+locale upper_semilattice = order +
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
   assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -101,10 +101,10 @@
 lemma order_le_err [iff]:
   "order(le r) = order r"
 apply (rule iffI)
- apply (subst order_def)
+ apply (subst Semilat.order_def)
  apply (blast dest: order_antisym OK_le_err_OK [THEN iffD2]
               intro: order_trans OK_le_err_OK [THEN iffD1])
-apply (subst order_def)
+apply (subst Semilat.order_def)
 apply (blast intro: le_err_refl le_err_trans le_err_antisym
              dest: order_refl)
 done 
@@ -252,7 +252,7 @@
 
 lemma eq_order_le:
   "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
-apply (unfold order_def)
+apply (unfold Semilat.order_def)
 apply blast
 done
 
diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -87,7 +87,7 @@
 
 lemma order_widen:
   "acyclic (subcls1 G) \<Longrightarrow> order (subtype G)"
-  apply (unfold order_def lesub_def subtype_def)
+  apply (unfold Semilat.order_def lesub_def subtype_def)
   apply (auto intro: widen_trans)
   apply (case_tac x)
    apply (case_tac y)
diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -124,7 +124,7 @@
 
 lemma order_listI [simp, intro!]:
   "order r \<Longrightarrow> order(Listn.le r)"
-apply (subst order_def)
+apply (subst Semilat.order_def)
 apply (blast intro: le_list_refl le_list_trans le_list_antisym
              dest: order_refl)
 done
diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -54,7 +54,7 @@
 
 lemma order_le_opt [intro!,simp]:
   "order r \<Longrightarrow> order(le r)"
-apply (subst order_def)
+apply (subst Semilat.order_def)
 apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
 done 
 
diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/MicroJava/BV/Product.thy
--- a/src/HOL/MicroJava/BV/Product.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -42,7 +42,7 @@
 
 lemma order_le_prod [iff]:
   "order(Product.le rA rB) = (order rA & order rB)"
-apply (unfold order_def)
+apply (unfold Semilat.order_def)
 apply simp
 apply blast
 done 
diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/Orderings.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -122,10 +122,10 @@
 
 subsection {* Partial orderings *}
 
-locale partial_order = preorder + 
+locale order = preorder + 
   assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
 
-context partial_order
+context order
 begin
 
 text {* Asymmetry. *}
@@ -181,7 +181,7 @@
   order_less_le: "(x < y) = (x <= y & x ~= y)"
 
 interpretation order:
-  partial_order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
+  order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
 apply unfold_locales
 apply (rule order_refl)
 apply (erule (1) order_trans)
@@ -192,7 +192,7 @@
 
 subsection {* Linear (total) orders *}
 
-locale linorder = partial_order +
+locale linorder = order +
   assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
 begin
 
diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -1,4 +1,4 @@
- (*  ID:         $Id$
+(*  ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
@@ -8,8 +8,6 @@
 imports Main Product_ord List_lexord
 begin
 
-section {* Collection classes as examples for code generation *}
-
 fun
   abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   "abs_sorted cmp [] \<longleftrightarrow> True"
@@ -22,7 +20,7 @@
 abbreviation
   "sorted \<equiv> abs_sorted less_eq"
 
-lemma (in partial_order) sorted_weakening:
+lemma (in order) sorted_weakening:
   assumes "sorted (x # xs)"
   shows "sorted xs"
 using prems proof (induct xs)