Re: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus

On 20.07.2011 20:19, Anja Gerbes wrote:
I am working with Isabelle, but in the following lemmas I cannot solve the problem. Can you tell me how I can complete the proof of the following lemma?

lemma subst_no_occ:
  shows "\<not>  occ (Var v) t
      \<Longrightarrow>  Var v \<noteq>  t
      \<Longrightarrow>  t \<triangleleft>  [(v,s)] = t"
    and "\<not>  occ_list (Var v) ts
      \<Longrightarrow>  (\<And>u. u \<in>  set ts
        \<Longrightarrow>  Var v \<noteq>  u)
      \<Longrightarrow>  apply_subst_list ts [(v,s)] = ts"
apply (induct rule: trm.inducts)
apply (simp_all)

If proofs get more complex, it is often a good idea, to use structured proofs instead of apply scripts (see the Isar Tutorial for an introduction, if you've have never worked with structured proofs).

So start your proof with

proof (induct rule: trm.inducts)

You can use Isabelle / Show Me / Cases in Proof General, to see which cases are there. It turns out, two of them are really easy:

proof (induct rule: trm.inducts)
  case Var then show ?case by simp
  case Nil_trm then show ?case by simp

Now, the two cases Fn and Cons_trm seem to be harder; neither simp nor auto can solve these directly; at least, as long as you don't give additional lemmas. At this point, you have multiple options, amongst others:

  - Split the proof into smaller steps, which might be easier to solve
  - Use find_theorems to find a useful lemma, which might already
    exist, but is not known to the various automatic solvers
  - Often quite useful: Try sledgehammer to find proofs automatically.
    Often the proof found by sledgehammer can also help you to identify
    lemmas which enable the simplifier to find a proof.

Let's have a look at Cons_trm.

  case Cons_term then show ?case
    apply simp

Still some goal left. How can we proceed? Hm, there is an "if" in the hypotheses:

 ~(if occ (Var v) trm then True else occ_list (Var v) list)

By default, the simplifier only expands an "if", if it can simplify the condition to either true or false. So it might help, if we tell Isabelle to do a case distinction on the condition:

    apply (cases "occ (Var v) trm")
    apply simp_all

>>> No subgoals!

Nice, that helped. Instead of using cases, We can also tell the simplifier to split the if and just use

    by (simp add: split_if)

instead. Now, how can we solve the last goal? Maybe "split_if" also helps us here?

  case Fn then show ?case
    apply (simp add: split_if)

No, does not seem to suffice. What's left?

⟦(⋀u. u ∈ set list ⟹ Var v ≠ u) ⟹ apply_subst_list list [(v, s)] = list;
     ¬ list_ex (op = (Var v)) list ∧
     (¬ list_ex (op = (Var v)) list ⟶ ¬ occ_list (Var v) list)⟧
    ⟹ apply_subst_list list [(v, s)] = list

Let's try brute force and invoke "sledgehammer". If I run sledgehammer on my version of Isabelle, it finds the following proof (might be different in the Isabelle 2011 release):

    by (metis (full_types) list_ex_iff)

This is a perfectly valid proof, but often you can gain knowledge about Isabelle's library, if you take this proof to find a new proof with the simplifier. So replace the proof we have till now with

  by (simp add: list_ex_iff split_if)

We're lucky, it works like a charm! Now, that we have found a proof, we can turn it into a really compact one: Each of our subgoals was solved with simp, so we replace the whole proof...qed block by

  by (induct rule: trm.inducts) (auto simp: list_ex_iff split_if)

(auto is much like the simplifier, but uses some more techniques and applies to all goals).

So, we now have found a really compact proof. But such a short, nice proof is often the result of some lengthy process. If you are proficient in Isabelle's library, you are considerably faster, but such knowledge comes only with experience.

And when you request help from others, it really helps, if you narrow your problem down. Instead of presenting the whole problem, just present the subgoal you are not able to solve; but provide enough context, that one can recreate what you have done. Exact questions have a much better chance to be answered.

If I would find a solution, how could I prove this lemma in Isabelle, then I could continue working on this and expand the following Lemma:

If you are sure that a lemma holds but you don't want to prove it right now, you can use "sorry" to fake a proof (as long as you are in quick'n'dirty mode). But of course, this always bears the risk that you build your later work on sand, not on a solid fundament ...

Greetings and HTH, Lars

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