*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] [Q]Question about Isabelle/hol*From*: 後藤 裕貴 <auf75646 at kwansei.ac.jp>*Date*: Fri, 29 Jun 2012 16:47:16 +0000*Accept-language*: ja-JP, en-US*Cc*: 高橋 和子 <ktaka at kwansei.ac.jp>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAAMXsiYAxVGYEzpycKG74gOHz=9mmVVV=GKJhRTndGiA56e0=w@mail.gmail.com>*References*: <46B3768E2D2DE5409CC25A5E1B984DFD1156394F@i-mail-a02.nuc.kwansei.ac.jp>, <CAAMXsiYAxVGYEzpycKG74gOHz=9mmVVV=GKJhRTndGiA56e0=w@mail.gmail.com>*Thread-index*: Ac1UzsBcRW/5KpfaSUqD228qg/bH/f//0N+AgAKwhnY=*Thread-topic*: [isabelle] [Q]Question about Isabelle/hol

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

**References**:**[isabelle] [Q]Question about Isabelle/hol***From:*後藤 裕貴

**Re: [isabelle] [Q]Question about Isabelle/hol***From:*Brian Huffman

- Previous by Date: Re: [isabelle] PIDE Display of Assumptions
- Next by Date: Re: [isabelle] PIDE Display of Assumptions
- Previous by Thread: Re: [isabelle] [Q]Question about Isabelle/hol
- Next by Thread: [isabelle] Pending sort hypotheses
- Cl-isabelle-users June 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