Theory utp_alphabet

section ‹ Alphabet Manipulation ›

theory utp_alphabet
  imports
    utp_pred utp_usedby
begin

subsection ‹ Preliminaries ›
  
text ‹ Alphabets are simply types that characterise the state-space of an expression. Thus
  the Isabelle type system ensures that predicates cannot refer to variables not in the alphabet
  as this would be a type error. Often one would like to add or remove additional variables, for 
  example if we wish to have a predicate which ranges only a smaller state-space, and then
  lift it into a predicate over a larger one. This is useful, for example, when dealing with
  relations which refer only to undashed variables (conditions) since we can use the type system
  to ensure well-formedness. 

  In this theory we will set up operators for extending and contracting and alphabet. 
  We first set up a theorem attribute for alphabet laws and a tactic. ›
  
named_theorems alpha

method alpha_tac = (simp add: alpha unrest)?

subsection ‹ Alphabet Extrusion ›

text ‹ Alter an alphabet by application of a lens that demonstrates how the smaller alphabet
  ($\beta$) injects into the larger alphabet ($\alpha$). This changes the type of the expression
  so it is parametrised over the large alphabet. We do this by using the lens \emph{get}
  function to extract the smaller state binding, and then apply this to the expression. 

  We call this "extrusion" rather than "extension" because if the extension lens is bijective
  then it does not extend the alphabet. Nevertheless, it does have an effect because the type
  will be different which can be useful when converting predicates with equivalent alphabets. ›

lift_definition aext :: "('a, 'β) uexpr ⇒ ('β, 'α) lens ⇒ ('a, 'α) uexpr" (infixr "⊕p" 95)
is "λ P x b. P (get⇘x⇙ b)" .

update_uexpr_rep_eq_thms

text ‹ Next we prove some of the key laws. Extending an alphabet twice is equivalent to extending
  by the composition of the two lenses. ›
  
lemma aext_twice: "(P ⊕p a) ⊕p b = P ⊕p (a ;L b)"
  by (pred_auto)

text ‹ The bijective @{term "1L"} lens identifies the source and view types. Thus an alphabet
  extension using this has no effect. ›
    
lemma aext_id [simp]: "P ⊕p 1L = P"
  by (pred_auto)

text ‹ Literals do not depend on any variables, and thus applying an alphabet extension only
  alters the predicate's type, and not its valuation .›
    
lemma aext_lit [simp]: "«v» ⊕p a = «v»"
  by (pred_auto)

lemma aext_zero [simp]: "0 ⊕p a = 0"
  by (pred_auto)

lemma aext_one [simp]: "1 ⊕p a = 1"
  by (pred_auto)

lemma aext_numeral [simp]: "numeral n ⊕p a = numeral n"
  by (pred_auto)

lemma aext_true [simp]: "true ⊕p a = true"
  by (pred_auto)

lemma aext_false [simp]: "false ⊕p a = false"
  by (pred_auto)

lemma aext_not [alpha]: "(¬ P) ⊕p x = (¬ (P ⊕p x))"
  by (pred_auto)

lemma aext_and [alpha]: "(P ∧ Q) ⊕p x = (P ⊕p x ∧ Q ⊕p x)"
  by (pred_auto)

lemma aext_or [alpha]: "(P ∨ Q) ⊕p x = (P ⊕p x ∨ Q ⊕p x)"
  by (pred_auto)

lemma aext_imp [alpha]: "(P ⇒ Q) ⊕p x = (P ⊕p x ⇒ Q ⊕p x)"
  by (pred_auto)

lemma aext_iff [alpha]: "(P ⇔ Q) ⊕p x = (P ⊕p x ⇔ Q ⊕p x)"
  by (pred_auto)
    
lemma aext_shAll [alpha]: "(∀ x ∙ P(x)) ⊕p a = (∀ x ∙ P(x) ⊕p a)"
  by (pred_auto)

lemma aext_UINF_ind [alpha]: "(⨅ x ∙ P x) ⊕p a =(⨅ x ∙ (P x ⊕p a))"
  by (pred_auto)

lemma aext_UINF_mem [alpha]: "(⨅ x∈A ∙ P x) ⊕p a =(⨅ x∈A ∙ (P x ⊕p a))"
  by (pred_auto)
    
text ‹ Alphabet extension distributes through the function liftings. ›
    
lemma aext_uop [alpha]: "uop f u ⊕p a = uop f (u ⊕p a)"
  by (pred_auto)

lemma aext_bop [alpha]: "bop f u v ⊕p a = bop f (u ⊕p a) (v ⊕p a)"
  by (pred_auto)

lemma aext_trop [alpha]: "trop f u v w ⊕p a = trop f (u ⊕p a) (v ⊕p a) (w ⊕p a)"
  by (pred_auto)

lemma aext_qtop [alpha]: "qtop f u v w x ⊕p a = qtop f (u ⊕p a) (v ⊕p a) (w ⊕p a) (x ⊕p a)"
  by (pred_auto)

lemma aext_plus [alpha]:
  "(x + y) ⊕p a = (x ⊕p a) + (y ⊕p a)"
  by (pred_auto)

