[isabelle-dev] Safe approach to hypothesis substitution
krauss at in.tum.de
Tue Aug 24 19:51:46 CEST 2010
Andreas Schropp wrote:
> On 08/24/2010 06:35 PM, Makarius wrote:
>> Just like global types/consts/defs, local fixes/assumes merely
>> generate an infinite collection of consequences. The latter is what
>> you are working with conceptually, but it is not practical. So the
>> system provides further slots to declare certain consequences of a
>> context to certain tools: simp, intro, elim etc.
> I don't get this response:
> if a Free x is not mentioned in any assumes, the elimination of a hyp
> x=t can not affect provability of the goal,
> because any deductions involving x can be done with an arbitrary term of
> the same type (esp. t) instead, right?
The safety concerns discussed here are not the only relevant design
principle. If a method would peek at the assumtions in a context, you
would get a different behaviour of
lemma fixes x shows "A x ==> B x"
lemma fixes x
assumes a: "A x"
shows "B x"
apply (insert a)
Safe or not, this is obviously undesirable.
More information about the isabelle-dev