renamed locale partial_order to order
authorhaftmann
Tue Jan 16 08:06:57 2007 +0100 (2007-01-16)
changeset 2206800bed5ac9884
parent 22067 39d5d42116c4
child 22069 8668c056c507
renamed locale partial_order to order
src/HOL/Lattices.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Opt.thy
src/HOL/MicroJava/BV/Product.thy
src/HOL/Orderings.thy
src/HOL/ex/CodeCollections.thy
     1.1 --- a/src/HOL/Lattices.thy	Tue Jan 16 08:06:55 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Tue Jan 16 08:06:57 2007 +0100
     1.3 @@ -16,12 +16,12 @@
     1.4  Finite_Set}. In the longer term it may be better to define arbitrary
     1.5  sups and infs via @{text THE}. *}
     1.6  
     1.7 -locale lower_semilattice = partial_order +
     1.8 +locale lower_semilattice = order +
     1.9    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.10    assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
    1.11    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    1.12  
    1.13 -locale upper_semilattice = partial_order +
    1.14 +locale upper_semilattice = order +
    1.15    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.16    assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
    1.17    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
     2.1 --- a/src/HOL/MicroJava/BV/Err.thy	Tue Jan 16 08:06:55 2007 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Tue Jan 16 08:06:57 2007 +0100
     2.3 @@ -101,10 +101,10 @@
     2.4  lemma order_le_err [iff]:
     2.5    "order(le r) = order r"
     2.6  apply (rule iffI)
     2.7 - apply (subst order_def)
     2.8 + apply (subst Semilat.order_def)
     2.9   apply (blast dest: order_antisym OK_le_err_OK [THEN iffD2]
    2.10                intro: order_trans OK_le_err_OK [THEN iffD1])
    2.11 -apply (subst order_def)
    2.12 +apply (subst Semilat.order_def)
    2.13  apply (blast intro: le_err_refl le_err_trans le_err_antisym
    2.14               dest: order_refl)
    2.15  done 
    2.16 @@ -252,7 +252,7 @@
    2.17  
    2.18  lemma eq_order_le:
    2.19    "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
    2.20 -apply (unfold order_def)
    2.21 +apply (unfold Semilat.order_def)
    2.22  apply blast
    2.23  done
    2.24  
     3.1 --- a/src/HOL/MicroJava/BV/JType.thy	Tue Jan 16 08:06:55 2007 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Tue Jan 16 08:06:57 2007 +0100
     3.3 @@ -87,7 +87,7 @@
     3.4  
     3.5  lemma order_widen:
     3.6    "acyclic (subcls1 G) \<Longrightarrow> order (subtype G)"
     3.7 -  apply (unfold order_def lesub_def subtype_def)
     3.8 +  apply (unfold Semilat.order_def lesub_def subtype_def)
     3.9    apply (auto intro: widen_trans)
    3.10    apply (case_tac x)
    3.11     apply (case_tac y)
     4.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 08:06:55 2007 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 08:06:57 2007 +0100
     4.3 @@ -124,7 +124,7 @@
     4.4  
     4.5  lemma order_listI [simp, intro!]:
     4.6    "order r \<Longrightarrow> order(Listn.le r)"
     4.7 -apply (subst order_def)
     4.8 +apply (subst Semilat.order_def)
     4.9  apply (blast intro: le_list_refl le_list_trans le_list_antisym
    4.10               dest: order_refl)
    4.11  done
     5.1 --- a/src/HOL/MicroJava/BV/Opt.thy	Tue Jan 16 08:06:55 2007 +0100
     5.2 +++ b/src/HOL/MicroJava/BV/Opt.thy	Tue Jan 16 08:06:57 2007 +0100
     5.3 @@ -54,7 +54,7 @@
     5.4  
     5.5  lemma order_le_opt [intro!,simp]:
     5.6    "order r \<Longrightarrow> order(le r)"
     5.7 -apply (subst order_def)
     5.8 +apply (subst Semilat.order_def)
     5.9  apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
    5.10  done 
    5.11  
     6.1 --- a/src/HOL/MicroJava/BV/Product.thy	Tue Jan 16 08:06:55 2007 +0100
     6.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Tue Jan 16 08:06:57 2007 +0100
     6.3 @@ -42,7 +42,7 @@
     6.4  
     6.5  lemma order_le_prod [iff]:
     6.6    "order(Product.le rA rB) = (order rA & order rB)"
     6.7 -apply (unfold order_def)
     6.8 +apply (unfold Semilat.order_def)
     6.9  apply simp
    6.10  apply blast
    6.11  done 
     7.1 --- a/src/HOL/Orderings.thy	Tue Jan 16 08:06:55 2007 +0100
     7.2 +++ b/src/HOL/Orderings.thy	Tue Jan 16 08:06:57 2007 +0100
     7.3 @@ -122,10 +122,10 @@
     7.4  
     7.5  subsection {* Partial orderings *}
     7.6  
     7.7 -locale partial_order = preorder + 
     7.8 +locale order = preorder + 
     7.9    assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
    7.10  
    7.11 -context partial_order
    7.12 +context order
    7.13  begin
    7.14  
    7.15  text {* Asymmetry. *}
    7.16 @@ -181,7 +181,7 @@
    7.17    order_less_le: "(x < y) = (x <= y & x ~= y)"
    7.18  
    7.19  interpretation order:
    7.20 -  partial_order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
    7.21 +  order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
    7.22  apply unfold_locales
    7.23  apply (rule order_refl)
    7.24  apply (erule (1) order_trans)
    7.25 @@ -192,7 +192,7 @@
    7.26  
    7.27  subsection {* Linear (total) orders *}
    7.28  
    7.29 -locale linorder = partial_order +
    7.30 +locale linorder = order +
    7.31    assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    7.32  begin
    7.33  
     8.1 --- a/src/HOL/ex/CodeCollections.thy	Tue Jan 16 08:06:55 2007 +0100
     8.2 +++ b/src/HOL/ex/CodeCollections.thy	Tue Jan 16 08:06:57 2007 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 - (*  ID:         $Id$
     8.5 +(*  ID:         $Id$
     8.6      Author:     Florian Haftmann, TU Muenchen
     8.7  *)
     8.8  
     8.9 @@ -8,8 +8,6 @@
    8.10  imports Main Product_ord List_lexord
    8.11  begin
    8.12  
    8.13 -section {* Collection classes as examples for code generation *}
    8.14 -
    8.15  fun
    8.16    abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    8.17    "abs_sorted cmp [] \<longleftrightarrow> True"
    8.18 @@ -22,7 +20,7 @@
    8.19  abbreviation
    8.20    "sorted \<equiv> abs_sorted less_eq"
    8.21  
    8.22 -lemma (in partial_order) sorted_weakening:
    8.23 +lemma (in order) sorted_weakening:
    8.24    assumes "sorted (x # xs)"
    8.25    shows "sorted xs"
    8.26  using prems proof (induct xs)