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
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
