# HG changeset patch
# User nipkow
# Date 1722615918 -7200
# Node ID 362d750f5788601272a32a97160409e6bfee9943
# Parent  06350a8745c99ab17cf2c795254a94dd1621c185
got rid of references to system-generated names

diff -r 06350a8745c9 -r 362d750f5788 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 01 14:07:34 2024 +0200
+++ b/src/HOL/List.thy	Fri Aug 02 18:25:18 2024 +0200
@@ -6629,14 +6629,33 @@
 lemma lexn_conv:
   "lexn r n =
     {(xs,ys). length xs = n \<and> length ys = n \<and>
-    (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"
+    (\<exists>xys x y xs' ys'. xs = xys @ x#xs' \<and> ys = xys @ y # ys' \<and> (x, y) \<in> r)}"
+  (is "?L n = ?R n" is "_ = {(xs,ys). ?len n xs \<and> ?len n ys \<and> (\<exists>xys. ?P xs ys xys)}")
 proof (induction n)
   case (Suc n)
+(* A compact proof referring to a system-generated name:
   then show ?case
-    apply (simp add: image_Collect lex_prod_def, safe, blast)
-     apply (rule_tac x = "ab # xys" in exI, simp)
-    apply (case_tac xys; force)
+    apply (auto simp add: image_Collect lex_prod_def)
+    apply blast
+    apply (meson Cons_eq_appendI)
+    apply (case_tac xys; fastforce)
     done
+*)
+  have "(xs,ys) \<in> ?L (Suc n)" if r: "(xs,ys) \<in> ?R (Suc n)" for xs ys
+  proof -
+    from r obtain xys where r': "?len (Suc n) xs" "?len (Suc n) ys" "?P xs ys xys" by auto
+    then show ?thesis
+    proof (cases xys)
+      case Nil
+      thus ?thesis using r' by (auto simp: image_Collect lex_prod_def)
+    next
+      case Cons
+      thus ?thesis using r' Suc by (fastforce simp: image_Collect lex_prod_def)
+    qed
+  qed
+  moreover have "(xs,ys) \<in> ?L (Suc n) \<Longrightarrow> (xs,ys) \<in> ?R (Suc n)" for xs ys
+    using Suc by (auto simp add: image_Collect lex_prod_def)(blast, meson Cons_eq_appendI)
+  ultimately show ?case by (meson pred_equals_eq2)
 qed auto
 
 text\<open>By Mathias Fleury:\<close>
diff -r 06350a8745c9 -r 362d750f5788 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Aug 01 14:07:34 2024 +0200
+++ b/src/HOL/Presburger.thy	Fri Aug 02 18:25:18 2024 +0200
@@ -241,7 +241,7 @@
 next
   assume d: "d dvd D"
   {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
-      by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: algebra_simps)}
+      using dvd_add_left_iff[OF d, of "x+t"] by (simp add: algebra_simps)}
   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
 qed blast