# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1591888433 -3600
# Node ID 82b00b8f18716283d2d4927672e0e9e25193d7f7
# Parent  914baafb3da4176b9656f298afa56ac2a0a5967b
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas

diff -r 914baafb3da4 -r 82b00b8f1871 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 11 14:18:34 2020 +0200
+++ b/src/HOL/List.thy	Thu Jun 11 16:13:53 2020 +0100
@@ -6326,7 +6326,6 @@
     by (metis DomainE Int_emptyI RangeE lexn_length)
 qed
 
-
 lemma lexn_conv:
   "lexn r n =
     {(xs,ys). length xs = n \<and> length ys = n \<and>
@@ -6516,7 +6515,6 @@
   by (meson irrefl_def lex_take_index)
 
 
-
 subsubsection \<open>Lexicographic Ordering\<close>
 
 text \<open>Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
@@ -6618,11 +6616,11 @@
 qed
 
 lemma lexord_trans:
-    "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
-by(auto simp: trans_def intro:lexord_partial_trans)
+  "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
+  by(auto simp: trans_def intro:lexord_partial_trans)
 
 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
-by (rule transI, drule lexord_trans, blast)
+  by (meson lexord_trans transI)
 
 lemma total_lexord: "total r \<Longrightarrow> total (lexord r)"
   unfolding total_on_def
@@ -6653,10 +6651,7 @@
 lemma lexord_asym:
   assumes "asym R"
   shows "asym (lexord R)"
-proof
-  from assms obtain "irrefl R" by (blast elim: asym.cases)
-  then show "irrefl (lexord R)" by (rule lexord_irrefl)
-next
+proof 
   fix xs ys
   assume "(xs, ys) \<in> lexord R"
   then show "(ys, xs) \<notin> lexord R"
@@ -6679,6 +6674,38 @@
   then show ?thesis by (rule asym.cases) (auto simp add: hyp)
 qed
 
+lemma asym_lex: "asym R \<Longrightarrow> asym (lex R)"
+  by (meson asym.simps irrefl_lex lexord_asym lexord_lex)
+
+lemma asym_lenlex: "asym R \<Longrightarrow> asym (lenlex R)"
+  by (simp add: lenlex_def asym_inv_image asym_less_than asym_lex asym_lex_prod)
+
+lemma lenlex_append1:
+  assumes len: "(us,xs) \<in> lenlex R" and eq: "length vs = length ys" 
+  shows "(us @ vs, xs @ ys) \<in> lenlex R"
+  using len
+proof (induction us)
+  case Nil
+  then show ?case 
+    by (simp add: lenlex_def eq)
+next
+  case (Cons u us)
+  with lex_append_rightI show ?case
+    by (fastforce simp add: lenlex_def eq)
+qed
+
+lemma lenlex_append2 [simp]:
+  assumes "irrefl R"
+  shows "(us @ xs, us @ ys) \<in> lenlex R \<longleftrightarrow> (xs, ys) \<in> lenlex R"
+proof (induction us)
+  case Nil
+  then show ?case 
+    by (simp add: lenlex_def)
+next
+  case (Cons u us)
+  with assms show ?case
+    by (auto simp: lenlex_def irrefl_def)
+qed
 
 text \<open>
   Predicate version of lexicographic order integrated with Isabelle's order type classes.
diff -r 914baafb3da4 -r 82b00b8f1871 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Jun 11 14:18:34 2020 +0200
+++ b/src/HOL/Relation.thy	Thu Jun 11 16:13:53 2020 +0100
@@ -245,14 +245,19 @@
 subsubsection \<open>Asymmetry\<close>
 
 inductive asym :: "'a rel \<Rightarrow> bool"
-  where asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
+  where asymI: "(\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
 
 inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
+  where asympI: "(\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
 
 lemma asymp_asym_eq [pred_set_conv]: "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R"
   by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)
 
+lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R"
+  by (simp add: asym.simps)
+
+lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
+  by (blast intro: asymI dest: asymD)
 
 subsubsection \<open>Symmetry\<close>
 
@@ -1136,6 +1141,9 @@
 lemma total_inv_image: "\<lbrakk>inj f; total r\<rbrakk> \<Longrightarrow> total (inv_image r f)"
   unfolding inv_image_def total_on_def by (auto simp: inj_eq)
 
+lemma asym_inv_image: "asym R \<Longrightarrow> asym (inv_image R f)"
+  by (simp add: inv_image_def asym_iff)
+
 lemma in_inv_image[simp]: "(x, y) \<in> inv_image r f \<longleftrightarrow> (f x, f y) \<in> r"
   by (auto simp: inv_image_def)
 
diff -r 914baafb3da4 -r 82b00b8f1871 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Jun 11 14:18:34 2020 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Jun 11 16:13:53 2020 +0100
@@ -583,6 +583,9 @@
 lemma irrefl_less_than: "irrefl less_than"
   using irrefl_def by blast
 
+lemma asym_less_than: "asym less_than"
+  by (simp add: asym.simps irrefl_less_than)
+
 lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
   using total_on_def by force+
 
@@ -798,6 +801,9 @@
 lemma total_on_lex_prod [simp]: "total_on A r \<Longrightarrow> total_on B s \<Longrightarrow> total_on (A \<times> B) (r <*lex*> s)"
   by (auto simp: total_on_def)
 
+lemma asym_lex_prod: "\<lbrakk>asym R; asym S\<rbrakk> \<Longrightarrow> asym (R <*lex*> S)"
+  by (auto simp add: asym_iff lex_prod_def)
+
 lemma total_lex_prod [simp]: "total r \<Longrightarrow> total s \<Longrightarrow> total (r <*lex*> s)"
   by (auto simp: total_on_def)