text‹ \sloppypar
In this section, we generalize to bicategories the proof of the Coherence Theorem
that we previously gave for monoidal categories
(see ‹MonoidalCategory.evaluation_map.coherence› in @{session MonoidalCategory}).
As was the case for the previous proof, the current proof takes a syntactic approach.
First we define a formal ``bicategorical language'' of terms constructed using
syntactic operators that correspond to the various operations (vertical and horizontal
composition, associators and unitors) found in a bicategory.
Terms of the language are classified as formal ``arrows'', ``identities'', or ``objects''
according to the syntactic operators used in their formation.
A class of terms called ``canonical'' is also defined in this way.
Functions that map ``arrows'' to their ``domain'' and ``codomain'', and to their
``source'' and ``target'' are defined by recursion on the structure of terms.
Next, we define a notion of ``normal form'' for terms in this language and we
give a recursive definition of a function that maps terms to their normal forms.
Normalization moves vertical composition inside of horizontal composition and
``flattens'' horizontal composition by associating all horizontal compositions to the right.
In addition, normalization deletes from a term any horizontal composites involving an arrow
and its source or target, replacing such composites by just the arrow itself.
We then define a ``reduction function'' that maps each identity term ‹t› to a
``canonical'' term ‹t\↓› that connects ‹t› with its normal form. The definition of reduction
is also recursive, but it is somewhat more complex than normalization in that it
involves two mutually recursive functions: one that applies to any identity term
and another that applies only to terms that are the horizontal composite
of two identity terms.
The next step is to define an ``evaluation function'' that evaluates terms in a given
bicategory (which is left as an unspecified parameter). We show that evaluation respects
bicategorical structure:
the domain, codomain, source, and target mappings on terms correspond under evaluation
to the actual domain, codomain, source and target mappings on the given bicategory,
the vertical and horizontal composition on terms correspond to the actual vertical
and horizontal composition of the bicategory, and unit and associativity terms evaluate
to the actual unit and associativity isomorphisms of the bicategory.
In addition, ``object terms'' evaluate to objects (\emph{i.e.}~0-cells),
``identity terms'' evaluate to identities (\emph{i.e.}~1-cells),
``arrow terms'' evaluate to arrows (\emph{i.e.}~2-cells), and ``canonical terms'' evaluate
to canonical isomorphisms.
A term is defined to be ``coherent'' if, roughly speaking, it is a formal arrow
whose evaluation commutes with the evaluations of the reductions to normal form of
its domain and codomain.
We then prove the Coherence Theorem, expressed in the form: ``every arrow is coherent.''
This implies a more classical version of the Coherence Theorem, which says that:
``syntactically parallel arrows with the same normal form have equal evaluations''. ›
subsection"Bicategorical Language"
text‹
For the most part, the definition of the ``bicategorical language'' of terms is
a straightforward generalization of the ``monoidal language'' that we used for
monoidal categories.
Some modifications are required, however, due to the fact that horizontal composition
in a bicategory is a partial operation, whereas the the tensor product in a monoidal
category is well-defined for all pairs of arrows.
One difference is that we have found it necessary to introduce a new class of primitive
terms whose elements represent ``formal objects'', so that there is some way to
identify the source and target of what would otherwise be an empty horizontal composite.
This was not an issue for monoidal categories, because the totality of horizontal
composition meant that there was no need for syntactically defined sources and targets.
Another difference is what we have chosen for the ``generators'' of the language
and how they are used to form primitive terms. For monoidal categories,
we supposed that we were given a category ‹C› and the syntax contained a constructor
to form a primitive term corresponding to each arrow of ‹C›.
We assumed a category as the given data, rather than something less structured,
such as a graph, because we were primarily interested in the tensor product and
the associators and unitors, and were relatively uninterested in the strictly
associative and unital composition of the underlying category.
For bicategories, we also take the vertical composition as given for the same
reasons; however, this is not yet sufficient due to the fact that horizontal
composition in a bicategory is a partial operation, in contrast to the tensor
product in a monoidal category, which is defined for all pairs of arrows.
To deal with this issue, for bicategories we assume that source and target
mappings are also given, so that the given data forms a category with
``horizontal homs''. The given source and target mappings are extended to all terms
and used to define when two terms are ``formally horizontally composable''. ›
locale bicategorical_language =
category V +
horizontal_homs V src trg for V :: "'a comp" (infixr‹⋅›55) and src :: "'a ==> 'a" and trg :: "'a ==> 'a" begin
text‹
Constructor ‹Prim0› is used to construct ``formal objects'' and ‹Prim› is used to
construct primitive terms that are not formal objects. ›
primrec Trg :: "'a term ==> 'a term" where"Trg \<langle>μ\<rangle>0 = \<langle>μ\<rangle>0"
| "Trg \<langle>μ\<rangle> = \<langle>trg μ\<rangle>0"
| "Trg (t \<star> u) = Trg t"
| "Trg (t \<cdot> u) = Trg t"
| "Trg \<l>[t] = Trg t"
| "Trg \<l>-1[t] = Trg t"
| "Trg \<r>[t] = Trg t"
| "Trg \<r>-1[t] = Trg t"
| "Trg \<a>[t, u, v] = Trg t"
| "Trg \<a>-1[t, u, v] = Trg t"
primrec Dom :: "'a term ==> 'a term" where"Dom \<langle>μ\<rangle>0 = \<langle>μ\<rangle>0"
| "Dom \<langle>μ\<rangle> = \<langle>dom μ\<rangle>"
| "Dom (t \<star> u) = Dom t \<star> Dom u"
| "Dom (t \<cdot> u) = Dom u"
| "Dom \<l>[t] = Trg t \<star> Dom t"
| "Dom \<l>-1[t] = Dom t"
| "Dom \<r>[t] = Dom t \<star> Src t"
| "Dom \<r>-1[t] = Dom t"
| "Dom \<a>[t, u, v] = (Dom t \<star> Dom u) \<star> Dom v"
| "Dom \<a>-1[t, u, v] = Dom t \<star> (Dom u \<star> Dom v)"
primrec Cod :: "'a term ==> 'a term" where"Cod \<langle>μ\<rangle>0 = \<langle>μ\<rangle>0"
| "Cod \<langle>μ\<rangle> = \<langle>cod μ\<rangle>"
| "Cod (t \<star> u) = Cod t \<star> Cod u"
| "Cod (t \<cdot> u) = Cod t"
| "Cod \<l>[t] = Cod t"
| "Cod \<l>-1[t] = Trg t \<star> Cod t"
| "Cod \<r>[t] = Cod t"
| "Cod \<r>-1[t] = Cod t \<star> Src t"
| "Cod \<a>[t, u, v] = Cod t \<star> (Cod u \<star> Cod v)"
| "Cod \<a>-1[t, u, v] = (Cod t \<star> Cod u) \<star> Cod v"
text‹
A term is a ``formal arrow'' if it is constructed from primitive arrows in such a way
that horizontal and vertical composition are applied only to formally composable pairs
of terms. The definitions of ``formal identity'' and ``formal object'' follow a
similar pattern. ›
primrec Arr :: "'a term ==> bool" where"Arr \<langle>μ\<rangle>0 = obj μ"
| "Arr \<langle>μ\<rangle> = arr μ"
| "Arr (t \<star> u) = (Arr t ∧ Arr u ∧ Src t = Trg u)"
| "Arr (t \<cdot> u) = (Arr t ∧ Arr u ∧ Dom t = Cod u)"
| "Arr \<l>[t] = Arr t"
| "Arr \<l>-1[t] = Arr t"
| "Arr \<r>[t] = Arr t"
| "Arr \<r>-1[t] = Arr t"
| "Arr \<a>[t, u, v] = (Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v)"
| "Arr \<a>-1[t, u, v] = (Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v)"
primrec Ide :: "'a term ==> bool" where"Ide \<langle>μ\<rangle>0 = obj μ"
| "Ide \<langle>μ\<rangle> = ide μ"
| "Ide (t \<star> u) = (Ide t ∧ Ide u ∧ Src t = Trg u)"
| "Ide (t \<cdot> u) = False"
| "Ide \<l>[t] = False"
| "Ide \<l>-1[t] = False"
| "Ide \<r>[t] = False"
| "Ide \<r>-1[t] = False"
| "Ide \<a>[t, u, v] = False"
| "Ide \<a>-1[t, u, v] = False"
lemma Ide_in_Hom: assumes"Ide t" shows"t ∈ HHom (Src t) (Trg t)"and"t ∈ VHom t t" proof - have1: "Ide t ==> t ∈ HHom (Src t) (Trg t) ∧ t ∈ VHom t t" by (induct t, auto) show"t ∈ HHom (Src t) (Trg t)"using assms 1by simp show"t ∈ VHom t t"using assms 1by simp qed
lemma Obj_in_Hom: assumes"Obj t" shows"t ∈ HHom t t"and"t ∈ VHom t t" proof - have1: "Obj t ==> t ∈ HHom t t ∧ t ∈ VHom t t" by (induct t, auto) show"t ∈ HHom t t"using assms 1by simp show"t ∈ VHom t t"using assms 1by simp qed
text‹
A formal arrow is ``canonical'' if the only primitive arrows used in its construction
are objects and identities. ›
primrec Can :: "'a term ==> bool" where"Can \<langle>μ\<rangle>0 = obj μ"
| "Can \<langle>μ\<rangle> = ide μ"
| "Can (t \<star> u) = (Can t ∧ Can u ∧ Src t = Trg u)"
| "Can (t \<cdot> u) = (Can t ∧ Can u ∧ Dom t = Cod u)"
| "Can \<l>[t] = Can t"
| "Can \<l>-1[t] = Can t"
| "Can \<r>[t] = Can t"
| "Can \<r>-1[t] = Can t"
| "Can \<a>[t, u, v] = (Can t ∧ Can u ∧ Can v ∧ Src t = Trg u ∧ Src u = Trg v)"
| "Can \<a>-1[t, u, v] = (Can t ∧ Can u ∧ Can v ∧ Src t = Trg u ∧ Src u = Trg v)"
lemma Ide_implies_Can: shows"Ide t ==> Can t" by (induct t, auto)
lemma Can_implies_Arr: shows"Can t ==> Arr t" by (induct t, auto)
text‹
Canonical arrows can be formally inverted. ›
lemma Src_Inv [simp]: shows"Can t ==> Src (Inv t) = Src t" using Can_implies_Arr VSeq_implies_HPar apply (induct t, auto) by metis
lemma Trg_Inv [simp]: shows"Can t ==> Trg (Inv t) = Trg t" using Can_implies_Arr VSeq_implies_HPar apply (induct t, auto) by metis
lemma Dom_Inv [simp]: shows"Can t ==> Dom (Inv t) = Cod t" by (induct t, auto)
lemma Cod_Inv [simp]: shows"Can t ==> Cod (Inv t) = Dom t" by (induct t, auto)
lemma Inv_preserves_Ide: shows"Ide t ==> Ide (Inv t)" using Ide_implies_Can by (induct t, auto)
lemma Can_Inv [simp]: shows"Can t ==> Can (Inv t)" by (induct t, auto)
lemma Inv_in_Hom [intro]: assumes"Can t" shows"Inv t ∈ HHom (Src t) (Trg t)"and"Inv t ∈ VHom (Cod t) (Dom t)" using assms Can_Inv Can_implies_Arr by simp_all
lemma Inv_Ide [simp]: assumes"Ide a" shows"Inv a = a" using assms by (induct a, auto)
lemma Inv_Inv [simp]: assumes"Can t" shows"Inv (Inv t) = t" using assms by (induct t, auto)
subsection"Normal Terms"
text‹
We call a term ``normal'' if it is either a formal object or it is constructed from
primitive arrows using only horizontal composition associated to the right.
Essentially, such terms are (typed) composable sequences of arrows of @{term V},
where the empty list is represented by a formal object and ‹\⋆› is used as
the list constructor. ›
fun Nml :: "'a term ==> bool" where"Nml \<langle>μ\<rangle>0 = obj μ"
| "Nml \<langle>μ\<rangle> = arr μ"
| "Nml (\<langle>ν\<rangle> \<star> u) = (arr ν ∧ Nml u ∧¬ is_Prim0 u ∧\<langle>src ν\<rangle>0 = Trg u)"
| "Nml _ = False"
lemma Nml_HcompD: assumes"Nml (t \<star> u)" shows"\<langle>un_Prim t\<rangle> = t"and"arr (un_Prim t)"and"Nml t"and"Nml u" and"¬ is_Prim0 u"and"\<langle>src (un_Prim t)\<rangle>0 = Trg u"and"Src t = Trg u" proof - have1: "t = \<langle>un_Prim t\<rangle> ∧ arr (un_Prim t) ∧ Nml t ∧ Nml u ∧¬ is_Prim0 u ∧ \<langle>src (un_Prim t)\<rangle>0 = Trg u" using assms by (cases t; simp; cases u; simp) show"\<langle>un_Prim t\<rangle> = t"using1by simp show"arr (un_Prim t)"using1by simp show"Nml t"using1by simp show"Nml u"using1by simp show"¬ is_Prim0 u"using1by simp show"\<langle>src (un_Prim t)\<rangle>0 = Trg u"using1by simp show"Src t = Trg u" using assms apply (cases t) by simp_all qed
lemma Nml_implies_Arr: shows"Nml t ==> Arr t" by (induct t, auto simp add: Nml_HcompD)
lemma Nml_Src [simp]: shows"Nml t ==> Nml (Src t)" apply (induct t, simp_all) using Nml_HcompD by metis
lemma Nml_Trg [simp]: shows"Nml t ==> Nml (Trg t)" apply (induct t, simp_all) using Nml_HcompD by metis
lemma Nml_Dom [simp]: shows"Nml t ==> Nml (Dom t)" proof (induct t, simp_all add: Nml_HcompD) fix u v assume I1: "Nml (Dom u)" assume I2: "Nml (Dom v)" assume uv: "Nml (u \<star> v)" show"Nml (Dom u \<star> Dom v)" proof - have1: "is_Prim (Dom u) ∧ arr (un_Prim (Dom u)) ∧ Dom u = \<langle>dom (un_Prim u)\<rangle>" using uv by (cases u; simp; cases v, simp_all) have2: "Nml v ∧¬ is_Prim0 v ∧¬ is_Vcomp v ∧¬ is_Lunit' v ∧¬ is_Runit' v" using uv by (cases u, simp_all; cases v, simp_all) have"arr (dom (un_Prim u))" using1by fastforce moreoverhave"Nml (Dom v) ∧¬ is_Prim0 v" using2 I2 by (cases v, simp_all) moreoverhave"\<langle>src (dom (un_Prim u))\<rangle>0 = Trg (Dom v)" proof - have"Trg (Dom v) = Src (Dom u)" using uv Nml_implies_Arr by fastforce alsohave"... = \<langle>src (dom (un_Prim u))\<rangle>0" using1by fastforce finallyshow ?thesis by argo qed moreoverhave"¬ is_Prim0 (Dom v)" using2by (cases v, simp_all) ultimatelyshow ?thesis using12by simp qed qed
lemma Nml_Cod [simp]: shows"Nml t ==> Nml (Cod t)" proof (induct t, simp_all add: Nml_HcompD) fix u v assume I1: "Nml (Cod u)" assume I2: "Nml (Cod v)" assume uv: "Nml (u \<star> v)" show"Nml (Cod u \<star> Cod v)" proof - have1: "is_Prim (Cod u) ∧ arr (un_Prim (Cod u)) ∧ Cod u = \<langle>cod (un_Prim u)\<rangle>" using uv by (cases u; simp; cases v, simp_all) have2: "Nml v ∧¬ is_Prim0 v ∧¬ is_Vcomp v ∧¬ is_Lunit' v ∧¬ is_Runit' v" using uv by (cases u; simp; cases v, simp_all) have"arr (cod (un_Prim u))" using1by fastforce moreoverhave"Nml (Cod v) ∧¬ is_Prim0 v" using2 I2 by (cases v, simp_all) moreoverhave"\<langle>src (cod (un_Prim u))\<rangle>0 = Trg (Cod v)" proof - have"Trg (Cod v) = Src (Cod u)" using uv Nml_implies_Arr by fastforce alsohave"... = \<langle>src (cod (un_Prim u))\<rangle>0" using1by fastforce finallyshow ?thesis by argo qed moreoverhave"¬ is_Prim0 (Cod v)" using2by (cases v; simp) ultimatelyshow ?thesis using12by simp qed qed
lemma Nml_Inv [simp]: assumes"Can t"and"Nml t" shows"Nml (Inv t)" proof - have"Can t ∧ Nml t ==> Nml (Inv t)" apply (induct t, simp_all) proof - fix u v assume I1: "Nml u ==> Nml (Inv u)" assume I2: "Nml v ==> Nml (Inv v)" assume uv: "Can u ∧ Can v ∧ Src u = Trg v ∧ Nml (u \<star> v)" show"Nml (Inv u \<star> Inv v)" proof - have u: "Arr u ∧ Can u"using uv Can_implies_Arr by blast have v: "Arr v ∧ Can v"using uv Can_implies_Arr by blast have1: "\<langle>un_Prim u\<rangle> = u ∧ ide (un_Prim u) ∧ Nml u ∧ Nml v ∧¬ is_Prim0 v ∧ \<langle>src (un_Prim u)\<rangle>0 = Trg v" using uv Nml_HcompD [of u v] apply simp using uv by (cases u, simp_all) have2: "\<langle>un_Prim (Inv u)\<rangle> = Inv u ∧ arr (un_Prim (Inv u)) ∧ Nml (Inv u)" using1by (cases u; simp) moreoverhave"Nml (Inv v) ∧¬ is_Prim0 (Inv v)" using1 I2 by (cases v, simp_all) moreoverhave"\<langle>src (un_Prim (Inv u))\<rangle>0 = Trg (Inv v)" using12 v by (cases u, simp_all) ultimatelyshow ?thesis by (cases u, simp_all) qed qed thus ?thesis using assms by blast qed
text‹
The following function defines a horizontal composition for normal terms.
If such terms are regarded as lists, this is just (typed) list concatenation. ›
fun HcompNml (infixr‹\⌊\⋆\⌋›53) where"\<langle>ν\<rangle>0\<lfloor>\<star>\<rfloor> u = u"
| "t \<lfloor>\<star>\<rfloor> \<langle>μ\<rangle>0 = t"
| "\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u = \<langle>ν\<rangle> \<star> u"
| "(t \<star> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
| "t \<lfloor>\<star>\<rfloor> u = undefined"
lemma HcompNml_Prim [simp]: assumes"¬ is_Prim0 t" shows"\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> t = \<langle>ν\<rangle> \<star> t" using assms by (cases t, simp_all)
lemma HcompNml_term_Prim0 [simp]: assumes"Src t = Trg \<langle>μ\<rangle>0" shows"t \<lfloor>\<star>\<rfloor> \<langle>μ\<rangle>0 = t" using assms by (cases t, simp_all)
lemma HcompNml_Nml: assumes"Nml (t \<star> u)" shows"t \<lfloor>\<star>\<rfloor> u = t \<star> u" using assms HcompNml_Prim by (metis Nml_HcompD(1) Nml_HcompD(5))
lemma Nml_HcompNml: assumes"Nml t"and"Nml u"and"Src t = Trg u" shows"Nml (t \<lfloor>\<star>\<rfloor> u)" and"Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u" and"Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u" and"Src (t \<lfloor>\<star>\<rfloor> u) = Src u" and"Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t" proof - have0: "∧u. [ Nml t; Nml u; Src t = Trg u ]==> Nml (t \<lfloor>\<star>\<rfloor> u) ∧ Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u ∧ Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u ∧ Src (t \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t" proof (induct t, simp_all add: Nml_HcompD(1-4)) fix ν :: 'a and u :: "'a term" assume ν: "arr ν" assume u: "Nml u" assume1: "\<langle>src ν\<rangle>0 = Trg u" show"Nml (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) ∧ Dom (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>dom ν\<rangle> \<lfloor>\<star>\<rfloor> Dom u ∧ Cod (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>cod ν\<rangle> \<lfloor>\<star>\<rfloor> Cod u ∧ Src (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>trg ν\<rangle>0" using u ν 1by (cases u, simp_all) next fix u v w assume I1: "∧x. Nml x ==> Src v = Trg x ==> Nml (v \<lfloor>\<star>\<rfloor> x) ∧ Dom (v \<lfloor>\<star>\<rfloor> x) = Dom v \<lfloor>\<star>\<rfloor> Dom x ∧ Cod (v \<lfloor>\<star>\<rfloor> x) = Cod v \<lfloor>\<star>\<rfloor> Cod x ∧ Src (v \<lfloor>\<star>\<rfloor> x) = Src x ∧ Trg (v \<lfloor>\<star>\<rfloor> x) = Trg v" assume I2: "∧x. Nml x ==> Trg u = Trg x ==> Nml (w \<lfloor>\<star>\<rfloor> x) ∧ Dom (w \<lfloor>\<star>\<rfloor> x) = Dom w \<lfloor>\<star>\<rfloor> Dom x ∧ Cod (w \<lfloor>\<star>\<rfloor> x) = Cod w \<lfloor>\<star>\<rfloor> Cod x ∧ Src (w \<lfloor>\<star>\<rfloor> x) = Src x ∧ Trg (w \<lfloor>\<star>\<rfloor> x) = Trg w" assume vw: "Nml (v \<star> w)" assume u: "Nml u" assume wu: "Src w = Trg u" show"Nml ((v \<star> w) \<lfloor>\<star>\<rfloor> u) ∧ Dom ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = (Dom v \<star> Dom w) \<lfloor>\<star>\<rfloor> Dom u ∧ Cod ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = (Cod v \<star> Cod w) \<lfloor>\<star>\<rfloor> Cod u ∧ Src ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = Trg v" proof - have v: "v = \<langle>un_Prim v\<rangle> ∧ Nml v" using vw Nml_implies_Arr Nml_HcompD by metis have w: "Nml w ∧¬ is_Prim0 w ∧\<langle>src (un_Prim v)\<rangle>0 = Trg w" using vw by (simp add: Nml_HcompD) have"is_Prim0 u ==> ?thesis"by (cases u; simp add: vw wu) moreoverhave"¬ is_Prim0 u ==> ?thesis" proof - assume1: "¬ is_Prim0 u" have"Src v = Trg (w \<lfloor>\<star>\<rfloor> u)" using u v w I2 [of u] by (cases v, simp_all) hence"Nml (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) ∧ Dom (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Dom v \<lfloor>\<star>\<rfloor> Dom (w \<lfloor>\<star>\<rfloor> u) ∧ Cod (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Cod v \<lfloor>\<star>\<rfloor> Cod (w \<lfloor>\<star>\<rfloor> u) ∧ Src (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Trg v" using u v w I1 [of "w \<lfloor>\<star>\<rfloor> u"] I2 [of u] by argo moreoverhave"v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u = (v \<star> w) \<lfloor>\<star>\<rfloor> u" using1by (cases u, simp_all) moreoverhave"(Dom v \<star> Dom w) \<lfloor>\<star>\<rfloor> Dom u = Dom v \<lfloor>\<star>\<rfloor> Dom (w \<lfloor>\<star>\<rfloor> u)" using v w u vw 1 I2 Nml_Dom HcompNml_Prim Nml_HcompD(1) Nml_HcompD(5) by (cases u, simp_all) moreoverhave"(Cod v \<star> Cod w) \<lfloor>\<star>\<rfloor> Cod u = Cod v \<lfloor>\<star>\<rfloor> Cod (w \<lfloor>\<star>\<rfloor> u)" using v w u vw 1 I2 Nml_HcompD(1) Nml_HcompD(5) HcompNml_Prim by (cases u, simp_all) ultimatelyshow ?thesis by argo qed ultimatelyshow ?thesis by blast qed next fix a u assume a: "obj a" assume u: "Nml u" assume au: "\<langle>a\<rangle>0 = Trg u" show"Nml (Trg u \<lfloor>\<star>\<rfloor> u) ∧ Dom (Trg u \<lfloor>\<star>\<rfloor> u) = Dom (Trg u) \<lfloor>\<star>\<rfloor> Dom u ∧ Cod (Trg u \<lfloor>\<star>\<rfloor> u) = Cod (Trg u) \<lfloor>\<star>\<rfloor> Cod u ∧ Src (Trg u \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (Trg u \<lfloor>\<star>\<rfloor> u) = Trg (Trg u)" using au by (metis Cod.simps(1) Dom.simps(1) HcompNml.simps(1) Trg.simps(1) u) qed show"Nml (t \<lfloor>\<star>\<rfloor> u) "using assms 0by blast show"Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u"usingassms 0by blast show"Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u"usingassms 0by blast show"Src (t \<lfloor>\<star>\<rfloor> u) = Src u"using assms 0by blast show"Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t"using assms 0by blast qed
lemma HcompNml_in_Hom [intro]: assumes"Nml t"and"Nml u"and"Src t = Trg u" shows"t \<lfloor>\<star>\<rfloor> u ∈ HHom (Src u) (Trg t)" and"t \<lfloor>\<star>\<rfloor> u ∈ VHom (Dom t \<lfloor>\<star>\<rfloor> Dom u) (Cod t \<lfloor>\<star>\<rfloor> Cod u)" using assms Nml_HcompNml Nml_implies_Arr by auto
lemma Src_HcompNml: assumes"Nml t"and"Nml u"and"Src t = Trg u" shows"Src (t \<lfloor>\<star>\<rfloor> u) = Src u" using assms Nml_HcompNml(4) by simp
lemma Trg_HcompNml: assumes"Nml t"and"Nml u"and"Src t = Trg u" shows"Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t" using assms Nml_HcompNml(5) by simp
lemma Dom_HcompNml: assumes"Nml t"and"Nml u"and"Src t = Trg u" shows"Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u" using assms Nml_HcompNml(2) by simp
lemma Cod_HcompNml: assumes"Nml t"and"Nml u"and"Src t = Trg u" shows"Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u" using assms Nml_HcompNml(3) by simp
lemma is_Hcomp_HcompNml: assumes"Nml t"and"Nml u"and"Src t = Trg u" and"¬ is_Prim0 t"and"¬ is_Prim0 u" shows"is_Hcomp (t \<lfloor>\<star>\<rfloor> u)" proof - have"[¬ is_Hcomp (t \<lfloor>\<star>\<rfloor> u); Nml t; Nml u; Src t = Trg u; ¬ is_Prim0 t; ¬ is_Prim0 u ] ==> False" proof (induct t, simp_all add: Nml_HcompD) fix a assume a: "obj a" assume u: "Nml u" assume1: "¬ is_Hcomp u" assume2: "¬ is_Prim0 (Trg u)" show"False" using u 12by (cases u; simp) next fix v w assume I2: "¬ is_Hcomp (w \<lfloor>\<star>\<rfloor> u) ==> False" assume vw: "Nml (v \<star> w)" assume u: "Nml u" assume1: "¬ is_Hcomp ((v \<star> w) \<lfloor>\<star>\<rfloor> u)" assume2: "¬ is_Prim0 u" assume3: "Src w = Trg u" show"False" proof - have v: "v = \<langle>un_Prim v\<rangle>" using vw Nml_HcompD by metis have w: "Nml w ∧¬ is_Prim0 w ∧\<langle>src (un_Prim v)\<rangle>0 = Trg w" using vw Nml_HcompD [of v w] by blast have"(v \<star> w) \<lfloor>\<star>\<rfloor> u = v \<star> (w \<lfloor>\<star>\<rfloor> u)" proof - have"(v \<star> w) \<lfloor>\<star>\<rfloor> u = \<langle>un_Prim v\<rangle> \<lfloor>\<star>\<rfloor> (w \<lfloor>\<star>\<rfloor> u)" using u v 2by (cases u, simp_all) alsohave"... = \<langle>un_Prim v\<rangle> \<star> (w \<lfloor>\<star>\<rfloor> u)" using u w I2 by fastforce alsohave"... = v \<star> (w \<lfloor>\<star>\<rfloor> u)" using v by simp finallyshow ?thesis by simp qed thus ?thesis using1by simp qed qed thus ?thesis using assms by blast qed
text‹
The following function defines the ``dimension'' of a term,
which is the number of inputs (or outputs) when the term is regarded as an
interconnection matrix.
For normal terms, this is just the length of the term when regarded as a list
of arrows of @{term C}.
This function is used as a ranking of terms in the subsequent associativity proof. ›
primrec dim :: "'a term ==> nat" where"dim \<langle>μ\<rangle>0 = 0"
| "dim \<langle>μ\<rangle> = 1"
| "dim (t \<star> u) = (dim t + dim u)"
| "dim (t \<cdot> u) = dim t"
| "dim \<l>[t] = dim t"
| "dim \<l>-1[t] = dim t"
| "dim \<r>[t] = dim t"
| "dim \<r>-1[t] = dim t"
| "dim \<a>[t, u, v] = dim t + dim u + dim v"
| "dim \<a>-1[t, u, v] = dim t + dim u + dim v"
lemma HcompNml_assoc: assumes"Nml t"and"Nml u"and"Nml v"and"Src t = Trg u"and"Src u = Trg v" shows"(t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)" proof - have"∧n t u v. [ dim t = n; Nml t; Nml u; Nml v; Src t = Trg u; Src u = Trg v ]==> (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)" proof - fix n show"∧t u v. [ dim t = n; Nml t; Nml u; Nml v; Src t = Trg u; Src u = Trg v ]==> (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)" proof (induction n rule: nat_less_induct) fix n :: nat and t :: "'a term"and u v assume I: "∀m<n. ∀t u v. dim t = m ⟶ Nml t ⟶ Nml u ⟶ Nml v ⟶ Src t = Trg u ⟶ Src u = Trg v ⟶ (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)" assume dim: "dim t = n" assume t: "Nml t" assume u: "Nml u" assume v: "Nml v" assume tu: "Src t = Trg u" assume uv: "Src u = Trg v" show"(t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)" proof - have"is_Prim0 t ==> ?thesis"by (cases t; simp) moreoverhave"¬is_Prim0 t ==> is_Prim0 u ==> ?thesis" by (cases t; simp; cases u; simp) moreoverhave"¬ is_Prim0 t ==>¬ is_Prim0 u ==> is_Prim0 v ==> ?thesis" proof - assume1: "¬ is_Prim0 t" assume2: "¬ is_Prim0 u" assume3: "is_Prim0 v" have"¬is_Prim0 (t \<lfloor>\<star>\<rfloor> u)" using12 t u tu is_Hcomp_HcompNml [of t u] by (cases t, simp, cases u, auto) thus ?thesis using123 tu uv by (cases v, simp, cases "t \<lfloor>\<star>\<rfloor> u", simp_all) qed moreoverhave"¬is_Prim0 t ∧¬ is_Prim0 u ∧¬ is_Prim0 v ∧ is_Prim t ==> ?thesis" using v by (cases t, simp_all, cases u, simp_all; cases v, simp_all) moreoverhave"¬is_Prim0 t ∧¬ is_Prim0 u ∧¬ is_Prim0 v ∧ is_Hcomp t ==> ?thesis" proof (cases t, simp_all) fix w :: "'a term"and x :: "'a term" assume1: " ¬ is_Prim0 u ∧¬ is_Prim0 v" assume2: "t = (w \<star> x)" show"((w \<star> x) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = (w \<star> x) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)" proof - have w: "w = \<langle>un_Prim w\<rangle>" using t 12 Nml_HcompD by metis have x: "Nml x" using t w 12by (metis Nml.simps(3)) have"((w \<star> x) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = (w \<lfloor>\<star>\<rfloor> (x \<lfloor>\<star>\<rfloor> u)) \<lfloor>\<star>\<rfloor> v" using u v w x 12by (cases u, simp_all) alsohave"... = (w \<star> (x \<lfloor>\<star>\<rfloor> u)) \<lfloor>\<star>\<rfloor> v" using t w u 12 HcompNml_Prim is_Hcomp_HcompNml Nml_HcompD by (metis Src.simps(3) term.distinct_disc(3) tu) alsohave"... = w \<lfloor>\<star>\<rfloor> ((x \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v)" using u v w x 1by (cases u, simp_all; cases v, simp_all) alsohave"... = w \<lfloor>\<star>\<rfloor> (x \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v))" proof - have"dim x < dim t" using2 w by (cases w; simp) moreoverhave"Src x = Trg u ∧ Src u = Trg v" using tu uv 2by auto ultimatelyshow ?thesis using u v x dim I by simp qed alsohave"... = (w \<star> x) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)" proof - have3: "is_Hcomp (u \<lfloor>\<star>\<rfloor> v)" using u v uv 1 is_Hcomp_HcompNml by auto obtain u' :: "'a term"and v' where uv': "u \<lfloor>\<star>\<rfloor> v = u' \<star> v'" using3 is_Hcomp_def by blast thus ?thesis by simp qed finallyshow ?thesis by simp qed qed moreoverhave"is_Prim0 t ∨ is_Prim t ∨ is_Hcomp t" using t by (cases t, simp_all) ultimatelyshow ?thesis by blast qed qed qed thus ?thesis using assms by blast qed
lemma HcompNml_Trg_Nml: assumes"Nml t" shows"Trg t \<lfloor>\<star>\<rfloor> t = t" proof - have"Nml t ==> Trg t \<lfloor>\<star>\<rfloor> t = t" proof (induct t, simp_all add: Nml_HcompD) fix u v assume uv: "Nml (u \<star> v)" assume I1: "Trg u \<lfloor>\<star>\<rfloor> u = u" have1: "Nml u ∧ Nml v ∧ Src u = Trg v" using uv Nml_HcompD by blast have2: "Trg (u \<star> v) = Trg u" using uv by auto show"Trg u \<lfloor>\<star>\<rfloor> u \<star> v = u \<star> v" proof - have"Trg u \<lfloor>\<star>\<rfloor> u \<star> v = Trg u \<lfloor>\<star>\<rfloor> u \<lfloor>\<star>\<rfloor> v" using uv HcompNml_Nml by simp alsohave"... = (Trg u \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v" using12 HcompNml_assoc Src_Trg Nml_Trg Nml_implies_Arr by simp alsohave"... = u \<star> v" using I1 uv HcompNml_Nml by simp finallyshow ?thesis by simp qed qed thus ?thesis using assms by simp qed
lemma HcompNml_Nml_Src: assumes"Nml t" shows"t \<lfloor>\<star>\<rfloor> Src t = t" proof - have"Nml t ==> t \<lfloor>\<star>\<rfloor> Src t = t" proof (induct t, simp_all add: Nml_HcompD) fix u v assume uv: "Nml (u \<star> v)" assume I2: "v \<lfloor>\<star>\<rfloor> Src v = v" have1: "Nml u ∧ Nml v ∧ Src u = Trg v" using uv Nml_HcompD by blast have2: "Src (u \<star> v) = Src v" using uv Trg_HcompNml by auto show"(u \<star> v) \<lfloor>\<star>\<rfloor> Src v = u \<star> v" proof - have"(u \<star> v) \<lfloor>\<star>\<rfloor> Src v = (u \<lfloor>\<star>\<rfloor> v) \<lfloor>\<star>\<rfloor> Src v" using uv HcompNml_Nml by simp alsohave"... = u \<lfloor>\<star>\<rfloor> (v \<lfloor>\<star>\<rfloor> Src v)" using12 HcompNml_assoc Trg_Src Nml_Src Nml_implies_Arr by simp alsohave"... = u \<star> v" using I2 uv HcompNml_Nml by simp finallyshow ?thesis by simp qed qed thus ?thesis using assms by simp qed
lemma HcompNml_Obj_Nml: assumes"Obj t"and"Nml u"and"Src t = Trg u" shows"t \<lfloor>\<star>\<rfloor> u = u" using assms by (cases t, simp_all add: HcompNml_Trg_Nml)
lemma HcompNml_Nml_Obj: assumes"Nml t"and"Obj u"and"Src t = Trg u" shows"t \<lfloor>\<star>\<rfloor> u = t" using assms by (cases u, simp_all)
lemma Ide_HcompNml: assumes"Ide t"and"Ide u"and"Nml t"and"Nml u"and"Src t = Trg u" shows"Ide (t \<lfloor>\<star>\<rfloor> u)" using assms by (metis (mono_tags, lifting) Nml_HcompNml(1) Nml_implies_Arr Dom_HcompNml
Ide_Dom Ide_in_Hom(2) mem_Collect_eq)
lemma Can_HcompNml: assumes"Can t"and"Can u"and"Nml t"and"Nml u"and"Src t = Trg u" shows"Can (t \<lfloor>\<star>\<rfloor> u)" proof - have"∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Src t = Trg u ]==> Can (t \<lfloor>\<star>\<rfloor> u)" proof (induct t, simp_all add: HcompNml_Trg_Nml HcompNml_Nml_Src) show"∧x u. ide x ∧ arr x ==> Can u ∧ Nml u ==>\<langle>src x\<rangle>0 = Trg u ==> Can (\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u)" by (metis Ide.simps(1-2) Ide_implies_Can Can.simps(3) Nml.elims(2)
Nml.simps(2) HcompNml.simps(12) HcompNml_Prim Ide_HcompNml
Src.simps(2) term.disc(2)) show"∧v w u. (∧u. Nml v ==> Can u ∧ Nml u ==> Trg w = Trg u ==> Can (v \<lfloor>\<star>\<rfloor> u)) ==> (∧ua. Nml w ==> Can ua ∧ Nml ua ==> Trg u = Trg ua ==> Can (w \<lfloor>\<star>\<rfloor> ua)) ==> Can v ∧ Can w ∧ Src v = Trg w ∧ Nml (v \<star> w) ==> Can u ∧ Nml u ==> Src w = Trg u ==> Can ((v \<star> w) \<lfloor>\<star>\<rfloor> u)" by (metis Nml_HcompD(3-4) HcompNml_Nml Nml_HcompNml(1)
HcompNml_assoc Trg_HcompNml) qed thus ?thesis using assms by blast qed
lemma Inv_HcompNml: assumes"Can t"and"Can u"and"Nml t"and"Nml u"and"Src t = Trg u" shows"Inv (t \<lfloor>\<star>\<rfloor> u) = Inv t \<lfloor>\<star>\<rfloor> Inv u" proof - have"∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Src t = Trg u ] ==> Inv (t \<lfloor>\<star>\<rfloor> u) = Inv t \<lfloor>\<star>\<rfloor> Inv u" proof (induct t, simp_all add: HcompNml_Trg_Nml HcompNml_Nml_Src) show"∧x u. [ obj x; Can u ∧ Nml u; \<langle>x\<rangle>0 = Trg u ]==> Inv u = Inv (Trg u) \<lfloor>\<star>\<rfloor> Inv u" by (metis HcompNml.simps(1) Inv.simps(1)) show"∧x u. ide x ∧ arr x ==> Can u ∧ Nml u ==>\<langle>src x\<rangle>0 = Trg u ==> Inv (\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>x\<rangle> \<lfloor>\<star>\<rfloor> Inv u" by (metis Ide.simps(2) HcompNml.simps(2) HcompNml_Prim Inv.simps(1,3)
Inv_Ide Inv_Inv is_Prim0_def) fix v w u assume I1: "∧x. Nml v ==> Can x ∧ Nml x ==> Trg w = Trg x ==> Inv (v \<lfloor>\<star>\<rfloor> x) = Inv v \<lfloor>\<star>\<rfloor> Inv x" assume I2: "∧x. Nml w ==> Can x ∧ Nml x ==> Trg u = Trg x ==> Inv (w \<lfloor>\<star>\<rfloor> x) = Inv w \<lfloor>\<star>\<rfloor> Inv x" assume vw: "Can v ∧ Can w ∧ Src v = Trg w ∧ Nml (v \<star> w)" assume wu: "Src w = Trg u" assume u: "Can u ∧ Nml u" have v: "Can v ∧ Nml v" using vw Nml_HcompD by blast have w: "Can w ∧ Nml w" using v vw by (cases v, simp_all) show"Inv ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = (Inv v \<star> Inv w) \<lfloor>\<star>\<rfloor> Inv u" proof - have"is_Prim0 u ==> ?thesis" apply (cases u) by simp_all moreoverhave"¬ is_Prim0 u ==> ?thesis" proof - assume1: "¬ is_Prim0 u" have"Inv ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = Inv (v \<lfloor>\<star>\<rfloor> (w \<lfloor>\<star>\<rfloor> u))" using1by (cases u, simp_all) alsohave"... = Inv v \<lfloor>\<star>\<rfloor> Inv (w \<lfloor>\<star>\<rfloor> u)" using u v w vw wu I1 Nml_HcompNml Can_HcompNml Nml_Inv Can_Inv by simp alsohave"... = Inv v \<lfloor>\<star>\<rfloor> (Inv w \<lfloor>\<star>\<rfloor> Inv u)" using u v w I2 Nml_HcompNml by simp alsohave"... = (Inv v \<star> Inv w) \<lfloor>\<star>\<rfloor> Inv u" using v 1by (cases u, simp_all) finallyshow ?thesis by blast qed ultimatelyshow ?thesis by blast qed qed thus ?thesis using assms by blast qed
text‹
The following function defines vertical composition for compatible normal terms,
by ``pushing the composition down'' to arrows of @{text V}. ›
fun VcompNml :: "'a term ==> 'a term ==> 'a term" (infixr‹\⌊\⋅\⌋›55) where"\<langle>ν\<rangle>0\<lfloor>\<cdot>\<rfloor> u = u"
| "\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> \<langle>μ\<rangle> = \<langle>ν ⋅ μ\<rangle>"
| "(u \<star> v) \<lfloor>\<cdot>\<rfloor> (w \<star> x) = (u \<lfloor>\<cdot>\<rfloor> w\<star> v \<lfloor>\<cdot>\<rfloor> x)"
| "t \<lfloor>\<cdot>\<rfloor> \<langle>μ\<rangle>0 = t"
| "t \<lfloor>\<cdot>\<rfloor> _ = undefined \<cdot> undefined"
text‹
Note that the last clause above is not relevant to normal terms.
We have chosen a provably non-normal value in order to validate associativity. ›
lemma Nml_VcompNml: assumes"Nml t"and"Nml u"and"Dom t = Cod u" shows"Nml (t \<lfloor>\<cdot>\<rfloor> u)" and"Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u" and"Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t" proof - have0: "∧u. [ Nml t; Nml u; Dom t = Cod u ]==> Nml (t \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t" proof (induct t, simp_all add: Nml_HcompD) show"∧x u. obj x ==> Nml u ==>\<langle>x\<rangle>0 = Cod u ==> Nml (Cod u \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (Cod u \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod (Cod u \<lfloor>\<cdot>\<rfloor> u) = Cod (Cod u)" by (metis Cod.simps(1) VcompNml.simps(1)) fix ν u assume ν: "arr ν" assume u: "Nml u" assume1: "\<langle>dom ν\<rangle> = Cod u" show"Nml (\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod (\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> u) = \<langle>cod ν\<rangle>" using ν u 1by (cases u, simp_all) next fix u v w assume I2: "∧u. [ Nml u; Dom w = Cod u ]==> Nml (w \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (w \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod (w \<lfloor>\<cdot>\<rfloor> u) = Cod w" assume vw: "Nml (v \<star> w)" have v: "Nml v" using vw Nml_HcompD by blast have w: "Nml w" using vw Nml_HcompD by blast assume u: "Nml u" assume1: "(Dom v \<star> Dom w) = Cod u" show"Nml ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) ∧ Dom ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) = Cod v \<star> Cod w" using u v w 1 proof (cases u, simp_all) fix x y assume2: "u = x \<star> y" have4: "is_Prim x ∧ x = \<langle>un_Prim x\<rangle> ∧ arr (un_Prim x) ∧ Nml y ∧¬ is_Prim0 y" using u 2by (cases x, cases y, simp_all) have5: "is_Prim v ∧ v = \<langle>un_Prim v\<rangle> ∧ arr (un_Prim v) ∧ Nml w ∧¬ is_Prim0 w" using v w vw by (cases v, simp_all) have6: "dom (un_Prim v) = cod (un_Prim x) ∧ Dom w = Cod y" proof - have"\<langle>src (un_Prim v)\<rangle>0 = Trg w"using vw Nml_HcompD [of v w] by simp thus"dom (un_Prim v) = cod (un_Prim x) ∧ Dom w = Cod y" using1245apply (cases u, simp_all) by (metis Cod.simps(2) Dom.simps(2) term.simps(2)) qed have"(v \<star> w) \<lfloor>\<cdot>\<rfloor> u = \<langle>un_Prim v ⋅ un_Prim x\<rangle> \<star> w \<lfloor>\<cdot>\<rfloor> y" using2456 VcompNml.simps(2) [of "un_Prim v""un_Prim x"] by simp moreoverhave"Nml (\<langle>un_Prim v ⋅ un_Prim x\<rangle> \<star> w \<lfloor>\<cdot>\<rfloor> y)" proof - have"Nml (w \<lfloor>\<cdot>\<rfloor> y)" using I2 456by simp moreoverhave"¬ is_Prim0 (w \<lfloor>\<cdot>\<rfloor> y)" using vw 456 I2 Nml_Cod Nml_HcompD(5) is_Prim0_def by (metis Cod.simps(1) Cod.simps(3)) moreoverhave"\<langle>src (un_Prim v ⋅ un_Prim x)\<rangle>0 = Trg (w \<lfloor>\<cdot>\<rfloor> y)" using vw 456 I2 Nml_HcompD(6) Nml_implies_Arr
src.as_nat_trans.naturality1 src.as_nat_trans.preserves_comp_2
Trg_Cod src_cod by (metis seqI) ultimatelyshow ?thesis using456 Nml.simps(3) [of "un_Prim v ⋅ un_Prim x""(w \<lfloor>\<cdot>\<rfloor> y)"] by simp qed ultimatelyshow"Nml (v \<lfloor>\<cdot>\<rfloor> x \<star> w \<lfloor>\<cdot>\<rfloor> y) ∧ Dom (v \<lfloor>\<cdot>\<rfloor> x) = Dom x ∧ Dom (w \<lfloor>\<cdot>\<rfloor> y) = Dom y ∧ Cod (v \<lfloor>\<cdot>\<rfloor> x) = Cod v ∧ Cod (w \<lfloor>\<cdot>\<rfloor> y) = Cod w" using456 I2 by (metis (no_types, lifting) Cod.simps(2) Dom.simps(2) VcompNml.simps(2)
cod_comp dom_comp seqI) qed qed show"Nml (t \<lfloor>\<cdot>\<rfloor> u)"using assms 0by blast show"Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u"using assms 0by blast show"Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t"using assms 0by blast qed
lemma VcompNml_in_Hom [intro]: assumes"Nml t"and"Nml u"and"Dom t = Cod u" shows"t \<lfloor>\<cdot>\<rfloor> u ∈ HHom (Src u) (Trg u)"and"t \<lfloor>\<cdot>\<rfloor> u ∈ VHom (Dom u) (Cod t)" proof - show1: "t \<lfloor>\<cdot>\<rfloor> u ∈ VHom (Dom u) (Cod t)" using assms Nml_VcompNml Nml_implies_Arr by simp show"t \<lfloor>\<cdot>\<rfloor> u ∈ HHom (Src u) (Trg u)" using assms 1 Src_Dom Trg_Dom Nml_implies_Arr by fastforce qed
lemma Src_VcompNml: assumes"Nml t"and"Nml u"and"Dom t = Cod u" shows"Src (t \<lfloor>\<cdot>\<rfloor> u) = Src u" using assms VcompNml_in_Hom by simp
lemma Trg_VcompNml: assumes"Nml t"and"Nml u"and"Dom t = Cod u" shows"Trg (t \<lfloor>\<cdot>\<rfloor> u) = Trg u" using assms VcompNml_in_Hom by simp
lemma Dom_VcompNml: assumes"Nml t"and"Nml u"and"Dom t = Cod u" shows"Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u" using assms Nml_VcompNml(2) by simp
lemma Cod_VcompNml: assumes"Nml t"and"Nml u"and"Dom t = Cod u" shows"Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t" using assms Nml_VcompNml(3) by simp
lemma VcompNml_Cod_Nml [simp]: assumes"Nml t" shows"VcompNml (Cod t) t = t" proof - have"Nml t ==> Cod t \<lfloor>\<cdot>\<rfloor> t = t" apply (induct t) by (auto simp add: Nml_HcompD comp_cod_arr) thus ?thesis using assms by blast qed
lemma VcompNml_Nml_Dom [simp]: assumes"Nml t" shows"t \<lfloor>\<cdot>\<rfloor> (Dom t) = t" proof - have"Nml t ==> t \<lfloor>\<cdot>\<rfloor> Dom t = t" apply (induct t) by (auto simp add: Nml_HcompD comp_arr_dom) thus ?thesis using assms by blast qed
lemma VcompNml_Ide_Nml [simp]: assumes"Nml t"and"Ide a"and"Dom a = Cod t" shows"a \<lfloor>\<cdot>\<rfloor> t = t" using assms Ide_in_Hom by simp
lemma VcompNml_Nml_Ide [simp]: assumes"Nml t"and"Ide a"and"Dom t = Cod a" shows"t \<lfloor>\<cdot>\<rfloor> a = t" using assms Ide_in_Hom by auto
lemma VcompNml_assoc: assumes"Nml t"and"Nml u"and"Nml v" and"Dom t = Cod u"and"Dom u = Cod v" shows"(t \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = t \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)" proof - have"∧u v. [ Nml t; Nml u; Nml v; Dom t = Cod u; Dom u = Cod v ]==> (t \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = t \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)" proof (induct t, simp_all) show"∧x u v. obj x ==> Nml u ==> Nml v ==>\<langle>x\<rangle>0 = Cod u ==> Dom u = Cod v ==> u \<lfloor>\<cdot>\<rfloor> v = Cod u \<lfloor>\<cdot>\<rfloor> u \<lfloor>\<cdot>\<rfloor> v" by (metis VcompNml.simps(1)) fix f u v assume f: "arr f" assume u: "Nml u" assume v: "Nml v" assume1: "\<langle>dom f\<rangle> = Cod u" assume2: "Dom u = Cod v" show"(\<langle>f\<rangle> \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = \<langle>f\<rangle> \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)" using u v f 12 comp_assoc apply (cases u) apply simp_all apply (cases v) by simp_all next fix u v w x assume I1: "∧u v. [ Nml w; Nml u; Nml v; Dom w = Cod u; Dom u = Cod v ]==> (w \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = w \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)" assume I2: "∧u v. [ Nml x; Nml u; Nml v; Dom x = Cod u; Dom u = Cod v ]==> (x \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = x \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)" assume wx: "Nml (w \<star> x)" assume u: "Nml u" assume v: "Nml v" assume1: "(Dom w \<star> Dom x) = Cod u" assume2: "Dom u = Cod v" show"((w \<star> x) \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = (w \<star> x) \<lfloor>\<cdot>\<rfloor> u \<lfloor>\<cdot>\<rfloor> v" proof - have w: "Nml w" using wx Nml_HcompD by blast have x: "Nml x" using wx Nml_HcompD by blast have"is_Hcomp u" using u 1by (cases u) simp_all thus ?thesis using u v apply (cases u, simp_all, cases v, simp_all) proof - fix u1 u2 v1 v2 assume3: "u = (u1 \<star> u2)" assume4: "v = (v1 \<star> v2)" show"(w \<lfloor>\<cdot>\<rfloor> u1) \<lfloor>\<cdot>\<rfloor> v1 = w \<lfloor>\<cdot>\<rfloor> u1 \<lfloor>\<cdot>\<rfloor> v1 ∧ (x \<lfloor>\<cdot>\<rfloor> u2) \<lfloor>\<cdot>\<rfloor> v2 = x \<lfloor>\<cdot>\<rfloor> u2 \<lfloor>\<cdot>\<rfloor> v2" proof - have"Nml u1 ∧ Nml u2" using u 3 Nml_HcompD by blast moreoverhave"Nml v1 ∧ Nml v2" using v 4 Nml_HcompD by blast ultimatelyshow ?thesis using w x I1 I2 1234by simp qed qed qed qed thus ?thesis using assms by blast qed
lemma Ide_VcompNml: assumes"Ide t"and"Ide u"and"Nml t"and"Nml u"and"Dom t = Cod u" shows"Ide (t \<lfloor>\<cdot>\<rfloor> u)" proof - have"∧u. [ Ide t; Ide u; Nml t; Nml u; Dom t = Cod u ]==> Ide (VcompNml t u)" by (induct t, simp_all) thus ?thesis using assms by blast qed
lemma Can_VcompNml: assumes"Can t"and"Can u"and"Nml t"and"Nml u"and"Dom t = Cod u" shows"Can (t \<lfloor>\<cdot>\<rfloor> u)" proof - have"∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Dom t = Cod u ]==> Can (t \<lfloor>\<cdot>\<rfloor> u)" proof (induct t, simp_all) fix t u v assume I1: "∧v. [ Nml t; Can v ∧ Nml v; Dom t = Cod v ]==> Can (t \<lfloor>\<cdot>\<rfloor> v)" assume I2: "∧v. [ Nml u; Can v ∧ Nml v; Dom u = Cod v ]==> Can (u \<lfloor>\<cdot>\<rfloor> v)" assume tu: "Can t ∧ Can u ∧ Src t = Trg u ∧ Nml (t \<star> u)" have t: "Can t ∧ Nml t" using tu Nml_HcompD by blast have u: "Can u ∧ Nml u" using tu Nml_HcompD by blast assume v: "Can v ∧ Nml v" assume1: "(Dom t \<star> Dom u) = Cod v" show"Can ((t \<star> u) \<lfloor>\<cdot>\<rfloor> v)" proof - have2: "(Dom t \<star> Dom u) = Cod v"using1by simp show ?thesis using v 2 proof (cases v; simp) fix w x assume wx: "v = (w \<star> x)" have"Can w ∧ Nml w"using v wx Nml_HcompD Can.simps(3) by blast moreoverhave"Can x ∧ Nml x"using v wx Nml_HcompD Can.simps(3) by blast moreoverhave"Dom t = Cod w"using2 wx by simp moreoverhave ux: "Dom u = Cod x"using2 wx by simp ultimatelyshow"Can (t \<lfloor>\<cdot>\<rfloor> w) ∧ Can (u \<lfloor>\<cdot>\<rfloor> x) ∧ Src (t \<lfloor>\<cdot>\<rfloor> w) = Trg (u \<lfloor>\<cdot>\<rfloor> x)" using t u v tu wx I1 I2 by (metis Nml_HcompD(7) Src_VcompNml Trg_VcompNml) qed qed qed thus ?thesis using assms by blast qed
lemma Inv_VcompNml: assumes"Can t"and"Can u"and"Nml t"and"Nml u"and"Dom t = Cod u" shows"Inv (t \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> Inv t" proof - have"∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Dom t = Cod u ]==> Inv (t \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> Inv t" proof (induct t, simp_all) show"∧x u. [ obj x; Can u ∧ Nml u; \<langle>x\<rangle>0 = Cod u ]==> Inv u = Inv u \<lfloor>\<cdot>\<rfloor> Inv (Cod u)" by (simp add: Can_implies_Arr) show"∧x u. [ ide x ∧ arr x; Can u ∧ Nml u; \<langle>x\<rangle> = Cod u ]==> Inv u = Inv u \<lfloor>\<cdot>\<rfloor> Inv (Cod u)" by (simp add: Can_implies_Arr) fix v w u assume vw: "Can v ∧ Can w ∧ Src v = Trg w ∧ Nml (v \<star> w)" have v: "Can v ∧ Nml w" using vw Nml_HcompD by blast have w: "Can w ∧ Nml w" using vw Nml_HcompD by blast assume I1: "∧x. [ Nml v; Can x ∧ Nml x; Dom v = Cod x ]==> Inv (v \<lfloor>\<cdot>\<rfloor> x) = Inv x \<lfloor>\<cdot>\<rfloor> Inv v" assume I2: "∧x. [ Nml w; Can x ∧ Nml x; Dom w = Cod x ]==> Inv (w \<lfloor>\<cdot>\<rfloor> x) = Inv x \<lfloor>\<cdot>\<rfloor> Inv w" assume u: "Can u ∧ Nml u" assume1: "(Dom v \<star> Dom w) = Cod u" show"Inv ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> Inv w)" using v 1 proof (cases w, simp_all) show"∧μ. obj μ ==> Dom v \<star> \<langle>μ\<rangle>0 = Cod u ==> w = \<langle>μ\<rangle>0==> Can v ==> Inv ((v \<star> \<langle>μ\<rangle>0) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> \<langle>μ\<rangle>0)" using Nml_HcompD(5) is_Prim0_def vw by blast show"∧μ. arr μ ==> Dom v \<star> \<langle>dom μ\<rangle> = Cod u ==> w = \<langle>μ\<rangle> ==> Can v ==> Inv ((v \<star> \<langle>μ\<rangle>) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> \<langle>inv μ\<rangle>)" by (metis Ide.simps(2) Can.simps(2) Nml_HcompD(1) Dom.simps(2) Inv_Ide
Dom_Inv Nml_Inv ideD(2) inv_ide VcompNml_Cod_Nml VcompNml_Nml_Dom
u vw) show"∧y z. Nml (y \<star> z) ==> Dom v \<star> Dom y \<star> Dom z = Cod u ==> w = y \<star> z ==> Can v ==> Inv ((v \<star> y \<star> z) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> Inv y \<star> Inv z)" proof - fix y z assume2: "Nml (y \<star> z)" assume yz: "w = y \<star> z" show"Inv ((v \<star> y \<star> z) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> Inv y \<star> Inv z)" using u vw yz I1 I2 12 VcompNml_Nml_Ide apply (cases u) apply simp_all by (metis Nml_HcompD(3-4)) qed qed qed thus ?thesis using assms by blast qed
lemma Can_and_Nml_implies_Ide: assumes"Can t"and"Nml t" shows"Ide t" proof - have"[ Can t; Nml t ]==> Ide t" apply (induct t) by (simp_all add: Nml_HcompD) thus ?thesis using assms by blast qed
lemma VcompNml_Can_Inv [simp]: assumes"Can t"and"Nml t" shows"t \<lfloor>\<cdot>\<rfloor> Inv t = Cod t" using assms Can_and_Nml_implies_Ide Ide_in_Hom by simp
lemma VcompNml_Inv_Can [simp]: assumes"Can t"and"Nml t" shows"Inv t \<lfloor>\<cdot>\<rfloor> t = Dom t" using assms Can_and_Nml_implies_Ide Ide_in_Hom by simp
text‹
The next fact is a syntactic version of the interchange law, for normal terms. ›
lemma VcompNml_HcompNml: assumes"Nml t"and"Nml u"and"Nml v"and"Nml w" and"VSeq t v"and"VSeq u w"and"Src v = Trg w" shows"(t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)" proof - have"∧u v w. [ Nml t; Nml u; Nml v; Nml w; VSeq t v; VSeq u w; Src t = Trg u; Src v = Trg w ]==> (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)" proof (induct t, simp_all) fix u v w x assume u: "Nml u" assume v: "Nml v" assume w: "Nml w" assume uw: "VSeq u w" show"∧x. Arr v ∧\<langle>x\<rangle>0 = Cod v ==> (Cod v \<lfloor>\<star>\<rfloor> u)\<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = v \<lfloor>\<star>\<rfloor> u\<lfloor>\<cdot>\<rfloor> w" using u v w uw by (cases v) simp_all show"∧x. [ arr x; Arr v ∧\<langle>dom x\<rangle> = Cod v; \<langle>src x\<rangle>0= Trg u; Src v = Trg w ]==> (\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = \<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w" proof - fix x assume x: "arr x" assume1: "Arr v ∧\<langle>dom x\<rangle> = Cod v" assume tu: "\<langle>src x\<rangle>0 = Trg u" assume vw: "Src v = Trg w" show"(\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = \<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w" proof - have2: "v = \<langle>un_Prim v\<rangle> ∧ arr (un_Prim v)"using v 1by (cases v) simp_all have"is_Prim0 u ==> ?thesis" using u v w x tu uw vw 12 Cod.simps(3) VcompNml_Cod_Nml Dom.simps(2)
HcompNml_Prim HcompNml_term_Prim0 Nml_HcompNml(3) HcompNml_Trg_Nml apply (cases u) apply simp_all by (cases w, simp_all add: Src_VcompNml) moreoverhave"¬ is_Prim0 u ==> ?thesis" proof - assume3: "¬ is_Prim0 u" hence4: "¬ is_Prim0 w"using u w uw by (cases u, simp_all; cases w, simp_all) have"(\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (\<langle>x\<rangle> \<star> u) \<lfloor>\<cdot>\<rfloor> (v \<star> w)" proof - have"\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u = \<langle>x\<rangle> \<star> u" using u x 3 HcompNml_Nml by (cases u, simp_all) moreoverhave"v \<lfloor>\<star>\<rfloor> w = v \<star> w" using w 24 HcompNml_Nml by (cases v, simp_all; cases w, simp_all) ultimatelyshow ?thesis by simp qed alsohave5: "... = (\<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v) \<star> (u \<lfloor>\<cdot>\<rfloor> w)"by simp alsohave"... = (\<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)" using x u w uw vw 12345
HcompNml_Nml HcompNml_Prim Nml_HcompNml(1) by (metis Cod.simps(3) Nml.simps(3) Dom.simps(2) Dom.simps(3)
Nml_VcompNml(1) tu v) finallyshow ?thesis by blast qed ultimatelyshow ?thesis by blast qed qed fix t1 t2 assume t12: "Nml (t1 \<star> t2)" assume I1: "∧u v w. [ Nml t1; Nml u; Nml v; Nml w; Arr v ∧ Dom t1 = Cod v; VSeq u w; Trg t2 = Trg u; Src v = Trg w ]==> (t1 \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = t1 \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w" assume I2: "∧u' v w. [ Nml t2; Nml u'; Nml v; Nml w; Arr v ∧ Dom t2 = Cod v; VSeq u' w; Trg u = Trg u'; Src v = Trg w ]==> (t2 \<lfloor>\<star>\<rfloor> u') \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t2 \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u' \<lfloor>\<cdot>\<rfloor> w)" have t1: "t1 = \<langle>un_Prim t1\<rangle> ∧ arr (un_Prim t1) ∧ Nml t1" using t12 by (cases t1, simp_all) have t2: "Nml t2 ∧¬is_Prim0 t2" using t12 by (cases t1, simp_all) assume vw: "Src v = Trg w" assume tu: "Src t2 = Trg u" assume1: "Arr t1 ∧ Arr t2 ∧ Src t1 = Trg t2 ∧ Arr v ∧ (Dom t1 \<star> Dom t2) = Cod v" show"((t1 \<star> t2) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t1 \<star> t2) \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w" proof - have"is_Prim0 u ==> ?thesis" using u v w uw tu vw t12 I1 I2 1 Obj_Src apply (cases u) apply simp_all by (cases w, simp_all add: Src_VcompNml) moreoverhave"¬ is_Prim0 u ==> ?thesis" proof - assume u': "¬ is_Prim0 u" hence w': "¬ is_Prim0 w"using u w uw by (cases u, simp_all; cases w, simp_all) show ?thesis using1 v proof (cases v, simp_all) fix v1 v2 assume v12: "v = v1 \<star> v2" have v1: "v1 = \<langle>un_Prim v1\<rangle> ∧ arr (un_Prim v1) ∧ Nml v1" using v v12 by (cases v1, simp_all) have v2: "Nml v2 ∧¬ is_Prim0 v2" using v v12 by (cases v1, simp_all) have2: "v = (\<langle>un_Prim v1\<rangle> \<star> v2)" using v1 v12 by simp show"((t1 \<star> t2) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> ((v1 \<star> v2) \<lfloor>\<star>\<rfloor> w) = (t1 \<lfloor>\<cdot>\<rfloor> v1 \<star> t2 \<lfloor>\<cdot>\<rfloor> v2) \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w" proof - have3: "(t1 \<star> t2) \<lfloor>\<star>\<rfloor> u = t1 \<lfloor>\<star>\<rfloor> (t2 \<lfloor>\<star>\<rfloor> u)" using u u' by (cases u, simp_all) have4: "v \<lfloor>\<star>\<rfloor> w = v1 \<lfloor>\<star>\<rfloor> v2 \<lfloor>\<star>\<rfloor> w" proof - have"Src v1 = Trg v2" using v v12 1 Arr.simps(3) Nml_HcompD(7) by blast moreoverhave"Src v2 = Trg w" using v v12 vw by simp ultimatelyshow ?thesis using v w v1 v2 v12 2 HcompNml_assoc [of v1 v2 w] HcompNml_Nml by metis qed have"((t1 \<star> t2) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> ((v1 \<star> v2) \<lfloor>\<star>\<rfloor> w) = (t1 \<lfloor>\<star>\<rfloor> (t2 \<lfloor>\<star>\<rfloor> u)) \<lfloor>\<cdot>\<rfloor> (v1 \<lfloor>\<star>\<rfloor> (v2 \<lfloor>\<star>\<rfloor> w))" using34 v12 by simp alsohave"... = (t1 \<lfloor>\<cdot>\<rfloor> v1) \<lfloor>\<star>\<rfloor> ((t2 \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v2 \<lfloor>\<star>\<rfloor> w))" proof - have"is_Hcomp (t2 \<lfloor>\<star>\<rfloor> u)" using t2 u u' tu is_Hcomp_HcompNml by auto moreoverhave"is_Hcomp (v2 \<lfloor>\<star>\<rfloor> w)" using v2 v12 w w' vw is_Hcomp_HcompNml by auto ultimatelyshow ?thesis using u u' v w t1 v1 t12 v12 HcompNml_Prim by (metis VcompNml.simps(2) VcompNml.simps(3) is_Hcomp_def term.distinct_disc(3)) qed alsohave"... = (t1 \<lfloor>\<cdot>\<rfloor> v1) \<lfloor>\<star>\<rfloor> (t2 \<lfloor>\<cdot>\<rfloor> v2) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)" using u w tu uw vw t2 v2 12 Nml_implies_Arr I2 by auto alsohave"... = ((t1 \<lfloor>\<cdot>\<rfloor> v1) \<star> (t2 \<lfloor>\<cdot>\<rfloor> v2)) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)" proof - have"¬is_Prim0 (u \<lfloor>\<cdot>\<rfloor> w)" using u w u' w' by (cases u, simp_all; cases w, simp_all) hence"((t1 \<lfloor>\<cdot>\<rfloor> v1) \<star> (t2 \<lfloor>\<cdot>\<rfloor> v2)) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w) = (t1 \<lfloor>\<cdot>\<rfloor> v1) \<lfloor>\<star>\<rfloor> ((t2 \<lfloor>\<cdot>\<rfloor> v2) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w))" by (cases "u \<lfloor>\<cdot>\<rfloor> w") simp_all thus ?thesis by presburger qed finallyshow ?thesis by blast qed qed qed ultimatelyshow ?thesis by blast qed qed moreoverhave"Src t = Trg u" using assms Src_Dom Trg_Dom Src_Cod Trg_Cod Nml_implies_Arr by metis ultimatelyshow ?thesis using assms by simp qed
text‹
The following function reduces a formal arrow to normal form. ›
lemma Nmlize_in_Hom [intro]: assumes"Arr t" shows"\<lfloor>t\<rfloor> ∈ HHom (Src t) (Trg t)"and"\<lfloor>t\<rfloor> ∈ VHom \<lfloor>Dom t\<rfloor> \<lfloor>Cod t\<rfloor>" using assms Nml_Nmlize Nml_implies_Arr by auto
lemma Nmlize_Src: assumes"Arr t" shows"\<lfloor>Src t\<rfloor> = Src \<lfloor>t\<rfloor>"and"\<lfloor>Src t\<rfloor> = Src t" proof - have1: "Obj (Src t)" using assms by simp obtain a where a: "obj a ∧ Src t = \<langle>a\<rangle>0" using1by (cases "Src t", simp_all) show"\<lfloor>Src t\<rfloor> = Src t" using a by simp thus"\<lfloor>Src t\<rfloor> = Src \<lfloor>t\<rfloor>" using assms Nmlize_in_Hom by simp qed
lemma Nmlize_Trg: assumes"Arr t" shows"\<lfloor>Trg t\<rfloor> = Trg \<lfloor>t\<rfloor>"and"\<lfloor>Trg t\<rfloor> = Trg t" proof - have1: "Obj (Trg t)" using assms by simp obtain a where a: "obj a ∧ Trg t = \<langle>a\<rangle>0" using1by (cases "Trg t", simp_all) show"\<lfloor>Trg t\<rfloor> = Trg t" using a by simp thus"\<lfloor>Trg t\<rfloor> = Trg \<lfloor>t\<rfloor>" using assms Nmlize_in_Hom by simp qed
lemma Nmlize_Dom: assumes"Arr t" shows"\<lfloor>Dom t\<rfloor> = Dom \<lfloor>t\<rfloor>" using assms Nmlize_in_Hom by simp
lemma Nmlize_Cod: assumes"Arr t" shows"\<lfloor>Cod t\<rfloor> = Cod \<lfloor>t\<rfloor>" using assms Nmlize_in_Hom by simp
lemma Ide_Nmlize_Ide: assumes"Ide t" shows"Ide \<lfloor>t\<rfloor>" proof - have"Ide t ==> Ide \<lfloor>t\<rfloor>" using Ide_HcompNml Nml_Nmlize by (induct t, simp_all) thus ?thesis using assms by blast qed
lemma Ide_Nmlize_Can: assumes"Can t" shows"Ide \<lfloor>t\<rfloor>" proof - have"Can t ==> Ide \<lfloor>t\<rfloor>" using Can_implies_Arr Ide_HcompNml Nml_Nmlize Ide_VcompNml Nml_HcompNml apply (induct t) apply (auto simp add: Dom_Ide Cod_Ide) by (metis Ide_VcompNml) thus ?thesis using assms by blast qed
lemma Can_Nmlize_Can: assumes"Can t" shows"Can \<lfloor>t\<rfloor>" using assms Ide_Nmlize_Can Ide_implies_Can by auto
lemma Nmlize_Nml [simp]: assumes"Nml t" shows"\<lfloor>t\<rfloor> = t" proof - have"Nml t ==>\<lfloor>t\<rfloor> = t" apply (induct t, simp_all) using HcompNml_Prim Nml_HcompD by metis thus ?thesis using assms by blast qed
lemma Nmlize_Nmlize [simp]: assumes"Arr t" shows"\<lfloor>\<lfloor>t\<rfloor>\<rfloor> = \<lfloor>t\<rfloor>" using assms Nml_Nmlize Nmlize_Nml by blast
lemma Nmlize_Hcomp: assumes"Arr t"and"Arr u" shows"\<lfloor>t \<star> u\<rfloor> = \<lfloor>\<lfloor>t\<rfloor> \<star> \<lfloor>u\<rfloor>\<rfloor>" using assms Nmlize_Nmlize by simp
lemma Nmlize_Hcomp_Obj_Arr [simp]: assumes"Arr u" shows"\<lfloor>\<langle>b\<rangle>0\<star> u\<rfloor> = \<lfloor>u\<rfloor>" using assms by simp
lemma Nmlize_Hcomp_Arr_Obj [simp]: assumes"Arr t"and"Src t = \<langle>a\<rangle>0" shows"\<lfloor>t \<star> \<langle>a\<rangle>0\<rfloor> = \<lfloor>t\<rfloor>" using assms HcompNml_Nml_Src Nmlize_in_Hom by simp
lemma Nmlize_Hcomp_Prim_Arr [simp]: assumes"Arr u"and"¬ is_Prim0\<lfloor>u\<rfloor>" shows"\<lfloor>\<langle>μ\<rangle> \<star> u\<rfloor> = \<langle>μ\<rangle> \<star> \<lfloor>u\<rfloor>" using assms by simp
lemma Nmlize_Hcomp_Hcomp: assumes"Arr t"and"Arr u"and"Arr v"and"Src t = Trg u"and"Src u = Trg v" shows"\<lfloor>(t \<star> u) \<star> v\<rfloor> = \<lfloor>\<lfloor>t\<rfloor> \<star> (\<lfloor>u\<rfloor> \<star> \<lfloor>v\<rfloor>)\<rfloor>" using assms Nml_Nmlize Nmlize_Nmlize by (simp add: HcompNml_assoc)
lemma Nmlize_Hcomp_Hcomp': assumes"Arr t"and"Arr u"and"Arr v"and"Src t = Trg u"and"Src u = Trg v" shows"\<lfloor>t \<star> u \<star> v\<rfloor> = \<lfloor>\<lfloor>t\<rfloor> \<star> \<lfloor>u\<rfloor> \<star> \<lfloor>v\<rfloor>\<rfloor>" using assms Nml_Nmlize Nmlize_Nmlize by (simp add: HcompNml_assoc)
lemma Nmlize_Vcomp_Cod_Arr: assumes"Arr t" shows"\<lfloor>Cod t \<cdot> t\<rfloor> = \<lfloor>t\<rfloor>" proof - have"Arr t ==>\<lfloor>Cod t \<cdot> t\<rfloor> = \<lfloor>t\<rfloor>" proof (induct t, simp_all) show"∧x. arr x ==> cod x ⋅ x = x" using comp_cod_arr by blast fix t1 t2 show"∧t1 t2. \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t2\<rfloor> ==> HSeq t1 t2 ==> (\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) = \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>" using VcompNml_HcompNml Ide_Cod Nml_Nmlize Nmlize_in_Hom by simp show"\<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> =\<lfloor>t2\<rfloor> ==> VSeq t1 t2 ==> \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor>" using VcompNml_assoc [of "\<lfloor>Cod t1\<rfloor>""\<lfloor>t1\<rfloor>""\<lfloor>t2\<rfloor>"] Ide_Cod
Nml_Nmlize by simp next show"∧t. \<lfloor>Cod t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==> (\<lfloor>Trg t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t\<rfloor>) \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor>" by (metis Arr.simps(6) Cod.simps(6) Nmlize.simps(3) Nmlize.simps(6)
Nmlize_Cod) show"∧t. \<lfloor>Cod t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==> (\<lfloor>Cod t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Src t\<rfloor>) \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor>" by (simp add: Nml_Nmlize(1) Nml_Nmlize(2) Nmlize_Src(2) HcompNml_Nml_Obj) show"∧t1 t2 t3. \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t2\<rfloor> ==> \<lfloor>Cod t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t3\<rfloor> = \<lfloor>t3\<rfloor> ==> Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==> (\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> ((\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) = (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>" using VcompNml_HcompNml Ide_Cod HcompNml_in_Hom Nml_HcompNml
Nml_Nmlize Nmlize_in_Hom HcompNml_assoc by simp show"∧t1 t2 t3. \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t2\<rfloor> ==> \<lfloor>Cod t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t3\<rfloor> = \<lfloor>t3\<rfloor> ==> Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==> ((\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>Cod t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>t1\<rfloor>\<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) = \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>" using VcompNml_HcompNml Ide_Cod HcompNml_in_Hom Nml_HcompNml
Nml_Nmlize Nmlize_in_Hom HcompNml_assoc by simp qed thus ?thesis using assms by blast qed
lemma Nmlize_Vcomp_Arr_Dom: assumes"Arr t" shows"\<lfloor>t \<cdot> Dom t\<rfloor> = \<lfloor>t\<rfloor>" proof - have"Arr t ==>\<lfloor>t \<cdot> Dom t\<rfloor> = \<lfloor>t\<rfloor>" proof (induct t, simp_all) show"∧x. arr x ==> x ⋅ local.dom x = x" using comp_arr_dom by blast fix t1 t2 show"\<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t1\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> =\<lfloor>t2\<rfloor> ==> HSeq t1 t2 ==> (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor>) = \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>" using VcompNml_HcompNml Ide_Dom HcompNml_in_Hom Nml_HcompNml
Nml_Nmlize Nmlize_in_Hom HcompNml_assoc by simp show"\<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Cod t2\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> =\<lfloor>t2\<rfloor> ==> VSeq t1 t2 ==> (\<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor>" using VcompNml_assoc [of "\<lfloor>t1\<rfloor>""\<lfloor>t2\<rfloor>""\<lfloor>Dom t2\<rfloor>"] Ide_Dom Nml_Nmlize by simp next show"∧t. \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==>\<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> (\<lfloor>Trg t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t\<rfloor>) = \<lfloor>t\<rfloor>" by (simp add: Nml_Nmlize(1) Nml_Nmlize(3) Nmlize_Trg(2)
HcompNml_Obj_Nml bicategorical_language.Ide_Dom
bicategorical_language_axioms) show"∧t. \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==>\<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> (\<lfloor>Dom t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Src t\<rfloor>) = \<lfloor>t\<rfloor>" by (simp add: Nml_Nmlize(1) Nml_Nmlize(2) Nmlize_Src(2) HcompNml_Nml_Obj) show"∧t1 t2 t3. \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t1\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t2\<rfloor> ==> \<lfloor>t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t3\<rfloor> = \<lfloor>t3\<rfloor> ==> Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==> ((\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> ((\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>Dom t3\<rfloor>) = (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>" using VcompNml_HcompNml Ide_Dom HcompNml_in_Hom Nml_HcompNml
Nml_Nmlize Nmlize_in_Hom HcompNml_assoc by simp show"∧t1 t2 t3. \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t1\<rfloor> = \<lfloor>t1\<rfloor> ==>\<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t2\<rfloor> ==> \<lfloor>t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t3\<rfloor> = \<lfloor>t3\<rfloor> ==> Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==> (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t3\<rfloor>) = \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>" using VcompNml_HcompNml Ide_Dom HcompNml_in_Hom Nml_HcompNml
Nml_Nmlize Nmlize_in_Hom HcompNml_assoc by simp qed thus ?thesis using assms by blast qed
lemma Nmlize_Inv: assumes"Can t" shows"\<lfloor>Inv t\<rfloor> = Inv \<lfloor>t\<rfloor>" proof - have"Can t ==>\<lfloor>Inv t\<rfloor> = Inv \<lfloor>t\<rfloor>" proof (induct t, simp_all) fix u v assume I1: "\<lfloor>Inv u\<rfloor> = Inv \<lfloor>u\<rfloor>" assume I2: "\<lfloor>Inv v\<rfloor> = Inv \<lfloor>v\<rfloor>" show"Can u ∧ Can v ∧ Src u = Trg v ==> Inv \<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> Inv \<lfloor>v\<rfloor> = Inv (\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>)" using Inv_HcompNml Nml_Nmlize Can_implies_Arr Can_Nmlize_Can
I1 I2 by simp show"Can u ∧ Can v ∧ Dom u = Cod v ==> Inv \<lfloor>v\<rfloor> \<lfloor>\<cdot>\<rfloor> Inv \<lfloor>u\<rfloor> = Inv (\<lfloor>u\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>v\<rfloor>)" using Inv_VcompNml Nml_Nmlize Can_implies_Arr Nmlize_in_Hom Can_Nmlize_Can
I1 I2 by simp fix w assume I3: "\<lfloor>Inv w\<rfloor> = Inv \<lfloor>w\<rfloor>" assume uvw: "Can u ∧ Can v ∧ Can w ∧ Src u = Trg v ∧ Src v = Trg w" show"Inv \<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> (Inv \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> Inv \<lfloor>w\<rfloor>) = Inv ((\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>)" using uvw I1 I2 I3
Inv_HcompNml Nml_Nmlize Can_implies_Arr Can_Nmlize_Can
Nml_HcompNml Can_HcompNml HcompNml_assoc by simp show"(Inv \<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> Inv \<lfloor>v\<rfloor>) \<lfloor>\<star>\<rfloor> Inv \<lfloor>w\<rfloor> = Inv (\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> (\<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>))" using uvw I1 I2 I3
Inv_HcompNml Nml_Nmlize Can_implies_Arr Can_Nmlize_Can
Nml_HcompNml Can_HcompNml HcompNml_assoc Can_Inv by simp qed thus ?thesis using assms by blast qed
subsection"Reductions"
text‹
Function ‹red› defined below takes a formal identity @{term t} to a canonical arrow ‹f\↓∈ Hom f \⌊f\⌋›. The auxiliary function ‹red2› takes a pair @{term "(f, g)"}
of normalized formal identities and produces a canonical arrow ‹f \⇓ g ∈ Hom (f \⋆ g) \⌊f \⋆ g\⌋›. ›
fun red2 (infixr‹\⇓›53) where"\<langle>b\<rangle>0\<Down> u = \<l>[u]"
| "\<langle>f\<rangle> \<Down> \<langle>a\<rangle>0 = \<r>[\<langle>f\<rangle>]"
| "\<langle>f\<rangle> \<Down> u = \<langle>f\<rangle> \<star> u"
| "(t \<star> u) \<Down> \<langle>a\<rangle>0 = \<r>[t \<star> u]"
| "(t \<star> u) \<Down> v = (t \<Down> \<lfloor>u \<star> v\<rfloor>) \<cdot> (t \<star> (u \<Down> v)) \<cdot> \<a>[t, u, v]"
| "t \<Down> u = undefined"
fun red (‹_\↓› [56] 56) where"\<langle>f\<rangle>0\<down> = \<langle>f\<rangle>0"
| "\<langle>f\<rangle>\<down> = \<langle>f\<rangle>"
| "(t \<star> u)\<down> = (if Nml (t \<star> u) then t \<star> u else (\<lfloor>t\<rfloor> \<Down> \<lfloor>u\<rfloor>) \<cdot> (t\<down> \<star> u\<down>))"
| "t\<down> = undefined"
lemma red_Nml [simp]: assumes"Nml a" shows"a\<down> = a" using assms by (cases a, simp_all)
lemma red2_Nml: assumes"Nml (a \<star> b)" shows"a \<Down> b = a \<star> b" proof - have a: "a = \<langle>un_Prim a\<rangle>" using assms Nml_HcompD by metis have b: "Nml b ∧¬ is_Prim0 b" using assms Nml_HcompD by metis show ?thesis using a b apply (cases b) apply simp_all apply (metis red2.simps(3)) by (metis red2.simps(4)) qed
lemma Can_red2: assumes"Ide a"and"Nml a"and"Ide b"and"Nml b"and"Src a = Trg b" shows"Can (a \<Down> b)" and"a \<Down> b ∈ VHom (a \<star> b) \<lfloor>a \<star> b\<rfloor>" proof - have0: "∧b. [ Ide a ∧ Nml a; Ide b ∧ Nml b; Src a = Trg b ]==> Can (a \<Down> b) ∧ a \<Down> b ∈ VHom (a \<star> b) \<lfloor>a \<star> b\<rfloor>" proof (induct a, simp_all add: HcompNml_Nml_Src HcompNml_Trg_Nml) fix x b show"Ide b ∧ Nml b ==> Can (Trg b \<Down> b) ∧ Arr (Trg b \<Down> b) ∧ Dom (Trg b \<Down> b) = Trg b \<star> b ∧ Cod (Trg b \<Down> b) = b" using Ide_implies_Can Ide_in_Hom Nmlize_Nml apply (cases b, simp_all) proof - fix u v assume uv: "Ide u ∧ Ide v ∧ Src u = Trg v ∧ Nml (u \<star> v)" show"Can (Trg u \<Down> (u \<star> v)) ∧ Arr (Trg u \<Down> (u \<star> v)) ∧ Dom (Trg u \<Down> (u \<star> v)) = Trg u \<star> u \<star> v ∧ Cod (Trg u \<Down> (u \<star> v)) = u \<star> v" using uv Ide_implies_Can Can_implies_Arr Ide_in_Hom by (cases u, simp_all) qed show"ide x ∧ arr x ==> Ide b ∧ Nml b ==>\<langle>src x\<rangle>0 = Trg b ==> Can (\<langle>x\<rangle> \<Down> b) ∧ Arr (\<langle>x\<rangle> \<Down> b) ∧ Dom (\<langle>x\<rangle> \<Down> b) = \<langle>x\<rangle> \<star> b ∧ Cod (\<langle>x\<rangle> \<Down> b) = \<langle>x\<rangle> \<lfloor>\<star>\<rfloor> b" using Ide_implies_Can Can_implies_Arr Nmlize_Nml Ide_in_Hom by (cases b, simp_all) next fix u v w assume uv: "Ide u ∧ Ide v ∧ Src u = Trg v ∧ Nml (u \<star> v)" assume vw: "Src v = Trg w" assume w: "Ide w ∧ Nml w" assume I1: "∧w. [ Nml u; Ide w ∧ Nml w; Trg v = Trg w ]==> Can (u \<Down> w) ∧ Arr (u \<Down> w) ∧ Dom (u \<Down> w) = u \<star> w ∧ Cod (u \<Down> w) = u \<lfloor>\<star>\<rfloor> w" assume I2: "∧x. [ Nml v; Ide x ∧ Nml x; Trg w = Trg x ]==> Can (v \<Down> x) ∧ Arr (v \<Down> x) ∧ Dom (v \<Down> x) = v \<star> x ∧ Cod (v \<Down> x) = v \<lfloor>\<star>\<rfloor> x" show"Can ((u \<star> v) \<Down> w) ∧ Arr ((u \<star> v) \<Down> w) ∧ Dom ((u \<star> v) \<Down> w) = (u \<star> v) \<star> w ∧ Cod ((u \<star> v) \<Down> w) = (\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>) \<lfloor>\<star>\<rfloor> w" proof - have u: "Nml u ∧ Ide u" using uv Nml_HcompD by blast have v: "Nml v ∧ Ide v" using uv Nml_HcompD by blast have"is_Prim0 w ==> ?thesis" proof - assume1: "is_Prim0 w" have2: "(u \<star> v) \<Down> w = \<r>[u \<star> v]" using1by (cases w, simp_all) have3: "Can (u \<Down> v) ∧ Arr (u \<Down> v) ∧ Dom (u \<Down> v) = u \<star> v ∧ Cod (u \<Down> v) = u \<star> v" using u v uv 12 I1 Nmlize_Nml Nmlize.simps(3) by metis hence4: "VSeq (u \<Down> v) \<r>[u \<star> v]" using uv by (metis (mono_tags, lifting) Arr.simps(7) Cod.simps(3) Cod.simps(7)
Nml_implies_Arr Ide_in_Hom(2) mem_Collect_eq) have"Can ((u \<star> v) \<Down> w)" using1234 uv by (simp add: Ide_implies_Can) moreoverhave"Dom ((u \<star> v) \<Down> w) = (u \<star> v) \<star> w" using1234 u v w uv vw I1 Ide_in_Hom Nml_HcompNml Ide_in_Hom apply (cases w) by simp_all moreoverhave"Cod ((u \<star> v) \<Down> w) = \<lfloor>(u \<star> v) \<star> w\<rfloor>" using1234 uv using Nmlize_Nml apply (cases w, simp_all) by (metis Nmlize.simps(3) Nmlize_Nml HcompNml.simps(3)) ultimatelyshow ?thesis using w Can_implies_Arr by (simp add: 1 uv) qed moreoverhave"¬ is_Prim0 w ==> ?thesis" proof - assume1: "¬ is_Prim0 w" have2: "(u \<star> v) \<Down> w = (u \<Down> \<lfloor>v \<star> w\<rfloor>) \<cdot> (u \<star> v \<Down> w) \<cdot> \<a>[u, v, w]" using1 u v uv w by (cases w; simp) have3: "Can (u \<Down> \<lfloor>v \<star> w\<rfloor>) ∧ Dom (u \<Down> \<lfloor>v \<star> w\<rfloor>) = u \<star> \<lfloor>v \<star> w\<rfloor> ∧ Cod (u \<Down> \<lfloor>v \<star> w\<rfloor>) = \<lfloor>u \<star> (v \<star> w)\<rfloor>" proof - have"Can (u \<Down> \<lfloor>v \<star> w\<rfloor>) ∧ Dom (u \<Down> \<lfloor>v \<star> w\<rfloor>) = u \<star> \<lfloor>v \<star> w\<rfloor> ∧ Cod (u \<Down> \<lfloor>v \<star> w\<rfloor>) = u \<lfloor>\<star>\<rfloor> \<lfloor>v \<star> w\<rfloor>" using w uv Ide_HcompNml Nml_HcompNml(1) apply (cases u, simp_all) using u v vw I1 Nmlize_in_Hom(1) [of "v \<star> w"] Nml_Nmlize Ide_Nmlize_Ide by simp moreoverhave"u \<lfloor>\<star>\<rfloor> \<lfloor>v \<star> w\<rfloor> = \<lfloor>u \<star> (v \<star> w)\<rfloor>" using uv u w Nmlize_Hcomp Nmlize_Nmlize Nml_implies_Arr by simp ultimatelyshow ?thesis by presburger qed have4: "Can (v \<Down> w) ∧ Dom (v \<Down> w) = v \<star> w ∧ Cod (v \<Down> w) = \<lfloor>v \<star> w\<rfloor>" using v w vw 12 I2 by simp hence5: "Src (v \<Down> w) = Src w ∧ Trg (v \<Down> w) = Trg v" using Src_Dom Trg_Dom Can_implies_Arr by fastforce have"Can (u \<star> (v \<Down> w)) ∧ Dom (u \<star> (v \<Down> w)) = u \<star> (v \<star> w) ∧ Cod (u \<star> (v \<Down> w)) = u \<star> \<lfloor>v \<star> w\<rfloor>" using u uv vw 45 Ide_implies_Can Ide_in_Hom by simp moreoverhave"\<lfloor>u \<star> \<lfloor>v \<star> w\<rfloor>\<rfloor> = \<lfloor>u \<star> v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>" proof - have"\<lfloor>u \<star> \<lfloor>v \<star> w\<rfloor>\<rfloor> = u \<lfloor>\<star>\<rfloor> (v \<lfloor>\<star>\<rfloor> w)" using u v w 4 by (metis Ide_Dom Can_implies_Arr Ide_implies_Arr
Nml_Nmlize(1) Nmlize.simps(3) Nmlize_Nml) alsohave"... = (u \<lfloor>\<star>\<rfloor> v) \<lfloor>\<star>\<rfloor> w" using u v w uv vw HcompNml_assoc by metis alsohave"... = \<lfloor>u \<star> v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>" using u v w by (metis Nmlize.simps(3) Nmlize_Nml) finallyshow ?thesis by blast qed moreoverhave"Can \<a>[u, v, w]∧ Dom \<a>[u, v, w] = (u \<star> v) \<star> w ∧ Cod \<a>[u, v, w] = u \<star> (v \<star> w)" using uv vw w Ide_implies_Can Ide_in_Hom by auto ultimatelyshow ?thesis using uv w 234 Nml_implies_Arr Nmlize_Nmlize Ide_implies_Can
Nmlize_Nml Ide_Dom Can_implies_Arr by (metis Can.simps(4) Cod.simps(4) Dom.simps(4) Nmlize.simps(3)) qed ultimatelyshow ?thesis by blast qed qed show"Can (a \<Down> b)"using assms 0by blast show"a \<Down> b ∈ VHom (a \<star> b) \<lfloor>a \<star> b\<rfloor>"using0 assms by blast qed
lemma red2_in_Hom [intro]: assumes"Ide u"and"Nml u"and"Ide v"and"Nml v"and"Src u = Trg v" shows"u \<Down> v ∈ HHom (Src v) (Trg u)"and"u \<Down> v ∈ VHom (u \<star> v) \<lfloor>u \<star> v\<rfloor>" proof - show1: "u \<Down> v ∈ VHom (u \<star> v) \<lfloor>u \<star> v\<rfloor>" using assms Can_red2 Can_implies_Arr by simp show"u \<Down> v ∈ HHom (Src v) (Trg u)" using assms 1 Src_Dom [of "u \<Down> v"] Trg_Dom [of "u \<Down> v"] Can_red2 Can_implies_Arr by simp qed
lemma red2_simps [simp]: assumes"Ide u"and"Nml u"and"Ide v"and"Nml v"and"Src u = Trg v" shows"Src (u \<Down> v) = Src v"and"Trg (u \<Down> v) = Trg u" and"Dom (u \<Down> v) = u \<star> v"and"Cod (u \<Down> v) = \<lfloor>u \<star> v\<rfloor>" using assms red2_in_Hom by auto
lemma Can_red: assumes"Ide u" shows"Can (u\<down>)"and"u\<down> ∈ VHom u \<lfloor>u\<rfloor>" proof - have0: "Ide u ==> Can (u\<down>) ∧ u\<down> ∈ VHom u \<lfloor>u\<rfloor>" proof (induct u, simp_all add: Dom_Ide Cod_Ide) fix v w assume v: "Can (v\<down>) ∧ Arr (v\<down>) ∧ Dom (v\<down>) = v ∧ Cod (v\<down>) = \<lfloor>v\<rfloor>" assume w: "Can (w\<down>) ∧ Arr (w\<down>) ∧ Dom (w\<down>) = w ∧ Cod (w\<down>) = \<lfloor>w\<rfloor>" assume vw: "Ide v ∧ Ide w ∧ Src v = Trg w" show"(Nml (v \<star> w) ⟶ Can v ∧ Can w ∧ v \<star> w = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>) ∧ (¬ Nml (v \<star> w) ⟶ Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>)∧ Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Arr (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧ Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>)" proof show"Nml (v \<star> w) ⟶ Can v ∧ Can w ∧ v \<star> w = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>" using vw Nml_HcompD Ide_implies_Can Dom_Inv VcompNml_Ide_Nml Inv_Ide
Nmlize.simps(3) Nmlize_Nml by metis show"¬ Nml (v \<star> w) ⟶ Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>)∧ Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Arr (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧ Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>" proof assume1: "¬ Nml (v \<star> w)" have"Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>)" using v w vw Can_red2 Nml_Nmlize Ide_Nmlize_Ide Nml_HcompNml Ide_HcompNml by simp moreoverhave"Src (v\<down>) = Trg (w\<down>)" using v w vw Src_Dom Trg_Dom by metis moreoverhave"Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>" using v w vw Can_red2 Nml_Nmlize Ide_Nmlize_Ide by simp ultimatelyshow"Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧ Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Arr (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧ Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>" using Can_implies_Arr by blast qed qed qed show"Can (u\<down>)"using assms 0by blast show"u\<down> ∈ VHom u \<lfloor>u\<rfloor>"using assms 0by blast qed
lemma red_in_Hom [intro]: assumes"Ide t" shows"t\<down> ∈ HHom (Src t) (Trg t)"and"t\<down> ∈ VHom t \<lfloor>t\<rfloor>" proof - show1: "t\<down> ∈ VHom t \<lfloor>t\<rfloor>" using assms Can_red Can_implies_Arr by simp show"t\<down> ∈ HHom (Src t) (Trg t)" using assms 1 Src_Dom [of "t\<down>"] Trg_Dom [of "t\<down>"] Can_red Can_implies_Arr by simp qed
lemma red_simps [simp]: assumes"Ide t" shows"Src (t\<down>) = Src t"and"Trg (t\<down>) = Trg t" and"Dom (t\<down>) = t"and"Cod (t\<down>) = \<lfloor>t\<rfloor>" using assms red_in_Hom by auto
lemma red_Src: assumes"Ide t" shows"Src t\<down> = Src t" using assms is_Prim0_Src [of t] by (cases "Src t", simp_all)
lemma red_Trg: assumes"Ide t" shows"Trg t\<down> = Trg t" using assms is_Prim0_Trg [of t] by (cases "Trg t", simp_all)
lemma Nmlize_red [simp]: assumes"Ide t" shows"\<lfloor>t\<down>\<rfloor> = \<lfloor>t\<rfloor>" using assms Can_red Ide_Nmlize_Can Nmlize_in_Hom Ide_in_Hom by fastforce
lemma Nmlize_red2 [simp]: assumes"Ide t"and"Ide u"and"Nml t"and"Nml u"and"Src t = Trg u" shows"\<lfloor>t \<Down> u\<rfloor> = \<lfloor>t \<star> u\<rfloor>" using assms Can_red2 Ide_Nmlize_Can Nmlize_in_Hom [of "t \<Down> u"] red2_in_Hom Ide_in_Hom by simp
end
subsection"Evaluation"
text‹
The following locale is concerned with the evaluation of terms of the bicategorical
language determined by ‹C›, ‹srcC›, and ‹trgC› in a bicategory ‹(V, H, a, i, src, trg)›,
given a source and target-preserving functor from ‹C› to ‹V›. ›
locale evaluation_map =
C: horizontal_homs C srcC trgC +
bicategorical_language C srcC trgC +
bicategory V H ai src trg +
E: "functor" C V E for C :: "'c comp" (infixr‹⋅C›55) and srcC :: "'c ==> 'c" and trgC :: "'c ==> 'c" and V :: "'b comp" (infixr‹⋅›55) and H :: "'b comp" (infixr‹⋆›53) anda :: "'b ==> 'b ==> 'b ==> 'b" (‹a[_, _, _]›) andi :: "'b ==> 'b" (‹i[_]›) and src :: "'b ==> 'b" and trg :: "'b ==> 'b" and E :: "'c ==> 'b" + assumes preserves_src: "E (srcC x) = src (E x)" and preserves_trg: "E (trgC x) = trg (E x)" begin
(* TODO: Figure out why this notation has to be reinstated. *) notation Nmlize (‹\⌊_\⌋›) notation HcompNml (infixr‹\⌊\⋆\⌋›53) notation VcompNml (infixr‹\⌊\⋅\⌋›55) notation red (‹_\↓› [56] 56) notation red2 (infixr‹\⇓›53)
lemma preserves_obj: assumes"C.obj a" shows"obj (E a)" proof (unfold obj_def) show"arr (E a) ∧ src (E a) = E a" proof show"arr (E a)"using assms C.obj_simps by simp have"src (E a) = E (srcC a)" using assms preserves_src by metis alsohave"... = E a" using assms C.obj_simps by simp finallyshow"src (E a) = E a"by simp qed qed
lemma eval_in_hom': shows"Arr t ==>«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬" proof (induct t) show"∧x. Arr \<langle>x\<rangle>0==> «{\<langle>x\<rangle>0} : {Src \<langle>x\<rangle>0}→{Trg \<langle>x\<rangle>0}¬∧«{\<langle>x\<rangle>0} : {Dom \<langle>x\<rangle>0}==>{Cod \<langle>x\<rangle>0}¬" apply (simp add: preserves_src preserves_trg) using preserves_src preserves_trg C.objE by (metis (full_types) C.obj_def' E.preserves_arr E.preserves_ide in_hhom_def
ide_in_hom(2)) show"∧x. Arr \<langle>x\<rangle> ==> «{\<langle>x\<rangle>} : {Src \<langle>x\<rangle>}→{Trg \<langle>x\<rangle>}¬∧«{\<langle>x\<rangle>} : {Dom \<langle>x\<rangle>}==>{Cod \<langle>x\<rangle>}¬" by (auto simp add: preserves_src preserves_trg) show"∧t1 t2. (Arr t1 ==>«{t1} : {Src t1}→{Trg t1}¬∧«{t1} : {Dom t1}==>{Cod t1}¬) ==> (Arr t2 ==>«{t2} : {Src t2}→{Trg t2}¬∧«{t2} : {Dom t2}==>{Cod t2}¬) ==> Arr (t1 \<star> t2) ==> «{t1 \<star> t2} : {Src (t1 \<star> t2)}→{Trg (t1 \<star> t2)}¬∧ «{t1 \<star> t2} : {Dom (t1 \<star> t2)}==>{Cod (t1 \<star> t2)}¬" using hcomp_in_hhom in_hhom_def vconn_implies_hpar(1) vconn_implies_hpar(2) by auto show"∧t1 t2. (Arr t1 ==>«{t1} : {Src t1}→{Trg t1}¬∧«{t1} : {Dom t1}==>{Cod t1}¬) ==> (Arr t2 ==>«{t2} : {Src t2}→{Trg t2}¬∧«{t2} : {Dom t2}==>{Cod t2}¬) ==> Arr (t1 \<cdot> t2) ==> «{t1 \<cdot> t2} : {Src (t1 \<cdot> t2)}→{Trg (t1 \<cdot> t2)}¬∧ «{t1 \<cdot> t2} : {Dom (t1 \<cdot> t2)}==>{Cod (t1 \<cdot> t2)}¬" using VSeq_implies_HPar seqI' by auto show"∧t. (Arr t ==>«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬) ==> Arr \<l>[t]==> «{\<l>[t]} : {Src \<l>[t]}→{Trg \<l>[t]}¬∧«{\<l>[t]} : {Dom \<l>[t]}==>{Cod \<l>[t]}¬" proof (simp add: preserves_src preserves_trg) fix t assume t: "«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬" assume1: "Arr t" show"«l{t} : {Src t}→{Trg t}¬∧«l{t} : {Trg t}⋆{Dom t}==>{Cod t}¬" proof - have"src (l{t}) = {Src t}" using t 1 by (metis (no_types, lifting) l.preserves_cod arr_cod in_hhomE map_simp src_cod) moreoverhave"trg (l{t}) = {Trg t}" using t 1 by (metis (no_types, lifting) l.preserves_cod arr_cod in_hhomE map_simp trg_cod) moreoverhave"«l{t} : {Trg t}⋆{Dom t}==>{Cod t}¬" using t 1 apply (elim conjE in_hhomE) by (intro in_homI, auto) ultimatelyshow ?thesis by auto qed qed show"∧t. (Arr t ==>«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬) ==> Arr \<l>-1[t]==> «{\<l>-1[t]} : {Src \<l>-1[t]}→{Trg \<l>-1[t]}¬∧ «{\<l>-1[t]} : {Dom \<l>-1[t]}==>{Cod \<l>-1[t]}¬" proof (simp add: preserves_src preserves_trg) fix t assume t: "«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬" assume1: "Arr t" show"«l'.map {t} : {Src t}→{Trg t}¬∧ «l'.map {t} : {Dom t}==>{Trg t}⋆{Cod t}¬" proof - have"src (l'.map {t}) = {Src t}" using t 1l'.preserves_dom arr_dom map_simp l'.preserves_reflects_arr src_dom by (metis (no_types, lifting) in_hhomE) moreoverhave"trg (l'.map {t}) = {Trg t}" using t 1l'.preserves_dom arr_dom map_simp l'.preserves_reflects_arr trg_dom by (metis (no_types, lifting) in_hhomE) moreoverhave"«l'.map {t} : {Dom t}==>{Trg t}⋆{Cod t}¬" using t 1l'.preserves_hom apply (intro in_homI) apply auto[1] apply fastforce by fastforce ultimatelyshow ?thesis by blast qed qed show"∧t. (Arr t ==>«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬) ==> Arr \<r>[t]==> «{\<r>[t]} : {Src \<r>[t]}→{Trg \<r>[t]}¬∧«{\<r>[t]} : {Dom \<r>[t]}==>{Cod \<r>[t]}¬" proof (simp add: preserves_src preserves_trg) fix t assume t: "«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬" assume1: "Arr t" show"«r{t} : {Src t}→{Trg t}¬∧«r{t} : {Dom t}⋆{Src t}==>{Cod t}¬" proof - have"src (r{t}) = {Src t}" using t 1r.preserves_cod arr_cod map_simp r.preserves_reflects_arr src_cod by (metis (no_types, lifting) in_hhomE) moreoverhave"trg (r{t}) = {Trg t}" using t 1r.preserves_cod arr_cod map_simp r.preserves_reflects_arr trg_cod by (metis (no_types, lifting) in_hhomE) moreoverhave"«r{t} : {Dom t}⋆{Src t}==>{Cod t}¬" using t 1by force ultimatelyshow ?thesis by blast qed qed show"∧t. (Arr t ==>«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬) ==> Arr \<r>-1[t]==> «{\<r>-1[t]} : {Src \<r>-1[t]}→{Trg \<r>-1[t]}¬∧ «{\<r>-1[t]} : {Dom \<r>-1[t]}==>{Cod \<r>-1[t]}¬" proof (simp add: preserves_src preserves_trg) fix t assume t: "«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬" assume1: "Arr t" show"«r'.map {t} : {Src t}→{Trg t}¬∧ «r'.map {t} : {Dom t}==>{Cod t}⋆{Src t}¬" proof - have"src (r'.map {t}) = {Src t}" using t 1r'.preserves_dom arr_dom map_simp r'.preserves_reflects_arr src_dom by (metis (no_types, lifting) in_hhomE) moreoverhave"trg (r'.map {t}) = {Trg t}" using t 1r'.preserves_dom arr_dom map_simp r'.preserves_reflects_arr trg_dom by (metis (no_types, lifting) in_hhomE) moreoverhave"«r'.map {t} : {Dom t}==>{Cod t}⋆{Src t}¬" using t 1 src_cod arr_cod r'.preserves_hom [of "{t}""{Dom t}""{Cod t}"] apply (elim conjE in_hhomE) by (intro in_homI, auto) ultimatelyshow ?thesis by blast qed qed show"∧t u v. (Arr t ==>«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬) ==> (Arr u ==>«{u} : {Src u}→{Trg u}¬∧«{u} : {Dom u}==>{Cod u}¬) ==> (Arr v ==>«{v} : {Src v}→{Trg v}¬∧«{v} : {Dom v}==>{Cod v}¬) ==> Arr \<a>[t, u, v]==> «{\<a>[t, u, v]} : {Src \<a>[t, u, v]}→{Trg \<a>[t, u, v]}¬∧ «{\<a>[t, u, v]} : {Dom \<a>[t, u, v]}==>{Cod \<a>[t, u, v]}¬" proof (simp add: preserves_src preserves_trg) fix t u v assume t: "«{t} : {Trg u}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬" assume u: "«{u} : {Trg v}→{Trg u}¬∧«{u} : {Dom u}==>{Cod u}¬" assume v: "«{v} : {Src v}→{Trg v}¬∧«{v} : {Dom v}==>{Cod v}¬" assume tuv: "Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v" show"«α ({t}, {u}, {v}) : {Src v}→{Trg t}¬∧ «α ({t}, {u}, {v}) : ({Dom t}⋆{Dom u}) ⋆{Dom v}==>{Cod t}⋆{Cod u}⋆{Cod v}¬" proof - have1: "VVV.in_hom ({t}, {u}, {v}) ({Dom t}, {Dom u}, {Dom v}) ({Cod t}, {Cod u}, {Cod v})" proof - have"({t}, {u}, {v}) ∈ VxVxV.hom ({Dom t}, {Dom u}, {Dom v}) ({Cod t}, {Cod u}, {Cod v})" using t u v tuv by simp moreoverhave"({t}, {u}, {v}) ∈ {τμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧ src (fst τμν) = trg (fst (snd τμν))}" using t u v tuv by fastforce ultimatelyshow ?thesis using VVV.hom_char
[of "({Dom t}, {Dom u}, {Dom v})""({Cod t}, {Cod u}, {Cod v})"] by blast qed have4: "VVV.arr ({Dom t}, {Dom u}, {Dom v})" using1 VVV.ide_dom VVV.dom_simp by (elim VVV.in_homE) force have5: "VVV.arr ({Cod t}, {Cod u}, {Cod v})" using1 VVV.ide_cod VVV.cod_simp VVV.in_hom_charSbCby blast have2: "«α ({t}, {u}, {v}) : ({Dom t}⋆{Dom u}) ⋆{Dom v}==>{Cod t}⋆{Cod u}⋆{Cod v}¬" using145 HoHV_def HoVH_def α_def
α.preserves_hom [of "({t}, {u}, {v})""({Dom t}, {Dom u}, {Dom v})" "({Cod t}, {Cod u}, {Cod v})"] by simp have3: "«α ({t}, {u}, {v}) : {Src v}→{Trg t}¬" proof show"arr (α ({t}, {u}, {v}))" using2by auto show"src (α ({t}, {u}, {v})) = {Src v}" proof - have"src (α ({t}, {u}, {v})) = src (({Dom t}⋆{Dom u}) ⋆{Dom v})" using2 src_dom [of "α ({t}, {u}, {v})"] by fastforce alsohave"... = src {Dom v}" using4 VVV.arr_charSbC VV.arr_charSbCby simp alsohave"... = src (dom {v})" using v by fastforce alsohave"... = {Src v}" using v by auto finallyshow ?thesis by auto qed show"trg (α ({t}, {u}, {v})) = {Trg t}" proof - have"trg (α ({t}, {u}, {v})) = trg (({Dom t}⋆{Dom u}) ⋆{Dom v})" using2 trg_dom [of "α ({t}, {u}, {v})"] by fastforce alsohave"... = trg {Dom t}" using4 VVV.arr_charSbC VV.arr_charSbCby simp alsohave"... = trg (dom {t})" using t by fastforce alsohave"... = {Trg t}" using t by auto finallyshow ?thesis by auto qed qed show ?thesis using23by simp qed qed show"∧t u v. (Arr t ==>«{t} : {Src t}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬) ==> (Arr u ==>«{u} : {Src u}→{Trg u}¬∧«{u} : {Dom u}==>{Cod u}¬) ==> (Arr v ==>«{v} : {Src v}→{Trg v}¬∧«{v} : {Dom v}==>{Cod v}¬) ==> Arr \<a>-1[t, u, v]==> «{\<a>-1[t, u, v]} : {Src \<a>-1[t, u, v]}→{Trg \<a>-1[t, u, v]}¬∧ «{\<a>-1[t, u, v]} : {Dom \<a>-1[t, u, v]}==>{Cod \<a>-1[t, u, v]}¬" proof (simp add: preserves_src preserves_trg) fix t u v assume t: "«{t} : {Trg u}→{Trg t}¬∧«{t} : {Dom t}==>{Cod t}¬" assume u: "«{u} : {Trg v}→{Trg u}¬∧«{u} : {Dom u}==>{Cod u}¬" assume v: "«{v} : {Src v}→{Trg v}¬∧«{v} : {Dom v}==>{Cod v}¬" assume tuv: "Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v" show"«α'.map ({t}, {u}, {v}) : {Src v}→{Trg t}¬∧ «α'.map ({t}, {u}, {v}) : {Dom t}⋆{Dom u}⋆{Dom v}==> ({Cod t}⋆{Cod u}) ⋆{Cod v}¬" proof - have1: "VVV.in_hom ({t}, {u}, {v}) ({Dom t}, {Dom u}, {Dom v}) ({Cod t}, {Cod u}, {Cod v})" using t u v tuv VVV.hom_char VVV.arr_charSbC VV.arr_charSbC VVV.dom_charSbC VVV.cod_charSbC apply (elim conjE in_hhomE in_homE) apply (intro VVV.in_homI) by simp_all have4: "VVV.arr ({Dom t}, {Dom u}, {Dom v})" using"1" VVV.in_hom_charSbCby blast have5: "VVV.arr ({Cod t}, {Cod u}, {Cod v})" using"1" VVV.in_hom_charSbCby blast have2: "«α'.map ({t}, {u}, {v}) : {Dom t}⋆{Dom u}⋆{Dom v}==> ({Cod t}⋆{Cod u}) ⋆{Cod v}¬" using145 HoHV_def HoVH_def α'.map_def
α'.preserves_hom [of "({t}, {u}, {v})""({Dom t}, {Dom u}, {Dom v})" "({Cod t}, {Cod u}, {Cod v})"] by simp have3: "«α'.map ({t}, {u}, {v}) : {Src v}→{Trg t}¬" proof show"arr (α'.map ({t}, {u}, {v}))" using2by auto show"src (α'.map ({t}, {u}, {v})) = {Src v}" proof - have"src (α'.map ({t}, {u}, {v})) = src ({Dom t}⋆{Dom u}⋆{Dom v})" using2 src_dom [of "α'.map ({t}, {u}, {v})"] by fastforce alsohave"... = src {Dom v}" using4 VVV.arr_charSbC VV.arr_charSbCby simp alsohave"... = src (dom {v})" using v by fastforce alsohave"... = {Src v}" using v by auto finallyshow ?thesis by auto qed show"trg (α'.map ({t}, {u}, {v})) = {Trg t}" proof - have"trg (α'.map ({t}, {u}, {v})) = trg ({Dom t}⋆{Dom u}⋆{Dom v})" using2 trg_dom [of "α'.map ({t}, {u}, {v})"] by fastforce alsohave"... = trg {Dom t}" using4 VVV.arr_charSbC VV.arr_charSbC hseqI' by simp alsohave"... = trg (dom {t})" using t by fastforce alsohave"... = {Trg t}" using t by auto finallyshow ?thesis by auto qed qed show ?thesis using23by simp qed qed qed
lemma eval_in_hom [intro]: assumes"Arr t" shows"«{t} : {Src t}→{Trg t}¬"and"«{t} : {Dom t}==>{Cod t}¬" using assms eval_in_hom' by simp_all
(* *TODO:Itseemstomethatthenaturalusefulorientationofthesefactsissyntax *tosemantics.However,havingthisasthedefaultmakesitimpossibletodovarious *proofsbysimpalone.Thishastobesortedout.Forrightnow,Iamgoingtoinclude *bothversions,whichwillhavetobeexplicitlyinvokedwhereneeded.
*) lemma eval_simps: assumes"Arr f" shows"arr {f}"and"{Src f} = src {f}"and"{Trg f} = trg {f}" and"{Dom f} = dom {f}"and"{Cod f} = cod {f}" using assms eval_in_hom [of f] by auto
lemma eval_simps': assumes"Arr f" shows"arr {f}"and"src {f} = {Src f}"and"trg {f} = {Trg f}" and"dom {f} = {Dom f}"and"cod {f} = {Cod f}" using assms eval_in_hom by auto
lemma obj_eval_Obj: shows"Obj t ==> obj {t}" using preserves_obj by (induct t) auto
lemma ide_eval_Ide: shows"Ide t ==> ide {t}" by (induct t, auto simp add: eval_simps')
lemma arr_eval_Arr [simp]: assumes"Arr t" shows"arr {t}" using assms by (simp add: eval_simps')
lemma eval_Runit' [simp]: assumes"Arr t" shows"{\<r>-1[t]} = r-1[{Cod t}] ⋅{t}" using assms r'.naturality2 r_ide_simp by (simp add: eval_simps)
lemma eval_Assoc [simp]: assumes"Arr t"and"Arr u"and"Arr v"and"Src t = Trg u"and"Src u = Trg v" shows"{\<a>[t, u, v]} = α (cod {t}, cod {u}, cod {v}) ⋅ (({t}⋆{u}) ⋆{v})" proof - have"{\<a>[t, u, v]} = α ({t}, {u}, {v})"by simp alsohave"... = α (VVV.cod ({t}, {u}, {v})) ⋅ HoHV ({t}, {u}, {v})" using assms α.naturality2 [of "({t}, {u}, {v})"] VVV.arr_charSbC VVV.cod_charSbC
α.extensionality α_def by auto alsohave"... = α (cod {t}, cod {u}, cod {v}) ⋅ (({t}⋆{u}) ⋆{v})" unfolding HoHV_def α_def using assms VVV.arr_charSbC VV.arr_charSbC VVV.cod_charSbC α.extensionality by auto finallyshow ?thesis by simp qed
lemma eval_Assoc' [simp]: assumes"Arr t"and"Arr u"and"Arr v"and"Src t = Trg u"and"Src u = Trg v" shows"{\<a>-1[t, u, v]} = a-1[cod {t}, cod {u}, cod {v}] ⋅ ({t}⋆{u}⋆{v})" proof - have"{\<a>-1[t, u, v]} = α'.map ({t}, {u}, {v})"by simp alsohave"... = α'.map (VVV.cod ({t}, {u}, {v})) ⋅ HoVH ({t}, {u}, {v})" using assms α'.naturality2 [of "({t}, {u}, {v})"] VVV.arr_charSbC VVV.cod_charSbC
α'.extensionality by simp alsohave"... = α'.map (cod {t}, cod {u}, cod {v}) ⋅ ({t}⋆{u}⋆{v})" unfolding HoVH_def using assms VVV.arr_charSbC VV.arr_charSbC VVV.cod_charSbC α'.extensionality apply simp using eval_simps'(2) eval_simps'(3) by presburger finallyshow ?thesis usinga'_defby simp qed
lemma eval_Lunit_Ide [simp]: assumes"Ide t" shows"{\<l>[t]} = l[{t}]" using assms l_ide_simp ide_eval_Ide by simp
lemma eval_Lunit'_Ide [simp]: assumes"Ide t" shows"{\<l>-1[t]} = l-1[{t}]" using assms l_ide_simp ide_eval_Ide by simp
lemma eval_Runit_Ide [simp]: assumes"Ide t" shows"{\<r>[t]} = r[{t}]" using assms r_ide_simp ide_eval_Ide by simp
lemma eval_Runit'_Ide [simp]: assumes"Ide t" shows"{\<r>-1[t]} = r-1[{t}]" using assms r_ide_simp ide_eval_Ide by simp
lemma eval_Assoc_Ide [simp]: assumes"Ide t"and"Ide u"and"Ide v"and"Src t = Trg u"and"Src u = Trg v" shows"{\<a>[t, u, v]} = α ({t}, {u}, {v})" using assms by simp
lemma eval_Assoc'_Ide [simp]: assumes"Ide t"and"Ide u"and"Ide v"and"Src t = Trg u"and"Src u = Trg v" shows"{\<a>-1[t, u, v]} = a-1[{t}, {u}, {v}]" using assms a'_defby simp
lemma iso_eval_Can: shows"Can t ==> iso {t}" proof (induct t; simp add: fsts.intros snds.intros) show"∧x. C.obj x ==> iso (E x)"by auto show"∧t1 t2. [ iso {t1}; iso {t2}; Can t1 ∧ Can t2 ∧ Src t1 = Trg t2 ]==> iso ({t1}⋆{t2})" using Can_implies_Arr by (simp add: eval_simps') show "∧t1 t2. [ iso {t1}; iso {t2}; Can t1 ∧ Can t2 ∧ Dom t1 = Cod t2 ]==> iso ({t1}⋅{t2})" using Can_implies_Arr isos_compose by (simp add: eval_simps') show "∧t. [ iso {t}; Can t ]==> iso (l{t})" using l.preserves_iso by auto show "∧t. [ iso {t}; Can t ]==> iso (l'.map {t})" using l'.preserves_iso by simp show "∧t. [ iso {t}; Can t ]==> iso (r{t})" using r.preserves_iso by auto show "∧t. [ iso {t}; Can t ]==> iso (r'.map {t})" using r'.preserves_iso by simp fix t1 t2 t3 assume t1: "iso {t1}" and t2: "iso {t2}" and t3: "iso {t3}" assume 1: "Can t1 ∧ Can t2 ∧ Can t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3" have 2: "VVV.iso ({t1}, {t2}, {t3})" proof - have 3: "VxVxV.iso ({t1}, {t2}, {t3})" using t1 t2 t3 Can_implies_Arr VxVxV.iso_char VxV.iso_char by simp moreover have "VVV.arr (VxVxV.inv ({t1}, {t2}, {t3}))" proof - have "VxVxV.inv ({t1}, {t2}, {t3}) = (inv {t1}, inv {t2}, inv {t3})" using t1 t2 t3 3 by simp thus ?thesis using t1 t2 t3 1 Can_implies_Arr VVV.arr_charSbC VV.arr_charSbC by (simp add: eval_simps') qed ultimately show ?thesis using t1 t2 t3 1 Can_implies_Arr VVV.iso_charSbC VVV.arr_charSbC by (auto simp add: eval_simps') qed show "iso (α ({t1}, {t2}, {t3}))" using 2 α_def α.preserves_iso by auto show "iso (α'.map ({t1}, {t2}, {t3}))" using 2 α'.preserves_iso by simp qed
lemma eval_Inv_Can: shows "Can t ==>{Inv t} = inv {t}" proof (induct t) show "∧x. Can \<langle>x\<rangle>0==>{Inv \<langle>x\<rangle>0} = inv {\<langle>x\<rangle>0}" by auto show "∧x. Can \<langle>x\<rangle> ==>{Inv \<langle>x\<rangle>} = inv {\<langle>x\<rangle>}" by simp show "∧t1 t2. (Can t1 ==>{Inv t1} = inv {t1}) ==> (Can t2 ==>{Inv t2} = inv {t2}) ==> Can (t1 \<star> t2) ==>{Inv (t1 \<star> t2)} = inv {t1 \<star> t2}" using iso_eval_Can Can_implies_Arr by (simp add: eval_simps') show "∧t1 t2. (Can t1 ==>{Inv t1} = inv {t1}) ==> (Can t2 ==>{Inv t2} = inv {t2}) ==> Can (t1 \<cdot> t2) ==>{Inv (t1 \<cdot> t2)} = inv {t1 \<cdot> t2}" using iso_eval_Can inv_comp Can_implies_Arr by (simp add: eval_simps') fix t assume I: "Can t ==>{Inv t} = inv {t}" show "Can \<l>[t]==>{Inv \<l>[t]} = inv {\<l>[t]}" proof - assume t: "Can \<l>[t]" have "{Inv \<l>[t]} = {\<l>-1[Inv t]}" by simp also have "... = l'.map (inv {t})" using t I by simp also have "... = l'.map (cod (inv {t})) ⋅ inv {t}" using t l'.naturality2 iso_inv_iso iso_eval_Can iso_is_arr by (metis (no_types, lifting) Can.simps(5) map_simp) also have "... = inv ({t}⋅l (dom {t}))" proof - have 1: "iso {t}" using t iso_eval_Can by simp moreover have "iso (l (dom {t}))" using t 1 l.components_are_iso ide_dom by blast moreover have "seq {t} (l (dom {t}))" using t 1 iso_is_arr by auto ultimately show ?thesis using t 1 inv_comp by auto qed also have "... = inv {\<l>[t]}" using t iso_eval_Can l_ide_simp lunit_naturality Can_implies_Arr eval_Lunit by (auto simp add: eval_simps) finally show ?thesis by blast qed show "Can \<l>-1[t]==>{Inv \<l>-1[t]} = inv {\<l>-1[t]}" proof - assume t: "Can (Lunit' t)" have "{Inv (Lunit' t)} = {Lunit (Inv t)}" by simp also have "... = l (inv {t})" using t I by simp also have "... = inv {t}⋅l (dom (inv {t}))" using t l.naturality1 iso_inv_iso iso_eval_Can iso_is_arr by (metis (no_types, lifting) Can.simps(6) map_simp) also have "... = inv (l'.map (cod {t}) ⋅{t})" proof - have 1: "iso {t}" using t iso_eval_Can by simp moreover have "iso (l'.map (cod {t}))" using t 1 l'.components_are_iso ide_cod by blast moreover have "seq (l'.map (cod {t})) {t}" using t 1 iso_is_arr by auto ultimately show ?thesis using t 1 inv_comp by auto qed also have "... = inv {\<l>-1[t]}" using t l'.naturality2 iso_eval_Can iso_is_arr by force finally show ?thesis by auto qed show "Can \<r>[t]==>{Inv \<r>[t]} = inv {\<r>[t]}" proof - assume t: "Can \<r>[t]" have "{Inv \<r>[t]} = {\<r>-1[Inv t]}" by simp also have "... = r'.map (inv {t})" using t I by simp also have "... = r'.map (cod (inv {t})) ⋅ inv {t}" using t r'.naturality2 map_simp iso_inv_iso iso_eval_Can iso_is_arr by (metis (no_types, lifting) Can.simps(7)) also have "... = inv ({t}⋅r (dom {t}))" proof - have 1: "iso {t}" using t iso_eval_Can by simp moreover have "iso (r (dom {t}))" using t 1 r.components_are_iso ide_dom by blast moreover have "seq {t} (r (dom {t}))" using t 1 iso_is_arr by simp ultimately show ?thesis using t 1 inv_comp by auto qed also have "... = inv {\<r>[t]}" using t r_ide_simp iso_eval_Can runit_naturality Can_implies_Arr eval_Runit by (auto simp add: eval_simps) finally show ?thesis by blast qed show "Can \<r>-1[t]==>{Inv \<r>-1[t]} = inv {\<r>-1[t]}" proof - assume t: "Can \<r>-1[t]" have "{Inv \<r>-1[t]} = {\<r>[Inv t]}" by simp also have "... = r (inv {t})" using t I by simp also have "... = inv {t}⋅r (dom (inv {t}))" using t r.naturality1 map_simp iso_inv_iso iso_eval_Can iso_is_arr by (metis (no_types, lifting) Can.simps(8)) also have "... = inv (r'.map (cod {t}) ⋅{t})" proof - have 1: "iso {t}" using t iso_eval_Can by simp moreover have "iso (r'.map (cod {t}))" using t 1 r'.components_are_iso ide_cod by blast moreover have "seq (r'.map (cod {t})) {t}" using t 1 iso_is_arr by auto ultimately show ?thesis using t 1 inv_comp by auto qed also have "... = inv {\<r>-1[t]}" using t r'.naturality2 iso_eval_Can iso_is_arr by auto finally show ?thesis by auto qed next fix t u v assume I1: "Can t ==>{Inv t} = inv {t}" assume I2: "Can u ==>{Inv u} = inv {u}" assume I3: "Can v ==>{Inv v} = inv {v}" show "Can \<a>[t, u, v]==>{Inv \<a>[t, u, v]} = inv {\<a>[t, u, v]}" proof - assume "Can \<a>[t, u, v]" hence tuv: "Can t ∧ Can u ∧ Can v ∧ Src t = Trg u ∧ Src u = Trg v" by simp have "{Inv \<a>[t, u, v]} = {\<a>-1[Inv t, Inv u, Inv v]}" by simp also have "... = a-1[dom {t}, dom {u}, dom {v}] ⋅ (inv {t}⋆ inv {u}⋆ inv {v})" using tuv I1 I2 I3 eval_in_hom α'.map_ide_simp inv_in_hom iso_eval_Can assoc'_naturality Can_implies_Arr Src_Inv Trg_Inv eval_Assoc' Dom_Inv Can_Inv cod_inv by presburger also have "... = inv (({t}⋆{u}⋆{v}) ⋅ α (dom {t}, dom {u}, dom {v}))" using tuv iso_eval_Can Can_implies_Arr eval_simps'(2) eval_simps'(3) α_def by (simp add: inv_comp) also have "... = inv (α ({t}, {u}, {v}))" using tuv Can_implies_Arr α_def by (metis assoc_naturality1 arr_eval_Arr eval_simps'(2) eval_simps'(3) fst_conv snd_conv) also have "... = inv {\<a>[t, u, v]}" by simp finally show ?thesis by blast qed show "Can \<a>-1[t, u, v]==>{Inv \<a>-1[t, u, v]} = inv {\<a>-1[t, u, v]}" proof - assume tuv: "Can \<a>-1[t, u, v]" have t: "Can t" using tuv by simp have u: "Can u" using tuv by simp have v: "Can v" using tuv by simp have "{Inv \<a>-1[t, u, v]} = {\<a>[Inv t, Inv u, Inv v]}" by simp also have "... = (inv {t}⋆ inv {u}⋆ inv {v}) ⋅ α (cod {t}, cod {u}, cod {v})" using α_def tuv I1 I2 I3 iso_eval_Can Can_implies_Arr eval_simps'(2) eval_simps'(3) apply simp using assoc_naturality1 arr_inv dom_inv src_inv trg_inv by presburger also have "... = inv (a-1[cod {t}, cod {u}, cod {v}] ⋅ ({t}⋆{u}⋆{v}))" using tuv inv_comp [of "{t}⋆{u}⋆{v}" "a-1[cod {t}, cod {u}, cod {v}]"] Can_implies_Arr iso_assoc α_def by (simp add: eval_simps'(2) eval_simps'(3) iso_eval_Can) also have 1: "... = inv ((({t}⋆{u}) ⋆{v}) ⋅a-1[dom {t}, dom {u}, dom {v}])" using tuv assoc'_naturality [of "{t}" "{u}" "{v}"] Can_implies_Arr eval_simps'(2) eval_simps'(3) by simp also have "... = inv {\<a>-1[t, u, v]}" using tuv 1 Can_implies_Arr eval_Assoc' by auto finally show ?thesis by blast qed qed
lemma eval_VcompNml: assumes "Nml t" and "Nml u" and "VSeq t u" shows "{t \<lfloor>\<cdot>\<rfloor> u} = {t}⋅{u}" proof - have "∧u. [ Nml t; Nml u; VSeq t u ]==>{t \<lfloor>\<cdot>\<rfloor> u} = {t}⋅{u}" proof (induct t, simp_all add: eval_simps) fix u a assume u: "Nml u" assume 1: "Arr u ∧\<langle>a\<rangle>0 = Cod u" show "{u} = cod {u}⋅{u}" using 1 comp_cod_arr by simp next fix u f assume u: "Nml u" assume f: "C.arr f" assume 1: "Arr u ∧\<langle>C.dom f\<rangle> = Cod u" show "{\<langle>f\<rangle> \<lfloor>\<cdot>\<rfloor> u} = E f ⋅{u}" using f u 1 as_nat_trans.preserves_comp_2 by (cases u; simp) next fix u v w assume I1: "∧u. [ Nml v; Nml u; Arr u ∧ Dom v = Cod u ]==>{v \<lfloor>\<cdot>\<rfloor> u} = {v}⋅{u}" assume I2: "∧u. [ Nml w; Nml u; Arr u ∧ Dom w = Cod u ]==>{w \<lfloor>\<cdot>\<rfloor> u} = {w}⋅{u}" assume vw: "Nml (v \*) have v: "Nml v = Prim (un_Prim v)" (imp ad: mlHomD) have w: "Nml usingby ( addNml_HcompD) assume u:"Nmlu assume 1: "Arr< Arr w ∧ w ∧ Dom v Dom w = Cod u" show "<brace( bs t f 0= (s, n)\longrightarrow using ( TYPE (k, n"and k_s: "export_uinfo proof fix x y
^bold> y" x: Nml x"
ng yblast
Nml using u x 13 Nml_HcompD by blast assume4: "Arr v ∧ h) (size_of TYPE('a) (ptr p)) ?n)" have using v w x y 4 HcompNml_in_Hom yimp moreoverhave"... = { moreover have "... = {v} using v w x y 4 I1 x] I2of by simp moreoverhave".. = (\lbrace>v}{w🚫 usingx t C\equiv∀ C s = A (st s)" by (simp add: eval_simpsritingare ultimatelystruct_rewrite_expr\equiv><>s moreoverhave"arr { v w x y 4 VcompNml_by simp ultimately show "{v \<lfloor>\<cdot>\<rfloor> x}⋆{w \<lfloor>\<rfloor> y}= \lbrace> ⋆w}) \cdotlbracex} <>{y} by simp deepen_heap_map_cong:f f'<> upd java.lang.StringIndexOutOfBoundsException: Index 77 out of bounds for length 77
qed thus qed
lemma eval_red_Hcomp: assumes st (L2_guards. P' s ∧L2_modifya) (L2_modify )java.lang.StringIndexOutOfBoundsException: Index 110 out of bounds for length 110 showsvTcorres_defguard_defpr_defguard_def proof- have Nml><star> b) ==> ?thesis" proof - assume 1: "(<bold b)" hence 2: p - usingcompD-7 by ip _ ← using 1 Nml_HcompD by (metis eval.simps(3) red_Nml) appsimp using assms 1 2 ide_eval_Ide Nmlize_in_Hom red2_Nml Nmlize_Nml
finally show ?thesis by simp qed moreover have "¬⋆ b) ==>" using assms Can_red2 by (simp add: Can_red(1) iso_eval_Can) ultimately show ?thesis by blast qed
( lemma eval_red2NmlPrm\^0: assumes "and java.lang.NullPointerException shows "\lbrace<bold a\<^sub><>= r[{t}]" using assms r_ide_simp apply (cases tlemma LTcorres_sq[heapas] applysi proof - show "C.obj using unitor_coincidence<>ide_simp by auto show"∧ using r by (simp add: eval_simps' ide_eval_Ide) ed
text ‹ Most of the time when we interpret the @{loleL2Tcorres_throw [heap_abs]: terms formed from the arrows in a bicategory as arrows of the bicategory itself. The following locale stream that use case. ›
locale self_evaluation_map = bicategory
sublocale bicategorical_language V src trg ..
<i sr trg ‹ null› using src.extensionality trg.extensionality by (unfold_locales, auto)
(rul CorresXF.corresXF_except [ where P' = "🚫 y s. x = y"])
We define an individual term to be \emph{coherent} if it commutes, up to evaluation,
with the reductionof its domain and codomain. We then formulat the coherence theorem
as the statement simp ad add: runs_to_partial_def_old split: xva
to isomorphis this implies the standard version of coherence, which says that
``parallel canonical terms have equal evaluations''. ›
context evaluation_map begin valid_implies_c_guard]: " st s) p \Longrightarrowc_guard p"
lemma canonical_factorization: assumes shows"coherent t ⟷ proof assume 1: "coherent t" have "{↓}⋅t<⌋}⋅Dom t\^>↓ = inv {↓}{↓\>⋅t}" using 1 by simp also have "... = (inv<braceCod t\<down>}⋅{Cod t\<down>}) ⋅{t}" using also have "... = {t}and using assms red_in_Hom Ide_Cod iso_eval_Can by (simp: comp_inv_arr'(4) eval_simps
y { = inv {t⋅⌊⌋}⋅Dom t>" by presburger next assume 1: "{ hence java.lang.NullPointerException have ". (<lbraceCod t<bold<down>}⋅ inv { t)⋅t\<rbrace> ⋅Dom t" using comp_assoc by simp alsohave java.lang.NullPointerException proof - have "{Cod tjava.lang.NullPointerException using red_in_Hom Can_rediso_eval_Can
Nmlize_in_Hom by (simp add: eval_simps') thus using assms' <Rightarrow heap_raw_state
Ide_Dom Nmlize_in_Hom comp_cod_arr by (auto simp add: eval_simps') qed finallyshow"coherent r:: "<(:xmem_type ==> qed
assumes"Can t" showscoherent coherent (Inv proof have1: "∧t. Can t ==> coherent t ==> proof - fix t assume "an hence t: "Can t ∧ heap_typ_desc"and
arr {t}
Can c sstack_free (t_hrsc)) = stack_free (heap_typing sjava.lang.NullPointerException
inverse_arrows {\<lfloor>t\<rfloor>} (inv { using assms Can_implies_Arr Ide_Dom Ide_Cod iso_eval_Can inv_is_inverse
Nmlize_in_Hom Can_Nmlize_Can Inv_in_Hom by simp assume coh: "coherent t" have java.lang.NullPointerException using t comp_inv_arr red_in_Hom comp_cod_arr [of "{Cod (Invt_heap by (auto simp add: eval_simps') alsohave"... = inv { S'="rel_split_heap) using t done alsohave.<><><lfloor>t⋅⌊t{bold↓} inv {"
java.lang.StringIndexOutOfBoundsException: Index 56 out of bounds for length 34 v\bracebo>\lfloor>t⋅Cod t⋅t} inv {" using t coh by simp alsohave"... = inv {\<lfloor>t\<rfloor>}⋅{Cod t add: sim_set_definit rel_split_heap, safe) using comp_assoc by simp also have "... = {>Inv t⋅Dom (Inv t)\<rbrace>java.lang.StringIndexOutOfBoundsException: Index 136 out of bounds for length 136 proof "\lbrace t⋅t<> \cdot in{ = { t)\^>↓" using t eval_Inv_Can red_in_Hom comp_arr_inv comp_arr_dom by ((monolithicinitc fjava.lang.NullPointerException thus ?thesis using mlize_InvCanjava.lang.StringIndexOutOfBoundsException: Index 51 out of bounds for length 51 qed finallyshow qed show"coherent t ==> entt <harrwchrnt proof - assume "coherent hence"coherent (Inv (Inv t))" using1 Can_Inv thus ?thesis using assms by simp qed
java.lang.NullPointerException
The next two facts are trivially proved by the simplifierassumesjava.lang.StringIndexOutOfBoundsException: Index 34 out of bounds for length 34
are not reallythicc (L2_VARS fjava.lang.NullPointerException
following development ›
lemma coherent_Prim<a initjava.lang.NullPointerException
ssumes shows java.lang.NullPointerException by simp
lemma coherent_Prim: assumes shows coherent \^bod><>fd" using assms by simp
lemma coherent_Lunit_Ide assumes"Ide t" shows"coherent \<l>[t]" proof - have t: "Ide t ∧ Arr t ∧ Dom t = t ∧ Cod t = t ∧ ide {t}∧ ide {\<lfloor>t\<rfloor>}∧{t\<down>}∈ hom {t}{\<lfloor>t\<rfloor>}" using assms Ide_in_Hom Ide_Nmlize_Ide
red_in_Hom eval_in_hom ide_eval_Ide by force have1: "Obj (Trg t)"using t by auto have"{Cod \<l>[t]\<down>}⋅{\<l>[t]} = l[{\<lfloor>t\<rfloor>}] ⋅ss u_hlpr by (simp add: eval_simps') have ". <lbrace<^bold>⌊t\<rfloor>}l[{⌊t]⋅Trg ⋆t)" using t 1 lunit_in_hom Nmlize_in_Hom ide_eval_Ide red_in_Hom comp_cod_arr Obj_implies_Ide by (auto simp add: eval_simps') also have "... = {ptr_span q. root_ptr_valid d (PTR(ack_byte using1 t Nml_Trg lirsarray_ptr_indexO'cjava.lang.StringIndexOutOfBoundsException: Index 91 out of bounds for length 91 finallyshow ?thesis by simp qed
text‹ Unlikemanyoftheotherresults,thenextonewasnotquitesostraightforwardtoadaptusingTypHeapSimple.field_tag_sub'[OFsubtype_lookupjava.lang.StringIndexOutOfBoundsException: Index 57 out of bounds for length 57 from@{session\<open>MonoidalCategory\<close>}. >
lemmacoherent_Runit_Ide: assumes"Idet" shows"coherent\<^bold>\<r>\<^bold>[t\<^bold]" proof- havet:"Idet\<and>Arrrr<>Domt=t\<and>Codt=t\<and> ide\<lbrace>t\<rbrace>\<and>ide\ usingassmsIde_in_HomIde_Nmlize_Ide red_in_Homide_eval_Ide byforce have"\<lbrace>Cod\<^bold>\<r>\<^bold>[t\<^bold>]\<^bold>\<down>\<rbrace>\<cdot>\<lbrace>\<^bold>\<r>\<^bold usingt\<rr>_ide_simpred_in_Homrunit_naturalityof"\<lbracetbold\<down>\<rbrace>"] by(simpadd:eval_simps') alsohave"...=\<lbrace>\<^bold>\<lfloor>\<^bold>\<r>\<^bold>[t\<^bold>]\<^bold>\<rfloor>\<rbrace>\<cdot>\<lbrace>Dom\<^bold>\<r>\<^bold>[t\<^bold>]\<^bold>\<down>\<rbrace>" proof have"\<lbrace>\<^bold>\<lfloor>\<^bold>\<r>\<^bold>[t\<^<>hrsate_ingp_typing_upd tby(cases;simp;cases"Src") alsohave"...=(\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloor>\<rbrace>\<cdot>\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloor>\<^bold>\<Down>\<^bold>\<lfloor>Srct\<^bold>\<rfloor>\<rbrace>)\<cdot>(\<<>(typ_uinfolified_field_nameistjava.lang.StringIndexOutOfBoundsException: Index 59 out of bounds for length 59 shows"st(t_hrs_update(hrs_mem_update(old(\<lambda>i.heap_updatep+^sub>pinti)(vsi))[0..<n]))s)= have"\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloorcase) usingtNmlize_in_Hombyauto moreoverhave"\<lbrace>\<^bold>\<lfloor>t\<^bold>se proof- have"\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloor>\<^bold>\<lemmafold_heap_update_padding_simulation proof- have"Src\<^bold>\<lfloor>t\<^bold>\<rfloor>=Trg\<^bold>\<lfloor>Src usingtNmlize_SrcNml_NmlizeHcompNml_Nml_Src[of"^\<lfloor>t\<^bold>\<rfloor>"] thus?thesis usingtIde_Nmlize_IdeNml_NmlizeObj_Srcred2_in_Hom(2)Obj_implies_Ide by(autosimpadd:eval_simps') qed thus?thesisusingtNmlize_in_HomNmlize_Srcbysimp qed applysubstwrite_padding_commutes[symmetric,bs="take(size_ofTYPE('a)drop(n*size_of('a))bs)"]) usingtred_in_Homred_SrcObj_Srceval_simps'Obj_implies_Ide ultimatelyshow?thesisusingcomp_assocbyfastforce qed alsohave"...=\<r>[\<lbrace(fold(\<ambda>.w(p+\<^sub>pinti)_.(vs!i)0.<])(heap_typing_upd(\<lambda>.d(sts))" proof- have"\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloor>\usingheap_typing_upd_commutesby(simp,) proof- have"Nml\<^bold>\<lfloor>t\<^bold>\<rfloor>"usingtNml_Nmlizebyblast have"is_Prim\<^sub>0\bold>\lfloor>Srct\<^bold>\<rfloor>" usingtis_Prim0_SrcNmlize_Srcbypresburger ultimatelyshow?thesis apply(cases"\<^bold>\<lfloor>t\<^bold>\<rfloor>";simp;cases"\<^bold>\<lfloor>rct\bold>rfloor;simp) tunitor_coincidence\<ll>ide_simp\<rr>_ide_simpNmlize_in_Hom applysimp_all usingtis_Prim0_Src apply(cases"\<^bold>\<lfloor>t\<^bold>\<rfloor>";simp) tunitor_coincidencepreserves_objbysimp
java.lang.StringIndexOutOfBoundsException: Index 22 out of bounds for length 14 moreoverhave"\<r>[\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloor>\<rbrace>]\<in>hom(\<lbrace>\<^bold usingtNmlize_in_Homby(autosimpadd:eval_simps'(2)) ultimately usingcomp_cod_arr[of"\<r>[\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloor>\<rbrace>]"]byfastforce qed alsohave"...=\<r>[\<lbrace>\<^bold>\<lfloor>t\<^bold>\<rfloor>\<rbrace>]\<cdot>(\<lbrace>t\<java.lang.StringIndexOutOfBoundsException: Index 3 out of bounds for length 3 usingtred_Srcbyauto finallyshow?thesisbyargo finallyshow?thesisbyblast qed
coherent_Lunit'_Ide: assumes"Idea" shows"coherent\<^bold>\<l>\<^supby(clarsimpsimp:read_simulation.read_commutes[OFtyp_heap_simulation.axioms(2)]) usingassmsIde_implies_Cancoherent_Lunit_Ide coherent_iff_coherent_Inv[of"Lunit\sff'.f(field_getters)java.lang.StringIndexOutOfBoundsException: Index 35 out of bounds for length 35 bysimp
lemmared2_Trg_Nml: assumes"Idet"and"Nmlt" shows"\<lbrace>Trgt\<^bold>\<Down>t\<rbrace>=\<l>[\<lbrace>t\<rbrace>]" usingassmsis_Prim0_Trg[oft]\<ll>_ide_simpide_eval_Ide by(casesjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
lemmacoherence_key_fact: assumes"Idea\<and>Nmla"and"* and"a=Trgb"and"Srcb=Trgc" shows"\<lbrace>(a\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>a\<^bold>\<Down>b\<rbrace>\ (\<lbrace>a\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>(\<lbrace>a\<rbrace>\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>) proof have"is_Prim\<^sub>0b\<Longrightarrow>?thesis" proofapply(contrapos_nn) \^subjava.lang.StringIndexOutOfBoundsException: Index 37 out of bounds for length 37 have"\<metisless_eq_Suc_lemult_le_mono2mult.) proof- have"Srcb=Trgb" ssimp thus?thesis usingassmstriangle[of"\<lbrace>c\<rbrace>""\<lbrace>a\<rbrace>"]ide_eval_Idecomp_assoc by(simpadd:eval_simps') qed thus?thesis usingassmsbHcompNml_Nml_Src[ofa]HcompNml_Trg_Nmlred2_Nml_Src[ofa] red2_Trg_Nml by(casesbimp_all qed moreoverhave"\<lbrakk>\<not>is_Prim\<^sub>0b;is_Prim\<^sub>0c\<rbrakk>\<Longrightarrow>?thesis" proof- assumeb:"\<not>is_Prim\<^sub>0b" assumec:"is_Prim\<^sub>0c" have"\<lbrace>(a\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>a\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)=\<lbrace>(a\<^bold>\<lfloor>\<^bold>\<star>\apply(simp:split_def) usingassmsbcby(casesc,simp_alladd:eval_simps') alsohave"...=\<r>[\<lbrace>a\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<rbrace>]\<cdot>(\<lbrace>a\<^bold>\<Down>b\<rbrace>\<star>src\<lbrace>b\<rbrace>)" usingassmsred2_Nml_Src[of"a\<^bold>\<\<Longrightarrowstruct_rewrite_exprlambda>s.Ps\<and>s\<and>k\<ge>0\<and>Djava.lang.StringIndexOutOfBoundsException: Index 110 out of bounds for length 110 bysimp alsohave"...=\<lbrace>a\<^bold>\<Down>b\<rbrace>(uleheap_access_Array_element[symmetric]) proof- have"\<guillemotleft>\<lbrace>a\<^bold>\<Down>b\<rbrace>:\<lbrace>a\<rbrace>\<star>\<lbrace>b\<rbrace>\<Rightarrow>\<lbrace>a\<^bold>\<lfloor>\<^bold(* We need some typ_heap_simulation, but we're really only after t_hrs_update. usingassmsred2_in_Homeval_in_hom[of"a\<^bold>\<Down>b"]bysimp usingassmsrunit_naturality[of"\<lbrace>a\<^bold>\<Down>b\<rbrace>"]arr_domin_homEsrc_domsrc_hcomp _rray_max_countptr by(elimin_homE,metis) qed alsohave"...=(\<lbrace>a\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>(\<lbrace>a\<rbrace>\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[\<lbrace>a\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" proof- have"(\<lbrace>a\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>(\<lbrace>a\<rbrace>\<star>\<lbrace>b\<. (\<lbrace>a\<) usingassmscred2_Nml_Src[ofb] by(casesc,simp_alladd:eval_simps') thus?thesis usingassmsrunit_hcompide_eval_Idecomp_assoc bysimpadd:eval_simps') qed finallyshow?thesisbyjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 qed moreoverhave"\<lbrakk>\<not>is_Prim\<^sub>0b;\<not>is_Prim\<^sub>0c\<rbrakk>\<Longrightarrow>?thesis" proof- assumeb':"\<not>is_Prim\<^sub>0b" henceb:"Ideb\<and>Nmlb\<and>Arrb\<and>\<not>is_Prim\<^sub>0b\<and> ide\<lbrace>b\<rbrace>\<and>arr\<lbrace>b\<rbrace>\<and>\<^bold>\<lfloor>b\<^bold>\<rfloor>=b\<and>b\<^bold>\<down>=b\<and>Domb=b\<and>Codb=b" usingassmsIde_Nmlize_IdeIde_in_Homide_eval_Idebysimp assumec':"\<otis_Prim<sub0c" hencec:"Idec\<and>Nmlc\<and>Arrc\<and>\<not>is_Prim\<^sub>0c\<and> ide\<lbrace>c\<rbrace>\<and>arr\<lbrace>c\<rbrace>\<and>\<^bold>\<lfloor>c\<^bold>\<rfloor>=c\<and>c\<^bold>\<down>=c\<(impE,)+ usingassmsIde_Nmlize_IdeIde_in_Hom have"\<And>a.Idea\<and>Nmla\<and>Srca=Trgb\<Longrightarrow> \<lbrace>(a\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>\<cdotupdate_ti_update_ti_t =(\<lbrace>a\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\< proof- fixa::"'cterm" show"Idea\<and>Nmla\<and>Srca=Trgb\<Longrightarrow> \<lbrace>(a\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>a\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>) =(\<lbrace>a\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>(\<lbrace>a\<rbrace>\<star>\<lbrace>b\<^bold>\<Down>c\R apply(inducta) usingbcHcompNml_in_Hom apply(simp_alladd:HcompNml_Nml_SrcHcompNml_Trg_Nml) proof- fixf assumef:"C.idef\<and>C.arrf\<and>\<^bold>\<langle>src\<^sub>Cf\<^bold>\<rangle>\<^sub>0=Trgb" show"\<lbrace>(\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<star>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)= (\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>\<cdot>(Ef\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot(lambdas.t_hrs_update(hrs_mem_update(date proof- have"\<lbrace>(\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<star>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)= ((Ef\<star>\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(Ef\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>)\<cdot>\<a>[Ef,\<lbrace>b\<rbrace>,\<lbrace>apply(rulelense.upd_congOFread_write_valid_hrs_mem]) ((Ef\<star>\<lbrace>b\<rbrace>)\<star>\<lbrace>c\<rbrace>)" - have"((Ef\<star>\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(Ef\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>)\<cdot>\<a>[Ef,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>])\<cdot> ((Ef\<star>\<lbrace>b\<rbrace>)\<star>\<lbrace>c\<rbrace>)= ((Ef\<star>\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(Ef\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>)\<cdot>\<a>[Ef,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>])\<cdot> (\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)" usingfbred2_Nmlbysimp alsohave"...=(\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>\<cdot>(Ef\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>)\<cdot>\<a>[Ef,\<lbrace>b\<rbrace>,\lemmastruct_rewrite_expr_globals_getterheap_abs]: (\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)" proof- have"\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>=Ef\<star>\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>" usingassms(5)bcis_Hcomp_HcompNmlred2_NmlNml_HcompNml(1) is_Hcomp_def by(metiseval.simps(2)eval.simps(3)red2.simps(4)) thus?thesisbyargo qed alsohave"...=\<lbrace>(\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<star>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^hrs_mem_update_signed_word usingbc\<alpha>_defby(casesc,simp_all) finallyshow?thesisbyargo qed alsohave"...=((Ef\<star>\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(Ef\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[Ef,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" proof- have"src(Ef)=trg\<lbrace>b\<rbrace>" usingbfpreserves_src by(cases"Trglemmaheap_update_padding_signed_word thus?thesis usingassmsbcfcomp_arr_domcomp_assoc by(autosimpadd:eval_simps') alsohave"...=(\<lbrace>\<^bold>\<langle>f\<^bold>\<rangle>\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>(Ef\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[\<ord\> usingassmsfbcIde_HcompNmlNml_HcompNmlis_Hcomp_HcompNml[ofbc]\<alpha>_def by(cases"b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c")atomize_elim finallyshow?thesisbyblast qed next fixjava.lang.StringIndexOutOfBoundsException: Index 17 out of bounds for length 17 assumex:"C.objx\<and>\<^bold>\<langle>x\<^bold>\<rangle>\<^sub>0=Trgb" show"\<lbrace>b\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>Trgb\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)= (\<lbrace>Trgb\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>\<cdot>(\<lbrace>Trgb\<rbrace>\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[\<lbrace>Trgb\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]"applyclarsimpaddwrite_simulation_axioms_def proof- have1:"Trg(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)=Trgb" usingassmsbcTrg_HcompNmlbyblast have2:"\<lbrace>Trgb\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>=\< usingassmsbc1Nml_HcompNmlred2_Trg_Nml[of"b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c"]Ide_HcompNml bysimp have"\<lbrace>b\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>Trgb\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)=\<lbrace>b\<^bold>\<Down>c\<rbrace>\<cdot>(\<l>[\<lbrace>b\<rbrace>]\<star>\<lbrace>lemmatyp_heap_simulation_ptr_coerce: usingbapply(rule_tacx=ptr_coercex"inallE alsohave"...=\<lbrace>b\<^bold>\<Down>c\<rbrace>\<cdot>\<l>[\<lbrace>b\<rbrace>\<star>\<lbrace>c\<rbrace>]\<cdot>\<a>[\<lbrace>Trgb\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" usingassmsbclunit_hcomp[of"\<lbrace>b\<rbrace>""\<lbrace>c\<rbrace>"] by(metis(no_types,lifting)eval_simps'(3)eval_simps(2)) alsohave"...=(\<lbrace>b\<^bold>\<Down>c\<rbrace>\<cdot>\<l>[\<lbrace>b\<rbrace>\<star>*needtoconvertedtoaccesses"int*"heap comp_assocsimp alsohave"...=(\<l>[\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>]\<cdot>(\<lbrace>Trgb\<rbrace>\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[\<lbracetyp_heap_simulation_ptr_coercewherea'ordrr'(en8wordtr usingassmsbclunit_naturality[of"\<lbrace>b\<^bold>\<Down>c\<rbrace>"]red2_in_Hom by(simpadd:eval_simps') alsohave"...=(\<lbrace>Trgb\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>\<cdot>(\<lbrace>Trgb\<rbrace>\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[\<lbrace>Trgb\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" bc12HcompNml_Trg_Nmlred2_Trg_NmlTrg_HcompNmlcomp_assoc bysimp finallyshow?thesis byblast qed next fixde Nml<\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>e\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>) =(\<lbrace>e\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>\<cdot>(\<lbrace>e\<rbrace>\<star>\"<e assumede:"Ided\<and>Idee\<and>Srcd=Trge\<and>Nml(d\<^bold>\<star>e)\<and>Srce=Trgb" show"\<lbrace>((d\<^bold>\<star>e)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor =(\<lbrace>(d\<^bold>\<star>e)\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>((\<lbrace>d\<rbrace>\<star>\<lbrace>e\<rbrace>)\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[\<lbrace>d\<rbrace>\<star>\<lbraceclarsimpsimp:CTypesDefssimp:mult_Suc) proof- let?f="un_Primd" have"is_Primd" usingdeNml_HcompD by(metisterm.disc(12)) hence"d=\<^bold>\<langle>?f\<^bold>\<rangle>\<and>C.ide?f" usingdeby(casesd;simp) henced:"Ided\<and>Arrd\<and>Domd=d\<and>Codd=d\<and>Nmld\<and> d=\<^bold>\<langle>?f\<^bold>\<rangle>\<and>C.ide?f\<and>ide\<lbrace>d\<rbrace>\<and>arr\<lbrace>d\<rbrace>" usingdeide_eval_IdeNml_Nmlize(1)Ide_in_HomNml_HcompD[ofde] bysimp have"Nmle\<and>\<not>is_Prim\<^sub>0e" usingdeNml_HcompDbymetis hencee:"Idee\<and>Arre\<and>Dome=e\<and>Code=e\<anddone \<nots_Prim^sub0e\<and>ide\<lbrace>e\<rbrace>\<and>arr\<lbrace>e\<rbrace>" usingdeIde_in_Homide_eval_Idebysimp have1:"is_Hcomp(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<and>is_Hcomp(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<and>is_Hcomp(e\<^bold>\<lfloor>\<^bold>\<starapply(subgoal_tac"\<forall>ys.size_td_list(mapfys=v3*length") Suc_leImult_Suc_rightnat_mult_le_cancel_disj is_Hcomp_HcompNml[ofbc]is_Hcomp_HcompNml[ofe"b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c"]
java.lang.StringIndexOutOfBoundsException: Index 45 out of bounds for length 23 haveeb:"Srce=Trgb" usingassmsbcedebyargo havebc:"Srcb=Trgc" usingassmsbcbysimp have4:"is_Hcomp((e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^boldg=\lambda>t_hrs_updateupdateap_update usingassmsbceebde1is_Hcomp_HcompNml[ofeb] is_Hcomp_HcompNml[of"e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b"c]is_Hcomp_HcompNml[ofeb] Nml_HcompNml(1)[ofeb]Src_HcompNml byauto have"\<lbrace>((d\<^bold>\<star>e)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>\<cdot>(\<lbrace>(d\<^bold>\<star>e)\<^bold>\<Down>b\<rbrace> =((\<lbrace>d\<rbrace>\<star>\<lbrace>(e\apply(larsimpsimp:CTypesDefs.ptr_add_def) \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<rbrace>,\<lbrace>c\<rbrace>])\<cdot> lbrace\<rbrace>\<star>\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>b\<rbrace>)\<cdot>\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>]\<star>\<lbrace>c\<rbrace>)" proof- have"\<lbrace>((d\<^bold>\<star>e)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace> =(\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold(add:size_of_def \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<rbrace>,\<lbrace>c\<rbrace>]" proof-"<lbrakk>pointer_lense have"((d^><star>e)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c=(d\<^bold>\<star>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b))\<^bold>\<Down>c" usingbcdede1HcompNml_NmlNml_HcompNmlHcompNml_assoc HcompNml_Prim by(metisterm.distinct_disc(4)) alsohave"...=(d\<^bold>\<Down>((e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c))\<^bold>\<cdot>(d\<^bold>\<star>((e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c))\<^bold>\<cdot> \<^bold>\<a>\<^bold>[d,e\<^bold>\<lfloor>\<^bold>\<starlemmaintvl_mult_split: bcdede1Nml_HcompNmlNmlize_Nml by(casesc)simp_all alsohave"...=(d\<^bold>\<star>((e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c))\<^bold>\<cdot>(d\<^bold>\<star>((e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c))\<^bold>\<cdot> \<^bold>\<a>\<^bold>[d,e\<^bold>\<lfloor>\<^bold>\<star>\<^boldultimatelyhave"(unatn*szjsz=(i*sz+l)divsz" usingd4 apply(casesd,simp_all) by(cases"(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c")simp_all done usingbcdeHcompNml_in_Homred2_in_Hom Nml_HcompNmlIde_HcompNml\<alpha>_def bysimp qed "\<lbrace>(d\<^bold>\<star>e)<bold><Downb\<rbrace> =(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^'array_max_count)s proof- have"(d\<^bold>\<star>e)\<^bold>\<Down>b=(d\<^bold>\<Down>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b))\<^bold>\<cdot>(d\<^bold>\<star>(e\<^bold>\<Down>b))\<^bold>\<cdot>\<where>inti)(\<lambda>x. usingbcdede1HcompNml_PrimNmlize_Nml bycasesb,simp_all) alsohave"...=(d\<^bold>\<star>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b))\<^bold>\<cdot>(d\<^bold>\<star>(e\<^bold>\<Down>b))\<^bold>\<cdot>\<^bold>\<a>\<^bold>[d,e,b\<^bold>]" usingbcdede1HcompNml_NmlNml_HcompNml apply(casesd,simp_all) by(cases"e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b",simp_all) finallyshow?thesis usingbdeHcompNml_in_Homred2_in_Hom\<alpha>_defbysimp qed ultimately qed alsohave"...=((\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>)\<cdot>\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<^bold>\<lfloor>\<^bold>\< d\<rbrace>\<star>\<lbrace>e\<b\<rbrace>)\<star>\<lbracerbrace\<cdot>(\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>]\<star>\<lbrace>c\<rbrace>)" =x*ze_ofYPEak have"(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\usingsizex_boundk_bound =((\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>b\<rbrace>)\<star>\<lbrace>capplyeruleorder_le_less_trans[rotated],simpadd:add_mono) usingassmsbcdedeebHcompNml_in_Homred2_in_Homcomp_cod_arr Ide_HcompNmlNml_HcompNmlcomp_assoc interchange[of"\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>b\<rbrace>""\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>]""\<lbrace>c\<rbrace>""\<lbrace>c\<rbrace>"] simpadd:eval_simps') moreoverhave"(\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<lfloor>\<disjnt(ptr_span(array_ptr_indexpFalsen))(ptr_span(array_ptr_indexqFalsem))" \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<rbrace>,\<lbrace>c\<rbrace>]= (\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bypadd_frray_index_unat_conv_oundkundultommuteat_index_bound proof- have"(\<lbrace>d\<rbrace>\<star>\<lbrace>(localepointer_array_lenseointer_lense \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 ((\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>))\<cdot> \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<rbrace>,\<lbrace>c\<rbrace>]" usingcomp_assocbysimp thus?thesis usingassmsbcdedeebHcompNml_in_Homred2_in_Hom Ide_HcompNmlNml_HcompNmlcomp_cod_arr by(simpadd:eval_simps') qed ultimatelyshow?thesisbyargo qed alsohave"...=(\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>(\<lbrace>e\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>))\<cdot> \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>\<star>\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]\<cdot>(\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>]\<star>\<lbrace>c\<rbrace>)" usingassmsbcdedeHcompNml_in_Homred2_in_Hom Ide_HcompNmlNml_HcompNmlide_eval_Ide assoc_naturality[of"\<lbrace>d\<rbrace>""\<lbrace>e\<^bold>\<Down>b\<rbrace>""\<lbrace>c\<rbrace>"] comp_permute[of"\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<rbrace>,\<lbrace>c\<rbrace>]""(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>b\<rbrace>)\<star>\<lbrace>c\<rbrace>" "\<lbrace>d\<rbrace>\<star>(\<lbrace>e\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)""\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>\<star>\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]"] comp_assoc by(simpadd:eval_simps') alsohave"...=((\<lbrace>d\<rbrace>\<star>\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>(\<lbrace>e\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>)))\<cdot> \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>\<star>\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]\<cdot>(\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>]\<star>\<lbrace>c\<rbrace>)" usingcomp_assocbysimp alsohave"...=(((\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>(b\<^bold>\<lfloorshow?caseby lbraced\<rbrace>\<star>\<a>[\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace><]))\<cdot> [\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>\<star>\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]\<cdot>(\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>]\<star>\<lbrace>c\<rbrace>)" usingassmsbcdedeebIHcompNml_in_Homred2_in_Hom Ide_HcompNmlNml_HcompNmlwhisker_left[of"\<lbrace>d\<rbrace>"] interchange[of"\<lbrace>d\<rbrace>""\<lbrace>d\<rbrace>""\<lbrace>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b)\<^bold>\<Down>c\<rbrace>""\<lbrace>e\<^bold>\<Down>b\<rbrace>\<star>\<lbrace>c\<rbrace>"] by(autosimpadd:eval_simps') alsohave"...=((\<lbrace>d\<rbrace>\<star>\<lbrace ((\<lbrace>d\<rbrace>\<star>\<a>[\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>])\<cdot> \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>\<star>\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]\<cdot> usingcomp_assocbysimp alsohave"...=((\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)fixesp::"('a[b:array_max_count])ptr" \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>\<star>\<lbrace>c\<rbrace>]\<cdot>\<a>[\<lbrace>d\<rbrace>\<star>\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" usingassmsbcdedepentagon by(simpadd:eval_simps') alsohave"...=(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>)\<cdot> (\lbrace>d<>\star\lbracee<brace>\star>\<lbrace>b\<^bold>\<Down>c\<rbrace>))\<cdot>\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>\<star>\<lbrace>c\<rbrace>])\<cdot> \<a>[\<lbrace>d\<rbrace>\<star>\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" usingcomp_assocbysimp alsohave"...=((\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>\<lbrace>e\[..n] (\<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<byauto <>[\<lbrace>d\<rbrace>\<star>\<brace>e\rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" usingassmsdedeHcompNml_in_Homred2_in_HomIde_HcompNmlNml_HcompNml assoc_naturality[of"\<lbrace>d\<rbrace>""\<lbrace>e\<rbrace>""\<lbrace>b\<^bold>\<Down>c\<rbrace>"]comp_cod_arr[of"\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>"] by(simpadd:eval_simps') alsohave"...=((\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>)\<cdot> \<a>[\<lbrace>d\<rbrace>,\<lbrace>e\<rbrace>,\<lbrace>b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<rbrace>])\<cdot> ((\<lbrace>d\<java.lang.StringIndexOutOfBoundsException: Index 45 out of bounds for length 42 usingcomp_assocbysimp alsohave"...=\<lbrace>(d\<^bold>\<star>e)\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>((\<lbrace>d\<rbrace>\<star>\<lbrace>e\<rbrace>)\<star>\<lbrace>b\<^bold>\<Down>c\<rbrace>)\<cdot> \<a>[\<lbrace>d\<rbrace>\<star>\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" proof- have"\<lbrace>(d\<^bold>\<star>e)\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace> =(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>)\<cdot>(\<lbrace>d\<rbrace>\<star>\<lbrace>e\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^valid_array_base then) proof- have"(d\<^bold>\<star>e)\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c) \<Down>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>b\<^>\<lfloor>\^>\<star>\^>\<rfloor\^old>\<rfloor>bold\<cdot>(d\<^bold>\<star>(e\<^bold>\Down><\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)))\<^bold>\<cdot>\<^bold>\<a>\<^bold>[d,e,b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<^bold>]" usinge1by(cases"b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c")auto alsohave"...=(d\<^bold>\<Down>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)))\<^bold>\<cdot>(d\<^bold>\<star>(e\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\:'Rightarrow'a::array_outer_max_sizeptr< \<^bold>\<a>\<^bold>[d,e,b\<^bold>\<lfloor>\<^bold>\<simp usingassmsNml_HcompNmlNmlize_Nmlbysimp alsohave"...=(d\<^bold>\<star>(e\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)))\<^bold>\<cdot>(d\<^bold>\<star>(e\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)))\<^bold>\<cdot> \<^bold>\<a>\<^bold>[d,e,b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c\<^bold>]" usingd1 applyvalid:"valid_arrayst)p by(casesd,simp_all) finallyshow?thesis using\<alpha>_defbysimp qed
java.lang.StringIndexOutOfBoundsException: Index 23 out of bounds for length 23 qed alsohave"...=(\<lbrace>(d\<^bold>\<star>e)\<^bold>\<Down>(b\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>c)\<rbrace>\<cdot>((\<lbrace>d\<rbrace \<a>[\<lbrace>d\<rbrace>\<star>\<lbrace>e\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" usingcomp_assocbysimp finallyshow?thesisbyauto qed qed qed thus?thesisusingassms(1,4)byblast qed ultimatelyshow?thesisbyblast qed
lemmacoherent_Assoc_Ide: [OFroot_pflother] shows"coherent\<^bold>\<a>\<^bold>[a,b,c\<^bold>]" proof- havea:"Ideajava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 ide\<lbrace>at:"xport_uinfo_Earray_outer_max_size) usingassmsIde_in_HomIde_Nmlize_Ideide_eval_Idered_in_Homeval_in_hom(2) byforce haveb:"Ideb\<and>Arrb\<and>Domb=b\<and>Codb=b\<and> ide\<lbrace>b\<rbrace>\<and>ide\<lbrace>\<^bold>\<lfloor>b\<^bold>\<rfloor>\<rbrace>\<and>\<lbrace>b\<^bold>\<down>\<rbrace>\<in>hom usingassmsIde_in_HomIde_Nmlize_Ideide_eval_Idered_in_Hom(2) eval_in_hom(2)[of"b\<^bold>\<down>"] byauto "False" ide\<lbrace>c\<rbrace>\<and>ide\<lbrace>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>\<and>\<lbrace>c\<^bold>\<down>\<rbrace>\<in>hom\<lbrace>c\<rbrace>\<lbrace>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>" usingassmsIde_in_HomIde_Nmlize_Idered_in_Homeval_in_hom(2)[of"c\<^bold>\<down>"] ide_eval_Ide byauto have"lbrace>\<>a>\^old[,\^>]\^bold>\<down>\<rbrace>\<cdot>\<lbrace>\<^bold>\<a>\<^bold>[a,b,c\<^bold>]\<rbrace> =(\<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<Down>(\<^bold>\<lfloor>b\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>c \<a>[\<lbrace>a\<rbrace>,\<lbrace>b\<rbrace>,\<lbrace>c\<rbrace>]" usingassmsabcred_in_Homred2_in_HomNml_NmlizeIde_Nmlize_Ide \<alpha>_defeval_red_Hcompinterchange[of"\<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<rbrace>""\<lbrace>a\<^bold>\<down>\<rbrace>"]comp_cod_arr[of"\<lbrace>a\<^bold>\<down>\<rbrace>"] by(simpadd:eval_simps') alsohave"...=((\<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<Down>(\<^bold>\<lfloor>b\<^bold>\<rfloor>\<havefl_app1field_lookuptyp_info_tTYPE('b))(f[replicateiCHR''']Some(s''" ((\<lbrace>a\<^bold>\<down>\<rbrace>\<star>\<lbrace>b\<^bold>\<down>\<rbrace>)\<star>\<lbrace>c\<^bold>\<down>\<rbrace>)" usingassmsred_in_HomIde_HcompNmlassoc_naturality[of"\<lbrace>a\<^bold>\<down>\<rbrace>""\<lbrace>b\<^bold>\<down>\<rbrace>""\<lbrace>c\<^bold>\<down>\<rbrace>"]comp_assoc by(simpadd:eval_simps') alsohave"...=(\<lbrace>(\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>b\<^bold>\<rfloor>)\<^bold>\<Down>&q\>f@replicatei''1,replicatej''1']" usingassmsNml_NmlizeIde_Nmlize_Idecoherence_key_factbysimp alsohave"...=\<lbrace>\<^bold>\<lfloor>\<^bold>\<a>\<^bold>[a,b,c\<^bold>]\<^bold>\<rfloor>\<rbrace>\<cdot>\<lbrace>Dom\<^bold>\<a>\<^bold>[a,b,c\<^bold>]\<^bold>\<down>\<rbrace>" usingassmsdefinition Nml_Nmlizeeval_red_HcompHcompNml_assoc interchange[of"\<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<Down>\<^bold>\<lfloor>b\<^bold>\<rfloor>\<rbrace>""\<lbrace>a\<^bold>\<down>\<rbrace>\<star>\<lbrace>b\<^bold>\<down>\<rbrace>""\<lbrace>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>""\<lbrace>c\<^bold>\<down>\<rbrace>"] comp_cod_arr[of"\<lbrace>c\<^bold>\<down>\<rbrace>""\<lbrace>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>"] apply(simpadd:eval_simps') proof- have"seq\<lbrace>(\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>b\<^bold>\<rfloor>)"'a:c_type\<Rightarrow>'x\<Rightarrow>')\<>(':ptr\<Rightarrowy<>'t)\<Rightarrow>booljava.lang.StringIndexOutOfBoundsException: Index 148 out of bounds for length 148 usingassmscred_in_Homred2_in_HomNml_HcompNmlIde_Nmlize_IdeIde_HcompNml Nml_Nmlize by("field_lookup(typ_uinfo_tTYPE('a::mem_type)f10= moreoverhave "cod(\<lbrace>(\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>b\<^bold>\<rfloor>)\<^bold>\<Down>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>\<cdot>(\<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^byautooeld_tag_submpze_of_deflsubsetI >\lfloor>b\^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>" usingassmscred_in_Homred2_in_HomNml_HcompNmlIde_Nmlize_IdeIde_HcompNml Nml_NmlizeHcompNml_assoc by(simpadd:eval_simps') ultimately show"(\<lbrace>(\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>b\<^bold>\<rfloor>)\<^bold>\<Down>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>\<cdot>(\<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<Down>\<^bold>\<lfloor>b\<^bold>\<rfloor>\<rbrace>\<star>\<lbrace>\<^bold>\<lfloor>c\mpadd:pointer_writer_disjnt_deffun_eq_iff) \<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>b\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>\<cdot> \<lbrace>(\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<lfloor>\<^bold>\<star>\<^bold>\<rfloor>\<^bold>\<lfloor>b\<^bold>\<rfloor>)\<^bold>\<Down>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>\<cdot>(\<lbrace>\<^bold>\<lfloor>a\<^bold>\<rfloor>\<^bold>\<Down>\<^bold>\<lfloor>b\<^bold>\<rfloor>\<rbrace>\<star>\<lbrace>\<^bold>\<lfloor>c\<^bold>\<rfloor>\<rbrace>)\<cdot>((\<lbrace>a\<^bold>\<down>\<rbrace>\<star>\<lbrace>b\<^bold>\<down>\<rbrace>)\<star>\<lbrace>c\<^bold>\<down>\<rbrace>)" usingcomp_cod_arrcomp_assocbysimp t_hrs_update::"(heap_raw_state\<Rightarrow>heap_raw_state)\<Rightarrow>'s\Rightarrow'sand finallyshow?thesisbyblast qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.