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.

  -- Lars
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)"

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
  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 MHonArc.