Re: [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






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