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

17248  3 
theory Ex3 
4 
imports LCF 

5 
begin 

4905  6 

47025  7 
axiomatization 
8 
s :: "'a => 'a" and 

17248  9 
p :: "'a => 'a => 'a" 
47025  10 
where 
11 
p_strict: "p(UU) = UU" and 

17248  12 
p_s: "p(s(x),y) = s(p(x,y))" 
13 

19755  14 
declare p_strict [simp] p_s [simp] 
15 

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

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

17 
apply (tactic {* induct_tac @{context} "s" 1 *}) 
47025  18 
apply simp 
19 
apply simp 

19755  20 
done 
4905  21 

22 
end 