Theory OCL_Typing
chapter ‹Typing›
theory OCL_Typing
imports OCL_Object_Model "HOL-Library.Transitive_Closure_Table"
begin
text ‹
The following rules are more restrictive than rules given in
the OCL specification. This allows one to identify more errors
in expressions. However, these restrictions may be revised if necessary.
Perhaps some of them could be separated and should cause warnings
instead of errors.›
section ‹Operations Typing›
subsection ‹Metaclass Operations›
text ‹
All basic types in the theory are either nullable or non-nullable.
For example, instead of @{text Boolean} type we have two types:
@{text "Boolean[1]"} and @{text "Boolean[?]"}.
The @{text "allInstances()"} operation is extended accordingly:›
text ‹
▩‹Boolean[1].allInstances() = Set{true, false}
Boolean[?].allInstances() = Set{true, false, null}››
inductive mataop_type where
"mataop_type τ AllInstancesOp (Set τ)"
subsection ‹Type Operations›
text ‹
At first we decided to allow casting only to subtypes.
However sometimes it is necessary to cast expressions to supertypes,
for example, to access overridden attributes of a supertype.
So we allow casting to subtypes and supertypes.
Casting to other types is meaningless.›
text ‹
According to the Section 7.4.7 of the OCL specification
@{text "oclAsType()"} can be applied to collections as well as
to single values. I guess we can allow @{text "oclIsTypeOf()"}
and @{text "oclIsKindOf()"} for collections too.›
text ‹
Please take a note that the following expressions are prohibited,
because they always return true or false:›
text ‹
▩‹1.oclIsKindOf(OclAny[?])
1.oclIsKindOf(String[1])››
text ‹
Please take a note that:›
text ‹
▩‹Set{1,2,null,'abc'}->selectByKind(Integer[1]) = Set{1,2}
Set{1,2,null,'abc'}->selectByKind(Integer[?]) = Set{1,2,null}››
text ‹
The following expressions are prohibited, because they always
returns either the same or empty collections:›
text ‹
▩‹Set{1,2,null,'abc'}->selectByKind(OclAny[?])
Set{1,2,null,'abc'}->selectByKind(Collection(Boolean[1]))››
inductive typeop_type where
"σ < τ ∨ τ < σ ⟹
typeop_type DotCall OclAsTypeOp τ σ σ"
| "σ < τ ⟹
typeop_type DotCall OclIsTypeOfOp τ σ Boolean[1]"
| "σ < τ ⟹
typeop_type DotCall OclIsKindOfOp τ σ Boolean[1]"
| "element_type τ ρ ⟹ σ < ρ ⟹
update_element_type τ σ υ ⟹
typeop_type ArrowCall SelectByKindOp τ σ υ"
| "element_type τ ρ ⟹ σ < ρ ⟹
update_element_type τ σ υ ⟹
typeop_type ArrowCall SelectByTypeOp τ σ υ"
subsection ‹OclSuper Operations›
text ‹
It makes sense to compare values only with compatible types.›
inductive super_binop_type
:: "super_binop ⇒ ('a :: order) type ⇒ 'a type ⇒ 'a type ⇒ bool" where
"τ ≤ σ ∨ σ < τ ⟹
super_binop_type EqualOp τ σ Boolean[1]"
| "τ ≤ σ ∨ σ < τ ⟹
super_binop_type NotEqualOp τ σ Boolean[1]"
subsection ‹OclAny Operations›
text ‹
The OCL specification defines @{text "toString()"} operation
only for boolean and numeric types. However, I guess it is a good
idea to define it once for all basic types. Maybe it should be defined
for collections as well.›
inductive any_unop_type where
"τ ≤ OclAny[?] ⟹
any_unop_type OclAsSetOp τ (Set (to_required_type τ))"
| "τ ≤ OclAny[?] ⟹
any_unop_type OclIsNewOp τ Boolean[1]"
| "τ ≤ OclAny[?] ⟹
any_unop_type OclIsUndefinedOp τ Boolean[1]"
| "τ ≤ OclAny[?] ⟹
any_unop_type OclIsInvalidOp τ Boolean[1]"
| "τ ≤ OclAny[?] ⟹
any_unop_type OclLocaleOp τ String[1]"
| "τ ≤ OclAny[?] ⟹
any_unop_type ToStringOp τ String[1]"
subsection ‹Boolean Operations›
text ‹
Please take a note that:›
text ‹
▩‹true or false : Boolean[1]
true and null : Boolean[?]
null and null : OclVoid[?]››
inductive boolean_unop_type where
"τ ≤ Boolean[?] ⟹
boolean_unop_type NotOp τ τ"
inductive boolean_binop_type where
"τ ⊔ σ = ρ ⟹ ρ ≤ Boolean[?] ⟹
boolean_binop_type AndOp τ σ ρ"
| "τ ⊔ σ = ρ ⟹ ρ ≤ Boolean[?] ⟹
boolean_binop_type OrOp τ σ ρ"
| "τ ⊔ σ = ρ ⟹ ρ ≤ Boolean[?] ⟹
boolean_binop_type XorOp τ σ ρ"
| "τ ⊔ σ = ρ ⟹ ρ ≤ Boolean[?] ⟹
boolean_binop_type ImpliesOp τ σ ρ"
subsection ‹Numeric Operations›
text ‹
The expression @{text "1 + null"} is not well-typed.
Nullable numeric values should be converted to non-nullable ones.
This is a significant difference from the OCL specification.›
text ‹
Please take a note that many operations automatically casts
unlimited naturals to integers.›
text ‹
The difference between @{text "oclAsType(Integer)"} and
@{text "toInteger()"} for unlimited naturals is unclear.›
inductive numeric_unop_type where
"τ = Real[1] ⟹
numeric_unop_type UMinusOp τ Real[1]"
| "τ = UnlimitedNatural[1]─Integer[1] ⟹
numeric_unop_type UMinusOp τ Integer[1]"
| "τ = Real[1] ⟹
numeric_unop_type AbsOp τ Real[1]"
| "τ = UnlimitedNatural[1]─Integer[1] ⟹
numeric_unop_type AbsOp τ Integer[1]"
| "τ = UnlimitedNatural[1]─Real[1] ⟹
numeric_unop_type FloorOp τ Integer[1]"
| "τ = UnlimitedNatural[1]─Real[1] ⟹
numeric_unop_type RoundOp τ Integer[1]"
| "τ = UnlimitedNatural[1] ⟹
numeric_unop_type numeric_unop.ToIntegerOp τ Integer[1]"
inductive numeric_binop_type where
"τ ⊔ σ = ρ ⟹ ρ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type PlusOp τ σ ρ"
| "τ ⊔ σ = Real[1] ⟹
numeric_binop_type MinusOp τ σ Real[1]"
| "τ ⊔ σ = UnlimitedNatural[1]─Integer[1] ⟹
numeric_binop_type MinusOp τ σ Integer[1]"
| "τ ⊔ σ = ρ ⟹ ρ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type MultOp τ σ ρ"
| "τ = UnlimitedNatural[1]─Real[1] ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type DivideOp τ σ Real[1]"
| "τ ⊔ σ = ρ ⟹ ρ = UnlimitedNatural[1]─Integer[1] ⟹
numeric_binop_type DivOp τ σ ρ"
| "τ ⊔ σ = ρ ⟹ ρ = UnlimitedNatural[1]─Integer[1] ⟹
numeric_binop_type ModOp τ σ ρ"
| "τ ⊔ σ = ρ ⟹ ρ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type MaxOp τ σ ρ"
| "τ ⊔ σ = ρ ⟹ ρ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type MinOp τ σ ρ"
| "τ = UnlimitedNatural[1]─Real[1] ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type numeric_binop.LessOp τ σ Boolean[1]"
| "τ = UnlimitedNatural[1]─Real[1] ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type numeric_binop.LessEqOp τ σ Boolean[1]"
| "τ = UnlimitedNatural[1]─Real[1] ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type numeric_binop.GreaterOp τ σ Boolean[1]"
| "τ = UnlimitedNatural[1]─Real[1] ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
numeric_binop_type numeric_binop.GreaterEqOp τ σ Boolean[1]"
subsection ‹String Operations›
inductive string_unop_type where
"string_unop_type SizeOp String[1] Integer[1]"
| "string_unop_type CharactersOp String[1] (Sequence String[1])"
| "string_unop_type ToUpperCaseOp String[1] String[1]"
| "string_unop_type ToLowerCaseOp String[1] String[1]"
| "string_unop_type ToBooleanOp String[1] Boolean[1]"
| "string_unop_type ToIntegerOp String[1] Integer[1]"
| "string_unop_type ToRealOp String[1] Real[1]"
inductive string_binop_type where
"string_binop_type ConcatOp String[1] String[1] String[1]"
| "string_binop_type EqualsIgnoreCaseOp String[1] String[1] Boolean[1]"
| "string_binop_type LessOp String[1] String[1] Boolean[1]"
| "string_binop_type LessEqOp String[1] String[1] Boolean[1]"
| "string_binop_type GreaterOp String[1] String[1] Boolean[1]"
| "string_binop_type GreaterEqOp String[1] String[1] Boolean[1]"
| "string_binop_type IndexOfOp String[1] String[1] Integer[1]"
| "τ = UnlimitedNatural[1]─Integer[1] ⟹
string_binop_type AtOp String[1] τ String[1]"
inductive string_ternop_type where
"σ = UnlimitedNatural[1]─Integer[1] ⟹
ρ = UnlimitedNatural[1]─Integer[1] ⟹
string_ternop_type SubstringOp String[1] σ ρ String[1]"
subsection ‹Collection Operations›
text ‹
Please take a note, that @{text "flatten()"} preserves a collection kind.›
inductive collection_unop_type where
"element_type τ _ ⟹
collection_unop_type CollectionSizeOp τ Integer[1]"
| "element_type τ _ ⟹
collection_unop_type IsEmptyOp τ Boolean[1]"
| "element_type τ _ ⟹
collection_unop_type NotEmptyOp τ Boolean[1]"
| "element_type τ σ ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
collection_unop_type CollectionMaxOp τ σ"
| "element_type τ σ ⟹ operation σ STR ''max'' [σ] oper ⟹
collection_unop_type CollectionMaxOp τ σ"
| "element_type τ σ ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
collection_unop_type CollectionMinOp τ σ"
| "element_type τ σ ⟹ operation σ STR ''min'' [σ] oper ⟹
collection_unop_type CollectionMinOp τ σ"
| "element_type τ σ ⟹ σ = UnlimitedNatural[1]─Real[1] ⟹
collection_unop_type SumOp τ σ"
| "element_type τ σ ⟹ operation σ STR ''+'' [σ] oper ⟹
collection_unop_type SumOp τ σ"
| "element_type τ σ ⟹
collection_unop_type AsSetOp τ (Set σ)"
| "element_type τ σ ⟹
collection_unop_type AsOrderedSetOp τ (OrderedSet σ)"
| "element_type τ σ ⟹
collection_unop_type AsBagOp τ (Bag σ)"
| "element_type τ σ ⟹
collection_unop_type AsSequenceOp τ (Sequence σ)"
| "update_element_type τ (to_single_type τ) σ ⟹
collection_unop_type FlattenOp τ σ"
| "collection_unop_type FirstOp (OrderedSet τ) τ"
| "collection_unop_type FirstOp (Sequence τ) τ"
| "collection_unop_type LastOp (OrderedSet τ) τ"
| "collection_unop_type LastOp (Sequence τ) τ"
| "collection_unop_type ReverseOp (OrderedSet τ) (OrderedSet τ)"
| "collection_unop_type ReverseOp (Sequence τ) (Sequence τ)"
text ‹
Please take a note that if both arguments are collections,
then an element type of the resulting collection is a super type
of element types of orginal collections. However for single-valued
operations (@{text "append()"}, @{text "insertAt()"}, ...)
this behavior looks undesirable. So we restrict such arguments
to have a subtype of the collection element type.›
text ‹
Please take a note that we allow the following expressions:›
text ‹
▩‹let nullable_value : Integer[?] = null in
Sequence{1..3}->inculdes(nullable_value) and
Sequence{1..3}->inculdes(null) and
Sequence{1..3}->inculdesAll(Set{1,null})››
text ‹
The OCL specification defines @{text "including()"} and
@{text "excluding()"} operations for the @{text Sequence} type
but does not define them for the @{text OrderedSet} type.
We define them for all collection types.
It is a good idea to prohibit including of values that
do not conform to a collection element type.
However we do not restrict it.
At first we defined the following typing rules for the
@{text "excluding()"} operation:
{\isacharbar}\ {\isachardoublequoteopen}element{\isacharunderscore}type\ {\isasymtau}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isasymle}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isasymnoteq}\ OclVoid{\isacharbrackleft}{\isacharquery}{\isacharbrackright}\ {\isasymLongrightarrow}\isanewline
\ \ \ collection{\isacharunderscore}binop{\isacharunderscore}type\ ExcludingOp\ {\isasymtau}\ {\isasymsigma}\ {\isasymtau}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}element{\isacharunderscore}type\ {\isasymtau}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isasymle}\ {\isasymrho}\ {\isasymLongrightarrow}\ {\isasymsigma}\ {\isacharequal}\ OclVoid{\isacharbrackleft}{\isacharquery}{\isacharbrackright}\ {\isasymLongrightarrow}\isanewline
\ \ \ update{\isacharunderscore}element{\isacharunderscore}type\ {\isasymtau}\ {\isacharparenleft}to{\isacharunderscore}required{\isacharunderscore}type\ {\isasymrho}{\isacharparenright}\ {\isasymupsilon}\ {\isasymLongrightarrow}\isanewline
\ \ \ collection{\isacharunderscore}binop{\isacharunderscore}type\ ExcludingOp\ {\isasymtau}\ {\isasymsigma}\ {\isasymupsilon}{\isachardoublequoteclose}\isanewline
This operation could play a special role in a definition
of safe navigation operations:›
text ‹
▩‹Sequence{1,2,null}->exculding(null) : Integer[1]››
text ‹
However it is more natural to use a @{text "selectByKind(T[1])"}
operation instead.›
inductive collection_binop_type where
"element_type τ ρ ⟹ σ ≤ to_optional_type_nested ρ ⟹
collection_binop_type IncludesOp τ σ Boolean[1]"
| "element_type τ ρ ⟹ σ ≤ to_optional_type_nested ρ ⟹
collection_binop_type ExcludesOp τ σ Boolean[1]"
| "element_type τ ρ ⟹ σ ≤ to_optional_type_nested ρ ⟹
collection_binop_type CountOp τ σ Integer[1]"
| "element_type τ ρ ⟹ element_type σ υ ⟹ υ ≤ to_optional_type_nested ρ ⟹
collection_binop_type IncludesAllOp τ σ Boolean[1]"
| "element_type τ ρ ⟹ element_type σ υ ⟹ υ ≤ to_optional_type_nested ρ ⟹
collection_binop_type ExcludesAllOp τ σ Boolean[1]"
| "element_type τ ρ ⟹ element_type σ υ ⟹
collection_binop_type ProductOp τ σ
(Set (Tuple (fmap_of_list [(STR ''first'', ρ), (STR ''second'', υ)])))"
| "collection_binop_type UnionOp (Set τ) (Set σ) (Set (τ ⊔ σ))"
| "collection_binop_type UnionOp (Set τ) (Bag σ) (Bag (τ ⊔ σ))"
| "collection_binop_type UnionOp (Bag τ) (Set σ) (Bag (τ ⊔ σ))"
| "collection_binop_type UnionOp (Bag τ) (Bag σ) (Bag (τ ⊔ σ))"
| "collection_binop_type IntersectionOp (Set τ) (Set σ) (Set (τ ⊔ σ))"
| "collection_binop_type IntersectionOp (Set τ) (Bag σ) (Set (τ ⊔ σ))"
| "collection_binop_type IntersectionOp (Bag τ) (Set σ) (Set (τ ⊔ σ))"
| "collection_binop_type IntersectionOp (Bag τ) (Bag σ) (Bag (τ ⊔ σ))"
| "collection_binop_type SetMinusOp (Set τ) (Set σ) (Set τ)"
| "collection_binop_type SymmetricDifferenceOp (Set τ) (Set σ) (Set (τ ⊔ σ))"
| "element_type τ ρ ⟹ update_element_type τ (ρ ⊔ σ) υ ⟹
collection_binop_type IncludingOp τ σ υ"
| "element_type τ ρ ⟹ σ ≤ ρ ⟹
collection_binop_type ExcludingOp τ σ τ"
| "σ ≤ τ ⟹
collection_binop_type AppendOp (OrderedSet τ) σ (OrderedSet τ)"
| "σ ≤ τ ⟹
collection_binop_type AppendOp (Sequence τ) σ (Sequence τ)"
| "σ ≤ τ ⟹
collection_binop_type PrependOp (OrderedSet τ) σ (OrderedSet τ)"
| "σ ≤ τ ⟹
collection_binop_type PrependOp (Sequence τ) σ (Sequence τ)"
| "σ = UnlimitedNatural[1]─Integer[1] ⟹
collection_binop_type CollectionAtOp (OrderedSet τ) σ τ"
| "σ = UnlimitedNatural[1]─Integer[1] ⟹
collection_binop_type CollectionAtOp (Sequence τ) σ τ"
| "σ ≤ τ ⟹
collection_binop_type CollectionIndexOfOp (OrderedSet τ) σ Integer[1]"
| "σ ≤ τ ⟹
collection_binop_type CollectionIndexOfOp (Sequence τ) σ Integer[1]"
inductive collection_ternop_type where
"σ = UnlimitedNatural[1]─Integer[1] ⟹ ρ ≤ τ ⟹
collection_ternop_type InsertAtOp (OrderedSet τ) σ ρ (OrderedSet τ)"
| "σ = UnlimitedNatural[1]─Integer[1] ⟹ ρ ≤ τ ⟹
collection_ternop_type InsertAtOp (Sequence τ) σ ρ (Sequence τ)"
| "σ = UnlimitedNatural[1]─Integer[1] ⟹
ρ = UnlimitedNatural[1]─Integer[1] ⟹
collection_ternop_type SubOrderedSetOp (OrderedSet τ) σ ρ (OrderedSet τ)"
| "σ = UnlimitedNatural[1]─Integer[1] ⟹
ρ = UnlimitedNatural[1]─Integer[1] ⟹
collection_ternop_type SubSequenceOp (Sequence τ) σ ρ (Sequence τ)"
subsection ‹Coercions›
inductive unop_type where
"any_unop_type op τ σ ⟹
unop_type (Inl op) DotCall τ σ"
| "boolean_unop_type op τ σ ⟹
unop_type (Inr (Inl op)) DotCall τ σ"
| "numeric_unop_type op τ σ ⟹
unop_type (Inr (Inr (Inl op))) DotCall τ σ"
| "string_unop_type op τ σ ⟹
unop_type (Inr (Inr (Inr (Inl op)))) DotCall τ σ"
| "collection_unop_type op τ σ ⟹
unop_type (Inr (Inr (Inr (Inr op)))) ArrowCall τ σ"
inductive binop_type where
"super_binop_type op τ σ ρ ⟹
binop_type (Inl op) DotCall τ σ ρ"
| "boolean_binop_type op τ σ ρ ⟹
binop_type (Inr (Inl op)) DotCall τ σ ρ"
| "numeric_binop_type op τ σ ρ ⟹
binop_type (Inr (Inr (Inl op))) DotCall τ σ ρ"
| "string_binop_type op τ σ ρ ⟹
binop_type (Inr (Inr (Inr (Inl op)))) DotCall τ σ ρ"
| "collection_binop_type op τ σ ρ ⟹
binop_type (Inr (Inr (Inr (Inr op)))) ArrowCall τ σ ρ"
inductive ternop_type where
"string_ternop_type op τ σ ρ υ ⟹
ternop_type (Inl op) DotCall τ σ ρ υ"
| "collection_ternop_type op τ σ ρ υ ⟹
ternop_type (Inr op) ArrowCall τ σ ρ υ"
inductive op_type where
"unop_type op k τ υ ⟹
op_type (Inl op) k τ [] υ"
| "binop_type op k τ σ υ ⟹
op_type (Inr (Inl op)) k τ [σ] υ"
| "ternop_type op k τ σ ρ υ ⟹
op_type (Inr (Inr (Inl op))) k τ [σ, ρ] υ"
| "operation τ op π oper ⟹
op_type (Inr (Inr (Inr op))) DotCall τ π (oper_type oper)"
subsection ‹Simplification Rules›
inductive_simps op_type_alt_simps:
"mataop_type τ op σ"
"typeop_type k op τ σ ρ"
"op_type op k τ π σ"
"unop_type op k τ σ"
"binop_type op k τ σ ρ"
"ternop_type op k τ σ ρ υ"
"any_unop_type op τ σ"
"boolean_unop_type op τ σ"
"numeric_unop_type op τ σ"
"string_unop_type op τ σ"
"collection_unop_type op τ σ"
"super_binop_type op τ σ ρ"
"boolean_binop_type op τ σ ρ"
"numeric_binop_type op τ σ ρ"
"string_binop_type op τ σ ρ"
"collection_binop_type op τ σ ρ"
"string_ternop_type op τ σ ρ υ"
"collection_ternop_type op τ σ ρ υ"
subsection ‹Determinism›
lemma typeop_type_det:
"typeop_type op k τ σ ρ⇩1 ⟹
typeop_type op k τ σ ρ⇩2 ⟹ ρ⇩1 = ρ⇩2"
by (induct rule: typeop_type.induct;
auto simp add: typeop_type.simps update_element_type_det)
lemma any_unop_type_det:
"any_unop_type op τ σ⇩1 ⟹
any_unop_type op τ σ⇩2 ⟹ σ⇩1 = σ⇩2"
by (induct rule: any_unop_type.induct; simp add: any_unop_type.simps)
lemma boolean_unop_type_det:
"boolean_unop_type op τ σ⇩1 ⟹
boolean_unop_type op τ σ⇩2 ⟹ σ⇩1 = σ⇩2"
by (induct rule: boolean_unop_type.induct; simp add: boolean_unop_type.simps)
lemma numeric_unop_type_det:
"numeric_unop_type op τ σ⇩1 ⟹
numeric_unop_type op τ σ⇩2 ⟹ σ⇩1 = σ⇩2"
by (induct rule: numeric_unop_type.induct; auto simp add: numeric_unop_type.simps)
lemma string_unop_type_det:
"string_unop_type op τ σ⇩1 ⟹
string_unop_type op τ σ⇩2 ⟹ σ⇩1 = σ⇩2"
by (induct rule: string_unop_type.induct; simp add: string_unop_type.simps)
lemma collection_unop_type_det:
"collection_unop_type op τ σ⇩1 ⟹
collection_unop_type op τ σ⇩2 ⟹ σ⇩1 = σ⇩2"
apply (induct rule: collection_unop_type.induct)
by (erule collection_unop_type.cases;
auto simp add: element_type_det update_element_type_det)+
lemma unop_type_det:
"unop_type op k τ σ⇩1 ⟹
unop_type op k τ σ⇩2 ⟹ σ⇩1 = σ⇩2"
by (induct rule: unop_type.induct;
simp add: unop_type.simps any_unop_type_det
boolean_unop_type_det numeric_unop_type_det
string_unop_type_det collection_unop_type_det)
lemma super_binop_type_det:
"super_binop_type op τ σ ρ⇩1 ⟹
super_binop_type op τ σ ρ⇩2 ⟹ ρ⇩1 = ρ⇩2"
by (induct rule: super_binop_type.induct; auto simp add: super_binop_type.simps)
lemma boolean_binop_type_det:
"boolean_binop_type op τ σ ρ⇩1 ⟹
boolean_binop_type op τ σ ρ⇩2 ⟹ ρ⇩1 = ρ⇩2"
by (induct rule: boolean_binop_type.induct; simp add: boolean_binop_type.simps)
lemma numeric_binop_type_det:
"numeric_binop_type op τ σ ρ⇩1 ⟹
numeric_binop_type op τ σ ρ⇩2 ⟹ ρ⇩1 = ρ⇩2"
by (induct rule: numeric_binop_type.induct;
auto simp add: numeric_binop_type.simps split: if_splits)
lemma string_binop_type_det:
"string_binop_type op τ σ ρ⇩1 ⟹
string_binop_type op τ σ ρ⇩2 ⟹ ρ⇩1 = ρ⇩2"
by (induct rule: string_binop_type.induct; simp add: string_binop_type.simps)
lemma collection_binop_type_det:
"collection_binop_type op τ σ ρ⇩1 ⟹
collection_binop_type op τ σ ρ⇩2 ⟹ ρ⇩1 = ρ⇩2"
apply (induct rule: collection_binop_type.induct; simp add: collection_binop_type.simps)
using element_type_det update_element_type_det by blast+
lemma binop_type_det:
"binop_type op k τ σ ρ⇩1 ⟹
binop_type op k τ σ ρ⇩2 ⟹ ρ⇩1 = ρ⇩2"
by (induct rule: binop_type.induct;
simp add: binop_type.simps super_binop_type_det
boolean_binop_type_det numeric_binop_type_det
string_binop_type_det collection_binop_type_det)
lemma string_ternop_type_det:
"string_ternop_type op τ σ ρ υ⇩1 ⟹
string_ternop_type op τ σ ρ υ⇩2 ⟹ υ⇩1 = υ⇩2"
by (induct rule: string_ternop_type.induct; simp add: string_ternop_type.simps)
lemma collection_ternop_type_det:
"collection_ternop_type op τ σ ρ υ⇩1 ⟹
collection_ternop_type op τ σ ρ υ⇩2 ⟹ υ⇩1 = υ⇩2"
by (induct rule: collection_ternop_type.induct; simp add: collection_ternop_type.simps)
lemma ternop_type_det:
"ternop_type op k τ σ ρ υ⇩1 ⟹
ternop_type op k τ σ ρ υ⇩2 ⟹ υ⇩1 = υ⇩2"
by (induct rule: ternop_type.induct;
simp add: ternop_type.simps string_ternop_type_det collection_ternop_type_det)
lemma op_type_det:
"op_type op k τ π σ ⟹
op_type op k τ π ρ ⟹ σ = ρ"
apply (induct rule: op_type.induct)
apply (erule op_type.cases; simp add: unop_type_det)
apply (erule op_type.cases; simp add: binop_type_det)
apply (erule op_type.cases; simp add: ternop_type_det)
by (erule op_type.cases; simp; metis operation_det)
section ‹Expressions Typing›
text ‹
The following typing rules are preliminary. The final rules are given at
the end of the next chapter.›
inductive typing :: "('a :: ocl_object_model) type env ⇒ 'a expr ⇒ 'a type ⇒ bool"
("(1_/ ⊢⇩E/ (_ :/ _))" [51,51,51] 50)
and collection_parts_typing ("(1_/ ⊢⇩C/ (_ :/ _))" [51,51,51] 50)
and collection_part_typing ("(1_/ ⊢⇩P/ (_ :/ _))" [51,51,51] 50)
and iterator_typing ("(1_/ ⊢⇩I/ (_ :/ _))" [51,51,51] 50)
and expr_list_typing ("(1_/ ⊢⇩L/ (_ :/ _))" [51,51,51] 50) where
NullLiteralT:
"Γ ⊢⇩E NullLiteral : OclVoid[?]"
|BooleanLiteralT:
"Γ ⊢⇩E BooleanLiteral c : Boolean[1]"
|RealLiteralT:
"Γ ⊢⇩E RealLiteral c : Real[1]"
|IntegerLiteralT:
"Γ ⊢⇩E IntegerLiteral c : Integer[1]"
|UnlimitedNaturalLiteralT:
"Γ ⊢⇩E UnlimitedNaturalLiteral c : UnlimitedNatural[1]"
|StringLiteralT:
"Γ ⊢⇩E StringLiteral c : String[1]"
|EnumLiteralT:
"has_literal enum lit ⟹
Γ ⊢⇩E EnumLiteral enum lit : (Enum enum)[1]"
|SetLiteralT:
"Γ ⊢⇩C prts : τ ⟹
Γ ⊢⇩E CollectionLiteral SetKind prts : Set τ"
|OrderedSetLiteralT:
"Γ ⊢⇩C prts : τ ⟹
Γ ⊢⇩E CollectionLiteral OrderedSetKind prts : OrderedSet τ"
|BagLiteralT:
"Γ ⊢⇩C prts : τ ⟹
Γ ⊢⇩E CollectionLiteral BagKind prts : Bag τ"
|SequenceLiteralT:
"Γ ⊢⇩C prts : τ ⟹
Γ ⊢⇩E CollectionLiteral SequenceKind prts : Sequence τ"
|CollectionPartsSingletonT:
"Γ ⊢⇩P x : τ ⟹
Γ ⊢⇩C [x] : τ"
|CollectionPartsListT:
"Γ ⊢⇩P x : τ ⟹
Γ ⊢⇩C y # xs : σ ⟹
Γ ⊢⇩C x # y # xs : τ ⊔ σ"
|CollectionPartItemT:
"Γ ⊢⇩E a : τ ⟹
Γ ⊢⇩P CollectionItem a : τ"
|CollectionPartRangeT:
"Γ ⊢⇩E a : τ ⟹
Γ ⊢⇩E b : σ ⟹
τ = UnlimitedNatural[1]─Integer[1] ⟹
σ = UnlimitedNatural[1]─Integer[1] ⟹
Γ ⊢⇩P CollectionRange a b : Integer[1]"
|TupleLiteralNilT:
"Γ ⊢⇩E TupleLiteral [] : Tuple fmempty"
|TupleLiteralConsT:
"Γ ⊢⇩E TupleLiteral elems : Tuple ξ ⟹
Γ ⊢⇩E tuple_element_expr el : τ ⟹
tuple_element_type el = Some σ ⟹
τ ≤ σ ⟹
Γ ⊢⇩E TupleLiteral (el # elems) : Tuple (ξ(tuple_element_name el ↦⇩f σ))"
|LetT:
"Γ ⊢⇩E init : σ ⟹
σ ≤ τ ⟹
Γ(v ↦⇩f τ) ⊢⇩E body : ρ ⟹
Γ ⊢⇩E Let v (Some τ) init body : ρ"
|VarT:
"fmlookup Γ v = Some τ ⟹
Γ ⊢⇩E Var v : τ"
|IfT:
"Γ ⊢⇩E a : Boolean[1] ⟹
Γ ⊢⇩E b : σ ⟹
Γ ⊢⇩E c : ρ ⟹
Γ ⊢⇩E If a b c : σ ⊔ ρ"
|MetaOperationCallT:
"mataop_type τ op σ ⟹
Γ ⊢⇩E MetaOperationCall τ op : σ"
|StaticOperationCallT:
"Γ ⊢⇩L params : π ⟹
static_operation τ op π oper ⟹
Γ ⊢⇩E StaticOperationCall τ op params : oper_type oper"
|TypeOperationCallT:
"Γ ⊢⇩E a : τ ⟹
typeop_type k op τ σ ρ ⟹
Γ ⊢⇩E TypeOperationCall a k op σ : ρ"
|AttributeCallT:
"Γ ⊢⇩E src : ⟨𝒞⟩⇩𝒯[1] ⟹
attribute 𝒞 prop 𝒟 τ ⟹
Γ ⊢⇩E AttributeCall src DotCall prop : τ"
|AssociationEndCallT:
"Γ ⊢⇩E src : ⟨𝒞⟩⇩𝒯[1] ⟹
association_end 𝒞 from role 𝒟 end ⟹
Γ ⊢⇩E AssociationEndCall src DotCall from role : assoc_end_type end"
|AssociationClassCallT:
"Γ ⊢⇩E src : ⟨𝒞⟩⇩𝒯[1] ⟹
referred_by_association_class 𝒞 from 𝒜 𝒟 ⟹
Γ ⊢⇩E AssociationClassCall src DotCall from 𝒜 : class_assoc_type 𝒜"
|AssociationClassEndCallT:
"Γ ⊢⇩E src : ⟨𝒜⟩⇩𝒯[1] ⟹
association_class_end 𝒜 role end ⟹
Γ ⊢⇩E AssociationClassEndCall src DotCall role : class_assoc_end_type end"
|OperationCallT:
"Γ ⊢⇩E src : τ ⟹
Γ ⊢⇩L params : π ⟹
op_type op k τ π σ ⟹
Γ ⊢⇩E OperationCall src k op params : σ"
|TupleElementCallT:
"Γ ⊢⇩E src : Tuple π ⟹
fmlookup π elem = Some τ ⟹
Γ ⊢⇩E TupleElementCall src DotCall elem : τ"
|IteratorT:
"Γ ⊢⇩E src : τ ⟹
element_type τ σ ⟹
σ ≤ its_ty ⟹
Γ ++⇩f fmap_of_list (map (λit. (it, its_ty)) its) ⊢⇩E body : ρ ⟹
Γ ⊢⇩I (src, its, (Some its_ty), body) : (τ, σ, ρ)"
|IterateT:
"Γ ⊢⇩I (src, its, its_ty, Let res (Some res_t) res_init body) : (τ, σ, ρ) ⟹
ρ ≤ res_t ⟹
Γ ⊢⇩E IterateCall src ArrowCall its its_ty res (Some res_t) res_init body : ρ"
|AnyIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
ρ ≤ Boolean[?] ⟹
Γ ⊢⇩E AnyIteratorCall src ArrowCall its its_ty body : σ"
|ClosureIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
to_single_type ρ ≤ σ ⟹
to_unique_collection τ υ ⟹
Γ ⊢⇩E ClosureIteratorCall src ArrowCall its its_ty body : υ"
|CollectIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
to_nonunique_collection τ υ ⟹
update_element_type υ (to_single_type ρ) φ ⟹
Γ ⊢⇩E CollectIteratorCall src ArrowCall its its_ty body : φ"
|CollectNestedIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
to_nonunique_collection τ υ ⟹
update_element_type υ ρ φ ⟹
Γ ⊢⇩E CollectNestedIteratorCall src ArrowCall its its_ty body : φ"
|ExistsIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
ρ ≤ Boolean[?] ⟹
Γ ⊢⇩E ExistsIteratorCall src ArrowCall its its_ty body : ρ"
|ForAllIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
ρ ≤ Boolean[?] ⟹
Γ ⊢⇩E ForAllIteratorCall src ArrowCall its its_ty body : ρ"
|OneIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
ρ ≤ Boolean[?] ⟹
Γ ⊢⇩E OneIteratorCall src ArrowCall its its_ty body : Boolean[1]"
|IsUniqueIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
Γ ⊢⇩E IsUniqueIteratorCall src ArrowCall its its_ty body : Boolean[1]"
|SelectIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
ρ ≤ Boolean[?] ⟹
Γ ⊢⇩E SelectIteratorCall src ArrowCall its its_ty body : τ"
|RejectIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
ρ ≤ Boolean[?] ⟹
Γ ⊢⇩E RejectIteratorCall src ArrowCall its its_ty body : τ"
|SortedByIteratorT:
"Γ ⊢⇩I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
length its ≤ 1 ⟹
to_ordered_collection τ υ ⟹
Γ ⊢⇩E SortedByIteratorCall src ArrowCall its its_ty body : υ"
|ExprListNilT:
"Γ ⊢⇩L [] : []"
|ExprListConsT:
"Γ ⊢⇩E expr : τ ⟹
Γ ⊢⇩L exprs : π ⟹
Γ ⊢⇩L expr # exprs : τ # π"
section ‹Elimination Rules›
inductive_cases NullLiteralTE [elim]: "Γ ⊢⇩E NullLiteral : τ"
inductive_cases BooleanLiteralTE [elim]: "Γ ⊢⇩E BooleanLiteral c : τ"
inductive_cases RealLiteralTE [elim]: "Γ ⊢⇩E RealLiteral c : τ"
inductive_cases IntegerLiteralTE [elim]: "Γ ⊢⇩E IntegerLiteral c : τ"
inductive_cases UnlimitedNaturalLiteralTE [elim]: "Γ ⊢⇩E UnlimitedNaturalLiteral c : τ"
inductive_cases StringLiteralTE [elim]: "Γ ⊢⇩E StringLiteral c : τ"
inductive_cases EnumLiteralTE [elim]: "Γ ⊢⇩E EnumLiteral enm lit : τ"
inductive_cases CollectionLiteralTE [elim]: "Γ ⊢⇩E CollectionLiteral k prts : τ"
inductive_cases TupleLiteralTE [elim]: "Γ ⊢⇩E TupleLiteral elems : τ"
inductive_cases LetTE [elim]: "Γ ⊢⇩E Let v τ init body : σ"
inductive_cases VarTE [elim]: "Γ ⊢⇩E Var v : τ"
inductive_cases IfTE [elim]: "Γ ⊢⇩E If a b c : τ"
inductive_cases MetaOperationCallTE [elim]: "Γ ⊢⇩E MetaOperationCall τ op : σ"
inductive_cases StaticOperationCallTE [elim]: "Γ ⊢⇩E StaticOperationCall τ op as : σ"
inductive_cases TypeOperationCallTE [elim]: "Γ ⊢⇩E TypeOperationCall a k op σ : τ"
inductive_cases AttributeCallTE [elim]: "Γ ⊢⇩E AttributeCall src k prop : τ"
inductive_cases AssociationEndCallTE [elim]: "Γ ⊢⇩E AssociationEndCall src k role from : τ"
inductive_cases AssociationClassCallTE [elim]: "Γ ⊢⇩E AssociationClassCall src k a from : τ"
inductive_cases AssociationClassEndCallTE [elim]: "Γ ⊢⇩E AssociationClassEndCall src k role : τ"
inductive_cases OperationCallTE [elim]: "Γ ⊢⇩E OperationCall src k op params : τ"
inductive_cases TupleElementCallTE [elim]: "Γ ⊢⇩E TupleElementCall src k elem : τ"
inductive_cases IteratorTE [elim]: "Γ ⊢⇩I (src, its, body) : ys"
inductive_cases IterateTE [elim]: "Γ ⊢⇩E IterateCall src k its its_ty res res_t res_init body : τ"
inductive_cases AnyIteratorTE [elim]: "Γ ⊢⇩E AnyIteratorCall src k its its_ty body : τ"
inductive_cases ClosureIteratorTE [elim]: "Γ ⊢⇩E ClosureIteratorCall src k its its_ty body : τ"
inductive_cases CollectIteratorTE [elim]: "Γ ⊢⇩E CollectIteratorCall src k its its_ty body : τ"
inductive_cases CollectNestedIteratorTE [elim]: "Γ ⊢⇩E CollectNestedIteratorCall src k its its_ty body : τ"
inductive_cases ExistsIteratorTE [elim]: "Γ ⊢⇩E ExistsIteratorCall src k its its_ty body : τ"
inductive_cases ForAllIteratorTE [elim]: "Γ ⊢⇩E ForAllIteratorCall src k its its_ty body : τ"
inductive_cases OneIteratorTE [elim]: "Γ ⊢⇩E OneIteratorCall src k its its_ty body : τ"
inductive_cases IsUniqueIteratorTE [elim]: "Γ ⊢⇩E IsUniqueIteratorCall src k its its_ty body : τ"
inductive_cases SelectIteratorTE [elim]: "Γ ⊢⇩E SelectIteratorCall src k its its_ty body : τ"
inductive_cases RejectIteratorTE [elim]: "Γ ⊢⇩E RejectIteratorCall src k its its_ty body : τ"
inductive_cases SortedByIteratorTE [elim]: "Γ ⊢⇩E SortedByIteratorCall src k its its_ty body : τ"
inductive_cases CollectionPartsNilTE [elim]: "Γ ⊢⇩C [x] : τ"
inductive_cases CollectionPartsItemTE [elim]: "Γ ⊢⇩C x # y # xs : τ"
inductive_cases CollectionItemTE [elim]: "Γ ⊢⇩P CollectionItem a : τ"
inductive_cases CollectionRangeTE [elim]: "Γ ⊢⇩P CollectionRange a b : τ"
inductive_cases ExprListTE [elim]: "Γ ⊢⇩L exprs : π"
section ‹Simplification Rules›
inductive_simps typing_alt_simps:
"Γ ⊢⇩E NullLiteral : τ"
"Γ ⊢⇩E BooleanLiteral c : τ"
"Γ ⊢⇩E RealLiteral c : τ"
"Γ ⊢⇩E UnlimitedNaturalLiteral c : τ"
"Γ ⊢⇩E IntegerLiteral c : τ"
"Γ ⊢⇩E StringLiteral c : τ"
"Γ ⊢⇩E EnumLiteral enm lit : τ"
"Γ ⊢⇩E CollectionLiteral k prts : τ"
"Γ ⊢⇩E TupleLiteral [] : τ"
"Γ ⊢⇩E TupleLiteral (x # xs) : τ"
"Γ ⊢⇩E Let v τ init body : σ"
"Γ ⊢⇩E Var v : τ"
"Γ ⊢⇩E If a b c : τ"
"Γ ⊢⇩E MetaOperationCall τ op : σ"
"Γ ⊢⇩E StaticOperationCall τ op as : σ"
"Γ ⊢⇩E TypeOperationCall a k op σ : τ"
"Γ ⊢⇩E AttributeCall src k prop : τ"
"Γ ⊢⇩E AssociationEndCall src k role from : τ"
"Γ ⊢⇩E AssociationClassCall src k a from : τ"
"Γ ⊢⇩E AssociationClassEndCall src k role : τ"
"Γ ⊢⇩E OperationCall src k op params : τ"
"Γ ⊢⇩E TupleElementCall src k elem : τ"
"Γ ⊢⇩I (src, its, body) : ys"
"Γ ⊢⇩E IterateCall src k its its_ty res res_t res_init body : τ"
"Γ ⊢⇩E AnyIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E ClosureIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E CollectIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E CollectNestedIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E ExistsIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E ForAllIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E OneIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E IsUniqueIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E SelectIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E RejectIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩E SortedByIteratorCall src k its its_ty body : τ"
"Γ ⊢⇩C [x] : τ"
"Γ ⊢⇩C x # y # xs : τ"
"Γ ⊢⇩P CollectionItem a : τ"
"Γ ⊢⇩P CollectionRange a b : τ"
"Γ ⊢⇩L [] : π"
"Γ ⊢⇩L x # xs : π"
section ‹Determinism›
lemma
typing_det:
"Γ ⊢⇩E expr : τ ⟹
Γ ⊢⇩E expr : σ ⟹ τ = σ" and
collection_parts_typing_det:
"Γ ⊢⇩C prts : τ ⟹
Γ ⊢⇩C prts : σ ⟹ τ = σ" and
collection_part_typing_det:
"Γ ⊢⇩P prt : τ ⟹
Γ ⊢⇩P prt : σ ⟹ τ = σ" and
iterator_typing_det:
"Γ ⊢⇩I (src, its, body) : xs ⟹
Γ ⊢⇩I (src, its, body) : ys ⟹ xs = ys" and
expr_list_typing_det:
"Γ ⊢⇩L exprs : π ⟹
Γ ⊢⇩L exprs : ξ ⟹ π = ξ"
proof (induct arbitrary: σ and σ and σ and ys and ξ
rule: typing_collection_parts_typing_collection_part_typing_iterator_typing_expr_list_typing.inducts)
case (NullLiteralT Γ) thus ?case by auto
next
case (BooleanLiteralT Γ c) thus ?case by auto
next
case (RealLiteralT Γ c) thus ?case by auto
next
case (IntegerLiteralT Γ c) thus ?case by auto
next
case (UnlimitedNaturalLiteralT Γ c) thus ?case by auto
next
case (StringLiteralT Γ c) thus ?case by auto
next
case (EnumLiteralT Γ τ lit) thus ?case by auto
next
case (SetLiteralT Γ prts τ) thus ?case by blast
next
case (OrderedSetLiteralT Γ prts τ) thus ?case by blast
next
case (BagLiteralT Γ prts τ) thus ?case by blast
next
case (SequenceLiteralT Γ prts τ) thus ?case by blast
next
case (CollectionPartsSingletonT Γ x τ) thus ?case by blast
next
case (CollectionPartsListT Γ x τ y xs σ) thus ?case by blast
next
case (CollectionPartItemT Γ a τ) thus ?case by blast
next
case (CollectionPartRangeT Γ a τ b σ) thus ?case by blast
next
case (TupleLiteralNilT Γ) thus ?case by auto
next
case (TupleLiteralConsT Γ elems ξ el τ) show ?case
apply (insert TupleLiteralConsT.prems)
apply (erule TupleLiteralTE, simp)
using TupleLiteralConsT.hyps by auto
next
case (LetT Γ ℳ init σ τ v body ρ) thus ?case by blast
next
case (VarT Γ v τ ℳ) thus ?case by auto
next
case (IfT Γ a τ b σ c ρ) thus ?case
apply (insert IfT.prems)
apply (erule IfTE)
by (simp add: IfT.hyps)
next
case (MetaOperationCallT τ op σ Γ) thus ?case
by (metis MetaOperationCallTE mataop_type.cases)
next
case (StaticOperationCallT τ op π oper Γ as) thus ?case
apply (insert StaticOperationCallT.prems)
apply (erule StaticOperationCallTE)
using StaticOperationCallT.hyps static_operation_det by blast
next
case (TypeOperationCallT Γ a τ op σ ρ) thus ?case
by (metis TypeOperationCallTE typeop_type_det)
next
case (AttributeCallT Γ src τ 𝒞 "prop" 𝒟 σ) show ?case
apply (insert AttributeCallT.prems)
apply (erule AttributeCallTE)
using AttributeCallT.hyps attribute_det by blast
next
case (AssociationEndCallT Γ src 𝒞 "from" role 𝒟 "end") show ?case
apply (insert AssociationEndCallT.prems)
apply (erule AssociationEndCallTE)
using AssociationEndCallT.hyps association_end_det by blast
next
case (AssociationClassCallT Γ src 𝒞 "from" 𝒜) thus ?case by blast
next
case (AssociationClassEndCallT Γ src τ 𝒜 role "end") show ?case
apply (insert AssociationClassEndCallT.prems)
apply (erule AssociationClassEndCallTE)
using AssociationClassEndCallT.hyps association_class_end_det by blast
next
case (OperationCallT Γ src τ params π op k) show ?case
apply (insert OperationCallT.prems)
apply (erule OperationCallTE)
using OperationCallT.hyps op_type_det by blast
next
case (TupleElementCallT Γ src π elem τ) thus ?case
apply (insert TupleElementCallT.prems)
apply (erule TupleElementCallTE)
using TupleElementCallT.hyps by fastforce
next
case (IteratorT Γ src τ σ its_ty its body ρ) show ?case
apply (insert IteratorT.prems)
apply (erule IteratorTE)
using IteratorT.hyps element_type_det by blast
next
case (IterateT Γ src its its_ty res res_t res_init body τ σ ρ) show ?case
apply (insert IterateT.prems)
using IterateT.hyps by blast
next
case (AnyIteratorT Γ src its its_ty body τ σ ρ) thus ?case
by (meson AnyIteratorTE Pair_inject)
next
case (ClosureIteratorT Γ src its its_ty body τ σ ρ υ) show ?case
apply (insert ClosureIteratorT.prems)
apply (erule ClosureIteratorTE)
using ClosureIteratorT.hyps to_unique_collection_det by blast
next
case (CollectIteratorT Γ src its its_ty body τ σ ρ υ) show ?case
apply (insert CollectIteratorT.prems)
apply (erule CollectIteratorTE)
using CollectIteratorT.hyps to_nonunique_collection_det
update_element_type_det Pair_inject by metis
next
case (CollectNestedIteratorT Γ src its its_ty body τ σ ρ υ) show ?case
apply (insert CollectNestedIteratorT.prems)
apply (erule CollectNestedIteratorTE)
using CollectNestedIteratorT.hyps to_nonunique_collection_det
update_element_type_det Pair_inject by metis
next
case (ExistsIteratorT Γ src its its_ty body τ σ ρ) show ?case
apply (insert ExistsIteratorT.prems)
apply (erule ExistsIteratorTE)
using ExistsIteratorT.hyps Pair_inject by metis
next
case (ForAllIteratorT Γ ℳ src its its_ty body τ σ ρ) show ?case
apply (insert ForAllIteratorT.prems)
apply (erule ForAllIteratorTE)
using ForAllIteratorT.hyps Pair_inject by metis
next
case (OneIteratorT Γ ℳ src its its_ty body τ σ ρ) show ?case
apply (insert OneIteratorT.prems)
apply (erule OneIteratorTE)
by simp
next
case (IsUniqueIteratorT Γ ℳ src its its_ty body τ σ ρ) show ?case
apply (insert IsUniqueIteratorT.prems)
apply (erule IsUniqueIteratorTE)
by simp
next
case (SelectIteratorT Γ ℳ src its its_ty body τ σ ρ) show ?case
apply (insert SelectIteratorT.prems)
apply (erule SelectIteratorTE)
using SelectIteratorT.hyps by blast
next
case (RejectIteratorT Γ ℳ src its its_ty body τ σ ρ) show ?case
apply (insert RejectIteratorT.prems)
apply (erule RejectIteratorTE)
using RejectIteratorT.hyps by blast
next
case (SortedByIteratorT Γ ℳ src its its_ty body τ σ ρ υ) show ?case
apply (insert SortedByIteratorT.prems)
apply (erule SortedByIteratorTE)
using SortedByIteratorT.hyps to_ordered_collection_det by blast
next
case (ExprListNilT Γ) thus ?case
using expr_list_typing.cases by auto
next
case (ExprListConsT Γ expr τ exprs π) show ?case
apply (insert ExprListConsT.prems)
apply (erule ExprListTE)
by (simp_all add: ExprListConsT.hyps)
qed
section ‹Code Setup›