Re: [isabelle] [Q]Question about Isabelle/hol
- 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=GKJhRTndGiA56e0email@example.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?
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
> 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:
>> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and