Theory IDE_CP_Applications1

chapter β€ΉIDE-CP Functions \& Applications - Part Iβ€Ί


theory IDE_CP_Applications1
  imports IDE_CP_Core
  keywords "val" :: quasi_command
  abbrevs "<orelse>" = "π—ˆπ—‹π–Ύπ—…π—Œπ–Ύ"
      and "<pattern>" = "𝗉𝖺𝗍𝗍𝖾𝗋𝗇"
      and "<traverse>" = "π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ"
      and "<split>" = "π—Œπ—‰π—…π—‚π—"
      and "<strip>" = "π—Œπ—π—‹π—‚π—‰"
      and "<then>" = "𝗍𝗁𝖾𝗇"
      and "<commute>" = "π–Όπ—ˆπ—†π—†π—Žπ—π–Ύ"
      and "<bubbling>" = "π–»π—Žπ–»π–»π—…π—‚π—‡π—€"
      and "<assoc>" = "π–Ίπ—Œπ—Œπ—ˆπ–Ό"
      and "<scalar>" = "π—Œπ–Όπ–Ίπ—…π–Ίπ—‹"
      and "<open>" = "π—ˆπ—‰π–Ύπ—‡"
      and "<makes>" = "π—†π–Ίπ—„π–Ύπ—Œ"
begin

text β€Ή 

Note: Our reasoning is a calculus of sequents, but not the sequent calculus.
      The propβ€ΉX π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Yβ€Ί is a sequent β€ΉX ⊒ Yβ€Ί.
TODO: Maybe we should rename the word 'sequent' in MLs to 'state' as it is proof state instead of a sequent.

TODO: move me somewhere

There are essentially two transformation mechanism in the system, βˆƒ-free ToA and the To-Transformation.

βˆƒ-free ToA is the major reasoning process in the system. It is between BI assertions and limited in
introducing existential quantification, i.e., it cannot open an abstraction.
This limitation is reasonable and also due to technical reasons.

When a transformation from β€Ήx ⦂ Tβ€Ί introduces existentially quantification, e.g., to β€Ή{ y ⦂ U |y. P y }β€Ί,
it opens the abstraction of β€Ήx ⦂ Tβ€Ί.
The β€Ήxβ€Ί has no enough information to determine a unique value of β€Ήyβ€Ί but only a set of candidates,
which means the representation of β€Ήy ⦂ Uβ€Ί is more specific and therefore in a lower abstraction level.
For example, β€Ήx ⦂ Qβ€Ί is a rational number and β€Ή{ (a,b) ⦂ β„€ Γ— β„€ |a b. a/b = x }β€Ί is its representation.

As the major reasoning process in the system, the ToA reasoning should maintain the abstraction level,
and degenerate to a lower abstraction only when users ask so.
Reducing to a lower abstraction, should only happen when building the interfaces or internal
operations of the data structure.
Manually writing two annotations to open and to close the abstraction at the beginning and the ending
of the building of the interface, does not bring any thinking burden to users because the users of course
know, he is going to enter the representation of the abstraction in order to make the internal operation.
To-Transformation has capability to open an abstraction, as it supports the transformation introducing
existential quantification.

The technical difficulty to support introducing existential quantification is that, we instantiate
the existential quantification in the right side of a transformation goal to schematic variables
that can be instantiated to whatever later, so that we can enter the existential quantification
in the right and let the inner structure guide the next reasoning (like a goal-directed proof search).
The existential quantification at the left side is fixed before instantiating those in the right,
so the schematic variable can capture, i.e., can instantiate to any expression containing the fixed
existentially quantified variable of the left.
However, later when an existential quantification is introduced at the left side after
the instantiation of the right, the schematic variables cannot capture the new introduced existentially
quantified variables.
It is a deficiency of the current reasoning because it should not instantiate the right existential
quantification that early, but if we remain them, the quantifier brings a lot of troubles in the pattern
matching and the resolution of Ο†-LPR. Just like the meta universal quantifier is specially processed
by the resolution of Isabelle's kernel, the handling of the existential quantification should also
be integrated in our resolution kernel, but it is hard and the performance would be a problem as
we cannot enter the kernel as what Isabelle's resolution does.

The expected resolution:
β€ΉA a ⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y aβ€Ί    β€ΉX π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ βˆƒa. Y a ⟹ Bβ€Ί
-------------------------------------------------------
                    β€Ήβˆƒa. A a ⟹ Bβ€Ί


The To-Transformation is about a single Ο†-type term β€Ήx ⦂ Tβ€Ί. Given a Ο†-type β€ΉUβ€Ί, it transforms β€Ήx ⦂ Tβ€Ί
to a Ο†-type term β€Ήy ⦂ Uβ€Ί with whatever β€Ήyβ€Ί it could be, or even a set β€Ή{ y ⦂ U | y. P y }β€Ί.


-------------------------------------------------------------------------------------

ToA reasoning in the system by default does not change the abstraction level. Therefore, they are
writen in a function form β€Ήx ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ f(x) ⦂ Uβ€Ί instead of a relation form
β€Ήx ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. r yβ€Ί. We also call this function form β€Ήβˆƒβ€Ί-free ToA.

To open an abstraction, you can use To-Transformation:

    β–©β€Ήto β€ΉList OPENβ€Ίβ€Ί, in order to open β€ΉList Tβ€Ί into β€ΉList Repβ€Ί
    you can also use β–©β€Ήopen_abstraction β€ΉList _β€Ίβ€Ί which is a syntax sugar of β€Ήto β€ΉList OPENβ€Ίβ€Ί

To make an abstraction, just give the desired form and it invokes the synthesis process,

    β–©β€Ή β€Ή_ ⦂ MAKE Uβ€Ί β€Ί

Note you should not use To-Transformation to make an abstraction if the target β€ΉUβ€Ί that you want to make
requires to be assembled from more than one Ο†-type terms. It is because To-Transformation is used
to transform the first Ο†-type term β€Ήx ⦂ Tβ€Ί on your state sequent to whatever.
It considers the first Ο†-type term only.


--------------------------------------------------------------------------------------

Ο†-system provides 5 syntax to annotate Ο†-types, or in another words, to invoke transformation.

β–ͺ to β€Ήthe target Ο†-type you wantβ€Ί, it transforms the leading Ο†-type term β€Ήx ⦂ Tβ€Ί to β€Ή{ y ⦂ U |y. P y}β€Ί
                                   for the given β€ΉUβ€Ί and a set of object β€Ήyβ€Ί it can be.
                                   It can also generate program code to achieve the target.
                                   For example, if the leading term is β€Ήx ⦂ β„•β€Ί, the β€Ήto Floatβ€Ί can
                                   generate the program casting the integer.
β–ͺ is β€Ήthe expected objectβ€Ί, it transforms the leading Ο†-type term β€Ήx ⦂ Tβ€Ί to β€Ήy ⦂ Tβ€Ί for the given y.
β–ͺ as β€Ήthe expected object ⦂ the target Ο†-typeβ€Ί, as β€Ήy ⦂ Uβ€Ί is a syntax sugar of
                                   β–©β€Ήto Uβ€Ί followed by β–©β€Ήis yβ€Ί.
β–ͺ assert β€ΉBI assertionβ€Ί, asserts the entire of the current state is what. It is pure transformation
                         and never generates code.
β–ͺ β€Ήx ⦂ Tβ€Ί, (directly giving a BI assertion without a leading keyword),
           synthesis β€Ήx ⦂ Tβ€Ί using whatever terms in the current state.
           It may generate program code.
β€Ί


section β€ΉConventionβ€Ί

text β€ΉPriority:

β–ͺ 59: Fallback of Make Abstraction
β€Ί

section β€ΉElements of Actionsβ€Ί

subsubsection β€ΉActions only for implication onlyβ€Ί

consts π’œ_transformation :: β€Ήaction β‡’ actionβ€Ί

declare [[Ο†reason_default_pattern
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_transformation _β€Ί β‡’
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_transformation _β€Ί    (100)
  and β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ  _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_transformation _β€Ί β‡’
      β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ  _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_transformation _β€Ί    (100)
]]

lemma [Ο†reason 1010]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ_transformation actionβ€Ί
  unfolding Action_Tag_def
  using view_shift_by_implication .

lemma [Ο†reason 1000]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ_transformation actionβ€Ί
  unfolding Action_Tag_def .

