equal
deleted
inserted
replaced
30 apply (simplesubst H_unfold) |
30 apply (simplesubst H_unfold) |
31 apply simp |
31 apply simp |
32 done |
32 done |
33 |
33 |
34 lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)" |
34 lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)" |
35 apply (tactic {* induct_tac "K" 1 *}) |
35 apply (tactic {* induct_tac @{context} "K" 1 *}) |
36 apply (simp (no_asm)) |
36 apply (simp (no_asm)) |
37 apply (simp (no_asm) split: COND_cases_iff) |
37 apply (simp (no_asm) split: COND_cases_iff) |
38 apply (intro strip) |
38 apply (intro strip) |
39 apply (subst H_unfold) |
39 apply (subst H_unfold) |
40 apply (simp (no_asm_simp)) |
40 apply (simp (no_asm_simp)) |