lemma aext_minus [alpha]:
  "(x - y) ⊕p a = (x ⊕p a) - (y ⊕p a)"
  by (pred_auto)

lemma aext_uminus [simp]:
  "(- x) ⊕p a = - (x ⊕p a)"
  by (pred_auto)

lemma aext_times [alpha]:
  "(x * y) ⊕p a = (x ⊕p a) * (y ⊕p a)"
  by (pred_auto)

lemma aext_divide [alpha]:
  "(x / y) ⊕p a = (x ⊕p a) / (y ⊕p a)"
  by (pred_auto)

text ‹ Extending a variable expression over $x$ is equivalent to composing $x$ with the alphabet,
  thus effectively yielding a variable whose source is the large alphabet. ›
    
lemma aext_var [alpha]:
  "var x ⊕p a = var (x ;L a)"
  by (pred_auto)

lemma aext_ulambda [alpha]: "((λ x ∙ P(x)) ⊕p a) = (λ x ∙ P(x) ⊕p a)"
  by (pred_auto)

text ‹ Alphabet extension is monotonic and continuous. ›
    
lemma aext_mono: "P ⊑ Q ⟹ P ⊕p a ⊑ Q ⊕p a"
  by (pred_auto)

lemma aext_cont [alpha]: "vwb_lens a ⟹ (⨅ A) ⊕p a = (⨅ P∈A.  P ⊕p a)"
  by (pred_simp)
   
text ‹ If a variable is unrestricted in a predicate, then the extended variable is unrestricted
  in the predicate with an alphabet extension. ›
    
lemma unrest_aext [unrest]:
  "⟦ mwb_lens a; x ♯ p ⟧ ⟹ unrest (x ;L a) (p ⊕p a)"
  by (transfer, simp add: lens_comp_def)

text ‹ If a given variable (or alphabet) $b$ is independent of the extension lens $a$, that is, it is
  outside the original state-space of $p$, then it follows that once $p$ is extended by $a$ then
  $b$ cannot be restricted. ›
    
lemma unrest_aext_indep [unrest]:
  "a ⨝ b ⟹ b ♯ (p ⊕p a)"
  by pred_auto
    
subsection ‹ Expression Alphabet Restriction ›

text ‹ Restrict an alphabet by application of a lens that demonstrates how the smaller alphabet
  ($\beta$) injects into the larger alphabet ($\alpha$). Unlike extension, this operation
  can lose information if the expressions refers to variables in the larger alphabet. ›

lift_definition arestr :: "('a, 'α) uexpr ⇒ ('β, 'α) lens ⇒ ('a, 'β) uexpr" (infixr "↾e" 90)
is "λ P x b. P (create⇘x⇙ b)" .

update_uexpr_rep_eq_thms

lemma arestr_id [simp]: "P ↾e 1L = P"
  by (pred_auto)

lemma arestr_aext [simp]: "mwb_lens a ⟹ (P ⊕p a) ↾e a = P"
  by (pred_auto)

text ‹ If an expression's alphabet can be divided into two disjoint sections and the expression
  does not depend on the second half then restricting the expression to the first half is
  loss-less. ›

lemma aext_arestr [alpha]:
  assumes "mwb_lens a" "bij_lens (a +L b)" "a ⨝ b" "b ♯ P"
  shows "(P ↾e a) ⊕p a = P"
proof -
  from assms(2) have "1L ⊆L a +L b"
    by (simp add: bij_lens_equiv_id lens_equiv_def)
  with assms(1,3,4) show ?thesis
    apply (auto simp add: id_lens_def lens_plus_def sublens_def lens_comp_def prod.case_eq_if)
    apply (pred_simp)
    apply (metis lens_indep_comm mwb_lens_weak weak_lens.put_get)
    done
qed

text ‹ Alternative formulation of the above law using used-by instead of unrestriction. ›

lemma aext_arestr' [alpha]:
  assumes "a ♮ P"
  shows "(P ↾e a) ⊕p a = P"
  by (rel_simp, metis assms lens_override_def usedBy_uexpr.rep_eq)

lemma arestr_lit [simp]: "«v» ↾e a = «v»"
  by (pred_auto)

lemma arestr_zero [simp]: "0 ↾e a = 0"
  by (pred_auto)

lemma arestr_one [simp]: "1 ↾e a = 1"
  by (pred_auto)

lemma arestr_numeral [simp]: "numeral n ↾e a = numeral n"
  by (pred_auto)

lemma arestr_var [alpha]:
  "var x ↾e a = var (x /L a)"
  by (pred_auto)

lemma arestr_true [simp]: "true ↾e a = true"
  by (pred_auto)

lemma arestr_false [simp]: "false ↾e a = false"
  by (pred_auto)

lemma arestr_not [alpha]: "(¬ P)↾ea = (¬ (P↾ea))"
  by (pred_auto)

lemma arestr_and [alpha]: "(P ∧ Q)↾ex = (P↾ex ∧ Q↾ex)"
  by (pred_auto)

lemma arestr_or [alpha]: "(P ∨ Q)↾ex = (P↾ex ∨ Q↾ex)"
  by (pred_auto)

