author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 47025  b2b8ae61d6ad 
child 58889  5b7a9633cfa8 
permissions  rwrr 
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 