# 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.
{"ft_lang_label":"__label__en","ft_lang_prob":0.84757483,"math_prob":0.8351496,"size":1334,"snap":"2021-43-2021-49","text_gpt3_token_len":437,"char_repetition_ratio":0.13157895,"word_repetition_ratio":0.043010753,"special_character_ratio":0.36056972,"punctuation_ratio":0.10358566,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9741041,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-12-02T22:13:35Z\",\"WARC-Record-ID\":\"<urn:uuid:6b28efed-ad4b-42b1-9f89-381294079a1d>\",\"Content-Length\":\"6108\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:63a5c488-855f-479d-9a3d-f4191abf334c>\",\"WARC-Concurrent-To\":\"<urn:uuid:cb1b0061-4db4-4c01-9ea4-2e1b36b4e9c6>\",\"WARC-IP-Address\":\"131.111.8.15\",\"WARC-Target-URI\":\"https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00164.html\",\"WARC-Payload-Digest\":\"sha1:3BRKP5I734DU65UKBNJPJMCGOTIR2N6D\",\"WARC-Block-Digest\":\"sha1:QDQKRVAZ522FW5DBPUSHOIPB36DVCPGF\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-49/CC-MAIN-2021-49_segments_1637964362297.22_warc_CC-MAIN-20211202205828-20211202235828-00638.warc.gz\"}"}