Executable lexords.
--- 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>