58889
|
1 |
section {* Example 3.8 *}
|
4905
|
2 |
|
17248
|
3 |
theory Ex2
|
|
4 |
imports LCF
|
|
5 |
begin
|
4905
|
6 |
|
47025
|
7 |
axiomatization
|
|
8 |
P :: "'a => tr" and
|
|
9 |
F :: "'b => 'b" and
|
|
10 |
G :: "'a => 'a" and
|
|
11 |
H :: "'a => 'b => 'b" and
|
17248
|
12 |
K :: "('a => 'b => 'b) => ('a => 'b => 'b)"
|
47025
|
13 |
where
|
|
14 |
F_strict: "F(UU) = UU" and
|
|
15 |
K: "K = (%h x y. P(x) => y | F(h(G(x),y)))" and
|
17248
|
16 |
H: "H = FIX(K)"
|
|
17 |
|
19755
|
18 |
declare F_strict [simp] K [simp]
|
|
19 |
|
|
20 |
lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
|
|
21 |
apply (simplesubst H)
|
58973
|
22 |
apply (induct "K:: ('a=>'b=>'b) => ('a=>'b=>'b)")
|
47025
|
23 |
apply simp
|
|
24 |
apply (simp split: COND_cases_iff)
|
19755
|
25 |
done
|
4905
|
26 |
|
|
27 |
end
|