[isabelle-dev] NEWS: 'subgoal' command

[Makarius]

On Mon, 6 Jul 2015, Daniel Matichuk wrote:

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

The standard Isar naming policies already take care of such details. In 
Isabelle/757549b4bbe6 the 'subgoal' command now makes use of that instead 
of imitating old rename_tac.

I was first trying to reform rename_tac at the same time, but did not get 
very far with it.  Maybe we can actually phase that out in the longer run.


Here is also a plain Isar example that shows how seemingly inaccesible 
names can be used later in the proof text:

lemma "∀x. A x"
proof
   let ?A = A
   fix A
   show "?A A" sorry
qed


> Basically I expect any goal parameter that I have fixed to be given the 
> exact name that I specify, regardless of other global effects.

Exactly.  Implicit global effects from goal states are bad.  The 'subgoal' 
command is meant to introduce some structure into proof "scripts", and 
should not suffer from implicit statefulness.

Lets see how far we get with this.  So far I've made a few tiny 
applications of the new command, and it looks promising.  It was possible 
to eliminate rename_tac, rule_tac, case_tac in various places.


 	Makarius