src/HOL/HOLCF/ex/Domain_Proofs.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44066 d74182c93f04
child 49759 ecf1d5d87e5e
permissions -rw-r--r--
Quotient_Info stores only relation maps
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/ex/Domain_Proofs.thy
huffman@33591
     2
    Author:     Brian Huffman
huffman@33591
     3
*)
huffman@33591
     4
huffman@33591
     5
header {* Internal domain package proofs done manually *}
huffman@33591
     6
huffman@33591
     7
theory Domain_Proofs
huffman@33591
     8
imports HOLCF
huffman@33591
     9
begin
huffman@33591
    10
huffman@33591
    11
(*
huffman@33591
    12
huffman@33591
    13
The definitions and proofs below are for the following recursive
huffman@33591
    14
datatypes:
huffman@33591
    15
huffman@33591
    16
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
huffman@33787
    17
   and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
huffman@33787
    18
   and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
huffman@33591
    19
huffman@33591
    20
*)
huffman@33591
    21
huffman@33591
    22
(********************************************************************)
huffman@33591
    23
huffman@33591
    24
subsection {* Step 1: Define the new type combinators *}
huffman@33591
    25
huffman@33591
    26
text {* Start with the one-step non-recursive version *}
huffman@33591
    27
huffman@33591
    28
definition
huffman@39989
    29
  foo_bar_baz_deflF ::
huffman@41287
    30
    "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
huffman@33591
    31
where
huffman@40327
    32
  "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
huffman@41437
    33
    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
huffman@41437
    34
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
huffman@41437
    35
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
huffman@33591
    36
huffman@39989
    37
lemma foo_bar_baz_deflF_beta:
huffman@39989
    38
  "foo_bar_baz_deflF\<cdot>a\<cdot>t =
huffman@41437
    39
    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t))))
huffman@41437
    40
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
huffman@41437
    41
    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
huffman@39989
    42
unfolding foo_bar_baz_deflF_def
huffman@33781
    43
by (simp add: split_def)
huffman@33591
    44
huffman@33591
    45
text {* Individual type combinators are projected from the fixed point. *}
huffman@33591
    46
huffman@41287
    47
definition foo_defl :: "udom defl \<rightarrow> udom defl"
huffman@39989
    48
where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
huffman@33591
    49
huffman@41287
    50
definition bar_defl :: "udom defl \<rightarrow> udom defl"
huffman@39989
    51
where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
huffman@33591
    52
huffman@41287
    53
definition baz_defl :: "udom defl \<rightarrow> udom defl"
huffman@39989
    54
where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
huffman@33591
    55
huffman@36132
    56
lemma defl_apply_thms:
huffman@39989
    57
  "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"
huffman@39989
    58
  "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
huffman@39989
    59
  "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
huffman@39989
    60
unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
huffman@36132
    61
huffman@33591
    62
text {* Unfold rules for each combinator. *}
huffman@33591
    63
huffman@39989
    64
lemma foo_defl_unfold:
huffman@41437
    65
  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
huffman@39989
    66
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
huffman@33591
    67
huffman@41437
    68
lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
huffman@39989
    69
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
huffman@33591
    70
huffman@41437
    71
lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
huffman@39989
    72
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
huffman@33591
    73
huffman@33591
    74
text "The automation for the previous steps will be quite similar to
huffman@33591
    75
how the fixrec package works."
huffman@33591
    76
huffman@33591
    77
(********************************************************************)
huffman@33591
    78
huffman@33591
    79
subsection {* Step 2: Define types, prove class instances *}
huffman@33591
    80
huffman@33591
    81
text {* Use @{text pcpodef} with the appropriate type combinator. *}
huffman@33591
    82
huffman@41292
    83
pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
huffman@40038
    84
by (rule defl_set_bottom, rule adm_defl_set)
huffman@33591
    85
huffman@41292
    86
pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
huffman@40038
    87
by (rule defl_set_bottom, rule adm_defl_set)
huffman@33591
    88
huffman@41292
    89
pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
huffman@40038
    90
by (rule defl_set_bottom, rule adm_defl_set)
huffman@33591
    91
huffman@33591
    92
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
huffman@33591
    93
huffman@41292
    94
instantiation foo :: ("domain") "domain"
huffman@33591
    95
begin
huffman@33591
    96
huffman@33591
    97
definition emb_foo :: "'a foo \<rightarrow> udom"
huffman@33679
    98
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
huffman@33591
    99
huffman@33591
   100
definition prj_foo :: "udom \<rightarrow> 'a foo"
huffman@41292
   101
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"
huffman@33591
   102
