author  haftmann 
Sun, 18 Jan 2009 21:12:06 +0100  
changeset 29554  7e5e5ebb7bf7 
parent 27208  5fe899199f85 
child 35762  af3ff2ba4c54 
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)" 

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

21 
apply (tactic {* induct_tac @{context} "s" 1 *}) 
19755  22 
apply (simp (no_asm)) 
23 
apply (simp (no_asm)) 

24 
done 

4905  25 

26 
end 