src/HOLCF/FOCUS/Buffer.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14171 0cab06e3bbd0
child 15188 9d57263faf9e
permissions -rw-r--r--
Merged in license change from Isabelle2004
oheimb@11350
     1
(*  Title: 	HOLCF/FOCUS/Buffer.ML
wenzelm@11355
     2
    ID:         $Id$
oheimb@11350
     3
    Author: 	David von Oheimb, TU Muenchen
oheimb@11350
     4
*)
oheimb@11350
     5
oheimb@11350
     6
val set_cong = prove_goal Set.thy "!!X. A = B ==> (x:A) = (x:B)" (K [
oheimb@11350
     7
	etac subst 1, rtac refl 1]);
oheimb@11350
     8
oheimb@11350
     9
fun B_prover s tac eqs = prove_goal thy s (fn prems => [cut_facts_tac prems 1, 
oheimb@11350
    10
	tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
oheimb@11350
    11
oheimb@11350
    12
fun prove_forw  s thm     = B_prover s (dtac (thm RS iffD1)) [];
oheimb@11350
    13
fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
oheimb@11350
    14
oheimb@11350
    15
oheimb@11350
    16
(**** BufEq *******************************************************************)
oheimb@11350
    17
oheimb@11350
    18
val mono_BufEq_F = prove_goalw thy [mono_def, BufEq_F_def] 
oheimb@11350
    19
		"mono BufEq_F" (K [Fast_tac 1]);
oheimb@11350
    20
oheimb@11350
    21
val BufEq_fix = mono_BufEq_F RS (BufEq_def RS def_gfp_unfold);
oheimb@11350
    22
wenzelm@11655
    23
val BufEq_unfold = prove_goal thy "(f:BufEq) = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
oheimb@11350
    24
		\(!x. ? ff:BufEq. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>(ff\\<cdot>x)))" (K [
oheimb@11350
    25
	stac (BufEq_fix RS set_cong) 1,
oheimb@11350
    26
	rewtac BufEq_F_def,
oheimb@11350
    27
	Asm_full_simp_tac 1]);
oheimb@11350
    28
oheimb@11350
    29
val Buf_f_empty = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot><> = <>" BufEq_unfold;
oheimb@11350
    30
val Buf_f_d     = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot>(Md d\\<leadsto><>) = <>" BufEq_unfold;
oheimb@11350
    31
val Buf_f_d_req = prove_forw 
oheimb@11350
    32
	"f:BufEq \\<Longrightarrow> \\<exists>ff. ff:BufEq \\<and> f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x" BufEq_unfold;
oheimb@11350
    33
oheimb@11350
    34
oheimb@11350
    35
(**** BufAC_Asm ***************************************************************)
oheimb@11350
    36
oheimb@11350
    37
val mono_BufAC_Asm_F = prove_goalw thy [mono_def, BufAC_Asm_F_def]
oheimb@11350
    38
		"mono BufAC_Asm_F" (K [Fast_tac 1]);
oheimb@11350
    39
oheimb@11350
    40
val BufAC_Asm_fix = mono_BufAC_Asm_F RS (BufAC_Asm_def RS def_gfp_unfold);
oheimb@11350
    41
wenzelm@11655
    42
val BufAC_Asm_unfold = prove_goal thy "(s:BufAC_Asm) = (s = <> | (? d x. \
oheimb@11350
    43
\       s = Md d\\<leadsto>x & (x = <> | (ft\\<cdot>x = Def \\<bullet> & (rt\\<cdot>x):BufAC_Asm))))" (K [
oheimb@11350
    44
				stac (BufAC_Asm_fix RS set_cong) 1,
oheimb@11350
    45
				rewtac BufAC_Asm_F_def,
oheimb@11350
    46
				Asm_full_simp_tac 1]);
oheimb@11350
    47
oheimb@11350
    48
val BufAC_Asm_empty = prove_backw "<>     :BufAC_Asm" BufAC_Asm_unfold [];
oheimb@11350
    49
val BufAC_Asm_d     = prove_backw "Md d\\<leadsto><>:BufAC_Asm" BufAC_Asm_unfold [];
oheimb@11350
    50
val BufAC_Asm_d_req = prove_backw "x:BufAC_Asm ==> Md d\\<leadsto>\\<bullet>\\<leadsto>x:BufAC_Asm"
oheimb@11350
    51
							   BufAC_Asm_unfold [];
