# HG changeset patch
# User wenzelm
# Date 1730847104 -3600
# Node ID a1567e05f7fda969895c7069af4c5b804369b4fb
# Parent  4829e4c68d7c38d0b7ecc4c11434cfdb77d58768
tuned proofs;

diff -r 4829e4c68d7c -r a1567e05f7fd src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Tue Nov 05 23:45:39 2024 +0100
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Tue Nov 05 23:51:44 2024 +0100
@@ -87,13 +87,8 @@
   then obtain js where js: "liseq' xs i = card js" and "js \<in> iseq xs (Suc i)"
     and "finite js" and "Max js = i"
     by (auto simp add: liseq'_def intro: iseq_finite')
-  moreover {
-    fix js'
-    assume "js' \<in> iseq xs (Suc i)" "Max js' = i"
-    then have "card js' \<le> card js"
-      by (auto simp add: js [symmetric] liseq'_def iseq_finite intro!: iseq_singleton)
-  }
-  note max = this
+  moreover have max: "card js' \<le> card js" if "js' \<in> iseq xs (Suc i)" "Max js' = i" for js'
+    using that by (auto simp add: js [symmetric] liseq'_def iseq_finite intro!: iseq_singleton)
   moreover have "card {i} \<le> card js"
     by (rule max) (simp_all add: iseq_singleton)
   then have "js \<noteq> {}" by auto