# 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 \ 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' \ iseq xs (Suc i)" "Max js' = i" - then have "card js' \ card js" - by (auto simp add: js [symmetric] liseq'_def iseq_finite intro!: iseq_singleton) - } - note max = this + moreover have max: "card js' \ card js" if "js' \ 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} \ card js" by (rule max) (simp_all add: iseq_singleton) then have "js \ {}" by auto