--- a/NEWS Thu Jun 23 21:50:32 2022 +0200
+++ b/NEWS Thu Jun 23 22:16:53 2022 +0200
@@ -34,6 +34,9 @@
*** HOL ***
+* Theory Char_ord: streamlined logical specifications.
+Minor INCOMPATIBILITY.
+
* Rule split_of_bool_asm is not split any longer, analogously to
split_if_asm. INCOMPATIBILITY.
--- a/src/HOL/Library/Char_ord.thy Thu Jun 23 21:50:32 2022 +0200
+++ b/src/HOL/Library/Char_ord.thy Thu Jun 23 22:16:53 2022 +0200
@@ -8,14 +8,93 @@
imports Main
begin
+context linordered_semidom
+begin
+
+lemma horner_sum_nonnegative:
+ \<open>0 \<le> horner_sum of_bool 2 bs\<close>
+ by (induction bs) simp_all
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_bound:
+ \<open>horner_sum of_bool 2 bs < 2 ^ length bs\<close>
+proof (induction bs)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons b bs)
+ moreover define a where \<open>a = 2 ^ length bs - horner_sum of_bool 2 bs\<close>
+ ultimately have *: \<open>2 ^ length bs = horner_sum of_bool 2 bs + a\<close>
+ by simp
+ have \<open>1 < a * 2\<close> if \<open>0 < a\<close>
+ using that add_mono [of 1 a 1 a]
+ by (simp add: mult_2_right discrete)
+ with Cons show ?case
+ by (simp add: algebra_simps *)
+qed
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_less_eq_iff_lexordp_eq:
+ \<open>horner_sum of_bool 2 bs \<le> horner_sum of_bool 2 cs \<longleftrightarrow> lexordp_eq (rev bs) (rev cs)\<close>
+ if \<open>length bs = length cs\<close>
+proof -
+ have \<open>horner_sum of_bool 2 (rev bs) \<le> horner_sum of_bool 2 (rev cs) \<longleftrightarrow> lexordp_eq bs cs\<close>
+ if \<open>length bs = length cs\<close> for bs cs
+ using that proof (induction bs cs rule: list_induct2)
+ case Nil
+ then show ?case
+ by simp
+ next
+ case (Cons b bs c cs)
+ with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+ horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+ show ?case
+ by (auto simp add: horner_sum_append not_le Cons intro: add_strict_increasing2 add_increasing)
+ qed
+ from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+ by simp
+qed
+
+lemma horner_sum_less_iff_lexordp:
+ \<open>horner_sum of_bool 2 bs < horner_sum of_bool 2 cs \<longleftrightarrow> ord_class.lexordp (rev bs) (rev cs)\<close>
+ if \<open>length bs = length cs\<close>
+proof -
+ have \<open>horner_sum of_bool 2 (rev bs) < horner_sum of_bool 2 (rev cs) \<longleftrightarrow> ord_class.lexordp bs cs\<close>
+ if \<open>length bs = length cs\<close> for bs cs
+ using that proof (induction bs cs rule: list_induct2)
+ case Nil
+ then show ?case
+ by simp
+ next
+ case (Cons b bs c cs)
+ with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+ horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+ show ?case
+ by (auto simp add: horner_sum_append not_less Cons intro: add_strict_increasing2 add_increasing)
+ qed
+ from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+ by simp
+qed
+
+end
+
instantiation char :: linorder
begin
-definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
- where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
+definition less_eq_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
+ where \<open>c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)\<close>
-definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
- where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
+definition less_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
+ where \<open>c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)\<close>
instance
@@ -23,23 +102,21 @@
end
-lemma less_eq_char_simp [simp]:
- "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
- \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
- \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
- by (simp add: less_eq_char_def)
+lemma less_eq_char_simp [simp, code]:
+ \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
+ \<longleftrightarrow> lexordp_eq [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
+ by (simp only: less_eq_char_def of_char_def char.sel horner_sum_less_eq_iff_lexordp_eq list.size) simp
-lemma less_char_simp [simp]:
- "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
- \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
- < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
- by (simp add: less_char_def)
+lemma less_char_simp [simp, code]:
+ \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
+ \<longleftrightarrow> ord_class.lexordp [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
+ by (simp only: less_char_def of_char_def char.sel horner_sum_less_iff_lexordp list.size) simp
instantiation char :: distrib_lattice
begin
-definition "(inf :: char \<Rightarrow> _) = min"
-definition "(sup :: char \<Rightarrow> _) = max"
+definition \<open>(inf :: char \<Rightarrow> _) = min\<close>
+definition \<open>(sup :: char \<Rightarrow> _) = max\<close>
instance
by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
--- a/src/HOL/List.thy Thu Jun 23 21:50:32 2022 +0200
+++ b/src/HOL/List.thy Thu Jun 23 22:16:53 2022 +0200
@@ -2247,13 +2247,13 @@
lemma butlast_take:
"n \<le> length xs \<Longrightarrow> butlast (take n xs) = take (n - 1) xs"
- by (simp add: butlast_conv_take min.absorb1 min.absorb2)
+ by (simp add: butlast_conv_take)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
by (simp add: butlast_conv_take drop_take ac_simps)
lemma take_butlast: "n < length xs \<Longrightarrow> take n (butlast xs) = take n xs"
- by (simp add: butlast_conv_take min.absorb1)
+ by (simp add: butlast_conv_take)
lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
by (simp add: butlast_conv_take drop_take ac_simps)
@@ -2374,7 +2374,7 @@
qed auto
lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
- by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
+ by (simp add: set_conv_nth) force
subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
@@ -2808,7 +2808,7 @@
proof (induction "zip xs (zip ys zs)" arbitrary: xs ys zs)
case Nil
from Nil [symmetric] show ?case
- by (auto simp add: zip_eq_Nil_iff)
+ by auto
next
case (Cons xyz xyzs)
from Cons.hyps(2) [symmetric] show ?case
@@ -2820,7 +2820,7 @@
proof (induction "zip xs ys" arbitrary: xs ys)
case Nil
then show ?case
- by (auto simp add: zip_eq_Nil_iff dest: sym)
+ by auto
next
case (Cons xy xys)
from Cons.hyps(2) [symmetric] show ?case
@@ -3702,8 +3702,9 @@
proof (induct xs)
case (Cons x xs)
show ?case
- apply (auto simp add: Cons nth_Cons split: nat.split_asm)
- apply (metis Suc_less_eq2 in_set_conv_nth less_not_refl zero_less_Suc)+
+ apply (auto simp add: Cons nth_Cons less_Suc_eq_le split: nat.split_asm)
+ apply (metis Suc_leI in_set_conv_nth length_pos_if_in_set lessI less_imp_le_nat less_nat_zero_code)
+ apply (metis Suc_le_eq)
done
qed auto
@@ -5256,8 +5257,8 @@
case (Suc j)
have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
- { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
- by (cases x) simp_all
+ { fix xs :: \<open>'a list\<close> have "Suc j < length xs \<longleftrightarrow> xs \<noteq> [] \<and> j < length xs - Suc 0"
+ by (cases xs) simp_all
} note *** = this
have j_less: "j < length (transpose (xs # concat (map (case_list [] (\<lambda>h t. [t])) xss)))"
@@ -5282,6 +5283,7 @@
by (simp add: nth_transpose filter_map comp_def)
qed
+
subsubsection \<open>\<^const>\<open>min\<close> and \<^const>\<open>arg_min\<close>\<close>
lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
@@ -5548,8 +5550,6 @@
lemmas sorted2_simps = sorted1 sorted2
-lemmas [code] = sorted0 sorted2_simps
-
lemma sorted_append:
"sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
by (simp add: sorted_wrt_append)
@@ -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>