# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1598010177 -3600
# Node ID 881bd98bddee8f901c356cbc1694137fb3a82a7a
# Parent  6f20a44c3cb173f931a512c54536b50ab62000f0
reversing all the lex crap

diff -r 6f20a44c3cb1 -r 881bd98bddee src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -167,7 +167,7 @@
 (*<*)unfolding lexordp_def by (auto simp add: append)(*>*)
 
 lemma %quote [code_pred_intro]:
-  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b \<Longrightarrow> a\<noteq>b 
+  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b
   \<Longrightarrow> lexordp r xs ys"
 (*<*)unfolding lexordp_def append apply simp
 apply (rule disjI2) by auto(*>*)
@@ -179,14 +179,14 @@
   assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
     \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
   assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
-    \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> a\<noteq>b \<Longrightarrow> thesis"
+    \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis"
   {
     assume "\<exists>a v. ys = xs @ a # v"
     from this 1 have thesis
         by (fastforce simp add: append)
   } moreover
   {
-    assume "\<exists>u a b v w. r a b \<and> a\<noteq>b \<and> xs = u @ a # v \<and> ys = u @ b # w"
+    assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w"
     from this 2 have thesis by (fastforce simp add: append)
   } moreover
   note lexord
diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/Corec_Examples/Stream_Processor.thy
--- a/src/HOL/Corec_Examples/Stream_Processor.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Corec_Examples/Stream_Processor.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -61,26 +61,20 @@
 lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)"
   by (subst copy.code; simp)
 
