> On 3 Jul 2015, at 3:54 pm, Lars Noschinski <nosch...@in.tum.de> wrote:
>
> On 03.07.2015 04:02, Daniel Matichuk wrote:
>> Additionally, fresh names are chosen for any free variables that appear in
>> the subgoal
>>
>> e.g.
>>
>> lemma "⋀x y. A x y"
>> subgoal for A
>>
>> Results in "x" being named "Aa". In this case I would expect either an error
>> ("Free name clash") or for the new fixed term to shadow the free A.
>> The second choice is a bit strange, however, because you end up with two
>> different coloured "A"s in the goal.
>
> I would expect unspecified variables to get internal names, i.e. names
> ending with "_"; similar to variables not specified in a case command.
That's exactly what happens, here the goal parameter "y" becomes the fixed term
"y_" which can't be accessed.
The problem here is that I specified that I would like the goal parameter "x"
to be fixed and named "A", which clashes with the already-free A in my goal.
Normally this is a non-issue, if you were writing a "have" and had fixed some
"A" then it's impossible to refer to one from the original goal. The problem
here is that because you are generating a subgoal out of an existing one while
simultaneously providing names for goal parameters, there is an opportunity
to create a clash.
The most permissive behaviour is to fix a new term which shadows "A" (and is
formally named Aa__ internally). The goal then has two As in it, a skolem
(orange) A
and the original (blue) A. This could possibly emit a warning, but is logically
fine.
Basically I expect any goal parameter that I have fixed to be given the exact
name that I specify, regardless of other global effects.
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
