src/HOLCF/FOCUS/Stream_adm.ML
author wenzelm
Thu May 31 20:52:51 2001 +0200 (2001-05-31)
changeset 11355 778c369559d9
parent 11350 4c55b020d6ee
child 13454 01e2496dee05
permissions -rw-r--r--
tuned
oheimb@11350
     1
(*  Title: 	HOLCF/ex/Stream_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
(* ----------------------------------------------------------------------- *)
oheimb@11350
     8
oheimb@11350
     9
val down_cont_def = thm "down_cont_def";
oheimb@11350
    10
val INTER_down_iterate_is_gfp = thm "INTER_down_iterate_is_gfp";
oheimb@11350
    11
oheimb@11350
    12
section "admissibility";
oheimb@11350
    13
oheimb@11350
    14
Goal "[| chain Y; !i. P (Y i);\
oheimb@11350
    15
\(!!Y. [| chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]\
oheimb@11350
    16
\ ==> P(lub (range Y))) |] ==> P(lub (range Y))";
oheimb@11350
    17
by (cut_facts_tac (premises()) 1);
oheimb@11350
    18
by (eatac increasing_chain_adm_lemma 1 1);
oheimb@11350
    19
by (etac thin_rl 1);
oheimb@11350
    20
by (EVERY'[eresolve_tac (premises()), atac, etac thin_rl] 1);
oheimb@11350
    21
by (rtac allI 1);
oheimb@11350
    22
by (case_tac "!j. stream_finite (Y j)" 1);
wenzelm@11355
    23
by ( rtac (thm "chain_incr") 1);
oheimb@11350
    24
by ( rtac allI 1);
oheimb@11350
    25
by ( dtac spec 1);
oheimb@11350
    26
by ( Safe_tac);
oheimb@11350
    27
by ( rtac exI 1);
oheimb@11350
    28
by ( rtac slen_strict_mono 1);
oheimb@11350
    29
by (   etac spec 1);
oheimb@11350
    30
by (  atac 1);
oheimb@11350
    31
by ( atac 1);
oheimb@11350
    32
by (dtac (not_ex RS iffD1) 1);
oheimb@11350
    33
by (stac slen_infinite 1);
oheimb@11350
    34
by (etac thin_rl 1);
oheimb@11350
    35
by (dtac spec 1);
wenzelm@11355
    36
by (fold_goals_tac [thm "ile_def"]);
wenzelm@11355
    37
by (etac (thm "ile_iless_trans" RS (thm "Infty_eq" RS iffD1)) 1);
oheimb@11350
    38
by (Simp_tac 1);
oheimb@11350
    39
qed "flatstream_adm_lemma";
oheimb@11350
    40
oheimb@11350
    41
oheimb@11350
    42
(* should be without reference to stream length? *)
oheimb@11350
    43
Goalw [adm_def] "[|(!!Y. [| chain Y; !i. P (Y i); \
oheimb@11350
    44
\!k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P";
oheimb@11350
    45
by (strip_tac 1);
oheimb@11350
    46
by (eatac flatstream_adm_lemma 1 1);
oheimb@11350
    47
by (EVERY'[eresolve_tac (premises()), atac, atac] 1);
oheimb@11350
    48
qed "flatstream_admI";
oheimb@11350
    49
oheimb@11350
    50
oheimb@11350
    51
(* context (theory "Nat_InFinity");*)
oheimb@11350
    52
Goal "Fin (i + j) <= x ==> Fin i <= x";
wenzelm@11355
    53
by (rtac (thm "ile_trans") 1);
oheimb@11350
    54
by  (atac 2);
oheimb@11350
    55
by (Simp_tac 1);
oheimb@11350
    56
qed "ile_lemma";
oheimb@11350
    57
oheimb@11350
    58
Goalw [stream_monoP_def]
oheimb@11350
    59
"!!X. stream_monoP F ==> !i. ? l. !x y. \
oheimb@11350
    60
\ Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i";
oheimb@11350
    61
by (safe_tac HOL_cs);
oheimb@11350
    62
by (res_inst_tac [("x","i*ia")] exI 1);
oheimb@11350
    63
by (nat_ind_tac "ia" 1);
oheimb@11350
    64
by ( Simp_tac 1);
oheimb@11350
    65
by (Simp_tac 1);
oheimb@11350
    66
by (strip_tac 1);
oheimb@11350
    67
by (etac allE 1 THEN etac all_dupE 1 THEN dtac mp 1 THEN etac ile_lemma 1);
oheimb@11350
    68
by (dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1);
oheimb@11350
    69
by (etac allE 1 THEN dtac mp 1 THEN rtac ile_lemma 1);
wenzelm@11355
    70
by ( etac (thm "ile_trans") 1);
oheimb@11350
    71
by ( etac slen_mono 1);
oheimb@11350
    72
by (etac ssubst 1);
oheimb@11350
    73
by (safe_tac HOL_cs);
oheimb@11350
    74
by ( eatac (ile_lemma RS slen_take_lemma3 RS subst) 2 1);
oheimb@11350
    75
by (etac allE 1);
oheimb@11350
    76
by (etac allE 1);
oheimb@11350
    77
by (dtac mp 1);
oheimb@11350
    78
by ( etac slen_rt_mult 1);
oheimb@11350
    79
by (dtac mp 1);
oheimb@11350
    80
by (etac monofun_rt_mult 1);
oheimb@11350
    81
by (mp_tac 1); 
oheimb@11350
    82
by (atac 1);
oheimb@11350
    83
qed "stream_monoP2I";
oheimb@11350
    84
oheimb@11350
    85
Goal "[| !i. ? l. !x y. \
oheimb@11350
    86
\Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;\
oheimb@11350
    87
\   down_cont F |] ==> adm (%x. x:gfp F)";
oheimb@11350
    88
byev[	etac (INTER_down_iterate_is_gfp RS ssubst) 1, (* cont *)
oheimb@11350
    89
	Simp_tac 1,
oheimb@11350
    90
	resolve_tac adm_lemmas 1,
oheimb@11350
    91
	rtac flatstream_admI 1,
oheimb@11350
    92
	etac allE 1,
oheimb@11350
    93
	etac exE 1,
oheimb@11350
    94
	etac allE 1 THEN etac exE 1,
oheimb@11350
    95
	etac allE 1 THEN etac allE 1 THEN dtac mp 1, (* stream_monoP *)
wenzelm@11355
    96
	 dtac (thm "ileI1") 1,
wenzelm@11355
    97
	 dtac (thm "ile_trans") 1,
wenzelm@11355
    98
	  rtac (thm "ile_iSuc") 1,
wenzelm@11355
    99
	 dtac (thm "iSuc_ile_mono" RS iffD1) 1,
oheimb@11350
   100
	 atac 1,
oheimb@11350
   101
	dtac mp 1,
oheimb@11350
   102
	 etac is_ub_thelub 1,
oheimb@11350
   103
	Fast_tac 1];
oheimb@11350
   104
qed "stream_monoP2_gfp_admI";
oheimb@11350
   105
oheimb@11350
   106
bind_thm("fstream_gfp_admI",stream_monoP2I RS stream_monoP2_gfp_admI);
oheimb@11350
   107
oheimb@11350
   108
qed_goalw "stream_antiP2I" thy [stream_antiP_def]
oheimb@11350
   109
"!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]\
oheimb@11350
   110
\ ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i" (K [
oheimb@11350
   111
	rtac allI 1,
oheimb@11350
   112
	nat_ind_tac "i" 1,
oheimb@11350
   113
	 Simp_tac 1,
oheimb@11350
   114
	Simp_tac 1,
oheimb@11350
   115
	strip_tac 1,
oheimb@11350
   116
	etac allE 1 THEN etac all_dupE 1 THEN etac exE 1 THEN etac exE 1,
oheimb@11350
   117
	etac conjE 1,
oheimb@11350
   118
	case_tac "#x < Fin ia" 1,
oheimb@11350
   119
	 fast_tac HOL_cs 1,
wenzelm@11355
   120
	fold_goals_tac [thm "ile_def"],
oheimb@11350
   121
	mp_tac 1,
oheimb@11350
   122
	etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1,
oheimb@11350
   123
	etac ssubst 1,
oheimb@11350
   124
        etac allE 1 THEN mp_tac 1,
oheimb@11350
   125
	dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1,
oheimb@11350
   126
	etac conjE 1 THEN rtac conjI 1,
oheimb@11350
   127
	 etac (slen_take_lemma3 RS ssubst) 1 THEN atac 1,
oheimb@11350
   128
	 atac 1,
oheimb@11350
   129
	etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac monofun_rt_mult 1,
oheimb@11350
   130
	mp_tac 1,
oheimb@11350
   131
	atac 1]);
