|
2570
|
1 |
(* $Id$ *)
|
|
|
2 |
|
|
17291
|
3 |
theory Dagstuhl
|
|
|
4 |
imports Stream
|
|
|
5 |
begin
|
|
2570
|
6 |
|
|
|
7 |
consts
|
|
17291
|
8 |
y :: "'a"
|
|
2570
|
9 |
|
|
19763
|
10 |
definition
|
|
17291
|
11 |
YS :: "'a stream"
|
|
19763
|
12 |
"YS = fix$(LAM x. y && x)"
|
|
17291
|
13 |
YYS :: "'a stream"
|
|
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)
|
|
|
57 |
apply (simp (no_asm) add: stream.rews)
|
|
|
58 |
apply (subst YS_def2)
|
|
|
59 |
apply (subst YYS_def2)
|
|
|
60 |
apply (simp add: stream.rews)
|
|
|
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
|