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
```