src/LCF/ex/Ex2.thy
 author wenzelm Mon Feb 23 14:50:30 2015 +0100 (2015-02-23) changeset 59564 fdc03c8daacc parent 58977 9576b510f6a2 child 60770 240563fbf41d permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
 wenzelm@58889 ` 1` ```section {* Example 3.8 *} ``` wenzelm@4905 ` 2` wenzelm@17248 ` 3` ```theory Ex2 ``` wenzelm@58974 ` 4` ```imports "../LCF" ``` wenzelm@17248 ` 5` ```begin ``` wenzelm@4905 ` 6` wenzelm@47025 ` 7` ```axiomatization ``` wenzelm@58977 ` 8` ``` P :: "'a \ tr" and ``` wenzelm@58977 ` 9` ``` F :: "'b \ 'b" and ``` wenzelm@58977 ` 10` ``` G :: "'a \ 'a" and ``` wenzelm@58977 ` 11` ``` H :: "'a \ 'b \ 'b" and ``` wenzelm@58977 ` 12` ``` K :: "('a \ 'b \ 'b) \ ('a \ 'b \ 'b)" ``` wenzelm@47025 ` 13` ```where ``` wenzelm@47025 ` 14` ``` F_strict: "F(UU) = UU" and ``` wenzelm@58977 ` 15` ``` K: "K = (\h x y. P(x) \ y | F(h(G(x),y)))" and ``` wenzelm@17248 ` 16` ``` H: "H = FIX(K)" ``` wenzelm@17248 ` 17` wenzelm@19755 ` 18` ```declare F_strict [simp] K [simp] ``` wenzelm@19755 ` 19` wenzelm@58977 ` 20` ```lemma example: "\x. F(H(x::'a,y::'b)) = H(x,F(y))" ``` wenzelm@19755 ` 21` ``` apply (simplesubst H) ``` wenzelm@58977 ` 22` ``` apply (induct "K:: ('a\'b\'b) \ ('a\'b\'b)") ``` wenzelm@47025 ` 23` ``` apply simp ``` wenzelm@47025 ` 24` ``` apply (simp split: COND_cases_iff) ``` wenzelm@19755 ` 25` ``` done ``` wenzelm@4905 ` 26` wenzelm@4905 ` 27` ```end ```