src/HOLCF/FOCUS/Buffer_adm.ML
author wenzelm
Fri Oct 05 21:52:39 2001 +0200 (2001-10-05)
changeset 11701 3d51fbf81c17
parent 11655 923e4d0d36d5
child 11704 3c50a2cd6f00
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
oheimb@11350
     1
(*  Title: 	HOLCF/FOCUS/Buffer_adm.ML
wenzelm@11355
     2
    ID:         $Id$
oheimb@11350
     3
    Author: 	David von Oheimb, TU Muenchen
oheimb@11350
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
oheimb@11350
     5
*)
oheimb@11350
     6
oheimb@11350
     7
infixr 0 y;
oheimb@11350
     8
fun _ y t = by t;
oheimb@11350
     9
val b=9999;
oheimb@11350
    10
wenzelm@11355
    11
Addsimps [thm "Fin_0"];
oheimb@11350
    12
oheimb@11350
    13
val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
oheimb@11350
    14
val BufAC_Asm_d3 = prove_forw 
oheimb@11350
    15
    "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
oheimb@11350
    16
oheimb@11350
    17
val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
wenzelm@11655
    18
 "(s:BufAC_Asm_F A) = (s=<> | \
oheimb@11350
    19
\ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
oheimb@11350
    20
	Auto_tac]);
oheimb@11350
    21
oheimb@11350
    22
Goal "down_cont BufAC_Asm_F";
oheimb@11350
    23
by (auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Asm_F_def3]));
oheimb@11350
    24
qed "cont_BufAC_Asm_F";
oheimb@11350
    25
oheimb@11350
    26
val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
wenzelm@11655
    27
 "((s,t):BufAC_Cmt_F C) = (!d x.\
oheimb@11350
    28
\   (s = <>       --> t = <>                   ) & \
oheimb@11350
    29
\   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
oheimb@11350
    30
\   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
oheimb@11350
    31
	subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
oheimb@11350
    32
		   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
oheimb@11350
    33
	Asm_simp_tac 1,
oheimb@11350
    34
	auto_tac (claset() addIs [surjectiv_scons RS sym], simpset())]);
oheimb@11350
    35
oheimb@11350
    36
val cont_BufAC_Cmt_F = prove_goal thy "down_cont BufAC_Cmt_F" (K [
oheimb@11350
    37
	auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
oheimb@11350
    38
oheimb@11350
    39
oheimb@11350
    40
(**** adm_BufAC_Asm ***********************************************************)
oheimb@11350
    41
oheimb@11350
    42
Goalw [BufAC_Asm_F_def, stream_monoP_def] "stream_monoP BufAC_Asm_F";
oheimb@11350
    43
by (res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1);
wenzelm@11701
    44
by (res_inst_tac [("x","Suc (Suc 0)")] exI 1);
oheimb@11350
    45
by (Clarsimp_tac 1);
oheimb@11350
    46
qed "BufAC_Asm_F_stream_monoP";
oheimb@11350
    47
oheimb@11350
    48
val adm_BufAC_Asm = prove_goalw thy [BufAC_Asm_def] "adm (%x. x:BufAC_Asm)" (K [
oheimb@11350
    49
rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_monoP RS fstream_gfp_admI))1]);
oheimb@11350
    50
oheimb@11350
    51
oheimb@11350
    52
(**** adm_non_BufAC_Asm *******************************************************)
oheimb@11350
    53
oheimb@11350
    54
Goalw [stream_antiP_def, BufAC_Asm_F_def] "stream_antiP BufAC_Asm_F";
oheimb@11350
    55
b y strip_tac 1;
oheimb@11350
    56
b y res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1;
wenzelm@11701
    57
b y res_inst_tac [("x","Suc (Suc 0)")] exI 1;
oheimb@11350
    58
b y rtac conjI 1;
oheimb@11350
    59
b y  strip_tac 2;
oheimb@11350
    60
b y  dtac slen_mono 2;
wenzelm@11355
    61
b y  datac (thm "ile_trans") 1 2;
oheimb@11350
    62
b y ALLGOALS Force_tac;
oheimb@11350
    63
qed "BufAC_Asm_F_stream_antiP";
oheimb@11350
    64
oheimb@11350
    65
Goalw [BufAC_Asm_def] "adm (%u. u~:BufAC_Asm)";
oheimb@11350
    66
by (rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_antiP RS fstream_non_gfp_admI)) 1);
oheimb@11350
    67
qed "adm_non_BufAC_Asm";
oheimb@11350
    68
oheimb@11350
    69
(**** adm_BufAC ***************************************************************)
oheimb@11350
    70
oheimb@11350
    71
(*adm_non_BufAC_Asm*)
oheimb@11350
    72
