--- a/src/HOL/Fun.thy Wed Jan 22 19:17:59 2020 +0000
+++ b/src/HOL/Fun.thy Mon Jan 27 14:32:43 2020 +0000
@@ -283,15 +283,22 @@
from this A \<open>x = f x'\<close> B show ?thesis ..
qed
+lemma linorder_inj_onI:
+ fixes A :: "'a::order set"
+ assumes ne: "\<And>x y. \<lbrakk>x < y; x\<in>A; y\<in>A\<rbrakk> \<Longrightarrow> f x \<noteq> f y" and lin: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A\<rbrakk> \<Longrightarrow> x\<le>y \<or> y\<le>x"
+ shows "inj_on f A"
+proof (rule inj_onI)
+ fix x y
+ assume eq: "f x = f y" and "x\<in>A" "y\<in>A"
+ then show "x = y"
+ using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
+qed
+
lemma linorder_injI:
assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
shows "inj f"
- \<comment> \<open>Courtesy of Stephan Merz\<close>
-proof (rule inj_onI)
- show "x = y" if "f x = f y" for x y
- by (rule linorder_cases) (auto dest: assms simp: that)
-qed
-
+ \<comment> \<open>Courtesy of Stephan Merz\<close>
+using assms by (auto intro: linorder_inj_onI linear)
lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
unfolding Pow_def inj_on_def by blast
--- a/src/HOL/Fun_Def.thy Wed Jan 22 19:17:59 2020 +0000
+++ b/src/HOL/Fun_Def.thy Mon Jan 27 14:32:43 2020 +0000
@@ -207,6 +207,9 @@
lemma wf_pair_less[simp]: "wf pair_less"
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)
+
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"
and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
--- a/src/HOL/List.thy Wed Jan 22 19:17:59 2020 +0000
+++ b/src/HOL/List.thy Mon Jan 27 14:32:43 2020 +0000
@@ -367,12 +367,22 @@
"sorted [] = True" |
"sorted (x # ys) = ((\<forall>y \<in> set ys. x \<le> y) \<and> sorted ys)"
+fun strict_sorted :: "'a list \<Rightarrow> bool" where
+"strict_sorted [] = True" |
+"strict_sorted (x # ys) = ((\<forall>y \<in> List.set ys. x < y) \<and> strict_sorted ys)"
+
lemma sorted_sorted_wrt: "sorted = sorted_wrt (\<le>)"
proof (rule ext)
fix xs show "sorted xs = sorted_wrt (\<le>) xs"
by(induction xs rule: sorted.induct) auto
qed
+lemma strict_sorted_sorted_wrt: "strict_sorted = sorted_wrt (<)"
+proof (rule ext)
+ fix xs show "strict_sorted xs = sorted_wrt (<) xs"
+ by(induction xs rule: strict_sorted.induct) auto
+qed
+
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
"insort_key f x [] = [x]" |
"insort_key f x (y#ys) =
@@ -5089,6 +5099,36 @@
lemma infinite_UNIV_listI: "\<not> finite(UNIV::'a list set)"
by (metis UNIV_I finite_maxlen length_replicate less_irrefl)
+lemma same_length_different:
+ assumes "xs \<noteq> ys" and "length xs = length ys"
+ shows "\<exists>pre x xs' y ys'. x\<noteq>y \<and> xs = pre @ [x] @ xs' \<and> ys = pre @ [y] @ ys'"
+ using assms
+proof (induction xs arbitrary: ys)
+ case Nil
+ then show ?case by auto
+next
+ case (Cons x xs)
+ then obtain z zs where ys: "ys = Cons z zs"
+ by (metis length_Suc_conv)
+ show ?case
+ proof (cases "x=z")
+ case True
+ then have "xs \<noteq> zs" "length xs = length zs"
+ using Cons.prems ys by auto
+ then obtain pre u xs' v ys' where "u\<noteq>v" and xs: "xs = pre @ [u] @ xs'" and zs: "zs = pre @ [v] @ys'"
+ using Cons.IH by meson
+ then have "x # xs = (z#pre) @ [u] @ xs' \<and> ys = (z#pre) @ [v] @ ys'"
+ by (simp add: True ys)
+ with \<open>u\<noteq>v\<close> show ?thesis
+ by blast
+ next
+ case False
+ then have "x # xs = [] @ [x] @ xs \<and> ys = [] @ [z] @ zs"
+ by (simp add: ys)
+ then show ?thesis
+ using False by blast
+ qed
+qed
subsection \<open>Sorting\<close>
@@ -5802,6 +5842,18 @@
"sorted_list_of_set {m..<n} = [m..<n]"
by (rule sorted_distinct_set_unique) simp_all
+lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
+ by (induction l) (use less_le in auto)
+
+lemma strict_sorted_list_of_set [simp]: "strict_sorted (sorted_list_of_set A)"
+ by (simp add: strict_sorted_iff)
+
+lemma finite_set_strict_sorted:
+ fixes A :: "'a::linorder set"
+ assumes "finite A"
+ obtains l where "strict_sorted l" "List.set l = A" "length l = card A"
+ by (metis assms distinct_card distinct_sorted_list_of_set set_sorted_list_of_set strict_sorted_list_of_set)
+
subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>
@@ -6049,6 +6101,24 @@
length xs = length ys \<and> (xs, ys) \<in> lex r}"
by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
+lemma total_lenlex:
+ assumes "total r"
+ shows "total (lenlex r)"
+proof -
+ have "(xs,ys) \<in> lexn r (length xs) \<or> (ys,xs) \<in> lexn r (length xs)"
+ if "xs \<noteq> ys" and len: "length xs = length ys" for xs ys
+ proof -
+ obtain pre x xs' y ys' where "x\<noteq>y" and xs: "xs = pre @ [x] @ xs'" and ys: "ys = pre @ [y] @ys'"
+ by (meson len \<open>xs \<noteq> ys\<close> same_length_different)
+ 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 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 Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
by (simp add: lex_conv)
--- a/src/HOL/Nat.thy Wed Jan 22 19:17:59 2020 +0000
+++ b/src/HOL/Nat.thy Mon Jan 27 14:32:43 2020 +0000
@@ -734,17 +734,31 @@
by (cases m) simp_all
lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))"
-by (auto simp: less_Suc_eq)
+ by (auto simp: less_Suc_eq)
lemma All_less_Suc2: "(\<forall>i < Suc n. P i) = (P 0 \<and> (\<forall>i < n. P(Suc i)))"
-by (auto simp: less_Suc_eq_0_disj)
+ by (auto simp: less_Suc_eq_0_disj)
lemma Ex_less_Suc: "(\<exists>i < Suc n. P i) = (P n \<or> (\<exists>i < n. P i))"
-by (auto simp: less_Suc_eq)
+ by (auto simp: less_Suc_eq)
lemma Ex_less_Suc2: "(\<exists>i < Suc n. P i) = (P 0 \<or> (\<exists>i < n. P(Suc i)))"
-by (auto simp: less_Suc_eq_0_disj)
-
+ by (auto simp: less_Suc_eq_0_disj)
+
+text \<open>@{term mono} (non-strict) doesn't imply increasing, as the function could be constant\<close>
+lemma strict_mono_imp_increasing:
+ fixes n::nat
+ assumes "strict_mono f" shows "f n \<ge> n"
+proof (induction n)
+ case 0
+ then show ?case
+ by auto
+next
+ case (Suc n)
+ then show ?case
+ unfolding not_less_eq_eq [symmetric]
+ using Suc_n_not_le_n assms order_trans strict_mono_less_eq by blast
+qed
subsubsection \<open>Monotonicity of Addition\<close>
@@ -1213,19 +1227,19 @@
lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)"
for i j k :: nat
- by (induct j k rule: diff_induct) simp_all
+ by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc)
lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
for i j k :: nat
- by (fact diff_add_assoc [symmetric])
+ by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc)
lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i"
for i j k :: nat
- by (simp add: ac_simps)
+ by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc2)
lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
for i j k :: nat
- by (fact diff_add_assoc2 [symmetric])
+ by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc2)
lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)"
for i j k :: nat
--- a/src/HOL/Relation.thy Wed Jan 22 19:17:59 2020 +0000
+++ b/src/HOL/Relation.thy Mon Jan 27 14:32:43 2020 +0000
@@ -1127,12 +1127,13 @@
lemma trans_inv_image: "trans r \<Longrightarrow> trans (inv_image r f)"
unfolding trans_def inv_image_def
- apply (simp (no_asm))
- apply blast
- done
+ by (simp (no_asm)) blast
+
+lemma total_inv_image: "\<lbrakk>inj f; total r\<rbrakk> \<Longrightarrow> total (inv_image r f)"
+ unfolding inv_image_def total_on_def by (auto simp: inj_eq)
lemma in_inv_image[simp]: "(x, y) \<in> inv_image r f \<longleftrightarrow> (f x, f y) \<in> r"
- by (auto simp:inv_image_def)
+ by (auto simp: inv_image_def)
lemma converse_inv_image[simp]: "(inv_image R f)\<inverse> = inv_image (R\<inverse>) f"
unfolding inv_image_def converse_unfold by auto
--- a/src/HOL/Wellfounded.thy Wed Jan 22 19:17:59 2020 +0000
+++ b/src/HOL/Wellfounded.thy Mon Jan 27 14:32:43 2020 +0000
@@ -583,6 +583,9 @@
lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)"
by (simp add: less_than_def less_eq)
+lemma total_less_than: "total less_than"
+ using total_on_def by force
+
lemma wf_less: "wf {(x, y::nat). x < y}"
by (rule Wellfounded.wellorder_class.wf)
@@ -777,9 +780,14 @@
by (auto simp:lex_prod_def)
text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
-lemma trans_lex_prod [intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
+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)
+
+lemma total_lex_prod [simp]: "total r \<Longrightarrow> total s \<Longrightarrow> total (r <*lex*> s)"
+ by (auto simp: total_on_def)
text \<open>lexicographic combinations with measure functions\<close>