Theory Variables

section ‹ Variables as Lenses ›

theory Variables
  imports "Optics.Optics"
begin

text ‹ Here, we implement foundational constructors and syntax translations for state variables,
  using lens manipulations, for use in shallow expressions. ›

subsection ‹ Constructors ›

text ‹ The following bundle allows us to override the colon operator, which we use for variable
  namespaces. ›

bundle Expression_Syntax
begin

no_notation   
  Set.member  (‹'(:')›) and
  Set.member  (‹(‹notation=‹infix :››_/ : _)› [51, 51] 50)

end

unbundle Expression_Syntax

declare fst_vwb_lens [simp] and snd_vwb_lens [simp]

text ‹ Lenses~\cite{Foster2020-IsabelleUTP} can also be used to effectively define sets of variables. Here we define the
  the universal alphabet ($\Sigma$) to be the bijective lens @{term "1⇩_L"}. This characterises
  the whole of the source type, and thus is effectively the set of all alphabet variables. ›

definition univ_var :: "('α ⟹ 'α)" ("❙v") where
[lens_defs]: "univ_var = 1⇩_L"

lemma univ_var_vwb [simp]: "vwb_lens univ_var"
  by (simp add: univ_var_def)

definition univ_alpha :: "'s scene" where
[lens_defs]: "univ_alpha = ⊤⇩_S"

definition emp_alpha :: "'s scene" where
[lens_defs]: "emp_alpha = ⊥⇩_S"

definition var_alpha :: "('a ⟹ 's) ⇒ 's scene" where
[lens_defs]: "var_alpha x = lens_scene x"

definition ns_alpha :: "('b ⟹ 'c) ⇒ ('a ⟹ 'b) ⇒ 'a ⟹ 'c" where
[lens_defs]: "ns_alpha a x = x ;⇩_L a"

definition var_fst :: "('a × 'b ⟹ 's) ⇒ ('a ⟹ 's)" where
[lens_defs]: "var_fst x = fst⇩_L ;⇩_L x" 

definition var_snd :: "('a × 'b ⟹ 's) ⇒ ('b ⟹ 's)" where
[lens_defs]: "var_snd x = snd⇩_L ;⇩_L x" 

definition var_pair :: "('a ⟹ 's) ⇒ ('b ⟹ 's) ⇒ ('a × 'b ⟹ 's)" where
[lens_defs]: "var_pair x y = x +⇩_L y"

abbreviation var_member :: "('a ⟹ 's) ⇒ 's scene ⇒ bool" (infix "∈⇩_v" 50) where
"x ∈⇩_v A ≡ var_alpha x ≤ A"

lemma ns_alpha_weak [simp]: "⟦ weak_lens a; weak_lens x ⟧ ⟹ weak_lens (ns_alpha a x)"
  by (simp add: ns_alpha_def comp_weak_lens)

lemma ns_alpha_mwb [simp]: "⟦ mwb_lens a; mwb_lens x ⟧ ⟹ mwb_lens (ns_alpha a x)"
  by (simp add: ns_alpha_def comp_mwb_lens)

lemma ns_alpha_vwb [simp]: "⟦ vwb_lens a; vwb_lens x ⟧ ⟹ vwb_lens (ns_alpha a x)"
  by (simp add: ns_alpha_def comp_vwb_lens)

lemma ns_alpha_indep_1 [simp]: "a ⨝ b ⟹ ns_alpha a x ⨝ ns_alpha b y"
  by (simp add: lens_indep_left_ext lens_indep_right_ext ns_alpha_def)

lemma ns_alpha_indep_2 [simp]: "a ⨝ y ⟹ ns_alpha a x ⨝ y"
  by (simp add: lens_indep_left_ext ns_alpha_def)

lemma ns_alpha_indep_3 [simp]: "x ⨝ b ⟹ x ⨝ ns_alpha b y"
  by (simp add: lens_indep_sym)

