Theory Spec_Framework

(*TODO: it is possible and would be good if we separate the entire system into a pure BI logic with reasoning,
  and that applied over a semantic framework together with IDE-CP, but I have no time now.
*)

chapter ‹Specification Framework›

theory Spec_Framework
  imports Phi_BI.Phi_BI "Phi_Semantics_Framework.Phi_Semantics_Framework"
  keywords "fiction_space"  :: thy_goal
  abbrevs "<shifts>" = "𝗌𝗁𝗂𝖿𝗍𝗌"
    and   "<val>" = "𝗏𝖺𝗅"
    and   "<vals>" = "𝗏𝖺𝗅𝗌"
    and   "<typeof>" = "𝗍𝗒𝗉𝖾𝗈𝖿"
begin

subsubsection ‹Configuration›

declare [[φreason_default_pattern ‹Valid_Proc ?F› ⇒ ‹Valid_Proc ?F› (100)]]
declare Valid_Proc_bind[φreason 1200]
declare φarg.simps[φsafe_simp] φarg.sel[φsafe_simp]

optional_translations (do_notation)
  "_do_then t" <= "_do_bind (_constrain _idtdummy TY) t"
  "_do_cons A (_do_cons B C)" <= "_do_cons (_do_cons A B) C"

syntax "_φV3" :: ‹logic ⇒ logic› ("_⇩'(⇩3⇩')")
       "_φV4" :: ‹logic ⇒ logic› ("_⇩'(⇩4⇩')")
       "_φV5" :: ‹logic ⇒ logic› ("_⇩'(⇩5⇩')")
       "_φV6" :: ‹logic ⇒ logic› ("_⇩'(⇩6⇩')")
       "_φV7" :: ‹logic ⇒ logic› ("_⇩'(⇩7⇩')")

optional_translations (do_notation)
  "x⇩(⇩2⇩)" <= "x⇩(⇩2⇩)⇩(⇩1⇩)"
  "x⇩(⇩3⇩)" <= "x⇩(⇩2⇩)⇩(⇩2⇩)"
  "x⇩(⇩4⇩)" <= "x⇩(⇩2⇩)⇩(⇩3⇩)"
  "x⇩(⇩5⇩)" <= "x⇩(⇩2⇩)⇩(⇩4⇩)"
  "x⇩(⇩6⇩)" <= "x⇩(⇩2⇩)⇩(⇩5⇩)"
  "x⇩(⇩7⇩)" <= "x⇩(⇩2⇩)⇩(⇩6⇩)"

  "x" <= "CONST φarg x"

print_translation ‹[
  (\<^const_syntax>‹bind_do›, fn _ => (
    fn (*[A, Abs B] =>
          Const(\<^const_syntax>‹bind_do›, dummyT)
            $ A
            $ (case Syntax_Trans.atomic_abs_tr' B
                 of (f,x) => Const(\<^syntax_const>‹_abs›, dummyT) $ f $ x)
     |*) [A, Const ("_abs", _) $ _ $ _] => raise Match
     | [_, Abs _] => raise Match
     | [A, B] =>
          Const(\<^const_syntax>‹bind_do›, dummyT)
            $ A
            $ (case Syntax_Trans.atomic_abs_tr' ("_", dummyT, Term.incr_boundvars 1 B $ Bound 0)
                 of (f,x) => Const(\<^syntax_const>‹_abs›, dummyT) $ f $ x) ))
]›

(*
term ‹φV_fst x›
term ‹φV_snd x›
term ‹λx. φV_fst (φV_snd x)›
term ‹λx. (φV_snd (φV_snd x))›
term ‹λx. φV_fst (φV_snd (φV_snd x))›
term ‹λx. φV_snd (φV_snd (φV_snd x))›
term ‹λx. φV_fst (φV_snd (φV_snd (φV_snd x)))›
term ‹λx. φV_snd (φV_snd (φV_snd (φV_snd x)))›
term ‹λx. φV_snd (φV_fst (φV_snd (φV_snd x)))›
term ‹λx. φV_snd (φV_snd (φV_snd (φV_snd (φV_snd x))))›
*)

section ‹Fiction›

unspecified_type FIC
unspecified_type FIC_N

type_synonym fiction = ‹FIC_N ⇒ FIC›
type_synonym 'a assertion = ‹'a BI›
type_synonym assn = ‹fiction BI›
type_synonym rassn = ‹resource BI›
type_synonym 'T fiction_entry = "(FIC_N, FIC, 'T) Resource_Space.kind"

setup ‹Sign.mandatory_path "FIC"›

consts DOMAIN :: ‹FIC_N ⇒ FIC sep_homo_set›

debt_axiomatization sort: ‹OFCLASS(FIC, sep_algebra_class)›

setup ‹Sign.parent_path›

instance FIC :: sep_algebra using FIC.sort .

instantiation FIC :: sep_carrier_1 begin
definition mul_carrier_FIC :: ‹FIC ⇒ bool› where ‹mul_carrier_FIC = (λ_. True)›
  ― ‹As a type specially defined to represent the representation of fictions, it can be noisy-free.›
instance by (standard; simp add: mul_carrier_FIC_def)
end

consts INTERPRET :: ‹FIC_N ⇒ (FIC, resource) unital_homo_interp›

interpretation FIC: fictional_space FIC.DOMAIN INTERPRET .

definition "INTERP_RES fic ≡ BI_lift RES.SPACE ⊓ FIC.INTERP fic 𝗌𝗎𝖻𝗃 fic ∈ FIC.SPACE"
  ― ‹Interpret a fiction›

lemma In_INTERP_RES:
  ‹r ⊨ INTERP_RES fic ⟷ r ∈ RES.SPACE ∧ fic ∈ FIC.SPACE ∧ r ⊨ FIC.INTERP fic›
  unfolding INTERP_RES_def by simp blast

definition INTERP_SPEC :: ‹assn ⇒ rassn›
  ― ‹Interpret a fictional specification›
  where "INTERP_SPEC T = BI_Monad_Comb (INTERP_RES `⇩I T)"

lemma INTERP_SPEC:
  ‹res ⊨ INTERP_SPEC T ⟷ (∃fic. fic ⊨ T ∧ res ⊨ INTERP_RES fic)›
  unfolding INTERP_SPEC_def
  by simp blast

lemma INTERP_SPEC_sub[intro, simp]: ‹A ≤ B ⟹ INTERP_SPEC A ≤ INTERP_SPEC B›
  unfolding INTERP_SPEC_def less_eq_BI_iff by simp blast

lemma INTERP_SPEC_plus[iff]:
  ‹INTERP_SPEC (A + B) = INTERP_SPEC A + INTERP_SPEC B›
  unfolding BI_eq_iff
  by (simp add: INTERP_SPEC) blast

lemma INTERP_SPEC_0[iff]:
  ‹ INTERP_SPEC 0 = 0 ›
  unfolding BI_eq_iff
  by (simp add: INTERP_SPEC)

(*
lemma INTERP_SPEC_empty[intro, simp]:
  ‹S = {} ⟹ INTERP_SPEC S = {}›
  unfolding INTERP_SPEC_def set_eq_iff by simp

lemma INTERP_SPEC_0[simp]:
  ‹INTERP_SPEC 0  = 0›
  ‹INTERP_SPEC {} = {}›
  unfolding INTERP_SPEC_def zero_set_def by simp+
*)

ML_file ‹library/spec_framework/fiction_space.ML›
ML_file ‹library/spec_framework/fiction_space_more.ML›

ML ‹Fiction_Space.define_command \<^command_keyword>‹fiction_space› "extend fictions"›

(*
lemma INTERP_mult:
  ‹ Fic_Space f1
⟹ Fic_Space f2
⟹ dom1 r1 ∩ dom1 r2 = {}
⟹ dom1 f1 ∩ dom1 f2 = {}
⟹ r1 ∈ ℐ INTERP f1
⟹ r2 ∈ ℐ INTERP f2
⟹ f1 ## f2
⟹ r1 * r2 ∈ ℐ INTERP (f1 * f2) ∧ r1 ## r2›
  unfolding INTERP_def Fic_Space_def
  by (simp add: dom1_sep_mult_disjoint times_fun prod.union_disjoint
                disjoint_dom1_eq_1[of f1 f2],
      meson dom1_disjoint_sep_disj times_set_I) *)


section ‹Specification of Value›

type_synonym value_assertion = ‹VAL BI›

subsection ‹Primitive φ-Types›

subsubsection ‹Value›

