Re: [isabelle] [Q]Question about Isabelle/hol



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.