oheimb@11350
   132
oheimb@11350
   133
qed_goalw "stream_antiP2_non_gfp_admI" thy [adm_def]
oheimb@11350
   134
"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] \
oheimb@11350
   135
\ ==> adm (%u. ~ u:gfp F)" (K [
oheimb@11350
   136
	asm_simp_tac (simpset() addsimps [INTER_down_iterate_is_gfp]) 1,
oheimb@11350
   137
	fast_tac (claset() addSDs [is_ub_thelub]) 1]);
oheimb@11350
   138
oheimb@11350
   139
bind_thm ("fstream_non_gfp_admI", stream_antiP2I RS 
oheimb@11350
   140
				stream_antiP2_non_gfp_admI);
oheimb@11350
   141
oheimb@11350
   142
oheimb@11350
   143
oheimb@11350
   144
(**new approach for adm********************************************************)
oheimb@11350
   145
oheimb@11350
   146
section "antitonP";
oheimb@11350
   147
oheimb@11350
   148
Goalw [antitonP_def] "[| antitonP P; y:P; x<<y |] ==> x:P";
oheimb@11350
   149
by Auto_tac;
oheimb@11350
   150
qed "antitonPD";
oheimb@11350
   151
oheimb@11350
   152
Goalw [antitonP_def]"!x y. y:P --> x<<y --> x:P ==> antitonP P";
oheimb@11350
   153