lemma arestr_imp [alpha]: "(P ⇒ Q)↾ex = (P↾ex ⇒ Q↾ex)"
  by (pred_auto)

subsection ‹ Predicate Alphabet Restriction ›
  
text ‹ In order to restrict the variables of a predicate, we also need to existentially quantify
  away the other variables. We can't do this at the level of expressions, as quantifiers are not
  applicable here. Consequently, we need a specialised version of alphabet restriction for
  predicates. It both restricts the variables using quantification and then removes them
  from the alphabet type using expression restriction. ›

definition upred_ares :: "'α upred ⇒ ('β ⟹ 'α) ⇒ 'β upred" 
where [upred_defs]: "upred_ares P a = (P ↾v a) ↾e a"
    
syntax
  "_upred_ares" :: "logic ⇒ salpha ⇒ logic" (infixl "↾p" 90)

translations
  "_upred_ares P a" == "CONST upred_ares P a"
  
lemma upred_aext_ares [alpha]: 
  "vwb_lens a ⟹ P ⊕p a ↾p a = P"
  by (pred_auto)
    
lemma upred_ares_aext [alpha]:
  "a ♮ P ⟹ (P ↾p a) ⊕p a = P"
  by (pred_auto)

lemma upred_arestr_lit [simp]: "«v» ↾p a = «v»"
  by (pred_auto)

lemma upred_arestr_true [simp]: "true ↾p a = true"
  by (pred_auto)

lemma upred_arestr_false [simp]: "false ↾p a = false"
  by (pred_auto)

lemma upred_arestr_or [alpha]: "(P ∨ Q)↾px = (P↾px ∨ Q↾px)"
  by (pred_auto)
    
subsection ‹ Alphabet Lens Laws ›

lemma alpha_in_var [alpha]: "x ;L fstL = in_var x"
  by (simp add: in_var_def)

lemma alpha_out_var [alpha]: "x ;L sndL = out_var x"
  by (simp add: out_var_def)

lemma in_var_prod_lens [alpha]:
  "wb_lens Y ⟹ in_var x ;L (X ×L Y) = in_var (x ;L X)"
  by (simp add: in_var_def prod_as_plus lens_comp_assoc[THEN sym] fst_lens_plus)

lemma out_var_prod_lens [alpha]:
  "wb_lens X ⟹ out_var x ;L (X ×L Y) = out_var (x ;L Y)"
  apply (simp add: out_var_def prod_as_plus lens_comp_assoc[THEN sym])
  apply (subst snd_lens_plus)
  using comp_wb_lens fst_vwb_lens vwb_lens_wb apply blast
   apply (simp add: alpha_in_var alpha_out_var)
  apply (simp)
  done
  
subsection ‹ Substitution Alphabet Extension ›

text ‹ This allows us to extend the alphabet of a substitution, in a similar way to expressions. ›
  
definition subst_ext :: "'α usubst ⇒ ('α ⟹ 'β) ⇒ 'β usubst" (infix "⊕s" 65) where
[upred_defs]: "σ ⊕s x = (λ s. put⇘x⇙ s (σ (get⇘x⇙ s)))"

lemma id_subst_ext [usubst]:
  "wb_lens x ⟹ id ⊕s x = id"
  by pred_auto

lemma upd_subst_ext [alpha]:
  "vwb_lens x ⟹ σ(y ↦s v) ⊕s x = (σ ⊕s x)(&x:y ↦s v ⊕p x)"
  by pred_auto

lemma apply_subst_ext [alpha]:
  "vwb_lens x ⟹ (σ † e) ⊕p x = (σ ⊕s x) † (e ⊕p x)"
  by (pred_auto)

lemma aext_upred_eq [alpha]:
  "((e =u f) ⊕p a) = ((e ⊕p a) =u (f ⊕p a))"
  by (pred_auto)

lemma subst_aext_comp [usubst]:
  "vwb_lens a ⟹ (σ ⊕s a) ∘ (ρ ⊕s a) = (σ ∘ ρ) ⊕s a"
  by pred_auto
    
subsection ‹ Substitution Alphabet Restriction ›

text ‹ This allows us to reduce the alphabet of a substitution, in a similar way to expressions. ›
  
definition subst_res :: "'α usubst ⇒ ('β ⟹ 'α) ⇒ 'β usubst" (infix "↾s" 65) where
[upred_defs]: "σ ↾s x = (λ s. get⇘x⇙ (σ (create⇘x⇙ s)))"

lemma id_subst_res [usubst]:
  "mwb_lens x ⟹ id ↾s x = id"
  by pred_auto

lemma upd_subst_res [alpha]:
  "mwb_lens x ⟹ σ(&x:y ↦s v) ↾s x = (σ ↾s x)(&y ↦s v ↾e x)"
  by (pred_auto)

lemma subst_ext_res [usubst]:
  "mwb_lens x ⟹ (σ ⊕s x) ↾s x = σ"
  by (pred_auto)

lemma unrest_subst_alpha_ext [unrest]:
  "x ⨝ y ⟹ x ♯ (P ⊕s y)"
  by (pred_simp robust, metis lens_indep_def)
end