huffman@41287
   103
definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"
huffman@41292
   104
where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"
huffman@40491
   105
huffman@40491
   106
definition
huffman@41292
   107
  "(liftemb :: 'a foo u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
huffman@40491
   108
huffman@40491
   109
definition
huffman@41292
   110
  "(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj"
huffman@40491
   111
huffman@40491
   112
definition
huffman@41436
   113
  "liftdefl \<equiv> \<lambda>(t::'a foo itself). liftdefl_of\<cdot>DEFL('a foo)"
huffman@33591
   114
huffman@33591
   115
instance
huffman@41292
   116
apply (rule typedef_domain_class)
huffman@33591
   117
apply (rule type_definition_foo)
huffman@33591
   118
apply (rule below_foo_def)
huffman@33591
   119
apply (rule emb_foo_def)
huffman@33591
   120
apply (rule prj_foo_def)
huffman@39989
   121
apply (rule defl_foo_def)
huffman@40491
   122
apply (rule liftemb_foo_def)
huffman@40491
   123
apply (rule liftprj_foo_def)
huffman@40491
   124
apply (rule liftdefl_foo_def)
huffman@33591
   125
done
huffman@33591
   126
huffman@33591
   127
end
huffman@33591
   128
huffman@41292
   129
instantiation bar :: ("domain") "domain"
huffman@33591
   130
begin
huffman@33591
   131
huffman@33591
   132
definition emb_bar :: "'a bar \<rightarrow> udom"
huffman@33679
   133
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
huffman@33591
   134
huffman@33591
   135
definition prj_bar :: "udom \<rightarrow> 'a bar"
huffman@41292
   136
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"
huffman@33591
   137
huffman@41287
   138
definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"
huffman@41292
   139
where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"
huffman@40491
   140
huffman@40491
   141
definition
huffman@41292
   142
  "(liftemb :: 'a bar u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
huffman@40491
   143
huffman@40491
   144
definition
huffman@41292
   145
  "(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj"
huffman@40491
   146
huffman@40491
   147
definition
huffman@41436
   148
  "liftdefl \<equiv> \<lambda>(t::'a bar itself). liftdefl_of\<cdot>DEFL('a bar)"
huffman@33591
   149
huffman@33591
   150
instance
huffman@41292
   151
apply (rule typedef_domain_class)
huffman@33591
   152
apply (rule type_definition_bar)
huffman@33591
   153
apply (rule below_bar_def)
huffman@33591
   154
apply (rule emb_bar_def)
huffman@33591
   155
apply (rule prj_bar_def)
huffman@39989
   156
apply (rule defl_bar_def)
huffman@40491
   157
apply (rule liftemb_bar_def)
huffman@40491
   158
apply (rule liftprj_bar_def)
huffman@40491
   159
apply (rule liftdefl_bar_def)
huffman@33591
   160
done
huffman@33591
   161
huffman@33591
   162
end
huffman@33591
   163
huffman@41292
   164
instantiation baz :: ("domain") "domain"
huffman@33591
   165
begin
huffman@33591
   166
huffman@33591
   167
definition emb_baz :: "'a baz \<rightarrow> udom"
huffman@33679
   168
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
huffman@33591
   169
huffman@33591
   170
definition prj_baz :: "udom \<rightarrow> 'a baz"
huffman@41292
   171
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"
huffman@33591
   172
huffman@41287
   173
definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"
huffman@41292
   174
where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"
huffman@40491
   175
huffman@40491
   176
definition
huffman@41292
   177
  "(liftemb :: 'a baz u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"
huffman@40491
   178
huffman@40491
   179
definition
huffman@41292
   180
  "(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj"
huffman@40491
   181
huffman@40491
   182
definition
huffman@41436
   183
  "liftdefl \<equiv> \<lambda>(t::'a baz itself). liftdefl_of\<cdot>DEFL('a baz)"
huffman@33591
   184
huffman@33591
   185
instance
huffman@41292
   186
apply (rule typedef_domain_class)
huffman@33591
   187
apply (rule type_definition_baz)
huffman@33591
   188
apply (rule below_baz_def)
huffman@33591
   189
apply (rule emb_baz_def)
huffman@33591
   190
apply (rule prj_baz_def)
huffman@39989
   191
apply (rule defl_baz_def)
huffman@40491
   192
apply (rule liftemb_baz_def)
huffman@40491
   193
apply (rule liftprj_baz_def)
huffman@40491
   194
apply (rule liftdefl_baz_def)
huffman@33591
   195
