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?
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)
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
Still some goal left. How can we proceed? Hm, there is an "if" in the
~(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")
>>> 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