*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Fri, 22 Jul 2011 12:26:35 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1311324791.13218.466.camel@macbroy12.informatik.tu-muenchen.de>*References*: <20110720181936.223550@gmx.net> <4E285C1C.5050401@in.tum.de> <1311324791.13218.466.camel@macbroy12.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.17) Gecko/20110606 Icedove/3.1.10

On 22.07.2011 10:53, Johannes Hölzl wrote:

Hey, A nice description how proving in Isabelle actually works!

Thanks!

Just a small note about split_if: Am Donnerstag, den 21.07.2011, 19:04 +0200 schrieb Lars Noschinski: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? next case Fn then show ?case apply (simp add: split_if) No, does not seem to suffice. What's left?It should work with (simp split: split_if) i.e. it is not a normal simp rule but added to the splitter.

(simp split: split_if_asm)

[...]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)

This should be "(auto simp add: list_ex_iff split_if)"

qedI don't have your theories but I assume (simp add: list_ex_iff) is enough? Otherwise (simp add: list_ex_iff split: split_if) would be required.

[I attached theory I used] No, this does not suffice. And while (auto simp: list_ex_iff split: split_if_asm) is probably the more correct solution, mine suffices to prove this goal. -- Lars

theory Scratch imports Main begin datatype 'a trm = Var 'a | Fn 'a "('a trm list)" type_synonym 'a subst = "('a \<times> 'a trm) list" abbreviation (input) eq where "eq x \<equiv> \<lambda>y. x = y" fun assoc :: "'a \<Rightarrow> 'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" where "assoc v d [] = d" | "assoc v d ((u, t) # xs) = (if (v = u) then t else assoc v d xs)" primrec apply_subst_list :: "('a trm) list \<Rightarrow> 'a subst \<Rightarrow> ('a trm) list" and apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60) where "apply_subst_list [] s = []" | "apply_subst_list (x#xs) s = (apply_subst x s)#(apply_subst_list xs s)" | "(Var v) \<triangleleft> s = assoc v (Var v) s" | "(Fn f xs) \<triangleleft> s = (Fn f (apply_subst_list xs s))" primrec occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" and occ_list :: "'a trm \<Rightarrow> 'a trm list \<Rightarrow> bool" where "occ u (Var v) = False" | "occ u (Fn f xs) = (if (list_ex (eq u) xs) then True else (occ_list u xs))" | "occ_list u [] = False" | "occ_list u (x#xs) = (if occ u x then True else occ_list u xs)" 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" proof (induct rule: trm.inducts) case Var then show ?case by simp next case Nil_trm then show ?case by simp next case Cons_trm then show ?case by (simp split: split_if_asm) next case Fn then show ?case apply (auto simp: list_ex_iff split: split_if_asm)

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

**Re: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] [isabelle-dev] Countable instantiation addition
- Next by Date: [isabelle] TR10
- Previous by Thread: Re: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus
- Next by Thread: [isabelle] Code generation in Isabelle
- 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