src/HOL/HOLCF/ex/Concurrency_Monad.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 43524 d75e285fcf3e
child 62110 8d75ff14e3e9
permissions -rw-r--r--
Quotient_Info stores only relation maps
huffman@43524
     1
(*  Title:      HOL/HOLCF/ex/Concurrency_Monad.thy
huffman@43524
     2
    Author:     Brian Huffman
huffman@43524
     3
*)
huffman@43524
     4
huffman@43524
     5
theory Concurrency_Monad
huffman@43524
     6
imports HOLCF
huffman@43524
     7
begin
huffman@43524
     8
huffman@43524
     9
text {* This file contains the concurrency monad example from
huffman@43524
    10
  Chapter 7 of the author's PhD thesis. *}
huffman@43524
    11
huffman@43524
    12
subsection {* State/nondeterminism monad, as a type synonym *}
huffman@43524
    13
huffman@43524
    14
type_synonym ('s, 'a) N = "'s \<rightarrow> ('a u \<otimes> 's u)\<natural>"
huffman@43524
    15
huffman@43524
    16
definition mapN :: "('a \<rightarrow> 'b) \<rightarrow> ('s, 'a) N \<rightarrow> ('s, 'b) N"
huffman@43524
    17
  where "mapN = (\<Lambda> f. cfun_map\<cdot>ID\<cdot>(convex_map\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>ID)))"
huffman@43524
    18
huffman@43524
    19
definition unitN :: "'a \<rightarrow> ('s, 'a) N"
huffman@43524
    20
  where "unitN = (\<Lambda> x. (\<Lambda> s. convex_unit\<cdot>(:up\<cdot>x, up\<cdot>s:)))"
huffman@43524
    21
huffman@43524
    22
definition bindN :: "('s, 'a) N \<rightarrow> ('a \<rightarrow> ('s, 'b) N) \<rightarrow> ('s, 'b) N"
huffman@43524
    23
  where "bindN = (\<Lambda> c k. (\<Lambda> s. convex_bind\<cdot>(c\<cdot>s)\<cdot>(\<Lambda> (:up\<cdot>x, up\<cdot>s':). k\<cdot>x\<cdot>s')))"
huffman@43524
    24
huffman@43524
    25
definition plusN :: "('s, 'a) N \<rightarrow> ('s, 'a) N \<rightarrow> ('s, 'a) N"
huffman@43524
    26
  where "plusN = (\<Lambda> a b. (\<Lambda> s. convex_plus\<cdot>(a\<cdot>s)\<cdot>(b\<cdot>s)))"
huffman@43524
    27
huffman@43524
    28
lemma mapN_ID: "mapN\<cdot>ID = ID"
huffman@43524
    29
by (simp add: mapN_def domain_map_ID)
huffman@43524
    30
huffman@43524
    31
lemma mapN_mapN: "mapN\<cdot>f\<cdot>(mapN\<cdot>g\<cdot>m) = mapN\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>m"
huffman@43524
    32
unfolding mapN_def ID_def
huffman@43524
    33
by (simp add: cfun_map_map convex_map_map sprod_map_map u_map_map eta_cfun)
huffman@43524
    34
huffman@43524
    35
lemma mapN_unitN: "mapN\<cdot>f\<cdot>(unitN\<cdot>x) = unitN\<cdot>(f\<cdot>x)"
huffman@43524
    36
unfolding mapN_def unitN_def
huffman@43524
    37
by (simp add: cfun_map_def)
huffman@43524
    38
huffman@43524
    39
lemma bindN_unitN: "bindN\<cdot>(unitN\<cdot>a)\<cdot>f = f\<cdot>a"
huffman@43524
    40
by (simp add: unitN_def bindN_def eta_cfun)
huffman@43524
    41
huffman@43524
    42
lemma mapN_conv_bindN: "mapN\<cdot>f\<cdot>m = bindN\<cdot>m\<cdot>(unitN oo f)"
huffman@43524
    43
apply (simp add: mapN_def bindN_def unitN_def)
huffman@43524
    44
apply (rule cfun_eqI, simp)
huffman@43524
    45
apply (simp add: convex_map_def)
huffman@43524
    46
apply (rule cfun_arg_cong)
huffman@43524
    47
apply (rule cfun_eqI, simp, rename_tac p)
huffman@43524
    48
apply (case_tac p, simp)
huffman@43524
    49
apply (case_tac x, simp)
huffman@43524
    50
apply (case_tac y, simp)
huffman@43524
    51
apply simp
huffman@43524
    52
done
huffman@43524
    53
huffman@43524
    54
lemma bindN_unitN_right: "bindN\<cdot>m\<cdot>unitN = m"
huffman@43524
    55
proof -
huffman@43524
    56
  have "mapN\<cdot>ID\<cdot>m = m" by (simp add: mapN_ID)
huffman@43524
    57
  thus ?thesis by (simp add: mapN_conv_bindN)
huffman@43524
    58
qed
huffman@43524
    59
huffman@43524
    60
lemma bindN_bindN:
huffman@43524
    61
  "bindN\<cdot>(bindN\<cdot>m\<cdot>f)\<cdot>g = bindN\<cdot>m\<cdot>(\<Lambda> x. bindN\<cdot>(f\<cdot>x)\<cdot>g)"
huffman@43524
    62
apply (rule cfun_eqI, rename_tac s)
huffman@43524
    63
apply (simp add: bindN_def)
huffman@43524
    64
apply (simp add: convex_bind_bind)
huffman@43524
    65
apply (rule cfun_arg_cong)
huffman@43524
    66
apply (rule cfun_eqI, rename_tac w)
huffman@43524
    67
apply (case_tac w, simp)
huffman@43524
    68
apply (case_tac x, simp)
huffman@43524
    69
apply (case_tac y, simp)
huffman@43524
    70
apply simp
huffman@43524
    71
done
huffman@43524
    72
huffman@43524
    73
lemma mapN_bindN: "mapN\<cdot>f\<cdot>(bindN\<cdot>m\<cdot>g) = bindN\<cdot>m\<cdot>(\<Lambda> x. mapN\<cdot>f\<cdot>(g\<cdot>x))"
huffman@43524
    74
by (simp add: mapN_conv_bindN bindN_bindN)
huffman@43524
    75
huffman@43524
    76
lemma bindN_mapN: "bindN\<cdot>(mapN\<cdot>f\<cdot>m)\<cdot>g = bindN\<cdot>m\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))"
huffman@43524
    77
by (simp add: mapN_conv_bindN bindN_bindN bindN_unitN)
huffman@43524
    78
huffman@43524
    79
lemma mapN_plusN:
huffman@43524
    80
  "mapN\<cdot>f\<cdot>(plusN\<cdot>a\<cdot>b) = plusN\<cdot>(mapN\<cdot>f\<cdot>a)\<cdot>(mapN\<cdot>f\<cdot>b)"
huffman@43524
    81
unfolding mapN_def plusN_def by (simp add: cfun_map_def)
huffman@43524
    82
huffman@43524
    83
lemma plusN_commute: "plusN\<cdot>a\<cdot>b = plusN\<cdot>b\<cdot>a"
huffman@43524
    84
unfolding plusN_def by (simp add: convex_plus_commute)
huffman@43524
    85
huffman@43524
    86
lemma plusN_assoc: "plusN\<cdot>(plusN\<cdot>a\<cdot>b)\<cdot>c = plusN\<cdot>a\<cdot>(plusN\<cdot>b\<cdot>c)"
huffman@43524
    87
unfolding plusN_def by (simp add: convex_plus_assoc)
huffman@43524
    88
huffman@43524
    89
lemma plusN_absorb: "plusN\<cdot>a\<cdot>a = a"
huffman@43524
    90
unfolding plusN_def by (simp add: eta_cfun)
huffman@43524
    91
huffman@43524
    92
huffman@43524
    93
subsection {* Resumption-state-nondeterminism monad *}
huffman@43524
    94
huffman@43524
    95
domain ('s, 'a) R = Done (lazy "'a") | More (lazy "('s, ('s, 'a) R) N")
huffman@43524
    96
huffman@43524
    97
thm R.take_induct
huffman@43524
    98
huffman@43524
    99
lemma R_induct [case_names adm bottom Done More, induct type: R]:
huffman@43524
   100
  fixes P :: "('s, 'a) R \<Rightarrow> bool"
huffman@43524
   101
  assumes adm: "adm P"
huffman@43524
   102
  assumes bottom: "P \<bottom>"
huffman@43524
   103
  assumes Done: "\<And>x. P (Done\<cdot>x)"
huffman@43524
   104
  assumes More: "\<And>p c. (\<And>r::('s, 'a) R. P (p\<cdot>r)) \<Longrightarrow> P (More\<cdot>(mapN\<cdot>p\<cdot>c))"
huffman@43524
   105
  shows "P r"
huffman@43524
   106
proof (induct r rule: R.take_induct)
huffman@43524
   107
  show "adm P" by fact
huffman@43524
   108
next
huffman@43524
   109
  fix n
huffman@43524
   110
  show "P (R_take n\<cdot>r)"
huffman@43524
   111
  proof (induct n arbitrary: r)
huffman@43524
   112
    case 0 show ?case by (simp add: bottom)
huffman@43524
   113
  next
huffman@43524
   114
    case (Suc n r)
huffman@43524
   115
    show ?case
huffman@43524
   116
      apply (cases r)
huffman@43524
   117
      apply (simp add: bottom)
huffman@43524
   118
      apply (simp add: Done)
huffman@43524
   119
      using More [OF Suc]
huffman@43524
   120
      apply (simp add: mapN_def)
huffman@43524
   121
      done
huffman@43524
   122
  qed
huffman@43524
   123
qed
huffman@43524
   124
huffman@43524
   125
declare R.take_rews(2) [simp del]
huffman@43524
   126
huffman@43524
   127
lemma R_take_Suc_More [simp]:
huffman@43524
   128
  "R_take (Suc n)\<cdot>(More\<cdot>k) = More\<cdot>(mapN\<cdot>(R_take n)\<cdot>k)"
huffman@43524
   129
by (simp add: mapN_def R.take_rews(2))
huffman@43524
   130
huffman@43524
   131
huffman@43524
   132
subsection {* Map function *}
huffman@43524
   133
huffman@43524
   134
fixrec mapR :: "('a \<rightarrow> 'b) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R"
huffman@43524
   135
  where "mapR\<cdot>f\<cdot>(Done\<cdot>a) = Done\<cdot>(f\<cdot>a)"
huffman@43524
   136
  | "mapR\<cdot>f\<cdot>(More\<cdot>k) = More\<cdot>(mapN\<cdot>(mapR\<cdot>f)\<cdot>k)"
huffman@43524
   137
huffman@43524
   138
lemma mapR_strict [simp]: "mapR\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@43524
   139
by fixrec_simp
huffman@43524
   140
huffman@43524
   141
lemma mapR_mapR: "mapR\<cdot>f\<cdot>(mapR\<cdot>g\<cdot>r) = mapR\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>r"
huffman@43524
   142
by (induct r) (simp_all add: mapN_mapN)
huffman@43524
   143
huffman@43524
   144
lemma mapR_ID: "mapR\<cdot>ID\<cdot>r = r"
huffman@43524
   145
by (induct r) (simp_all add: mapN_mapN eta_cfun)
huffman@43524
   146
huffman@43524
   147
lemma "mapR\<cdot>f\<cdot>(mapR\<cdot>g\<cdot>r) = mapR\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>r"
huffman@43524
   148
apply (induct r)
huffman@43524
   149
apply simp
huffman@43524
   150
apply simp
huffman@43524
   151
apply simp
huffman@43524
   152
apply (simp (no_asm))
huffman@43524
   153
apply (simp (no_asm) add: mapN_mapN)
huffman@43524
   154
apply simp
huffman@43524
   155
done
huffman@43524
   156
huffman@43524
   157
huffman@43524
   158
subsection {* Monadic bind function *}
huffman@43524
   159
huffman@43524
   160
fixrec bindR :: "('s, 'a) R \<rightarrow> ('a \<rightarrow> ('s, 'b) R) \<rightarrow> ('s, 'b) R"
huffman@43524
   161
  where "bindR\<cdot>(Done\<cdot>x)\<cdot>k = k\<cdot>x"
huffman@43524
   162
  | "bindR\<cdot>(More\<cdot>c)\<cdot>k = More\<cdot>(mapN\<cdot>(\<Lambda> r. bindR\<cdot>r\<cdot>k)\<cdot>c)"
huffman@43524
   163
huffman@43524
   164
lemma bindR_strict [simp]: "bindR\<cdot>\<bottom>\<cdot>k = \<bottom>"
huffman@43524
   165
by fixrec_simp
huffman@43524
   166
huffman@43524
   167
lemma bindR_Done_right: "bindR\<cdot>r\<cdot>Done = r"
huffman@43524
   168
by (induct r) (simp_all add: mapN_mapN eta_cfun)
huffman@43524
   169
huffman@43524
   170
lemma mapR_conv_bindR: "mapR\<cdot>f\<cdot>r = bindR\<cdot>r\<cdot>(\<Lambda> x. Done\<cdot>(f\<cdot>x))"
huffman@43524
   171
by (induct r) (simp_all add: mapN_mapN)
huffman@43524
   172
huffman@43524
   173
lemma bindR_bindR: "bindR\<cdot>(bindR\<cdot>r\<cdot>f)\<cdot>g = bindR\<cdot>r\<cdot>(\<Lambda> x. bindR\<cdot>(f\<cdot>x)\<cdot>g)"
huffman@43524
   174
by (induct r) (simp_all add: mapN_mapN)
huffman@43524
   175
huffman@43524
   176
lemma "bindR\<cdot>(bindR\<cdot>r\<cdot>f)\<cdot>g = bindR\<cdot>r\<cdot>(\<Lambda> x. bindR\<cdot>(f\<cdot>x)\<cdot>g)"
huffman@43524
   177
apply (induct r)
huffman@43524
   178
apply (simp_all add: mapN_mapN)
huffman@43524
   179
done
huffman@43524
   180
huffman@43524
   181
subsection {* Zip function *}
huffman@43524
   182
huffman@43524
   183
fixrec zipR :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R \<rightarrow> ('s, 'c) R"
huffman@43524
   184
  where zipR_Done_Done:
huffman@43524
   185
    "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>(Done\<cdot>y) = Done\<cdot>(f\<cdot>x\<cdot>y)"
huffman@43524
   186
  | zipR_Done_More:
huffman@43524
   187
    "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>(More\<cdot>b) =
huffman@43524
   188
      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r)\<cdot>b)"
