Quelle  utp_lift.thy

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 fst_L"

abbreviation drop_pre :: "('a, 'α × 'β) uexpr ==> ('a, 'α) uexpr" (‹⌊_⌋_<›)
where "⌊P⌋_< ≡ P 🛇_e fst_L"

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 snd_L"

abbreviation drop_post :: "('a, 'α × 'β) uexpr ==> ('a, 'β) uexpr" (‹⌊_⌋_>›)
where "⌊P⌋_> ≡ P 🛇_e snd_L"
  
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