| author | huffman |
| Tue, 15 Nov 2011 09:22:19 +0100 | |
| changeset 45501 | 697e387bb859 |
| parent 35762 | af3ff2ba4c54 |
| child 47025 | b2b8ae61d6ad |
| permissions | -rw-r--r-- |
| 17248 | 1 |
header {* Section 10.4 *}
|
| 4905 | 2 |
|
| 17248 | 3 |
theory Ex1 |
4 |
imports LCF |
|
5 |
begin |
|
| 4905 | 6 |
|
7 |
consts |
|
| 17248 | 8 |
P :: "'a => tr" |
9 |
G :: "'a => 'a" |
|
10 |
H :: "'a => 'a" |
|
11 |
K :: "('a => 'a) => ('a => 'a)"
|
|
| 4905 | 12 |
|
| 17248 | 13 |
axioms |
14 |
P_strict: "P(UU) = UU" |
|
15 |
K: "K = (%h x. P(x) => x | h(h(G(x))))" |
|
16 |
H: "H = FIX(K)" |
|
17 |
||
| 19755 | 18 |
|
19 |
declare P_strict [simp] K [simp] |
|
20 |
||
21 |
lemma H_unfold: "H = K(H)" |
|
22 |
apply (simplesubst H) |
|
23 |
apply (rule FIX_eq [symmetric]) |
|
24 |
done |
|
25 |
||
26 |
lemma H_strict [simp]: "H(UU)=UU" |
|
27 |
apply (simplesubst H_unfold) |
|
28 |
apply simp |
|
29 |
done |
|
30 |
||
31 |
lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)" |
|
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
19755
diff
changeset
|
32 |
apply (tactic {* induct_tac @{context} "K" 1 *})
|
| 19755 | 33 |
apply (simp (no_asm)) |
34 |
apply (simp (no_asm) split: COND_cases_iff) |
|
35 |
apply (intro strip) |
|
36 |
apply (subst H_unfold) |
|
37 |
apply (simp (no_asm_simp)) |
|
38 |
done |
|
39 |
||
40 |
lemma H_idemp: "ALL x. H(H(x)) = H(x)" |
|
41 |
apply (rule H_idemp_lemma [folded H]) |
|
42 |
done |
|
| 4905 | 43 |
|
44 |
end |