Goal "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\\<cdot>s = ff\\<cdot>s";
oheimb@11350
    73
by (rtac fstream_ind2 1);
oheimb@11350
    74
by (simp_tac (simpset() addsimps [adm_non_BufAC_Asm]) 1);
oheimb@11350
    75
by   (force_tac (claset() addDs [Buf_f_empty], simpset()) 1);
oheimb@11350
    76
by  (force_tac (claset() addSDs [BufAC_Asm_d2] 
oheimb@11350
    77
		addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
oheimb@11350
    78
by (safe_tac (claset() addSDs [BufAC_Asm_d3]));
oheimb@11350
    79
by (REPEAT(dtac Buf_f_d_req 1));
oheimb@11350
    80
by (fast_tac (claset() addEs [ssubst]) 1);
oheimb@11350
    81
qed_spec_mp "BufAC_Asm_cong";
oheimb@11350
    82
oheimb@11350
    83
(*adm_non_BufAC_Asm,BufAC_Asm_cong*)
oheimb@11350
    84
val BufAC_Cmt_d_req = prove_goal thy 
oheimb@11350
    85
"!!X. [|f:BufEq; s:BufAC_Asm; (s, f\\<cdot>s):BufAC_Cmt|] ==> (a\\<leadsto>b\\<leadsto>s, f\\<cdot>(a\\<leadsto>b\\<leadsto>s)):BufAC_Cmt"
oheimb@11350
    86
 (K [
oheimb@11350
    87
	rtac (BufAC_Cmt_unfold RS iffD2) 1,
oheimb@11350
    88
	strip_tac 1,
oheimb@11350
    89
	forward_tac [Buf_f_d_req] 1,
oheimb@11350
    90
	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
oheimb@11350
    91
oheimb@11350
    92
(*adm_BufAC_Asm*)
oheimb@11350
    93
Goal "antitonP BufAC_Asm";
oheimb@11350
    94
b y rtac antitonPI 1;
oheimb@11350
    95
b y rtac allI 1;
oheimb@11350
    96
b y rtac fstream_ind2 1;
oheimb@11350
    97
b y   REPEAT(resolve_tac adm_lemmas 1);
oheimb@11350
    98
b y    rtac cont_id 1;
oheimb@11350
    99
b y    rtac adm_BufAC_Asm 1;
oheimb@11350
   100
b y   safe_tac HOL_cs;
oheimb@11350
   101
b y   rtac BufAC_Asm_empty 1;
oheimb@11350
   102
b y  force_tac (claset() addSDs [fstream_prefix]
oheimb@11350
   103
		addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
oheimb@11350
   104
b y  force_tac (claset() addSDs [fstream_prefix]
oheimb@11350
   105
		addDs [] addIs []
oheimb@11350
   106
		addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
oheimb@11350
   107
qed "BufAC_Asm_antiton";
oheimb@11350
   108
oheimb@11350
   109
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
oheimb@11350
   110
Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
oheimb@11350
   111
		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
oheimb@11350
   112
		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
wenzelm@11701
   113
by (res_inst_tac [("x","%i. # 2*i")] exI 1);
oheimb@11350
   114
by (rtac allI 1);
oheimb@11350
   115
by (nat_ind_tac "i" 1);
oheimb@11350
   116
by ( Simp_tac 1);
oheimb@11350
   117
by (simp_tac (simpset() addsimps [add_commute]) 1);
oheimb@11350
   118
by (strip_tac 1);
oheimb@11350
   119
by (stac BufAC_Cmt_F_def3 1);
oheimb@11350
   120
by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1);
oheimb@11350
   121
by (Safe_tac);
oheimb@11350
   122
by (   etac Buf_f_empty 1);
oheimb@11350
   123
by (  etac Buf_f_d 1);
oheimb@11350
   124
by ( dtac Buf_f_d_req 1);
oheimb@11350
   125
by ( EVERY[safe_tac HOL_cs, etac ssubst 1, Simp_tac 1]);
oheimb@11350
   126
by (safe_tac (claset() addSDs [slen_fscons_eq RS iffD1] addSss simpset()));
oheimb@11350
   127
(*
oheimb@11350
   128
 1. \\<And>i d xa ya t.
oheimb@11350
   129
       \\<lbrakk>f \\<in> BufEq;
oheimb@11350
   130
          \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
oheimb@11350
   131
                x \\<sqsubseteq> s \\<longrightarrow>
wenzelm@11701
   132
                Fin (# 2 * i) < #x \\<longrightarrow>
oheimb@11350
   133
                (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
oheimb@11350
   134
                (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
wenzelm@11701
   135
          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (# 2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
oheimb@11350
   136
          (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
oheimb@11350
   137
       \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
oheimb@11350
   138
*)
oheimb@11350
   139
by (rotate_tac 2 1);
oheimb@11350
   140
by (dtac BufAC_Asm_prefix2 1);
oheimb@11350
   141
by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]); 
oheimb@11350
   142
by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1]);
oheimb@11350
   143
by (		subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
oheimb@11350
   144
by ( atac 2);
oheimb@11350
   145
by (		rotate_tac ~1 1);
oheimb@11350
   146
by (		Asm_full_simp_tac 1);
oheimb@11350
   147
by (hyp_subst_tac 1);
oheimb@11350
   148
(*
oheimb@11350
   149
 1. \\<And>i d xa ya t ff ffa.
wenzelm@11701
   150
       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (# 2 * i) < #ya;
oheimb@11350
   151
          (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
oheimb@11350
   152
          \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
oheimb@11350
   153
                x \\<sqsubseteq> s \\<longrightarrow>
wenzelm@11701
   154
                Fin (# 2 * i) < #x \\<longrightarrow>
oheimb@11350
   155
                (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
oheimb@11350
   156
                (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
oheimb@11350
   157
          xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>
oheimb@11350
   158
       \\<Longrightarrow> (xa, ff\\<cdot>xa) \\<in> down_iterate BufAC_Cmt_F i
oheimb@11350
   159
*)
oheimb@11350
   160
by (smp_tac 2 1);
oheimb@11350
   161
by (mp_tac 1);
oheimb@11350
   162
by (mp_tac 1);
oheimb@11350
   163
by (etac impE 1);
oheimb@11350
   164
by ( EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1]);
oheimb@11350
   165
by ( eatac (BufAC_Asm_antiton RS antitonPD) 1 1);
oheimb@11350
   166
by (EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1, atac 1]);
oheimb@11350
   167
qed "BufAC_Cmt_2stream_monoP";
oheimb@11350
   168
wenzelm@11655
   169
Goalw [BufAC_Cmt_def] "(x\\<in>BufAC_Cmt) = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
oheimb@11350
   170
by (stac (cont_BufAC_Cmt_F RS INTER_down_iterate_is_gfp) 1);
oheimb@11350
   171
by (Fast_tac 1);
oheimb@11350
   172
qed "BufAC_Cmt_iterate_all";
oheimb@11350
   173
oheimb@11350
   174
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
oheimb@11350
   175
  BufAC_Cmt_2stream_monoP*)
oheimb@11350
   176
Goal "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\\<cdot>s):BufAC_Cmt)";
oheimb@11350
   177
by (rtac flatstream_admI 1);
oheimb@11350
   178
by (stac BufAC_Cmt_iterate_all 1);
oheimb@11350
   179
by (dtac BufAC_Cmt_2stream_monoP 1);
oheimb@11350
   180
by Safe_tac;
oheimb@11350
   181
by (EVERY'[dtac spec, etac exE] 1);
oheimb@11350
   182
by (EVERY'[dtac spec, etac impE] 1);
oheimb@11350
   183
by  (etac (BufAC_Asm_antiton RS antitonPD) 1);
oheimb@11350
   184
by  (etac is_ub_thelub 1);
oheimb@11350
   185
by (smp_tac 3 1);
oheimb@11350
   186
by (dtac is_ub_thelub 1);
oheimb@11350
   187
by (mp_tac 1);
oheimb@11350
   188
by (mp_tac 1);
oheimb@11350
   189
by (etac mp 1);
oheimb@11350
   190
by (dtac (BufAC_Cmt_iterate_all RS iffD1) 1);
oheimb@11350
   191
by (etac spec 1);
oheimb@11350
   192
qed "adm_BufAC";
oheimb@11350
   193
oheimb@11350
   194
oheimb@11350
   195
oheimb@11350
   196
(**** Buf_Eq_imp_AC by induction **********************************************)
oheimb@11350
   197
oheimb@11350
   198
(*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
oheimb@11350
   199
  BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*)
oheimb@11350
   200
Goalw [BufAC_def] "BufEq <= BufAC";
oheimb@11350
   201
by (rtac subsetI 1);
oheimb@11350
   202
by (Simp_tac 1);
oheimb@11350
   203
by (rtac allI 1);
oheimb@11350
   204
by (rtac fstream_ind2 1);
oheimb@11350
   205
back();
oheimb@11350
   206
by (   etac adm_BufAC 1);
oheimb@11350
   207
by (  Safe_tac);
oheimb@11350
   208
by (   etac BufAC_Cmt_empty 1);
oheimb@11350
   209
by (  etac BufAC_Cmt_d 1);
oheimb@11350
   210
by ( dtac BufAC_Asm_prefix2 1);
oheimb@11350
   211
by ( contr_tac 1);
oheimb@11350
   212
by (fast_tac (claset() addIs [BufAC_Cmt_d_req, BufAC_Asm_prefix2]) 1);
oheimb@11350
   213
qed "Buf_Eq_imp_AC";
oheimb@11350
   214
oheimb@11350
   215
(**** new approach for admissibility, reduces itself to absurdity *************)
oheimb@11350
   216
oheimb@11350
   217
Goal "adm (\\<lambda>x. x\\<in>BufAC_Asm)";
oheimb@11350
   218
by(rtac def_gfp_admI 1);
oheimb@11350
   219
by(rtac BufAC_Asm_def 1);
oheimb@11350
   220
b y Safe_tac;
oheimb@11350
   221
b y rewtac BufAC_Asm_F_def;
oheimb@11350
   222
b y Safe_tac;
oheimb@11350
   223
b y etac swap 1;
oheimb@11350
   224
b y dtac (fstream_exhaust_eq RS iffD1) 1;
oheimb@11350
   225
b y Clarsimp_tac 1;
oheimb@11350
   226
b y datac fstream_lub_lemma 1 1;
oheimb@11350
   227
b y Clarify_tac 1;
oheimb@11350
   228
b y eres_inst_tac [("x","j")] all_dupE 1;
oheimb@11350
   229
b y Asm_full_simp_tac 1;
oheimb@11350
   230
b y dtac (BufAC_Asm_d2) 1;
oheimb@11350
   231
b y Clarify_tac 1;
oheimb@11350
   232
b y Simp_tac 1;
oheimb@11350
   233
b y rtac disjCI 1;
oheimb@11350
   234
b y etac swap 1;
oheimb@11350
   235
b y dtac (fstream_exhaust_eq RS iffD1) 1;
oheimb@11350
   236
b y Clarsimp_tac 1;
oheimb@11350
   237
b y datac fstream_lub_lemma 1 1;
oheimb@11350
   238
b y Clarsimp_tac 1;
oheimb@11350
   239
b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;
oheimb@11350
   240
b y res_inst_tac [("x","Xa")] exI 1;
oheimb@11350
   241
br allI 1;
oheimb@11350
   242
b y rotate_tac ~1 1;
oheimb@11350
   243
b y eres_inst_tac [("x","i")] allE 1;
oheimb@11350
   244
b y Clarsimp_tac 1;
oheimb@11350
   245
b y eres_inst_tac [("x","jb")] allE 1;
oheimb@11350
   246
b y Clarsimp_tac 1;
oheimb@11350
   247
b y eres_inst_tac [("x","jc")] allE 1;
oheimb@11350
   248
by (clarsimp_tac (claset() addSDs [BufAC_Asm_d3], simpset()) 1);
oheimb@11350
   249
qed "adm_BufAC_Asm";
oheimb@11350
   250
oheimb@11350
   251
Goal "adm (\\<lambda>u. u \\<notin> BufAC_Asm)"; (* uses antitonP *)
oheimb@11350
   252
by (rtac def_gfp_adm_nonP 1);
oheimb@11350
   253
by (rtac BufAC_Asm_def 1);
oheimb@11350
   254
b y rewtac BufAC_Asm_F_def;
oheimb@11350
   255
b y Safe_tac;
oheimb@11350
   256
b y etac swap 1;
oheimb@11350
   257
b y dtac (fstream_exhaust_eq RS iffD1) 1;
oheimb@11350
   258
b y Clarsimp_tac 1;
oheimb@11350
   259
b y ftac fstream_prefix 1;
oheimb@11350
   260
b y Clarsimp_tac 1;
oheimb@11350
   261
b y ftac BufAC_Asm_d2 1;
oheimb@11350
   262
b y Clarsimp_tac 1;
oheimb@11350
   263
b y rotate_tac ~1 1;
oheimb@11350
   264
b y etac contrapos_pp 1;
oheimb@11350
   265
b y dtac (fstream_exhaust_eq RS iffD1) 1;
oheimb@11350
   266
b y Clarsimp_tac 1;
oheimb@11350
   267
b y ftac fstream_prefix 1;
oheimb@11350
   268
b y Clarsimp_tac 1;
oheimb@11350
   269
b y ftac BufAC_Asm_d3 1;
oheimb@11350
   270
b y Force_tac 1;
oheimb@11350
   271
qed "adm_non_BufAC_Asm";
oheimb@11350
   272
oheimb@11350
   273
Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
oheimb@11350
   274
by(rtac triv_admI 1);
oheimb@11350
   275
by(Clarify_tac 1);
oheimb@11350
   276
by(eatac Buf_Eq_imp_AC_lemma 1 1); 
oheimb@11350
   277
      (* this is what we originally aimed to show, using admissibilty :-( *)
oheimb@11350
   278
qed "adm_BufAC";