equal
deleted
inserted
replaced
|
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 |
|
18 goal thy "ALL x. H(FIX(K,x)) = FIX(K,x)"; |
|
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); |