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