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