oheimb@11350
    52
val BufAC_Asm_prefix2 = prove_forw "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm"
oheimb@11350
    53
							 BufAC_Asm_unfold;
oheimb@11350
    54
oheimb@11350
    55
oheimb@11350
    56
(**** BBufAC_Cmt **************************************************************)
oheimb@11350
    57
oheimb@11350
    58
val mono_BufAC_Cmt_F = prove_goalw thy [mono_def, BufAC_Cmt_F_def] 
oheimb@11350
    59
		"mono BufAC_Cmt_F" (K [Fast_tac 1]);
oheimb@11350
    60
oheimb@11350
    61
val BufAC_Cmt_fix = mono_BufAC_Cmt_F RS (BufAC_Cmt_def RS def_gfp_unfold);
oheimb@11350
    62
wenzelm@11655
    63
val BufAC_Cmt_unfold = prove_goal thy "((s,t):BufAC_Cmt) = (!d x. \
oheimb@11350
    64
    \(s = <>       -->      t = <>) & \
oheimb@11350
    65
    \(s = Md d\\<leadsto><>  -->      t = <>) & \
oheimb@11350
    66
    \(s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x, rt\\<cdot>t):BufAC_Cmt))" (K [
oheimb@11350
    67
	stac (BufAC_Cmt_fix RS set_cong) 1,
oheimb@11350
    68
	rewtac BufAC_Cmt_F_def,
oheimb@11350
    69
	Asm_full_simp_tac 1]);
oheimb@11350
    70
oheimb@11350
    71
val BufAC_Cmt_empty = prove_backw "f:BufEq ==> (<>, f\\<cdot><>):BufAC_Cmt"
oheimb@11350
    72
				BufAC_Cmt_unfold [Buf_f_empty];
oheimb@11350
    73
oheimb@11350
    74
val BufAC_Cmt_d = prove_backw "f:BufEq ==> (a\\<leadsto>\\<bottom>, f\\<cdot>(a\\<leadsto>\\<bottom>)):BufAC_Cmt" 
oheimb@11350
    75
				BufAC_Cmt_unfold [Buf_f_d];
oheimb@11350
    76
oheimb@11350
    77
val BufAC_Cmt_d2 = prove_forw 
oheimb@11350
    78
 "(Md d\\<leadsto>\\<bottom>, f\\<cdot>(Md d\\<leadsto>\\<bottom>)):BufAC_Cmt ==> f\\<cdot>(Md d\\<leadsto>\\<bottom>) = \\<bottom>" BufAC_Cmt_unfold;
oheimb@11350
    79
val BufAC_Cmt_d3 = prove_forw 
oheimb@11350
    80
"(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> (x, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x))):BufAC_Cmt"
oheimb@11350
    81
							BufAC_Cmt_unfold;
oheimb@11350
    82
oheimb@11350
    83
val BufAC_Cmt_d32 = prove_forw 
oheimb@11350
    84
"(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> ft\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)) = Def d"
oheimb@11350
    85
							BufAC_Cmt_unfold;
oheimb@11350
    86
oheimb@11350
    87
(**** BufAC *******************************************************************)
oheimb@11350
    88
oheimb@11350
    89
Goalw [BufAC_def] "f \\<in> BufAC \\<Longrightarrow> f\\<cdot>(Md d\\<leadsto>\\<bottom>) = \\<bottom>";
oheimb@11350
    90
by (fast_tac (claset() addIs [BufAC_Cmt_d2, BufAC_Asm_d]) 1);
oheimb@11350
    91
qed "BufAC_f_d";
oheimb@11350
    92
oheimb@11350
    93
Goal "(? ff:B. (!x. f\\<cdot>(a\\<leadsto>b\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)) = \
oheimb@11350
    94
   \((!x. ft\\<cdot>(f\\<cdot>(a\\<leadsto>b\\<leadsto>x)) = Def d) & (LAM x. rt\\<cdot>(f\\<cdot>(a\\<leadsto>b\\<leadsto>x))):B)";
oheimb@11350
    95
