equal
deleted
inserted
replaced
146 lemma [code]: |
146 lemma [code]: |
147 "exists_upto p k as \<longleftrightarrow> (if k \<le> 0 then False else |
147 "exists_upto p k as \<longleftrightarrow> (if k \<le> 0 then False else |
148 let l = k - 1 in p (sub' (as, l)) \<or> exists_upto p l as)" |
148 let l = k - 1 in p (sub' (as, l)) \<or> exists_upto p l as)" |
149 proof (cases "k \<ge> 1") |
149 proof (cases "k \<ge> 1") |
150 case False |
150 case False |
|
151 then have \<open>k \<le> 0\<close> |
|
152 including integer.lifting by transfer simp |
151 then show ?thesis |
153 then show ?thesis |
152 by (auto simp add: not_le discrete) |
154 by simp |
153 next |
155 next |
154 case True |
156 case True |
155 then have less: "k \<le> 0 \<longleftrightarrow> False" |
157 then have less: "k \<le> 0 \<longleftrightarrow> False" |
156 by simp |
158 by simp |
157 define n where "n = nat_of_integer (k - 1)" |
159 define n where "n = nat_of_integer (k - 1)" |