done
huffman@33591
   196
huffman@33591
   197
end
huffman@33591
   198
huffman@39989
   199
text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
huffman@33591
   200
huffman@41292
   201
lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
huffman@39989
   202
apply (rule typedef_DEFL)
huffman@39989
   203
apply (rule defl_foo_def)
huffman@33591
   204
done
huffman@33591
   205
huffman@41292
   206
lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"
huffman@39989
   207
apply (rule typedef_DEFL)
huffman@39989
   208
apply (rule defl_bar_def)
huffman@39974
   209
done
huffman@39974
   210
huffman@41292
   211
lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"
huffman@39989
   212
apply (rule typedef_DEFL)
huffman@39989
   213
apply (rule defl_baz_def)
huffman@33591
   214
done
huffman@33591
   215
huffman@39989
   216
text {* Prove DEFL equations using type combinator unfold lemmas. *}
huffman@33591
   217
huffman@39989
   218
lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
huffman@40491
   219
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
huffman@39989
   220
by (rule foo_defl_unfold)
huffman@33591
   221
huffman@39989
   222
lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
huffman@40491
   223
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
huffman@39989
   224
by (rule bar_defl_unfold)
huffman@33591
   225
huffman@39989
   226
lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
huffman@40491
   227
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
huffman@39989
   228
by (rule baz_defl_unfold)
huffman@33591
   229
huffman@33591
   230
(********************************************************************)
huffman@33591
   231
huffman@33591
   232
subsection {* Step 3: Define rep and abs functions *}
huffman@33591
   233
huffman@40037
   234
text {* Define them all using @{text prj} and @{text emb}! *}
huffman@33591
   235
huffman@33591
   236
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
huffman@40037
   237
where "foo_rep \<equiv> prj oo emb"
huffman@33591
   238
huffman@33591
   239
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
huffman@40037
   240
where "foo_abs \<equiv> prj oo emb"
huffman@33591
   241
huffman@33787
   242
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
huffman@40037
   243
where "bar_rep \<equiv> prj oo emb"
huffman@33591
   244
huffman@33787
   245
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
huffman@40037
   246
where "bar_abs \<equiv> prj oo emb"
huffman@33591
   247
huffman@33787
   248
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
huffman@40037
   249
where "baz_rep \<equiv> prj oo emb"
huffman@33591
   250
huffman@33787
   251
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
huffman@40037
   252
where "baz_abs \<equiv> prj oo emb"
huffman@33779
   253
huffman@33779
   254
text {* Prove isomorphism rules. *}
huffman@33779
   255
huffman@33779
   256
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
huffman@39989
   257
by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
huffman@33779
   258
huffman@33779
   259
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
huffman@39989
   260
by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
huffman@33779
   261
huffman@33779
   262
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
huffman@39989
   263
by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
huffman@33779
   264
huffman@33779
   265
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
huffman@39989
   266
by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
huffman@33779
   267
huffman@33779
   268
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
huffman@39989
   269
by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
huffman@33779
   270
huffman@33779
   271
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
huffman@39989
   272
by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
huffman@33591
   273
huffman@33591
   274
text {* Prove isodefl rules using @{text isodefl_coerce}. *}
huffman@33591
   275
huffman@33591
   276
lemma isodefl_foo_abs:
huffman@33591
   277
  "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
huffman@39989
   278
by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
huffman@33591
   279
huffman@33591
   280
lemma isodefl_bar_abs:
huffman@33591
   281
  "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
huffman@39989
   282
by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
huffman@33591
   283
huffman@33591
   284
lemma isodefl_baz_abs:
huffman@33591
   285
  "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
huffman@39989
   286
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
huffman@33591
   287
huffman@33591
   288
(********************************************************************)
huffman@33591
   289
huffman@33591
   290
subsection {* Step 4: Define map functions, prove isodefl property *}
huffman@33591
   291
huffman@33591
   292
text {* Start with the one-step non-recursive version. *}
huffman@33591
   293
huffman@33591
   294
text {* Note that the type of the map function depends on which
huffman@33591
   295
variables are used in positive and negative positions. *}
huffman@33591
   296
huffman@33591
   297
definition
huffman@33591
   298
  foo_bar_baz_mapF ::
huffman@33787
   299
    "('a \<rightarrow> 'b) \<rightarrow>
huffman@33787
   300
     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
huffman@33787
   301
     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
huffman@33591
   302
where
huffman@40327
   303
  "foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3).
