[isabelle-dev] goals inserts facts into goal statement
andreas.lochbihler at inf.ethz.ch
Fri Jul 24 11:08:15 CEST 2015
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 *)
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?
PS: I am using Isabelle/3444e0bf9261.
More information about the isabelle-dev