waynee95 (Dec 13 2022 at 19:24): waynee95 (Dec 13 2022 at 19:24):I have the following situation:
lemma lapprox_tm0_stays_stable:
assumes "lapprox_tm0 η0 η1 d φ x ⊥ n = lapprox_tm0 η0 η1 d φ x ⊥ (Suc n)"
and "m ≥ n"
shows "lapprox_tm0 η0 η1 d φ x ⊥ m = lapprox_tm0 η0 η1 d φ x ⊥ n"
proof (induction m)
case 0
with assms(2) have "n = 0"
sorry
have "lapprox_tm0 η0 η1 d φ x ⊥ 0 = (⊥, η1, d)"
by simp
with ‹n = 0› show ?case
by simp
next
case (Suc m)
then show ?case
by (metis assms(1) lapprox_tm0.simps(2))
qed
Why is it not possible to conclude that "n = 0" given that "m = 0" here and "m \geq n" from the assumption?
Simon Roßkopf (Dec 13 2022 at 20:00):If you need to use an assumption in the induction, it needs to be part of the proof state before you use induction, otherwise it will not be available.
You can add them by adding using assms before starting your proof.
Last updated: Dec 21 2024 at 16:20 UTC