huffman@43524
   189
  | zipR_More_Done:
huffman@43524
   190
    "zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>(Done\<cdot>y) =
huffman@43524
   191
      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y))\<cdot>a)"
huffman@43524
   192
  | zipR_More_More:
huffman@43524
   193
    "zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>(More\<cdot>b) =
huffman@43524
   194
      More\<cdot>(plusN\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>r)\<cdot>b)
huffman@43524
   195
                 \<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(More\<cdot>b))\<cdot>a))"
huffman@43524
   196
huffman@43524
   197
lemma zipR_strict1 [simp]: "zipR\<cdot>f\<cdot>\<bottom>\<cdot>r = \<bottom>"
huffman@43524
   198
by fixrec_simp
huffman@43524
   199
huffman@43524
   200
lemma zipR_strict2 [simp]: "zipR\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
huffman@43524
   201
by (fixrec_simp, cases r, simp_all)
huffman@43524
   202
huffman@43524
   203
abbreviation apR (infixl "\<diamond>" 70)
huffman@43524
   204
  where "a \<diamond> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
huffman@43524
   205
huffman@43524
   206
text {* Proofs that @{text zipR} satisfies the applicative functor laws: *}
huffman@43524
   207
huffman@43524
   208
lemma R_homomorphism: "Done\<cdot>f \<diamond> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
huffman@43524
   209
  by simp