(*  this is an instance (though unification cannot handle this) of
oheimb@11350
    96
Goal "(? ff:B. (!x. f\\<cdot>x = d\\<leadsto>ff\\<cdot>x)) = \
oheimb@11350
    97
   \((!x. ft\\<cdot>(f\\<cdot>x) = Def d) & (LAM x. rt\\<cdot>(f\\<cdot>x)):B)";*)
oheimb@11350
    98
by Safe_tac;
oheimb@11350
    99
by (  res_inst_tac [("P","(%x. x:B)")] ssubst 2);
oheimb@11350
   100
by (   atac 3);
oheimb@11350
   101
by (  rtac ext_cfun 2);
oheimb@11350
   102
by (  dtac spec 2);
oheimb@11350
   103
by (  dres_inst_tac [("f","rt")] cfun_arg_cong 2);
oheimb@11350
   104
by (  Asm_full_simp_tac 2);
oheimb@11350
   105
by ( Full_simp_tac 2);
oheimb@11350
   106
by (rtac bexI 2);
oheimb@11350
   107
by Auto_tac;
oheimb@11350
   108
by (dtac spec 1);
oheimb@11350
   109
by (etac exE 1);;
oheimb@11350
   110
by (etac ssubst 1);
oheimb@11350
   111
by (Simp_tac 1);
oheimb@11350
   112
qed "ex_elim_lemma";
oheimb@11350
   113
oheimb@11350
   114
Goalw [BufAC_def] "f\\<in>BufAC \\<Longrightarrow> \\<exists>ff\\<in>BufAC. \\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x";
oheimb@11350
   115
by (rtac (ex_elim_lemma RS iffD2) 1);
oheimb@11350
   116
by Safe_tac;
oheimb@11350
   117
by  (fast_tac (claset() addIs [BufAC_Cmt_d32 RS Def_maximal, 
oheimb@11350
   118
             monofun_cfun_arg,	BufAC_Asm_empty RS BufAC_Asm_d_req]) 1);
oheimb@11350
   119
by (auto_tac (claset() addIs [BufAC_Cmt_d3, BufAC_Asm_d_req],simpset()));
oheimb@11350
   120
qed "BufAC_f_d_req";
oheimb@11350
   121
oheimb@11350
   122
oheimb@11350
   123
(**** BufSt *******************************************************************)
oheimb@11350
   124
oheimb@11350
   125
val mono_BufSt_F = prove_goalw thy [mono_def, BufSt_F_def] 
oheimb@11350
   126
		"mono BufSt_F" (K [Fast_tac 1]);
oheimb@11350
   127
oheimb@11350
   128
val BufSt_P_fix = mono_BufSt_F RS (BufSt_P_def RS def_gfp_unfold);
oheimb@11350
   129
wenzelm@11655
   130
val BufSt_P_unfold = prove_goal thy "(h:BufSt_P) = (!s. h s\\<cdot><> = <> & \
oheimb@11350
   131
	 \ (!d x. h \\<currency>     \\<cdot>(Md d\\<leadsto>x)   =    h (Sd d)\\<cdot>x & \
oheimb@11350
   132
  \   (? hh:BufSt_P. h (Sd d)\\<cdot>(\\<bullet>\\<leadsto>x)   = d\\<leadsto>(hh \\<currency>    \\<cdot>x))))" (K [
oheimb@11350
   133
	stac (BufSt_P_fix RS set_cong) 1,
oheimb@11350
   134
	rewtac BufSt_F_def,
oheimb@11350
   135
	Asm_full_simp_tac 1]);
oheimb@11350
   136
oheimb@11350
   137
val BufSt_P_empty = prove_forw "h:BufSt_P ==> h s     \\<cdot> <>       = <>" 
oheimb@11350
   138
			BufSt_P_unfold;
oheimb@11350
   139
val BufSt_P_d     = prove_forw "h:BufSt_P ==> h  \\<currency>    \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x"
oheimb@11350
   140
			BufSt_P_unfold;
oheimb@11350
   141
val BufSt_P_d_req = prove_forw "h:BufSt_P ==> \\<exists>hh\\<in>BufSt_P. \
oheimb@11350
   142
				         \ h (Sd d)\\<cdot>(\\<bullet>   \\<leadsto>x) = d\\<leadsto>(hh \\<currency>    \\<cdot>x)"
oheimb@11350
   143
			BufSt_P_unfold;
oheimb@11350
   144
oheimb@11350
   145
oheimb@11350
   146
(**** Buf_AC_imp_Eq ***********************************************************)
oheimb@11350
   147
oheimb@11350
   148
Goalw [BufEq_def] "BufAC \\<subseteq> BufEq";
oheimb@11350
   149
