| author | wenzelm |
| Fri, 03 Dec 2010 20:38:58 +0100 | |
| changeset 40945 | b8703f63bfb2 |
| parent 40774 | 0437dbc127b3 |
| child 41413 | 64cd30d6b0b8 |
| permissions | -rw-r--r-- |
| 17291 | 1 |
theory Dagstuhl |
2 |
imports Stream |
|
3 |
begin |
|
| 2570 | 4 |
|
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset
|
5 |
axiomatization |
| 17291 | 6 |
y :: "'a" |
| 2570 | 7 |
|
| 19763 | 8 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
9 |
YS :: "'a stream" where |
| 19763 | 10 |
"YS = fix$(LAM x. y && x)" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
11 |
|
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
12 |
definition |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
13 |
YYS :: "'a stream" where |
| 19763 | 14 |
"YYS = fix$(LAM z. y && y && z)" |
| 2570 | 15 |
|
| 19742 | 16 |
lemma YS_def2: "YS = y && YS" |
17 |
apply (rule trans) |
|
18 |
apply (rule fix_eq2) |
|
| 19763 | 19 |
apply (rule YS_def [THEN eq_reflection]) |
| 19742 | 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) |
|
| 19763 | 27 |
apply (rule YYS_def [THEN eq_reflection]) |
| 19742 | 28 |
apply (rule beta_cfun) |
29 |
apply simp |
|
30 |
done |
|
31 |
||
32 |
||
33 |
lemma lemma3: "YYS << y && YYS" |
|
| 19763 | 34 |
apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind]) |
| 19742 | 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" |
|
| 40431 | 49 |
apply (rule below_antisym) |
| 19742 | 50 |
apply (rule lemma4) |
51 |
apply (rule lemma3) |
|
52 |
done |
|
53 |
||
54 |
lemma wir_moel: "YS = YYS" |
|
|
35642
f478d5a9d238
generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents:
35174
diff
changeset
|
55 |
apply (rule stream.take_lemma) |
| 19742 | 56 |
apply (induct_tac n) |
| 35169 | 57 |
apply (simp (no_asm)) |
| 19742 | 58 |
apply (subst YS_def2) |
59 |
apply (subst YYS_def2) |
|
| 35169 | 60 |
apply simp |
| 19742 | 61 |
apply (rule lemma5 [symmetric, THEN subst]) |
62 |
apply (rule refl) |
|
63 |
done |
|
64 |
||
65 |
(* ------------------------------------------------------------------------ *) |
|
| 40945 | 66 |
(* Zweite L"osung: Bernhard Möller *) |
| 19742 | 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) |
|
| 35948 | 75 |
apply simp |
| 19742 | 76 |
apply (simp add: YS_def2 [symmetric]) |
77 |
done |
|
78 |
||
79 |
lemma lemma7: "YS << YYS" |
|
| 19763 | 80 |
apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind]) |
| 19742 | 81 |
apply simp_all |
82 |
apply (subst lemma5 [symmetric]) |
|
83 |
apply (erule monofun_cfun_arg) |
|
84 |
done |
|
85 |
||
86 |
lemma wir_moel': "YS = YYS" |
|
| 40431 | 87 |
apply (rule below_antisym) |
| 19742 | 88 |
apply (rule lemma7) |
89 |
apply (rule lemma6) |
|
90 |
done |
|
| 17291 | 91 |
|
| 2570 | 92 |
end |