Theory PhiSem_Base

theory PhiSem_Base
  imports Phi_System.PhiSem_Formalization_Tools
begin

section ‹Semantics Base›

subsection ‹Type Classes for Common Reasoning Strategies›


φtype_def Uninit_Val :: ‹TY ⇒ (VAL, unit) φ› ("⊤[_]")
  where ‹x ⦂ ⊤[TY] ≡ v ⦂ Itself 𝗌𝗎𝖻𝗃 v. v ∈ Well_Type TY›
  deriving Basic
       and Abstract_Domain⇩L

(*
term x

lemma
  ‹∃c. c ∈ Well_Type TY ⟷ TY ≠ 𝗉𝗈𝗂𝗌𝗈𝗇›
*)

(*
definition Atomic_SemTyp :: ‹TY ⇒ bool›
  where ‹Atomic_SemTyp TY ≡ True›

φreasoner_group Atomic_SemTyp = (1000, [1000, 2000]) for ‹Atomic_SemTyp TY›
  ‹testing whether ‹TY› is an aomitc semantic type, i.e., integers, booleans, floats, but except
    arrays and records›

declare [[
  φreason_default_pattern ‹Atomic_SemTyp ?TY› ⇒ ‹Atomic_SemTyp ?TY› (100),
  φdefault_reasoner_group ‹Atomic_SemTyp _› : %Atomic_SemTyp (100)
]]
*)


end