author  blanchet 
Mon, 20 Dec 2010 14:17:49 +0100  
changeset 41317  fc48faccd77b 
parent 35762  af3ff2ba4c54 
child 47025  b2b8ae61d6ad 
permissions  rwrr 
17248  1 
header {* Section 10.4 *} 
4905  2 

17248  3 
theory Ex1 
4 
imports LCF 

5 
begin 

4905  6 

7 
consts 

17248  8 
P :: "'a => tr" 
9 
G :: "'a => 'a" 

10 
H :: "'a => 'a" 

11 
K :: "('a => 'a) => ('a => 'a)" 

4905  12 

17248  13 
axioms 
14 
P_strict: "P(UU) = UU" 

15 
K: "K = (%h x. P(x) => x  h(h(G(x))))" 

16 
H: "H = FIX(K)" 

17 

19755  18 

19 
declare P_strict [simp] K [simp] 

20 

21 
lemma H_unfold: "H = K(H)" 

22 
apply (simplesubst H) 

23 
apply (rule FIX_eq [symmetric]) 

24 
done 

25 

26 
lemma H_strict [simp]: "H(UU)=UU" 

27 
apply (simplesubst H_unfold) 

28 
apply simp 

29 
done 

30 

31 
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

32 
apply (tactic {* induct_tac @{context} "K" 1 *}) 
19755  33 
apply (simp (no_asm)) 
34 
apply (simp (no_asm) split: COND_cases_iff) 

35 
apply (intro strip) 

36 
apply (subst H_unfold) 

37 
apply (simp (no_asm_simp)) 

38 
done 

39 

40 
lemma H_idemp: "ALL x. H(H(x)) = H(x)" 

41 
apply (rule H_idemp_lemma [folded H]) 

42 
done 

4905  43 

44 
end 