[isabelle-dev] Safe approach to hypothesis substitution

[Andreas Schropp]

On 08/24/2010 09:13 PM, Andreas Schropp wrote:
> On 08/24/2010 07:51 PM, Alexander Krauss wrote:
>>
>> 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.

BTW: if you want to be even more conservative you
take both fixes and assumes into account
(are the Frees in assumes always guaranteed to be fixed?)
when approximating safeness of equality-elimination.
Then you would have to compare e.g.

lemma shows "!! x. A x ==> B x"
apply method

and

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

to observe the difference. Is that better or worse? ^^