huffman@43524
   210
huffman@43524
   211
lemma R_identity: "Done\<cdot>ID \<diamond> r = r"
huffman@43524
   212
  by (induct r, simp_all add: mapN_mapN eta_cfun)
huffman@43524
   213
huffman@43524
   214
lemma R_interchange: "r \<diamond> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamond> r"
huffman@43524
   215
  by (induct r, simp_all add: mapN_mapN)
huffman@43524
   216
huffman@43524
   217
text {* The associativity rule is the hard one! *}
huffman@43524
   218
huffman@43524
   219
lemma R_associativity: "Done\<cdot>cfcomp \<diamond> r1 \<diamond> r2 \<diamond> r3 = r1 \<diamond> (r2 \<diamond> r3)"
huffman@43524
   220
proof (induct r1 arbitrary: r2 r3)
huffman@43524
   221
  case (Done x1) thus ?case
huffman@43524
   222
  proof (induct r2 arbitrary: r3)
huffman@43524
   223
    case (Done x2) thus ?case
huffman@43524
   224
    proof (induct r3)
huffman@43524
   225
      case (More p3 c3) thus ?case (* Done/Done/More *)
huffman@43524
   226
        by (simp add: mapN_mapN)
huffman@43524
   227
    qed simp_all
huffman@43524
   228
  next
