I am trying to replace some of my old usages of case goal_* with the new goals method. In
the course, I encountered the problem that goal inserts the facts chained in as additional
assumptions of my goals and also for the case bindings. This is unfortunate when I use
goals sequenced after rule. Below is a prototypical example:
lemma foo: "[| X; Y; X ==> Y; Y ==> X |] ==> True" by simp
have "A" and "B"
then (* chaining is required to instantiate the free variables in the theorem
*)
show True
proof(rule foo)
case goal_1
...
next
case goal_2
...
Now, when I replace (rule foo) with (rule foo, goals), the goals methods inserts the facts
A and B into every subgoal and into the case bindings. Is there a canonical way to avoid this?
I can of course write
apply(rule foo) proof goals
but this feels like going against the spirit of Isar. Why does goals have to insert
chained facts at all?
Andreas
PS: I am using Isabelle/3444e0bf9261.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
