src/HOLCF/pcpo.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/pcpo.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for pcpo.thy
     7 *)
     8  
     9 open Pcpo;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* in pcpo's everthing equal to THE lub has lub properties for every chain  *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 val thelubE = prove_goal  Pcpo.thy 
    16 	"[| is_chain(S);lub(range(S)) = l::'a::pcpo|] ==> range(S) <<| l "
    17 (fn prems =>
    18 	[
    19 	(cut_facts_tac prems 1), 
    20 	(hyp_subst_tac 1),
    21 	(rtac lubI 1),
    22 	(etac cpo 1)
    23 	]);
    24 
    25 (* ------------------------------------------------------------------------ *)
    26 (* Properties of the lub                                                    *)
    27 (* ------------------------------------------------------------------------ *)
    28 
    29 
    30 val is_ub_thelub = (cpo RS lubI RS is_ub_lub);
    31 (* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
    32 
    33 val is_lub_thelub = (cpo RS lubI RS is_lub_lub);
    34 (* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
    35 
    36 
    37 (* ------------------------------------------------------------------------ *)
    38 (* the << relation between two chains is preserved by their lubs            *)
    39 (* ------------------------------------------------------------------------ *)
    40 
    41 val lub_mono = prove_goal Pcpo.thy 
    42 	"[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
    43 \           ==> lub(range(C1)) << lub(range(C2))"
    44 (fn prems =>
    45 	[
    46 	(cut_facts_tac prems 1),
    47 	(etac is_lub_thelub 1),
    48 	(rtac ub_rangeI 1),
    49 	(rtac allI 1),
    50 	(rtac trans_less 1),
    51 	(etac spec 1),
    52 	(etac is_ub_thelub 1)
    53 	]);
    54 
    55 (* ------------------------------------------------------------------------ *)
    56 (* the = relation between two chains is preserved by their lubs            *)
    57 (* ------------------------------------------------------------------------ *)
    58 
    59 val lub_equal = prove_goal Pcpo.thy
    60 "[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\
    61 \	==> lub(range(C1))=lub(range(C2))"
    62 (fn prems =>
    63 	[
    64 	(cut_facts_tac prems 1),
    65 	(rtac antisym_less 1),
    66 	(rtac lub_mono 1),
    67 	(atac 1),
    68 	(atac 1),
    69 	(strip_tac 1),
    70 	(rtac (antisym_less_inverse RS conjunct1) 1),
    71 	(etac spec 1),
    72 	(rtac lub_mono 1),
    73 	(atac 1),
    74 	(atac 1),
    75 	(strip_tac 1),
    76 	(rtac (antisym_less_inverse RS conjunct2) 1),
    77 	(etac spec 1)
    78 	]);
    79 
    80 (* ------------------------------------------------------------------------ *)
    81 (* more results about mono and = of lubs of chains                          *)
    82 (* ------------------------------------------------------------------------ *)
    83 
    84 val lub_mono2 = prove_goal Pcpo.thy 
    85 "[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
    86 \ ==> lub(range(X))<<lub(range(Y))"
    87  (fn prems =>
    88 	[
    89 	(rtac  exE 1),
    90 	(resolve_tac prems 1),
    91 	(rtac is_lub_thelub 1),
    92 	(resolve_tac prems 1),
    93 	(rtac ub_rangeI 1),
    94 	(strip_tac 1),
    95 	(res_inst_tac [("Q","x<i")] classical2 1),
    96 	(res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1),
    97 	(rtac sym 1),
    98 	(fast_tac HOL_cs 1),
    99 	(rtac is_ub_thelub 1),
   100 	(resolve_tac prems 1),
   101 	(res_inst_tac [("y","X(Suc(x))")] trans_less 1),
   102 	(rtac (chain_mono RS mp) 1),
   103 	(resolve_tac prems 1),
   104 	(rtac (not_less_eq RS subst) 1),
   105 	(atac 1),
   106 	(res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1),
   107 	(rtac sym 1),
   108 	(asm_simp_tac nat_ss 1),
   109 	(rtac is_ub_thelub 1),
   110 	(resolve_tac prems 1)
   111 	]);
   112 
   113 val lub_equal2 = prove_goal Pcpo.thy 
   114 "[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
   115 \ ==> lub(range(X))=lub(range(Y))"
   116  (fn prems =>
   117 	[
   118 	(rtac antisym_less 1),
   119 	(rtac lub_mono2 1),
   120 	(REPEAT (resolve_tac prems 1)),
   121 	(cut_facts_tac prems 1),
   122 	(rtac lub_mono2 1),
   123 	(safe_tac HOL_cs),
   124 	(step_tac HOL_cs 1),
   125 	(safe_tac HOL_cs),
   126 	(rtac sym 1),
   127 	(fast_tac HOL_cs 1)
   128 	]);
   129 
   130 val lub_mono3 = prove_goal Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\
   131 \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
   132  (fn prems =>
   133 	[
   134 	(cut_facts_tac prems 1),
   135 	(rtac is_lub_thelub 1),
   136 	(atac 1),
   137 	(rtac ub_rangeI 1),
   138 	(strip_tac 1),
   139 	(etac allE 1),
   140 	(etac exE 1),
   141 	(rtac trans_less 1),
   142 	(rtac is_ub_thelub 2),
   143 	(atac 2),
   144 	(atac 1)
   145 	]);
   146 
   147 (* ------------------------------------------------------------------------ *)
   148 (* usefull lemmas about UU                                                  *)
   149 (* ------------------------------------------------------------------------ *)
   150 
   151 val eq_UU_iff = prove_goal Pcpo.thy "(x=UU)=(x<<UU)"
   152  (fn prems =>
   153 	[
   154 	(rtac iffI 1),
   155 	(hyp_subst_tac 1),
   156 	(rtac refl_less 1),
   157 	(rtac antisym_less 1),
   158 	(atac 1),
   159 	(rtac minimal 1)
   160 	]);
   161 
   162 val UU_I = prove_goal Pcpo.thy "x << UU ==> x = UU"
   163  (fn prems =>
   164 	[
   165 	(rtac (eq_UU_iff RS ssubst) 1),
   166 	(resolve_tac prems 1)
   167 	]);
   168 
   169 val not_less2not_eq = prove_goal Pcpo.thy "~x<<y ==> ~x=y"
   170  (fn prems =>
   171 	[
   172 	(cut_facts_tac prems 1),
   173 	(rtac classical3 1),
   174 	(atac 1),
   175 	(hyp_subst_tac 1),
   176 	(rtac refl_less 1)
   177 	]);
   178 
   179 
   180 val chain_UU_I = prove_goal Pcpo.thy
   181 	"[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU"
   182 (fn prems =>
   183 	[
   184 	(cut_facts_tac prems 1),
   185 	(rtac allI 1),
   186 	(rtac antisym_less 1),
   187 	(rtac minimal 2),
   188 	(res_inst_tac [("t","UU")] subst 1),
   189 	(atac 1),
   190 	(etac is_ub_thelub 1)
   191 	]);
   192 
   193 
   194 val chain_UU_I_inverse = prove_goal Pcpo.thy 
   195 	"!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
   196 (fn prems =>
   197 	[
   198 	(cut_facts_tac prems 1),
   199 	(rtac lub_chain_maxelem 1),
   200 	(rtac is_chainI 1),
   201 	(rtac allI 1),
   202 	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
   203 	(rtac sym 1),
   204 	(etac spec 1),
   205 	(rtac minimal 1),
   206 	(rtac exI 1),
   207 	(etac spec 1),
   208 	(rtac allI 1),
   209 	(rtac (antisym_less_inverse RS conjunct1) 1),
   210 	(etac spec 1)
   211 	]);
   212 
   213 val chain_UU_I_inverse2 = prove_goal Pcpo.thy 
   214 	"~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU"
   215  (fn prems =>
   216 	[
   217 	(cut_facts_tac prems 1),
   218 	(rtac (notall2ex RS iffD1) 1),
   219 	(rtac swap 1),
   220 	(rtac chain_UU_I_inverse 2),
   221 	(etac notnotD 2),
   222 	(atac 1)
   223 	]);
   224 
   225 
   226 val notUU_I = prove_goal Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU"
   227 (fn prems =>
   228 	[
   229 	(cut_facts_tac prems 1),
   230 	(etac contrapos 1),
   231 	(rtac UU_I 1),
   232 	(hyp_subst_tac 1),
   233 	(atac 1)
   234 	]);
   235 
   236 
   237 val chain_mono2 = prove_goal Pcpo.thy 
   238 "[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
   239 \ ==> ? j.!i.j<i-->~Y(i)=UU"
   240  (fn prems =>
   241 	[
   242 	(cut_facts_tac prems 1),
   243 	(safe_tac HOL_cs),
   244 	(step_tac HOL_cs 1),
   245 	(strip_tac 1),
   246 	(rtac notUU_I 1),
   247 	(atac 2),
   248 	(etac (chain_mono RS mp) 1),
   249 	(atac 1)
   250 	]);
   251 
   252 
   253 
   254 
   255 (* ------------------------------------------------------------------------ *)
   256 (* uniqueness in void                                                       *)
   257 (* ------------------------------------------------------------------------ *)
   258 
   259 val unique_void2 = prove_goal Pcpo.thy "x::void=UU"
   260  (fn prems =>
   261 	[
   262 	(rtac (inst_void_pcpo RS ssubst) 1),
   263 	(rtac (Rep_Void_inverse RS subst) 1),
   264 	(rtac (Rep_Void_inverse RS subst) 1),
   265 	(rtac arg_cong 1),
   266 	(rtac box_equals 1),
   267 	(rtac refl 1),
   268 	(rtac (unique_void RS sym) 1),
   269 	(rtac (unique_void RS sym) 1)
   270 	]);
   271 
   272