Re: [isabelle] [isabelle-dev] Occur-Check Problem in Isabelle

Hi Anja,

> bin Studenten an der Goethe-Uni in Frankfurt und beschäftige mich sehr
> stark mit dem Isabelle Beweis-System.

The usual language on the Isabelle mailing lists is english. Also, please note that this list is for discussions about the development _of_ Isabelle. Using (or developing _in_ Isabelle) is on-topic on the isabelle-users at mailing list[1]. I'm redirecting your post there.

> Currently I am sitting at the following problem in Isabelle.
> In the lemma "subst_no_occ" I get no further, I strongly suspect that I
> am in the functions"apply_subst" and "occ" have overlooked something
> important and something gets lost in the proof.

> lemma subst_no_occ: "\neg occ (Var v) t \Longrightarrow Var v \neq t
>    \Longrightarrow t \triangleleft [(v,s)] = t"

You meant "\<not>" instead of "\<neg>" here, right?

> apply(induct t)
> apply(simp)
> apply(simp)
> apply(simp)
> apply(simp)
> done

Your example is incomplete, so it is hard to give useful advice. I tried to complete it as follows:

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

In this case, "apply (induct t)" introduces a new schematic variable into the goal, which is instantiated by the second "simp". The goals which remains after the 4th simp is actually unsolvable; quickcheck finds a counter example.

The problem is here that the definition of trm (and apply_subst) contain nested recursion and hence you need to do induction over both apply_subst and apply_subst_list at the same time.

  -- Lars


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.