huffman@43524
   229
    case (More p2 c2) thus ?case
huffman@43524
   230
    proof (induct r3)
huffman@43524
   231
      case (Done x3) thus ?case (* Done/More/Done *)
huffman@43524
   232
        by (simp add: mapN_mapN)
huffman@43524
   233
    next
huffman@43524
   234
      case (More p3 c3) thus ?case (* Done/More/More *)
huffman@43524
   235
        by (simp add: mapN_mapN mapN_plusN)
huffman@43524
   236
    qed simp_all
huffman@43524
   237
  qed simp_all
huffman@43524
   238
next
huffman@43524
   239
  case (More p1 c1) thus ?case
huffman@43524
   240
  proof (induct r2 arbitrary: r3)
huffman@43524
   241
    case (Done y) thus ?case
huffman@43524
   242
    proof (induct r3)
huffman@43524
   243
      case (Done x3) thus ?case
huffman@43524
   244
        by (simp add: mapN_mapN)
huffman@43524
   245
    next
huffman@43524
   246
      case (More p3 c3) thus ?case
huffman@43524
   247
        by (simp add: mapN_mapN)
huffman@43524
   248
    qed simp_all
huffman@43524
   249
  next
huffman@43524
   250
    case (More p2 c2) thus ?case
huffman@43524
   251
    proof (induct r3)
