--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Mon Nov 18 18:04:45 2013 +0100
@@ -13,8 +13,6 @@
declare
ordLeq_Well_order_simp[simp]
- ordLess_Well_order_simp[simp]
- ordIso_Well_order_simp[simp]
not_ordLeq_iff_ordLess[simp]
not_ordLess_iff_ordLeq[simp]
@@ -88,7 +86,7 @@
by (auto simp add: ofilter_subset_embedS_iso)
-subsection {* Ordering the well-orders by existence of embeddings *}
+subsection {* Ordering the well-orders by existence of embeddings *}
corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq"
using ordLeq_reflexive unfolding ordLeq_def refl_on_def
@@ -113,6 +111,16 @@
corollary ordIso_equiv: "equiv {r. Well_order r} ordIso"
by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans)
+lemma ordLess_Well_order_simp[simp]:
+assumes "r <o r'"
+shows "Well_order r \<and> Well_order r'"
+using assms unfolding ordLess_def by simp
+
+lemma ordIso_Well_order_simp[simp]:
+assumes "r =o r'"
+shows "Well_order r \<and> Well_order r'"
+using assms unfolding ordIso_def by simp
+
lemma ordLess_irrefl: "irrefl ordLess"
by(unfold irrefl_def, auto simp add: ordLess_irreflexive)
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_LFP.thy Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_LFP.thy Mon Nov 18 18:04:45 2013 +0100
@@ -330,7 +330,7 @@
-subsection {* Ordering the well-orders by existence of embeddings *}
+subsection {* Ordering the well-orders by existence of embeddings *}
text {* We define three relations between well-orders:
@@ -383,18 +383,6 @@
using assms unfolding ordLeq_def by simp
-lemma ordLess_Well_order_simp:
-assumes "r <o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordLess_def by simp
-
-
-lemma ordIso_Well_order_simp:
-assumes "r =o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordIso_def by simp
-
-
text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,