| author | huffman |
| Wed, 17 Feb 2010 10:00:22 -0800 | |
| changeset 35174 | e15040ae75d7 |
| parent 35169 | 31cbcb019003 |
| child 35642 | f478d5a9d238 |
| 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" |
|
49 |
apply (rule antisym_less) |
|
50 |
apply (rule lemma4) |
|
51 |
apply (rule lemma3) |
|
52 |
done |
|
53 |
||
54 |
lemma wir_moel: "YS = YYS" |
|
55 |
apply (rule stream.take_lemmas) |
|
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 |
(* ------------------------------------------------------------------------ *) |
|
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 (tactic "cont_tacR 1") |
|
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" |
|
87 |
apply (rule antisym_less) |
|
88 |
apply (rule lemma7) |
|
89 |
apply (rule lemma6) |
|
90 |
done |
|
| 17291 | 91 |
|
| 2570 | 92 |
end |