Theory IDE_CP_App2

(*IDE_CP_P: Programming Module*)
theory IDE_CP_App2
  imports Phi_Types
begin

section ‹Derivers for IDE-CP›

subsection ‹Properties of Semantic Value›


subsubsection ‹Semantic Type›

context begin

private lemma φTA_SemTy_rule:
  ‹ 𝗋EIF Ant Ant'
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 Ant' ⟹ Abstract_Domain T D)
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 Ant' ⟹ Abstract_Domain⇩L T D⇩L)
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (Ant' ⟶ TY = (if Ex D then TY' else 𝗉𝗈𝗂𝗌𝗈𝗇) ∧ D⇩L = D)
⟹ (⋀x. Ant ⟶ Semantic_Type' (x ⦂ T) TY' @tag φTA_subgoal undefined)
⟹ 𝗋Success
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ Ant @tag φTA_ANT
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY ›
  unfolding Action_Tag_def Premise_def Abstract_Domain_def 𝗋EIF_def Abstract_Domain⇩L_def 𝗋ESC_def
            SType_Of_def Inhabited_def Semantic_Type'_def Semantic_Type_def
  by (auto,
      smt (z3) Action_Tag_def Premise_True Satisfiable_def φSemType_Itself_brute exE_some,
      meson)

(*
private lemma φTA_SemTy_rule:
  ‹ (⋀x. Ant ⟶ 𝗍𝗒𝗉𝖾𝗈𝖿 (x ⦂ T) = TY @tag φTA_subgoal 𝒜infer)
⟹ 𝗋Success
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ Ant @tag φTA_ANT
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY ›
  unfolding Action_Tag_def Premise_def
  by (rule SType_Of'_implies_SType_Of, clarsimp)
*)

private lemma φTA_SemTy_IH_rewr:
  ‹ Trueprop (Ant ⟶ PPP @tag φTA_subgoal undefined) ≡
    (Ant @tag φTA_ANT ⟹ PPP ) ›
  unfolding Action_Tag_def atomize_imp Premise_def
  ..

private lemma φTA_SemTy_cong:
  ‹ TY ≡ TY'
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY ≡ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY' ›
  for T :: ‹(VAL,'x) φ›
  by simp


ML_file ‹library/phi_type_algebra/semantic_type.ML›

end

φproperty_deriver Semantic_Type 120 for (‹SType_Of _ = _›)
    = ‹ Phi_Type_Derivers.semantic_type › 

ML_file ‹library/additions/infer_semantic_type_prem.ML›


(*
subsubsection ‹Semantic Type Rewrites›

context begin

private lemma styp_of_derv_rule':
  ‹ Abstract_Domain⇩L T D⇩L
⟹ Abstract_Domain T D
⟹ Semantic_Type T TY
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 ((∃x. D⇩L x) = (∃x. D x) ∧
            ((∃x. D x) ⟶ TY' = TY) ∧
            ((∀x. ¬ D x) ⟶ TY' = 𝗉𝗈𝗂𝗌𝗈𝗇))
⟹ SType_Of T = TY' ›
  unfolding Abstract_Domain⇩L_def Abstract_Domain_def 𝗋ESC_def 𝗋EIF_def
            Premise_def SType_Of_def Inhabited_def 
  by (auto, metis Satisfiable_def Semantic_Type_def Well_Type_unique some_equality,
            simp add: Satisfiable_def Semantic_Type_def)

private lemma styp_of_derv_rule:
  ‹ (Ant @tag φTA_ANT ⟹ SType_Of T = TY')
⟹ 𝗋Success
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ Ant @tag φTA_ANT
⟹ SType_Of T = TY' › .

ML_file ‹library/phi_type_algebra/SType_Of.ML›

end

φproperty_deriver SType_Of 150 for (‹SType_Of _ = _›)
    = ‹ Phi_Type_Derivers.STyp_Of › 
*)


subsubsection ‹Semantic Zero Value›

context begin

private lemma φTA_Semantic_Zero_Val_rule:
  ‹ (Ant ⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇 ⟶ Zero TY ≠ None ∧ (∀v. Zero TY = Some v ⟶ v ⊨ (z ⦂ T))))
⟹ 𝗋Success
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ Ant @tag φTA_ANT
⟹ Semantic_Zero_Val TY T z ›
  unfolding Semantic_Zero_Val_def Premise_def Action_Tag_def
  by clarsimp

ML_file ‹library/phi_type_algebra/semantic_zero_val.ML›

end

φproperty_deriver Semantic_Zero_Val 130 for (‹Semantic_Zero_Val _ _ _›)
  requires Semantic_Type
    = ‹ Phi_Type_Derivers.semantic_zero_val › 


declare [[φparameter_default_equality ‹TY› ⇒ obligation (100)]]


subsection ‹‹φApp_Conv›› ― ‹used only when the given ToA is not in the target space›

lemma [φreason_template default %φapp_conv_derived+10]:
  ‹ Functional_Transformation_Functor Fa Fb T U (λx. {D x}) R pm fm
⟹ NO_LAMBDA_CONVERTIBLE TYPE('c⇩a × 'x⇩a) TYPE('c × 'x) @tag 𝒜_template_reason None
⟹ 𝗀𝗎𝖺𝗋𝖽 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 D x = a ∧ b ∈ R x
⟹ NO_SIMP (ToA_App_Conv TYPE('c⇩a⇩a) TYPE('c⇩a) T ToA (a ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 b ⦂ U 𝗐𝗂𝗍𝗁 P))
⟹ ToA_App_Conv TYPE('c⇩a⇩a) TYPE('c) (Fa T) ToA (x ⦂ Fa T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 fm (λ_. b) (λ_. P) x ⦂ Fb U 𝗐𝗂𝗍𝗁 pm (λ_. b) (λ_. P) x) ›
  for Fa :: ‹('c⇩a,'x⇩a) φ ⇒ ('c,'x) φ›
  unfolding ToA_App_Conv_def 𝗋Guard_def Premise_def Functional_Transformation_Functor_def NO_SIMP_def
  by clarsimp

(* TODO: planned
lemma [φreason_template default %φapp_conv_derived]:
  ‹ Functional_Transformation_Functor Fa Fb T U D R pm fm
⟹ NO_MATCH (λx. {D'' x}) D @tag 𝒜_template_reason
⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒 D' : (∀a ∈ D x. Q a) @tag 𝒜_template_reason
⟹ NO_SIMP (φApp_Conv ToA (∀a. Q a ⟶ (a ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 f a ⦂ U 𝗐𝗂𝗍𝗁 P a)))
⟹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 (∀a ∈ D x. f a ∈ R x)
⟹ φApp_Conv ToA (D' ⟶ (x ⦂ Fa T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 fm f P x ⦂ Fb U 𝗐𝗂𝗍𝗁 pm f P x)) ›
  unfolding Functional_Transformation_Functor_def φApp_Conv_def 𝗋Guard_def Premise_def
            Action_Tag_def Simplify_def NO_SIMP_def
  by clarsimp
*)


section ‹Value \& Reasoning over it›

subsection ‹φ-Type Abstraction›

local_setup ‹
  Phi_Type.add_type {no_auto=true}
        (\<^binding>‹Val›, \<^pattern>‹Val::VAL φarg ⇒ (VAL, ?'a) φ ⇒ (?'x::one, ?'a) φ›,
         Phi_Type.DIRECT_DEF (Thm.transfer \<^theory> @{thm' Val_def}),
         ⌂, Phi_Type.Derivings.empty, [], NONE)
   #> snd ›

local_setup ‹
  Phi_Type.add_type {no_auto=true}
        (\<^binding>‹Vals›, \<^pattern>‹Vals::VAL list φarg ⇒ (VAL list, ?'a) φ ⇒ (?'x::one, ?'a) φ›,
         Phi_Type.DIRECT_DEF (Thm.transfer \<^theory> @{thm' Vals_def}),
         ⌂, Phi_Type.Derivings.empty, [], NONE)
   #> snd ›

let_φtype Val
  deriving ‹Abstract_Domain T P
        ⟹ Abstract_Domain (𝗏𝖺𝗅[v] T) P›
       and ‹Abstract_Domain⇩L (𝗏𝖺𝗅[v] T) (λx. φarg.dest v ⊨ (x ⦂ T))›
       and ‹Object_Equiv T eq
        ⟹ Object_Equiv (𝗏𝖺𝗅[v] T) eq›
       and Basic
       and ‹Identity_Elements⇩I (𝗏𝖺𝗅[v] T) (λx. True) (λx. True)›
       and ‹ ERROR TEXT(‹Insuffieicnt arguments or local values›)
         ⟹ Identity_Elements⇩E (𝗏𝖺𝗅[v] T) (λx. False)›
       and Functional_Transformation_Functor


subsubsection ‹Application Methods for Transformations›

(*TODO: I really don't like this. It is not generic.
It should be some generic structural morphism.*)

lemma [φreason 2100 for ‹
  PROP φApplication (Trueprop (?x ⦂ ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P))
          (Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?x ⦂ Val ?raw ?T❟ ?R)) ?Result
› except ‹
  PROP φApplication (Trueprop (?x ⦂ Val ?raw ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P))
          (Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?R)) ?Result
›]:
  ‹ PROP φApplication (Trueprop (x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ U 𝗐𝗂𝗍𝗁 P))
      (Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 x ⦂ Val raw T❟ R))
      (𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 y ⦂ Val raw U❟ R) ∧ P)›
  unfolding φApplication_def Premise_def
  by (simp, smt (verit, del_insts) CurrentConstruction_def INTERP_SPEC_subj Satisfaction_def
                                   Subjection_expn Subjection_times(1) Transformation_def Val.unfold)


lemma [φreason 2000 for ‹
  PROP φApplication (Trueprop (?x' ⦂ ?T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P))
      (Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?x ⦂ Val ?raw ?T❟ ?R)) ?Result
› except ‹
  PROP φApplication (Trueprop (?x ⦂ Val ?raw ?T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?y ⦂ ?U 𝗐𝗂𝗍𝗁 ?P))
          (Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 ?blk [?RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 ?R)) ?Result
›]:
  ‹ SUBGOAL TOP_GOAL G
⟹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x' ⦂ T' 𝗐𝗂𝗍𝗁 Any
⟹ SOLVE_SUBGOAL G
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ PROP φApplication (Trueprop (x' ⦂ T' 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ U 𝗐𝗂𝗍𝗁 P))
      (Trueprop (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 x ⦂ Val raw T❟ R))
      (𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True ⟹ (𝖼𝗎𝗋𝗋𝖾𝗇𝗍 blk [RR] 𝗋𝖾𝗌𝗎𝗅𝗍𝗌 𝗂𝗇 y ⦂ Val raw U❟ R) ∧ P)›
  unfolding φApplication_def Action_Tag_def Premise_def
  by (simp, smt (z3) Action_Tag_E Action_Tag_I Premise_True
                     Val.functional_transformation φapply_implication 𝗋Guard_I transformation_right_frame)


subsubsection ‹Synthesis›

lemma [φreason %φsynthesis_parse for
  ‹Synthesis_Parse (?x ⦂ (?T::?'a ⇒ VAL BI)) (?X::?'ret ⇒ assn)›
]:
  ‹Synthesis_Parse (x ⦂ T) (λv. x ⦂ Val v T)›
  unfolding Synthesis_Parse_def ..

lemma [φreason %φsynthesis_parse for
  ‹Synthesis_Parse (MAKE _ (?T::?'a ⇒ VAL BI)) (?X::?'ret ⇒ assn)›
]:
  ‹Synthesis_Parse (MAKE n T) (λv. x ⦂ MAKE n (Val v T))›
  unfolding Synthesis_Parse_def ..

lemma [φreason %φsynthesis_parse for
  ‹Synthesis_Parse (?raw::?'a φarg) (?X::?'ret ⇒ assn)›
]:
  ‹Synthesis_Parse raw (λ_. x ⦂ Val raw T)›
  unfolding Synthesis_Parse_def ..

subsubsection ‹Special Parsing of Annotations›

lemma [φreason %To_ToA_fallback]:
  ‹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ U 𝗌𝗎𝖻𝗃 y. r y @tag to U'
⟹ x ⦂ 𝗏𝖺𝗅[v] T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ 𝗏𝖺𝗅[v] U 𝗌𝗎𝖻𝗃 y. r y @tag to U' ›
  unfolding Action_Tag_def Transformation_def
  by clarsimp


subsubsection ‹Short-cut of ToA›

text ‹We can assume the name bindings of values are lambda-equivalent. ›

φreasoner_group Val_ToA = (1100, [1100, 1120]) in ToA_cut
  ‹Short-cut transformations about values›

declare [[φtrace_reasoning = 1]]

lemma [φreason %Val_ToA+20 for ‹_ ⦂ 𝗏𝖺𝗅[_] _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ 𝗏𝖺𝗅[_] _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›]:
  "x ⦂ 𝗏𝖺𝗅[v] T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Void @tag 𝒯𝒫"
  unfolding REMAINS_def Transformation_def Action_Tag_def
  by simp

lemma [φreason %Val_ToA+10 for ‹_ ⦂ 𝗏𝖺𝗅[_] _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ 𝗏𝖺𝗅[_] _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›]:
  " y ⦂ U 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ T 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ y ⦂ 𝗏𝖺𝗅[v] U 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Void 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫"
  unfolding Transformation_def Action_Tag_def
  by (simp add: times_list_def)



lemma [φreason %Val_ToA+20 for ‹_ ⦂ 𝗏𝖺𝗅[_] _ ❟ _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ 𝗏𝖺𝗅[_] _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›]:
  "x ⦂ 𝗏𝖺𝗅[v] T❟ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R @tag 𝒯𝒫"
  unfolding REMAINS_def Transformation_def Action_Tag_def
  by simp

lemma [φreason %Val_ToA+10 for ‹_ ⦂ 𝗏𝖺𝗅[_] _ ❟ _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ 𝗏𝖺𝗅[_] _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›]:
  " y ⦂ U 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ T 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ y ⦂ 𝗏𝖺𝗅[v] U❟ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫"
  unfolding Transformation_def Action_Tag_def
  by (simp add: times_list_def) metis

lemma [φreason %Val_ToA for ‹_❟ _ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 _ ⦂ 𝗏𝖺𝗅[_] _ 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›]:
  " R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R' 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ X❟ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 X❟ R' 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫"
  unfolding REMAINS_def split_paired_All Action_Tag_def
  by (simp add: mult.left_commute transformation_left_frame)

lemma [φreason %Val_ToA except ‹_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x ⦂ 𝗏𝖺𝗅[?v] ?V 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›
    if ‹fn (_, sequent) =>
          case #2 (Phi_Syntax.dest_transformation (
                  Logic.strip_assums_concl (Phi_Help.leading_antecedent' sequent)))
            of Const(\<^const_name>‹REMAINS›, _) $ X $ _ =>
                  not (Phi_Syntax.is_BI_connective X)
       › ]:
  " R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R' 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫
⟹ x ⦂ 𝗏𝖺𝗅[v] V❟ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 x ⦂ 𝗏𝖺𝗅[v] V❟ R' 𝗐𝗂𝗍𝗁 P @tag 𝒯𝒫"
  unfolding REMAINS_def Action_Tag_def
  by (metis (no_types, opaque_lifting) transformation_right_frame mult.assoc mult.commute)




subsection ‹Access of Local Values›

typedecl valname ― ‹Binding of local values used in user programming interface, only used syntactically›

subsubsection ‹Conventions›

φreasoner_group ToA_access_to_local_value = (1000, [1000,1100]) in ToA_cut
    ‹Access local values via ToA›
  and synthesis_access_to_local_value = (1000, [1000, 1100]) in φsynthesis_cut
    ‹Access local values via Synthesis›

  and local_value = (1000, [1000, 1000])
                    for ‹φarg.dest (v <val-of> (name::valname) <path> []) ⊨ (x ⦂ T)›
    ‹specification facts of local values›


subsubsection ‹Read›

(*
lemma [φreason 1200 for ‹?S1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?S2❟ SYNTHESIS ?x ⦂ Val ?raw ?T›]:
  ‹ φarg.dest raw ∈ (x ⦂ T)
⟹ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 R❟ SYNTHESIS x ⦂ 𝗏𝖺𝗅[raw] T›
  unfolding Action_Tag_def
  by (cases raw; simp add: Val_expn transformation_refl) *)

lemma [φreason %ToA_access_to_local_value
           for ‹_ 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x <val-of> (?raw::VAL φarg) <path> ?path ⦂ ?T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫›]:
  ‹ φarg.dest raw ⊨ (x ⦂ T)
⟹ report_unprocessed_element_index path ℰℐℋ𝒪𝒪𝒦_none
⟹ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x <val-of> raw <path> path ⦂ 𝗏𝖺𝗅[raw] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R @tag 𝒯𝒫›
  for R :: ‹'c::sep_magma_1 BI›
  unfolding Action_Tag_def REMAINS_def
  by (cases raw; simp add: Val.unfold)

lemma [φreason %ToA_access_to_local_value for
    ‹𝗉𝗋𝗈𝖼 ?GG ⦃ ?R ⟼ λret. ?x <val-of> (?raw::VAL φarg) <path> ?path ⦂ ?T ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag synthesis›
]:
  ‹ φarg.dest raw ⊨ (x ⦂ T)
⟹ report_unprocessed_element_index path ℰℐℋ𝒪𝒪𝒦_none
⟹ 𝗉𝗋𝗈𝖼 Return raw ⦃ R ⟼ λret. x <val-of> raw <path> path ⦂ 𝗏𝖺𝗅[ret] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ @tag synthesis›
  unfolding Action_Tag_def REMAINS_def
  by (cases raw; simp add: φM_Success)

lemma φarg_val_varify_type:
  ‹ φarg.dest raw ⊨ (x  ⦂ T)
⟹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x' ⦂ T' 𝗐𝗂𝗍𝗁 Any @tag 𝒯𝒫
||| FAIL TEXT(‹Expect the value› raw ‹has spec› (x' ⦂ T') ‹but is specified by›
      (x ⦂ T) ‹actually, and the conversion fails.›)
⟹ φarg.dest raw ⊨ (x' ⦂ T')›
  unfolding Transformation_def atomize_Branch FAIL_def Action_Tag_def
  by blast

lemma [φreason %ToA_access_to_local_value for
    ‹?S1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x <set-to> (?raw::VAL φarg) <path> _ ⦂ ?T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?S2 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 ›
]:
  ‹ ERROR TEXT(‹Local value is immutable. Cannot assign to› raw)
⟹ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x <set-to> (raw::VAL φarg) <path> any ⦂ T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R @tag 𝒯𝒫›
  unfolding ERROR_def
  by blast

lemma [OF φarg_val_varify_type,
       φreason %φant_by_synthesis for ‹PROP Synthesis_by (?raw::VAL φarg) (Trueprop (𝗉𝗋𝗈𝖼 ?f ⦃ ?R1 ⟼ λret. ?x ⦂ Val ret ?T❟ ?R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E ))›]:
  ‹ φarg.dest raw ⊨ (x ⦂ T)
⟹ PROP Synthesis_by raw (Trueprop (𝗉𝗋𝗈𝖼 Return raw ⦃ R ⟼ λret. x ⦂ Val ret T❟ R ⦄))›
  unfolding Synthesis_by_def Action_Tag_def φProcedure_def Return_def det_lift_def
  by (cases raw; simp add: Val.unfold less_eq_BI_iff)


subsubsection ‹Assignment›

lemma [OF φarg_val_varify_type,
       φreason %ToA_access_to_local_value for ‹?S1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 ?x <val-of> (?name::valname) <path> ?path ⦂ ?T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?S2 𝗐𝗂𝗍𝗁 _ @tag 𝒯𝒫 ›]:
  ‹ φarg.dest (raw <val-of> (name::valname) <path> []) ⊨ (x ⦂ T)
⟹ report_unprocessed_element_index path ℰℐℋ𝒪𝒪𝒦_none
⟹ R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x <val-of> name <path> path ⦂ 𝗏𝖺𝗅[raw] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R @tag 𝒯𝒫 ›
  for R :: ‹'c::sep_magma_1 BI›
  unfolding Action_Tag_def REMAINS_def
  by (cases raw; simp add: Val.unfold)

lemma [OF φarg_val_varify_type,
       φreason %synthesis_access_to_local_value for
    ‹𝗉𝗋𝗈𝖼 ?GG ⦃ ?R ⟼ λret. ?x <val-of> (?name::valname) <path> ?path ⦂ ?T ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag synthesis›
]:
  ‹ φarg.dest (raw <val-of> (name::valname) <path> []) ⊨ (x ⦂ T)
⟹ report_unprocessed_element_index path ℰℐℋ𝒪𝒪𝒦_none
⟹ 𝗉𝗋𝗈𝖼 Return raw ⦃ R ⟼ λret. x <val-of> name <path> path ⦂ 𝗏𝖺𝗅[ret] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ @tag synthesis›
  unfolding Action_Tag_def REMAINS_def
  by (cases raw; simp add: φM_Success)




lemma "__set_value_rule__":
  ‹ (φarg.dest (v <val-of> (name::valname) <path> []) ⊨ (x ⦂ T) ⟹ 𝗉𝗋𝗈𝖼 F ⦃ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E )
⟹ 𝗉𝗋𝗈𝖼 F ⦃ x ⦂ 𝗏𝖺𝗅[v] T❟ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ R' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
  unfolding φProcedure_def Value_of_def REMAINS_def
  by (clarsimp simp add: Val.unfold INTERP_SPEC_subj less_eq_BI_iff)

lemma "__fast_assign_val__":
  ‹ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 R' 𝗐𝗂𝗍𝗁 P
⟹ x ⦂ 𝗏𝖺𝗅[v] T❟ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 R' 𝗐𝗂𝗍𝗁 φarg.dest (v <val-of> (name::valname) <path> []) ⊨ (x ⦂ T) ∧ P›
  unfolding Transformation_def
  by (clarsimp simp add: Val.unfold; blast)

lemma "__fast_assign_val_0__":
  ‹ Void 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 R ›
  unfolding REMAINS_def
  by simp

ML_file ‹library/additions/local_value.ML›


(*subsection ‹Deep Representation of Values›

abbreviation Vals :: ‹(VAL, 'a) φ ⇒ (VAL list, 'a) φ› ("𝗏𝖺𝗅❙s _" [51] 50)
  where ‹Vals ≡ List_Item›

translations "(CONST Vals T) ∗ (CONST Vals U)" == "XCONST Vals (T ∗ U)"*)

subsection ‹MAKE Abstraction for Values›

lemma [φreason %φsynthesis_cut for ‹𝗉𝗋𝗈𝖼 _ ⦃ _ ⟼ λret. ?y ⦂ MAKE ?n (𝗏𝖺𝗅[ret] ?U) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 ?E @tag synthesis›]:
  ‹ X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗅[v] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R
⟹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ MAKE n U 𝗐𝗂𝗍𝗁 any
⟹ 𝗉𝗋𝗈𝖼 Return v ⦃ X ⟼ λret. y ⦂ MAKE n (𝗏𝖺𝗅[ret] U) 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ @tag synthesis›
  unfolding MAKE_def
  ❴ premises X[] and T[]
    X T
  ❵ .

subsection ‹Programming Methods for Showing Properties of Values›

subsubsection ‹Semantic Type›
(*
lemma [φreason %φprogramming_method]:
  ‹ PROP φProgramming_Method (⋀x. x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 A x) M D R F
⟹ Friendly_Help TEXT(‹Hi! You are trying to show the value abstraction› S ‹has semantic type› TY
      ‹Now you entered the programming mode and you need to transform the specification to›
      ‹some representation of φ-types whose semantic type is know so that we can verify your claim.›)
⟹ PROP φProgramming_Method (Trueprop (𝗍𝗒𝗉𝖾𝗈𝖿 T = TY)) M D
                             ((⋀x. 𝗍𝗒𝗉𝖾𝗈𝖿 (A x) = TY @tag 𝒜infer) &&& PROP R) F›
  unfolding φProgramming_Method_def ToA_Construction_def Transformation_def Action_Tag_def
 
  apply (simp add: subset_iff conjunction_imp, rule SType_Of'_implies_SType_Of)
  subgoal premises prems for xx
    thm prems(1)[OF ‹PROP D› ‹PROP R› ‹PROP F›, of xx]
    apply (insert prems(3)[of xx] prems(1)[OF ‹PROP D› ‹PROP R› ‹PROP F›, of xx])
    by (insert prems(3) prems(1)[OF ‹PROP D› ‹PROP R› ‹PROP F›], blast) .
*)

subsubsection ‹Zero Value›

consts working_mode_Semantic_Zero_Val :: working_mode

lemma φdeduce_zero_value:
  ‹ Semantic_Type' (x ⦂ T) TY
⟹ 𝗉𝖺𝗋𝖺𝗆 (y ⦂ U)
⟹ Semantic_Zero_Val TY U y
⟹ y ⦂ U 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ T 𝗐𝗂𝗍𝗁 Any
⟹ 𝗈𝖻𝗅𝗂𝗀𝖺𝗍𝗂𝗈𝗇 True
⟹ Semantic_Zero_Val TY T x›
  unfolding ToA_Construction_def Semantic_Zero_Val_def image_iff Satisfiable_def Transformation_def
  by clarsimp

lemma [φreason %φprogramming_method]:
  ‹ PROP φProgramming_Method (Trueprop (Semantic_Zero_Val TY T x)) working_mode_Semantic_Zero_Val
                             (Trueprop (Semantic_Zero_Val TY T x))
                             (Trueprop True)
                             (Trueprop True)›
  unfolding φProgramming_Method_def .


subsubsection ‹Equality›

lemma [φreason %φprogramming_method]:
  ‹ PROP φProgramming_Method
          (⋀x y vx vy. 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 ceq x y
              ⟹ x ⦂ 𝗏𝖺𝗅[vx] T ❟ y ⦂ 𝗏𝖺𝗅[vy] T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x' ⦂ 𝗏𝖺𝗅[vx] U ❟ y' ⦂ 𝗏𝖺𝗅[vy] U
                  𝗌𝗎𝖻𝗃-𝗋𝖾𝖺𝗌𝗈𝗇𝗂𝗇𝗀 φEqual U ceq' eq'
                  𝗌𝗎𝖻𝗃 U x' y'. ceq' x' y' ∧ eq x y = eq' x' y')
          M D R F
⟹ Friendly_Help
    TEXT(‹Hi! Transform the specification to some representation of φ-types whose› φEqual
         ‹property is known so that we can generate proof obligations for your claim.›)
⟹ PROP φProgramming_Method (Trueprop (φEqual T ceq eq)) M D R F›
  (is ‹PROP φProgramming_Method (PROP ?IMP) _ _ _ _ ⟹ PROP _›
   is ‹PROP ?PPP ⟹ PROP _›)
  unfolding φProgramming_Method_def conjunction_imp
proof -
  have rule: ‹PROP ?IMP ⟹ φEqual T ceq eq›
  unfolding φEqual_def Premise_def Transformation_def Subj_Reasoning_def
  by (clarsimp simp add: φarg_All, blast)

  assume D: ‹PROP D›
    and  R: ‹PROP R›
    and  F: ‹PROP F›
    and PP: ‹PROP D ⟹ PROP R ⟹ PROP F ⟹ PROP ?IMP›
  show ‹φEqual T ceq eq›
    using PP[OF D R F, THEN rule] .
qed

subsubsection ‹Finale›

ML_file ‹library/additions/value_properties.ML›

hide_fact φdeduce_zero_value


(*
TODO: fix this feature
subsubsection ‹Auto unfolding for value list›

lemma [φprogramming_simps]:
  ‹(∃*x. x ⦂ Val rawv Empty_List) = (1 𝗌𝗎𝖻𝗃 USELESS (rawv = φV_nil))›
  unfolding set_eq_iff USELESS_def
  by (cases rawv; simp add: φexpns)

lemma [φprogramming_simps]:
  ‹(∃*x. x ⦂ Val rawv (List_Item T))
 = (∃*x. x ⦂ Val (φV_hd rawv) T 𝗌𝗎𝖻𝗃 USELESS (∃v. rawv = φV_cons v φV_nil))›
  unfolding set_eq_iff φV_cons_def USELESS_def
  apply (cases rawv; clarsimp simp add: φexpns φV_tl_def φV_hd_def times_list_def; rule;
          clarsimp simp add: φarg_All φarg_exists)
  by blast+

lemma [simp]:
  ‹ [] ∉ (∃*x. x ⦂ L)
⟹ ((∃*x. x ⦂ Val rawv (List_Item T ∗ L)) :: 'a::sep_algebra set)
  = ((∃*x. x ⦂ Val (φV_tl rawv) L) * (∃*x. x ⦂ Val (φV_hd rawv) T))›
  unfolding set_eq_iff
  apply (cases rawv; clarsimp simp add: φexpns φV_tl_def φV_hd_def times_list_def)
  by (metis (no_types, opaque_lifting) append_Cons append_Nil list.exhaust_sel
            list.sel(1) list.sel(2) list.sel(3))

lemma [simp]:
  ‹[] ∉ (∃*x. x ⦂ (List_Item T ∗ L))›
  by (rule; clarsimp simp add: φexpns times_list_def)

lemma [simp]:
  ‹[] ∉ (∃*x. x ⦂ List_Item T)›
  by (rule; clarsimp simp add: φexpns times_list_def)
*)




end