[isabelle-dev] Safe approach to hypothesis substitution

[Alexander Krauss]

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"
apply method

and

lemma fixes x
   assumes a: "A x"
   shows "B x"
apply (insert a)
apply method

Safe or not, this is obviously undesirable.

Alex