[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.