|
4905
|
1 |
|
|
|
2 |
simpset_ref() := LCF_ss;
|
|
|
3 |
|
|
|
4 |
Addsimps [P_strict,K];
|
|
|
5 |
|
|
|
6 |
val H_unfold = prove_goal thy "H = K(H)"
|
|
|
7 |
(fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]);
|
|
|
8 |
|
|
|
9 |
bind_thm ("H_unfold", H_unfold);
|
|
|
10 |
|
|
|
11 |
|
|
|
12 |
val H_strict = prove_goal thy "H(UU)=UU"
|
|
|
13 |
(fn _ => [stac H_unfold 1, Simp_tac 1]);
|
|
|
14 |
|
|
|
15 |
bind_thm ("H_strict", H_strict);
|
|
|
16 |
Addsimps [H_strict];
|
|
|
17 |
|
|
5061
|
18 |
Goal "ALL x. H(FIX(K,x)) = FIX(K,x)";
|
|
4905
|
19 |
by (induct_tac "K" 1);
|
|
|
20 |
by (Simp_tac 1);
|
|
|
21 |
by (simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
|
|
|
22 |
by (strip_tac 1);
|
|
|
23 |
by (stac H_unfold 1);
|
|
|
24 |
by (Asm_simp_tac 1);
|
|
|
25 |
qed "H_idemp_lemma";
|
|
|
26 |
|
|
|
27 |
val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
|
|
|
28 |
bind_thm ("H_idemp", H_idemp);
|