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