[isabelle-dev] goals inserts facts into goal statement

Andreas Lochbihler 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 *)
   show True
   proof(rule foo)
     case goal_1
     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?


PS: I am using Isabelle/3444e0bf9261.

More information about the isabelle-dev mailing list