Email Gateway (Aug 18 2022 at 18:08): Email Gateway (Aug 18 2022 at 18:08):From: Lars Noschinski <noschinl@in.tum.de>
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@cl.cam.ac.uk 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
[1]: https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
Email Gateway (Aug 18 2022 at 18:08):From: Lars Noschinski <noschinl@in.tum.de>
Hi Anja,
On 13.07.2011 23:00, Anja Gerbes wrote:
thanks for the reply.
This problem was already known to me, so I've asked this question.
You should have mentioned this in your question. It takes quite some
time to identify a problem; in particular in someone's else theory.
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.
You can do simultaneous induction if you connect the goals by "and":
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)
...
-- Lars
Last updated: Apr 25 2024 at 12:23 UTC