by (Fast_tac 1);
oheimb@11350
   154
qed "antitonPI";
oheimb@11350
   155
oheimb@11350
   156
Goalw [adm_def] "antitonP P ==> adm (%u. u~:P)";
oheimb@11350
   157
by (auto_tac (claset() addDs [antitonPD] addEs [is_ub_thelub],simpset()));
oheimb@11350
   158
qed "antitonP_adm_non_P";
oheimb@11350
   159
oheimb@11350
   160
Goal "P \\<equiv> gfp F \\<Longrightarrow> {y. \\<exists>x::'a::pcpo. y \\<sqsubseteq> x \\<and> x \\<in> P} \\<subseteq> F {y. \\<exists>x. y \\<sqsubseteq> x \\<and> x \\<in> P} \\<Longrightarrow> \
oheimb@11350
   161
\ adm (\\<lambda>u. u\\<notin>P)";
oheimb@11350
   162
by (Asm_full_simp_tac 1);
oheimb@11350
   163
by (rtac antitonP_adm_non_P 1);
oheimb@11350
   164
by (rtac antitonPI 1);
oheimb@11350
   165
by (dtac gfp_upperbound 1);
oheimb@11350
   166
by (Fast_tac 1);
oheimb@11350
   167
qed "def_gfp_adm_nonP";
oheimb@11350
   168
oheimb@11350
   169
Goalw [adm_def] 
oheimb@11350
   170
"{lub (range Y) |Y. chain Y & (\\<forall>i. Y i \\<in> P)} \\<subseteq> P \\<Longrightarrow> adm (\\<lambda>x. x\\<in>P)";
oheimb@11350
   171
by (Fast_tac 1);
oheimb@11350
   172
qed "adm_set";
oheimb@11350
   173
oheimb@11350
   174
Goal "P \\<equiv> gfp F \\<Longrightarrow> {lub (range Y) |Y. chain Y \\<and> (\\<forall>i. Y i \\<in> P)} \\<subseteq> \
oheimb@11350
   175
\ F {lub (range Y) |Y. chain Y \\<and> (\\<forall>i. Y i \\<in> P)} \\<Longrightarrow> adm (\\<lambda>x. x\\<in>P)";
oheimb@11350
   176
by (Asm_full_simp_tac 1);
oheimb@11350
   177
by (rtac adm_set 1);
oheimb@11350
   178
by (etac gfp_upperbound 1);
oheimb@11350
   179
qed "def_gfp_admI";