1 (* |
|
2 ID: $ $ |
|
3 *) |
|
4 |
|
5 |
|
6 open Dagstuhl; |
|
7 |
|
8 val YS_def2 = fix_prover Dagstuhl.thy YS_def "YS = scons[y][YS]"; |
|
9 val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]"; |
|
10 |
|
11 |
|
12 val prems = goal Dagstuhl.thy "YYS << scons[y][YYS]"; |
|
13 by (rtac (YYS_def RS ssubst) 1); |
|
14 by (rtac fix_ind 1); |
|
15 by (resolve_tac adm_thms 1); |
|
16 by (contX_tacR 1); |
|
17 by (rtac minimal 1); |
|
18 by (rtac (beta_cfun RS ssubst) 1); |
|
19 by (contX_tacR 1); |
|
20 by (rtac monofun_cfun_arg 1); |
|
21 by (rtac monofun_cfun_arg 1); |
|
22 by (atac 1); |
|
23 val lemma3 = result(); |
|
24 |
|
25 val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS"; |
|
26 by (rtac (YYS_def2 RS ssubst) 1); |
|
27 back(); |
|
28 by (rtac monofun_cfun_arg 1); |
|
29 by (rtac lemma3 1); |
|
30 val lemma4 = result(); |
|
31 |
|
32 (* val lemma5 = lemma3 RS (lemma4 RS antisym_less) *) |
|
33 |
|
34 val prems = goal Dagstuhl.thy "scons[y][YYS] = YYS"; |
|
35 by (rtac antisym_less 1); |
|
36 by (rtac lemma4 1); |
|
37 by (rtac lemma3 1); |
|
38 val lemma5 = result(); |
|
39 |
|
40 val prems = goal Dagstuhl.thy "YS = YYS"; |
|
41 by (rtac stream_take_lemma 1); |
|
42 by (nat_ind_tac "n" 1); |
|
43 by (simp_tac (HOLCF_ss addsimps stream_rews) 1); |
|
44 by (res_inst_tac [("y1","y")] (YS_def2 RS ssubst) 1); |
|
45 by (res_inst_tac [("y1","y")] (YYS_def2 RS ssubst) 1); |
|
46 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1); |
|
47 by (rtac (lemma5 RS sym RS subst) 1); |
|
48 by (rtac refl 1); |
|
49 val wir_moel = result(); |
|
50 |
|
51 (* ------------------------------------------------------------------------ *) |
|
52 (* Zweite L"osung: Bernhard M"oller *) |
|
53 (* statt Beweis von wir_moel "uber take_lemma beidseitige Inclusion *) |
|
54 (* verwendet lemma5 *) |
|
55 (* ------------------------------------------------------------------------ *) |
|
56 |
|
57 val prems = goal Dagstuhl.thy "YYS << YS"; |
|
58 by (rtac (YYS_def RS ssubst) 1); |
|
59 by (rtac fix_least 1); |
|
60 by (rtac (beta_cfun RS ssubst) 1); |
|
61 by (contX_tacR 1); |
|
62 by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1); |
|
63 val lemma6 = result(); |
|
64 |
|
65 val prems = goal Dagstuhl.thy "YS << YYS"; |
|
66 by (rtac (YS_def RS ssubst) 1); |
|
67 by (rtac fix_ind 1); |
|
68 by (resolve_tac adm_thms 1); |
|
69 by (contX_tacR 1); |
|
70 by (rtac minimal 1); |
|
71 by (rtac (beta_cfun RS ssubst) 1); |
|
72 by (contX_tacR 1); |
|
73 by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1); |
|
74 by (etac monofun_cfun_arg 1); |
|
75 val lemma7 = result(); |
|
76 |
|
77 val wir_moel = lemma6 RS (lemma7 RS antisym_less); |
|
78 |
|
79 |
|
80 (* ------------------------------------------------------------------------ *) |
|
81 (* L"osung aus Dagstuhl (F.R.) *) |
|
82 (* Wie oben, jedoch ohne Konstantendefinition f"ur YS, YYS *) |
|
83 (* ------------------------------------------------------------------------ *) |
|
84 |
|
85 val prems = goal Stream2.thy |
|
86 "(fix[LAM x. scons[y][x]]) = scons[y][fix[LAM x. scons[y][x]]]"; |
|
87 by (rtac (fix_eq RS ssubst) 1); |
|
88 back(); |
|
89 back(); |
|
90 by (rtac (beta_cfun RS ssubst) 1); |
|
91 by (contX_tacR 1); |
|
92 by (rtac refl 1); |
|
93 val lemma1 = result(); |
|
94 |
|
95 val prems = goal Stream2.thy |
|
96 "(fix[ LAM z. scons[y][scons[y][z]]]) = \ |
|
97 \ scons[y][scons[y][(fix[ LAM z. scons[y][scons[y][z]]])]]"; |
|
98 by (rtac (fix_eq RS ssubst) 1); |
|
99 back(); |
|
100 back(); |
|
101 by (rtac (beta_cfun RS ssubst) 1); |
|
102 by (contX_tacR 1); |
|
103 by (rtac refl 1); |
|
104 val lemma2 = result(); |
|
105 |
|
106 val prems = goal Stream2.thy |
|
107 "fix[LAM z. scons[y][scons[y][z]]] << \ |
|
108 \ scons[y][fix[LAM z. scons[y][scons[y][z]]]]"; |
|
109 by (rtac fix_ind 1); |
|
110 by (resolve_tac adm_thms 1); |
|
111 by (contX_tacR 1); |
|
112 by (rtac minimal 1); |
|
113 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1); |
|
114 by (rtac monofun_cfun_arg 1); |
|
115 by (rtac monofun_cfun_arg 1); |
|
116 by (atac 1); |
|
117 val lemma3 = result(); |
|
118 |
|
119 val prems = goal Stream2.thy |
|
120 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\ |
|
121 \ fix[LAM z. scons[y][scons[y][z]]]"; |
|
122 by (rtac (lemma2 RS ssubst) 1); |
|
123 back(); |
|
124 by (rtac monofun_cfun_arg 1); |
|
125 by (rtac lemma3 1); |
|
126 val lemma4 = result(); |
|
127 |
|
128 val prems = goal Stream2.thy |
|
129 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\ |
|
130 \ fix[LAM z. scons[y][scons[y][z]]]"; |
|
131 by (rtac antisym_less 1); |
|
132 by (rtac lemma4 1); |
|
133 by (rtac lemma3 1); |
|
134 val lemma5 = result(); |
|
135 |
|
136 val prems = goal Stream2.thy |
|
137 "(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])"; |
|
138 by (rtac stream_take_lemma 1); |
|
139 by (nat_ind_tac "n" 1); |
|
140 by (simp_tac (HOLCF_ss addsimps stream_rews) 1); |
|
141 by (rtac (lemma1 RS ssubst) 1); |
|
142 by (rtac (lemma2 RS ssubst) 1); |
|
143 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1); |
|
144 by (rtac (lemma5 RS sym RS subst) 1); |
|
145 by (rtac refl 1); |
|
146 val wir_moel = result(); |
|
147 |
|
148 |
|
149 |
|