Theory IDE_CP_Reasoning1

chapter ‹Reasoning Processes in IDE-CP - Part I›

text ‹The part includes small process that can be built without infrastructure of
  IDE-CP, and declarations of other large process.›

theory IDE_CP_Reasoning1
  imports Spec_Framework Phi_BI.Phi_BI
  abbrevs "<subj-reasoning>" = "𝗌𝗎𝖻𝗃-𝗋𝖾𝖺𝗌𝗈𝗇𝗂𝗇𝗀"
begin

section ‹Annotations Guiding the Reasoning›

subsection ‹Small Annotations›

subsubsection ‹Matches›

definition Assertion_Matches :: ‹'a BI ⇒ 'a BI ⇒ 'a BI› (infixl "<matches>" 18)
  where ‹(S <matches> pattern) = S›

text ‹The annotation marking on a target \<^term>‹Y <matches> A› in a ToA or a view shift
  restricts that the source have to first match pattern ‹A›.›

lemma [φreason 2000]:
  ‹Matches X A ⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P ⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 (Y <matches> A) 𝗐𝗂𝗍𝗁 P›
  unfolding Assertion_Matches_def .

lemma [φreason 2000]:
  ‹Matches X A ⟹ X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P ⟹ X 𝗌𝗁𝗂𝖿𝗍𝗌 (Y <matches> A) 𝗐𝗂𝗍𝗁 P›
  unfolding Assertion_Matches_def .

subsubsection ‹Useless Tag›

definition USELESS :: ‹bool ⇒ bool› where ‹USELESS x = x›

lemma [simp]: ‹USELESS True› unfolding USELESS_def ..

text ‹Simplification plays an important role in the programming in IDE_CP.
  We use it to simplify the specification and evaluate the abstract state.

  It is powerful as a transformation preserving all information,
  but sometimes we expect the transformation is weaker and unequal by disposing
  some useless information that we do not need.
  For example, we want to rewrite \<^term>‹x ⦂ T› to \<^term>‹y ⦂ U› but the rewrite may be held
  only with an additional proposition \<^term>‹Useless› which is useless for us,
  \[ \<^prop>‹x ⦂ T ≡ y ⦂ U 𝗌𝗎𝖻𝗃 Useless› \]
  In cases like this, we can wrap the useless proposition by tag ‹‹USELESS››,
  as \<^prop>‹x ⦂ T ≡ y ⦂ U 𝗌𝗎𝖻𝗃 USELESS Useless›. The equality is still held because
  \<^prop>‹USELESS P ≡ P›, but IDE-CP is configured to drop the \<^prop>‹Useless›
  so the work space will not be polluted by helpless propositions.
›

subsubsection ‹Generated Rules during Reasoning or Programming›

text ‹Annotate a rule generated during the programming, to differentiate from the normal
  contextual facts. The normal facts are stored in ‹φlemmata› while the generated rules
  are in ‹φgenerated› (or maybe a better name like φgenerated_rules?)›


text ‹TODO: update this

Note, the argument here means any φ-Type in the pre-condition, not necessary argument value.

  If in a procedure or an implication rule or a view shift rule,
  there is an argument where the procedure or the rule retains its structure,
  this argument can be marked by \<^term>‹SMORPH arg›.

  Recall when applying the procedure or the rule, the reasoner extracts \<^term>‹arg› from the
    current φ-BI specification \<^term>‹X› of the current sequent.
  This extraction may break \<^term>‹X› especially when the \<^term>‹arg› to be extracted is
    scattered and embedded in multiple φ-Types in \<^term>‹X›.
  For example, extract \<^term>‹(x1, y2) ⦂ (A1 * B2)› from
    \<^term>‹((x1, x2) ⦂ (A1 * A2)) * ((y1, (y2, y3)) ⦂ (B1 * (B2 * B3)))›.
  After the application, the following sequent will have broken structures because
    the original structure of \<^term>‹X› is destroyed in order to extract \<^term>‹arg›.
  However, the structure of the new \<^term>‹arg'› may not changes.
  If so, by reversing the extraction, it is possible to recovery the original structure of \<^term>‹X›,
    only with changed value of the corresponding part of \<^term>‹arg› in \<^term>‹X›.

  The system supports multiple arguments to be marked by \<^term>‹SMORPH arg›.
  And the system applies the reverse morphism in the correct order.
  A requirement is,
  those structural-retained argument should locate at the end of the procedure's or the rule's
    argument list. Or else, because the reasoner does not record the extraction morphism of
    arguments not marked by \<^term>‹SMORPH arg›, those arguments which occur after the
    structural-retained arguments change the φ-BI specification by their extraction
    causing the recorded morphism of previous \<^term>‹SMORPH arg› mismatch the current
    φ-BI specification and so possibly not able to be applied any more.