lemma ns_alpha_indep_4 [simp]: "⟦ mwb_lens a; x ⨝ y ⟧ ⟹ ns_alpha a x ⨝ ns_alpha a y"
  by (simp add: ns_alpha_def)

lemma var_fst_mwb [simp]: "mwb_lens x ⟹ mwb_lens (var_fst x)"
  by (simp add: var_fst_def comp_mwb_lens)

lemma var_snd_mwb [simp]: "mwb_lens x ⟹ mwb_lens (var_snd x)"
  by (simp add: var_snd_def comp_mwb_lens)

lemma var_fst_vwb [simp]: "vwb_lens x ⟹ vwb_lens (var_fst x)"
  by (simp add: var_fst_def comp_vwb_lens)

lemma var_snd_vwb [simp]: "vwb_lens x ⟹ vwb_lens (var_snd x)"
  by (simp add: var_snd_def comp_vwb_lens)

lemma var_fst_indep_1 [simp]: "x ⨝ y ⟹ var_fst x ⨝ y"
  by (simp add: var_fst_def lens_indep_left_ext)

lemma var_fst_indep_2 [simp]: "x ⨝ y ⟹ x ⨝ var_fst y"
  by (simp add: var_fst_def lens_indep_right_ext)

lemma var_snd_indep_1 [simp]: "x ⨝ y ⟹ var_snd x ⨝ y"
  by (simp add: var_snd_def lens_indep_left_ext)

lemma var_snd_indep_2 [simp]: "x ⨝ y ⟹ x ⨝ var_snd y"
  by (simp add: var_snd_def lens_indep_right_ext)

lemma mwb_var_pair [simp]: "⟦ mwb_lens x; mwb_lens y; x ⨝ y ⟧ ⟹ mwb_lens (var_pair x y)"
  by (simp add: var_pair_def plus_mwb_lens)

lemma vwb_var_pair [simp]: "⟦ vwb_lens x; vwb_lens y; x ⨝ y ⟧ ⟹ vwb_lens (var_pair x y)"
  by (simp add: var_pair_def)

lemma var_pair_pres_indep [simp]:
  "⟦ x ⨝ y; x ⨝ z ⟧ ⟹ x ⨝ var_pair y z"
  "⟦ x ⨝ y; x ⨝ z ⟧ ⟹ var_pair y z ⨝ x"
  by (simp_all add: var_pair_def lens_indep_sym)

definition res_alpha :: "('a ⟹ 'b) ⇒ ('c ⟹ 'b) ⇒ 'a ⟹ 'c" where
[lens_defs]: "res_alpha x a = x /⇩_L a"

lemma idem_scene_var [simp]:
  "vwb_lens x ⟹ idem_scene (var_alpha x)"
  by (simp add: lens_defs)

lemma var_alpha_combine: "⟦ vwb_lens x; vwb_lens y; x ⨝ y ⟧ ⟹ var_alpha x ⊔⇩_S var_alpha y = var_alpha (x +⇩_L y)"
  by (simp add: lens_plus_scene var_alpha_def)

lemma var_alpha_indep [simp]: 
  assumes "vwb_lens x" "vwb_lens y"
  shows "var_alpha x ⨝⇩_S var_alpha y ⟷ x ⨝ y"
  by (simp add: assms(1) assms(2) lens_indep_scene var_alpha_def)

lemma pre_var_indep_prod [simp]: "x ⨝ a ⟹ ns_alpha fst⇩_L x ⨝ a ×⇩_L b"
  using lens_indep.lens_put_irr2
  by (unfold_locales, force simp add: lens_defs prod.case_eq_if lens_indep_comm)+

lemma post_var_indep_prod [simp]: "x ⨝ b ⟹ ns_alpha snd⇩_L x ⨝ a ×⇩_L b"
  using lens_indep.lens_put_irr2
  by (unfold_locales, force simp add: lens_defs prod.case_eq_if lens_indep_comm)+

lemma lens_indep_impl_scene_indep_var [simp]:
  "(X ⨝ Y) ⟹ var_alpha X ⨝⇩_S var_alpha Y"
  by (simp add: var_alpha_def)

