| author | haftmann |
| Tue, 02 Jun 2009 15:53:05 +0200 | |
| changeset 31377 | a48f9ef9de15 |
| parent 25135 | 4f8176c940cf |
| child 35169 | 31cbcb019003 |
| permissions | -rw-r--r-- |
| 2570 | 1 |
(* $Id$ *) |
2 |
||
| 17291 | 3 |
theory Dagstuhl |
4 |
imports Stream |
|
5 |
begin |
|
| 2570 | 6 |
|
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset
|
7 |
axiomatization |
| 17291 | 8 |
y :: "'a" |
| 2570 | 9 |
|
| 19763 | 10 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
11 |
YS :: "'a stream" where |
| 19763 | 12 |
"YS = fix$(LAM x. y && x)" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
13 |
|
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
14 |
definition |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
15 |
YYS :: "'a stream" where |
| 19763 | 16 |
"YYS = fix$(LAM z. y && y && z)" |
| 2570 | 17 |
|
| 19742 | 18 |
lemma YS_def2: "YS = y && YS" |
19 |
apply (rule trans) |
|
20 |
apply (rule fix_eq2) |
|
| 19763 | 21 |
apply (rule YS_def [THEN eq_reflection]) |
| 19742 | 22 |
apply (rule beta_cfun) |
23 |
apply simp |
|
24 |
done |
|
25 |
||
26 |
lemma YYS_def2: "YYS = y && y && YYS" |
|
27 |
apply (rule trans) |
|
28 |
apply (rule fix_eq2) |
|
| 19763 | 29 |
apply (rule YYS_def [THEN eq_reflection]) |
| 19742 | 30 |
apply (rule beta_cfun) |
31 |
apply simp |
|
32 |
done |
|
33 |
||
34 |
||
35 |
lemma lemma3: "YYS << y && YYS" |
|
| 19763 | 36 |
apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind]) |
| 19742 | 37 |
apply simp_all |
38 |
apply (rule monofun_cfun_arg) |
|
39 |
apply (rule monofun_cfun_arg) |
|
40 |
apply assumption |
|
41 |
done |
|
42 |
||
43 |
lemma lemma4: "y && YYS << YYS" |
|
44 |
apply (subst YYS_def2) |
|
45 |
back |
|
46 |
apply (rule monofun_cfun_arg) |
|
47 |
apply (rule lemma3) |
|
48 |
done |
|
49 |
||
50 |
lemma lemma5: "y && YYS = YYS" |
|
51 |
apply (rule antisym_less) |
|
52 |
apply (rule lemma4) |
|
53 |
apply (rule lemma3) |
|
54 |
done |
|
55 |
||
56 |
lemma wir_moel: "YS = YYS" |
|
57 |
apply (rule stream.take_lemmas) |
|
58 |
apply (induct_tac n) |
|
59 |
apply (simp (no_asm) add: stream.rews) |
|
60 |
apply (subst YS_def2) |
|
61 |
apply (subst YYS_def2) |
|
62 |
apply (simp add: stream.rews) |
|
63 |
apply (rule lemma5 [symmetric, THEN subst]) |
|
64 |
apply (rule refl) |
|
65 |
done |
|
66 |
||
67 |
(* ------------------------------------------------------------------------ *) |
|
68 |
(* Zweite L"osung: Bernhard Möller *) |
|
69 |
(* statt Beweis von wir_moel "uber take_lemma beidseitige Inclusion *) |
|
70 |
(* verwendet lemma5 *) |
|
71 |
(* ------------------------------------------------------------------------ *) |
|
72 |
||
73 |
lemma lemma6: "YYS << YS" |
|
74 |
apply (unfold YYS_def) |
|
75 |
apply (rule fix_least) |
|
76 |
apply (subst beta_cfun) |
|
77 |
apply (tactic "cont_tacR 1") |
|
78 |
apply (simp add: YS_def2 [symmetric]) |
|
79 |
done |
|
80 |
||
81 |
lemma lemma7: "YS << YYS" |
|
| 19763 | 82 |
apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind]) |
| 19742 | 83 |
apply simp_all |
84 |
apply (subst lemma5 [symmetric]) |
|
85 |
apply (erule monofun_cfun_arg) |
|
86 |
done |
|
87 |
||
88 |
lemma wir_moel': "YS = YYS" |
|
89 |
apply (rule antisym_less) |
|
90 |
apply (rule lemma7) |
|
91 |
apply (rule lemma6) |
|
92 |
done |
|
| 17291 | 93 |
|
| 2570 | 94 |
end |