by (rtac gfp_upperbound 1);
oheimb@11350
   150
by (rewtac BufEq_F_def);
oheimb@11350
   151
by Safe_tac;
oheimb@11350
   152
by  (etac BufAC_f_d 1);
oheimb@11350
   153
by (dtac BufAC_f_d_req 1);
oheimb@11350
   154
by (Fast_tac 1);
oheimb@11350
   155
qed "Buf_AC_imp_Eq";
oheimb@11350
   156
oheimb@11350
   157
oheimb@11350
   158
(**** Buf_Eq_imp_AC by coinduction ********************************************)
oheimb@11350
   159
oheimb@11350
   160
Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \
oheimb@11350
   161
\ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)";
berghofe@13454
   162
by (induct_tac "n" 1);
oheimb@11350
   163
by  (Simp_tac 1);
oheimb@11350
   164
by (strip_tac 1);
oheimb@11350
   165
by (dtac (BufAC_Asm_unfold RS iffD1) 1);
oheimb@11350
   166
by Safe_tac;
oheimb@11350
   167
by   (asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1);
oheimb@11350
   168
by  (asm_simp_tac (simpset() addsimps [Buf_f_d]) 1);
oheimb@11350
   169
by (dtac (ft_eq RS iffD1) 1);
oheimb@11350
   170
by (Clarsimp_tac 1);
oheimb@11350
   171
by (REPEAT(dtac Buf_f_d_req 1));
oheimb@11350
   172
by Safe_tac;
oheimb@11350
   173
by (REPEAT(etac ssubst 1));
oheimb@11350
   174
by (Simp_tac 1);
oheimb@11350
   175
by (Fast_tac 1);
oheimb@11350
   176
qed_spec_mp "BufAC_Asm_cong_lemma";
oheimb@11350
   177
Goal "\\<lbrakk>f \\<in> BufEq; ff \\<in> BufEq; s \\<in> BufAC_Asm\\<rbrakk> \\<Longrightarrow> f\\<cdot>s = ff\\<cdot>s";
oheimb@11350
   178
by (resolve_tac stream.take_lemmas 1);
oheimb@11350
   179
by (eatac BufAC_Asm_cong_lemma 2 1);
oheimb@11350
   180
qed "BufAC_Asm_cong";
oheimb@11350
   181
oheimb@11350
   182
Goalw [BufAC_Cmt_def] "\\<lbrakk>f \\<in> BufEq; x \\<in> BufAC_Asm\\<rbrakk> \\<Longrightarrow> (x, f\\<cdot>x) \\<in> BufAC_Cmt";
oheimb@11350
   183
by (rotate_tac ~1 1);
oheimb@11350
   184
by (etac weak_coinduct_image 1);
oheimb@11350
   185
by (rewtac BufAC_Cmt_F_def);
oheimb@11350
   186
by Safe_tac;
oheimb@11350
   187
by    (etac Buf_f_empty 1);
oheimb@11350
   188
by   (etac Buf_f_d 1);
oheimb@11350
   189
by  (dtac Buf_f_d_req 1);
oheimb@11350
   190
by  (Clarsimp_tac 1);
oheimb@11350
   191
by  (etac exI 1);
oheimb@11350
   192
by (dtac BufAC_Asm_prefix2 1);
oheimb@11350
   193
by (ftac Buf_f_d_req 1);
oheimb@11350
   194
by (Clarsimp_tac 1);
oheimb@11350
   195
by (etac ssubst 1);
oheimb@11350
   196
by (Simp_tac 1);
oheimb@11350
   197
by (datac BufAC_Asm_cong 2 1);
oheimb@11350
   198
by (etac subst 1);
oheimb@11350
   199
by (etac imageI 1);
oheimb@11350
   200
qed "Buf_Eq_imp_AC_lemma";
oheimb@11350
   201
Goalw [BufAC_def] "BufEq \\<subseteq> BufAC";
oheimb@11350
   202
by (Clarify_tac 1);
oheimb@11350
   203
by (eatac Buf_Eq_imp_AC_lemma 1 1);
oheimb@11350
   204
qed "Buf_Eq_imp_AC";
oheimb@11350
   205
oheimb@11350
   206
(**** Buf_Eq_eq_AC ************************************************************)
oheimb@11350
   207
oheimb@11350
   208
