equal
deleted
inserted
replaced
380 fix P xs x |
380 fix P xs x |
381 assume "llist_in xs x" "P x" "\<not> P (head xs)" |
381 assume "llist_in xs x" "P x" "\<not> P (head xs)" |
382 from this(1,2) obtain a where "P (head ((tail ^^ a) xs))" |
382 from this(1,2) obtain a where "P (head ((tail ^^ a) xs))" |
383 by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right |
383 by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right |
384 simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i]) |
384 simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i]) |
385 moreover |
|
386 with \<open>\<not> P (head xs)\<close> |
385 with \<open>\<not> P (head xs)\<close> |
387 have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))" |
386 have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))" |
388 by (intro Least_Suc) auto |
387 by (intro Least_Suc) auto |
389 then show "(LEAST n. P (head ((tail ^^ n) (tail xs)))) < (LEAST n. P (head ((tail ^^ n) xs)))" |
388 then show "(LEAST n. P (head ((tail ^^ n) (tail xs)))) < (LEAST n. P (head ((tail ^^ n) xs)))" |
390 by (simp add: funpow_swap1[of tail]) |
389 by (simp add: funpow_swap1[of tail]) |