author | wenzelm |
Tue, 11 Nov 2014 15:55:31 +0100 | |
changeset 58977 | 9576b510f6a2 |
parent 58974 | cbc2ac19d783 |
child 60770 | 240563fbf41d |
permissions | -rw-r--r-- |
58889 | 1 |
section {* Addition with fixpoint of successor *} |
4905 | 2 |
|
17248 | 3 |
theory Ex3 |
58974 | 4 |
imports "../LCF" |
17248 | 5 |
begin |
4905 | 6 |
|
47025 | 7 |
axiomatization |
58977 | 8 |
s :: "'a \<Rightarrow> 'a" and |
9 |
p :: "'a \<Rightarrow> 'a \<Rightarrow> '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)" |
|
58973 | 17 |
apply (induct s) |
47025 | 18 |
apply simp |
19 |
apply simp |
|
19755 | 20 |
done |
4905 | 21 |
|
22 |
end |