# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1581425735 0
# Node ID d8fb621fea025baffe9a1a67f99e46287c4dae0e
# Parent  6c52b1d71f8b26c7da74427601658173912075e4
some lemmas about the lex ordering on lists, etc.

diff -r 6c52b1d71f8b -r d8fb621fea02 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Feb 10 23:04:45 2020 +0100
+++ b/CONTRIBUTORS	Tue Feb 11 12:55:35 2020 +0000
@@ -16,6 +16,14 @@
 * October 2019: Maximilian Schäffeler
   Port of the HOL Light decision procedure for metric spaces.
 
+* January 2020: LC Paulson
+  The full finite Ramsey's theorem and elements of finite and infinite 
+  Ramsey theory.
+
+* February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf
+  Simplified, generalised version of ZF/Constructible.
+
+
 
 Contributions to Isabelle2019
 -----------------------------
diff -r 6c52b1d71f8b -r d8fb621fea02 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Feb 10 23:04:45 2020 +0100
+++ b/src/HOL/List.thy	Tue Feb 11 12:55:35 2020 +0000
@@ -6031,7 +6031,7 @@
 done
 
 text\<open>By Mathias Fleury:\<close>
-lemma lexn_transI:
+proposition lexn_transI:
   assumes "trans r" shows "trans (lexn r n)"
 unfolding trans_def
 proof (intro allI impI)
@@ -6096,6 +6096,11 @@
   qed
 qed
 
+corollary lex_transI:
+    assumes "trans r" shows "trans (lex r)"
+  using lexn_transI [OF assms]
+  by (clarsimp simp add: lex_def trans_def) (metis lexn_length)
+
 lemma lex_conv:
   "lex r =
     {(xs,ys). length xs = length ys \<and>
@@ -6128,6 +6133,10 @@
     by (fastforce simp: lenlex_def total_on_def lex_def)
 qed
 
+lemma lenlex_transI [intro]: "trans r \<Longrightarrow> trans (lenlex r)"
+  unfolding lenlex_def
+  by (meson lex_transI trans_inv_image trans_less_than trans_lex_prod)
+
 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
 by (simp add: lex_conv)
 
@@ -6142,6 +6151,20 @@
    prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
   by (metis hd_append append_Nil list.sel(1) list.sel(3) tl_append2)
 
+lemma Nil_lenlex_iff1 [simp]: "([], ns) \<in> lenlex r \<longleftrightarrow> ns \<noteq> []" 
+  and Nil_lenlex_iff2 [simp]: "(ns,[]) \<notin> lenlex r"
+  by (auto simp: lenlex_def)
+
+lemma Cons_lenlex_iff: 
+  "((m # ms, n # ns) \<in> lenlex r) \<longleftrightarrow> 
+    length ms < length ns 
+  \<or> length ms = length ns \<and> (m,n) \<in> r 
+  \<or> (m = n \<and> (ms,ns) \<in> lenlex r)"
+  by (auto simp: lenlex_def)
+
+lemma lenlex_length: "(ms, ns) \<in> lenlex r \<Longrightarrow> length ms \<le> length ns"
+  by (auto simp: lenlex_def)
+
 lemma lex_append_rightI:
   "(xs, ys) \<in> lex r \<Longrightarrow> length vs = length us \<Longrightarrow> (xs @ us, ys @ vs) \<in> lex r"
 by (fastforce simp: lex_def lexn_conv)
diff -r 6c52b1d71f8b -r d8fb621fea02 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Feb 10 23:04:45 2020 +0100
+++ b/src/HOL/Power.thy	Tue Feb 11 12:55:35 2020 +0000
@@ -904,13 +904,14 @@
   from power_strict_increasing_iff [OF this] less show ?thesis ..
 qed
 
-lemma power_dvd_imp_le: "i ^ m dvd i ^ n \<Longrightarrow> 1 < i \<Longrightarrow> m \<le> n"
-  for i m n :: nat
-  apply (rule power_le_imp_le_exp)
-   apply assumption
-  apply (erule dvd_imp_le)
-  apply simp
-  done
+lemma power_gt_expt: "n > Suc 0 \<Longrightarrow> n^k > k"
+  by (induction k) (auto simp: less_trans_Suc n_less_m_mult_n)
+
+lemma power_dvd_imp_le:
+  fixes i :: nat
+  assumes "i ^ m dvd i ^ n" "1 < i"
+  shows "m \<le> n"
+  using assms by (auto intro: power_le_imp_le_exp [OF \<open>1 < i\<close> dvd_imp_le])
 
 lemma dvd_power_iff_le:
   fixes k::nat
@@ -968,7 +969,7 @@
 qed
 
 lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2"
-shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
+  shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
 proof -
   have "1 \<le> k - 1" using assms(2) by arith
   from ex_power_ivl1[OF assms(1) this]