›


subsubsection ‹Beta-reduction Hint for φ-Type›

definition β_Hint_for_φ (binder "λ⇩β " 10)
  where ‹β_Hint_for_φ f ≡ f›

text ‹Occasionally, it can be convenient technically to use ‹x ⦂ (λa. S a)› that will be β-reduced
      transparently to ‹S›. The tag \<^const>‹β_Hint_for_φ› allowing syntax ‹x ⦂ (λ⇩β a. S a)› hints
      the reasoner to β-reduce the φ-type term.›

lemma β_Hint_for_φ[simp]:
  ‹x ⦂ (λ⇩β y. S y) ≡ S x›
  unfolding β_Hint_for_φ_def φType_def .

paragraph ‹Identity_Element›

lemma [φreason %cutting]:
  ‹ Identity_Element⇩I (S x) P
⟹ Identity_Element⇩I (x ⦂ (λ⇩β y. S y)) P ›
  by simp

lemma [φreason %cutting]:
  ‹ Identity_Element⇩E (S x)
⟹ Identity_Element⇩E (x ⦂ (λ⇩β y. S y)) ›
  by simp

paragraph ‹Transformation Rules›

lemma [φreason 1000]:
  ‹ S x 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P
⟹ x ⦂ (λ⇩β y. S y) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P ›
  by simp

(*TODO! this 𝒜?!*)
lemma [φreason 1000]:
  ‹ S x 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P @tag 𝒜
⟹ x ⦂ (λ⇩β y. S y) 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P @tag 𝒜 ›
  by simp

lemma [φreason 1000]:
  ‹ S x * R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P
⟹ (x ⦂ (λ⇩β y. S y)) * R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P ›
  by simp

lemma [φreason 1000]:
  ‹ S x * R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P @tag 𝒜
⟹ (x ⦂ (λ⇩β y. S y)) * R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P @tag 𝒜 ›
  by simp

lemma [φreason 1000]:
  ‹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S x 𝗐𝗂𝗍𝗁 P
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ (λ⇩β y. S y) 𝗐𝗂𝗍𝗁 P ›
  by simp

lemma [φreason 1000]:
  ‹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S x 𝗐𝗂𝗍𝗁 P @tag 𝒜
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ (λ⇩β y. S y) 𝗐𝗂𝗍𝗁 P @tag 𝒜 ›
  by simp

lemma [φreason 1000]:
  ‹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S x 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ (λ⇩β y. S y) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P ›
  by simp

lemma [φreason 1000]:
  ‹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S x 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag 𝒜
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ (λ⇩β y. S y) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag 𝒜 ›
  by simp



section ‹Small Reasoning Process›

subsection ‹Auxiliaries›


subsubsection ‹Semantic Expansion of φ-Types›

consts MODE_φEXPN :: mode ― ‹relating to named_theorems ‹φexpn››

abbreviation φexpn_Premise ("<φexpn> _" [26] 26) where ‹φexpn_Premise ≡ Premise MODE_φEXPN›

φreasoner_ML φexpn_Premise 10 (‹<φexpn> ?P›) = ‹
  Seq.ORELSE (
  Phi_Reasoners.wrap (PLPR_Simplifier.simplifier (K Seq.empty) (fn ctxt =>
                            ctxt addsimps (Useful_Thms.get ctxt)) {fix_vars=false}),
  Phi_Reasoners.wrap (PLPR_Simplifier.simplifier (K Seq.empty) (fn ctxt =>
        Phi_Expansions.enhance (ctxt addsimps (Useful_Thms.get ctxt))) {fix_vars=false})) o snd