lemma [Ο†reason 1100]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ PROP Do_Action (π’œ_transformation action)
      (Trueprop (CurrentConstruction mode s H X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ CurrentConstruction mode s H Y ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Action_Tag_def
  using Ο†apply_implication by blast

lemma [Ο†reason 1100]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ PROP Do_Action (π’œ_transformation action)
      (Trueprop (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ Y) ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Transformation_def ToA_Construction_def
  by blast


subsubsection β€ΉView Shiftβ€Ί

consts π’œ_view_shift_or_imp :: β€Ήaction β‡’ actionβ€Ί

lemma [Ο†reason 1100]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ PROP Do_Action (π’œ_view_shift_or_imp action)
      (Trueprop (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ Y) ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Transformation_def ToA_Construction_def
  by blast

lemma do_π’œ_view_shift_or_imp_VS:
  β€Ή X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ PROP Do_Action (π’œ_view_shift_or_imp action)
      (Trueprop (CurrentConstruction mode s H X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ CurrentConstruction mode s H Y ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Action_Tag_def
  using Ο†apply_view_shift by blast

lemma do_π’œ_view_shift_or_imp_VS_degrade:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ PROP Do_Action (π’œ_view_shift_or_imp action)
      (Trueprop (CurrentConstruction mode s H X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ CurrentConstruction mode s H Y ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Action_Tag_def
  using Ο†apply_implication by blast

declare [[Ο†reason 1100 do_π’œ_view_shift_or_imp_VS do_π’œ_view_shift_or_imp_VS_degrade
      for β€ΉPROP Do_Action (π’œ_view_shift_or_imp ?action)
                (Trueprop (CurrentConstruction ?mode ?s ?H ?X))
                (PROP ?Result)β€Ί]]

hide_fact do_π’œ_view_shift_or_imp_VS do_π’œ_view_shift_or_imp_VS_degrade


subsubsection β€ΉMorphismβ€Ί

consts π’œ_morphism :: β€Ήaction β‡’ actionβ€Ί

lemma [Ο†reason 1100]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ
⟹ PROP Do_Action (π’œ_morphism π’œ)
      (Trueprop (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ (π–Ίπ–»π—Œπ—π—‹π–Ίπ–Όπ—π—‚π—ˆπ—‡(s) π—‚π—Œ Y) ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Transformation_def ToA_Construction_def
  by blast

context begin

private lemma do_π’œ_morphism_proc:
  β€Ή π—‰π—‹π—ˆπ–Ό f ⦃ S ⟼ T' ⦄ π—π—π—‹π—ˆπ—π—Œ E' @tag π’œ
⟹ PROP Do_Action (π’œ_morphism π’œ)
      (Trueprop (π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 S))
      ( π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True
        ⟹ PROP Ο†Application (Trueprop (π—‰π—‹π—ˆπ–Ό f ⦃ S ⟼ T' ⦄ π—π—π—‹π—ˆπ—π—Œ E' ))
                               (Trueprop (π–Όπ—Žπ—‹π—‹π–Ύπ—‡π— blk [H] π—‹π–Ύπ—Œπ—Žπ—…π—π—Œ 𝗂𝗇 S)) (PROP Result)
        ⟹ PROP Result) β€Ί
  unfolding Do_Action_def Action_Tag_def Ο†Application_def
  subgoal premises prems
    by (rule prems(4), rule prems(2), rule prems(1)) .

private lemma do_π’œ_morphism_VS:
  β€Ή X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ
⟹ PROP Do_Action (π’œ_morphism π’œ)
      (Trueprop (CurrentConstruction mode s H X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ CurrentConstruction mode s H Y ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Action_Tag_def
  using Ο†apply_view_shift by blast

private lemma do_π’œ_morphism_ToA:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag action
⟹ PROP Do_Action (π’œ_morphism action)
      (Trueprop (CurrentConstruction mode s H X))
      (π—ˆπ–»π—…π—‚π—€π–Ίπ—π—‚π—ˆπ—‡ True ⟹ CurrentConstruction mode s H Y ∧ P )β€Ί
  unfolding Do_Action_def Action_Tag_def Action_Tag_def
  using Ο†apply_implication by blast

declare [[Ο†reason 1100 do_π’œ_morphism_proc do_π’œ_morphism_VS do_π’œ_morphism_ToA
      for β€ΉPROP Do_Action (π’œ_morphism ?action)
                (Trueprop (CurrentConstruction ?mode ?s ?H ?X))
                (PROP ?Result)β€Ί]]

end


subsubsection β€ΉNap, a space for injectionβ€Ί

consts π’œnap :: β€Ήaction β‡’ actionβ€Ί

lemma [Ο†reason 10]:
  β€Ή P @tag A
⟹ P @tag π’œnap Aβ€Ί
  unfolding Action_Tag_def .

subsubsection β€ΉActions for β€Ήβˆƒβˆ§β€Ί-free MTFβ€Ί

consts π’œ_simple_MTF :: β€Ήaction β‡’ actionβ€Ί

declare [[Ο†reason_default_pattern
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_simple_MTF _β€Ί β‡’
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_simple_MTF _β€Ί    (100)
  and β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ  _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_simple_MTF _β€Ί β‡’
      β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ  _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_simple_MTF _β€Ί    (100)
]]

paragraph β€ΉImplicationβ€Ί

lemma [Ο†reason 1010]:
  β€Ή (π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ Q ⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF A)
⟹ X π—Œπ—Žπ–»π—ƒ Q π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y π—Œπ—Žπ–»π—ƒ Q 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF Aβ€Ί
  unfolding Action_Tag_def Transformation_def
  by (simp, blast)

lemma [Ο†reason 1010]:
  β€Ή (β‹€x. X x π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y x 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF A)
⟹ ExBI X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ ExBI Y 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF Aβ€Ί
  unfolding Action_Tag_def Transformation_def
  by (simp, blast)

paragraph β€ΉView Shiftβ€Ί

lemma [Ο†reason 1010]:
  β€Ή (π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ Q ⟹ X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF A)
⟹ X π—Œπ—Žπ–»π—ƒ Q π—Œπ—π—‚π–Ώπ—π—Œ Y π—Œπ—Žπ–»π—ƒ Q 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF Aβ€Ί
  unfolding Action_Tag_def View_Shift_def
  by (simp add: INTERP_SPEC_subj, blast)

lemma [Ο†reason 1010]:
  β€Ή (β‹€x. X x π—Œπ—π—‚π–Ώπ—π—Œ Y x 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF A)
⟹ ExBI X π—Œπ—π—‚π–Ώπ—π—Œ ExBI Y 𝗐𝗂𝗍𝗁 P @tag π’œ_simple_MTF Aβ€Ί
  unfolding Action_Tag_def View_Shift_def
  by (clarsimp simp add: INTERP_SPEC_ex, metis)

paragraph β€ΉFinishβ€Ί

lemma [Ο†reason 1000]:
  β€Ή XXX @tag A
⟹ XXX @tag π’œ_simple_MTF Aβ€Ί
  unfolding Action_Tag_def .

subsubsection β€ΉActions for the leading item onlyβ€Ί

consts π’œ_leading_item' :: β€Ήaction β‡’ actionβ€Ί

abbreviation β€Ήπ’œ_leading_item A ≑ π’œ_simple_MTF (π’œ_leading_item' A)β€Ί

declare [[Ο†reason_default_pattern
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_leading_item' _β€Ί β‡’
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_leading_item' _β€Ί    (100)
  and β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ  _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_leading_item' _β€Ί β‡’
      β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ  _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_leading_item' _β€Ί    (100)
]]

paragraph β€ΉImplicationβ€Ί

lemma [Ο†reason 1050]:
  β€Ή ERROR TEXT(β€ΉThere is no item!β€Ί)
⟹ TECHNICAL X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Any 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' Aβ€Ί
  ― β€ΉNever bind technical itemsβ€Ί
  unfolding Action_Tag_def ERROR_def by blast

lemma [Ο†reason 1050]:
  β€Ή ERROR TEXT(β€ΉThere is no item!β€Ί)
⟹ Void π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Any 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' Aβ€Ί
  ― β€ΉNever bind technical itemsβ€Ί
  unfolding Action_Tag_def ERROR_def by blast


lemma [Ο†reason 1020]:
  β€Ή R π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ R' 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' A
⟹ (TECHNICAL X) * R π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (TECHNICAL X) * R' 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' Aβ€Ί
  ― β€ΉNever bind technical itemsβ€Ί
  unfolding Action_Tag_def
  using transformation_left_frame .

lemma [Ο†reason 1010]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag A
⟹ X * R π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y * R 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' Aβ€Ί
  unfolding Action_Tag_def
  using transformation_right_frame .

lemma [Ο†reason 1000]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag A
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' Aβ€Ί
  unfolding Action_Tag_def .

lemma [Ο†reason 1010]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 Q @tag A
⟹ X π—Œπ—Žπ–»π—ƒ P π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y π—Œπ—Žπ–»π—ƒ P 𝗐𝗂𝗍𝗁 Q @tag π’œ_leading_item' Aβ€Ί
  unfolding Action_Tag_def Transformation_def
  by clarsimp


paragraph β€ΉView Shiftβ€Ί

lemma [Ο†reason 1010]:
  β€Ή X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 P @tag A
⟹ X❟ R π—Œπ—π—‚π–Ώπ—π—Œ Y❟ R 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' Aβ€Ί
  unfolding Action_Tag_def
  using Ο†view_shift_intro_frame .

lemma [Ο†reason 1000]:
  β€Ή X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 P @tag A
⟹ X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item' Aβ€Ί
  unfolding Action_Tag_def .

lemma [Ο†reason 1010]:
  β€Ή X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 Q @tag A
⟹ X π—Œπ—Žπ–»π—ƒ P π—Œπ—π—‚π–Ώπ—π—Œ Y π—Œπ—Žπ–»π—ƒ P 𝗐𝗂𝗍𝗁 Q @tag π’œ_leading_item' Aβ€Ί
  unfolding Action_Tag_def View_Shift_def
  by (simp add: INTERP_SPEC_subj, blast)


subsubsection β€ΉMapping Ο†-Type Items by View Shiftβ€Ί

declare [[Ο†reason_default_pattern
    β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_map_each_item _β€Ί β‡’
    β€Ή?X π—Œπ—π—‚π–Ώπ—π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œ_map_each_item _β€Ί    (100)
]]


paragraph β€ΉSupplemantaryβ€Ί

lemma [Ο†reason %π’œ_map_each_item]:
  β€Ή TECHNICAL X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ TECHNICAL X @tag π’œ_map_each_item π’œβ€Ί
  ― β€ΉNever bind technical itemsβ€Ί
  unfolding Action_Tag_def Technical_def
  by simp


section β€ΉBasic Applicationsβ€Ί

subsection β€ΉGeneral Syntaxβ€Ί

consts synt_orelse :: β€Ή'a β‡’ 'b β‡’ 'aβ€Ί (infixr "π—ˆπ—‹π–Ύπ—…π—Œπ–Ύ" 30)

subsection β€ΉIs \& Assertβ€Ί

lemma is_Ο†app:
  β€Ή 𝗉𝖺𝗋𝖺𝗆 y
⟹ Object_Equiv T eq
⟹ π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ eq x y
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ T β€Ί
  unfolding Premise_def Object_Equiv_def
  by blast

lemma assert_Ο†app:
  ‹𝗉𝖺𝗋𝖺𝗆 Y ⟹ π–½π—ˆ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 Any ⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Yβ€Ί
  unfolding Action_Tag_def Do_def
  using transformation_weaken by blast



subsection β€ΉSimplificationβ€Ί

subsubsection β€ΉBubblingβ€Ί

definition Bubbling :: β€Ή'a β‡’ 'aβ€Ί ("π–»π—Žπ–»π–»π—…π—‚π—‡π—€ _" [61] 60) where β€ΉBubbling x = xβ€Ί

paragraph β€ΉGeneral Rulesβ€Ί

lemma [Ο†reason default %Ο†simp_fallback]:
  β€Ή x ⦂ π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T π—Œπ—Žπ–»π—ƒ x'. x' = x @tag π’œsimp β€Ί
  unfolding Action_Tag_def Bubbling_def Transformation_def
  by simp

lemma [Ο†reason default %Ο†simp_fallback]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T π—Œπ—Žπ–»π—ƒ x'. x' = x @tag π’œbackward_simp β€Ί
  unfolding Action_Tag_def Bubbling_def Transformation_def
  by simp

paragraph β€ΉBubbling Ο†Sepβ€Ί

abbreviation Bubbling_Ο†Sep (infixr "βˆ—π’œ" 70)
    where "A βˆ—π’œ B ≑ π–»π—Žπ–»π–»π—…π—‚π—‡π—€ Ο†Prod A B"
  ― β€ΉThe separation operator that will expand by the system automaticallyβ€Ί

lemma [Ο†reason %Ο†simp_cut]:
  β€Ή NO_MATCH (Ua βˆ—π’œ Ub) U
⟹ x ⦂ (Ta βˆ—π’œ Tb) βˆ— U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ (Ta βˆ— U) βˆ—π’œ Tb π—Œπ—Žπ–»π—ƒ y. y = ((fst (fst x), snd x), snd (fst x)) @tag π’œsimp β€Ί
  for U :: β€Ή('c::sep_ab_semigroup,'a) Ο†β€Ί
  unfolding Bubbling_def Action_Tag_def Transformation_def
  by (cases x; clarsimp;
      metis sep_disj_commuteI sep_disj_multD1 sep_disj_multI2 sep_mult_assoc sep_mult_commute) 

lemma [Ο†reason %Ο†simp_cut]:
  β€Ή NO_MATCH (Ta βˆ—π’œ Tb) T
⟹ x ⦂ T βˆ— (Ua βˆ—π’œ Ub) π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ (T βˆ— Ua) βˆ—π’œ Ub π—Œπ—Žπ–»π—ƒ y. y = ((fst x, fst (snd x)), snd (snd x)) @tag π’œsimp β€Ί
  for T :: β€Ή('c::sep_semigroup,'a) Ο†β€Ί
  unfolding Bubbling_def Action_Tag_def Transformation_def
  by (cases x; clarsimp; insert sep_disj_multD1 sep_disj_multI1 sep_mult_assoc'; blast)

lemma [Ο†reason %Ο†simp_cut+10]:
  β€Ή x ⦂ (Ta βˆ—π’œ Tb) βˆ— (Ua βˆ—π’œ Ub) π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ (Ta βˆ— Ua) βˆ—π’œ (Tb βˆ— Ub) π—Œπ—Žπ–»π—ƒ y.
              y = ((fst (fst x), fst (snd x)), (snd (fst x), snd (snd x))) @tag π’œsimp β€Ί
  for Ta :: β€Ή('c::sep_ab_semigroup,'a) Ο†β€Ί
  unfolding Bubbling_def Action_Tag_def Transformation_def
  by (cases x; clarsimp; smt (verit, ccfv_threshold) sep_disj_commuteI sep_disj_multD1
                             sep_disj_multI1 sep_mult_assoc' sep_mult_commute)

paragraph β€ΉTransformationβ€Ί

subparagraph β€ΉReduction in Sourceβ€Ί

lemma [Ο†reason %ToA_red]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P
⟹ x ⦂ π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding Bubbling_def .

lemma [Ο†reason %ToA_red]:
  β€Ή (x ⦂ T) * R π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P
⟹ (x ⦂ π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T) * R π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding Bubbling_def .

lemma [Ο†reason %ToA_red]:
  β€Ή x ⦂ T ✼ W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P
⟹ x ⦂ (π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T) ✼ W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding Bubbling_def .

subparagraph β€ΉReduction in Targetβ€Ί

lemma [Ο†reason %ToA_red]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T 𝗐𝗂𝗍𝗁 P
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding Bubbling_def .

lemma [Ο†reason %ToA_red]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ R 𝗐𝗂𝗍𝗁 P
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ R 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding Bubbling_def .

lemma [Ο†reason %ToA_red]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T ✼ W 𝗐𝗂𝗍𝗁 P
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ (π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T) ✼ W 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding Bubbling_def .

paragraph β€ΉVarious Properties of Bubbling Tagβ€Ί

lemma [Ο†reason %abstract_domain]:
  β€Ή Abstract_Domain T D
⟹ Abstract_Domain (π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T) D β€Ί
  unfolding Bubbling_def .

lemma [Ο†reason %abstract_domain]:
  β€Ή Abstract_DomainL T D
⟹ Abstract_DomainL (π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T) D β€Ί
  unfolding Bubbling_def .

lemma [Ο†reason %identity_element_cut]:
  β€Ή Identity_ElementsI T D P
⟹ Identity_ElementsI (π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T) D P β€Ί
  unfolding Bubbling_def .

lemma [Ο†reason %identity_element_cut]:
  β€Ή Identity_ElementsE T D
⟹ Identity_ElementsE (π–»π—Žπ–»π–»π—…π—‚π—‡π—€ T) D β€Ί
  unfolding Bubbling_def .

subsection β€ΉToβ€Ί

consts to :: β€Ή('a,'b) Ο† β‡’ actionβ€Ί
       π’œpattern  :: β€Ή'redex β‡’ 'residue β‡’ ('c,'d) Ο†β€Ί ("𝗉𝖺𝗍𝗍𝖾𝗋𝗇 _ β‡’ _" [42,42] 41)
       π’œtraverse :: β€Ή('a,'b) Ο† β‡’ ('c,'d) Ο†β€Ί ("π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ _" [30] 29) ― β€Ήenter to elements recursivelyβ€Ί
       π’œthen     :: β€Ή('a,'b) Ο† β‡’ ('c,'d) Ο† β‡’ ('c,'d) Ο†β€Ί (infixr "𝗍𝗁𝖾𝗇" 28)
                    ― β€Ήβ€Ήπ’œ 𝗍𝗁𝖾𝗇 ℬ› hints to first transform to β€Ήπ’œβ€Ί and then from β€Ήπ’œβ€Ί to ‹ℬ›.
                        β€Ήπ’œβ€Ί and ‹ℬ› can be special commands.β€Ί
       π’œcommute  :: β€Ή'Ο†F β‡’ 'Ο†G β‡’ ('c,'a) Ο†β€Ί ("π–Όπ—ˆπ—†π—†π—Žπ—π–Ύ")
                    ― β€Ήβ€Ήπ–Όπ—ˆπ—†π—†π—Žπ—π–Ύ F Gβ€Ί hints to swap β€ΉF (G T)β€Ί to β€ΉG (F T)β€Ί by particularly applying
                        Commutative-Tyop rules (see β€ΉTyops_Commuteβ€Ί). β€Ί

Ο†reasoner_group To_ToA = (100, [0,4000]) for β€Ήx ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. r x y 𝗐𝗂𝗍𝗁 P @tag to Uβ€Ί
    β€ΉRules of To-Transformation that transforms β€Ήx ⦂ Tβ€Ί to β€Ήy ⦂ Uβ€Ί for certain β€Ήyβ€Ί constrained by a
     relation with β€Ήxβ€Ί.β€Ί
 and To_ToA_fail = (0, [0,0]) in To_ToA and in fail
    β€ΉFailure report in To-Transformationβ€Ί
 and To_ToA_system_fallback = (1, [1,1]) in To_ToA > To_ToA_fail
    β€ΉSystem To-Transformation rules falling back to normal transformation.β€Ί
 and To_ToA_fallback = (10, [2,20]) in To_ToA > To_ToA_system_fallback
    β€ΉA general group allocating priority space for fallbacks of To-Transformation.β€Ί
 and To_ToA_derived = (50, [30,70]) in To_ToA > To_ToA_fallback and < default
    β€ΉAutomatically derived To-Transformation rulesβ€Ί
 and To_ToA_cut     = (1000, [1000,1100]) in To_ToA
    β€ΉCutting To-Transformation rulesβ€Ί
 and To_ToA_success = (4000, [4000,4000]) in To_ToA > To_ToA_cut
    β€ΉImmediate successβ€Ί
 and To_ToA_user    = (100, [80, 120]) in To_ToA and < To_ToA_cut and > To_ToA_system_fallback
    β€Ήdefault group for user rulesβ€Ί

(* abbreviation β€Ήπ’œ_transform_to T ≑ π’œ_leading_item (π’œnap (to T)) β€Ί *)

ML β€Ήfun mk_pattern_for_To_ToAformation ctxt term =
  let val idx = Term.maxidx_of_term term + 1
      fun chk_P (Const(const_nameβ€ΉTrueβ€Ί, _)) = Var(("P",idx), HOLogic.boolT)
        | chk_P X = error ("To-Transformation should not contain a 𝗐𝗂𝗍𝗁 clause, but given\n" ^
                           Context.cases Syntax.string_of_term_global Syntax.string_of_term ctxt X)
      val i = Unsynchronized.ref idx
      fun relax (Const(N, _)) = (i := !i + 1; Const(N, TVar(("t",!i), [])))
        | relax (A $ B) = relax A $ relax B
        | relax (Abs(N,_,X)) = (i := !i + 1; Abs(N, TVar(("t",!i),[]), relax X))
        | relax (Free X) = Free X
        | relax (Var v) = Var v
        (*| relax (Var (v, _)) = (i := !i + 1; Var(v, TVar(("t",!i),[]))) *)
        | relax (Bound i) = Bound i
   in case term
        of Trueprop $ (Action_Tag $ (Trans $ X $ _ $ P) $ To_Tag) =>
           SOME [Trueprop $ (Action_Tag
              $ (relax Trans $ X $ Var(("Y",idx), TVar(("model",idx),[])) $ chk_P P)
              $ relax To_Tag)]
  endβ€Ί

declare [[

  Ο†reason_default_pattern_ML β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (y ⦂ ?U π—Œπ—Žπ–»π—ƒ y. ?R y) 𝗐𝗂𝗍𝗁 ?P @tag to ?Tβ€Ί β‡’
    β€Ήmk_pattern_for_To_ToAformationβ€Ί (100),

  Ο†reason_default_pattern
    β€Ή?X @tag to ?Aβ€Ί β‡’ β€ΉERROR TEXT(β€ΉMalformed To-Transformation: β€Ί (?X @tag to ?A) ⏎
                                      β€ΉExpect: β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (y ⦂ ?Y π—Œπ—Žπ–»π—ƒ y. ?r y) @tag to _β€Ίβ€Ί)β€Ί (1),

  Ο†default_reasoner_group β€Ή_ @tag to _β€Ί : %To_ToA_user (100)
]]


subsubsection β€ΉSimplification Protectβ€Ί

definition [simplification_protect]:
  β€ΉΟ†To_Transformation_Simp_Protect X U r A ≑ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. r y @tag to Aβ€Ί

lemma Ο†To_Transformation_Simp_Protect_cong[cong]:
  β€Ή X ≑ X'
⟹ U ≑ U'
⟹ r ≑ r'
⟹ Ο†To_Transformation_Simp_Protect X U r A ≑ Ο†To_Transformation_Simp_Protect X' U' r' A β€Ί
  by simp

subsubsection β€ΉExtracting Pureβ€Ί

lemma [Ο†reason %extract_pure]:
  β€Ή 𝗋EIF A P
⟹ 𝗋EIF (A @tag to T) P β€Ί
  unfolding Action_Tag_def .

lemma [Ο†reason %extract_pure]:
  β€Ή 𝗋ESC P A
⟹ 𝗋ESC P (A @tag to T) β€Ί
  unfolding Action_Tag_def .

subsubsection β€ΉEntry Pointβ€Ί

lemma to_Ο†app:
  β€Ή 𝗉𝖺𝗋𝖺𝗆 T
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Ya 𝗐𝗂𝗍𝗁 P @tag π’œ_leading_item (to T)
⟹ Ya π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag π’œ_apply_simplication
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding Do_def Action_Tag_def Transformation_def
  by simp

lemmas "π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ_π—π—ˆ_Ο†app" = to_Ο†app

subsubsection β€ΉTerminationβ€Ί

lemma ToA_trivial:
  β€Ήx ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T π—Œπ—Žπ–»π—ƒ x'. x' = x @tag to anyβ€Ί
  unfolding Action_Tag_def
  by (simp add: ExBI_defined)

lemma [Ο†reason no explorative backtrack %To_ToA_fail for β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to _β€Ί]:
  β€Ή TRACE_FAIL TEXT(β€ΉFail to transformβ€Ί X β€Ήtoβ€Ί T)
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag to Tβ€Ί
  unfolding Action_Tag_def TRACE_FAIL_def by blast

lemma [Ο†reason default %To_ToA_system_fallback]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y' ⦂ U 𝗐𝗂𝗍𝗁 P
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. y = y' ∧ P @tag to Uβ€Ί
  unfolding Action_Tag_def
  by (simp add: ExBI_defined)

lemma [Ο†reason %To_ToA_success]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T π—Œπ—Žπ–»π—ƒ x'. x' = x @tag to Tβ€Ί
  unfolding Action_Tag_def
  by (simp add: ExBI_defined)


subsubsection β€ΉSpecial Formsβ€Ί

lemma [Ο†reason %To_ToA_cut]:
  β€Ή (π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡ C ⟹ A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ Ua π—Œπ—Žπ–»π—ƒ y. ra y @tag to T)
⟹ (π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡ Β¬ C ⟹ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ Ub π—Œπ—Žπ–»π—ƒ y. rb y @tag to T)
⟹ If C A B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ If C Ua Ub π—Œπ—Žπ–»π—ƒ y. (if C then ra y else rb y) @tag to Tβ€Ί
  unfolding Action_Tag_def Premise_def
  by (cases C; simp)

lemma [Ο†reason %To_ToA_cut]:
  β€Ή (π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡ C ⟹ x ⦂ A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ Ua π—Œπ—Žπ–»π—ƒ y. ra y @tag to T)
⟹ (π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡ Β¬ C ⟹ x ⦂ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ Ub π—Œπ—Žπ–»π—ƒ y. rb y @tag to T)
⟹ x ⦂ If C A B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ If C Ua Ub π—Œπ—Žπ–»π—ƒ y. (if C then ra y else rb y) @tag to Tβ€Ί
  unfolding Action_Tag_def Premise_def
  by (cases C; simp)


lemma [Ο†reason %To_ToA_cut for β€Ή1 π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to _β€Ί]:
  β€Ή () ⦂ β—‹ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to T
⟹ 1 π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to T β€Ί
  by simp


subsubsection β€ΉNo Changeβ€Ί

consts π’œNO_CHANGE :: β€Ή('a,'b) Ο†β€Ί ("π—‡π—ˆ-𝖼𝗁𝖺𝗇𝗀𝖾")

lemma [Ο†reason %To_ToA_cut]:
  β€Ήx ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T π—Œπ—Žπ–»π—ƒ x'. x' = x @tag to π—‡π—ˆ-𝖼𝗁𝖺𝗇𝗀𝖾 β€Ί
  unfolding Action_Tag_def
  by (simp add: ExBI_defined)

lemma [Ο†reason !10]:
  β€Ήx ⦂ β—‹ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ β—‹ π—Œπ—Žπ–»π—ƒ y. True @tag to π—‡π—ˆ-𝖼𝗁𝖺𝗇𝗀𝖾›
  unfolding Action_Tag_def Transformation_def
  by simp


subsubsection β€ΉPatternβ€Ί

Ο†reasoner_group To_ToA_pattern_shortcut = (3000, [3000,3000]) in To_ToA and > To_ToA_cut β€Ήβ€Ί

context begin

private lemma π’œ_strip_traverse:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to A
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ A) β€Ί
  unfolding Action_Tag_def .

private lemma π’œ_pattern_meet:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to U
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (𝗉𝖺𝗍𝗍𝖾𝗋𝗇 T β‡’ U) β€Ί
  unfolding Action_Tag_def .

private lemma π’œ_pattern_meet1:
  β€Ή x ⦂ T p π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (U p)
⟹ x ⦂ T p π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (𝗉𝖺𝗍𝗍𝖾𝗋𝗇 T β‡’ U) β€Ί
  unfolding Action_Tag_def .

private lemma π’œ_pattern_not_meet:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to π—‡π—ˆ-𝖼𝗁𝖺𝗇𝗀𝖾
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to π’œ β€Ί
  unfolding Action_Tag_def .

private lemma π’œ_pattern_meet_this:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to U
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (𝗉𝖺𝗍𝗍𝖾𝗋𝗇 T β‡’ U π—ˆπ—‹π–Ύπ—…π—Œπ–Ύ others) β€Ί
  unfolding Action_Tag_def .

private lemma π’œ_pattern_meet_this1:
  β€Ή x ⦂ T p π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (U p)
⟹ x ⦂ T p π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (𝗉𝖺𝗍𝗍𝖾𝗋𝗇 T β‡’ U π—ˆπ—‹π–Ύπ—…π—Œπ–Ύ others) β€Ί
  unfolding Action_Tag_def .

private lemma π’œ_pattern_meet_that:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to that
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag to (this π—ˆπ—‹π–Ύπ—…π—Œπ–Ύ that) β€Ί
  unfolding Action_Tag_def .

Ο†reasoner_ML π’œpattern %To_ToA_pattern_shortcut
    ( β€Ή_ ⦂ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to (𝗉𝖺𝗍𝗍𝖾𝗋𝗇 _ β‡’ _)β€Ί
    | β€Ή_ ⦂ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to (_ π—ˆπ—‹π–Ύπ—…π—Œπ–Ύ _)β€Ί
    | β€Ή_ ⦂ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to (π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ _)β€Ί ) =
β€Ήfn (_, (ctxt, sequent)) => Seq.make (fn () =>
  let fun parse_patterns (Const(const_nameβ€Ήsynt_orelseβ€Ί, _) $ X $ Y)
            = parse_patterns X @ parse_patterns Y
        | parse_patterns (Const(const_nameβ€Ήπ’œpatternβ€Ί, _) $ Pat $ _) = [Pat]
        | parse_patterns _ = []

      val (bvs, ToA) = Phi_Help.strip_meta_hhf_bvs (Phi_Help.leading_antecedent' sequent)
      val (T, A) = case ToA of _ (*Trueprop*) $ (_ (*Action_Tag*)
                              $ (Const _ (*Transformation*) $ (_ (*Ο†Type*) $ _ $ T) $ _ $ _)
                              $ (_ (*to*) $ A))
                             => (T, A)

      val (is_traverse, A') = case A of Const(const_nameβ€Ήπ’œtraverseβ€Ί, _) $ A' => (true, A')
                                      | A' => (false, A')
      val pats = parse_patterns A'

   in if null pats then NONE
      else
  let val idx = Thm.maxidx_of sequent
      val bvtys = map snd bvs

      fun reconstruct_pattern redex =
        let val param_redex = rev (#1 (dest_parameterized_phi_ty (fastype_of1 (bvtys,redex))))
            fun reconstruct _ [] redex = Envir.beta_eta_contract redex
              | reconstruct i (ty::param_tys) redex =
                  let val var = Var(("𝗉",i+idx), bvtys ---> ty)
                             |> fold_index (fn (i, _) => fn X => X $ Bound i) bvtys
                   in reconstruct (i+1) param_tys (redex $ var)
                  end
         in (length param_redex, reconstruct 0 param_redex redex)
        end
      val pats = map reconstruct_pattern pats

      val len = length pats
      val thy = Proof_Context.theory_of ctxt

      fun meet_pattern rules (i,len) th =
        if i = 0
        then let val rule = if i = len - 1 then #1 rules else #2 rules
              in rule RS th
             end
        else meet_pattern rules (i-1,len-1) (@{thm' π’œ_pattern_meet_that} RS th)

      fun meet_pattern' A i th =
        meet_pattern A (i,len) (if is_traverse then @{thm' π’œ_strip_traverse} RS th else th)

      fun bad_pattern pat = error ("Bad Pattern: " ^ Syntax.string_of_term ctxt pat)

      (*we give a fast but weak check, and expect improving it later*)
      val const_heads = map_filter ((fn Const(N, _) => SOME N | _ => NONE) o Term.head_of o snd) pats
      val free_heads = map_filter ((fn Free(N, _) => SOME N | _ => NONE) o Term.head_of o snd) pats
      val cannot_shortcut = Phi_Syntax.exists_parameters_that_are_phi_types
                                 (fn Const (N', _) => member (op =) const_heads N'
                                   | Free (N', _) => member (op =) free_heads N'
                                   | _ => false)

   in case get_index (fn (param_num, pat) =>
        if PLPR_Pattern.matches thy (K false) bvs (pat, T)
        then SOME (case param_num of 0 => (@{thm' π’œ_pattern_meet}, @{thm' π’œ_pattern_meet_this})
                                   | 1 => (@{thm' π’œ_pattern_meet1}, @{thm' π’œ_pattern_meet_this1})
                                   | _ => raise THM ("right now we only support patterns of upto 1 parameter", 1, [sequent]))
        else NONE) pats
   of NONE => if cannot_shortcut T then NONE
              else (SOME ((ctxt, @{thm' ToA_trivial} RS sequent), Seq.empty)
                 handle THM _ =>
                    SOME ((ctxt, @{thm' π’œ_pattern_not_meet} RS sequent), Seq.empty))
    | SOME (i, rules) => SOME ((ctxt, meet_pattern' rules i sequent), Seq.empty)
  end end
)β€Ί

end



subsubsection β€ΉProductβ€Ί

(* β€Ήtoβ€Ί is for single Ο†-type item!

lemma prod_transform_to1:
  β€Ή A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ X 𝗐𝗂𝗍𝗁 P @tag to T
⟹ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 Q @tag to U
⟹ A * B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ X * Y 𝗐𝗂𝗍𝗁 P ∧ Q @tag to (T βˆ— U)β€Ί
  unfolding Action_Tag_def
  by (meson transformation_left_frame transformation_right_frame transformation_trans)

lemma prod_transform_to2:
  β€Ή A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ X 𝗐𝗂𝗍𝗁 P @tag to U
⟹ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 Q @tag to T
⟹ A * B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ X * Y 𝗐𝗂𝗍𝗁 P ∧ Q @tag to (T βˆ— U)β€Ί
  unfolding Action_Tag_def
  by (meson transformation_left_frame transformation_right_frame transformation_trans)

declare [[Ο†reason 1200 prod_transform_to1 prod_transform_to2
      for β€Ή?A * ?B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to (?T βˆ— ?U)β€Ί]]

hide_fact prod_transform_to1 prod_transform_to2

lemma [Ο†reason 1100]:
  β€Ή A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ X 𝗐𝗂𝗍𝗁 P @tag to T
⟹ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 Q @tag to T
⟹ A * B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ X * Y 𝗐𝗂𝗍𝗁 P ∧ Q @tag to Tβ€Ί
  unfolding Action_Tag_def
  by (meson transformation_left_frame transformation_right_frame transformation_trans)
*)

text β€ΉBy default, the To-Transformation does not recognize β€Ήto (A βˆ— B βˆ— C)β€Ί as a request of
permutation for instance β€ΉC βˆ— B βˆ— Aβ€Ί (the search cost is huge!).
Instead, it recognizes the request as transforming β€ΉCβ€Ί to β€ΉAβ€Ί, β€ΉBβ€Ί to β€ΉBβ€Ί, and β€ΉCβ€Ί to β€ΉAβ€Ί element-wisely.
If you want to make the β€ΉA βˆ— B βˆ— Cβ€Ί as a whole so that the system can do the permutation,
write it as β€Ήto (id (A βˆ— B βˆ— C))β€Ί and a fallback will be encountered reducing the problem to
normal transformation.β€Ί

lemma Prod_ToTransform[Ο†reason %To_ToA_cut]:
  β€Ή fst x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T' π—Œπ—Žπ–»π—ƒ x'. ra x' @tag to A
⟹ snd x ⦂ U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y' ⦂ U' π—Œπ—Žπ–»π—ƒ y'. rb y' @tag to B
⟹ x ⦂ (T βˆ— U) π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ xy' ⦂ (T' βˆ— U') π—Œπ—Žπ–»π—ƒ xy'. ra (fst xy') ∧ rb (snd xy') @tag to (A βˆ— B)β€Ί
  unfolding Action_Tag_def Transformation_def
  by (cases x; simp; blast)

lemma Prod_ToTransform_rev:
  β€Ή fst x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T' π—Œπ—Žπ–»π—ƒ x'. ra x' @tag to B
⟹ snd x ⦂ U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y' ⦂ U' π—Œπ—Žπ–»π—ƒ y'. rb y' @tag to A
⟹ x ⦂ (T βˆ— U) π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ xy' ⦂ (T' βˆ— U') π—Œπ—Žπ–»π—ƒ xy'. ra (fst xy') ∧ rb (snd xy') @tag to (A βˆ— B)β€Ί
  unfolding Action_Tag_def Transformation_def
  by (cases x; simp; blast)

lemma [Ο†reason %To_ToA_cut+10]:
  β€Ή fst x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T' π—Œπ—Žπ–»π—ƒ x'. ra x' @tag to (π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ Target)
⟹ snd x ⦂ U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y' ⦂ U' π—Œπ—Žπ–»π—ƒ y'. rb y' @tag to (π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ Target)
⟹ x ⦂ (T βˆ— U) π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ xy' ⦂ (T' βˆ— U') π—Œπ—Žπ–»π—ƒ xy'. ra (fst xy') ∧ rb (snd xy') @tag to (π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ Target)β€Ί
  unfolding Action_Tag_def Transformation_def
  by (cases x; simp; blast)


(* Is this still required?

lemma [Ο†reason 1210 for β€Ή_ ⦂ _ βˆ— _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to ( _ π–Ώπ—ˆπ—‹ _ βˆ— _) β€Ί]:
  β€Ή fst x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T' π—Œπ—Žπ–»π—ƒ x'. ra x' 𝗐𝗂𝗍𝗁 P @tag to (T' π–Ώπ—ˆπ—‹ T)
⟹ snd x ⦂ U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y' ⦂ U' π—Œπ—Žπ–»π—ƒ y'. rb y' 𝗐𝗂𝗍𝗁 Q @tag to (U' π–Ώπ—ˆπ—‹ U)
⟹ x ⦂ (T βˆ— U) π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ xy' ⦂ (T' βˆ— U') π—Œπ—Žπ–»π—ƒ xy'. ra (fst xy') ∧ rb (snd xy') 𝗐𝗂𝗍𝗁 P ∧ Q
    @tag to (T' βˆ— U' π–Ώπ—ˆπ—‹ T βˆ— U)β€Ί
  unfolding Action_Tag_def Transformation_def
  by (cases x; simp; blast)
*)

subsubsection β€ΉTo Itselfβ€Ί

declare [[Ο†reason_default_pattern
    β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (y ⦂ _ π—Œπ—Žπ–»π—ƒ y. _) 𝗐𝗂𝗍𝗁 _ @tag to Itselfβ€Ί β‡’ β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to Itselfβ€Ί (200)
      ― β€ΉHere we varify the type of the β€ΉItselfβ€Ί β€Ί
]]

lemma [Ο†reason default %To_ToA_fallback]:
  β€Ήx ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ v ⦂ (Itself :: ('v,'v) Ο†) π—Œπ—Žπ–»π—ƒ v. v ⊨ (x ⦂ T) @tag to (Itself :: ('v,'v) Ο†)β€Ί
  unfolding Action_Tag_def Transformation_def
  by simp

lemma [Ο†reason %To_ToA_cut]:
  β€Ή fst x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ Itself π—Œπ—Žπ–»π—ƒ x. ra x @tag to (Itself :: ('c,'c) Ο†)
⟹ snd x ⦂ U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ Itself π—Œπ—Žπ–»π—ƒ x. rb x @tag to (Itself :: ('c,'c) Ο†)
⟹ x ⦂ T βˆ— U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ (Itself :: ('c::sep_magma,'c) Ο†) π—Œπ—Žπ–»π—ƒ x.
                    (βˆƒa b. x = a * b ∧ a ## b ∧ rb b ∧ ra a) @tag to (Itself :: ('c,'c) Ο†) β€Ί
  unfolding Action_Tag_def Transformation_def
  by (cases x; simp; blast)

paragraph β€ΉSpecial Formsβ€Ί

lemma [Ο†reason %To_ToA_cut]:
  β€Ή 1 π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (y::'b::one) ⦂ Itself π—Œπ—Žπ–»π—ƒ y. y = 1 @tag to (Itself :: ('b, 'b) Ο†) β€Ί
  unfolding Action_Tag_def Transformation_def
  by simp

lemma [Ο†reason %To_ToA_cut]:
  β€Ή (π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡ C ⟹ x ⦂ A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (y :: 'a) ⦂ Itself π—Œπ—Žπ–»π—ƒ y. ra y @tag to (Itself :: ('a,'a) Ο†))
⟹ (π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡ Β¬ C ⟹ x ⦂ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ Itself π—Œπ—Žπ–»π—ƒ y. rb y @tag to (Itself :: ('a,'a) Ο†))
⟹ x ⦂ If C A B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ Itself π—Œπ—Žπ–»π—ƒ y. (if C then ra y else rb y) @tag to (Itself :: ('a,'a) Ο†)β€Ί
  unfolding Action_Tag_def Transformation_def Premise_def
  by simp

lemma [Ο†reason %To_ToA_cut]:
  β€Ήx ⦂ βŠ€Ο† π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ v ⦂ Itself π—Œπ—Žπ–»π—ƒ v. True @tag to Itselfβ€Ί
  unfolding Action_Tag_def Transformation_def
  by simp


subsubsection β€ΉThen: Subsequent Executionβ€Ί

lemma [Ο†reason %To_ToA_cut]:
  β€Ή X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. r y @tag to π’œ
⟹ (β‹€y. π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡ r y ⟹ y ⦂ U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ z ⦂ W π—Œπ—Žπ–»π—ƒ z. r' y z @tag to ℬ)
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ z ⦂ W π—Œπ—Žπ–»π—ƒ z. (βˆƒy. r y ∧ r' y z) @tag to (π’œ 𝗍𝗁𝖾𝗇 ℬ) β€Ί
  unfolding Action_Tag_def Premise_def Transformation_def
  by clarsimp blast



subsection β€ΉAsβ€Ί

lemma as_Ο†app:
  " 𝗉𝖺𝗋𝖺𝗆 (y ⦂ U)
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y' ⦂ U π—Œπ—Žπ–»π—ƒ y'. P y' @tag to U
⟹ Object_Equiv U eq
⟹ π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ (βˆ€y'. P y' ⟢ eq y' y)
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U "
  unfolding Premise_def Action_Tag_def Object_Equiv_def Transformation_def
  by simp blast



subsection β€ΉCase Analysisβ€Ί

(*TODO: review \& documenting!*)

consts π’œcase :: action

(*
Ο†reasoner_group π’œcase = (1000, [1000,2000]) for (β€ΉX @tag π’œcaseβ€Ί)
  β€Ήβ€Ί *)

subsubsection β€ΉFrameworkβ€Ί

declare [[
  Ο†reason_default_pattern
      β€Ή ?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œcase β€Ί β‡’ β€Ή ?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œcase β€Ί  (100)
  and β€Ή ?X π—Œπ—π—‚π–Ώπ—π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œcase β€Ί β‡’ β€Ή ?X π—Œπ—π—‚π–Ώπ—π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag π’œcase β€Ί   (100)
  and β€Ή π—‰π—‹π—ˆπ–Ό _ ⦃ ?X ⟼ _ ⦄ π—π—π—‹π—ˆπ—π—Œ _ @tag π’œcase β€Ί β‡’ β€Ή π—‰π—‹π—ˆπ–Ό _ ⦃ ?X ⟼ _ ⦄ π—π—π—‹π—ˆπ—π—Œ _ @tag π’œcase β€Ί (100)
  and β€Ή ?X @tag π’œcase β€Ί β‡’ β€ΉERROR TEXT(β€ΉMalformed π’œcase ruleβ€Ί (?X @tag π’œcase))β€Ί (0)
]]

lemma "_cases_app_rule_": β€ΉCall_Action (π’œ_morphism π’œcase)β€Ί ..

ML_file β€Ήlibrary/tools/induct_analysis.MLβ€Ί

hide_fact "_cases_app_rule_"

Ο†lang_parser case_analysis (%Ο†parser_unique, %Ο†lang_expr) ["case_analysis"] (β€Ή_β€Ί)
  β€Ή IDECP_Induct_Analysis.case_analysis_processor β€Ί


subsubsection β€ΉCase Rulesβ€Ί

lemma [Ο†reason 1000]:
  β€Ή π—Žπ—Œπ–Ύπ—‹ A π—Œπ—π—‚π–Ώπ—π—Œ YA
⟹ π—Žπ—Œπ–Ύπ—‹ B π—Œπ—π—‚π–Ώπ—π—Œ YB
⟹ π–½π—ˆ π—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[assertion_simps SOURCE] Y : YA + YB
⟹ B + A π—Œπ—π—‚π–Ώπ—π—Œ Y @tag π’œcase β€Ί
  unfolding Argument_def Action_Tag_def Simplify_def View_Shift_def Do_def
  by (simp add: distrib_right)

lemma [Ο†reason 1000]:
  β€Ή π—Žπ—Œπ–Ύπ—‹ A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ YA
⟹ π—Žπ—Œπ–Ύπ—‹ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ YB
⟹ π–½π—ˆ π—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[assertion_simps SOURCE] Y : YA + YB
⟹ B + A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag π’œcase β€Ί
  unfolding Argument_def Action_Tag_def Simplify_def View_Shift_def Transformation_def Do_def
  by simp

lemma [Ο†reason 1000]:
  β€Ή π—Žπ—Œπ–Ύπ—‹ π—‰π—‹π—ˆπ–Ό fA ⦃ A ⟼ YA ⦄ π—π—π—‹π—ˆπ—π—Œ EA
⟹ π—Žπ—Œπ–Ύπ—‹ π—‰π—‹π—ˆπ–Ό fB ⦃ B ⟼ YB ⦄ π—π—π—‹π—ˆπ—π—Œ EB
⟹ π–½π—ˆ π–Όπ—ˆπ—‡π–½π—‚π—π—‚π—ˆπ—‡[procedure_ss] fA = fB
⟹ π–½π—ˆ π—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[assertion_simps SOURCE] Y : YA + YB
⟹ π–½π—ˆ π—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[assertion_simps ABNORMAL] E : EA + EB
⟹ π—‰π—‹π—ˆπ–Ό fA ⦃ B + A ⟼ Y ⦄ π—π—π—‹π—ˆπ—π—Œ E @tag π’œcase β€Ί
  unfolding Action_Tag_def Simplify_def Premise_def Argument_def Do_def
  by (simp, metis Ο†CASE Ο†CONSEQ add.commute plus_fun view_shift_refl view_shift_union(1))

lemma [Ο†reason 1000]:
  β€Ή (π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ P ⟹ π—Žπ—Œπ–Ύπ—‹ A π—Œπ—π—‚π–Ώπ—π—Œ Ya)
⟹ (π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ Β¬ P ⟹ π—Žπ—Œπ–Ύπ—‹ B π—Œπ—π—‚π–Ώπ—π—Œ Yb)
⟹ π–½π—ˆ If P Ya Yb π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag invoke_br_join
⟹ If P A B π—Œπ—π—‚π–Ώπ—π—Œ Y @tag π’œcaseβ€Ί
  unfolding Argument_def Action_Tag_def Premise_def Do_def
  apply (cases P; simp)
  using Ο†view_trans view_shift_by_implication apply fastforce
  using View_Shift_def view_shift_by_implication by force

lemma [Ο†reason 1000]:
  β€Ή (π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ P ⟹ π—Žπ—Œπ–Ύπ—‹ A π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Ya)
⟹ (π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ Β¬ P ⟹ π—Žπ—Œπ–Ύπ—‹ B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Yb)
⟹ π–½π—ˆ If P Ya Yb π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag invoke_br_join
⟹ If P A B π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag π’œcaseβ€Ί
  unfolding Argument_def Action_Tag_def Premise_def Do_def
  apply (cases P; simp)
  using transformation_trans apply fastforce
  using transformation_trans by fastforce

lemma [Ο†reason default 0]:
  β€Ή FAIL TEXT(β€ΉDon't know how to case-splitβ€Ί X)
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y @tag π’œcaseβ€Ί
  unfolding FAIL_def
  by blast


(*lemma [Ο†reason 1000]:
  β€Ή 𝗉𝖺𝗋𝖺𝗆 P
⟹ (π—‰π—‹π–Ύπ—†π—‚π—Œπ–Ύ P ⟹ π—Žπ—Œπ–Ύπ—‹ X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 PA)
⟹ π—Žπ—Œπ–Ύπ—‹ B π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 PB
⟹ X π—Œπ—π—‚π–Ώπ—π—Œ Y 𝗐𝗂𝗍𝗁 PB ∨ PA @tag π’œ_action_caseβ€Ί
  unfolding Argument_def Action_Tag_def using Ο†CASE_VS . *)


subsection β€ΉOpen \& Make Abstractionβ€Ί


subsubsection β€ΉOpen Abstractionβ€Ί

definition OPEN :: β€Ήnat β‡’ 'x β‡’ 'xβ€Ί where β€ΉOPEN i X ≑ Xβ€Ί
  ― β€ΉWhen the definition of the Ο†-type involves multiple equations, β€Ήiβ€Ί hints which equation should be used.
     β€Ήiβ€Ί can be a unknown variable to let the reasoner infer the proper one but it can fail and when it
     fails branches diverge for each equation.β€Ί

declare [[
  Ο†reason_default_pattern
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ ?Y 𝗐𝗂𝗍𝗁 ?P @tag OPEN ?i ?Aβ€Ί β‡’
      β€ΉERROR TEXT(β€ΉMalformed ruleβ€Ί (?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ ?Y 𝗐𝗂𝗍𝗁 ?P @tag OPEN ?i ?A))β€Ί (1)
  and β€Ή_ ⦂ ?T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ @tag OPEN _ 𝒯𝒫› β‡’ β€Ή_ ⦂ ?T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ @tag OPEN _ 𝒯𝒫 β€Ί (100)
  and β€Ή?var ⦂ ?T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ @tag OPEN _ 𝒯𝒫'β€Ί β‡’ β€Ή_ ⦂ ?T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ @tag OPEN _ 𝒯𝒫' β€Ί (100)
]]

(*
declare [[
  Ο†reason_default_pattern β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (y ⦂ ?U π—Œπ—Žπ–»π—ƒ y. ?R y) 𝗐𝗂𝗍𝗁 _ @tag to (OPEN _ _)β€Ί β‡’
                          β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to (OPEN _ _)β€Ί (200)
    and β€Ή_ ⦂ OPEN _ ?T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›
     β‡’ β€Ή_ ⦂ OPEN _ ?T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫› (700)
    and β€Ή(_ ⦂ OPEN _ ?T) * _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›
     β‡’ β€Ή(_ ⦂ OPEN _ ?T) * _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫› (700)
    and β€Ή_ ⦂ OPEN _ ?T ✼ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫'β€Ί
     β‡’ β€Ή_ ⦂ OPEN _ ?T ✼ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫'β€Ί (700)
]]
*)

paragraph β€ΉSyntaxβ€Ί

syntax π—ˆπ—‰π–Ύπ—‡  :: β€Ήlogicβ€Ί ("π—ˆπ—‰π–Ύπ—‡")
       π—ˆπ—‰π–Ύπ—‡' :: β€Ήnat β‡’ logicβ€Ί ("π—ˆπ—‰π–Ύπ—‡'(_')")

parse_ast_translation β€Ήlet open Ast in [
  (syntax_constβ€Ήπ—ˆπ—‰π–Ύπ—‡β€Ί, fn ctxt => fn args =>
      Appl [Constant const_syntaxβ€ΉOPENβ€Ί,
        Appl [Constant "_constrain", Constant const_syntaxβ€ΉPure.dummy_patternβ€Ί, Variable "\^E\^Fposition\^E<position>\^E\^F\^E"],
        Appl [Constant "_constrain", Constant const_syntaxβ€ΉPure.dummy_patternβ€Ί, Variable "\^E\^Fposition\^E<position>\^E\^F\^E"]] ),
  (syntax_constβ€Ήπ—ˆπ—‰π–Ύπ—‡'β€Ί, fn ctxt => fn args =>
      Appl [Constant const_syntaxβ€ΉOPENβ€Ί,
        hd args,
        Appl [Constant "_constrain", Constant const_syntaxβ€ΉPure.dummy_patternβ€Ί, Variable "\^E\^Fposition\^E<position>\^E\^F\^E"]] )
] endβ€Ί


paragraph β€ΉApplicationβ€Ί

(* deprecated
lemma open_abstraction_Ο†app:
  β€Ή Friendly_Help TEXT(β€ΉJust tell me which Ο†-type you want to open.β€Ί ⏎
      β€ΉInput a lambda abstraction e.g. β€ΉΞ»x. List (Box x)β€Ί as a pattern where the lambda variable is the Ο†-type you want to destruct.β€Ί
      β€ΉI will matchβ€Ί T β€Ήwith the pattern.β€Ί ⏎
      β€ΉYou can also use an underscore to denote the target Ο†-type in this pattern so you don't need to write a lambda abstraction, e.g. β€ΉList (Box _)β€Ίβ€Ί)
⟹ 𝗉𝖺𝗋𝖺𝗆 target
⟹ π–½π—ˆ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag to (target (OPEN i any))
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 Pβ€Ί
  unfolding Do_def Action_Tag_def . *)

lemma ―‹fallbackβ€Ί
  [Ο†reason default %To_ToA_fallback for β€Ή_ ⦂ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag to (OPEN _ _)β€Ί]:
  β€Ή FAIL TEXT(β€ΉFail to destruct Ο†-typeβ€Ί T)
⟹ x ⦂ Any π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag to (OPEN i T) β€Ί
  unfolding FAIL_def
  by blast


paragraph β€ΉTransformationβ€Ί

Ο†reasoner_group
      ToA_open_entry = (%ToA_splitting-30, [%ToA_splitting-30, %ToA_splitting-30]) β€Ήβ€Ί
  and ToA_open_to_entry = (%To_ToA_derived-10, [%To_ToA_derived-10, %To_ToA_derived-10]) β€Ήβ€Ί
  and ToA_open_all = (100, [10, 3000]) β€Ήβ€Ί
  and ToA_open = (1020,[1000,1040]) in ToA_open_all β€Ήβ€Ί
  and ToA_open_red = (2500, [2500, 2600]) in ToA_open_all and > ToA_open β€Ήβ€Ί
  and ToA_open_fail = (10, [10,10]) in ToA_open_all and < ToA_open β€Ήβ€Ί


subparagraph β€ΉSystemβ€Ί

lemma [Ο†reason %ToA_open_to_entry for β€Ή_ ⦂ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _  𝗐𝗂𝗍𝗁 _ @tag to (OPEN _ _)β€Ί]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y' ⦂ U @tag OPEN i 𝒯𝒫'
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. y = y' @tag to (OPEN i T) β€Ί
  unfolding Action_Tag_def Simplify_def 𝗋Guard_def Premise_def
  by simp

lemma [Ο†reason %ToA_open_red]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U @tag OPEN i 𝒯𝒫'
⟹ x ⦂ 𝗏𝖺𝗅[v] T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ 𝗏𝖺𝗅[v] U @tag OPEN i 𝒯𝒫' β€Ί
  unfolding Action_Tag_def Transformation_def
  by simp

lemma [Ο†reason %ToA_open_entry]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ OP @tag OPEN i 𝒯𝒫
⟹ OP π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ x ⦂ OPEN i T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫 β€Ί
  unfolding Action_Tag_def OPEN_def
  using mk_elim_transformation by blast

lemma [Ο†reason %ToA_open_entry]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ OP @tag OPEN i 𝒯𝒫
⟹ OP * W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ (x ⦂ OPEN i T) * W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫 β€Ί
  unfolding Action_Tag_def OPEN_def
  using mk_elim_transformation transformation_right_frame by blast

lemma [Ο†reason %ToA_open_entry]:
  β€Ή fst x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ m ⦂ M @tag OPEN i 𝒯𝒫'
⟹ (m, snd x) ⦂ M ✼ W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ R 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫'
⟹ x ⦂ OPEN i T ✼ W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ R 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫' β€Ί
  unfolding Action_Tag_def OPEN_def Ο†Prod'_def
  by (smt (z3) Ο†Prod_expn' prod.exhaust_sel transformation_right_frame transformation_trans)


lemma [Ο†reason %ToA_open_red for β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag OPEN undefined _β€Ί]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag OPEN some A
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag OPEN undefined A β€Ί
  unfolding Action_Tag_def
  by simp

lemma [Ο†reason %ToA_open_red for β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag OPEN (Suc 0) _β€Ί]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag OPEN 1 A
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag OPEN (Suc 0) A β€Ί
  unfolding Action_Tag_def
  by simp

lemma [Ο†reason default %ToA_open_fail for β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag OPEN _ _β€Ί]:
  β€Ή ERROR TEXT(β€Ήtheβ€Ί i β€Ήth constructor ofβ€Ί T β€Ήis unknownβ€Ί)
⟹ x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P @tag OPEN i A β€Ί
  unfolding ERROR_def by simp


paragraph β€ΉReasoning Setupβ€Ί

ML β€Ή
structure Gen_Open_Abstraction_SS = Simpset (
  val initial_ss = Simpset_Configure.Minimal_SS
  val binding = SOME bindingβ€Ήgen_open_abstraction_simpsβ€Ί
  val comment = "Simplification rules used when generating open-abstraction rules"
  val attribute = NONE
  val post_merging = I
) β€Ί

setup β€ΉContext.theory_map (Gen_Open_Abstraction_SS.map (fn ctxt =>
          ctxt addsimprocs [simprocβ€Ήdefined_Exβ€Ί, simprocβ€Ήdefined_Allβ€Ί, simprocβ€ΉNO_MATCHβ€Ί]
               addsimps @{thms' HOL.simp_thms}
            |> Simplifier.add_cong @{thm' mk_symbol_cong}))β€Ί


paragraph β€ΉRules of Various Reasoningβ€Ί

lemma [Ο†reason %extract_pure]:
  β€Ή x ⦂ T π—‚π—†π—‰π—…π—‚π–Ύπ—Œ P
⟹ x ⦂ OPEN i T π—‚π—†π—‰π—…π—‚π–Ύπ—Œ P β€Ί
  unfolding OPEN_def .

lemma [Ο†reason %extract_pure]:
  β€Ή P π—Œπ—Žπ–Ώπ–Ώπ—‚π–Όπ–Ύπ—Œ x ⦂ T
⟹ P π—Œπ—Žπ–Ώπ–Ώπ—‚π–Όπ–Ύπ—Œ x ⦂ OPEN i T β€Ί
  unfolding OPEN_def .

lemma [Ο†reason %abstract_domain]:
  β€Ή Abstract_Domain T D
⟹ Abstract_Domain (OPEN i T) D β€Ί
  unfolding OPEN_def .

lemma abstract_domain_OPEN:
  β€Ή (β‹€x. x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U' π—Œπ—Žπ–»π—ƒ y. r x y @tag to (OPEN i T))
⟹ Abstract_Domain U' D
⟹ Abstract_Domain (OPEN i T) (Ξ»x. βˆƒy. r x y ∧ D y) β€Ί
  unfolding OPEN_def Abstract_Domain_def Action_Tag_def 𝗋EIF_def Transformation_def Satisfiable_def
  by clarsimp blast

lemma [Ο†reason %abstract_domain]:
  β€Ή Abstract_DomainL T D
⟹ Abstract_DomainL (OPEN i T) D β€Ί
  unfolding OPEN_def .

lemma [Ο†reason %identity_element_cut]:
  β€Ή Identity_ElementsI T D P
⟹ Identity_ElementsI (OPEN i T) D P β€Ί
  unfolding OPEN_def .

lemma [Ο†reason %identity_element_cut]:
  β€Ή Identity_ElementsE T D
⟹ Identity_ElementsE (OPEN i T) D β€Ί
  unfolding OPEN_def .

lemma Identity_ElementsI_OPEN:
  β€Ή (β‹€x. x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. r x y @tag to (OPEN i T))
⟹ Identity_ElementsI U D P
⟹ Identity_ElementsI (OPEN i T) (Ξ»x. βˆ€y. r x y ∧ D y) (Ξ»x. βˆƒy. r x y ∧ P y) β€Ί
  unfolding Identity_ElementsI_def Identity_ElementI_def Transformation_def Action_Tag_def OPEN_def
  by clarsimp blast


lemma [Ο†reason %Ο†functionality]:
  β€Ή Functionality T P
⟹ Functionality (OPEN i T) P β€Ί
  unfolding Functionality_def OPEN_def
  by clarsimp

lemma Functionality_OPEN:
  β€Ή (β‹€x. x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. r x y @tag to (OPEN i T))
⟹ Functionality U P
⟹ Functionality (OPEN i T) (Ξ»x. (βˆ€y. r x y ⟢ P y) ∧ (βˆ€y1 y2. r x y1 ∧ r x y2 ⟢ y1 = y2)) β€Ί
  unfolding Functionality_def Action_Tag_def OPEN_def Transformation_def
  by clarsimp metis

bundle Functionality_OPEN = Functionality_OPEN[Ο†reason %Ο†functionality+10]

lemma [Ο†reason %carrier_set_cut]:
  β€Ή Carrier_Set T D
⟹ Carrier_Set (OPEN i T) D β€Ί
  unfolding Carrier_Set_def Within_Carrier_Set_def Action_Tag_def OPEN_def
  by clarsimp



lemma Carrier_Set_OPEN[Ο†reason %carrier_set_cut]:
  β€Ή (β‹€x. x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ y ⦂ U π—Œπ—Žπ–»π—ƒ y. r x y @tag to (OPEN i T))
⟹ Carrier_Set U D
⟹ Carrier_Set (OPEN i T) (Ξ»x. βˆ€y. r x y ⟢ D y) β€Ί
  unfolding Carrier_Set_def Within_Carrier_Set_def Action_Tag_def Transformation_def OPEN_def
  by clarsimp blast

bundle Carrier_Set_OPEN = Carrier_Set_OPEN[Ο†reason %carrier_set_cut+10]



subsubsection β€ΉMake Abstractionβ€Ί

text β€ΉApplies one step of constructingβ€Ί

definition MAKE :: β€Ήnat β‡’ 'x β‡’ 'xβ€Ί
  where [assertion_simps_source, Ο†programming_simps]: β€ΉMAKE i X ≑ Xβ€Ί
  ― β€ΉWhen the definition of the Ο†-type involves multiple equations, β€Ήiβ€Ί hints which equation should be used.
     β€Ήiβ€Ί can be a unknown variable to let the reasoner infer the proper one but it can fail and when it
     fails branches diverge for each equation.β€Ί

declare [[
  Ο†reason_default_pattern
      β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ ?Y 𝗐𝗂𝗍𝗁 ?P @tag MAKE ?i ?Aβ€Ί β‡’
      β€ΉERROR TEXT(β€ΉMalformed ruleβ€Ί (?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ ?Y 𝗐𝗂𝗍𝗁 ?P @tag MAKE ?i ?A))β€Ί (1)
  and β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ?T @tag MAKE _ 𝒯𝒫› β‡’ β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ?T @tag MAKE _ 𝒯𝒫 β€Ί (100)
  and β€Ή?var ⦂ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ?T @tag MAKE _ 𝒯𝒫'β€Ί β‡’ β€Ή_ ⦂ _ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ?T @tag MAKE _ 𝒯𝒫' β€Ί (100)
]]

declare [[
  Ο†reason_default_pattern β€Ή?X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (y ⦂ ?U π—Œπ—Žπ–»π—ƒ y. ?R y) 𝗐𝗂𝗍𝗁 _ @tag to (MAKE _ _)β€Ί β‡’
     β€ΉERROR TEXT(β€ΉThere is no need to declare a To-Transformation rule for MAKE. Just use the normal ToA and synthesisβ€Ί)β€Ί (200)
  and β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ MAKE _ ?T 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί β‡’ β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ MAKE _ ?T 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί (700)
  and β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ MAKE _ ?T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί β‡’
      β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ MAKE _ ?T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί (700)
  and β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ● MAKE _ ?T 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί β‡’ β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ● MAKE _ ?T 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί (700)
  and β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ● MAKE _ ?T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί β‡’
      β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ ⦂ ● MAKE _ ?T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 β€Ί (700)
]]

Ο†reasoner_group ToA_Make_all = (100, [10, 3000]) β€Ήβ€Ί
  and ToA_Make = (1020, [1000, 1040]) in ToA_Make_all β€Ήβ€Ί
  and ToA_Make_fallback = (20, [10,30]) in ToA_Make_all and < ToA_Make β€Ήβ€Ί
  and ToA_Make_norm = (2000, [2000,2200]) in ToA_Make_all and > ToA_Make β€Ήβ€Ί
  and ToA_Make_top = (2800, [2800,2830]) in ToA_Make_all and > ToA_Make_norm β€Ήβ€Ί

  and ToA_Make_entry = (%ToA_splitting_source+30, [%ToA_splitting_source+30, %ToA_splitting_source+30])
                      in ToA and > ToA_splitting_source and < ToA_splitting_target
      β€ΉTransformation rules that making the annotated Ο†-type. The tag β€ΉMAKEβ€Ί emphasizes the user's intention
       to apply the Ο†-type construction rules which are normally not activated in the usual reasoning.β€Ί


ML_file β€Ήlibrary/syntax/make_and_open.MLβ€Ί

paragraph β€ΉSugarβ€Ί

Ο†lang_parser π—†π–Ίπ—„π–Ύπ—Œ (%Ο†parser_unique, 0) ["π—†π–Ίπ—„π–Ύπ—Œ"] (β€ΉPROP _β€Ί)
β€Ή fn s => Args.$$$ "π—†π–Ίπ—„π–Ύπ—Œ" |-- Scan.option (keywordβ€Ή(β€Ί |-- Parse.nat --| keywordβ€Ή)β€Ί) --
          Parse.position (Parse.group (fn () => "term") (Parse.inner_syntax (Parse.cartouche || Parse.number)))
       >> (fn (n,term) =>
          phi_synthesis_parser s (fn _ => fn term =>
            let val make = Const(const_nameβ€ΉMAKEβ€Ί, dummyT)
                              $ (case n of NONE => Term.dummy
                                         | SOME N => HOLogic.mk_number Typeβ€Ήnatβ€Ί N)
                fun mark ((t1 as Const(const_nameβ€ΉΟ†Typeβ€Ί, _)) $ t2 $ t3)
                      = t1 $ t2 $ (make $ t3)
                  | mark t3 = make $ t3
             in mark term
            end) term ) β€Ί

paragraph β€ΉSystemβ€Ί

lemma [Ο†reason %ToA_Make_entry]:
  β€Ή M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T @tag MAKE i 𝒯𝒫
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ M 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ MAKE i T 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫 β€Ί
  unfolding Action_Tag_def MAKE_def
  using mk_intro_transformation by blast

lemma [Ο†reason %ToA_Make_entry]:
  β€Ή M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T @tag MAKE i 𝒯𝒫
⟹ π—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[assertion_simps TARGET] M' : Ξ¨[Some] M
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ M' 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ ● MAKE i T 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫 β€Ί
  unfolding Action_Tag_def MAKE_def Transformation_def Simplify_def
  by simp blast

lemma [Ο†reason %ToA_Make_entry]:
  β€Ή M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T @tag MAKE i 𝒯𝒫
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ M π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ R 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ MAKE i T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ R 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫 β€Ί
  unfolding Action_Tag_def MAKE_def
  by (smt (z3) REMAINS_expn Transformation_def sep_conj_expn)

lemma [Ο†reason %ToA_Make_entry]:
  β€Ή M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T @tag MAKE i 𝒯𝒫
⟹ π—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[assertion_simps TARGET] M' : Ξ¨[Some] M
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ M' π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ R 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ ● MAKE i T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ R 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫 β€Ί
  unfolding Action_Tag_def MAKE_def Transformation_def Simplify_def
  by simp meson
  

lemma [Ο†reason %ToA_Make_entry]:
  β€Ή fst m ⦂ M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T @tag MAKE i 𝒯𝒫'
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ m ⦂ M ✼ R @tag 𝒯𝒫'
⟹ X π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ (x, snd m) ⦂ MAKE i T ✼ R @tag 𝒯𝒫' β€Ί
  unfolding Action_Tag_def MAKE_def Ο†Prod'_def
  apply (simp add: Ο†Prod_expn'' Ο†Prod_expn')
  using mk_intro_transformation transformation_right_frame by blast
  
lemma [Ο†reason default %ToA_Make_fallback for β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ @tag MAKE _ _β€Ί]:
  β€Ή ERROR TEXT(β€Ήtheβ€Ί i β€Ήth constructor ofβ€Ί T β€Ήis unknownβ€Ί)
⟹ M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ T @tag MAKE i A β€Ί
  unfolding ERROR_def by simp

lemma [Ο†reason %ToA_Make_norm for β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ @tag MAKE undefined _β€Ί]:
  β€Ή M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ N @tag MAKE some A
⟹ M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ N @tag MAKE undefined A β€Ί
  unfolding Action_Tag_def
  by simp

lemma [Ο†reason %ToA_Make_norm for β€Ή_ π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ _ @tag MAKE (Suc 0) _β€Ί]:
  β€Ή M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ N @tag MAKE 1 A
⟹ M π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ N @tag MAKE (Suc 0) A β€Ί
  unfolding Action_Tag_def
  by simp

paragraph β€ΉReductions in Sourceβ€Ί

text β€Ήβ€ΉMAKEβ€Ί tag in source is senselessβ€Ί

lemma [Ο†reason %ToA_red]:
  β€Ή x ⦂ T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P
⟹ x ⦂ MAKE i T π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding MAKE_def
  by simp

lemma [Ο†reason %ToA_red]:
  β€Ή x ⦂ T ✼ W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P
⟹ x ⦂ MAKE i T ✼ W π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ Y 𝗐𝗂𝗍𝗁 P β€Ί
  unfolding MAKE_def
  by simp


paragraph β€ΉRules of Various Reasoningβ€Ί

lemma [Ο†reason %extract_pure]:
  β€Ή x ⦂ T π—‚π—†π—‰π—…π—‚π–Ύπ—Œ P
⟹ x ⦂ MAKE i T π—‚π—†π—‰π—…π—‚π–Ύπ—Œ P β€Ί
  unfolding MAKE_def .

lemma [Ο†reason %extract_pure]:
  β€Ή P π—Œπ—Žπ–Ώπ–Ώπ—‚π–Όπ–Ύπ—Œ x ⦂ T
⟹ P π—Œπ—Žπ–Ώπ–Ώπ—‚π–Όπ–Ύπ—Œ x ⦂ MAKE i T β€Ί
  unfolding MAKE_def .

lemma abstract_domain_MAKE:
  β€Ή (β‹€x. X x π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ MAKE i T 𝗐𝗂𝗍𝗁 PP)
⟹ (β‹€x. D x π—Œπ—Žπ–Ώπ–Ώπ—‚π–Όπ–Ύπ—Œ X x)
⟹ Abstract_DomainL (MAKE i T) D β€Ί
  unfolding MAKE_def Abstract_DomainL_def 𝗋ESC_def Transformation_def Action_Tag_def Satisfiable_def
  by clarsimp blast

Ο†reasoner_group abstract_domain_OPEN_MAKE = (%abstract_domain+100, [%abstract_domain+100, %abstract_domain+100])
                                             in abstract_domain_all and > abstract_domain β€Ήβ€Ί

bundle abstract_domain_OPEN_MAKE =
  abstract_domain_MAKE[Ο†adding_property = false,
                       Ο†reason %abstract_domain_OPEN_MAKE,
                       Ο†adding_property = true]
  abstract_domain_OPEN[Ο†adding_property = false,
                       Ο†reason %abstract_domain_OPEN_MAKE,
                       Ο†adding_property = true]


lemma [Ο†reason %abstract_domain]:
  β€Ή Abstract_Domain T D
⟹ Abstract_Domain (MAKE i T) D β€Ί
  unfolding MAKE_def .

(*
lemma [Ο†reason %abstract_domain]:
  β€Ή Abstract_DomainL T D
⟹ Abstract_DomainL (MAKE T) D β€Ί
  unfolding MAKE_def .
*)

lemma [Ο†reason %identity_element_cut]:
  β€Ή Identity_ElementsI T D P
⟹ Identity_ElementsI (MAKE i T) D P β€Ί
  unfolding MAKE_def .

lemma [Ο†reason %identity_element_cut]:
  β€Ή Identity_ElementsE T D
⟹ Identity_ElementsE (MAKE i T) D β€Ί
  unfolding MAKE_def .

lemma Identity_ElementsE_MAKE:
  β€Ή (β‹€x. X x π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ MAKE i T 𝗐𝗂𝗍𝗁 PP)
⟹ (β‹€x. π—Œπ—‚π—†π—‰π—…π—‚π–Ώπ—’[mode_embed_into_Ο†type] (f x ⦂ U) : X x)
⟹ Identity_ElementsE U D
⟹ Identity_ElementsE (MAKE i T) (D o f) β€Ί
  unfolding Identity_ElementsE_def Simplify_def Transformation_def Identity_ElementE_def
  apply clarsimp
  by metis

bundle Identity_Elements_OPEN_MAKE =
  Identity_ElementsI_OPEN [Ο†adding_property = false,
                           Ο†reason %identity_element_OPEN_MAKE,
                           Ο†adding_property = true]
  Identity_ElementsE_MAKE [Ο†adding_property = false,
                           Ο†reason %identity_element_OPEN_MAKE,
                           Ο†adding_property = true]

lemma [Ο†reason %carrier_set_cut]:
  β€Ή Carrier_Set T D
⟹ Carrier_Set (MAKE i T) D β€Ί
  unfolding Carrier_Set_def Within_Carrier_Set_def Action_Tag_def MAKE_def
  by clarsimp

lemma [Ο†reason %Ο†functionality]:
  β€Ή Functionality T P
⟹ Functionality (MAKE i T) P β€Ί
  unfolding Functionality_def MAKE_def
  by clarsimp

paragraph β€ΉSetup Synthesis Moduleβ€Ί

lemma [Ο†reason default %Ο†synthesis_cut for β€Ήπ—‰π—‹π—ˆπ–Ό _ ⦃ _ ⟼ Ξ»v. ?x ⦂ MAKE ?i ?T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ ?R ⦄ π—π—π—‹π—ˆπ—π—Œ _ @tag synthesisβ€Ί]:
  β€Ή S1 π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x ⦂ MAKE i T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ S2 𝗐𝗂𝗍𝗁 Any
⟹ π—‰π—‹π—ˆπ–Ό Return Ο†V_none ⦃ S1 ⟼ Ξ»v. x ⦂ MAKE i T π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ S2 ⦄ @tag synthesisβ€Ί
  unfolding MAKE_def Action_Tag_def
  using Ο†__Return_rule__ view_shift_by_implication by blast



subsection β€ΉSplitβ€Ί

consts π’œassoc :: β€Ή'a β‡’ 'b β‡’ modeβ€Ί
       π’œscalar :: β€Ή'a β‡’ 'b β‡’ modeβ€Ί
       π’œsplit :: β€Ήmode β‡’ ('a,'b) Ο†β€Ί ("π—Œπ—‰π—…π—‚π—[_]" [100] 1000)

abbreviation π’œsplit_default ("π—Œπ—‰π—…π—‚π—")
  where β€Ήπ’œsplit_default ≑ π’œsplit defaultβ€Ί

abbreviation π’œsplit_assoc ("π—Œπ—‰π—…π—‚π—-π–Ίπ—Œπ—Œπ—ˆπ–Ό")
  where β€Ήπ’œsplit_assoc a b ≑ π’œsplit (π’œassoc a b)β€Ί

abbreviation π’œsplit_scalar ("π—Œπ—‰π—…π—‚π—-π—Œπ–Όπ–Ίπ—…π–Ίπ—‹")
  where β€Ήπ’œsplit_scalar a b ≑ π’œsplit (π’œscalar a b)β€Ί

text β€ΉSyntax:

β–ͺ termβ€Ήto (List (π—Œπ—‰π—…π—‚π— βˆ— other))β€Ί splits for instance termβ€ΉList ((A βˆ— B) βˆ— other)β€Ί into
  termβ€ΉList (A βˆ— other)β€Ί and termβ€ΉList (B βˆ— other)β€Ί, leaving the termβ€Ήotherβ€Ί unchanged.

β–ͺ termβ€Ήto (π—π—‹π–Ίπ—π–Ύπ—‹π—Œπ–Ύ 𝗉𝖺𝗍𝗍𝖾𝗋𝗇 pat β‡’ π—Œπ—‰π—…π—‚π—)β€Ί splits any sub-Ο†type matching the pattern

β€Ί

lemma [Ο†reason %To_ToA_cut]:
  β€Ή x ⦂ T βˆ— U π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ x' ⦂ T βˆ—π’œ U π—Œπ—Žπ–»π—ƒ x'. x' = x @tag to π—Œπ—‰π—…π—‚π— β€Ί
  unfolding Action_Tag_def Transformation_def Bubbling_def
  by (simp add: ExBI_defined)


subsection β€ΉDuplicate \& Shrinkβ€Ί

consts action_dup    :: β€Ήactionβ€Ί
       action_shrink :: β€Ήactionβ€Ί
       action_drop   :: β€Ήactionβ€Ί

lemma dup_Ο†app:
  β€ΉCall_Action (π’œ_transformation (π’œ_leading_item (π’œ_structural_1_2 action_dup)))β€Ί ..

lemma shrink_Ο†app:
  β€ΉCall_Action (π’œ_transformation (multi_arity (π’œ_structural_2_1 action_shrink)))β€Ί ..

lemma drop_Ο†app:
  β€ΉCall_Action (π’œ_view_shift_or_imp (multi_arity action_drop))β€Ί ..


section β€ΉSupplementary of Reasoningβ€Ί

(*TODO move me! see Phi_BI.thy/Basic_Ο†Types/Itself/Construction from Raw Abstraction*)

subsection β€ΉMake Abstraction from Raw Representationβ€Ί
    ― β€Ήis a sort of reasoning process useful later in making initial Hoare triples from semantic raw
      representation (which are represented by Itself, i.e., no abstraction).β€Ί

text β€ΉPreviously, we introduced β€Ήto Itselfβ€Ί transformation which gives the mechanism reducing
  an abstraction back to the concrete raw representation.
  To be its counterpart, this section presents the mechanism recovering abstractions
  from a raw concrete representation.β€Ί




end