60770
|
1 |
section \<open>Addition with fixpoint of successor\<close>
|
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
|