equal
deleted
inserted
replaced
4 theory Ex4 |
4 theory Ex4 |
5 imports "../LCF" |
5 imports "../LCF" |
6 begin |
6 begin |
7 |
7 |
8 lemma example: |
8 lemma example: |
9 assumes asms: "f(p) << p" "!!q. f(q) << q ==> p << q" |
9 assumes asms: "f(p) << p" "\<And>q. f(q) << q \<Longrightarrow> p << q" |
10 shows "FIX(f)=p" |
10 shows "FIX(f)=p" |
11 apply (unfold eq_def) |
11 apply (unfold eq_def) |
12 apply (rule conjI) |
12 apply (rule conjI) |
13 apply (induct f) |
13 apply (induct f) |
14 apply (rule minimal) |
14 apply (rule minimal) |