Theory utp_lift

section ‹ Lifting Expressions ›

theory utp_lift
  imports
    utp_alphabet
begin

subsection ‹ Lifting definitions ›

text ‹ We define operators for converting an expression to and from a relational state space
  with the help of alphabet extrusion and restriction. In general throughout Isabelle/UTP
  we adopt the notation $\lceil P \rceil$ with some subscript to denote lifting an expression
  into a larger alphabet, and $\lfloor P \rfloor$ for dropping into a smaller alphabet.

  The following two functions lift and drop an expression, respectively, whose alphabet is 
  @{typ "'α"}, into a product alphabet @{typ "'α × 'β"}. This allows us to deal with expressions
  which refer only to undashed variables, and use the type-system to ensure this. ›

abbreviation lift_pre :: "('a, 'α) uexpr ⇒ ('a, 'α × 'β) uexpr" (‹⌈_⌉<›)
where "⌈P⌉< ≡ P ⊕p fstL"

abbreviation drop_pre :: "('a, 'α × 'β) uexpr ⇒ ('a, 'α) uexpr" (‹⌊_⌋<›)
where "⌊P⌋< ≡ P ↾e fstL"

text ‹ The following two functions lift and drop an expression, respectively, whose alphabet is 
  @{typ "'β"}, into a product alphabet @{typ "'α × 'β"}. This allows us to deal with expressions
  which refer only to dashed variables. ›
  
abbreviation lift_post :: "('a, 'β) uexpr ⇒ ('a, 'α × 'β) uexpr" (‹⌈_⌉>›)
where "⌈P⌉> ≡ P ⊕p sndL"

abbreviation drop_post :: "('a, 'α × 'β) uexpr ⇒ ('a, 'β) uexpr" (‹⌊_⌋>›)
where "⌊P⌋> ≡ P ↾e sndL"
  
subsection ‹ Lifting Laws ›

text ‹ With the help of our alphabet laws, we can prove some intuitive laws about alphabet
  lifting. For example, lifting variables yields an unprimed or primed relational variable
  expression, respectively. ›
  
lemma lift_pre_var [simp]:
  "⌈var x⌉< = $x"
  by (alpha_tac)

lemma lift_post_var [simp]:
  "⌈var x⌉> = $x´"
  by (alpha_tac)

subsection ‹ Substitution Laws ›
    
lemma pre_var_subst [usubst]:
  "σ($x ↦s «v») † ⌈P⌉< = σ † ⌈P⟦«v»/&x⟧⌉<"
  by (pred_simp)
    
subsection ‹ Unrestriction laws ›

text ‹ Crucially, the lifting operators allow us to demonstrate unrestriction properties. For
  example, we can show that no primed variable is restricted in an expression over only the
  first element of the state-space product type. ›
  
lemma unrest_dash_var_pre [unrest]:
  fixes x :: "('a ⟹ 'α)"
  shows "$x´ ♯ ⌈p⌉<"
  by (pred_auto)

end