huffman@33591
   304
    (
huffman@33591
   305
      foo_abs oo
huffman@33591
   306
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
huffman@33591
   307
          oo foo_rep
huffman@33591
   308
    ,
huffman@33787
   309
      bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
huffman@33591
   310
    ,
huffman@33787
   311
      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
huffman@33781
   312
    )))"
huffman@33591
   313
huffman@33591
   314
lemma foo_bar_baz_mapF_beta:
huffman@33591
   315
  "foo_bar_baz_mapF\<cdot>f\<cdot>d =
huffman@33591
   316
    (
huffman@33591
   317
      foo_abs oo
huffman@33591
   318
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
huffman@33591
   319
          oo foo_rep
huffman@33591
   320
    ,
huffman@33787
   321
      bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
huffman@33591
   322
    ,
huffman@33787
   323
      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
huffman@33591
   324
    )"
huffman@33591
   325
unfolding foo_bar_baz_mapF_def
huffman@33781
   326
by (simp add: split_def)
huffman@33591
   327
huffman@33591
   328
text {* Individual map functions are projected from the fixed point. *}
huffman@33591
   329
huffman@33591
   330
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
huffman@33591
   331
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
huffman@33591
   332
huffman@33591
   333
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
huffman@33591
   334
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
huffman@33591
   335
huffman@33787
   336
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
huffman@33591
   337
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
huffman@33591
   338
huffman@36132
   339
lemma map_apply_thms:
huffman@36132
   340
  "foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))"
huffman@36132
   341
  "bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
huffman@36132
   342
  "baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
huffman@36132
   343
unfolding foo_map_def bar_map_def baz_map_def by simp_all
huffman@36132
   344
huffman@33591
   345
text {* Prove isodefl rules for all map functions simultaneously. *}
huffman@33591
   346
huffman@33591
   347
lemma isodefl_foo_bar_baz:
huffman@41292
   348
  assumes isodefl_d: "isodefl d t"
huffman@33591
   349
  shows
huffman@39989
   350
  "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
huffman@39989
   351
  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
huffman@39989
   352
  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
huffman@36132
   353
unfolding map_apply_thms defl_apply_thms
huffman@33787
   354
 apply (rule parallel_fix_ind)
huffman@33591
   355
   apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
huffman@33591
   356
  apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
huffman@33591
   357
 apply (simp only: foo_bar_baz_mapF_beta
huffman@39989
   358
                   foo_bar_baz_deflF_beta
huffman@33591
   359
                   fst_conv snd_conv)
huffman@33591
   360
 apply (elim conjE)
huffman@33591
   361
 apply (intro
huffman@33591
   362
  conjI
huffman@33591
   363
  isodefl_foo_abs
huffman@33591
   364
  isodefl_bar_abs
huffman@33591
   365
  isodefl_baz_abs
huffman@40491
   366
  domain_isodefl
huffman@40491
   367
  isodefl_ID_DEFL isodefl_LIFTDEFL
huffman@33591
   368
  isodefl_d
huffman@33591
   369
 )
huffman@33591
   370
 apply assumption+
huffman@33591
   371
done
huffman@33591
   372
huffman@33591
   373
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
huffman@33591
   374
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
huffman@33591
   375
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
huffman@33591
   376
huffman@39989
   377
text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
huffman@33591
   378
huffman@33591
   379
lemma foo_map_ID: "foo_map\<cdot>ID = ID"
huffman@39989
   380
apply (rule isodefl_DEFL_imp_ID)
huffman@39989
   381
apply (subst DEFL_foo)
huffman@33591
   382
apply (rule isodefl_foo)
huffman@41292
   383
apply (rule isodefl_ID_DEFL)
huffman@33591
   384
done
huffman@33591
   385
huffman@33591
   386
lemma bar_map_ID: "bar_map\<cdot>ID = ID"
huffman@39989
   387
apply (rule isodefl_DEFL_imp_ID)
huffman@39989
   388
apply (subst DEFL_bar)
huffman@33591
   389
apply (rule isodefl_bar)
huffman@41292
   390
apply (rule isodefl_ID_DEFL)
huffman@33591
   391
done
huffman@33591
   392
huffman@33591
   393
lemma baz_map_ID: "baz_map\<cdot>ID = ID"
huffman@39989
   394
apply (rule isodefl_DEFL_imp_ID)
huffman@39989
   395
apply (subst DEFL_baz)
huffman@33591
   396
apply (rule isodefl_baz)
huffman@41292
   397
apply (rule isodefl_ID_DEFL)
huffman@33591
   398
done
huffman@33591
   399
huffman@33591
   400
