src/CCL/ex/Stream.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 35762 af3ff2ba4c54
child 41526 54b4686704af
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      CCL/ex/Stream.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 header {* Programs defined over streams *}
     7 
     8 theory Stream
     9 imports List
    10 begin
    11 
    12 consts
    13   iter1   ::  "[i=>i,i]=>i"
    14   iter2   ::  "[i=>i,i]=>i"
    15 
    16 defs
    17 
    18   iter1_def:   "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
    19   iter2_def:   "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
    20 
    21 
    22 (*
    23 Proving properties about infinite lists using coinduction:
    24     Lists(A)  is the set of all finite and infinite lists of elements of A.
    25     ILists(A) is the set of infinite lists of elements of A.
    26 *)
    27 
    28 
    29 subsection {* Map of composition is composition of maps *}
    30 
    31 lemma map_comp:
    32   assumes 1: "l:Lists(A)"
    33   shows "map(f o g,l) = map(f,map(g,l))"
    34   apply (tactic {* eq_coinduct3_tac @{context}
    35     "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
    36    apply (blast intro: 1)
    37   apply safe
    38   apply (drule ListsXH [THEN iffD1])
    39   apply (tactic "EQgen_tac @{context} [] 1")
    40    apply fastsimp
    41   done
    42 
    43 (*** Mapping the identity function leaves a list unchanged ***)
    44 
    45 lemma map_id:
    46   assumes 1: "l:Lists(A)"
    47   shows "map(%x. x,l) = l"
    48   apply (tactic {* eq_coinduct3_tac @{context}
    49     "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *})
    50   apply (blast intro: 1)
    51   apply safe
    52   apply (drule ListsXH [THEN iffD1])
    53   apply (tactic "EQgen_tac @{context} [] 1")
    54   apply blast
    55   done
    56 
    57 
    58 subsection {* Mapping distributes over append *}
    59 
    60 lemma map_append:
    61   assumes "l:Lists(A)"
    62     and "m:Lists(A)"
    63   shows "map(f,l@m) = map(f,l) @ map(f,m)"
    64   apply (tactic {* eq_coinduct3_tac @{context}
    65     "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *})
    66   apply (blast intro: prems)
    67   apply safe
    68   apply (drule ListsXH [THEN iffD1])
    69   apply (tactic "EQgen_tac @{context} [] 1")
    70   apply (drule ListsXH [THEN iffD1])
    71   apply (tactic "EQgen_tac @{context} [] 1")
    72   apply blast
    73   done
    74 
    75 
    76 subsection {* Append is associative *}
    77 
    78 lemma append_assoc:
    79   assumes "k:Lists(A)"
    80     and "l:Lists(A)"
    81     and "m:Lists(A)"
    82   shows "k @ l @ m = (k @ l) @ m"
    83   apply (tactic {* eq_coinduct3_tac @{context}
    84     "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*})
    85   apply (blast intro: prems)
    86   apply safe
    87   apply (drule ListsXH [THEN iffD1])
    88   apply (tactic "EQgen_tac @{context} [] 1")
    89    prefer 2
    90    apply blast
    91   apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1
    92     THEN EQgen_tac @{context} [] 1) *})
    93   done
    94 
    95 
    96 subsection {* Appending anything to an infinite list doesn't alter it *}
    97 
    98 lemma ilist_append:
    99   assumes "l:ILists(A)"
   100   shows "l @ m = l"
   101   apply (tactic {* eq_coinduct3_tac @{context}
   102     "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
   103   apply (blast intro: prems)
   104   apply safe
   105   apply (drule IListsXH [THEN iffD1])
   106   apply (tactic "EQgen_tac @{context} [] 1")
   107   apply blast
   108   done
   109 
   110 (*** The equivalance of two versions of an iteration function       ***)
   111 (*                                                                    *)
   112 (*        fun iter1(f,a) = a$iter1(f,f(a))                            *)
   113 (*        fun iter2(f,a) = a$map(f,iter2(f,a))                        *)
   114 
   115 lemma iter1B: "iter1(f,a) = a$iter1(f,f(a))"
   116   apply (unfold iter1_def)
   117   apply (rule letrecB [THEN trans])
   118   apply simp
   119   done
   120 
   121 lemma iter2B: "iter2(f,a) = a $ map(f,iter2(f,a))"
   122   apply (unfold iter2_def)
   123   apply (rule letrecB [THEN trans])
   124   apply (rule refl)
   125   done
   126 
   127 lemma iter2Blemma:
   128   "n:Nat ==>  
   129     map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"
   130   apply (rule_tac P = "%x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst])
   131   apply (simp add: nmapBcons)
   132   done
   133 
   134 lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)"
   135   apply (tactic {* eq_coinduct3_tac @{context}
   136     "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
   137   apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
   138   apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *})
   139   apply (subst napply_f, assumption)
   140   apply (rule_tac f1 = f in napplyBsucc [THEN subst])
   141   apply blast
   142   done
   143 
   144 end