author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 47025  b2b8ae61d6ad 
child 58889  5b7a9633cfa8 
permissions  rwrr 
17248  1 
header {* Example 3.8 *} 
4905  2 

17248  3 
theory Ex2 
4 
imports LCF 

5 
begin 

4905  6 

47025  7 
axiomatization 
8 
P :: "'a => tr" and 

9 
F :: "'b => 'b" and 

10 
G :: "'a => 'a" and 

11 
H :: "'a => 'b => 'b" and 

17248  12 
K :: "('a => 'b => 'b) => ('a => 'b => 'b)" 
47025  13 
where 
14 
F_strict: "F(UU) = UU" and 

15 
K: "K = (%h x y. P(x) => y  F(h(G(x),y)))" and 

17248  16 
H: "H = FIX(K)" 
17 

19755  18 
declare F_strict [simp] K [simp] 
19 

20 
lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))" 

21 
apply (simplesubst H) 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
19755
diff
changeset

22 
apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *}) 
47025  23 
apply simp 
24 
apply (simp split: COND_cases_iff) 

19755  25 
done 
4905  26 

27 
end 