Email Gateway (Aug 22 2022 at 10:55): Email Gateway (Aug 22 2022 at 10:55):From: noam neer <noamneer@gmail.com>
in the tutorial that comes with Isabelle 2015 (end of section 5.8.1, page
79) it is said that the 'subst' method can perform substitutions in a
subgoal's assumptions. however the following proof step fails to replace
the left 1 with 'real(Suc 0)' and gives the error messege "Failed to apply
proof method". why?
lemma "real (m::nat) = 1 ==> m = 1"
apply (subst real_of_nat_one[symmetric])
oops
Email Gateway (Aug 22 2022 at 10:55):From: Andrew Gacek <andrew.gacek@gmail.com>
Use the (asm) modifier to substitute in the assumptions:
lemma "real (m::nat) = 1 ==> m = 1"
apply (subst (asm) real_of_nat_one[symmetric])
-Andrew
Last updated: Apr 24 2024 at 04:17 UTC