definition Val :: ‹VAL φarg ⇒ (VAL, 'a) φ ⇒ ('x::one, 'a) φ› ("𝗏𝖺𝗅[_] _" [22,22] 21)
  where ‹Val val T = (λx. 1 𝗌𝗎𝖻𝗃 φarg.dest val ⊨ (x ⦂ T))›

definition Vals :: ‹VAL list φarg ⇒ (VAL list, 'a) φ ⇒ ('x::one, 'a) φ› ("𝗏𝖺𝗅𝗌[_] _" [22,22] 21)
  where ‹Vals vals T = (λx. 1 𝗌𝗎𝖻𝗃 φarg.dest vals ⊨ (x ⦂ T))›

lemma Val_expn [simp, φexpns]:
  ‹v ⊨ (x ⦂ Val val T) ⟷ v = 1 ∧ φarg.dest val ⊨ (x ⦂ T)›
  unfolding Val_def φType_def by simp

lemma Vals_expn [simp, φexpns]:
  ‹v ⊨ (x ⦂ Vals val T) ⟷ v = 1 ∧ φarg.dest val ⊨ (x ⦂ T)›
  unfolding Vals_def φType_def by simp

lemma Val_inh_rewr:
  ‹Satisfiable (x ⦂ Val val T) ≡ φarg.dest val ⊨ (x ⦂ T)›
  unfolding Satisfiable_def by clarsimp

lemma Vals_inh_rewr:
  ‹Satisfiable (x ⦂ Vals val T) ≡ φarg.dest val ⊨ (x ⦂ T)›
  unfolding Satisfiable_def by clarsimp


paragraph ‹Syntax›

consts anonymous :: 'a

syntax val_syntax  :: "logic ⇒ logic" ("𝗏𝖺𝗅 _"  [22] 21)
       vals_syntax :: "logic ⇒ logic" ("𝗏𝖺𝗅𝗌 _" [22] 21)

translations
  "𝗏𝖺𝗅 x ⦂ T" => "x ⦂ CONST Val (CONST anonymous) T"
  "𝗏𝖺𝗅 T" => "CONST Val (CONST anonymous) T"
  "𝗏𝖺𝗅𝗌 x ⦂ T" => "x ⦂ CONST Vals (CONST anonymous) T"
  "𝗏𝖺𝗅𝗌 T" => "CONST Vals (CONST anonymous) T"

ML_file ‹library/syntax/value.ML›


subsubsection ‹Abnormal›

definition AbnormalObj :: ‹VAL φarg ⇒ (VAL, 'a) φ ⇒ ('x::one, 'a) φ›
  where ‹AbnormalObj ≡ Val›

(*TODO: more about exception

Any exception object will be specified by this type. and by this we clarify the difference
between a value and an exception object.
Then in exception specs, any Val is senseless and will be removed.*)


subsection ‹Semantic Type›

consts Type_Of_syntax :: ‹'a ⇒ TY› ("𝗍𝗒𝗉𝖾𝗈𝖿")

definition Semantic_Type :: ‹(VAL, 'x) φ ⇒ TY ⇒ bool›
  where ‹Semantic_Type T TY ≡ (∀x v. v ⊨ (x ⦂ T) ⟶ v ∈ Well_Type TY) ›

definition Semantic_Type' :: ‹VAL BI ⇒ TY ⇒ bool›
  where ‹Semantic_Type' A TY ≡ (∀v. v ⊨ A ⟶ v ∈ Well_Type TY) ›

definition SType_Of :: ‹(VAL, 'x) φ ⇒ TY›
  where ‹SType_Of T = (
      if Inhabited T ∧ (∃TY. Semantic_Type T TY)
      then (@TY. Semantic_Type T TY)
      else 𝗉𝗈𝗂𝗌𝗈𝗇 )›

definition SType_Of' :: ‹VAL BI ⇒ TY›
  where ‹SType_Of' A = (
      if Satisfiable A ∧ (∃TY. Semantic_Type' A TY)
      then (@TY. Semantic_Type' A TY)
      else 𝗉𝗈𝗂𝗌𝗈𝗇 )›

adhoc_overloading Type_Of_syntax SType_Of SType_Of'

lemma SType_Of'_implies_SType_Of:
  ‹ (⋀x. 𝗍𝗒𝗉𝖾𝗈𝖿 (x ⦂ T) = TY)
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY›
  unfolding SType_Of_def SType_Of'_def Inhabited_def Semantic_Type_def Semantic_Type'_def
  by (auto, smt (verit) Satisfiable_def Well_Type_unique tfl_some,
            smt (verit, best) tfl_some)

lemma SType_Of'_implies_SType_Of''':
  ‹ Abstract_Domain T D
⟹ Abstract_Domain⇩L T D⇩L
⟹ (⋀x. D x ∨ (∀y. ¬ D⇩L y) ⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 (x ⦂ T) = TY)
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY›
  unfolding SType_Of_def SType_Of'_def Inhabited_def Abstract_Domain⇩L_def
            Action_Tag_def 𝗋ESC_def 𝗋EIF_def Abstract_Domain_def Satisfiable_def
            Semantic_Type_def Semantic_Type'_def
  by (auto,
      smt (verit, ccfv_SIG) Well_Type_unique someI,
      smt (verit, ccfv_SIG) someI)

lemma SType_Of_not_poison:
  ‹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY ∧ TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇 ⟷ Inhabited T ∧ (∀x v. v ⊨ (x ⦂ T) ⟶ v ∈ Well_Type TY) ›
  unfolding SType_Of_def Inhabited_def Satisfiable_def
            Semantic_Type_def Semantic_Type'_def
  by (auto, smt (verit, best) someI2_ex, insert Well_Type_disjoint, blast)

lemma SType_Of'_not_poison:
  ‹ 𝗍𝗒𝗉𝖾𝗈𝖿 A = TY ∧ TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇 ⟷ Satisfiable A ∧ (∀v. v ⊨ A ⟶ v ∈ Well_Type TY) ›
  unfolding SType_Of'_def Satisfiable_def Semantic_Type_def Semantic_Type'_def
  by (auto, smt (verit, best) someI2_ex, insert Well_Type_disjoint, blast)


(*
subsubsection ‹Single Value›

definition Semantic_Type :: ‹(VAL,'x) φ ⇒ TY ⇒ bool›
  where ‹Semantic_Type T TY ⟷ (∀x v. v ⊨ (x ⦂ T) ⟶ v ∈ Well_Type TY)›

definition Semantic_Type' :: "value_assertion ⇒ TY ⇒ bool"
  where ‹Semantic_Type' S TY ⟷ (∀v. v ⊨ S ⟶ v ∈ Well_Type TY)›
  ― ‹Values specified by ‹S› are all of semantic type ‹TY›.›

(*definition φφSemType :: "(VAL, 'a) φ ⇒ ('a ⇒ bool) ⇒ ('a ⇒ TY) ⇒ bool"
  where ‹φφSemType T D TY ≡ (∀x. D x ⟶ φSemType (x ⦂ T) (TY x))›*)

declare [[
  φreason_default_pattern ‹Semantic_Type ?T _›  ⇒ ‹Semantic_Type ?T _›  (100)
                      and ‹Semantic_Type' ?A _› ⇒ ‹Semantic_Type' ?A _› (100)
]]
*)

φreasoner_group φsem_type_infer_all = (100, [1, 2000]) for (‹SType_Of T = _ @tag 𝒜infer›, ‹SType_Of' T = _ @tag 𝒜infer› )‹›
            and φsem_type_infer_fallback = (1, [1, 1]) in φsem_type_infer_all ‹›
            and φsem_type_infer_brute = (10, [10,20]) in φsem_type_infer_all
                                                     and > φsem_type_infer_fallback ‹›
            and φsem_type_infer_cut = (1000, [1000, 1030]) in φsem_type_infer_all ‹›
            and φsem_type_infer_derived = (50, [50,60]) in φsem_type_infer_all
                                                       and > φsem_type_infer_brute ‹›

φreasoner_group Semantic_Type_all = (100, [10, 2000]) for (‹Semantic_Type _ _›, ‹Semantic_Type' _ _›) ‹›
  and Semantic_Type = (1000, [1000,1030]) in Semantic_Type_all ‹›
  and Semantic_Type_default = (50, [30,80]) in Semantic_Type_all ‹›
  and Semantic_Type_fallback = (15, [10,20]) in Semantic_Type_all and < Semantic_Type_default ‹›

declare [[
    φreason_default_pattern ‹Semantic_Type ?T _› ⇒ ‹Semantic_Type ?T ?var› (100)
                        and ‹Semantic_Type' ?T _› ⇒ ‹Semantic_Type' ?T ?var› (100),
    φdefault_reasoner_group ‹Semantic_Type _ _› : %Semantic_Type (100),
    φdefault_reasoner_group ‹Semantic_Type' _ _› : %Semantic_Type (100),

    φreason_default_pattern ‹SType_Of  ?T = _ @tag 𝒜infer› ⇒ ‹SType_Of  ?T = _ @tag 𝒜infer› (100)
                        and ‹SType_Of' ?T = _ @tag 𝒜infer› ⇒ ‹SType_Of' ?T = _ @tag 𝒜infer› (100),
    φdefault_reasoner_group ‹SType_Of  ?T = _ @tag 𝒜infer› : %φsem_type_infer_cut (100),
    φdefault_reasoner_group ‹SType_Of' ?T = _ @tag 𝒜infer› : %φsem_type_infer_cut (100)
]]


(*
φreasoner_group φsem_type = (100, [0, 3000]) for (‹SType_Of T = TY @tag 𝒜infer›)
      ‹giving the semantic type of the concrete value satisfying the given assertion or φ-type›
  and φsem_type_fail = (0, [0,0]) in φsem_type
      ‹failures›
  and φsem_type_brute = (2, [2,2]) in φsem_type > φsem_type_fail
      ‹reducing to concrete level, used only when deriving rules.›
  and φsem_type_failback = (3, [3,3]) in φsem_type > φsem_type_brute
      ‹system usage›
  and φsem_type_assertion = (10, [10,10]) in φsem_type and > φsem_type_failback
      ‹asserting the given with a semantic type if any›
(*and φsem_type_φtyp = (10, [10,10]) in φsem_type and > φsem_type_fail
      ‹‹φSemType› -> ‹φφSemType››*)
  and φsem_type_derived = (50, [50,50]) in φsem_type and > φsem_type_assertion
      ‹derived rules›
  and φsem_type_cut = (1000, [1000,1030]) in φsem_type and > φsem_type_derived
      ‹cutting rules›
  and φsem_type_red = (2200, [2200,2500]) in φsem_type and > φsem_type_cut
      ‹reduction and evaluation›

φreasoner_group sem_typ_chk = (80, [80,90]) > lambda_unify_all ‹›
  *)

(*lemma φSemType_unique:
  ‹ S ≠ {}
⟹ φSemType S T1
⟹ φSemType S T2
⟹ T1 = T2›
  unfolding φSemType_def subset_iff
  using Well_Type_unique by blast *)

(* definition SemTyp_Of :: ‹VAL set ⇒ TY›
  where ‹SemTyp_Of S = (@TY. φSemType S TY)›

lemma SemTyp_Of_I[intro!, simp]:
  ‹S ≠ {} ⟹ φSemType S TY ⟹ SemTyp_Of S = TY›
  unfolding SemTyp_Of_def
  using φSemType_unique by blast *)

(*

lemma [φreason 100]:
  ‹ (⋀x. φSemType (x ⦂ T) TY)
⟹ φφSemType T TY›
  .. *)

paragraph ‹Basic Rules›

lemma [φreason %φsem_type_infer_fallback]:
  ‹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒 TY : 𝗍𝗒𝗉𝖾𝗈𝖿 A
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 A = TY @tag 𝒜infer ›
  for A :: ‹VAL BI›
  unfolding Action_Tag_def Simplify_def
  by blast

lemma φSemType_Itself_brute:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 v ∈ Well_Type TY
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 (v ⦂ Itself) = TY @tag 𝒜infer ›
  unfolding SType_Of'_def Inhabited_def Satisfiable_def Premise_def Action_Tag_def
            Semantic_Type_def Semantic_Type'_def
  by (auto, insert Well_Type_unique, blast)

lemma φsem_type_by_sat:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 ((∀v. v ⊨ S ⟶ v ∈ Well_Type TY) ∧ (¬ Satisfiable S ⟶ TY = 𝗉𝗈𝗂𝗌𝗈𝗇))
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 S = TY @tag 𝒜infer ›
  unfolding Premise_def 𝗋Guard_def SType_Of'_def Satisfiable_def Action_Tag_def
            Semantic_Type_def Semantic_Type'_def
  by (auto simp: split_ifs, insert Well_Type_unique, blast)
  

(*
lemma φsem_type_brute_EIF':
  ‹ 𝗋EIF (Semantic_Type' S TY) (∀v. v ⊨ S ⟶ v ∈ Well_Type TY) ›
  unfolding 𝗋EIF_def Semantic_Type'_def
  by blast

lemma φsem_type_brute_EIF:
  ‹ 𝗋EIF (Semantic_Type T TY) (∀x v. v ⊨ (x ⦂ T) ⟶ v ∈ Well_Type TY) ›
  unfolding 𝗋EIF_def Semantic_Type_def
  by blast
*)

bundle φsem_type_sat_EIF = φsem_type_by_sat[φreason default %φsem_type_infer_brute]
                        (* φsem_type_brute_EIF[φreason %extract_pure]
                           φsem_type_brute_EIF'[φreason %extract_pure]  *)
                           φSemType_Itself_brute[φreason %φsem_type_infer_cut]

(*
lemma [φreason default %φsem_type_failback]:
  ‹ 𝗀𝗎𝖺𝗋𝖽 Semantic_Type T TY
⟹ Semantic_Type' (x ⦂ T) TY ›
  unfolding Semantic_Type'_def Semantic_Type_def 𝗋Guard_def
  by simp
*)

paragraph ‹Over Logic Connectives›

lemma 𝗍𝗒𝗉𝖾𝗈𝖿_plus[simp]:
  ‹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = 𝗍𝗒𝗉𝖾𝗈𝖿 U
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 (T + U) = 𝗍𝗒𝗉𝖾𝗈𝖿 T ›
  for T :: ‹VAL BI›
  unfolding SType_Of'_def Inhabited_def Satisfiable_def subset_iff Semantic_Type_def Semantic_Type'_def
  using Well_Type_unique by (clarsimp, smt (z3) someI)

lemma [φreason add]:
  ‹ 𝗍𝗒𝗉𝖾𝗈𝖿 T = TY⇩1 @tag 𝒜infer
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 U = TY⇩2 @tag 𝒜infer
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 TY⇩1 = TY⇩2
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 (T + U) = TY⇩1 @tag 𝒜infer ›
  for T :: ‹VAL BI›
  unfolding Action_Tag_def Premise_def
  by simp

lemma 𝗍𝗒𝗉𝖾𝗈𝖿_bot[simp]:
  ‹ 𝗍𝗒𝗉𝖾𝗈𝖿 ⊥⇩B⇩I = 𝗉𝗈𝗂𝗌𝗈𝗇 ›
  unfolding SType_Of'_def
  by auto

lemma [φreason add]:
  ‹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 P ⟶ 𝗍𝗒𝗉𝖾𝗈𝖿 X = TY @tag 𝒜infer
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 (X 𝗌𝗎𝖻𝗃 P) = (if P then TY else 𝗉𝗈𝗂𝗌𝗈𝗇) @tag 𝒜infer ›
  unfolding Action_Tag_def Premise_def
  by auto

lemma 𝗍𝗒𝗉𝖾𝗈𝖿_𝗌𝗎𝖻𝗃[simp]:
  ‹ 𝗍𝗒𝗉𝖾𝗈𝖿 (X 𝗌𝗎𝖻𝗃 P) = (if P then 𝗍𝗒𝗉𝖾𝗈𝖿 X else 𝗉𝗈𝗂𝗌𝗈𝗇) ›
  by auto

lemma [φreason add]:
  ‹ (⋀x. 𝗍𝗒𝗉𝖾𝗈𝖿 (X x) = TY @tag 𝒜infer)
⟹ 𝗍𝗒𝗉𝖾𝗈𝖿 (ExBI X) = TY @tag 𝒜infer ›
  unfolding Action_Tag_def SType_Of'_def Inhabited_def Satisfiable_def subset_iff            
  by (auto,
      metis (no_types, lifting) ExBI_expn Semantic_Type'_def Well_Type_unique verit_sko_ex',
      metis ExBI_expn Satisfaction_def Semantic_Type'_def tfl_some)

subsubsection ‹Auxiliary Reasoners›

paragraph ‹Check Type Literal›

definition ‹Is_Type_Literal (TY::TY) ≡ True›

φreasoner_group Is_Type_Literal = (1000, [10, 2000]) for ‹Is_Type_Literal TY› ‹›
    and Is_Type_Literal_default = (10, [10, 20]) in Is_Type_Literal ‹›

declare [[ φdefault_reasoner_group ‹Is_Type_Literal _› : %Is_Type_Literal (100) ]]

lemma Is_Type_Literal_I[intro!]: ‹Is_Type_Literal X›
  unfolding Is_Type_Literal_def ..

φreasoner_ML Is_Type_Literal_Free default %Is_Type_Literal_default (‹Is_Type_Literal _›) = ‹
  fn (_,(ctxt,sequent)) =>
    case Thm.major_prem_of sequent
      of Trueprop $ (Const(\<^const_name>‹Is_Type_Literal›, _) $ (Const(\<^const_name>‹SType_Of›, _) $ Free _)) =>
          Seq.single (ctxt, @{thm' Is_Type_Literal_I} RS sequent)
       | _ => Seq.empty
›

paragraph ‹Unfolding ‹𝗍𝗒𝗉𝖾𝗈𝖿 T››

φreasoner_group eval_sem_typ = (100, [75, 2000]) > lambda_unify__default
                                ‹Unfolding ‹𝗍𝗒𝗉𝖾𝗈𝖿 T› exhausitively, with checking the result is not a poison.›

(*
lemma Semantic_Type_alt_def:
  ‹ Semantic_Type T TY ⟷ Inhabited T ∧ (∀x v. v ⊨ (x ⦂ T) ⟶ v ∈ Well_Type TY) ›
  unfolding Semantic_Type_def
  by (smt (verit, del_insts) SType_Of_not_poison Bot_Satisfiable Inhabited_def Int_iff SType_Of_def
      Satisfaction_def Well_Type_disjoint φBot.expansion φBot.unfold φType_eqI bot_eq_BI_bot someI) 

lemma Semantic_Type'_alt_def:
  ‹ Semantic_Type' A TY ⟷ Satisfiable A ∧ (∀v. v ⊨ A ⟶ v ∈ Well_Type TY) ›
  unfolding Semantic_Type'_def
  using SType_Of'_not_poison
  by (smt (verit, best) Action_Tag_def Premise_def φsem_type_by_sat)
*)



(*
paragraph ‹Conversion From Strong to Weak›

(* ML_file ‹library/spec_framework/semantic_type.ML› *)

*) 

subsubsection ‹Reasoning›

lemma [φreason default %Semantic_Type_fallback+5]:
  ‹ Abstract_Domain T D
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 Ex D ⟹ 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒 TY : 𝗍𝗒𝗉𝖾𝗈𝖿 T)
― ‹Is_Type_Literal TY 𝗈𝗋 𝖿𝖺𝗂𝗅 TEXT(‹Fail to evaluate› (𝗍𝗒𝗉𝖾𝗈𝖿 T))›
⟹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 (Ex D ⟶ TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇) 𝗈𝗋 𝖿𝖺𝗂𝗅 TEXT(‹Fail to evaluate› (𝗍𝗒𝗉𝖾𝗈𝖿 T) ‹: fail to show› (TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇))
⟹ Semantic_Type T TY ›
  unfolding Semantic_Type_def Simplify_def Premise_def OR_FAIL_def Abstract_Domain_def Premise_def
  by (auto simp add: Satisfiable_def 𝗋EIF_def, metis SType_Of_not_poison)

lemma [φreason default %Semantic_Type_fallback for ‹Semantic_Type _ _›
                                            except ‹Semantic_Type _ ?var›]:
  ‹ Semantic_Type T TY'
⟹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 TY = TY' 𝗈𝗋 𝖿𝖺𝗂𝗅 TEXT(‹Expecting› (𝗍𝗒𝗉𝖾𝗈𝖿 T) ‹to be› TY ‹but actually› TY')
⟹ Semantic_Type T TY ›
  unfolding OR_FAIL_def Premise_def
  by simp


lemma [φreason default %Semantic_Type_fallback+5]:
  ‹ Semantic_Type T TY
⟹ Semantic_Type' (x ⦂ T) TY ›
  unfolding Semantic_Type'_def Semantic_Type_def
  by auto

lemma [φreason default %Semantic_Type_fallback for ‹Semantic_Type' _ _›
                                            except ‹Semantic_Type' _ ?var›]:
  ‹ Semantic_Type' A TY'
⟹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 TY = TY' 𝗈𝗋 𝖿𝖺𝗂𝗅 TEXT(‹Expecting› (𝗍𝗒𝗉𝖾𝗈𝖿 A) ‹to be› TY ‹but actually› TY')
⟹ Semantic_Type' A TY ›
  unfolding OR_FAIL_def Premise_def
  by simp

lemma [φreason default %Semantic_Type_default]:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (v ∈ Well_Type TY)
⟹ Semantic_Type' (v ⦂ Itself) TY ›
  unfolding Premise_def Semantic_Type'_def
  by auto

lemma [φreason add]:
  ‹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 P ⟹ Semantic_Type' A TY)
⟹ Semantic_Type' (A 𝗌𝗎𝖻𝗃 P) TY ›
  unfolding Semantic_Type'_def
  by auto

lemma [φreason add]:
  ‹ (⋀x. Semantic_Type' (A x) TY)
⟹ Semantic_Type' (∃*x. A x) TY ›
  unfolding Semantic_Type'_def
  by auto


subsubsection ‹Multiple Values›

definition Well_Typed_Vals :: ‹TY list ⇒ 'a::VALs φarg set›
  where ‹Well_Typed_Vals TYs = {vs. list_all2 (λv T. v ∈ Well_Type T) (to_vals (φarg.dest vs)) TYs}›

definition Semantic_Types :: ‹('a::VALs φarg ⇒ assn) ⇒ TY list ⇒ bool›
  where ‹Semantic_Types spec TYs = (∀v. Satisfiable (spec v) ⟶ v ∈ Well_Typed_Vals TYs)›

definition ‹Semantic_Types_i = Semantic_Types›

declare [[
      φreason_default_pattern ‹Semantic_Types_i ?S _› ⇒ ‹Semantic_Types_i ?S _› (100)
                          and ‹Semantic_Types   ?S _› ⇒ ‹Semantic_Types   ?S _› (100),
      φdefault_reasoner_group ‹Semantic_Types   _ _› : %φsem_type_infer_cut (100),
      φdefault_reasoner_group ‹Semantic_Types_i _ _› : %φsem_type_infer_cut (100)
]]

lemma [φreason add]:
  ‹ (⋀v. S v 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 P v)
⟹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 (∃x. P x) ⟶ Semantic_Types_i S TYs
⟹ Semantic_Types S TYs ›
  unfolding Semantic_Types_i_def Semantic_Types_def Premise_def 𝗋EIF_def
  by auto

(*
subsubsection ‹Semantic Typeof›

definition SType_Of :: ‹(VAL, 'x) φ ⇒ TY›
  where ‹SType_Of T = (
      if Inhabited T
      then (@TY. Semantic_Type T TY)
      else 𝗉𝗈𝗂𝗌𝗈𝗇)›




lemma
  ‹ Semantic_Type T TY
⟹ Semantic_Type T (SType_Of T) ›
  unfolding SType_Of_def
  apply auto
  apply (simp add: someI)
  by (meson Inhabited_def Satisfiable_I Semantic_Type_def)



lemma SType_Of_unfold:
  ‹ Semantic_Type T TY
⟹ Inhabited T
⟹ SType_Of T ≡ TY ›
  unfolding Semantic_Type_def Inhabited_def SType_Of_def atomize_eq Satisfiable_def
  using Well_Type_unique
  by (clarsimp, smt (verit, del_insts) Satisfiable_def someI)

ML_file ‹library/tools/unfold_typeof.ML›
*)

(*
subsubsection ‹Generalized Semantic Typeof --- using Syntax Inference only›

definition Generalized_Semantic_Type :: ‹'any ⇒ TY ⇒ bool›
  where ‹Generalized_Semantic_Type T TY ≡ True›
  ― ‹merely providing a syntactical inference that may help certain inferences like inferring
      the semantic type of a memory partial object as that used in the inference for ‹𝗉𝗈𝗂𝗇𝗍𝖾𝗋-𝗈𝖿››

declare [[ φreason_default_pattern
    ‹Generalized_Semantic_Type ?T _› ⇒ ‹Generalized_Semantic_Type ?T _› (100)
]]

φreasoner_group generalized_sematic_type = (100, [1,3000]) ‹Generalized_Semantic_Type›
            and generalized_sematic_type_cut = (1000, [1000,1030]) in generalized_sematic_type ‹cut›
            and generalized_sematic_type_fallback = (10, [10,10]) in generalized_sematic_type ‹fallback›

lemma [φreason default %generalized_sematic_type_fallback]:
  ‹ (SYNTACTIC_MODE ⟹ Semantic_Type T TY)
⟹ Generalized_Semantic_Type T TY›
  unfolding Generalized_Semantic_Type_def ..

lemma Semantic_Type_by_Synt_Sugar:
  ‹ 𝗀𝗎𝖺𝗋𝖽 SYNTACTIC_MODE
⟹ Semantic_Type T (𝗍𝗒𝗉𝖾𝗈𝖿 T) ›
  unfolding 𝗋Guard_def SYNTACTIC_MODE_def by blast

bundle Semantic_Type_by_Synt_Sugar =
          Semantic_Type_by_Synt_Sugar[φreason default %Semantic_Type_fallback-5]
*)

subsection ‹Zero Value›

definition Semantic_Zero_Val :: "TY ⇒ (VAL,'a) φ ⇒ 'a ⇒ bool"
  where "Semantic_Zero_Val ty T x ⟷ (ty ≠ 𝗉𝗈𝗂𝗌𝗈𝗇 ⟶ (∃v. Zero ty = Some v ∧ v ⊨ (x ⦂ T)))"

declare [[φreason_default_pattern ‹Semantic_Zero_Val _ ?T _› ⇒ ‹Semantic_Zero_Val _ ?T ?varz› (100) ]]

φreasoner_group semantic_zero_val_all = (100, [0, 3000]) for ‹Semantic_Zero_Val TY T x›
    ‹giving the semantic zero value on the abstraction side›
  and semantic_zero_val_fail = (0, [0,0]) in semantic_zero_val_all
    ‹failure›
  and semantic_zero_val_fallback = (10, [1,20]) in semantic_zero_val_all and > semantic_zero_val_fail
    ‹reducing to semantic level, only used in deriving rules›
  and semantic_zero_val_cut = (1000, [1000, 1000]) in semantic_zero_val_all
    ‹cutting rules›
  and semantic_zero_val_derived = (50, [50,50]) in semantic_zero_val_all
                                               and < semantic_zero_val_cut
                                               and > semantic_zero_val_fallback
    ‹derived rules›

subsubsection ‹Basic Rules›

lemma [φreason default %semantic_zero_val_fail]:
  ‹ FAIL TEXT(‹Don't know any semantic zero value satisfying φ-type› T)
⟹ Semantic_Zero_Val TY T x ›
  unfolding FAIL_def
  by blast

lemma [φreason %extract_pure]:
  ‹ Abstract_Domain T P
⟹ 𝗋EIF (Semantic_Zero_Val TY T x) (TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇 ⟶ P x) ›
  unfolding Abstract_Domain_def Semantic_Zero_Val_def 𝗋EIF_def Satisfiable_def
  by blast

(*lemma Semantic_Zero_Val_brute:
  ‹ 𝗀𝗎𝖺𝗋𝖽 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 (∃v. Zero TY = Some v ∧ v ⊨ (x ⦂ T))
⟹ Semantic_Zero_Val TY T x ›
  unfolding Semantic_Zero_Val_def 𝗋Guard_def Premise_def
  by blast
*)

lemma Semantic_Zero_Val_EIF_sat:
  ‹ 𝗋EIF (Semantic_Zero_Val TY T x) (TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇 ⟶ (∃v. Zero TY = Some v ∧ v ⊨ (x ⦂ T))) ›
  unfolding 𝗋EIF_def Semantic_Zero_Val_def
  by blast

bundle Semantic_Zero_Val_EIF_brute = (*Semantic_Zero_Val_brute[φreason default %semantic_zero_val_brute]*)
                                     Semantic_Zero_Val_EIF_sat[φreason %extract_pure+10]

(*
lemma [φreason %semantic_zero_val_fallback for ‹Semantic_Zero_Val _ _ _›
                                        except ‹Semantic_Zero_Val ?var _ _› ]:
  ‹ Semantic_Zero_Val TY' U z
⟹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 TY = TY'
⟹ Semantic_Zero_Val TY  U z ›
  unfolding Premise_def
  by simp
*)

lemma [φreason %semantic_zero_val_cut for ‹Semantic_Zero_Val (𝗍𝗒𝗉𝖾𝗈𝖿 (_ :: (VAL,_) φ)) _ _› ]:
  ‹ 𝗀𝗎𝖺𝗋𝖽 𝗌𝗂𝗆𝗉𝗅𝗂𝖿𝗒[𝖼𝗁𝖺𝗇𝗀𝖾𝖽 default] TY : 𝗍𝗒𝗉𝖾𝗈𝖿 T
⟹ Semantic_Zero_Val TY U z
⟹ Semantic_Zero_Val (𝗍𝗒𝗉𝖾𝗈𝖿 T) U z ›
  for T :: ‹(VAL,'x) φ›
  unfolding 𝗋Guard_def Simplify_def
  by simp


subsection ‹Equality›

definition φEqual :: "(VAL,'a) φ ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
  where "φEqual T can_eq eq ⟷ (∀p1 p2 x1 x2 res.
    can_eq x1 x2 ∧ p1 ⊨ (x1 ⦂ T) ∧ p2 ⊨ (x2 ⦂ T)
      ⟶ Can_EqCompare res p1 p2 ∧ (EqCompare p1 p2 = eq x1 x2))"

declare [[φreason_default_pattern ‹φEqual ?TY ?can_eq ?eq› ⇒ ‹φEqual ?TY _ _› (100) ]]


subsection ‹Functional›

definition Is_Functional :: ‹'a BI ⇒ bool›
  where ‹Is_Functional S ⟷ (∀x y. x ⊨ S ∧ y ⊨ S ⟶ x = y)›

definition Functionality :: ‹('c,'a) φ ⇒ ('a ⇒ bool) ⇒ bool›
  where ‹Functionality T p ⟷ (∀x u v. p x ∧ u ⊨ (x ⦂ T) ∧ v ⊨ (x ⦂ T) ⟶ u = v)›
  ― ‹A lower bound of the set in which φ-type assertions are functional›

declare [[φreason_default_pattern ‹Is_Functional ?S› ⇒ ‹Is_Functional ?S› (100)
                              and ‹Functionality ?T _› ⇒ ‹Functionality ?T _› (100)]]

φreasoner_group φfunctionality_all = (%cutting, [1,3000]) for (‹Is_Functional S›, ‹Functionality T p›)
    ‹All reasoning rules giving functionality of φ-types, meaning if the assertion uniquely fixes
     a concrete object for each abstract object.›
  and φfunctionality = (%cutting, [%cutting, %cutting+30]) in φfunctionality_all
    ‹Default rules are cutting›
  and derived_φfunctionality = (50, [40,60]) in φfunctionality_all and < φfunctionality
    ‹Derived rules›
  and φfunctional_to_functionality = (10, [10,10]) in φfunctionality_all and < derived_φfunctionality
    ‹Trunning ‹Is_Functional (x : T)› to ‹Functionality T p››
  and φfunctionality_brute = (2, [2,2]) in φfunctionality_all and < φfunctional_to_functionality
    ‹reducing to concrete semantics, and only used in deriving rules›


subsubsection ‹Basic Rules›

lemma functional_concretize:
  ‹ Functionality T ((=) x)
⟹ v ⊨ (x ⦂ T)
⟹ v = concretize T x ›
  unfolding concretize_def φType_def Functionality_def
  by (simp add: some_equality)

lemma concretize_eq:
  ‹ Abstract_Domain⇩L T ((=) x)
⟹ Functionality U ((=) y)
⟹ x ⦂ T 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 y ⦂ U
⟹ concretize T x = concretize U y ›
  unfolding Transformation_def Abstract_Domain⇩L_def 𝗋ESC_def
  by (simp add: concretize_SAT functional_concretize)


(*deprecated*)
lemma Is_Functional_premise_extraction:
  ‹Is_Functional S ≡ (∀u v. u ⊨ S ∧ v ⊨ S ⟶ u = v) ∧ True›
  unfolding Is_Functional_def atomize_eq
  by blast

(*deprecated*)
lemma Functionality_premise_extraction:
  ‹Functionality T P ≡ (∀x u v. P x ∧ u ⊨ (x ⦂ T) ∧ v ⊨ (x ⦂ T) ⟶ u = v) ∧ True›
  unfolding Functionality_def atomize_eq
  by blast

lemma Functionality_sub:
  ‹ (∀x. P' x ⟶ P x)
⟹ Functionality T P
⟹ Functionality T P' ›
  unfolding Functionality_def
  by auto

(* lemma Is_Functional_alt:
  ‹Is_Functional S ⟷ (S = {} ∨ (∃x. S = {x}))›
  unfolding Is_Functional_def by blast *)

lemma Is_Functional_I[intro!]:
  ‹ (⋀x y. x ⊨ A ⟹ y ⊨ A ⟹ x = y)
⟹ Is_Functional A ›
  unfolding Is_Functional_def by blast

lemma Is_Functional_imp:
  ‹ S 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 S'
⟹ Is_Functional S'
⟹ Is_Functional S›
  unfolding Transformation_def Is_Functional_def
  by blast

lemma [φreason no explorative backtrack 0]:
  ‹ TRACE_FAIL TEXT(‹Fail to show› S ‹is functional›)
⟹ Is_Functional S›
  unfolding TRACE_FAIL_def
  by blast

lemma [φreason default %φfunctional_to_functionality]:
  ‹ Functionality T p
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 p x
⟹ Is_Functional (x ⦂ T)›
  unfolding Premise_def Is_Functional_def Functionality_def
  by simp


lemma Is_Functional_brute:
  ‹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (∀u v. u ⊨ S ∧ v ⊨ S ⟶ u = v)
⟹ Is_Functional S ›
  unfolding Is_Functional_def Premise_def
  by blast

lemma Is_Functional_EIF_brute:
  ‹ 𝗋EIF (Is_Functional S) (∀u v. u ⊨ S ∧ v ⊨ S ⟶ u = v) ›
  unfolding 𝗋EIF_def Is_Functional_def
  by blast

lemma Functionality_EIF_brute:
  ‹ 𝗋EIF (Functionality T D) (∀x u v. D x ∧ u ⊨ (x ⦂ T) ∧ v ⊨ (x ⦂ T) ⟶ u = v) ›
  unfolding 𝗋EIF_def Functionality_def
  by blast

bundle Is_Functional_brute = Is_Functional_brute[φreason default %φfunctionality_brute]
                             Is_Functional_EIF_brute[φreason %extract_pure+10]
                             Functionality_EIF_brute[φreason %extract_pure+10]


subsubsection ‹Basic Types and Connectives›

lemma [φreason %φfunctionality]:
  ‹Functionality Itself (λ_. True)›
  unfolding Functionality_def
  by clarsimp

lemma [φreason %φfunctionality]:
  ‹ Is_Functional 1 ›
  unfolding Is_Functional_def
  by simp

lemma [φreason %φfunctionality]:
  ‹ Is_Functional 0 ›
  unfolding Is_Functional_def
  by simp

lemma [φreason %φfunctionality]:
  ‹ Is_Functional A
⟹ Is_Functional B
⟹ Is_Functional (A ⊓ B) ›
  unfolding Is_Functional_def
  by simp

lemma [φreason %φfunctionality]:
  ‹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 P ⟹ Is_Functional S)
⟹ Is_Functional (S 𝗌𝗎𝖻𝗃 P) ›
  unfolding Is_Functional_def Premise_def
  by simp

(* ― ‹derived automatically later›
lemma [φreason %φfunctionality]:
  ‹ Functionality T p⇩T
⟹ Functionality U p⇩U
⟹ Functionality (T ∗ U) (λ(x,y). p⇩T x ∧ p⇩U y)›
  unfolding Functionality_def
  by clarsimp blast
*)

lemma [φreason %φfunctionality]:
  ‹ Is_Functional A
⟹ Is_Functional B
⟹ Is_Functional (A * B)›
  unfolding Is_Functional_def set_eq_iff
  by (simp add: set_mult_expn, blast)

lemma [φreason %φfunctionality]:
  ‹ Is_Functional A
⟹ Is_Functional B
⟹ Is_Functional (A 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 B)›
  unfolding Is_Functional_def set_eq_iff REMAINS_def
  by (simp add: set_mult_expn, blast)

lemma [φreason %φfunctionality]:
  ‹ Functionality T p⇩T
⟹ Functionality U p⇩U
⟹ Functionality (T ✼ U) (λ(x,y). p⇩T x ∧ p⇩U y)›
  unfolding Functionality_def φProd'_def
  by clarsimp blast

lemma [φreason %φfunctionality]:
  ‹ (⋀i∈S. Is_Functional (A i))
⟹ Is_Functional (✱i∈S. A i) ›
  unfolding Is_Functional_def Mul_Quant_def atomize_Ball Ball_def
proof clarsimp
  fix x y
  assume prems: ‹∀x. x ∈ S ⟶ (∀xa y. xa ⊨ A x ∧ y ⊨ A x ⟶ xa = y)› (is ?A)
                ‹x ⊨ prod A S› (is ?B)
                ‹y ⊨ prod A S› (is ?C)
     and ‹finite S›
  have ‹?A ∧ ?B ∧ ?C ⟶ x = y›
    by (induct arbitrary: x y rule: finite_induct[OF ‹finite S›]; clarsimp; blast)
  then show ‹x = y›
    using prems by blast
qed


subsection ‹Carrier Set of Separation Algebra›

definition Within_Carrier_Set :: ‹'c::sep_carrier BI ⇒ bool›
  where ‹Within_Carrier_Set A ⟷ (∀v. v ⊨ A ⟶ mul_carrier v)›

definition Carrier_Set :: ‹('c::sep_carrier,'a) φ ⇒ ('a ⇒ bool) ⇒ bool›
  where ‹Carrier_Set T D ⟷ (∀x. D x ⟶ Within_Carrier_Set (x ⦂ T))›

declare [[φreason_default_pattern
      ‹Within_Carrier_Set ?A› ⇒ ‹Within_Carrier_Set ?A› (100)
  and ‹Carrier_Set ?T _› ⇒ ‹Carrier_Set ?T _› (100)
]]

φreasoner_group carrier_set = (100, [10,3000]) for ‹Within_Carrier_Set A›
    ‹Rules reasoning if the given assertion ‹A› with all its concrete objects falls in the carrier set of the separation algebra›
 and carrier_set_cut = (1000, [1000, 1030]) for ‹Within_Carrier_Set A› in carrier_set
    ‹Cutting rules›
 and carrier_set_red = (2500, [2500, 2530]) for ‹Within_Carrier_Set A› in carrier_set and > carrier_set_cut
    ‹Literal Reduction›
 and derived_carrier_set = (50, [50,50]) for (‹Within_Carrier_Set A›, ‹Carrier_Set T D›)
                                          in carrier_set and < carrier_set_cut
    ‹Derived rules›
 and carrier_set_to_within_carrier_set = (10, [10,10]) for (‹Within_Carrier_Set A›, ‹Carrier_Set T D›)
                                                        in carrier_set and < derived_carrier_set
    ‹Turning ‹Within_Carrier_Set (x : T)› to ‹Carrier_Set T D››

subsubsection ‹Extracting Pure Facts›

context begin

private lemma EIF_Within_Carrier_Set:
  ‹ 𝗋EIF (Within_Carrier_Set A) (∀v. v ⊨ A ⟶ mul_carrier v) ›
  unfolding Within_Carrier_Set_def 𝗋EIF_def
  by blast

private lemma ESC_Within_Carrier_Set:
  ‹ 𝗋ESC (∀v. v ⊨ A ⟶ mul_carrier v) (Within_Carrier_Set A) ›
  unfolding Within_Carrier_Set_def 𝗋ESC_def
  by blast

private lemma EIF_Carrier_Set:
  ‹ 𝗋EIF (Carrier_Set T D) (∀x v. D x ∧ v ⊨ (x ⦂ T) ⟶ mul_carrier v) ›
  unfolding Carrier_Set_def Within_Carrier_Set_def 𝗋EIF_def
  by blast

private lemma ESC_Carrier_Set:
  ‹ 𝗋ESC (∀x v. D x ∧ v ⊨ (x ⦂ T) ⟶ mul_carrier v) (Carrier_Set T D) ›
  unfolding Carrier_Set_def Within_Carrier_Set_def 𝗋ESC_def
  by blast

bundle extracting_Carrier_Set_sat =
          EIF_Within_Carrier_Set [φreason %extract_pure_sat]
          ESC_Within_Carrier_Set [φreason %extract_pure_sat]
          EIF_Carrier_Set [φreason %extract_pure_sat]
          ESC_Carrier_Set [φreason %extract_pure_sat]

end


subsubsection ‹Rules for Logical Connectives›

lemma [φreason default %carrier_set_to_within_carrier_set]:
  ‹ Carrier_Set T P
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 P x
⟹ Within_Carrier_Set (x ⦂ T) ›
  unfolding Carrier_Set_def Premise_def
  by blast

lemma [φreason %carrier_set_cut]:
  ‹ Within_Carrier_Set A
⟹ Within_Carrier_Set B
⟹ Within_Carrier_Set (A * B)›
  unfolding Within_Carrier_Set_def
  by (clarsimp simp add: mul_carrier_closed)

text ‹Though the above rule is reasonable enough, it is not reversible, essentially because
  the set of concrete objects satisfying ‹A * B› is far smaller than either of that satisfying ‹A› or ‹B›.›

lemma
  ‹Within_Carrier_Set (A * B) ⟹ Within_Carrier_Set A ∧ Within_Carrier_Set B›
  oops

lemma [φreason %carrier_set_cut]:
  ‹ (⋀i∈I. Within_Carrier_Set (A i))
⟹ Within_Carrier_Set (✱i∈I. A i) ›
  for A :: ‹'i ⇒ 'c :: {sep_algebra,sep_carrier_1} BI›
  unfolding Within_Carrier_Set_def Mul_Quant_def meta_Ball_def Premise_def
proof clarsimp
  fix v
  assume ‹finite I›
  show ‹(⋀x. x ∈ I ⟹ ∀v. v ⊨ A x ⟶ mul_carrier v) ⟹ v ⊨ prod A I ⟹ mul_carrier v›
    by (induct arbitrary: v rule: finite_induct[OF ‹finite I›]; clarsimp; metis mul_carrier_closed)
qed

(*
lemma ― ‹derived automatically later›
  ‹ Carrier_Set T P
⟹ Carrier_Set U Q
⟹ Carrier_Set (T ∗ U) (pred_prod P Q)›
  unfolding Carrier_Set_def Within_Carrier_Set_def
  by (clarsimp simp add: mul_carrier_closed)
*)

lemma [φreason %carrier_set_cut]:
  ‹ Within_Carrier_Set A
⟹ Within_Carrier_Set B
⟹ Within_Carrier_Set (A + B)›
  unfolding Within_Carrier_Set_def
  by clarsimp

lemma ― ‹The above rule is reversible›
  ‹ Within_Carrier_Set (A + B) ⟹ Within_Carrier_Set A ∧ Within_Carrier_Set B ›
  unfolding Within_Carrier_Set_def
  by clarsimp

lemma [φreason %carrier_set_cut]:
  ‹ (⋀x. Within_Carrier_Set (A x))
⟹ Within_Carrier_Set (ExBI A) ›
  unfolding Within_Carrier_Set_def
  by clarsimp

lemma ― ‹The above rule is reversible›
  ‹ Within_Carrier_Set (ExBI A) ⟹ Within_Carrier_Set (A x) ›
  unfolding Within_Carrier_Set_def
  by clarsimp blast

lemma [φreason %carrier_set_cut]:
  ‹ Within_Carrier_Set A
⟹ Within_Carrier_Set B
⟹ Within_Carrier_Set (A ⊓ B)›
  unfolding Within_Carrier_Set_def
  by clarsimp


text ‹The above rule is also not reversible. Essentially the rules for conjunctive connectives are not
  reversible due to the same reason as ‹*›. ›

lemma ‹ Within_Carrier_Set (A ⊓ B) ⟹ Within_Carrier_Set A ∧ Within_Carrier_Set B ›
  oops

lemma [φreason %carrier_set_cut]:
  ‹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 P ⟹ Within_Carrier_Set A)
⟹ Within_Carrier_Set (A 𝗌𝗎𝖻𝗃 P)›
  unfolding Within_Carrier_Set_def
  by clarsimp

lemma [φreason %carrier_set_cut]:
  ‹ Within_Carrier_Set 0 ›
  unfolding Within_Carrier_Set_def
  by simp

lemma [φreason %carrier_set_cut]:
  ‹ Within_Carrier_Set (1 :: 'a::sep_carrier_1 BI) ›
  unfolding Within_Carrier_Set_def
  by simp

paragraph ‹Case Split›

subparagraph ‹Reduction›

lemma [φreason %carrier_set_red]:
  ‹ Within_Carrier_Set (P a)
⟹ Within_Carrier_Set (case_sum P Q (Inl a)) ›
  by simp

lemma [φreason %carrier_set_red]:
  ‹ Within_Carrier_Set (Q b)
⟹ Within_Carrier_Set (case_sum P Q (Inr b)) ›
  by simp

subparagraph ‹Case Split›

lemma [φreason %carrier_set_cut]:
  ‹ (⋀a. 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 x = Inl a ⟹ Within_Carrier_Set (P a))
⟹ (⋀b. 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 x = Inr b ⟹ Within_Carrier_Set (Q b))
⟹ Within_Carrier_Set (case_sum P Q x) ›
  unfolding Premise_def
  by (cases x; clarsimp)

text ‹Also not reversible in non-trivial cases.›

subsubsection ‹Rules for Basic φ-Types›

lemma [φreason 1000]:
  ‹Carrier_Set Itself mul_carrier›
  unfolding Carrier_Set_def Within_Carrier_Set_def
  by simp

lemma [φreason 1000]:
  ‹Carrier_Set (○ :: ('c::sep_carrier_1, unit) φ) (λ_. True)›
  unfolding Carrier_Set_def Within_Carrier_Set_def
  by clarsimp


subsection ‹Separationally Functional› ― ‹A weaker and more general concept›

definition Sep_Functional :: ‹'a::sep_magma BI ⇒ bool›
  where ‹Sep_Functional S ⟷ (∀x y. x ⊨ S ∧ y ⊨ S ∧ x ## y ⟶ x = y) ›

declare [[φreason_default_pattern ‹Sep_Functional ?S› ⇒ ‹Sep_Functional ?S› (100)]]

lemma [φreason no explorative backtrack 1]:
  ‹ Is_Functional S
⟹ Sep_Functional S ›
  unfolding Sep_Functional_def Is_Functional_def
  by simp

lemma [φreason no explorative backtrack 0]:
  ‹ TRACE_FAIL TEXT(‹Fail to show› S ‹is separationally functional›)
⟹ Sep_Functional S›
  unfolding TRACE_FAIL_def
  by blast

lemma [φreason 1200]:
  ‹ Sep_Functional A
⟹ Sep_Functional B
⟹ Sep_Functional (A ⊓ B) ›
  unfolding Sep_Functional_def
  by simp

lemma [φreason 1200]:
  ‹ Sep_Functional A
⟹ Sep_Functional B
⟹ Sep_Functional (A * B)›
  for A :: ‹'a::sep_ab_semigroup BI›
  unfolding Sep_Functional_def
  by (clarsimp; metis sep_disj_commute sep_disj_multD1 sep_disj_multD2)

lemma [φreason 1200]:
  ‹ Sep_Functional (fst x ⦂ T)
⟹ Sep_Functional (snd x ⦂ U)
⟹ Sep_Functional (x ⦂ T ∗ U)›
  for T :: ‹('c::sep_ab_semigroup, 'a) φ›
  unfolding Sep_Functional_def
  by (cases x; clarsimp;
      metis sep_disj_commute sep_disj_multD1 sep_disj_multD2)

(*
lemma [φreason 1200]:
  ‹ (⋀i∈I. Sep_Functional (A i))
⟹ Sep_Functional (✱i∈I. A i) ›
  unfolding Mul_Quant_def atomize_Ball Ball_def
proof clarsimp
  *)



subsection ‹Reflexive Separation›

text ‹\<^prop>‹x ## x› is used to represented ‹x› is in the carrier set in some algebras like permission algebra.›

definition Sep_Reflexive :: ‹'a::sep_magma BI ⇒ bool›
  where ‹Sep_Reflexive S ⟷ (∀u. u ⊨ S ⟶ u ## u) ›

lemma [φreason 1000]:
  ‹ Sep_Reflexive A
⟹ Sep_Reflexive B
⟹ Sep_Reflexive (A * B) ›
  for A :: ‹'a::sep_refl BI›
  unfolding Sep_Reflexive_def
  by (clarsimp simp add: sep_refl_mult_I)

lemma [φreason 1000]:
  ‹ Sep_Reflexive (fst x ⦂ T)
⟹ Sep_Reflexive (snd x ⦂ U)
⟹ Sep_Reflexive (x ⦂ T ∗ U) ›
  for T :: ‹('c::sep_refl, 'a) φ›
  unfolding Sep_Reflexive_def
  by (clarsimp simp add: sep_refl_mult_I)

lemma [φreason 1000]:
  ‹ Sep_Reflexive A
⟹ Sep_Reflexive B
⟹ Sep_Reflexive (A + B) ›
  unfolding Sep_Reflexive_def
  by clarsimp

lemma [φreason 1000]:
  ‹ (⋀x. Sep_Reflexive (A x))
⟹ Sep_Reflexive (ExBI A) ›
  unfolding Sep_Reflexive_def
  by clarsimp

lemma [φreason 1000]:
  ‹ Sep_Reflexive A
⟹ Sep_Reflexive B
⟹ Sep_Reflexive (A ⊓ B) ›
  unfolding Sep_Reflexive_def
  by clarsimp

lemma [φreason 1000]:
  ‹ Sep_Reflexive A
⟹ Sep_Reflexive (A 𝗌𝗎𝖻𝗃 P) ›
  unfolding Sep_Reflexive_def
  by clarsimp


section ‹Specification of Monadic States›

definition StrictState :: "('ret φarg ⇒ rassn)
                          ⇒ (ABNM ⇒ rassn)
                          ⇒ 'ret comp BI"
  where "StrictState T E = BI {s. case s of Success val x ⇒ x ⊨ T val
                                    | Abnormal val x ⇒ x ⊨ E val
                                    | Invalid ⇒ False
                                    | NonTerm ⇒ False
                                    | AssumptionBroken ⇒ False
                  }"

definition LooseState  :: "('ret φarg ⇒ rassn)
                          ⇒ (ABNM ⇒ rassn)
                          ⇒ 'ret comp BI"
  where  "LooseState T E = BI {s. case s of Success val x ⇒ x ⊨ T val
                                    | Abnormal val x ⇒ x ⊨ E val
                                    | Invalid ⇒ False
                                    | NonTerm ⇒ True
                                    | AssumptionBroken ⇒ True
                  }"

lemma StrictState_expn[iff]:
        "Success vs x ⊨ StrictState T E ≡ x ⊨ T vs"
        "Abnormal v x ⊨ StrictState T E ≡ x ⊨ E v"
        "¬ (Invalid ⊨ StrictState T E)"
        "¬ (NonTerm ⊨ StrictState T E)"
        "¬ (AssumptionBroken ⊨ StrictState T E)"
        "¬ Itself Invalid ≤ StrictState T E"
        "¬ Itself NonTerm ≤ StrictState T E"
        "¬ Itself AssumptionBroken ≤ StrictState T E"
  and LooseState_expn[iff]:
        "Success vs x ⊨ LooseState T E ≡ x ⊨ T vs"
        "Abnormal v x ⊨ LooseState T E ≡ x ⊨ E v"
        "¬ (Invalid ⊨ LooseState T E)"
        "(NonTerm ⊨ LooseState T E)"
        "(AssumptionBroken ⊨ LooseState T E)"
        "¬ Itself Invalid ≤ LooseState T E"
        "Itself NonTerm ≤ LooseState T E"
        "Itself AssumptionBroken ≤ LooseState T E"
  by (simp_all add: StrictState_def LooseState_def less_eq_BI_iff)

lemma LooseState_expn' :
    "x ⊨ LooseState T E ⟷ x = NonTerm
                 ∨ x = AssumptionBroken
                 ∨ (∃x' v. x = Success v x' ∧ x' ⊨ T v)
                 ∨ (∃x' v. x = Abnormal v x' ∧ x' ⊨ E v)"
  by (cases x) simp_all

lemma StrictState_elim[elim]:
    "s ⊨ StrictState T E
⟹ (⋀x v. s = Success v x ⟹ x ⊨ T v ⟹ C)
⟹ (⋀x v. s = Abnormal v x ⟹ x ⊨ E v ⟹ C)
⟹ C" by (cases s) auto

lemma StrictState_intro[intro]:
    " x ⊨ T v ⟹ Success v x ⊨ StrictState T E"
    " x ⊨ E a ⟹ Abnormal a x ⊨ StrictState T E"
  by simp_all

lemma LooseState_E[elim]:
    "s ⊨ LooseState T E
⟹ (⋀x v. s = Success v x ⟹ x ⊨ T v ⟹ C)
⟹ (⋀x v. s = Abnormal v x ⟹ x ⊨ E v ⟹ C)
⟹ (s = NonTerm ⟹ C)
⟹ (s = AssumptionBroken ⟹ C)
⟹ C"
  by (cases s) auto

lemma LooseState_I[intro]:
  "x ⊨ T v ⟹ Success v x ⊨ LooseState T E"
  "x ⊨ E a ⟹ Abnormal a x ⊨ LooseState T E"
  "NonTerm ⊨ LooseState T E"
  "AssumptionBroken ⊨ LooseState T E" (*XXXXXXXXX TODO ERR*)
  by simp_all

lemma LooseState_upgrade:
  "s ⊨ LooseState T E ⟹ s ≠ AssumptionBroken ⟹ s ≠ NonTerm ⟹ s ⊨ StrictState T E"
  by (cases s) auto

lemma StrictState_degrade: "s ⊨ StrictState T E ⟹ s ⊨ LooseState T E" by (cases s) auto

lemma LooseState_introByStrict:
  "(s ≠ AssumptionBroken ⟹ s ≠ NonTerm ⟹ s ⊨ StrictState T E) ⟹ s ⊨ LooseState T E"
  by (cases s) auto

lemma StrictState_subset:
  ‹(⋀v. A v ≤ A' v) ⟹ (⋀v. E v ≤ E' v) ⟹ StrictState A E ≤ StrictState A' E'›
  unfolding less_eq_BI_iff StrictState_def by simp

lemma StrictState_subset'[intro]:
  ‹(⋀v. ∀s. s ⊨ A v ⟶ s ⊨ A' v) ⟹ (⋀v. ∀s. s ⊨ E v ⟶ s ⊨ E' v) ⟹ s ⊨ StrictState A E ⟹ s ⊨ StrictState A' E'›
  unfolding StrictState_def by (cases s; simp)

lemma LooseState_subset:
  ‹(⋀v. A v ≤ A' v) ⟹ (⋀v. E v ≤ E' v) ⟹ LooseState A E ≤ LooseState A' E'›
  unfolding less_eq_BI_iff LooseState_def by simp

lemma LooseState_subset'[intro]:
  ‹(⋀v. ∀s. s ⊨ A v ⟶ s ⊨ A' v) ⟹ (⋀v. ∀s. s ⊨ E v ⟶ s ⊨ E' v) ⟹ s ⊨ LooseState A E ⟹ s ⊨ LooseState A' E'›
  unfolding LooseState_def by (cases s; simp)


lemma LooseState_plus[iff]:
(*  ‹LooseState (A + B) E   = LooseState A E + LooseState B E› *)
  ‹LooseState X (λv. EA v + EB v) = LooseState X EA + LooseState X EB›
  unfolding BI_eq_iff LooseState_def by simp_all

lemma StrictState_plus[iff]:
(*  ‹StrictState (A + B) E   = StrictState A E  + StrictState B E› *)
  ‹StrictState X (λv. EA v + EB v) = StrictState X EA + StrictState X EB›
  unfolding BI_eq_iff StrictState_def by simp_all

abbreviation ‹Void ≡ (1::assn)›


section ‹Specification of Fictional Resource›

declare INTERP_SPEC[φexpns]

lemma  INTERP_SPEC_subj[φexpns]:
  ‹ INTERP_SPEC (S 𝗌𝗎𝖻𝗃 P) = (INTERP_SPEC S 𝗌𝗎𝖻𝗃 P) ›
  unfolding INTERP_SPEC_def by (simp add: BI_eq_iff, blast)

lemma  INTERP_SPEC_ex[φexpns]:
  ‹ INTERP_SPEC (ExBI S) = (∃* x. INTERP_SPEC (S x)) ›
  unfolding INTERP_SPEC_def by (simp add: BI_eq_iff, blast)

abbreviation COMMA :: ‹assn ⇒ assn ⇒ assn› ("_❟/ _" [17,16] 16)
  where ‹COMMA ≡ (*)›


section ‹Specification of Computation›

definition φProcedure :: "'ret proc
                        ⇒ assn
                        ⇒ ('ret φarg ⇒ assn)
                        ⇒ (ABNM ⇒ assn)
                        ⇒ bool"
  where "φProcedure f T U E ⟷
    (∀comp R. comp ⊨ INTERP_SPEC (T * R) ⟶
        BI_lift (f comp) ≤ LooseState (λv. INTERP_SPEC (U v * R)) (λv. INTERP_SPEC (E v * R)))"

abbreviation φProcedure_no_exception
  where ‹φProcedure_no_exception f T U ≡ φProcedure f T U 0›

notation (input)
         φProcedure ("𝗉𝗋𝗈𝖼 (2_)/ (0⦃ _/ ⟼ _ ⦄)/ 𝗍𝗁𝗋𝗈𝗐𝗌 (_)/ " [10,2,2,100] 100)
     and φProcedure_no_exception ("𝗉𝗋𝗈𝖼 (2_)/ ⦃ (2_) ⟼/ (2_) ⦄/ " [10,2,2] 100)

notation φProcedure_no_exception
            ("(‹consistent›𝗉𝗋𝗈𝖼 (_)/ 𝗂𝗇𝗉𝗎𝗍 (_)/ 𝗈𝗎𝗍𝗉𝗎𝗍 (_))" [2,2,2] 100)
     and φProcedure
            ("(‹consistent›𝗉𝗋𝗈𝖼 (_)/ 𝗂𝗇𝗉𝗎𝗍 (_)/ 𝗈𝗎𝗍𝗉𝗎𝗍 (_)/ 𝗍𝗁𝗋𝗈𝗐𝗌 (_))" [2,2,2,100] 100)

translations
  "CONST φProcedure p X Y E" <= "CONST φProcedure (_do_block p) X Y E"
  "CONST φProcedure_no_exception p X Y" <= "CONST φProcedure_no_exception (_do_block p) X Y"

lemma φProcedure_alt:
  ‹𝗉𝗋𝗈𝖼 f ⦃ T ⟼ U ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟷ (∀comp r. comp ⊨ INTERP_SPEC (T * Itself r)
        ⟶ BI_lift (f comp) ≤ LooseState (λv. INTERP_SPEC (U v * Itself r)) (λv. INTERP_SPEC (E v * Itself r)))›
  apply rule
  apply ((unfold φProcedure_def)[1], blast)
  unfolding φProcedure_def INTERP_SPEC subset_iff
  apply (clarsimp simp add: less_eq_BI_iff times_set_def split_comp_All INTERP_SPEC_def)
  by fastforce

lemmas φProcedure_I = φProcedure_alt[THEN iffD2]

lemma φProcedure_protect_body:
  ‹ T ≡ T'
⟹ U ≡ U'
⟹ E ≡ E'
⟹ φProcedure f T U E ≡ φProcedure f T' U' E'›
  by simp

subsubsection ‹Syntax›

ML_file ‹library/syntax/procedure.ML›

section ‹View Shift›

definition View_Shift
    :: "assn ⇒ assn ⇒ bool ⇒ bool" ("(2_/ 𝗌𝗁𝗂𝖿𝗍𝗌 _/ 𝗐𝗂𝗍𝗁 _)" [13,13,13] 12)
  where "View_Shift T U P ⟷ (∀x R. x ⊨ INTERP_SPEC (T * R) ⟶ x ⊨ INTERP_SPEC (U * R) ∧ P)"

abbreviation Simple_View_Shift
    :: "assn ⇒ assn ⇒ bool" ("(2_/ 𝗌𝗁𝗂𝖿𝗍𝗌 _)"  [13,13] 12)
  where ‹Simple_View_Shift T U ≡ View_Shift T U True›

declare [[φreason_default_pattern
    ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?Y 𝗐𝗂𝗍𝗁 _› ⇒ ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?Y 𝗐𝗂𝗍𝗁 _› (10)
and ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 _ ⦂ ?U 𝗐𝗂𝗍𝗁 _› ⇒ ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?var_y ⦂ ?U 𝗐𝗂𝗍𝗁 _› (20)
and ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _› ⇒ ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _› (20)
and ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 _ ⦂ ?U 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _› ⇒ ‹?X 𝗌𝗁𝗂𝖿𝗍𝗌 ?var_y ⦂ ?U 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝗐𝗂𝗍𝗁 _› (30)
]]

subsection ‹Basic Rules›

lemma View_Shift_imply_P:
  ‹ X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P1
⟹ (P1 ⟶ P2)
⟹ X 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P2›
  unfolding View_Shift_def
  by blast

lemma view_shift_by_implication[intro?, φreason 10]:
  ‹ A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 B 𝗐𝗂𝗍𝗁 P
⟹ A 𝗌𝗁𝗂𝖿𝗍𝗌 B 𝗐𝗂𝗍𝗁 P›
  unfolding Transformation_def View_Shift_def INTERP_SPEC_def
  by clarsimp blast

lemma view_shift_0[simp]:
  ‹ 0 𝗌𝗁𝗂𝖿𝗍𝗌 X 𝗐𝗂𝗍𝗁 any ›
  by (blast intro: view_shift_by_implication zero_implies_any)

lemma [φreason 2000 for ‹0 𝗌𝗁𝗂𝖿𝗍𝗌 ?X 𝗐𝗂𝗍𝗁 ?P›]:
  ‹ 0 𝗌𝗁𝗂𝖿𝗍𝗌 X 𝗐𝗂𝗍𝗁 False ›
  by simp

lemma view_shift_refl[φreason 2000 for ‹?A 𝗌𝗁𝗂𝖿𝗍𝗌 ?B 𝗐𝗂𝗍𝗁 ?P›]:
  "A 𝗌𝗁𝗂𝖿𝗍𝗌 A"
  by (blast intro: view_shift_by_implication transformation_refl)

lemma [φreason 800 for ‹?x ⦂ ?T 𝗌𝗁𝗂𝖿𝗍𝗌 ?y ⦂ ?T' 𝗐𝗂𝗍𝗁 ?P›]:
  " Object_Equiv T eq
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 eq x y
⟹ x ⦂ T 𝗌𝗁𝗂𝖿𝗍𝗌 y ⦂ T"
  unfolding Object_Equiv_def Premise_def
  by (insert view_shift_by_implication, presburger)

lemma view_shift_union[φreason 800]:
  ‹ A 𝗌𝗁𝗂𝖿𝗍𝗌 X 𝗐𝗂𝗍𝗁 P
⟹ A 𝗌𝗁𝗂𝖿𝗍𝗌 X + Y 𝗐𝗂𝗍𝗁 P›
  ‹ A 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P
⟹ A 𝗌𝗁𝗂𝖿𝗍𝗌 X + Y 𝗐𝗂𝗍𝗁 P›
  by (simp add: View_Shift_def distrib_right)+

lemma φview_shift_trans:
  "A 𝗌𝗁𝗂𝖿𝗍𝗌 B 𝗐𝗂𝗍𝗁 P
    ⟹ (P ⟹ B 𝗌𝗁𝗂𝖿𝗍𝗌 C 𝗐𝗂𝗍𝗁 Q)
    ⟹ A 𝗌𝗁𝗂𝖿𝗍𝗌 C 𝗐𝗂𝗍𝗁 P ∧ Q"
  unfolding View_Shift_def by blast

lemma φframe_view:
  ‹ A 𝗌𝗁𝗂𝖿𝗍𝗌 B 𝗐𝗂𝗍𝗁 P
⟹ A * R 𝗌𝗁𝗂𝖿𝗍𝗌 B * R 𝗐𝗂𝗍𝗁 P›
  unfolding View_Shift_def
  by (metis (no_types, lifting) mult.assoc)

lemma φview_shift_intro_frame:
  "U' 𝗌𝗁𝗂𝖿𝗍𝗌 U 𝗐𝗂𝗍𝗁 P ⟹ U' * R 𝗌𝗁𝗂𝖿𝗍𝗌 U * R 𝗐𝗂𝗍𝗁 P "
  by (simp add: φframe_view)

lemma φview_shift_intro_frame_R:
  "U' 𝗌𝗁𝗂𝖿𝗍𝗌 U 𝗐𝗂𝗍𝗁 P ⟹ R * U' 𝗌𝗁𝗂𝖿𝗍𝗌 R * U 𝗐𝗂𝗍𝗁 P "
  by (metis φframe_view mult.commute)


section ‹Hoare Rules \& SL Rules›

subsection ‹Fundamental Rules›

lemma φSKIP[simp,intro!]: "𝗉𝗋𝗈𝖼 det_lift (Success v) ⦃ T v ⟼ T ⦄"
  unfolding φProcedure_def det_lift_def less_eq_BI_iff by clarsimp

lemma φSEQ:
   "𝗉𝗋𝗈𝖼 f ⦃ A ⟼ B ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ (⋀vs. 𝗉𝗋𝗈𝖼 g vs ⦃ B vs ⟼ C ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E)
⟹ 𝗉𝗋𝗈𝖼 (f ⤜ (λv. g v)) ⦃ A ⟼ C ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E"
  unfolding φProcedure_def bind_def apply (clarsimp simp add: less_eq_BI_iff)
  subgoal for comp R x s
    apply (cases s; clarsimp; cases x; clarsimp; blast) . .

lemma φframe:
  " 𝗉𝗋𝗈𝖼 f ⦃ A ⟼ B ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ 𝗉𝗋𝗈𝖼 f ⦃ A * R ⟼ λret. B ret * R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 (λex. E ex * R) "
  unfolding φProcedure_def less_eq_BI_iff
  apply clarify subgoal premises prems for comp R' s
    using prems(1)[THEN spec[where x=comp], THEN spec[where x=‹R * R'›],
          simplified mult.assoc[symmetric], THEN mp, OF prems(2)] prems(3)
    by blast .

lemma φSatisfiable:
  ‹(Satisfiable X ⟹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E)
⟹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E›
  unfolding φProcedure_def Satisfiable_def
  by (meson INTERP_SPEC sep_conj_expn)


subsubsection ‹View Shift›

lemma φframe_view_right:
  ‹ A 𝗌𝗁𝗂𝖿𝗍𝗌 B 𝗐𝗂𝗍𝗁 P
⟹ A * R 𝗌𝗁𝗂𝖿𝗍𝗌 B * R 𝗐𝗂𝗍𝗁 P›
  unfolding View_Shift_def
  by (metis (no_types, lifting) mult.assoc mult.commute)

lemma φview_trans:
  ‹ A 𝗌𝗁𝗂𝖿𝗍𝗌 B 𝗐𝗂𝗍𝗁 P1
⟹ (P1 ⟹ B 𝗌𝗁𝗂𝖿𝗍𝗌 C 𝗐𝗂𝗍𝗁 P2)
⟹ A 𝗌𝗁𝗂𝖿𝗍𝗌 C 𝗐𝗂𝗍𝗁 P1 ∧ P2›
  unfolding View_Shift_def by blast

lemma φCONSEQ:
   "𝗉𝗋𝗈𝖼 f ⦃ A  ⟼ B  ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ A' 𝗌𝗁𝗂𝖿𝗍𝗌 A 𝗐𝗂𝗍𝗁 Any1
⟹ (⋀ret. B ret 𝗌𝗁𝗂𝖿𝗍𝗌 B' ret 𝗐𝗂𝗍𝗁 Any2)
⟹ (⋀ex.  E ex 𝗌𝗁𝗂𝖿𝗍𝗌 E' ex 𝗐𝗂𝗍𝗁 Any3)
⟹ 𝗉𝗋𝗈𝖼 f ⦃ A' ⟼ B' ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E' "
  unfolding φProcedure_def View_Shift_def less_eq_BI_iff
  by (clarsimp, smt (verit, del_insts) LooseState_expn')

subsection ‹Helper Rules›

lemma φframe0:
  "𝗉𝗋𝗈𝖼 f ⦃ A ⟼ B ⦄ ⟹ 𝗉𝗋𝗈𝖼 f ⦃ A * R ⟼ λret. B ret * R ⦄"
  using φframe[where E=0, simplified, folded zero_fun_def] .

lemma φCONSEQ'E:
   "(⋀v. E v 𝗌𝗁𝗂𝖿𝗍𝗌 E' v 𝗐𝗂𝗍𝗁 P3)
⟹ 𝗉𝗋𝗈𝖼 f ⦃ A  ⟼ B  ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ 𝗉𝗋𝗈𝖼 f ⦃ A ⟼ B ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E' "
  using φCONSEQ view_shift_refl by blast

lemmas φCONSEQ'E0 = φCONSEQ'E[OF view_shift_0, unfolded zero_fun_eta]

subsubsection ‹Case Analysis›

lemma φCASE:
  ‹ 𝗉𝗋𝗈𝖼 f ⦃ A ⟼ C ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ 𝗉𝗋𝗈𝖼 f ⦃ B ⟼ C ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E
⟹ 𝗉𝗋𝗈𝖼 f ⦃ A + B ⟼ C ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E›
  unfolding φProcedure_def
  by(simp add: distrib_right)

lemma φCASE_VS:
  ‹ A 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P1
⟹ B 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P2
⟹ B + A 𝗌𝗁𝗂𝖿𝗍𝗌 Y 𝗐𝗂𝗍𝗁 P2 ∨ P1›
  unfolding View_Shift_def
  by (simp add: distrib_right)

lemma φCASE_IMP:
  ‹ A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P1
⟹ B 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P2
⟹ B + A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P2 ∨ P1›
  unfolding Transformation_def
  by (simp add: distrib_left)


subsubsection ‹Normalization in Precondition›

lemma norm_precond_conj:
  "(𝗉𝗋𝗈𝖼 f ⦃ T 𝗌𝗎𝖻𝗃 P ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E) = (P ⟶ 𝗉𝗋𝗈𝖼 f ⦃ T ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E )"
  unfolding φProcedure_def
  by (simp add: INTERP_SPEC_subj) blast

lemmas norm_precond_conj_metaeq[unfolded atomize_eq[symmetric]] = norm_precond_conj

lemma norm_precond_ex:
  "(𝗉𝗋𝗈𝖼 f ⦃ ExBI X ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E) = (∀x. 𝗉𝗋𝗈𝖼 f ⦃ X x ⟼ Y ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E)"
  unfolding φProcedure_def
  by (simp add: INTERP_SPEC_ex) blast


ML_file ‹library/syntax/syntax0.ML›


section ‹Reasoning Configuration›

subsection ‹Normalization of Assertions›

consts semantic_mode :: mode
       ABNORMAL :: mode

ML ‹
structure Assertion_SS_Abnormal = Simpset (
  val initial_ss = Simpset_Configure.Empty_SS
  val binding = SOME \<^binding>‹assertion_simps_abnormal›
  val comment = "Simp rules normalizing particularly the abnormal spec of a triple."
  val attribute = NONE
  val post_merging = I
)
›

φreasoner_ML assertion_simp_abnormal 1300
  (‹Simplify (assertion_simps ABNORMAL) ?X' ?X›)
  = ‹Phi_Reasoners.wrap (PLPR_Simplifier.simplifier_by_ss' (K Seq.empty) (fn ctxt =>
      Raw_Simplifier.merge_ss (Assertion_SS.get' ctxt, Assertion_SS_Abnormal.get' ctxt)) {fix_vars=false}) o snd›

φreasoner_ML semantic_simps 1200
  (‹Premise semantic_mode _› | ‹Simplify semantic_mode ?X' ?X›
     )
  = ‹Phi_Reasoners.wrap (PLPR_Simplifier.simplifier (K Seq.empty) (fn ctxt =>
        Simplifier.clear_simpset ctxt addsimps @{thms φV_simps φarg.sel φarg.collapse}) {fix_vars=false}) o snd›

lemmas [assertion_simps] =
  φV_simps

end