val Buf_Eq_eq_AC = Buf_AC_imp_Eq RS (Buf_Eq_imp_AC RS subset_antisym);
oheimb@11350
   209
oheimb@11350
   210
oheimb@11350
   211
(**** alternative (not strictly) stronger version of Buf_Eq *******************)
oheimb@11350
   212
oheimb@11350
   213
val Buf_Eq_alt_imp_Eq = prove_goalw thy [BufEq_def,BufEq_alt_def] 
oheimb@11350
   214
	"BufEq_alt \\<subseteq> BufEq" (K [
oheimb@11350
   215
	rtac gfp_mono 1,
oheimb@11350
   216
	rewtac BufEq_F_def,
oheimb@11350
   217
	Fast_tac 1]);
oheimb@11350
   218
oheimb@11350
   219
(* direct proof of "BufEq \\<subseteq> BufEq_alt" seems impossible *)
oheimb@11350
   220
oheimb@11350
   221
oheimb@11350
   222
Goalw [BufEq_alt_def] "BufAC <= BufEq_alt";
oheimb@11350
   223
by (rtac gfp_upperbound 1);
oheimb@11350
   224
by (fast_tac (claset() addEs [BufAC_f_d, BufAC_f_d_req]) 1);
oheimb@11350
   225
qed "Buf_AC_imp_Eq_alt";
oheimb@11350
   226
oheimb@11350
   227
bind_thm ("Buf_Eq_imp_Eq_alt", 
oheimb@11350
   228
  subset_trans OF [Buf_Eq_imp_AC, Buf_AC_imp_Eq_alt]);
oheimb@11350
   229
oheimb@11350
   230
bind_thm ("Buf_Eq_alt_eq", 
oheimb@11350
   231
 subset_antisym OF [Buf_Eq_alt_imp_Eq, Buf_Eq_imp_Eq_alt]);
oheimb@11350
   232
oheimb@11350
   233
oheimb@11350
   234
(**** Buf_Eq_eq_St ************************************************************)
oheimb@11350
   235
oheimb@11350
   236
Goalw [BufSt_def, BufEq_def] "BufSt <= BufEq";
oheimb@11350
   237
by (rtac gfp_upperbound 1);
oheimb@11350
   238
by (rewtac BufEq_F_def);
oheimb@11350
   239
by Safe_tac;
oheimb@11350
   240
by ( asm_simp_tac (simpset() addsimps [BufSt_P_d, BufSt_P_empty]) 1);
oheimb@11350
   241
by (asm_simp_tac (simpset() addsimps [BufSt_P_d]) 1);
oheimb@11350
   242
by (dtac BufSt_P_d_req 1);
oheimb@11350
   243
by (Force_tac 1);
oheimb@11350
   244
qed "Buf_St_imp_Eq";
oheimb@11350
   245
oheimb@11350
   246
Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
oheimb@11350
   247
by Safe_tac;
oheimb@11350
   248
by (EVERY'[rename_tac "f", res_inst_tac 
skalberg@14171
   249
        [("x","\\<lambda>s. case s of Sd d => \\<Lambda> x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
oheimb@11350
   250
by ( Simp_tac 1);
oheimb@11350
   251
by (etac weak_coinduct_image 1);
oheimb@11350
   252
by (rewtac BufSt_F_def); 
oheimb@11350
   253
by (Simp_tac 1);
oheimb@11350
   254
by Safe_tac;
oheimb@11350
   255
by (  EVERY'[rename_tac "s", induct_tac "s"] 1);
oheimb@11350
   256
by (   asm_simp_tac (simpset() addsimps [Buf_f_d]) 1);
oheimb@11350
   257
by (  asm_simp_tac (simpset() addsimps [Buf_f_empty]) 1);
oheimb@11350
   258
by ( Simp_tac 1);
oheimb@11350
   259
by (Simp_tac 1);
oheimb@11350
   260
by (EVERY'[rename_tac"f d x",dres_inst_tac[("d","d"),("x","x")] Buf_f_d_req] 1);
oheimb@11350
   261
by Auto_tac;
oheimb@11350
   262
qed "Buf_Eq_imp_St";
oheimb@11350
   263
oheimb@11350
   264
bind_thm ("Buf_Eq_eq_St", Buf_St_imp_Eq RS (Buf_Eq_imp_St RS subset_antisym));
oheimb@11350
   265
oheimb@11350
   266
oheimb@11350
   267