author | wenzelm |
Thu, 10 Oct 2013 12:02:12 +0200 | |
changeset 54320 | b8bd31c7058c |
parent 47025 | b2b8ae61d6ad |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
17248 | 1 |
header {* Section 10.4 *} |
4905 | 2 |
|
17248 | 3 |
theory Ex1 |
4 |
imports LCF |
|
5 |
begin |
|
4905 | 6 |
|
47025 | 7 |
axiomatization |
8 |
P :: "'a => tr" and |
|
9 |
G :: "'a => 'a" and |
|
10 |
H :: "'a => 'a" and |
|
17248 | 11 |
K :: "('a => 'a) => ('a => 'a)" |
47025 | 12 |
where |
13 |
P_strict: "P(UU) = UU" and |
|
14 |
K: "K = (%h x. P(x) => x | h(h(G(x))))" and |
|
17248 | 15 |
H: "H = FIX(K)" |
16 |
||
19755 | 17 |
|
18 |
declare P_strict [simp] K [simp] |
|
19 |
||
20 |
lemma H_unfold: "H = K(H)" |
|
21 |
apply (simplesubst H) |
|
22 |
apply (rule FIX_eq [symmetric]) |
|
23 |
done |
|
24 |
||
25 |
lemma H_strict [simp]: "H(UU)=UU" |
|
26 |
apply (simplesubst H_unfold) |
|
27 |
apply simp |
|
28 |
done |
|
29 |
||
30 |
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
|
31 |
apply (tactic {* induct_tac @{context} "K" 1 *}) |
47025 | 32 |
apply simp |
33 |
apply (simp split: COND_cases_iff) |
|
19755 | 34 |
apply (intro strip) |
35 |
apply (subst H_unfold) |
|
47025 | 36 |
apply simp |
19755 | 37 |
done |
38 |
||
39 |
lemma H_idemp: "ALL x. H(H(x)) = H(x)" |
|
40 |
apply (rule H_idemp_lemma [folded H]) |
|
41 |
done |
|
4905 | 42 |
|
43 |
end |