author  wenzelm 
Thu, 01 Jun 2006 21:14:05 +0200  
changeset 19755  90f80de04c46 
parent 17248  81bf91654e73 
child 27208  5fe899199f85 
permissions  rwrr 
4905  1 

17248  2 
(* $Id$ *) 
3 

4 
header {* Addition with fixpoint of successor *} 

4905  5 

17248  6 
theory Ex3 
7 
imports LCF 

8 
begin 

4905  9 

10 
consts 

17248  11 
s :: "'a => 'a" 
12 
p :: "'a => 'a => 'a" 

4905  13 

17248  14 
axioms 
15 
p_strict: "p(UU) = UU" 

16 
p_s: "p(s(x),y) = s(p(x,y))" 

17 

19755  18 
declare p_strict [simp] p_s [simp] 
19 

20 
lemma example: "p(FIX(s),y) = FIX(s)" 

21 
apply (tactic {* induct_tac "s" 1 *}) 

22 
apply (simp (no_asm)) 

23 
apply (simp (no_asm)) 

24 
done 

4905  25 

26 
end 