*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] [Q]Question about Isabelle/hol*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Mon, 02 Jul 2012 13:01:35 +1000*In-reply-to*: <46B3768E2D2DE5409CC25A5E1B984DFD115639DB@i-mail-a02.nuc.kwansei.ac.jp>*References*: <46B3768E2D2DE5409CC25A5E1B984DFD1156394F@i-mail-a02.nuc.kwansei.ac.jp>, <CAAMXsiYAxVGYEzpycKG74gOHz=9mmVVV=GKJhRTndGiA56e0=w@mail.gmail.com> <46B3768E2D2DE5409CC25A5E1B984DFD115639DB@i-mail-a02.nuc.kwansei.ac.jp>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1

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. On 30/06/12 02:47, 後藤 裕貴 wrote: > Dear Mr. Huffman, > > Thank you very much for your help. > The cause of the "simp freeze" seemed to be "lemma" before it. > This later proof was proved by a method according to advice well > > Causative "lemma" is the following thing. > > lemma app_test_n[simp] : > "~ ( (simp_hd_eq xs y) = True | (simp_hd_eq ys y) = True ) > ==> ((simp_hd_eq xs y) = False) & ( (simp_hd_eq ys y) = False) " > apply simp > done > > I think that "lemma" which caused it cannot be established. > In spite of it, the proof is completed. > Which point will it be if caused by a definition of "simp_hd_eq"? > > It would be nice if you could reply. > > Yuki Goto > > ******************************************* > Yuki Goto > Information Technology Major > Kwansei Gakuin University > Hyogo, Japan > E-mail: auf75646 at kwansei.ac.jp > ******************************************* > > > > On Thu, Jun 28, 2012 at 3:38 AM, 後藤 裕貴 <auf75646 at kwansei.ac.jp> wrote: >> datatype >> char = A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z |Dot >> >> type_synonym str = "char list" >> >> fun simp_hd_eq :: "str list => str => bool" where >> "simp_hd_eq [] y = False" | >> "simp_hd_eq (x#xs) y = (if (str_eq x y) then True else (simp_hd_eq xs y) )" >> >> lemma simp_add_nq : "(simp_hd_eq xs y) = False & (simp_hd_eq ys y) = False ==> (simp_hd_eq (xs @ ys) y) = False" >> >> This is the first question and I cannot prove this lemma. >> Probably I think that I am self-evident, how can you prove it? > This lemma cannot be proved by simplification alone; it requires > induction: "apply (induct xs) apply auto" should do it. > >> lemma simp_hd_eq_app[simp] : "(simp_hd_eq xs y) = True ==> (simp_hd_eq (xs @ ys) y) = True" >> apply simp > "apply (induct xs) apply auto" should work here too. > >> When I was going to carry out "apply simp" in this "lemma", the second question is why "Proof General" freezes. >> Can you shed any light on this? > It doesn't freeze for me. You might try turning off "auto quickcheck" > or similar tools if they are enabled. > > Hope this helps, > - Brian > >

- Previous by Date: Re: [isabelle] Pending sort hypotheses
- Next by Date: [isabelle] [Fwd: [vstte-12-vc] VerifyThis Verification Competition @ FM 2012 - Call for participation]
- Previous by Thread: Re: [isabelle] Pending sort hypotheses
- 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