4905
|
1 |
|
60770
|
2 |
section \<open>Prefixpoints\<close>
|
4905
|
3 |
|
17248
|
4 |
theory Ex4
|
58974
|
5 |
imports "../LCF"
|
17248
|
6 |
begin
|
|
7 |
|
19755
|
8 |
lemma example:
|
58977
|
9 |
assumes asms: "f(p) << p" "\<And>q. f(q) << q \<Longrightarrow> p << q"
|
19755
|
10 |
shows "FIX(f)=p"
|
|
11 |
apply (unfold eq_def)
|
|
12 |
apply (rule conjI)
|
58973
|
13 |
apply (induct f)
|
19755
|
14 |
apply (rule minimal)
|
|
15 |
apply (intro strip)
|
|
16 |
apply (rule less_trans)
|
|
17 |
prefer 2
|
|
18 |
apply (rule asms)
|
|
19 |
apply (erule less_ap_term)
|
|
20 |
apply (rule asms)
|
|
21 |
apply (rule FIX_eq [THEN eq_imp_less1])
|
|
22 |
done
|
|
23 |
|
17248
|
24 |
end
|