huffman@43524
   252
      case (Done x3) thus ?case
huffman@43524
   253
        by (simp add: mapN_mapN mapN_plusN)
huffman@43524
   254
    next
huffman@43524
   255
      case (More p3 c3) thus ?case
huffman@43524
   256
        by (simp add: mapN_mapN mapN_plusN plusN_assoc)
huffman@43524
   257
    qed simp_all
huffman@43524
   258
  qed simp_all
huffman@43524
   259
qed simp_all
huffman@43524
   260
huffman@43524
   261
text {* Other miscellaneous properties about @{text zipR}: *}
huffman@43524
   262
huffman@43524
   263
lemma zipR_Done_left:
huffman@43524
   264
  shows "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r = mapR\<cdot>(f\<cdot>x)\<cdot>r"
huffman@43524
   265
by (induct r) (simp_all add: mapN_mapN)
huffman@43524
   266
huffman@43524
   267
lemma zipR_Done_right:
huffman@43524
   268
  shows "zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y) = mapR\<cdot>(\<Lambda> x. f\<cdot>x\<cdot>y)\<cdot>r"
huffman@43524
   269
by (induct r) (simp_all add: mapN_mapN)
huffman@43524
   270
huffman@43524
   271
lemma mapR_zipR: "mapR\<cdot>h\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b) = zipR\<cdot>(\<Lambda> x y. h\<cdot>(f\<cdot>x\<cdot>y))\<cdot>a\<cdot>b"
huffman@43524
   272
apply (induct a arbitrary: b)
huffman@43524
   273
apply simp
huffman@43524
   274
apply simp
huffman@43524
   275
apply (simp add: zipR_Done_left zipR_Done_right mapR_mapR)
huffman@43524
   276
apply (induct_tac b)
huffman@43524
   277
apply simp
huffman@43524
   278
apply simp
huffman@43524
   279
apply (simp add: mapN_mapN)
huffman@43524
   280
apply (simp add: mapN_mapN mapN_plusN)
huffman@43524
   281
done
huffman@43524
   282
huffman@43524
   283
lemma zipR_mapR_left: "zipR\<cdot>f\<cdot>(mapR\<cdot>h\<cdot>a)\<cdot>b = zipR\<cdot>(\<Lambda> x y. f\<cdot>(h\<cdot>x)\<cdot>y)\<cdot>a\<cdot>b"
huffman@43524
   284
apply (induct a arbitrary: b)
huffman@43524
   285
apply simp
huffman@43524
   286
apply simp
huffman@43524
   287
apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
huffman@43524
   288
apply (simp add: mapN_mapN)
huffman@43524
   289
apply (induct_tac b)
huffman@43524
   290
apply simp
huffman@43524
   291
apply simp
huffman@43524
   292
apply (simp add: mapN_mapN)
huffman@43524
   293
apply (simp add: mapN_mapN)
huffman@43524
   294
done
huffman@43524
   295
huffman@43524
   296
lemma zipR_mapR_right: "zipR\<cdot>f\<cdot>a\<cdot>(mapR\<cdot>h\<cdot>b) = zipR\<cdot>(\<Lambda> x y. f\<cdot>x\<cdot>(h\<cdot>y))\<cdot>a\<cdot>b"
huffman@43524
   297
apply (induct b arbitrary: a)
huffman@43524
   298
apply simp
huffman@43524
   299
apply simp
huffman@43524
   300
apply (simp add: zipR_Done_left zipR_Done_right)
huffman@43524
   301
apply (simp add: mapN_mapN)
huffman@43524
   302
apply (induct_tac a)
huffman@43524
   303
apply simp
huffman@43524
   304
apply simp
huffman@43524
   305
apply (simp add: mapN_mapN)
huffman@43524
   306
apply (simp add: mapN_mapN)
huffman@43524
   307
done
huffman@43524
   308
huffman@43524
   309
lemma zipR_commute:
huffman@43524
   310
  assumes f: "\<And>x y. f\<cdot>x\<cdot>y = g\<cdot>y\<cdot>x"
huffman@43524
   311
  shows "zipR\<cdot>f\<cdot>a\<cdot>b = zipR\<cdot>g\<cdot>b\<cdot>a"
huffman@43524
   312
apply (induct a arbitrary: b)
huffman@43524
   313
apply simp
huffman@43524
   314
apply simp
huffman@43524
   315
apply (simp add: zipR_Done_left zipR_Done_right f [symmetric] eta_cfun)
huffman@43524
   316
apply (induct_tac b)
huffman@43524
   317
apply simp
huffman@43524
   318
apply simp
huffman@43524
   319
apply (simp add: mapN_mapN)
huffman@43524
   320
apply (simp add: mapN_mapN mapN_plusN plusN_commute)
huffman@43524
   321
done
huffman@43524
   322
huffman@43524
   323
lemma zipR_assoc:
huffman@43524
   324
  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
huffman@43524
   325
  fixes f :: "'a \<rightarrow> 'b \<rightarrow> 'd" and g :: "'d \<rightarrow> 'c \<rightarrow> 'e"
huffman@43524
   326
  assumes gf: "\<And>x y z. g\<cdot>(f\<cdot>x\<cdot>y)\<cdot>z = h\<cdot>x\<cdot>(k\<cdot>y\<cdot>z)"
huffman@43524
   327
  shows "zipR\<cdot>g\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b)\<cdot>c = zipR\<cdot>h\<cdot>a\<cdot>(zipR\<cdot>k\<cdot>b\<cdot>c)" (is "?P a b c")
huffman@43524
   328
 apply (induct a arbitrary: b c)
huffman@43524
   329
    apply simp
huffman@43524
   330
   apply simp
huffman@43524
   331
  apply (simp add: zipR_Done_left zipR_Done_right)
huffman@43524
   332
  apply (simp add: zipR_mapR_left mapR_zipR gf)
huffman@43524
   333
 apply (rename_tac pA kA b c)
huffman@43524
   334
 apply (rule_tac x=c in spec)
huffman@43524
   335
 apply (induct_tac b)
huffman@43524
   336
    apply simp
huffman@43524
   337
   apply simp
huffman@43524
   338
  apply (simp add: mapN_mapN)
huffman@43524
   339
  apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
huffman@43524
   340
  apply (simp add: zipR_mapR_right)
huffman@43524
   341
  apply (rule allI, rename_tac c)
huffman@43524
   342
  apply (induct_tac c)
huffman@43524
   343
     apply simp
huffman@43524
   344
    apply simp
huffman@43524
   345
   apply (rename_tac z)
huffman@43524
   346
   apply (simp add: mapN_mapN)
huffman@43524
   347
   apply (simp add: zipR_mapR_left gf)
huffman@43524
   348
  apply (rename_tac pC kC)
