src/HOLCF/IOA/meta_theory/Sequence.thy
author huffman
Sun Mar 07 16:39:31 2010 -0800 (2010-03-07)
changeset 35642 f478d5a9d238
parent 35532 60647586b173
child 35781 b7738ab762b1
permissions -rw-r--r--
generate separate qualified theorem name for each type's reach and take_lemma
     1 (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
     2     Author:     Olaf Müller
     3 
     4 Sequences over flat domains with lifted elements.
     5 *)
     6 
     7 theory Sequence
     8 imports Seq
     9 begin
    10 
    11 defaultsort type
    12 
    13 types 'a Seq = "'a::type lift seq"
    14 
    15 consts
    16 
    17   Consq            ::"'a            => 'a Seq -> 'a Seq"
    18   Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
    19   Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
    20   Forall           ::"('a => bool)  => 'a Seq => bool"
    21   Last             ::"'a Seq        -> 'a lift"
    22   Dropwhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
    23   Takewhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
    24   Zip              ::"'a Seq        -> 'b Seq -> ('a * 'b) Seq"
    25   Flat             ::"('a Seq) seq   -> 'a Seq"
    26 
    27   Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"
    28 
    29 abbreviation
    30   Consq_syn  ("(_/>>_)"  [66,65] 65) where
    31   "a>>s == Consq a$s"
    32 
    33 notation (xsymbols)
    34   Consq_syn  ("(_\<leadsto>_)"  [66,65] 65)
    35 
    36 
    37 (* list Enumeration *)
    38 syntax
    39   "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
    40   "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
    41 translations
    42   "[x, xs!]"     == "x>>[xs!]"
    43   "[x!]"         == "x>>nil"
    44   "[x, xs?]"     == "x>>[xs?]"
    45   "[x?]"         == "x>>CONST UU"
    46 
    47 defs
    48 
    49 Consq_def:     "Consq a == LAM s. Def a ## s"
    50 
    51 Filter_def:    "Filter P == sfilter$(flift2 P)"
    52 
    53 Map_def:       "Map f  == smap$(flift2 f)"
    54 
    55 Forall_def:    "Forall P == sforall (flift2 P)"
    56 
    57 Last_def:      "Last == slast"
    58 
    59 Dropwhile_def: "Dropwhile P == sdropwhile$(flift2 P)"
    60 
    61 Takewhile_def: "Takewhile P == stakewhile$(flift2 P)"
    62 
    63 Flat_def:      "Flat == sflat"
    64 
    65 Zip_def:
    66   "Zip == (fix$(LAM h t1 t2. case t1 of
    67                nil   => nil
    68              | x##xs => (case t2 of
    69                           nil => UU
    70                         | y##ys => (case x of
    71                                       UU  => UU
    72                                     | Def a => (case y of
    73                                                   UU => UU
    74                                                 | Def b => Def (a,b)##(h$xs$ys))))))"
    75 
    76 Filter2_def:    "Filter2 P == (fix$(LAM h t. case t of
    77             nil => nil
    78           | x##xs => (case x of UU => UU | Def y => (if P y
    79                      then x##(h$xs)
    80                      else     h$xs))))"
    81 
    82 declare andalso_and [simp]
    83 declare andalso_or [simp]
    84 
    85 subsection "recursive equations of operators"
    86 
    87 subsubsection "Map"
    88 
    89 lemma Map_UU: "Map f$UU =UU"
    90 by (simp add: Map_def)
    91 
    92 lemma Map_nil: "Map f$nil =nil"
    93 by (simp add: Map_def)
    94 
    95 lemma Map_cons: "Map f$(x>>xs)=(f x) >> Map f$xs"
    96 by (simp add: Map_def Consq_def flift2_def)
    97 
    98 
    99 subsubsection {* Filter *}
   100 
   101 lemma Filter_UU: "Filter P$UU =UU"
   102 by (simp add: Filter_def)
   103 
   104 lemma Filter_nil: "Filter P$nil =nil"
   105 by (simp add: Filter_def)
   106 
   107 lemma Filter_cons:
   108   "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"
   109 by (simp add: Filter_def Consq_def flift2_def If_and_if)
   110 
   111 
   112 subsubsection {* Forall *}
   113 
   114 lemma Forall_UU: "Forall P UU"
   115 by (simp add: Forall_def sforall_def)
   116 
   117 lemma Forall_nil: "Forall P nil"
   118 by (simp add: Forall_def sforall_def)
   119 
   120 lemma Forall_cons: "Forall P (x>>xs)= (P x & Forall P xs)"
   121 by (simp add: Forall_def sforall_def Consq_def flift2_def)
   122 
   123 
   124 subsubsection {* Conc *}
   125 
   126 lemma Conc_cons: "(x>>xs) @@ y = x>>(xs @@y)"
   127 by (simp add: Consq_def)
   128 
   129 
   130 subsubsection {* Takewhile *}
   131 
   132 lemma Takewhile_UU: "Takewhile P$UU =UU"
   133 by (simp add: Takewhile_def)
   134 
   135 lemma Takewhile_nil: "Takewhile P$nil =nil"
   136 by (simp add: Takewhile_def)
   137 
   138 lemma Takewhile_cons:
   139   "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"
   140 by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
   141 
   142 
   143 subsubsection {* DropWhile *}
   144 
   145 lemma Dropwhile_UU: "Dropwhile P$UU =UU"
   146 by (simp add: Dropwhile_def)
   147 
   148 lemma Dropwhile_nil: "Dropwhile P$nil =nil"
   149 by (simp add: Dropwhile_def)
   150 
   151 lemma Dropwhile_cons:
   152   "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"
   153 by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
   154 
   155 
   156 subsubsection {* Last *}
   157 
   158 lemma Last_UU: "Last$UU =UU"
   159 by (simp add: Last_def)
   160 
   161 lemma Last_nil: "Last$nil =UU"
   162 by (simp add: Last_def)
   163 
   164 lemma Last_cons: "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"
   165 apply (simp add: Last_def Consq_def)
   166 apply (cases xs)
   167 apply simp_all
   168 done
   169 
   170 
   171 subsubsection {* Flat *}
   172 
   173 lemma Flat_UU: "Flat$UU =UU"
   174 by (simp add: Flat_def)
   175 
   176 lemma Flat_nil: "Flat$nil =nil"
   177 by (simp add: Flat_def)
   178 
   179 lemma Flat_cons: "Flat$(x##xs)= x @@ (Flat$xs)"
   180 by (simp add: Flat_def Consq_def)
   181 
   182 
   183 subsubsection {* Zip *}
   184 
   185 lemma Zip_unfold:
   186 "Zip = (LAM t1 t2. case t1 of
   187                 nil   => nil
   188               | x##xs => (case t2 of
   189                            nil => UU
   190                          | y##ys => (case x of
   191                                        UU  => UU
   192                                      | Def a => (case y of
   193                                                    UU => UU
   194                                                  | Def b => Def (a,b)##(Zip$xs$ys)))))"
   195 apply (rule trans)
   196 apply (rule fix_eq2)
   197 apply (rule Zip_def)
   198 apply (rule beta_cfun)
   199 apply simp
   200 done
   201 
   202 lemma Zip_UU1: "Zip$UU$y =UU"
   203 apply (subst Zip_unfold)
   204 apply simp
   205 done
   206 
   207 lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
   208 apply (subst Zip_unfold)
   209 apply simp
   210 apply (cases x)
   211 apply simp_all
   212 done
   213 
   214 lemma Zip_nil: "Zip$nil$y =nil"
   215 apply (subst Zip_unfold)
   216 apply simp
   217 done
   218 
   219 lemma Zip_cons_nil: "Zip$(x>>xs)$nil= UU"
   220 apply (subst Zip_unfold)
   221 apply (simp add: Consq_def)
   222 done
   223 
   224 lemma Zip_cons: "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"
   225 apply (rule trans)
   226 apply (subst Zip_unfold)
   227 apply simp
   228 apply (simp add: Consq_def)
   229 done
   230 
   231 lemmas [simp del] =
   232   sfilter_UU sfilter_nil sfilter_cons
   233   smap_UU smap_nil smap_cons
   234   sforall2_UU sforall2_nil sforall2_cons
   235   slast_UU slast_nil slast_cons
   236   stakewhile_UU  stakewhile_nil  stakewhile_cons
   237   sdropwhile_UU  sdropwhile_nil  sdropwhile_cons
   238   sflat_UU sflat_nil sflat_cons
   239   szip_UU1 szip_UU2 szip_nil szip_cons_nil szip_cons
   240 
   241 lemmas [simp] =
   242   Filter_UU Filter_nil Filter_cons
   243   Map_UU Map_nil Map_cons
   244   Forall_UU Forall_nil Forall_cons
   245   Last_UU Last_nil Last_cons
   246   Conc_cons
   247   Takewhile_UU Takewhile_nil Takewhile_cons
   248   Dropwhile_UU Dropwhile_nil Dropwhile_cons
   249   Zip_UU1 Zip_UU2 Zip_nil Zip_cons_nil Zip_cons
   250 
   251 
   252 
   253 section "Cons"
   254 
   255 lemma Consq_def2: "a>>s = (Def a)##s"
   256 apply (simp add: Consq_def)
   257 done
   258 
   259 lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a >> s)"
   260 apply (simp add: Consq_def2)
   261 apply (cut_tac seq.exhaust)
   262 apply (fast dest: not_Undef_is_Def [THEN iffD1])
   263 done
   264 
   265 
   266 lemma Seq_cases:
   267 "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P"
   268 apply (cut_tac x="x" in Seq_exhaust)
   269 apply (erule disjE)
   270 apply simp
   271 apply (erule disjE)
   272 apply simp
   273 apply (erule exE)+
   274 apply simp
   275 done
   276 
   277 (*
   278 fun Seq_case_tac s i = rule_tac x",s)] Seq_cases i
   279           THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
   280 *)
   281 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
   282 (*
   283 fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
   284                                              THEN Asm_full_simp_tac (i+1)
   285                                              THEN Asm_full_simp_tac i;
   286 *)
   287 
   288 lemma Cons_not_UU: "a>>s ~= UU"
   289 apply (subst Consq_def2)
   290 apply simp
   291 done
   292 
   293 
   294 lemma Cons_not_less_UU: "~(a>>x) << UU"
   295 apply (rule notI)
   296 apply (drule antisym_less)
   297 apply simp
   298 apply (simp add: Cons_not_UU)
   299 done
   300 
   301 lemma Cons_not_less_nil: "~a>>s << nil"
   302 apply (simp add: Consq_def2)
   303 done
   304 
   305 lemma Cons_not_nil: "a>>s ~= nil"
   306 apply (simp add: Consq_def2)
   307 done
   308 
   309 lemma Cons_not_nil2: "nil ~= a>>s"
   310 apply (simp add: Consq_def2)
   311 done
   312 
   313 lemma Cons_inject_eq: "(a>>s = b>>t) = (a = b & s = t)"
   314 apply (simp only: Consq_def2)
   315 apply (simp add: scons_inject_eq)
   316 done
   317 
   318 lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
   319 apply (simp add: Consq_def2)
   320 done
   321 
   322 lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
   323 apply (simp add: Consq_def)
   324 done
   325 
   326 lemmas [simp] =
   327   Cons_not_nil2 Cons_inject_eq Cons_inject_less_eq seq_take_Cons
   328   Cons_not_UU Cons_not_less_UU Cons_not_less_nil Cons_not_nil
   329 
   330 
   331 subsection "induction"
   332 
   333 lemma Seq_induct:
   334 "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
   335 apply (erule (2) seq.ind)
   336 apply defined
   337 apply (simp add: Consq_def)
   338 done
   339 
   340 lemma Seq_FinitePartial_ind:
   341 "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]
   342                 ==> seq_finite x --> P x"
   343 apply (erule (1) seq_finite_ind)
   344 apply defined
   345 apply (simp add: Consq_def)
   346 done
   347 
   348 lemma Seq_Finite_ind:
   349 "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
   350 apply (erule (1) Finite.induct)
   351 apply defined
   352 apply (simp add: Consq_def)
   353 done
   354 
   355 
   356 (* rws are definitions to be unfolded for admissibility check *)
   357 (*
   358 fun Seq_induct_tac s rws i = rule_tac x",s)] Seq_induct i
   359                          THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
   360                          THEN simp add: rws) i;
   361 
   362 fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
   363                               THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
   364 
   365 fun pair_tac s = rule_tac p",s)] PairE
   366                           THEN' hyp_subst_tac THEN' Simp_tac;
   367 *)
   368 (* induction on a sequence of pairs with pairsplitting and simplification *)
   369 (*
   370 fun pair_induct_tac s rws i =
   371            rule_tac x",s)] Seq_induct i
   372            THEN pair_tac "a" (i+3)
   373            THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
   374            THEN simp add: rws) i;
   375 *)
   376 
   377 
   378 (* ------------------------------------------------------------------------------------ *)
   379 
   380 subsection "HD,TL"
   381 
   382 lemma HD_Cons [simp]: "HD$(x>>y) = Def x"
   383 apply (simp add: Consq_def)
   384 done
   385 
   386 lemma TL_Cons [simp]: "TL$(x>>y) = y"
   387 apply (simp add: Consq_def)
   388 done
   389 
   390 (* ------------------------------------------------------------------------------------ *)
   391 
   392 subsection "Finite, Partial, Infinite"
   393 
   394 lemma Finite_Cons [simp]: "Finite (a>>xs) = Finite xs"
   395 apply (simp add: Consq_def2 Finite_cons)
   396 done
   397 
   398 lemma FiniteConc_1: "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)"
   399 apply (erule Seq_Finite_ind, simp_all)
   400 done
   401 
   402 lemma FiniteConc_2:
   403 "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"
   404 apply (erule Seq_Finite_ind)
   405 (* nil*)
   406 apply (intro strip)
   407 apply (rule_tac x="x" in Seq_cases, simp_all)
   408 (* cons *)
   409 apply (intro strip)
   410 apply (rule_tac x="x" in Seq_cases, simp_all)
   411 apply (rule_tac x="y" in Seq_cases, simp_all)
   412 done
   413 
   414 lemma FiniteConc [simp]: "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)"
   415 apply (rule iffI)
   416 apply (erule FiniteConc_2 [rule_format])
   417 apply (rule refl)
   418 apply (rule FiniteConc_1 [rule_format])
   419 apply auto
   420 done
   421 
   422 
   423 lemma FiniteMap1: "Finite s ==> Finite (Map f$s)"
   424 apply (erule Seq_Finite_ind, simp_all)
   425 done
   426 
   427 lemma FiniteMap2: "Finite s ==> ! t. (s = Map f$t) --> Finite t"
   428 apply (erule Seq_Finite_ind)
   429 apply (intro strip)
   430 apply (rule_tac x="t" in Seq_cases, simp_all)
   431 (* main case *)
   432 apply auto
   433 apply (rule_tac x="t" in Seq_cases, simp_all)
   434 done
   435 
   436 lemma Map2Finite: "Finite (Map f$s) = Finite s"
   437 apply auto
   438 apply (erule FiniteMap2 [rule_format])
   439 apply (rule refl)
   440 apply (erule FiniteMap1)
   441 done
   442 
   443 
   444 lemma FiniteFilter: "Finite s ==> Finite (Filter P$s)"
   445 apply (erule Seq_Finite_ind, simp_all)
   446 done
   447 
   448 
   449 (* ----------------------------------------------------------------------------------- *)
   450 
   451 subsection "Conc"
   452 
   453 lemma Conc_cong: "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"
   454 apply (erule Seq_Finite_ind, simp_all)
   455 done
   456 
   457 lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"
   458 apply (rule_tac x="x" in Seq_induct, simp_all)
   459 done
   460 
   461 lemma nilConc [simp]: "s@@ nil = s"
   462 apply (rule_tac x="s" in seq.ind)
   463 apply simp
   464 apply simp
   465 apply simp
   466 apply simp
   467 done
   468 
   469 
   470 (* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
   471 lemma nil_is_Conc: "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)"
   472 apply (rule_tac x="x" in Seq_cases)
   473 apply auto
   474 done
   475 
   476 lemma nil_is_Conc2: "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)"
   477 apply (rule_tac x="x" in Seq_cases)
   478 apply auto
   479 done
   480 
   481 
   482 (* ------------------------------------------------------------------------------------ *)
   483 
   484 subsection "Last"
   485 
   486 lemma Finite_Last1: "Finite s ==> s~=nil --> Last$s~=UU"
   487 apply (erule Seq_Finite_ind, simp_all)
   488 done
   489 
   490 lemma Finite_Last2: "Finite s ==> Last$s=UU --> s=nil"
   491 apply (erule Seq_Finite_ind, simp_all)
   492 apply fast
   493 done
   494 
   495 
   496 (* ------------------------------------------------------------------------------------ *)
   497 
   498 
   499 subsection "Filter, Conc"
   500 
   501 
   502 lemma FilterPQ: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
   503 apply (rule_tac x="s" in Seq_induct, simp_all)
   504 done
   505 
   506 lemma FilterConc: "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"
   507 apply (simp add: Filter_def sfiltersconc)
   508 done
   509 
   510 (* ------------------------------------------------------------------------------------ *)
   511 
   512 subsection "Map"
   513 
   514 lemma MapMap: "Map f$(Map g$s) = Map (f o g)$s"
   515 apply (rule_tac x="s" in Seq_induct, simp_all)
   516 done
   517 
   518 lemma MapConc: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
   519 apply (rule_tac x="x" in Seq_induct, simp_all)
   520 done
   521 
   522 lemma MapFilter: "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"
   523 apply (rule_tac x="x" in Seq_induct, simp_all)
   524 done
   525 
   526 lemma nilMap: "nil = (Map f$s) --> s= nil"
   527 apply (rule_tac x="s" in Seq_cases, simp_all)
   528 done
   529 
   530 
   531 lemma ForallMap: "Forall P (Map f$s) = Forall (P o f) s"
   532 apply (rule_tac x="s" in Seq_induct)
   533 apply (simp add: Forall_def sforall_def)
   534 apply simp_all
   535 done
   536 
   537 
   538 
   539 
   540 (* ------------------------------------------------------------------------------------ *)
   541 
   542 subsection "Forall"
   543 
   544 
   545 lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x)
   546          --> Forall Q ys"
   547 apply (rule_tac x="ys" in Seq_induct)
   548 apply (simp add: Forall_def sforall_def)
   549 apply simp_all
   550 done
   551 
   552 lemmas ForallPForallQ =
   553   ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI]
   554 
   555 lemma Forall_Conc_impl: "(Forall P x & Forall P y) --> Forall P (x @@ y)"
   556 apply (rule_tac x="x" in Seq_induct)
   557 apply (simp add: Forall_def sforall_def)
   558 apply simp_all
   559 done
   560 
   561 lemma Forall_Conc [simp]:
   562   "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"
   563 apply (erule Seq_Finite_ind, simp_all)
   564 done
   565 
   566 lemma ForallTL1: "Forall P s  --> Forall P (TL$s)"
   567 apply (rule_tac x="s" in Seq_induct)
   568 apply (simp add: Forall_def sforall_def)
   569 apply simp_all
   570 done
   571 
   572 lemmas ForallTL = ForallTL1 [THEN mp]
   573 
   574 lemma ForallDropwhile1: "Forall P s  --> Forall P (Dropwhile Q$s)"
   575 apply (rule_tac x="s" in Seq_induct)
   576 apply (simp add: Forall_def sforall_def)
   577 apply simp_all
   578 done
   579 
   580 lemmas ForallDropwhile = ForallDropwhile1 [THEN mp]
   581 
   582 
   583 (* only admissible in t, not if done in s *)
   584 
   585 lemma Forall_prefix: "! s. Forall P s --> t<<s --> Forall P t"
   586 apply (rule_tac x="t" in Seq_induct)
   587 apply (simp add: Forall_def sforall_def)
   588 apply simp_all
   589 apply (intro strip)
   590 apply (rule_tac x="sa" in Seq_cases)
   591 apply simp
   592 apply auto
   593 done
   594 
   595 lemmas Forall_prefixclosed = Forall_prefix [rule_format]
   596 
   597 lemma Forall_postfixclosed:
   598   "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"
   599 apply auto
   600 done
   601 
   602 
   603 lemma ForallPFilterQR1:
   604   "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"
   605 apply (rule_tac x="tr" in Seq_induct)
   606 apply (simp add: Forall_def sforall_def)
   607 apply simp_all
   608 done
   609 
   610 lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI]
   611 
   612 
   613 (* ------------------------------------------------------------------------------------- *)
   614 
   615 subsection "Forall, Filter"
   616 
   617 
   618 lemma ForallPFilterP: "Forall P (Filter P$x)"
   619 apply (simp add: Filter_def Forall_def forallPsfilterP)
   620 done
   621 
   622 (* holds also in other direction, then equal to forallPfilterP *)
   623 lemma ForallPFilterPid1: "Forall P x --> Filter P$x = x"
   624 apply (rule_tac x="x" in Seq_induct)
   625 apply (simp add: Forall_def sforall_def Filter_def)
   626 apply simp_all
   627 done
   628 
   629 lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]
   630 
   631 
   632 (* holds also in other direction *)
   633 lemma ForallnPFilterPnil1: "!! ys . Finite ys ==>
   634    Forall (%x. ~P x) ys --> Filter P$ys = nil "
   635 apply (erule Seq_Finite_ind, simp_all)
   636 done
   637 
   638 lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]
   639 
   640 
   641 (* holds also in other direction *)
   642 lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys
   643                   --> Filter P$ys = UU "
   644 apply (rule_tac x="ys" in Seq_induct)
   645 apply (simp add: Forall_def sforall_def)
   646 apply simp_all
   647 done
   648 
   649 lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI]
   650 
   651 
   652 (* inverse of ForallnPFilterPnil *)
   653 
   654 lemma FilternPnilForallP1: "!! ys . Filter P$ys = nil -->
   655    (Forall (%x. ~P x) ys & Finite ys)"
   656 apply (rule_tac x="ys" in Seq_induct)
   657 (* adm *)
   658 apply (simp add: Forall_def sforall_def)
   659 (* base cases *)
   660 apply simp
   661 apply simp
   662 (* main case *)
   663 apply simp
   664 done
   665 
   666 lemmas FilternPnilForallP = FilternPnilForallP1 [THEN mp]
   667 
   668 (* inverse of ForallnPFilterPUU. proved apply 2 lemmas because of adm problems *)
   669 
   670 lemma FilterUU_nFinite_lemma1: "Finite ys ==> Filter P$ys ~= UU"
   671 apply (erule Seq_Finite_ind, simp_all)
   672 done
   673 
   674 lemma FilterUU_nFinite_lemma2: "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"
   675 apply (rule_tac x="ys" in Seq_induct)
   676 apply (simp add: Forall_def sforall_def)
   677 apply simp_all
   678 done
   679 
   680 lemma FilternPUUForallP:
   681   "Filter P$ys = UU ==> (Forall (%x. ~P x) ys  & ~Finite ys)"
   682 apply (rule conjI)
   683 apply (cut_tac FilterUU_nFinite_lemma2 [THEN mp, COMP rev_contrapos])
   684 apply auto
   685 apply (blast dest!: FilterUU_nFinite_lemma1)
   686 done
   687 
   688 
   689 lemma ForallQFilterPnil:
   690   "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|]
   691     ==> Filter P$ys = nil"
   692 apply (erule ForallnPFilterPnil)
   693 apply (erule ForallPForallQ)
   694 apply auto
   695 done
   696 
   697 lemma ForallQFilterPUU:
   698  "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|]
   699     ==> Filter P$ys = UU "
   700 apply (erule ForallnPFilterPUU)
   701 apply (erule ForallPForallQ)
   702 apply auto
   703 done
   704 
   705 
   706 
   707 (* ------------------------------------------------------------------------------------- *)
   708 
   709 subsection "Takewhile, Forall, Filter"
   710 
   711 
   712 lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P$x)"
   713 apply (simp add: Forall_def Takewhile_def sforallPstakewhileP)
   714 done
   715 
   716 
   717 lemma ForallPTakewhileQ [simp]:
   718 "!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"
   719 apply (rule ForallPForallQ)
   720 apply (rule ForallPTakewhileP)
   721 apply auto
   722 done
   723 
   724 
   725 lemma FilterPTakewhileQnil [simp]:
   726   "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |]
   727    ==> Filter P$(Takewhile Q$ys) = nil"
   728 apply (erule ForallnPFilterPnil)
   729 apply (rule ForallPForallQ)
   730 apply (rule ForallPTakewhileP)
   731 apply auto
   732 done
   733 
   734 lemma FilterPTakewhileQid [simp]:
   735  "!! Q P. [| !!x. Q x ==> P x |] ==>
   736             Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
   737 apply (rule ForallPFilterPid)
   738 apply (rule ForallPForallQ)
   739 apply (rule ForallPTakewhileP)
   740 apply auto
   741 done
   742 
   743 
   744 lemma Takewhile_idempotent: "Takewhile P$(Takewhile P$s) = Takewhile P$s"
   745 apply (rule_tac x="s" in Seq_induct)
   746 apply (simp add: Forall_def sforall_def)
   747 apply simp_all
   748 done
   749 
   750 lemma ForallPTakewhileQnP [simp]:
   751  "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"
   752 apply (rule_tac x="s" in Seq_induct)
   753 apply (simp add: Forall_def sforall_def)
   754 apply simp_all
   755 done
   756 
   757 lemma ForallPDropwhileQnP [simp]:
   758  "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"
   759 apply (rule_tac x="s" in Seq_induct)
   760 apply (simp add: Forall_def sforall_def)
   761 apply simp_all
   762 done
   763 
   764 
   765 lemma TakewhileConc1:
   766  "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"
   767 apply (rule_tac x="s" in Seq_induct)
   768 apply (simp add: Forall_def sforall_def)
   769 apply simp_all
   770 done
   771 
   772 lemmas TakewhileConc = TakewhileConc1 [THEN mp]
   773 
   774 lemma DropwhileConc1:
   775  "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"
   776 apply (erule Seq_Finite_ind, simp_all)
   777 done
   778 
   779 lemmas DropwhileConc = DropwhileConc1 [THEN mp]
   780 
   781 
   782 
   783 (* ----------------------------------------------------------------------------------- *)
   784 
   785 subsection "coinductive characterizations of Filter"
   786 
   787 
   788 lemma divide_Seq_lemma:
   789  "HD$(Filter P$y) = Def x
   790     --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) 
   791              & Finite (Takewhile (%x. ~ P x)$y)  & P x"
   792 
   793 (* FIX: pay attention: is only admissible with chain-finite package to be added to
   794         adm test and Finite f x admissibility *)
   795 apply (rule_tac x="y" in Seq_induct)
   796 apply (simp add: adm_subst [OF _ adm_Finite])
   797 apply simp
   798 apply simp
   799 apply (case_tac "P a")
   800  apply simp
   801  apply blast
   802 (* ~ P a *)
   803 apply simp
   804 done
   805 
   806 lemma divide_Seq: "(x>>xs) << Filter P$y 
   807    ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))
   808       & Finite (Takewhile (%a. ~ P a)$y)  & P x"
   809 apply (rule divide_Seq_lemma [THEN mp])
   810 apply (drule_tac f="HD" and x="x>>xs" in  monofun_cfun_arg)
   811 apply simp
   812 done
   813 
   814 
   815 lemma nForall_HDFilter:
   816  "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
   817 (* Pay attention: is only admissible with chain-finite package to be added to
   818         adm test *)
   819 apply (rule_tac x="y" in Seq_induct)
   820 apply (simp add: Forall_def sforall_def)
   821 apply simp_all
   822 done
   823 
   824 
   825 lemma divide_Seq2: "~Forall P y
   826   ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) &
   827       Finite (Takewhile P$y) & (~ P x)"
   828 apply (drule nForall_HDFilter [THEN mp])
   829 apply safe
   830 apply (rule_tac x="x" in exI)
   831 apply (cut_tac P1="%x. ~ P x" in divide_Seq_lemma [THEN mp])
   832 apply auto
   833 done
   834 
   835 
   836 lemma divide_Seq3: "~Forall P y
   837   ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"
   838 apply (drule divide_Seq2)
   839 (*Auto_tac no longer proves it*)
   840 apply fastsimp
   841 done
   842 
   843 lemmas [simp] = FilterPQ FilterConc Conc_cong
   844 
   845 
   846 (* ------------------------------------------------------------------------------------- *)
   847 
   848 
   849 subsection "take_lemma"
   850 
   851 lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
   852 apply (rule iffI)
   853 apply (rule seq.take_lemma)
   854 apply auto
   855 done
   856 
   857 lemma take_reduction1:
   858 "  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2)
   859     --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))"
   860 apply (rule_tac x="x" in Seq_induct)
   861 apply simp_all
   862 apply (intro strip)
   863 apply (case_tac "n")
   864 apply auto
   865 apply (case_tac "n")
   866 apply auto
   867 done
   868 
   869 
   870 lemma take_reduction:
   871  "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|]
   872   ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))"
   873 apply (auto intro!: take_reduction1 [rule_format])
   874 done
   875 
   876 (* ------------------------------------------------------------------
   877           take-lemma and take_reduction for << instead of =
   878    ------------------------------------------------------------------ *)
   879 
   880 lemma take_reduction_less1:
   881 "  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2)
   882     --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))"
   883 apply (rule_tac x="x" in Seq_induct)
   884 apply simp_all
   885 apply (intro strip)
   886 apply (case_tac "n")
   887 apply auto
   888 apply (case_tac "n")
   889 apply auto
   890 done
   891 
   892 
   893 lemma take_reduction_less:
   894  "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|]
   895   ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))"
   896 apply (auto intro!: take_reduction_less1 [rule_format])
   897 done
   898 
   899 lemma take_lemma_less1:
   900   assumes "!! n. seq_take n$s1 << seq_take n$s2"
   901   shows "s1<<s2"
   902 apply (rule_tac t="s1" in seq.reach [THEN subst])
   903 apply (rule_tac t="s2" in seq.reach [THEN subst])
   904 apply (rule lub_mono)
   905 apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
   906 apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
   907 apply (rule assms)
   908 done
   909 
   910 
   911 lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')"
   912 apply (rule iffI)
   913 apply (rule take_lemma_less1)
   914 apply auto
   915 apply (erule monofun_cfun_arg)
   916 done
   917 
   918 (* ------------------------------------------------------------------
   919           take-lemma proof principles
   920    ------------------------------------------------------------------ *)
   921 
   922 lemma take_lemma_principle1:
   923  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
   924             !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
   925                           ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |]
   926                ==> A x --> (f x)=(g x)"
   927 apply (case_tac "Forall Q x")
   928 apply (auto dest!: divide_Seq3)
   929 done
   930 
   931 lemma take_lemma_principle2:
   932   "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
   933            !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
   934                           ==> ! n. seq_take n$(f (s1 @@ y>>s2))
   935                                  = seq_take n$(g (s1 @@ y>>s2)) |]
   936                ==> A x --> (f x)=(g x)"
   937 apply (case_tac "Forall Q x")
   938 apply (auto dest!: divide_Seq3)
   939 apply (rule seq.take_lemma)
   940 apply auto
   941 done
   942 
   943 
   944 (* Note: in the following proofs the ordering of proof steps is very
   945          important, as otherwise either (Forall Q s1) would be in the IH as
   946          assumption (then rule useless) or it is not possible to strengthen
   947          the IH apply doing a forall closure of the sequence t (then rule also useless).
   948          This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
   949          to be imbuilt into the rule, as induction has to be done early and the take lemma
   950          has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
   951 
   952 lemma take_lemma_induct:
   953 "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
   954          !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
   955                           Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
   956                           ==>   seq_take (Suc n)$(f (s1 @@ y>>s2))
   957                               = seq_take (Suc n)$(g (s1 @@ y>>s2)) |]
   958                ==> A x --> (f x)=(g x)"
   959 apply (rule impI)
   960 apply (rule seq.take_lemma)
   961 apply (rule mp)
   962 prefer 2 apply assumption
   963 apply (rule_tac x="x" in spec)
   964 apply (rule nat.induct)
   965 apply simp
   966 apply (rule allI)
   967 apply (case_tac "Forall Q xa")
   968 apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
   969 apply (auto dest!: divide_Seq3)
   970 done
   971 
   972 
   973 lemma take_lemma_less_induct:
   974 "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
   975         !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);
   976                           Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
   977                           ==>   seq_take n$(f (s1 @@ y>>s2))
   978                               = seq_take n$(g (s1 @@ y>>s2)) |]
   979                ==> A x --> (f x)=(g x)"
   980 apply (rule impI)
   981 apply (rule seq.take_lemma)
   982 apply (rule mp)
   983 prefer 2 apply assumption
   984 apply (rule_tac x="x" in spec)
   985 apply (rule nat_less_induct)
   986 apply (rule allI)
   987 apply (case_tac "Forall Q xa")
   988 apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
   989 apply (auto dest!: divide_Seq3)
   990 done
   991 
   992 
   993 
   994 lemma take_lemma_in_eq_out:
   995 "!! Q. [| A UU  ==> (f UU) = (g UU) ;
   996           A nil ==> (f nil) = (g nil) ;
   997           !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
   998                      A (y>>s) |]
   999                      ==>   seq_take (Suc n)$(f (y>>s))
  1000                          = seq_take (Suc n)$(g (y>>s)) |]
  1001                ==> A x --> (f x)=(g x)"
  1002 apply (rule impI)
  1003 apply (rule seq.take_lemma)
  1004 apply (rule mp)
  1005 prefer 2 apply assumption
  1006 apply (rule_tac x="x" in spec)
  1007 apply (rule nat.induct)
  1008 apply simp
  1009 apply (rule allI)
  1010 apply (rule_tac x="xa" in Seq_cases)
  1011 apply simp_all
  1012 done
  1013 
  1014 
  1015 (* ------------------------------------------------------------------------------------ *)
  1016 
  1017 subsection "alternative take_lemma proofs"
  1018 
  1019 
  1020 (* --------------------------------------------------------------- *)
  1021 (*              Alternative Proof of FilterPQ                      *)
  1022 (* --------------------------------------------------------------- *)
  1023 
  1024 declare FilterPQ [simp del]
  1025 
  1026 
  1027 (* In general: How to do this case without the same adm problems
  1028    as for the entire proof ? *)
  1029 lemma Filter_lemma1: "Forall (%x.~(P x & Q x)) s
  1030           --> Filter P$(Filter Q$s) =
  1031               Filter (%x. P x & Q x)$s"
  1032 
  1033 apply (rule_tac x="s" in Seq_induct)
  1034 apply (simp add: Forall_def sforall_def)
  1035 apply simp_all
  1036 done
  1037 
  1038 lemma Filter_lemma2: "Finite s ==>
  1039           (Forall (%x. (~P x) | (~ Q x)) s
  1040           --> Filter P$(Filter Q$s) = nil)"
  1041 apply (erule Seq_Finite_ind, simp_all)
  1042 done
  1043 
  1044 lemma Filter_lemma3: "Finite s ==>
  1045           Forall (%x. (~P x) | (~ Q x)) s
  1046           --> Filter (%x. P x & Q x)$s = nil"
  1047 apply (erule Seq_Finite_ind, simp_all)
  1048 done
  1049 
  1050 
  1051 lemma FilterPQ_takelemma: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
  1052 apply (rule_tac A1="%x. True" and
  1053                  Q1="%x.~(P x & Q x)" and x1="s" in
  1054                  take_lemma_induct [THEN mp])
  1055 (* better support for A = %x. True *)
  1056 apply (simp add: Filter_lemma1)
  1057 apply (simp add: Filter_lemma2 Filter_lemma3)
  1058 apply simp
  1059 done
  1060 
  1061 declare FilterPQ [simp]
  1062 
  1063 
  1064 (* --------------------------------------------------------------- *)
  1065 (*              Alternative Proof of MapConc                       *)
  1066 (* --------------------------------------------------------------- *)
  1067 
  1068 
  1069 
  1070 lemma MapConc_takelemma: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
  1071 apply (rule_tac A1="%x. True" and x1="x" in
  1072     take_lemma_in_eq_out [THEN mp])
  1073 apply auto
  1074 done
  1075 
  1076 
  1077 ML {*
  1078 
  1079 fun Seq_case_tac ctxt s i =
  1080   res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
  1081   THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
  1082 
  1083 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
  1084 fun Seq_case_simp_tac ctxt s i =
  1085   let val ss = simpset_of ctxt in
  1086     Seq_case_tac ctxt s i
  1087     THEN asm_simp_tac ss (i+2)
  1088     THEN asm_full_simp_tac ss (i+1)
  1089     THEN asm_full_simp_tac ss i
  1090   end;
  1091 
  1092 (* rws are definitions to be unfolded for admissibility check *)
  1093 fun Seq_induct_tac ctxt s rws i =
  1094   let val ss = simpset_of ctxt in
  1095     res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
  1096     THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
  1097     THEN simp_tac (ss addsimps rws) i
  1098   end;
  1099 
  1100 fun Seq_Finite_induct_tac ctxt i =
  1101   etac @{thm Seq_Finite_ind} i
  1102   THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i)));
  1103 
  1104 fun pair_tac ctxt s =
  1105   res_inst_tac ctxt [(("p", 0), s)] PairE
  1106   THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt);
  1107 
  1108 (* induction on a sequence of pairs with pairsplitting and simplification *)
  1109 fun pair_induct_tac ctxt s rws i =
  1110   let val ss = simpset_of ctxt in
  1111     res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
  1112     THEN pair_tac ctxt "a" (i+3)
  1113     THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
  1114     THEN simp_tac (ss addsimps rws) i
  1115   end;
  1116 
  1117 *}
  1118 
  1119 end