*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 21 Jul 2011 19:04:28 +0200*In-reply-to*: <20110720181936.223550@gmx.net>*References*: <20110720181936.223550@gmx.net>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.17) Gecko/20110606 Icedove/3.1.10

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) ... done

So start your proof with proof (induct rule: trm.inducts)

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

- 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. next case Cons_term then show ?case apply simp

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

apply (cases "occ (Var v) trm") apply simp_all >>> No subgoals!

by (simp add: split_if)

next 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

by (metis (full_types) list_ex_iff)

by (simp add: list_ex_iff split_if) qed

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

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:

Greetings and HTH, Lars

**References**:**[isabelle] Occur-Check Lemma and Unifikations-Algorithmus***From:*Anja Gerbes

- Previous by Date: Re: [isabelle] Countable instantiation addition
- Next by Date: Re: [isabelle] [isabelle-dev] Countable instantiation addition
- Previous by Thread: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus
- Next by Thread: Re: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list