Substitution behaviour in Isabelle

Question

I have the following lemma in Isabelle:

lemma lem1: "xs ∈ I 
 ⟹ map h1 xs = map (λx. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs"
by(auto)

which I want to apply to show the following one (with the same lambda expression):

lemma "xs ∈ I ⟹ (map h1 xs) ∈ K
 ⟹ (map (λx. if ∃ys∈I. x ∈ set ys then h1 x else h2 x) xs) ∈ K"

Common sense and sledgehammer suggest that (metis lem1) should work, but it does not. Any ideas?

Answer 1

I do not know what goes wrong with metis here, but by (subst (asm) lem1) works fine.

The subst method performs substitution with the given facts. By default, it will substitute the first subterm in the goal that matches the left-hand side of the equation you give it, if you also specify (asm), it will instead substitute in the premises. You can also specify precisely which matching subterms to replace; subst (2 4 6) will substitute the 2nd, 4th and 6th matching subterm (in the goal).

If the equation contains assumptions (as it does in your case), these assumptions will appear as new subgoals; in this case, the assumption of the equation and the goal that remains after the substitution are both already assumptions in your lemma, so they can be proven by assumption, which is why the by (subst (asm) lem1) go through. You could also do

apply (subst (asm) lem1)
apply assumption
apply assumption
done

Answer 2

Eberl got to the question first. I had already worked out a solution before his answer showed up, so I go ahead and present it, while trying to add some value. I also compare it to Eberl's apply-style proof.

(If you just want the proof, then skip to the bottom.)

My answer really is an attempt to make a small suggestion on the difficult task of how you get to a point where you can implement proofs, when many times it's very obvious what the logic should be.

In this case, lem1, along with the conditions of your second lemma, make it obvious that this should be something easy to prove.

Talking about Eberl, as if he might not notice, which he might not, and who I don't know, but from what I know, I categorize him as an "expert", him being in the graduate program at TUM, with access to the experts, where much of the Isabelle action is.

You ask about substitution, and so he gave you several proofs in which he limited himself to a proof in which the subst method had to be used. These experts are very important in being able to whip out proofs, but eventually, people like me and you need to somewhat get up to their level of understanding in how to use Isabelle.

Unlike Eberl, I brainstormed to find any way I could to prove the theorem. Well, your suggestion that it should be easy based on the equality in lem1 gave me some ideas.

Trying to bring any form of pontificating to a quick close, I suggest you try to get away from complete dependency on getting a proof in one big step using an auto tool, and learn how to break a proof down into smaller steps using either structured proofs, or apply-style proofs. For myself, I see the importance of both styles.

I would give you a link to a 900 page textbook on how to learn Isabelle, starting with natural deduction, and taking you up to a moderate level, like Martin Odersky's book for learning Scala, but such a book doesn't exist for Isabelle, or I'd be reading it, or have read it.

I give a structured proof. If you understand the Isar proof commands, it's just stating the logical obvious, and auto takes care of the low-level details. It's an example that using natural deduction rules is many times not needed for detailed proof steps.

One challenge for us is to learn all the Isar keywords and abbreviations, such as have, from this have, then, hence, with facts, etc. It's a daunting task at first, but doable, though I need to do much of the doable still.

Here's the outline of the proof of what I named lem2, where ultimately (I suppose) it's based on the subst axiom of HOL.eq, where HOL.eq is the HOL equality operator =.

1. Because the hypothesis of lem1 is also a condition of lem2, then the equality of lem1 holds.
2. By a2 of lem2, and because the equality of lem1 holds, then the conclusion of lem2 is proved.

This has been the long answer, and some people may not like this much verbiage. It's just to show, if you got the expertise, you can use some basic logic to get the job done. The auto tools only get you so far. To not be dependent on them takes a lot of work.

lemma lem1:
  "xs ∈ I 
     ==> (map h1 xs = map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs)"
by(auto)

lemma lem2:
  assumes a1: "xs ∈ I"
  assumes a2: "(map h1 xs) ∈ K"
  shows "(map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs) ∈ K"
proof-
  from a1
have "(map h1 xs = map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs)"
  by(auto simp add: lem1)
  from a2 and this 
    (* I could have used the abbreviation `with a2`. There are tons of
       abbreviations to learn.*)
show "(map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs) ∈ K"
  by(auto)
qed

thm lem2

Breaking out a proof, like the above, into what I call a bare-bones proof is actually a waste of time for where I'm at. Trial-and-error attempts, with auto methods taking up the slack, actually give me too much success. I waste too much time doing that, instead of being methodical, using a good understanding of natural deduction rules, along with the Isar techniques of structured proofs. And apply-style? Yea, you want that too, which ties heavily into natural deduction rules.

GC44 Free Trivial Tip: The thm lem2 shows you the proved statement of my lem2. I used an assumes/shows style instead of an A ==> B ==> C style like you used, but the proved statement for either will be the same, as can be shown using thm.

The subst Axiom Being at the Core of HOL Substitution

I add more value, if it is valued.

Because the question is about substitution, I show that the axiom subst is at the bottom of being able to do substitutions based on the HOL equality operator =, and I make concrete the subst formula using terms based on your expressions.

I partly do this because above I say "I suppose", and that bugs me.

The HOL axiom subst is at line 158 of HOL.thy, restated as a theorem:

theorem --"subst:" 
  "s = t ==> P s ==> P t"
by(rule subst)

Your lem1 is of the form xs ∈ I ==> s = t. In the proof of lem2, at the statement from a2 and this, you basically have s = t and P s, so by the subst axiom you have P t.

Here, I make the s, t, P s, and P t concrete with your values, where the statement by(rule subst) is a direct use of the subst axiom, and is not a use of the subst method:

theorem 
  "map h1 xs = map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs
  ==> (
  (map h1 xs) ∈ K ==> 
    (map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs) ∈ K      
  )"
by(rule subst)

This is not completely satisfying because I want to see the form P s and P t. So, using my basic knowledge of lambda calculus, I make P == (%x. x ∈ K):

theorem 
  "map h1 xs = map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs
  ==> (
  (%x. x ∈ K) (map h1 xs) ==> 
    (%x. x ∈ K) (map (%x. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs)      
  )"
by(rule subst)

As to what auto is doing in the structured proof, I assume it's not using the subst axiom directly, but somewhere, somehow, the subst axiom is the reason it can do the substitutions, I suppose, saying I suppose to always cover my logical tail, on the most trivial of things.