Re: [isabelle] [Q]Question about Isabelle/hol

I am sorry for the delay in my response.
I am grateful for all the help you game me while we were try to fix the issue.

I ask you a question about proof of "'a list list" this time.
I want to prove that there is not overlap even if I append it in each top on the list when "'a list list" does not have overlap.

fun prefix_app :: "'a list list => 'a list => 'a list list" where
"prefix_app [] y = []" |
"prefix_app xs [] = xs" |
"prefix_app (x#xs) y =  (y @ x) # (prefix_app xs y)"

lemma "(distinct xs) ==> (distinct (prefix_app xs y))"
apply (induct_tac y)

It does not occur to a proof method of this lemma.
If there is a solution, would you teach it?


Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646 at

>Date: Mon, 02 Jul 2012 13:01:35 +1000
>From: Thomas Sewell <Thomas.Sewell at>
>Subject: Re: [isabelle] [Q]Question about Isabelle/hol
>To: cl-isabelle-users at
>Message-ID: <4FF10F0F.1060508 at>
>Content-Type: text/plain; charset=ISO-2022-JP

>I think that the problem is that your lemma "app_test_n" has been
>declared [simp]. This rule is looping the simplifier (causing it to do
>busy-work with no progress). Note that Isabelle making no progress is
>different to Proof General crashing. You can probably still interrupt
>Isabelle and carry on.

>When rules of the form "P ==> Q & R" are added with [simp], the
>simplifier sees that as a recipe for showing Q or R by attempting to
>show P. In your case, Q == R and P can be simplified back to Q, which
>can then be attempted with the rule again, thus the loop. Care needs to
>be taken when adding "conditional rewrite rules" of the form "P ==> Q"
>to the simplifier.

>In this case, what was the point? Why make this a [simp] rule when the
>simplifier knows how to show this anyway?


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