*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] [Q]Question about Isabelle/hol*From*: 後藤 裕貴 <auf75646 at kwansei.ac.jp>*Date*: Sun, 22 Jul 2012 06:13:05 +0000*Accept-language*: ja-JP, en-US*Thread-index*: Ac1nzDIa2raSH1itSYGvizerJTSV2A==*Thread-topic*: [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 ******************************************* Yuki Goto Information Technology Major Kwansei Gakuin University Hyogo, Japan E-mail: auf75646 at kwansei.ac.jp ******************************************* >Date: Mon, 02 Jul 2012 13:01:35 +1000 >From: Thomas Sewell <Thomas.Sewell at nicta.com.au> >Subject: Re: [isabelle] [Q]Question about Isabelle/hol >To: cl-isabelle-users at lists.cam.ac.uk >Message-ID: <4FF10F0F.1060508 at nicta.com.au> >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? >Yours, >Thomas.

**Follow-Ups**:**Re: [isabelle] [Q]Question about Isabelle/hol***From:*Lars Noschinski

- Previous by Date: [isabelle] Changing the arity of a term in ML
- Next by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Previous by Thread: Re: [isabelle] [Q]Question about Isabelle/hol
- Next by Thread: Re: [isabelle] [Q]Question about Isabelle/hol
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list