equal
deleted
inserted
replaced
2 |
2 |
3 theory Ex1 |
3 theory Ex1 |
4 imports LCF |
4 imports LCF |
5 begin |
5 begin |
6 |
6 |
7 consts |
7 axiomatization |
8 P :: "'a => tr" |
8 P :: "'a => tr" and |
9 G :: "'a => 'a" |
9 G :: "'a => 'a" and |
10 H :: "'a => 'a" |
10 H :: "'a => 'a" and |
11 K :: "('a => 'a) => ('a => 'a)" |
11 K :: "('a => 'a) => ('a => 'a)" |
12 |
12 where |
13 axioms |
13 P_strict: "P(UU) = UU" and |
14 P_strict: "P(UU) = UU" |
14 K: "K = (%h x. P(x) => x | h(h(G(x))))" and |
15 K: "K = (%h x. P(x) => x | h(h(G(x))))" |
|
16 H: "H = FIX(K)" |
15 H: "H = FIX(K)" |
17 |
16 |
18 |
17 |
19 declare P_strict [simp] K [simp] |
18 declare P_strict [simp] K [simp] |
20 |
19 |
28 apply simp |
27 apply simp |
29 done |
28 done |
30 |
29 |
31 lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)" |
30 lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)" |
32 apply (tactic {* induct_tac @{context} "K" 1 *}) |
31 apply (tactic {* induct_tac @{context} "K" 1 *}) |
33 apply (simp (no_asm)) |
32 apply simp |
34 apply (simp (no_asm) split: COND_cases_iff) |
33 apply (simp split: COND_cases_iff) |
35 apply (intro strip) |
34 apply (intro strip) |
36 apply (subst H_unfold) |
35 apply (subst H_unfold) |
37 apply (simp (no_asm_simp)) |
36 apply simp |
38 done |
37 done |
39 |
38 |
40 lemma H_idemp: "ALL x. H(H(x)) = H(x)" |
39 lemma H_idemp: "ALL x. H(H(x)) = H(x)" |
41 apply (rule H_idemp_lemma [folded H]) |
40 apply (rule H_idemp_lemma [folded H]) |
42 done |
41 done |