[isabelle-dev] Safe approach to hypothesis substitution

[Andreas Schropp]

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

I am just talking about tracking Frees occuring in any assumptions, no
general peeking at assumptions. But I get your point.

And actually any tactic can peek at the assumptions, via examination
of the hyps of the goal-state, so this is at best an unenforcable design
consideration and nothing really changes by making this functionality
available from assumption.ML.

The more practical justification (opposed to the theoretical 
justification, which I
alluded to above) of doing this in the context of equality-elimination
might be that most of our tools are based on unification.
So they should be closed under substitutions, meaning that if they
can prove P, they can prove any well-typed substitutions of Frees and 
Vars in P?

>
> 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.

Well yes, but users have to be aware of the difference
between an assume (extending the context)
and an explicit goal assumption (not extending
the context) anyway. Otherwise things like

lemma "x=t ==> t=x" "x=x"
proof -
   assume "x=t"
   thus "t=x" by (rule sym)
   show "x=x" by (rule refl)
qed

should work too without bracing or reording.

>
> Alex