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