Re: [isabelle] intro rule for &&&



On Thu, 20 Dec 2012, Joachim Breitner wrote:

lemma assumes "A ∧ B" shows "A" "B"
using assms
apply rule

I was told, but don’t understand the reasons, that this works as an
intro rule for &&&:

&&& is merely funny Pure notation to say that there are several simultaneous goals to be proven.

The system needs to retain this structure for advanced methods like "induct", so it cannot be split into several goals by default. The splitting happends implicitly for any other proof method like "rule", which then acts on the first resulting subgoal only. There are other proof methods like "auto" that operate on all available subgoals, and consequently insert used facts into all of them at the start, so the above example will work here.

You can see the difference again in "simp" vs. "simp_all", which is the same tool acting either on the head goal or all goals: "apply simp_all" will solve the above, but not "apply simp".


Further fine points:

  assume "A & B"
  then have A and B by (simp, simp)  -- works

  assume "A & B"
  then have A and B by simp simp  -- fails

  assume "A & B"
  then have A and B apply simp apply simp done  -- fails

  assume "A & B"
  then have A and B
    apply simp
    using `A & B`
    apply simp
    done  -- works

The first one works, because the method expression with sequential composition "," uses the same facts each time: both simp steps will insert the given facts into the respective head subgoal before doing simplification.

The second version puts one simp in the "initial" slot of 'by', and the other in the "terminal" slot. Only the initial method expressions sees the used facts, they are reset afterwards.

The third version imitates the same operationally, using two separate 'apply' steps. The 'apply' command essentially "consumes" the used facts, so the second simp won't see them and fail.

The fourth version refreshes the consumed facts by explicit 'using' in the apply script, so it works again.


This illustrates that "by method1 method2" is structurally different from "by (method1, method2). I always emphasize the importance to do canonical "by induct auto" or "by cases auto" steps that way, and not "optimize" special cases where old-fashioned sequential composition via "," happens to work. The latter is merely an odd imitation of tactical proof style in Isar, and should have disappeared already 10 years ago.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.