# HG changeset patch
# User haftmann
# Date 1655885710 0
# Node ID 36965f6b3530756824c8a3f8e2d777ed7fe35407
# Parent  d078f848215521ff36ce8eb5b6816d528daeab4e
Executable lexords.

diff -r d078f8482155 -r 36965f6b3530 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 22 08:15:09 2022 +0000
+++ b/src/HOL/List.thy	Wed Jun 22 08:15:10 2022 +0000
@@ -5966,6 +5966,9 @@
 lemma sorted_enumerate [simp]: "sorted (map fst (enumerate n xs))"
 by (simp add: enumerate_eq_zip)
 
+lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
+ by (induct xs) (auto dest!: insort_is_Cons)
+
 text \<open>Stability of \<^const>\<open>sort_key\<close>:\<close>
 
 lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
@@ -7011,7 +7014,7 @@
 
 end
 
-lemma lexordp_simps [simp]:
+lemma lexordp_simps [simp, code]:
   "lexordp [] ys = (ys \<noteq> [])"
   "lexordp xs [] = False"
   "lexordp (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp xs ys"
@@ -7022,7 +7025,7 @@
 | Cons: "x < y \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
 | Cons_eq: "\<lbrakk> \<not> x < y; \<not> y < x; lexordp_eq xs ys \<rbrakk> \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
 
-lemma lexordp_eq_simps [simp]:
+lemma lexordp_eq_simps [simp, code]:
   "lexordp_eq [] ys = True"
   "lexordp_eq xs [] \<longleftrightarrow> xs = []"
   "lexordp_eq (x # xs) [] = False"
@@ -7062,7 +7065,7 @@
 end
 
 declare ord.lexordp_simps [simp, code]
-declare ord.lexordp_eq_simps [code, simp]
+declare ord.lexordp_eq_simps [simp, code]
 
 context order
 begin
@@ -7155,9 +7158,6 @@
 
 end
 
-lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
- by (induct xs) (auto dest!: insort_is_Cons)
-
 
 subsubsection \<open>Lexicographic combination of measure functions\<close>