# HG changeset patch
# User haftmann
# Date 1656921443 0
# Node ID aa0403e5535fda8fe60a974e033bd5e414546547
# Parent  34cd1d210b92eda0cb78d9e2b8bf38535a3c9301
more complete set of code equations

diff -r 34cd1d210b92 -r aa0403e5535f src/HOL/Library/Subseq_Order.thy
--- a/src/HOL/Library/Subseq_Order.thy	Mon Jul 04 07:57:22 2022 +0000
+++ b/src/HOL/Library/Subseq_Order.thy	Mon Jul 04 07:57:23 2022 +0000
@@ -20,8 +20,11 @@
 instantiation list :: (type) ord
 begin
 
-definition "xs \<le> ys \<longleftrightarrow> subseq xs ys" for xs ys :: "'a list"
-definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
+definition less_eq_list
+  where \<open>xs \<le> ys \<longleftrightarrow> subseq xs ys\<close> for xs ys :: \<open>'a list\<close>
+
+definition less_list
+  where \<open>xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs\<close> for xs ys :: \<open>'a list\<close>
 
 instance ..
 
@@ -44,8 +47,36 @@
 
 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
   list_emb.induct [of "(=)", folded less_eq_list_def]
+
+lemma less_eq_list_empty [code]:
+  \<open>[] \<le> xs \<longleftrightarrow> True\<close>
+  by (simp add: less_eq_list_def)
+
+lemma less_eq_list_below_empty [code]:
+  \<open>x # xs \<le> [] \<longleftrightarrow> False\<close>
+  by (simp add: less_eq_list_def)
+
+lemma le_list_Cons2_iff [simp, code]:
+  \<open>x # xs \<le> y # ys \<longleftrightarrow> (if x = y then xs \<le> ys else x # xs \<le> ys)\<close>
+  by (simp add: less_eq_list_def)
+
+lemma less_list_empty [simp]:
+  \<open>[] < xs \<longleftrightarrow> xs \<noteq> []\<close>
+  by (metis less_eq_list_def list_emb_Nil order_less_le)
+
+lemma less_list_empty_Cons [code]:
+  \<open>[] < x # xs \<longleftrightarrow> True\<close>
+  by simp_all
+
+lemma less_list_below_empty [simp, code]:
+  \<open>xs < [] \<longleftrightarrow> False\<close>
+  by (metis list_emb_Nil less_eq_list_def less_list_def)
+
+lemma less_list_Cons2_iff [code]:
+  \<open>x # xs < y # ys \<longleftrightarrow> (if x = y then xs < ys else x # xs \<le> ys)\<close>
+  by (simp add: less_le)
+
 lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "(=)", folded less_eq_list_def]
-lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def]
 lemmas le_list_map = subseq_map [folded less_eq_list_def]
 lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
 lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def]
@@ -53,12 +84,6 @@
 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def)
 
-lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
-  by (metis less_eq_list_def list_emb_Nil order_less_le)
-
-lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
-  by (metis list_emb_Nil less_eq_list_def less_list_def)
-
 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   by (unfold less_le less_eq_list_def) (auto)