›

lemma Premise_MODE_φEXPN[iff]: ‹<φexpn> True›
  unfolding Premise_def ..

text ‹Antecedent \<^prop>‹<φexpn> P› indicates the reasoner solving the premise \<^prop>‹P› using
  simplification rules of ‹φexpns›.›

subsubsection ‹Name tag by type›

(*TODO: elaborate this*)

datatype ('x, 'name) named (infix "<named>" 30) = tag 'x (*TODO: rename!!*)

syntax "__named__" :: ‹logic ⇒ tuple_args ⇒ logic› (infix "<<named>>" 25)


ML_file ‹library/syntax/name_by_type.ML›

text ‹It is a tool to annotate names on a term, e.g. \<^term>‹x <<named>> a, b›.
  The name tag is useful in lambda abstraction (including quantification) because the
  name of an abstraction variable is not preserved in many transformation especially
  simplifications. The name can be useful in the deductive programming, e.g. universally
  quantified variables in a sub-procedure like
  \[ ‹∀x y. proc f ⦃ VAL x ⦂ T❟ VAL y ⦂ U ⟼ any ⦄ ⟹ any'› \]
  When starting to write the sub-procedure f by command ‹❴›, φ-system fixes variables x and y
    with the name of x and y. The name of x and y then are significant for programming.
  To preserve the name, we use \<^typ>‹'any <named> 'φname_x × 'φname_y›,
    \<^prop>‹∀(x :: 'any <named> 'φname_x). sth›.
  We use free type variable to annotate it because it is most stable. No transformation
    changes the name of a free type variable.

  This feature is mostly used in ∗‹Expansion of Quantification› given in the immediate subsection.
  Therefore we put this part in the subsection of reasoning jobs, though itself is not related to
  any reasoning work.
›

lemma named_forall: "All P ⟷ (∀x. P (tag x))" by (metis named.exhaust)
lemma named_exists: "Ex P ⟷ (∃x. P (tag x))" by (metis named.exhaust)
lemma [simp]: "tag (case x of tag x ⇒ x) = x" by (cases x) simp
lemma named_All: "(⋀x. PROP P x) ≡ (⋀x. PROP P (tag x))"
proof fix x assume "(⋀x. PROP P x)" then show "PROP P (tag x)" .
next fix x :: "'a <named> 'b" assume "(⋀x. PROP P (tag x))" from ‹PROP P (tag (case x of tag x ⇒ x))› show "PROP P x" by simp
qed

lemma named_ExBI: "(∃*c. T c) = (∃*c. T (tag c) )" by (clarsimp simp add: named_exists BI_eq_iff)


subsubsection ‹Expansion of Quantification›

definition ‹eoq__fst = fst›
definition ‹eoq__snd = snd›

named_theorems named_expansion ‹Rewriting rules expanding named quantification.›

lemma eoq__fst[unfolded atomize_eq[symmetric], named_expansion]:
        ‹eoq__fst (x,y) = x› unfolding eoq__fst_def by simp
lemma eoq__snd[unfolded atomize_eq[symmetric], named_expansion]:
        ‹eoq__snd (x,y) = y› unfolding eoq__snd_def by simp

lemmas [unfolded atomize_eq[symmetric], named_expansion] =
  Product_Type.prod.case named.case id_apply

ML_file  "./library/tools/quant_expansion.ML"

hide_fact  eoq__fst eoq__snd
hide_const eoq__fst eoq__snd

simproc_setup named_forall_expansion ("All (P :: 'a <named> 'names ⇒ bool)") =
  ‹K (QuantExpansion.simproc_of
          (fn Type(\<^type_name>‹φarg›, _) => QuantExpansion.forall_expansion_arg_encoding
            | _ => QuantExpansion.forall_expansion))›

simproc_setup named_ex_expansion ("Ex (P :: 'a <named> 'names ⇒ bool)") =
  ‹K (QuantExpansion.simproc_of
          (fn Type(\<^type_name>‹φarg›, _) => QuantExpansion.exists_expansion_arg_encoding
            | _ => QuantExpansion.exists_expansion))›

simproc_setup named_exSet_expansion ("ExBI (P :: 'a <named> 'names ⇒ 'b BI)") =
  ‹K (QuantExpansion.simproc_of (K QuantExpansion.ExNu_expansion))›

simproc_setup named_metaAll_expansion ("Pure.all (P :: 'a <named> 'names ⇒ prop)") =
  ‹K (QuantExpansion.simproc_of
          (fn Type(\<^type_name>‹φarg›, _) => QuantExpansion.meta_All_expansion_arg_encoding
            | _ => QuantExpansion.meta_All_expansion))›

(*TODO: merge to procedure 1*)
ML_file "./library/syntax/procedure3.ML"


subsubsection ‹Rename λ-Abstraction›

definition rename_abstraction :: ‹'φname_name itself ⇒ 'a ⇒ 'a ⇒ bool›
  where ‹rename_abstraction name origin_abs named_abs ⟷ (origin_abs = named_abs)›

lemma rename_abstraction:
  ‹rename_abstraction name X X›
  unfolding rename_abstraction_def ..

φreasoner_ML rename_abstraction 1100 (‹rename_abstraction TYPE(?'name) ?Y ?Y'›) =
‹fn (_, (ctxt, sequent)) =>
  case Thm.major_prem_of sequent
    of \<^const>‹Trueprop› $ (Const (\<^const_name>‹rename_abstraction›, _)
                $ (Const (\<^const_name>‹Pure.type›, Type(\<^type_name>‹itself›, [name'])))
                $ Abs(_,ty,body)
                $ Var Y'') =>
      let
        val name = case Phi_Syntax.dest_name_tylabels name'
                     of [x] => x
                      | _ => raise TYPE ("only one name is expected", [name'], [])
        val Y' = Abs(name, ty, body) |> Thm.cterm_of ctxt
        val sequent = @{thm rename_abstraction} RS Thm.instantiate (TVars.empty, Vars.make [(Y'',Y')]) sequent
      in
        Seq.single (ctxt, sequent)
      end
     | term => raise THM ("Bad shape of rename_abstraction antecedent", 0, [sequent])
›

hide_fact rename_abstraction


subsubsection ‹λ-Abstraction Tag›

definition "lambda_abstraction" :: " 'a ⇒ 'b ⇒ ('a ⇒ 'b) ⇒ bool "
  where "lambda_abstraction x Y Y' ⟷ Y' x = Y"

lemma lambda_abstraction: "lambda_abstraction x (Y' x) Y'"
  unfolding lambda_abstraction_def ..

lemma [φreason 1200 for ‹lambda_abstraction (?x,?y) ?fx ?f›]:
  ‹ lambda_abstraction y fx f1
⟹ lambda_abstraction x f1 f2
⟹ lambda_abstraction (x,y) fx (case_prod f2)›
  unfolding lambda_abstraction_def by simp

φreasoner_ML lambda_abstraction 1100 ("lambda_abstraction ?x ?Y ?Y'") = ‹fn (_, (ctxt, sequent)) =>
  let
    val (Vs, _, \<^const>‹Trueprop› $ (Const (\<^const_name>‹lambda_abstraction›, _) $ x $ Y $ _))
      = Phi_Help.leading_antecedent (Thm.prop_of sequent)
    val Y' = Abs("", fastype_of x, abstract_over (x, Y))
    val idx = Thm.maxidx_of sequent + 1
    val vars = map Var (List.tabulate (length Vs, (fn i => ("v", i+idx))) ~~ map snd Vs)
    fun subst X = Term.subst_bounds (vars, X)
    val idx = idx + length Vs
    val rule = Drule.infer_instantiate ctxt
                  (map (apsnd (Thm.cterm_of ctxt)) [(("x",idx), subst x), (("Y'",idx),subst Y')])
                  (Thm.incr_indexes idx @{thm lambda_abstraction})
  in
    Seq.single (ctxt, rule RS sequent)
  end
›

hide_fact lambda_abstraction

lemma [φreason 1200 for ‹lambda_abstraction (tag ?x) ?fx ?f›]:
  ‹ lambda_abstraction x fx f
⟹ rename_abstraction TYPE('name) f f'
⟹ lambda_abstraction (tag x :: 'any <named> 'name) fx (case_named f')›
  unfolding lambda_abstraction_def rename_abstraction_def by simp


subsubsection ‹Introduce Frame Variable›

named_theorems frame_var_rewrs ‹Rewriting rules to normalize after inserting the frame variable›

declare mult.assoc[symmetric, frame_var_rewrs]
  Subjection_times[frame_var_rewrs]
  ExBI_times_right[frame_var_rewrs]

consts frame_var_rewrs :: mode

φreasoner_ML Subty_Simplify 2000 (‹Simplify frame_var_rewrs ?x ?y›)
  = ‹Phi_Reasoners.wrap (PLPR_Simplifier.simplifier_only (K Seq.empty) (fn ctxt =>
          Named_Theorems.get ctxt \<^named_theorems>‹frame_var_rewrs›) {fix_vars=false}) o snd›

definition φIntroFrameVar :: "'a::sep_magma BI option ⇒ 'a BI ⇒ 'a BI ⇒ 'a BI ⇒ 'a BI ⇒ bool"
  where "φIntroFrameVar R S' S T' T ⟷ (case R of Some R' ⇒ S' = (S * R') ∧ T' = T * R'
                                                 | None ⇒ S' = S ∧ T' = T )"

definition φIntroFrameVar' ::
  "assn ⇒ assn ⇒ assn ⇒ ('ret ⇒ assn) ⇒ ('ret ⇒ assn) ⇒ ('ex ⇒ assn) ⇒ ('ex ⇒ assn) ⇒ bool"
  where "φIntroFrameVar' R S' S T' T E' E ⟷ S' = (S * R) ∧ T' = (λret. T ret * R) ∧ E' = (λex. E ex * R) "

definition TAIL :: ‹assn ⇒ assn› where ‹TAIL S = S›

text ‹Antecedent \<^schematic_prop>‹φIntroFrameVar ?R ?S' S ?T' T› appends a frame variable
  \<^schematic_term>‹?R› to the source MTF \<^term>‹S› if the items in \<^term>‹S› do not have an ending
  frame variable already nor the ending item is not tagged by ‹TAIL›.
  If so, the reasoner returns ‹?S' := S * ?R› for a schematic ‹?R›,
  or else, the ‹S› is returned unchanged ‹?S' := ?S›.
  ‹φIntroFrameVar'› is similar.

  Tag ‹TAIL› is meaningful only when it tags the last item of a ‹∗›-sequence.
  It has a meaning of `the remaining everything' like, the target (RHS) item tagged by this
  means the item matches the whole remaining part of the source (LHS) part.
  ‹TAIL› also means, the tagged item is at the end and has a sense of ending, so no further
  padding is required (e.g. padding-of-void during NToA reasoning).
›

lemma φIntroFrameVar_No:
  "φIntroFrameVar None S S T T"
  unfolding φIntroFrameVar_def by simp

lemma φIntroFrameVar'_No:
  "φIntroFrameVar' 1 S S T T E E"
  unfolding φIntroFrameVar'_def by simp

lemma φIntroFrameVar_Yes:
  "φIntroFrameVar (Some R) (S 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) S (T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) T"
  unfolding φIntroFrameVar_def REMAINS_def by simp

lemma φIntroFrameVar'_Yes:
  " φIntroFrameVar' R (S 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) S (λret. T ret * R) T (λex. E ex * R) E"
  unfolding φIntroFrameVar'_def REMAINS_def by simp

φreasoner_ML φIntroFrameVar 1000 ("φIntroFrameVar ?R ?S' ?S ?T' ?T") =
‹fn (_, (ctxt, sequent)) =>
  let val (Const (\<^const_name>‹φIntroFrameVar›, \<^Type>‹fun \<^Type>‹option TY› _›) $ _ $ _ $ S $ _ $ _) =
          Thm.major_prem_of sequent |> HOLogic.dest_Trueprop
      val suppressed = not (Sign.of_sort (Proof_Context.theory_of ctxt) (TY, \<^sort>‹sep_magma_1›))
                orelse case S
                         of Const(\<^const_name>‹REMAINS›, _) $ _ $ R =>
                              Term.is_Var (Term.head_of R)
                          | _ => (case Phi_Syntax.rightmost_sep S
                         of (\<^const>‹TAIL› $ _) => true
                          | RR => Term.is_Var (Term.head_of RR))
  in if suppressed
     then Seq.single (ctxt, @{thm φIntroFrameVar_No}  RS sequent)
     else Seq.single (ctxt, @{thm φIntroFrameVar_Yes} RS sequent)
  end›

φreasoner_ML φIntroFrameVar' 1000 ("φIntroFrameVar' ?R ?S' ?S ?T' ?T ?E' ?E") =
‹fn (_, (ctxt, sequent)) =>
  let val (Const (\<^const_name>‹φIntroFrameVar'›, _) $ _ $ _ $ S $ _ $ _ $ _ $ _) =
          Thm.major_prem_of sequent |> HOLogic.dest_Trueprop
      val suppressed = case S
                         of Const(\<^const_name>‹REMAINS›, _) $ _ $ R =>
                              Term.is_Var (Term.head_of R)
                          | _ => (case Phi_Syntax.rightmost_sep S
                         of (\<^const>‹TAIL› $ _) => true
                          | RR => Term.is_Var (Term.head_of RR))
  in if suppressed
     then Seq.single (ctxt, @{thm φIntroFrameVar'_No}  RS sequent)
     else Seq.single (ctxt, @{thm φIntroFrameVar'_Yes} RS sequent)
  end›

hide_fact φIntroFrameVar_No φIntroFrameVar'_No φIntroFrameVar_Yes φIntroFrameVar'_Yes


subsubsection ‹Reasoning Goals Embedded in BI Assertion›

definition Subj_Reasoning :: ‹ 'p BI ⇒ bool ⇒ 'p BI › (infixl "𝗌𝗎𝖻𝗃-𝗋𝖾𝖺𝗌𝗈𝗇𝗂𝗇𝗀" 15)
  where ‹Subj_Reasoning ≡ Subjection›

lemma [φreason 1000]:
  ‹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P
⟹ A
⟹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗌𝗎𝖻𝗃-𝗋𝖾𝖺𝗌𝗈𝗇𝗂𝗇𝗀 A 𝗐𝗂𝗍𝗁 P›
  unfolding Subj_Reasoning_def Transformation_def
  by simp

subsection ‹Embed BI Assertion into φ-Type›

lemma φType_conv_eq_1:
  ‹T = U ⟹ (x ⦂ T) = U x›
  unfolding φType_def by simp

lemma φType_conv_eq_2:
  ‹T = U ⟹ (x ⦂ T) = (x ⦂ U)›
  unfolding φType_def by simp

ML_file ‹library/phi_type_algebra/helps.ML›
ML_file ‹library/tools/embed_BI_into_phi_types.ML›

consts mode_embed_into_φtype :: mode

φreasoner_ML Simp_Premise 10 (‹𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[mode_embed_into_φtype] _ : _›)
  = ‹Phi_Reasoners.wrap (PLPR_Simplifier.simplifier (K Seq.empty)
                        (fn ctxt => Embed_into_Phi_Type.equip ctxt) {fix_vars=true}) o snd›

 
lemmas [embed_into_φtype] =
    φNone_itself_is_one[where any=‹()›] φProd_expn' φAny_def

ML ‹Embed_into_Phi_Type.print \<^context> true›

paragraph ‹Debug Usage›

method_setup embed_into_φtype = ‹
let val no_asmN = "no_asm";
    val no_asm_useN = "no_asm_use";
    val no_asm_simpN = "no_asm_simp";
    val asm_lrN = "asm_lr";

    fun conv_mode x =
      ((Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
        Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
        Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
        Scan.succeed asm_full_simp_tac) |> Scan.lift) x;
in conv_mode >> (fn simp => fn ctxt =>
      Method.METHOD (fn ths => Method.insert_tac ctxt ths 1 THEN simp
          (Phi_Conv.Embed_into_Phi_Type.equip ctxt) 1 ))
end›


subsection ‹Semantic Type of Multiple Values›

lemma [φreason 1200 for ‹Semantic_Types_i (λvs. ?x ⦂ 𝗏𝖺𝗅[φV_fst vs] ?T❟ ?R vs) _›]:
  ‹ Semantic_Type T TY
⟹ Semantic_Types_i (λvs. R vs) TYs
⟹ Semantic_Types_i (λvs. x ⦂ 𝗏𝖺𝗅[φV_fst vs] T❟ R (φV_snd vs)) (TY#TYs)›
  unfolding Semantic_Types_i_def Semantic_Types_def
            Well_Typed_Vals_def φarg_forall Semantic_Type_def subset_iff
  by (clarsimp simp add: to_vals_prod_def to_vals_VAL_def Val_inh_rewr)

lemma [φreason 1200]:
  ‹ Semantic_Type T TY
⟹ Semantic_Types_i (λvs. x ⦂ 𝗏𝖺𝗅[vs] T❟ R) [TY]›
  unfolding Semantic_Types_i_def Semantic_Types_def
            Well_Typed_Vals_def φarg_forall Semantic_Type_def subset_iff
  by (clarsimp simp add: to_vals_prod_def to_vals_VAL_def Val_inh_rewr)

lemma [φreason 1200]:
  ‹ Semantic_Types_i R TYs
⟹ Semantic_Types_i (λvs. S❟ R vs) TYs›
  unfolding Semantic_Types_i_def Semantic_Types_def Well_Typed_Vals_def by clarsimp

lemma [φreason 2000]:
  ‹ Semantic_Types_i (λ_::unit φarg. Void) []›
  unfolding Semantic_Types_i_def Semantic_Types_def Well_Typed_Vals_def to_vals_unit_def by clarsimp

lemma [φreason 1020 except ‹Semantic_Types_i (λvs. ?A vs❟ ?B vs) _›]:
  ‹ Semantic_Types_i (λvs. R vs❟ Void) TYs
⟹ Semantic_Types_i R TYs›
  unfolding Semantic_Types_i_def Well_Typed_Vals_def by clarsimp

lemma [φreason 1000]:
  ‹ FAIL TEXT(‹Fail to infer the semantic type of› R)
⟹ Semantic_Types_i R TYs›
  unfolding Semantic_Types_i_def Well_Typed_Vals_def FAIL_def by clarsimp

lemma [φreason 1200]:
  ‹ Semantic_Types_i (λret. (exp ret) (v ret)) TYs
⟹ Semantic_Types_i (λret. Let (v ret) (exp ret)) TYs›
  unfolding Let_def .

lemma [φreason 1200]:
  ‹ Semantic_Types_i (λret. f ret (fst (x ret)) (snd (x ret))) TYs
⟹ Semantic_Types_i (λret. case_prod (f ret) (x ret)) TYs›
  by (simp add: case_prod_beta')

lemma [φreason 1200]:
  ‹(⋀x. Semantic_Types_i (λret. (S ret) x) TYs)
⟹ Semantic_Types_i (λret. ExBI (S ret)) TYs›
  unfolding Semantic_Types_i_def Semantic_Types_def Well_Typed_Vals_def Satisfiable_def ExBI_expn
  by clarsimp blast

lemma [φreason 1200]:
  ‹(⋀x. Semantic_Types_i (λret. S ret) TYs)
⟹ Semantic_Types_i (λret. S ret 𝗌𝗎𝖻𝗃 P ret) TYs›
  unfolding Semantic_Types_i_def Semantic_Types_def Well_Typed_Vals_def Satisfiable_def Subjection_expn
  by clarsimp


subsection ‹Removing Values› (*TODO: depreciate me*)

definition ‹Remove_Values (Input::assn) (Output::assn) ⟷ (Input 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Output)›

text ‹The process \<^prop>‹Remove_Values Input Output› removes value assertions ‹x ⦂ 𝗏𝖺𝗅 T›
  from the assertion ‹Input›. Bounded values such the return value of a procedure are not removed.›

text ‹Given an assertion X, antecedent \<^term>‹Remove_Values X X'›
  returns X' where all free value assertions \<^term>‹x ⦂ Val raw T› filtered out, where \<^term>‹raw›
  contains at least one free variable of \<^typ>‹'a φarg›.

  It is typically used in exception. When a computation triggers an exception at state X,
    the state recorded in the exception is exactly X' where value assertions are filtered out.›

declare [[φreason_default_pattern ‹Remove_Values ?X _› ⇒ ‹Remove_Values ?X _› (100)]]

(* lemma [φreason for ‹Remove_Values ?ex ?var_X ?Z›]:
  ‹Remove_Values ex X X›
  unfolding Remove_Values_def using transformation_refl . *)

lemma [φreason 1200]:
  ‹(⋀c. Remove_Values (T c) (T' c))
⟹ Remove_Values (ExBI T) (ExBI T')›
  unfolding Remove_Values_def Transformation_def
  by simp blast

lemma [φreason 1200]:
  ‹(⋀c. Remove_Values (T c * R) (T' c * R'))
⟹ Remove_Values (ExBI T * R) (ExBI T' * R')›
  unfolding Remove_Values_def Transformation_def
  by simp blast

lemma [φreason 1200]:
  ‹ Remove_Values T T'
⟹ Remove_Values (T 𝗌𝗎𝖻𝗃 P) (T' 𝗌𝗎𝖻𝗃 P)›
  unfolding Remove_Values_def Transformation_def
  by simp

lemma [φreason 1200]:
  ‹ Remove_Values (T * R) (T' * R')
⟹ Remove_Values ((T 𝗌𝗎𝖻𝗃 P) * R) ((T' 𝗌𝗎𝖻𝗃 P) * R')›
  unfolding Remove_Values_def Transformation_def
  by simp

lemma [φreason 1200]:
  ‹ Remove_Values A A'
⟹ Remove_Values B B'
⟹ Remove_Values (A 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 B) (A' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 B')›
  unfolding REMAINS_def Remove_Values_def Transformation_def REMAINS_def
  by (simp; blast)

lemma [φreason 1200]:
  ‹ Remove_Values A A'
⟹ Remove_Values B B'
⟹ Remove_Values (A + B) (A' + B')›
  unfolding Remove_Values_def Transformation_def
  by blast

lemma [φreason 1200]:
  ‹ Remove_Values R R'
⟹ Remove_Values ((x ⦂ Val raw T) * R) R'›
  unfolding Remove_Values_def Transformation_def by (simp add: Val_expn)

lemma [φreason 1200]:
  ‹Remove_Values (x ⦂ Val raw T) 1›
  unfolding Remove_Values_def Transformation_def by (simp add: Val_expn)

lemma [φreason 1200]:
  ‹ Remove_Values A A'
⟹ Remove_Values (1 * A) A'›
  unfolding Remove_Values_def Transformation_def by simp

lemma [φreason 1200]:
  ‹ Remove_Values A A'
⟹ Remove_Values (A * 1) A'›
  unfolding Remove_Values_def Transformation_def by simp

lemma [φreason 1200]:
  ‹Remove_Values (0 * A) 0›
  unfolding Remove_Values_def Transformation_def by simp

lemma [φreason 1100]:
  ‹ Remove_Values A A'
⟹ Remove_Values B B'
⟹ Remove_Values (A * B) (A' * B')›
  unfolding Remove_Values_def Transformation_def by simp blast

lemma [φreason 1000]:
  ‹ Remove_Values A A›
  unfolding Remove_Values_def
  by simp



section ‹Declaration of Reasonig Process›

subsection ‹Declaration of Convergence of Branch›

consts invoke_br_join :: ‹action› (*TODO: move?*)


end