# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1580135563 0
# Node ID f2b783abfbe71694b263c5984da0c9e0a4fd2656
# Parent  43c2355648d2a0e7a8a1c18a7725533b19c2e8cb
A few lemmas connected with orderings

diff -r 43c2355648d2 -r f2b783abfbe7 src/HOL/Fun.thy
--- 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
diff -r 43c2355648d2 -r f2b783abfbe7 src/HOL/Fun_Def.thy
--- 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"
diff -r 43c2355648d2 -r f2b783abfbe7 src/HOL/List.thy
--- 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)
 
diff -r 43c2355648d2 -r f2b783abfbe7 src/HOL/Nat.thy
--- 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
diff -r 43c2355648d2 -r f2b783abfbe7 src/HOL/Relation.thy
--- 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
diff -r 43c2355648d2 -r f2b783abfbe7 src/HOL/Wellfounded.thy
--- 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>