# [isabelle] [Q]Question about Isabelle/hol

Dear Sirs/Madams,
My name is Yuki Goto and I am a graduate school student in Kwansei Gakuin University in Japan.
The reason why I am writing this email to you is I'd like to ask some questions about Isabelle/hol.
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 str_eq :: "str => str => bool" where
"str_eq [] _ = True" |
"str_eq _ [] = True" |
"str_eq (x#xs) (y#ys) = ( (x=y) & (str_eq xs ys))"
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?
lemma simp_hd_eq_app[simp] : "(simp_hd_eq xs y) = True ==> (simp_hd_eq (xs @ ys) y) = True"
apply simp
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?
In addition, I want to know whether Isabelle/hol is suitable for "String" and whether there is an example using "String".
I wish to thank you in advance for answering these questions,
Sincerely,
Yuki Goto
*******************************************
Yuki Goto
Information Technology Major
Kwansei Gakuin University
Hyogo, Japan
E-mail: auf75646 at kwansei.ac.jp
*******************************************

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