1 theory Dagstuhl |
|
2 imports Stream |
|
3 begin |
|
4 |
|
5 axiomatization |
|
6 y :: "'a" |
|
7 |
|
8 definition |
|
9 YS :: "'a stream" where |
|
10 "YS = fix$(LAM x. y && x)" |
|
11 |
|
12 definition |
|
13 YYS :: "'a stream" where |
|
14 "YYS = fix$(LAM z. y && y && z)" |
|
15 |
|
16 lemma YS_def2: "YS = y && YS" |
|
17 apply (rule trans) |
|
18 apply (rule fix_eq2) |
|
19 apply (rule YS_def [THEN eq_reflection]) |
|
20 apply (rule beta_cfun) |
|
21 apply simp |
|
22 done |
|
23 |
|
24 lemma YYS_def2: "YYS = y && y && YYS" |
|
25 apply (rule trans) |
|
26 apply (rule fix_eq2) |
|
27 apply (rule YYS_def [THEN eq_reflection]) |
|
28 apply (rule beta_cfun) |
|
29 apply simp |
|
30 done |
|
31 |
|
32 |
|
33 lemma lemma3: "YYS << y && YYS" |
|
34 apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind]) |
|
35 apply simp_all |
|
36 apply (rule monofun_cfun_arg) |
|
37 apply (rule monofun_cfun_arg) |
|
38 apply assumption |
|
39 done |
|
40 |
|
41 lemma lemma4: "y && YYS << YYS" |
|
42 apply (subst YYS_def2) |
|
43 back |
|
44 apply (rule monofun_cfun_arg) |
|
45 apply (rule lemma3) |
|
46 done |
|
47 |
|
48 lemma lemma5: "y && YYS = YYS" |
|
49 apply (rule below_antisym) |
|
50 apply (rule lemma4) |
|
51 apply (rule lemma3) |
|
52 done |
|
53 |
|
54 lemma wir_moel: "YS = YYS" |
|
55 apply (rule stream.take_lemma) |
|
56 apply (induct_tac n) |
|
57 apply (simp (no_asm)) |
|
58 apply (subst YS_def2) |
|
59 apply (subst YYS_def2) |
|
60 apply simp |
|
61 apply (rule lemma5 [symmetric, THEN subst]) |
|
62 apply (rule refl) |
|
63 done |
|
64 |
|
65 (* ------------------------------------------------------------------------ *) |
|
66 (* Zweite L"osung: Bernhard Möller *) |
|
67 (* statt Beweis von wir_moel "uber take_lemma beidseitige Inclusion *) |
|
68 (* verwendet lemma5 *) |
|
69 (* ------------------------------------------------------------------------ *) |
|
70 |
|
71 lemma lemma6: "YYS << YS" |
|
72 apply (unfold YYS_def) |
|
73 apply (rule fix_least) |
|
74 apply (subst beta_cfun) |
|
75 apply simp |
|
76 apply (simp add: YS_def2 [symmetric]) |
|
77 done |
|
78 |
|
79 lemma lemma7: "YS << YYS" |
|
80 apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind]) |
|
81 apply simp_all |
|
82 apply (subst lemma5 [symmetric]) |
|
83 apply (erule monofun_cfun_arg) |
|
84 done |
|
85 |
|
86 lemma wir_moel': "YS = YYS" |
|
87 apply (rule below_antisym) |
|
88 apply (rule lemma7) |
|
89 apply (rule lemma6) |
|
90 done |
|
91 |
|
92 end |
|