(********************************************************************)
huffman@33591
   401
huffman@36132
   402
subsection {* Step 5: Define take functions, prove lub-take lemmas *}
huffman@33781
   403
huffman@33781
   404
definition
huffman@36132
   405
  foo_bar_baz_takeF ::
huffman@33781
   406
    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
huffman@33781
   407
     ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
huffman@33781
   408
where
huffman@36132
   409
  "foo_bar_baz_takeF = (\<Lambda> p.
huffman@36132
   410
    ( foo_abs oo
huffman@36132
   411
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
huffman@36132
   412
          oo foo_rep
huffman@36132
   413
    , bar_abs oo
huffman@36132
   414
        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
huffman@36132
   415
    , baz_abs oo
huffman@36132
   416
        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
huffman@36132
   417
    ))"
huffman@36132
   418
huffman@36132
   419
lemma foo_bar_baz_takeF_beta:
huffman@36132
   420
  "foo_bar_baz_takeF\<cdot>p =
huffman@36132
   421
    ( foo_abs oo
huffman@36132
   422
        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
huffman@36132
   423
          oo foo_rep
huffman@36132
   424
    , bar_abs oo
huffman@36132
   425
        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
huffman@36132
   426
    , baz_abs oo
huffman@36132
   427
        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
huffman@36132
   428
    )"
huffman@36132
   429
unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp)
huffman@36132
   430
huffman@36132
   431
definition
huffman@36132
   432
  foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
huffman@36132
   433
where
huffman@36132
   434
  "foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))"
huffman@36132
   435
huffman@36132
   436
definition
huffman@36132
   437
  bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
huffman@36132
   438
where
huffman@36132
   439
  "bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
huffman@33591
   440
huffman@36132
   441
definition
huffman@36132
   442
  baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
huffman@36132
   443
where
huffman@36132
   444
  "baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
huffman@36132
   445
huffman@36132
   446
lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take"
huffman@36132
   447
unfolding foo_take_def bar_take_def baz_take_def
huffman@36132
   448
by (intro ch2ch_fst ch2ch_snd chain_iterate)+
huffman@36132
   449
huffman@36132
   450
lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>"
huffman@36132
   451
unfolding foo_take_def bar_take_def baz_take_def
huffman@36132
   452
by (simp only: iterate_0 fst_strict snd_strict)+
huffman@36132
   453
huffman@36132
   454
lemma take_Suc_thms:
huffman@36132
   455
  "foo_take (Suc n) =
huffman@36132
   456
    foo_abs oo ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(bar_take n))) oo foo_rep"
huffman@36132
   457
  "bar_take (Suc n) =
huffman@36132
   458
    bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep"
huffman@36132
   459
  "baz_take (Suc n) =
huffman@36132
   460
    baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep"
huffman@36132
   461
unfolding foo_take_def bar_take_def baz_take_def
huffman@36132
   462
by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+
huffman@36132
   463
huffman@36132
   464
lemma lub_take_lemma:
huffman@36132
   465
  "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
huffman@36132
   466
    = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
huffman@40771
   467
apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
huffman@36132
   468
apply (simp only: map_apply_thms pair_collapse)
huffman@36132
   469
apply (simp only: fix_def2)
huffman@36132
   470
apply (rule lub_eq)
huffman@36132
   471
apply (rule nat.induct)
huffman@36132
   472
apply (simp only: iterate_0 Pair_strict take_0_thms)
huffman@44066
   473
apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
huffman@36132
   474
                  foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
huffman@33781
   475
done
huffman@33591
   476
huffman@36132
   477
lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
huffman@36132
   478
apply (rule trans [OF _ foo_map_ID])
huffman@36132
   479
using lub_take_lemma
huffman@36132
   480
apply (elim Pair_inject)
huffman@36132
   481
apply assumption
huffman@36132
   482
done
huffman@33591
   483
huffman@36132
   484
lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID"
huffman@36132
   485
apply (rule trans [OF _ bar_map_ID])
huffman@36132
   486
using lub_take_lemma
huffman@36132
   487
apply (elim Pair_inject)
huffman@36132
   488
apply assumption
huffman@36132
   489
done
huffman@33591
   490
huffman@36132
   491
lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID"
huffman@36132
   492
apply (rule trans [OF _ baz_map_ID])
huffman@36132
   493
using lub_take_lemma
huffman@36132
   494
apply (elim Pair_inject)
huffman@36132
   495
apply assumption
huffman@36132
   496
done
huffman@33591
   497
huffman@33591
   498
end