declare lens_scene_override [simp]
declare uminus_scene_twice [simp]

lemma var_alpha_override [simp]: 
  "mwb_lens X ⟹ s⇩₁ ⊕⇩_S s⇩₂ on var_alpha X = s⇩₁ ⊕⇩_L s⇩₂ on X"
  by (simp add: var_alpha_def)

(* Some extra Scene laws; should be moved to Optics at some point *)

lemma var_alpha_indep_compl [simp]: 
  assumes "vwb_lens x" "vwb_lens y"
  shows "var_alpha x ⨝⇩_S - var_alpha y ⟷ x ⊆⇩_L y"
  by (simp add: assms scene_le_iff_indep_inv sublens_iff_subscene var_alpha_def)

lemma var_alpha_subset [simp]:
  assumes "vwb_lens x" "vwb_lens y"
  shows "var_alpha x ≤ var_alpha y ⟷ x ⊆⇩_L y"
  by (simp add: assms(1) assms(2) sublens_iff_subscene var_alpha_def)

subsection ‹ Syntax Translations ›

text ‹ In order to support nice syntax for variables, we here set up some translations. The first
  step is to introduce a collection of non-terminals. ›
  
nonterminal svid and svids and salpha and sframe_enum and sframe

text ‹ These non-terminals correspond to the following syntactic entities. Non-terminal 
  @{typ "svid"} is an atomic variable identifier, and @{typ "svids"} is a list of identifier. 
  @{typ "salpha"} is an alphabet or set of variables. @{typ "sframe"} is a frame. Such sets can 
  be constructed only through lens composition due to typing restrictions. Next we introduce some 
  syntax constructors. ›
   
syntax ― ‹ Identifiers ›
  "_svid"         :: "id_position ⇒ svid" ("_" [999] 999)
  "_svlongid"     :: "longid_position ⇒ svid" ("_" [999] 999)
  ""              :: "svid ⇒ svids" ("_")
  "_svid_list"    :: "svid ⇒ svids ⇒ svids" ("_,/ _")
  "_svid_alpha"   :: "svid" ("❙v")
  "_svid_index"   :: "id_position ⇒ logic ⇒ svid" ("_'(_')" [999] 999)
  "_svid_tuple"   :: "svids ⇒ svid" ("'(_')")
  "_svid_dot"     :: "svid ⇒ svid ⇒ svid" ("_:_" [999,998] 998)
  "_svid_res"     :: "svid ⇒ svid ⇒ svid" ("_↾_" [999,998] 998)
  "_svid_pre"     :: "svid ⇒ svid" ("_⇧^<" [997] 997)
  "_svid_post"    :: "svid ⇒ svid" ("_⇧^>" [997] 997)
  "_svid_fst"     :: "svid ⇒ svid" ("_.1" [997] 997)
  "_svid_snd"     :: "svid ⇒ svid" ("_.2" [997] 997)
  "_mk_svid_list" :: "svids ⇒ logic" ― ‹ Helper function for summing a list of identifiers ›
  "_of_svid_list"   :: "logic ⇒ svids" ― ‹ Reverse of the above ›
  "_svid_view"    :: "logic ⇒ svid" ("𝒱[_]") ― ‹ View of a symmetric lens ›
  "_svid_coview"  :: "logic ⇒ svid" ("𝒞[_]") ― ‹ Coview of a symmetric lens ›
  "_svid_prod"    :: "svid ⇒ svid ⇒ svid" (infixr "×" 85)
  "_svid_pow2"    :: "svid ⇒ svid" ("_⇧²" [999] 999)

text ‹ A variable can be decorated with an ampersand, to indicate it is a predicate variable, with 
  a dollar to indicate its an unprimed relational variable, or a dollar and ``acute'' symbol to 
  indicate its a primed relational variable. Isabelle's parser is extensible so additional
  decorations can be and are added later. ›

