[isabelle-dev] "Subgoal" command and meta-conjunctions

[Makarius]

On Thu, 11 Feb 2016, Daniel Matichuk wrote:

> Example:
>
> lemma
>  assumes A: A and B: B and C: C
>  shows
>  "A ∧ B ∧ C"
>  apply (intro conjI)
>  apply fold_subgoals[2]
>  subgoal by (auto intro: A B)
>  apply (rule C)
>  done
>
>
> This worked in my old implementation of subgoal, but I have recently 
> discovered that “subgoal” (Isabelle2016) is introducing the conjunction 
> before focusing. This results in only focusing on the first conjunct, 
> instead of the entire meta-conjunct.

There is already a relatively long history of the 'subgoal' command 
outside and inside the Isabelle repository. In the official repository the 
relevant change is this:

changeset:   60626:5d13babbb3f6
user:        wenzelm
date:        Wed Jul 01 22:37:49 2015 +0200
files:       src/Pure/subgoal.ML
description:
split multi-goals as usual (outermost Pure.conjunction only);


It means that the internal Pure.conjunction is treated as in normal proof 
method application: like multiple subgoals. Thus it is formally canonical, 
but it still needs to be proven or disproven in actual use.

An example application is this proof pattern for multiple structured 
goals:

lemma "A x ⟹ B x"
   and "X u ⟹ Y u"
   subgoal premises using ‹A x› sorry
   subgoal premises using ‹X u› sorry
   done

This replaces slightly awkward (is "?A ==> ?B") in the goal statement from 
the past. I have already changed a few existing proofs in that respect.


Certain "raw" proof methods do it differently, e.g. the "induct" family. 
The Pure.conjunction is preserved an somehow internalized into the 
reasoning step. There could be some syntax for 'subgoal' to mean that, but 
details need to be worked out.


> The obvious solution from my end is to have “fold_subgoals” use a custom 
> meta-connective that needs to be explicitly introduced after the 
> “subgoal”, but I was wondering if it would be possible to postpone the 
> meta-conjuction introduction until after the subgoal focus.

Note that there is something new introduced here that goes beyond plain 
multi-goals A and B and C: the result of fold_subgoals is !!x. P x ==> A x 
&& B x && C x with a prefix of goal parameters and premises.

It requires routine inspection if and how that affects existing uses of 
Pure.conjunction. The changeset above says "outermost Pure.conjunction 
only", which means I did not go into this question at that point.


BTW, the change above is from Jul-2015. A discussion like that started a 
few months earlier could have had an impact on the Isabelle2016 release, 
but now the train is already departed.


 	Makarius