huffman@43524
   349
  apply (simp add: mapN_mapN)
huffman@43524
   350
  apply (simp add: zipR_mapR_left gf)
huffman@43524
   351
 apply (rename_tac pB kB)
huffman@43524
   352
 apply (rule allI, rename_tac c)
huffman@43524
   353
 apply (induct_tac c)
huffman@43524
   354
    apply simp
huffman@43524
   355
   apply simp
huffman@43524
   356
  apply (simp add: mapN_mapN mapN_plusN)
huffman@43524
   357
 apply (rename_tac pC kC)
huffman@43524
   358
 apply (simp add: mapN_mapN mapN_plusN plusN_assoc)
huffman@43524
   359
done
huffman@43524
   360
huffman@43524
   361
text {* Alternative proof using take lemma. *}
huffman@43524
   362
huffman@43524
   363
lemma
huffman@43524
   364
  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
huffman@43524
   365
  fixes f :: "'a \<rightarrow> 'b \<rightarrow> 'd" and g :: "'d \<rightarrow> 'c \<rightarrow> 'e"
huffman@43524
   366
  assumes gf: "\<And>x y z. g\<cdot>(f\<cdot>x\<cdot>y)\<cdot>z = h\<cdot>x\<cdot>(k\<cdot>y\<cdot>z)"
huffman@43524
   367
  shows "zipR\<cdot>g\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b)\<cdot>c = zipR\<cdot>h\<cdot>a\<cdot>(zipR\<cdot>k\<cdot>b\<cdot>c)"
huffman@43524
   368
    (is "?lhs = ?rhs" is "?P a b c")
huffman@43524
   369
proof (rule R.take_lemma)
huffman@43524
   370
  fix n show "R_take n\<cdot>?lhs = R_take n\<cdot>?rhs"
huffman@43524
   371
  proof (induct n arbitrary: a b c)
huffman@43524
   372
    case (0 a b c)
huffman@43524
   373
    show ?case by simp
huffman@43524
   374
  next
huffman@43524
   375
    case (Suc n a b c)
huffman@43524
   376
    note IH = this
huffman@43524
   377
    let ?P = ?case
huffman@43524
   378
    show ?case
huffman@43524
   379
    proof (cases a)
huffman@43524
   380
      case bottom thus ?P by simp
huffman@43524
   381
    next
huffman@43524
   382
      case (Done x) thus ?P
huffman@43524
   383
        by (simp add: zipR_Done_left zipR_mapR_left mapR_zipR gf)
huffman@43524
   384
    next
huffman@43524
   385
      case (More nA) thus ?P
huffman@43524
   386
      proof (cases b)
huffman@43524
   387
        case bottom thus ?P by simp
huffman@43524
   388
      next
huffman@43524
   389
        case (Done y) thus ?P
huffman@43524
   390
          by (simp add: zipR_Done_left zipR_Done_right
huffman@43524
   391
            zipR_mapR_left zipR_mapR_right gf)
huffman@43524
   392
      next
huffman@43524
   393
        case (More nB) thus ?P
huffman@43524
   394
        proof (cases c)
huffman@43524
   395
          case bottom thus ?P by simp
huffman@43524
   396
        next
huffman@43524
   397
          case (Done z) thus ?P
huffman@43524
   398
            by (simp add: zipR_Done_right mapR_zipR zipR_mapR_right gf)
huffman@43524
   399
        next
huffman@43524
   400
          case (More nC)
huffman@43524
   401
          note H = `a = More\<cdot>nA` `b = More\<cdot>nB` `c = More\<cdot>nC`
huffman@43524
   402
          show ?P
huffman@43524
   403
            apply (simp only: H zipR_More_More)
huffman@43524
   404
            apply (simplesubst zipR_More_More [of f, symmetric])
huffman@43524
   405
            apply (simplesubst zipR_More_More [of k, symmetric])
huffman@43524
   406
            apply (simp only: H [symmetric])
huffman@43524
   407
            apply (simp add: mapN_mapN mapN_plusN plusN_assoc IH)
huffman@43524
   408
            done
huffman@43524
   409
        qed
huffman@43524
   410
      qed
huffman@43524
   411
    qed
huffman@43524
   412
  qed
huffman@43524
   413
qed
huffman@43524
   414
huffman@43524
   415
end