syntax ― ‹ Variable sets ›
  "_salphaid"    :: "id_position ⇒ salpha" ("_" [990] 990)
  "_salphavar"   :: "svid ⇒ salpha" ("$_" [990] 990)
  "_salphaparen" :: "salpha ⇒ salpha" ("'(_')")
  "_salphaunion" :: "salpha ⇒ salpha ⇒ salpha" (infixr "∪" 75)
  "_salphainter" :: "salpha ⇒ salpha ⇒ salpha" (infixr "∩" 75)
  "_salphaminus" :: "salpha ⇒ salpha ⇒ salpha" (infixl "-" 65)
  "_salphacompl" :: "salpha ⇒ salpha" ("- _" [81] 80)
  "_salpha_all"  :: "salpha" ("Σ")
  "_salpha_none" :: "salpha" ("∅")
(*  "_salpha_pre"  :: "salpha ⇒ salpha" ("_⇧^<" [989] 989)
  "_salpha_post" :: "salpha ⇒ salpha" ("_⇧^>" [989] 989) *)
  "_salphaset"   :: "svids ⇒ salpha" ("{_}")
  "_sframeid"    :: "id ⇒ sframe" ("_")
  "_sframeset"   :: "svids ⇒ sframe_enum" ("⦃_⦄")
  "_sframeunion" :: "sframe ⇒ sframe ⇒ sframe" (infixr "∪" 75)
  "_sframeinter" :: "sframe ⇒ sframe ⇒ sframe" (infixr "∩" 75)
  "_sframeminus" :: "sframe ⇒ sframe ⇒ sframe" (infixl "-" 65)
  "_sframecompl" :: "sframe ⇒ sframe" ("- _" [81] 80)
  "_sframe_all"  :: "sframe" ("Σ")
  "_sframe_none" :: "sframe" ("∅")
  "_sframe_pre"  :: "sframe ⇒ sframe" ("_⇧^<" [989] 989)
  "_sframe_post" :: "sframe ⇒ sframe" ("_⇧^>" [989] 989)
  "_sframe_enum" :: "sframe_enum ⇒ sframe" ("_")
  "_sframe_alpha" :: "sframe_enum ⇒ salpha" ("_")
  "_salphamk"    :: "logic ⇒ salpha"
  "_mk_alpha_list" :: "svids ⇒ logic"
  "_mk_frame_list" :: "svids ⇒ logic"

text ‹ The terminals of an alphabet are either HOL identifiers or UTP variable identifiers. 
  We support two ways of constructing alphabets; by composition of smaller alphabets using
  a semi-colon or by a set-style construction $\{a,b,c\}$ with a list of UTP variables. ›

syntax ― ‹ Quotations ›
  "_svid_set"    :: "svids ⇒ logic" ("{_}⇩_v")
  "_svid_empty"  :: "logic" ("{}⇩_v")
  "_svar"        :: "svid ⇒ logic" ("'(_')⇩_v")
  
text ‹ For various reasons, the syntax constructors above all yield specific grammar categories and
  will not parser at the HOL top level (basically this is to do with us wanting to reuse the syntax
  for expressions). As a result we provide some quotation constructors above. 

  Next we need to construct the syntax translations rules. Finally, we set up the translations rules. ›

