Re: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus
On 22.07.2011 10:53, Johannes Hölzl wrote:
Hey, A nice description how proving in Isabelle actually works!
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?
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.
In this case it also works for the simplifier. Actually, I had to go to
the old HOL manual, to find out, why one would usually use the splitter
for this. In our case, the if is in the assumption, so one would need
(simp split: split_if_asm)
here instead. But I'm quite fuzzy on the semantics of the split
parameter -- why would split_if be applied to the conclusion and
split_if_asm to the hypotheses? Is there somewhere a high-level
description of the splitter?
BTW: Is the isar-ref documentation about the split method correct? It
does not seem (and need) to accept the "(asm)" option?
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)"
I 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
[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.
theory Scratch imports
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)"
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
case Nil_trm then show ?case by simp
case Cons_trm then show ?case by (simp split: split_if_asm)
case Fn then show ?case apply (auto simp: list_ex_iff split: split_if_asm)
This archive was generated by a fusion of
Pipermail (Mailman edition) and