Theory PhiSem_Symbol

theory PhiSem_Symbol
  imports PhiSem_Base
  abbrevs "<symbol>" = "π—Œπ—’π—†π–»π—ˆπ—…"
begin

text β€ΉSemantic symbol type is a literal string which cannot be modified runtime and has fixed range
  during compilation time and runtime. Some languages have such notion in their semantics, like Ruby,
  while such notion can also be used as a pure tool for semantics formalization, for example,
  to model the attributes or the field names of a structure. β€Ί

section β€ΉSemanticsβ€Ί

debt_axiomatization π—Œπ—’π—†π–»π—ˆπ—… :: TY
                and sem_mk_symbol   :: β€Ήsymbol β‡’ VALβ€Ί
                and sem_dest_symbol :: β€ΉVAL β‡’ symbolβ€Ί
where WT_symbol  [simp]: β€ΉWell_Type π—Œπ—’π—†π–»π—ˆπ—… = { sem_mk_symbol sym | sym. True } β€Ί
  and can_eqcmp_aint[simp]: β€ΉCan_EqCompare res (sem_mk_symbol s1) (sem_mk_symbol s2)β€Ί
  and eqcmp_aint[simp]: β€ΉEqCompare (sem_mk_symbol s1) (sem_mk_symbol s2) ⟷ s1 = s2β€Ί
  and  zero_aint[simp]: β€ΉZero π—Œπ—’π—†π–»π—ˆπ—… = Some (sem_mk_symbol SYMBOL(zero))β€Ί

lemma sem_mk_symbol_inj[simp]:
  β€Ήsem_mk_symbol x = sem_mk_symbol y ⟷ x = yβ€Ί
  by (metis eqcmp_aint)

lemma [Ο†reason add]:
  β€Ή Is_Type_Literal π—Œπ—’π—†π–»π—ˆπ—… β€Ί
  unfolding Is_Type_Literal_def ..

lemma has_Zero_π—Œπ—’π—†π–»π—ˆπ—…[simp]:
  β€Ή has_Zero π—Œπ—’π—†π–»π—ˆπ—… β€Ί
  unfolding has_Zero_def
  by simp



section β€ΉΟ†-Typesβ€Ί

Ο†type_def Symbol :: "(VAL, symbol) Ο†"
  where β€Ήs ⦂ Symbol ≑ sem_mk_symbol s ⦂ Itselfβ€Ί
  deriving Basic
       and Abstract_DomainL
       and Functionality
       and β€Ήπ—π—’π—‰π–Ύπ—ˆπ–Ώ Symbol = π—Œπ—’π—†π–»π—ˆπ—…β€Ί
       and β€ΉSemantic_Zero_Val π—Œπ—’π—†π–»π—ˆπ—… Symbol SYMBOL(zero)β€Ί
       and Inhabited
       and Equiv_Class


lemma [Ο†reason 1000]:
  "Ο†Equal Symbol (Ξ»x y. True) (=)"
  unfolding Ο†Equal_def by simp


section β€ΉInstructionsβ€Ί

text β€ΉThere is no semantic instruction to make a symbol, because they are merely literal string
  known during compilation time.β€Ί

lemma [Ο†reason %Ο†synthesis_literal]:
  β€ΉX π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ s ⦂ 𝗏𝖺𝗅[semantic_literal (sem_mk_symbol s)] Symbol π—‹π–Ύπ—†π–Ίπ—‚π—‡π—Œ X @tag synthesisβ€Ί
  for X :: assn
  unfolding Transformation_def semantic_literal_def Action_Tag_def
  by clarsimp

lemma "_intro_symbol_":
  β€ΉS π—π—‹π–Ίπ—‡π—Œπ–Ώπ—ˆπ—‹π—†π—Œ S ❟ s ⦂ 𝗏𝖺𝗅[semantic_literal (sem_mk_symbol s)] Symbolβ€Ί
  unfolding Transformation_def semantic_literal_def
  by clarsimp


Ο†lang_parser literal_symbol (%Ο†parser_unique, %Ο†lang_push_val) ["<string>"]
                            (β€ΉCurrentConstruction programming_mode ?blk ?H ?Sβ€Ί) β€Ή
fn (oprs,(ctxt,sequent)) => Parse.string >> (fn s => fn _ =>
  (oprs, (ctxt, #transformation_rule Phi_Working_Mode.programming
            OF [sequent, Thm.instantiate
                            (TVars.empty, Vars.make [((("s",0),typβ€Ήsymbolβ€Ί),
                                                     Thm.cterm_of ctxt (Phi_Tool_Symbol.mk_symbol s))])
                            @{thm "_intro_symbol_"}])))
β€Ί



end