translations
  ― ‹ Identifiers ›
  "_svid x" ⇀ "x"
  "_svlongid x" ⇀ "x"
  "_svid_alpha" ⇌ "CONST univ_var"
  "_svid_tuple xs" ⇀ "_mk_svid_list xs"
  "_svid_dot x y" ⇌ "CONST ns_alpha x y"
  "_svid_index x i" ⇀ "x i"
  "_svid_res x y" ⇌ "x /⇩_L y" 
  "_svid_pre x" ⇌ "_svid_dot fst⇩_L x"
  "_svid_post x" ⇌ "_svid_dot snd⇩_L x"
  "_svid_fst x" ⇌ "CONST var_fst x"
  "_svid_snd x" ⇌ "CONST var_snd x"
  "_svid_prod x y" ⇌ "x ×⇩_L y"
  "_svid_pow2 x" ⇀ "x ×⇩_L x"
  "_mk_svid_list (_svid_list x xs)" ⇀ "CONST var_pair x (_mk_svid_list xs)"
  "_mk_svid_list x" ⇀ "x"
  "_mk_alpha_list (_svid_list x xs)" ⇀ "CONST var_alpha x ⊔⇩_S _mk_alpha_list xs"
  "_mk_alpha_list x" ⇀ "CONST var_alpha x"

  "_svid_view a" => "𝒱⇘a⇙"
  "_svid_coview a" => "𝒞⇘a⇙"

  "_svid_list (_svid_tuple (_of_svid_list (CONST var_pair x y))) (_of_svid_list z)" ↽ "_of_svid_list (CONST var_pair (CONST var_pair x y) z)"
  "_svid_list x (_of_svid_list y)"    ↽ "_of_svid_list (CONST var_pair x y)"
  "x"                                 ↽ "_of_svid_list x"

  "_svid_tuple (_svid_list x y)" ↽ "CONST var_pair x y"
  "_svid_list x ys" ↽ "_svid_list x (_svid_tuple ys)"

  ― ‹ Alphabets ›
  "_salphaparen a" ⇀ "a"
  "_salphaid x" ⇀ "x"
  "_salphaunion x y" ⇀ "x ⊔⇩_S y"
  "_salphainter x y" ⇀ "x ⊓⇩_S y"
  "_salphaminus x y" ⇀ "x - y"
  "_salphacompl x"  ⇀ "- x"
(*  "_salpha_pre A" ⇀ "A ;⇩_S fst⇩_L"
  "_salpha_post A" ⇀ "A ;⇩_S snd⇩_L" *)
(*  "_salphaprod a b" ⇌ "a ×⇩_L b" *)
  "_salphavar x" ⇌ "CONST var_alpha x"
  "_salphaset A" ⇀ "_mk_alpha_list A"  
  "_sframeid A" ⇀ "A"
  "(_svid_list x (_salphamk y))" ↽ "_salphamk (x +⇩_L y)" 
  "x" ↽ "_salphamk x"
  "_salpha_all" ⇌ "CONST univ_alpha"
  "_salpha_none" ⇌ "CONST emp_alpha"

  ― ‹ Quotations ›
  "_svid_set A" ⇀ "_mk_alpha_list A"
  "_svid_empty" ⇀ "0⇩_L"
  "_svar x" ⇀ "x"

text ‹ The translation rules mainly convert syntax into lens constructions, using a mixture
  of lens operators and the bespoke variable definitions. Notably, a colon variable identifier
  qualification becomes a lens composition, and variable sets are constructed using len sum. 
  The translation rules are carefully crafted to ensure both parsing and pretty printing. 

  Finally we create the following useful utility translation function that allows us to construct a 
  UTP variable (lens) type given a return and alphabet type. ›

syntax
  "_uvar_ty"      :: "type ⇒ type ⇒ type"

parse_translation ‹
let
  fun uvar_ty_tr [ty] = Syntax.const @{type_syntax lens} $ ty $ Syntax.const @{type_syntax dummy}
    | uvar_ty_tr ts = raise TERM ("uvar_ty_tr", ts);
in [(@{syntax_const "_uvar_ty"}, K uvar_ty_tr)] end
›

subsection ‹ Simplifications ›

lemma get_pre [simp]: "get⇘(x⇧^<)⇩_v⇙ (s⇩₁, s⇩₂) = get⇘x⇙ s⇩₁"
  by (simp add: lens_defs)

lemma get_post [simp]: "get⇘(x⇧^>)⇩_v⇙ (s⇩₁, s⇩₂) = get⇘x⇙ s⇩₂"
  by (simp add: lens_defs)

lemma get_prod_decomp: "get⇘x⇙ s = (get⇘var_fst x⇙ s, get⇘var_snd x⇙ s)"
  by (simp add: lens_defs)

end