-lemma wf_imp_irrefl:
-  assumes "wf r" shows "irrefl r" 
-  using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
-
-
 corecursive sp_comp (infixl "oo" 65) where
   "sp oo sp' = (case (out sp, out sp') of
       (Put b sp, _) \<Rightarrow> In (Put b (sp oo sp'))
     | (Get f, Put b sp) \<Rightarrow> In (f b) oo sp
     | (_, Get g) \<Rightarrow> get (\<lambda>a. (sp oo In (g a))))"
-  apply(relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
-    apply(auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
-  by (metis Get_neq)
+  by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
+    (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
 
 lemma run_copy_unique:
-  "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
-  apply corec_unique
-  apply(rule ext)
-  apply(subst copy.code)
-  apply simp
-  done
+    "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
+apply corec_unique
+apply(rule ext)
+apply(subst copy.code)
+apply simp
+done
 
 end
diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Fun_Def.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -208,7 +208,7 @@
   by (auto simp: pair_less_def)
 
 lemma total_pair_less [iff]: "total_on A pair_less" and trans_pair_less [iff]: "trans pair_less"
-  by (auto simp: total_on_def pair_less_def antisym_def)
+  by (auto simp: total_on_def pair_less_def)
 
 text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
 lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/Library/List_Lenlexorder.thy
--- a/src/HOL/Library/List_Lenlexorder.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Library/List_Lenlexorder.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -25,20 +25,17 @@
 proof
   have tr: "trans {(u, v::'a). u < v}"
     using trans_def by fastforce
-  have ant: "antisym {(u, v::'a). u < v}"
-    using antisym_def order.asym by auto
   have \<section>: False
     if "(xs,ys) \<in> lenlex {(u, v). u < v}" "(ys,xs) \<in> lenlex {(u, v). u < v}" for xs ys :: "'a list"
   proof -
     have "(xs,xs) \<in> lenlex {(u, v). u < v}"
-      using that ant transD [OF lenlex_transI [OF tr]] by blast
+      using that transD [OF lenlex_transI [OF tr]] by blast
     then show False
       by (meson case_prodD lenlex_irreflexive less_irrefl mem_Collect_eq)
   qed
   show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def)
   show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list"
-    using that ant transD [OF lenlex_transI [OF tr]]
-    by (auto simp add: list_le_def list_less_def)
+    using that transD [OF lenlex_transI [OF tr]] by (auto simp add: list_le_def list_less_def)
   show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list"
     using \<section> that list_le_def list_less_def by blast
   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
@@ -72,12 +69,19 @@
 lemma Nil_less_Cons [simp]: "[] < a # x"
   by (simp add: list_less_def)
 
+lemma Cons_less_Cons: "a # x < b # y \<longleftrightarrow> length x < length y \<or> length x = length y \<and> (a < b \<or> a = b \<and> x < y)"
+  using lenlex_length
+  by (fastforce simp: list_less_def Cons_lenlex_iff)
+
 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
   unfolding list_le_def by (cases x) auto
 
 lemma Nil_le_Cons [simp]: "[] \<le> x"
   unfolding list_le_def by (cases x) auto
 
+lemma Cons_le_Cons: "a # x \<le> b # y \<longleftrightarrow> length x < length y \<or> length x = length y \<and> (a < b \<or> a = b \<and> x \<le> y)"
+  by (auto simp: list_le_def Cons_less_Cons)
+
 instantiation list :: (order) order_bot
 begin
 
@@ -88,15 +92,4 @@
 
 end
 
-lemma Cons_less_Cons: 
-  fixes a :: "'a::order"
-  shows "a # xs < b # ys \<longleftrightarrow> length xs < length ys \<or> length xs = length ys \<and> (a < b \<or> a = b \<and> xs < ys)"
-  using lenlex_length
-  by (fastforce simp: list_less_def Cons_lenlex_iff)
-
-lemma Cons_le_Cons:
-  fixes a :: "'a::order"
-  shows "a # xs \<le> b # ys \<longleftrightarrow> length xs < length ys \<or> length xs = length ys \<and> (a < b \<or> a = b \<and> xs \<le> ys)"
-  by (auto simp: list_le_def Cons_less_Cons)
-
 end
diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/Library/List_Lexorder.thy
--- a/src/HOL/Library/List_Lexorder.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Library/List_Lexorder.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -26,20 +26,17 @@
   let ?r = "{(u, v::'a). u < v}"
   have tr: "trans ?r"
     using trans_def by fastforce
-  have *: "antisym {(u, v::'a). u < v}"
-    using antisym_def by fastforce
   have \<section>: False
     if "(xs,ys) \<in> lexord ?r" "(ys,xs) \<in> lexord ?r" for xs ys :: "'a list"
   proof -
     have "(xs,xs) \<in> lexord ?r"
-      using lexord_trans that tr * by blast
+      using that transD [OF lexord_transI [OF tr]] by blast
     then show False
       by (meson case_prodD lexord_irreflexive less_irrefl mem_Collect_eq)
   qed
   show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def)
   show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list"
-    using that transD [OF lexord_transI [OF tr]] *
-    by (auto simp add: list_le_def list_less_def)
+    using that transD [OF lexord_transI [OF tr]] by (auto simp add: list_le_def list_less_def)
   show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list"
     using \<section> that list_le_def list_less_def by blast
   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
@@ -73,7 +70,7 @@
 lemma Nil_less_Cons [simp]: "[] < a # x"
   by (simp add: list_less_def)
 
-lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> (if a = b then x < y else a < b)"
+lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
   by (simp add: list_less_def)
 
 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
@@ -82,7 +79,7 @@
 lemma Nil_le_Cons [simp]: "[] \<le> x"
   unfolding list_le_def by (cases x) auto
 
-lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> (if a = b then x \<le> y else a < b)"
+lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
   unfolding list_le_def by auto
 
 instantiation list :: (order) order_bot
diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/List.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -6348,11 +6348,11 @@
 lemma lexn_conv:
   "lexn r n =
     {(xs,ys). length xs = n \<and> length ys = n \<and>
-    (\<exists>xys x y xs' ys'. xs = xys @ x#xs' \<and> ys = xys @ y # ys' \<and> x\<noteq>y \<and> (x,y) \<in> r)}"
+    (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"
 proof (induction n)
   case (Suc n)
-  show ?case
-    apply (simp add: Suc image_Collect lex_prod_def, safe, blast)
+  then show ?case
+    apply (simp add: image_Collect lex_prod_def, safe, blast)
      apply (rule_tac x = "ab # xys" in exI, simp)
     apply (case_tac xys; force)
     done
@@ -6360,7 +6360,7 @@
 
 text\<open>By Mathias Fleury:\<close>
 proposition lexn_transI:
-  assumes "trans r" "antisym r" shows "trans (lexn r n)"
+  assumes "trans r" shows "trans (lexn r n)"
 unfolding trans_def
 proof (intro allI impI)
   fix as bs cs
@@ -6369,13 +6369,13 @@
     n: "length as = n" and "length bs = n" and
     as: "as = abs @ a # as'" and
     bs: "bs = abs @ b # bs'" and
-    abr: "(a, b) \<in> r" "a\<noteq>b"
+    abr: "(a, b) \<in> r"
     using asbs unfolding lexn_conv by blast
   obtain bcs b' c' cs' bs' where
     n': "length cs = n" and "length bs = n" and
     bs': "bs = bcs @ b' # bs'" and
     cs: "cs = bcs @ c' # cs'" and
-    b'c'r: "(b', c') \<in> r" "b'\<noteq>c'"
+    b'c'r: "(b', c') \<in> r"
     using bscs unfolding lexn_conv by blast
   consider (le) "length bcs < length abs"
     | (eq) "length bcs = length abs"
@@ -6385,7 +6385,7 @@
     let ?k = "length bcs"
     case le
     hence "as ! ?k = bs ! ?k" unfolding as bs by (simp add: nth_append)
-    hence "(as ! ?k, cs ! ?k) \<in> r" "as ! ?k \<noteq> cs ! ?k" using b'c'r unfolding bs' cs by auto
+    hence "(as ! ?k, cs ! ?k) \<in> r" using b'c'r unfolding bs' cs by auto
     moreover
     have "length bcs < length as" using le unfolding as by simp
     from id_take_nth_drop[OF this]
@@ -6397,12 +6397,12 @@
     moreover have "take ?k as = take ?k cs"
       using le arg_cong[OF bs, of "take (length bcs)"]
       unfolding cs as bs' by auto
-    ultimately show ?thesis using n n' \<open>b'\<noteq>c'\<close> unfolding lexn_conv by auto
+    ultimately show ?thesis using n n' unfolding lexn_conv by auto
   next
     let ?k = "length abs"
     case ge
     hence "bs ! ?k = cs ! ?k" unfolding bs' cs by (simp add: nth_append)
-    hence "(as ! ?k, cs ! ?k) \<in> r" "as ! ?k \<noteq> cs ! ?k" using abr unfolding as bs by auto
+    hence "(as ! ?k, cs ! ?k) \<in> r" using abr unfolding as bs by auto
     moreover
     have "length abs < length as" using ge unfolding as by simp
     from id_take_nth_drop[OF this]
@@ -6418,23 +6418,21 @@
     let ?k = "length abs"
     case eq
     hence *: "abs = bcs" "b = b'" using bs bs' by auto
-    then have "a\<noteq>c'"
-      using abr(1) antisymD assms(2) b'c'r(1) b'c'r(2) by fastforce
-    have "(a, c') \<in> r"
-      using * abr b'c'r assms unfolding trans_def by blast
-    with * \<open>a\<noteq>c'\<close> show ?thesis using n n' unfolding lexn_conv as bs cs by auto
+    hence "(a, c') \<in> r"
+      using abr b'c'r assms unfolding trans_def by blast
+    with * show ?thesis using n n' unfolding lexn_conv as bs cs by auto
   qed
 qed
 
 corollary lex_transI:
-    assumes "trans r" "antisym r" shows "trans (lex r)"
+    assumes "trans r" shows "trans (lex r)"
   using lexn_transI [OF assms]
   by (clarsimp simp add: lex_def trans_def) (metis lexn_length)
 
 lemma lex_conv:
   "lex r =
     {(xs,ys). length xs = length ys \<and>
-    (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> x\<noteq>y \<and> (x,y) \<in> r)}"
+    (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y) \<in> r)}"
 by (force simp add: lex_def lexn_conv)
 
 lemma wf_lenlex [intro!]: "wf r \<Longrightarrow> wf (lenlex r)"
@@ -6457,15 +6455,15 @@
     then consider "(x,y) \<in> r" | "(y,x) \<in> r"
       by (meson UNIV_I assms total_on_def)
     then show ?thesis
-    by cases (use len \<open>x\<noteq>y\<close> in \<open>(force simp add: lexn_conv xs ys)+\<close>)
+    by cases (use len in \<open>(force simp add: lexn_conv xs ys)+\<close>)
 qed
   then show ?thesis
     by (fastforce simp: lenlex_def total_on_def lex_def)
 qed
 
-lemma lenlex_transI [intro]: "\<lbrakk>trans r; antisym r\<rbrakk> \<Longrightarrow> trans (lenlex r)"
+lemma lenlex_transI [intro]: "trans r \<Longrightarrow> trans (lenlex r)"
   unfolding lenlex_def
-  by (simp add: antisym_def lex_transI trans_inv_image)
+  by (meson lex_transI trans_inv_image trans_less_than trans_lex_prod)
 
 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
   by (simp add: lex_conv)
@@ -6474,8 +6472,8 @@
   by (simp add:lex_conv)
 
 lemma Cons_in_lex [simp]:
-  "(x # xs, y # ys) \<in> lex r \<longleftrightarrow> x\<noteq>y \<and> (x,y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r"
-  (is "?lhs = ?rhs")
+  "(x # xs, y # ys) \<in> lex r \<longleftrightarrow> (x, y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r"
+ (is "?lhs = ?rhs")
 proof
   assume ?lhs then show ?rhs
     by (simp add: lex_conv) (metis hd_append list.sel(1) list.sel(3) tl_append2)
@@ -6491,7 +6489,7 @@
 lemma Cons_lenlex_iff: 
   "((m # ms, n # ns) \<in> lenlex r) \<longleftrightarrow> 
     length ms < length ns 
-  \<or> length ms = length ns \<and> m\<noteq>n \<and> (m,n) \<in> r 
+  \<or> length ms = length ns \<and> (m,n) \<in> r 
   \<or> (m = n \<and> (ms,ns) \<in> lenlex r)"
   by (auto simp: lenlex_def)
 
@@ -6499,7 +6497,7 @@
   by (induction xs) (auto simp add: Cons_lenlex_iff)
 
 lemma lenlex_trans:
-    "\<lbrakk>(x,y) \<in> lenlex r; (y,z) \<in> lenlex r; trans r; antisym r\<rbrakk> \<Longrightarrow> (x,z) \<in> lenlex r"
+    "\<lbrakk>(x,y) \<in> lenlex r; (y,z) \<in> lenlex r; trans r\<rbrakk> \<Longrightarrow> (x,z) \<in> lenlex r"
   by (meson lenlex_transI transD)
 
 lemma lenlex_length: "(ms, ns) \<in> lenlex r \<Longrightarrow> length ms \<le> length ns"
@@ -6547,30 +6545,23 @@
 
 definition lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
 "lexord r = {(x,y). \<exists> a v. y = x @ a # v \<or>
-            (\<exists> u a b v w. (a,b) \<in> r \<and> a\<noteq>b \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
-
+            (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
 
 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
-  by (unfold lexord_def, induct_tac y, auto)
+by (unfold lexord_def, induct_tac y, auto)
 
 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
-  by (unfold lexord_def, induct_tac x, auto)
+by (unfold lexord_def, induct_tac x, auto)
 
 lemma lexord_cons_cons[simp]:
-  "(a # x, b # y) \<in> lexord r \<longleftrightarrow> (if a=b then (x,y)\<in> lexord r else (a,b)\<in> r)"  (is "?lhs = ?rhs")
+  "(a # x, b # y) \<in> lexord r \<longleftrightarrow> (a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r)"  (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs
     apply (simp add: lexord_def)
     apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
     done
-next
-  assume ?rhs
-  then show ?lhs
-    apply (simp add: lexord_def split: if_split_asm)
-    apply (meson Cons_eq_appendI)
-    by blast
-qed 
+qed (auto simp add: lexord_def; (blast | meson Cons_eq_appendI))
 
 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
 
@@ -6578,7 +6569,7 @@
   by (induct_tac x, auto)
 
 lemma lexord_append_left_rightI:
-  "\<lbrakk>(a,b) \<in> r; a\<noteq>b\<rbrakk> \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
+  "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
   by (induct_tac u, auto)
 
 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
@@ -6591,13 +6582,13 @@
 lemma lexord_take_index_conv:
    "((x,y) \<in> lexord r) =
     ((length x < length y \<and> take (length x) y = x) \<or>
-     (\<exists>i. i < min(length x)(length y) \<and> take i x = take i y \<and> (x!i,y!i) \<in> r \<and> x!i \<noteq> y!i))"
+     (\<exists>i. i < min(length x)(length y) \<and> take i x = take i y \<and> (x!i,y!i) \<in> r))"
 proof -
   have "(\<exists>a v. y = x @ a # v) = (length x < length y \<and> take (length x) y = x)"
     by (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le)
   moreover
-  have "(\<exists>u a b. (a,b) \<in> r \<and> a\<noteq>b \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
-        (\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r \<and> x!i \<noteq> y!i)"
+  have "(\<exists>u a b. (a, b) \<in> r \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
+        (\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r)"
     apply safe
     using less_iff_Suc_add apply auto[1]
     by (metis id_take_nth_drop)
@@ -6613,12 +6604,10 @@
 qed auto
 
 lemma lexord_irreflexive: "\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
-  by (induct xs) auto
+by (induct xs) auto
 
 text\<open>By Ren\'e Thiemann:\<close>
 lemma lexord_partial_trans:
-  assumes "antisym r"
-  shows
   "(\<And>x y z. x \<in> set xs \<Longrightarrow> (x,y) \<in> r \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> (x,z) \<in> r)
    \<Longrightarrow>  (xs,ys) \<in> lexord r  \<Longrightarrow>  (ys,zs) \<in> lexord r \<Longrightarrow>  (xs,zs) \<in> lexord r"
 proof (induct xs arbitrary: ys zs)
@@ -6629,13 +6618,11 @@
   from Cons(3) obtain y ys where yys: "yys = y # ys" unfolding lexord_def
     by (cases yys, auto)
   note Cons = Cons[unfolded yys]
-  from Cons(3) have one: "x\<noteq>y \<and> (x,y) \<in> r \<or> x = y \<and> (xs,ys) \<in> lexord r"
-    by (auto split: if_split_asm)
+  from Cons(3) have one: "(x,y) \<in> r \<or> x = y \<and> (xs,ys) \<in> lexord r" by auto
   from Cons(4) obtain z zs where zzs: "zzs = z # zs" unfolding lexord_def
     by (cases zzs, auto)
   note Cons = Cons[unfolded zzs]
-  from Cons(4) have two: "y \<noteq> z \<and> (y,z) \<in> r \<or> y = z \<and> (ys,zs) \<in> lexord r" 
-    by (auto split: if_split_asm)
+  from Cons(4) have two: "(y,z) \<in> r \<or> y = z \<and> (ys,zs) \<in> lexord r" by auto
   {
     assume "(xs,ys) \<in> lexord r" and "(ys,zs) \<in> lexord r"
     from Cons(1)[OF _ this] Cons(2)
@@ -6646,16 +6633,15 @@
     from Cons(2)[OF _ this] have "(x,z) \<in> r" by auto
   } note ind2 = this
   from one two ind1 ind2
-  have "x\<noteq>z \<and> (x,z) \<in> r \<or> x = z \<and> (xs,zs) \<in> lexord r"
-    using assms by (auto simp: antisym_def)
-  thus ?case unfolding zzs by (auto split: if_split_asm)
+  have "(x,z) \<in> r \<or> x = z \<and> (xs,zs) \<in> lexord r" by blast
+  thus ?case unfolding zzs by auto
 qed
 
 lemma lexord_trans:
-  "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r; antisym r\<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
-  by(auto simp: trans_def intro: lexord_partial_trans)
-
-lemma lexord_transI:  "\<lbrakk>trans r; antisym r\<rbrakk> \<Longrightarrow> trans (lexord r)"
+  "\<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 (meson lexord_trans transI)
 
 lemma total_lexord: "total r \<Longrightarrow> total (lexord r)"
@@ -6673,7 +6659,7 @@
       by (metis lexord_Nil_left list.exhaust)
   next
     case (Cons a x y) then show ?case
-      by (metis eq_Nil_appendI lexord_append_rightI lexord_cons_cons list.exhaust)
+      by (cases y) (force+)
   qed
 qed
 
@@ -6860,7 +6846,7 @@
 
 lemma lexordp_conv_lexord:
   "lexordp xs ys \<longleftrightarrow> (xs, ys) \<in> lexord {(x, y). x < y}"
-  by (simp add: lexordp_iff lexord_def; blast)
+by(simp add: lexordp_iff lexord_def)
 
 lemma lexordp_eq_antisym:
   assumes "lexordp_eq xs ys" "lexordp_eq ys xs"
@@ -7415,8 +7401,8 @@
 lemma [code]:
   "lexordp r xs [] = False"
   "lexordp r [] (y#ys) = True"
-  "lexordp r (x # xs) (y # ys) = (if x = y then lexordp r xs ys else r x y)"
-  unfolding lexordp_def by auto
+  "lexordp r (x # xs) (y # ys) = (r x y \<or> (x = y \<and> lexordp r xs ys))"
+unfolding lexordp_def by auto
 
 text \<open>Bounded quantification and summation over nats.\<close>
 
diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -327,10 +327,6 @@
     done
 qed
 
-(*for lex*)
-lemma ne_lesssub_iff [simp]: "y\<noteq>x \<and> x <[r] y \<longleftrightarrow> x <[r] y"
-  by (meson lesssub_def)
-
 lemma iter_properties[rule_format]:
   assumes semilat: "semilat (A, r, f)"
   shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Wellfounded.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -770,13 +770,9 @@
 
 definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
     (infixr "<*lex*>" 80)
-    where "ra <*lex*> rb = {((a, b), (a', b')). a \<noteq> a' \<and> (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
+    where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
 
-lemma in_lex_prod[simp]: "NO_MATCH less_than r \<Longrightarrow> ((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> a \<noteq> a' \<and> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
-  by (auto simp:lex_prod_def)
-
-text\<open>compared with @{thm[source]in_lex_prod} this yields simpler results\<close>
-lemma in_lex_prod_less_than[simp]: "((a, b), (a', b')) \<in> less_than <*lex*> s \<longleftrightarrow>a<a' \<or> a = a' \<and> (b, b') \<in> s"
+lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
   by (auto simp:lex_prod_def)
 
 lemma wf_lex_prod [intro!]:
@@ -803,9 +799,8 @@
 qed auto
 
 text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
-lemma trans_lex_prod [simp,intro!]: "\<lbrakk>trans R1; trans R2; antisym R1\<rbrakk> \<Longrightarrow> trans (R1 <*lex*> R2)"
-  unfolding trans_def antisym_def lex_prod_def by blast
-
+lemma trans_lex_prod [simp,intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
+  unfolding trans_def lex_prod_def by blast
 
 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)