Quelle  utp_expr.thy

section ‹ UTP Expressions ›

theory utp_expr
imports
  utp_var
begin

subsection ‹ Expression type ›
  
purge_notation BNF_Def.convol (‹(‹indent=1 notation=‹mixfix convol››⟨_,/ _⟩)›)

text ‹ Before building the predicate model, we will build a model of expressions that generalise
 alphabetised predicates. Expressions are represented semantically as mapping from
 the alphabet @{typ "'α"} to the expression's type @{typ "'a"}. This general model will allow us to unify
 all constructions under one type. The majority definitions in the file are given using
 the \emph{lifting} package~cite‹"Huffman13"›, which allows us to reuse much of the existing
 library of HOL functions. ›

typedef ('t, 'α) uexpr = "UNIV :: ('α ==> 't) set" ..

setup_lifting type_definition_uexpr
    
notation Rep_uexpr (‹[_]_e›)
notation Abs_uexpr (‹mk_e›)

lemma uexpr_eq_iff:
  "e = f ⟷ (∀ b. [e]_e b = [f]_e b)"
  using Rep_uexpr_inject[of e f, THEN sym] by (auto)

text ‹ The term @{term "[e]_e b"} effectively refers to the semantic interpretation of the expression
 under the state-space valuation (or variables binding) @{term b}. It can be used, in concert
 with the lifting package, to interpret UTP constructs to their HOL equivalents. We create some
 theorem sets to store such transfer theorems. ›
    
named_theorems uexpr_defs and ueval and lit_simps and lit_norm

subsection ‹ Core expression constructs ›
  
text ‹ A variable expression corresponds to the lens $get$ function associated with a variable.
 Specifically, given a lens the expression always returns that portion of the state-space
 referred to by the lens. ›

lift_definition var :: "('t ==> 'α) ==> ('t, 'α) uexpr" is lens_get .

text ‹ A literal is simply a constant function expression, always returning the same value
 for any binding. ›

lift_definition lit :: "'t ==> ('t, 'α) uexpr" (‹«_¬›) is "λ v b. v" .

text ‹ We define lifting for unary, binary, ternary, and quaternary expression constructs, that
 simply take a HOL function with correct number of arguments and apply it function to all possible
 results of the expressions. ›

lift_definition uop :: "('a ==> 'b) ==> ('a, 'α) uexpr ==> ('b, 'α) uexpr"
  is "λ f e b. f (e b)" .
lift_definition bop ::
  "('a ==> 'b ==> 'c) ==> ('a, 'α) uexpr ==> ('b, 'α) uexpr ==> ('c, 'α) uexpr"
  is "λ f u v b. f (u b) (v b)" .
lift_definition trop ::
  "('a ==> 'b ==> 'c ==> 'd) ==> ('a, 'α) uexpr ==> ('b, 'α) uexpr ==> ('c, 'α) uexpr ==> ('d, 'α) uexpr"
  is "λ f u v w b. f (u b) (v b) (w b)" .
lift_definition qtop ::
  "('a ==> 'b ==> 'c ==> 'd ==> 'e) ==>
   ('a, 'α) uexpr ==> ('b, 'α) uexpr ==> ('c, 'α) uexpr ==> ('d, 'α) uexpr ==>
   ('e, 'α) uexpr"
  is "λ f u v w x b. f (u b) (v b) (w b) (x b)" .

text ‹ We also define a UTP expression version of function ($\lambda$) abstraction, that takes
 a function producing an expression and produces an expression producing a function. ›

lift_definition ulambda :: "('a ==> ('b, 'α) uexpr) ==> ('a ==> 'b, 'α) uexpr"
is "λ f A x. f x A" .

text ‹ We set up syntax for the conditional. This is effectively an infix version of
 if-then-else where the condition is in the middle. ›

definition uIf :: "bool ==> 'a ==> 'a ==> 'a" where
[uexpr_defs]: "uIf = If"

abbreviation cond ::
  "('a,'α) uexpr ==> (bool, 'α) uexpr ==> ('a,'α) uexpr ==> ('a,'α) uexpr"
  (‹(3_ ◃ _ ▹/ _)› [52,0,53] 52)
where "P ◃ b ▹ Q ≡ trop uIf b P Q"

text ‹ UTP expression is equality is simply HOL equality lifted using the @{term bop} binary
 expression constructor. ›
    
definition eq_upred :: "('a, 'α) uexpr ==> ('a, 'α) uexpr ==> (bool, 'α) uexpr" (infixl ‹=_u› 50)
where [uexpr_defs]: "eq_upred x y = bop HOL.eq x y"

text ‹ A literal is the expression @{term "«v¬"}, where @{term v} is any HOL term. Actually, the
 literal construct is very versatile and also allows us to refer to HOL variables within UTP
 expressions, and has a variety of other uses. It can therefore also be considered as a kind
 of quotation mechanism.

 We also set up syntax for UTP variable expressions. ›
  
syntax
  "_uuvar" :: "svar ==> logic" (‹_›)

syntax_consts
  "_uuvar" == var

translations
  "_uuvar x" == "CONST var x"
  
text ‹ Since we already have a parser for variables, we can directly reuse it and simply apply
 the @{term var} expression construct to lift the resulting variable to an expression. ›
  
subsection ‹ Type class instantiations ›

text ‹ Isabelle/HOL of course provides a large hierarchy of type classes that provide constructs
 such as numerals and the arithmetic operators. Fortunately we can directly make use of these
 for UTP expressions, and thus we now perform a long list of appropriate instantiations. We
 first lift the core arithemtic constants and operators using a mixture of literals, unary, and binary
 expression constructors. ›
  
instantiation uexpr :: (zero, type) zero
begin
  definition zero_uexpr_def [uexpr_defs]: "0 = lit 0"
instance ..
end

instantiation uexpr :: (one, type) one
begin
  definition one_uexpr_def [uexpr_defs]: "1 = lit 1"
instance ..

end

instantiation uexpr :: (plus, type) plus
begin
  definition plus_uexpr_def [uexpr_defs]: "u + v = bop (+) u v"
instance ..
end

instance uexpr :: (semigroup_add, type) semigroup_add
  by (intro_classes) (simp add: plus_uexpr_def zero_uexpr_def, transfer, simp add: add.assoc)+

text ‹ The following instantiation sets up numerals. This will allow us to have Isabelle number
 representations (i.e. 3,7,42,198 etc.) to UTP expressions directly. ›

instance uexpr :: (numeral, type) numeral
  by (intro_classes, simp add: plus_uexpr_def, transfer, simp add: add.assoc)
     
text ‹ We can also define the order relation on expressions. Now, unlike the previous group and ring
 constructs, the order relations @{term "(≤)"} and @{term "(≤)"} return a @{type bool} type.
 This order is not therefore the lifted order which allows us to compare the valuation of two
 expressions, but rather the order on expressions themselves. Notably, this instantiation will
 later allow us to talk about predicate refinements and complete lattices. ›
     
instantiation uexpr :: (ord, type) ord
begin
  lift_definition less_eq_uexpr :: "('a, 'b) uexpr ==> ('a, 'b) uexpr ==> bool"
  is "λ P Q. (∀ A. P A ≤ Q A)" .
  definition less_uexpr :: "('a, 'b) uexpr ==> ('a, 'b) uexpr ==> bool"
  where [uexpr_defs]: "less_uexpr P Q = (P ≤ Q ∧ ¬ Q ≤ P)"
instance ..
end

text ‹ UTP expressions whose return type is a partial ordered type, are also partially ordered
 as the following instantiation demonstrates. ›
  
instance uexpr :: (order, type) order
proof
  fix x y z :: "('a, 'b) uexpr"
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" by (simp add: less_uexpr_def)
  show "x ≤ x" by (transfer, auto)
  show "x ≤ y ==> y ≤ z ==> x ≤ z"
    by (transfer, blast intro:order.trans)
  show "x ≤ y ==> y ≤ x ==> x = y"
    by (transfer, rule ext, simp add: eq_iff)
qed

      
subsection ‹ Syntax translations ›

text ‹ The follows a large number of translations that lift HOL functions to UTP expressions
 using the various expression constructors defined above. Much of the time we try to keep
 the HOL syntax but add a "u" subscript. ›

text ‹ This operator allows us to get the characteristic set of a type. Essentially this is
 @{term "UNIV"}, but it retains the type syntactically for pretty printing. ›

definition set_of :: "'a itself ==> 'a set" where
[uexpr_defs]: "set_of t = UNIV"
      
text ‹ We add new non-terminals for UTP tuples and maplets. ›
  
nonterminal utuple_args and umaplet and umaplets

syntax ― ‹ Core expression constructs ›
  "_ucoerce"    :: "logic ==> type ==> logic" (infix ‹:_u› 50)
  "_ulambda"    :: "pttrn ==> logic ==> logic" (‹λ _ ∙ _› [0, 10] 10)
  "_ulens_ovrd" :: "logic ==> logic ==> salpha ==> logic" (‹_ ⊕ _ on _› [85, 0, 86] 86)
  "_ulens_get"  :: "logic ==> svar ==> logic" (‹_:_› [900,901] 901)
  "_umem"       :: "('a, 'α) uexpr ==> ('a set, 'α) uexpr ==> (bool, 'α) uexpr" (infix ‹∈_u› 50)

translations
  "λ x ∙ p" == "CONST ulambda (λ x. p)"
  "x :_u 'a" == "x :: ('a, _) uexpr"
  "_ulens_ovrd f g a" => "CONST bop (CONST lens_override a) f g"
  "_ulens_ovrd f g a" <= "CONST bop (λx y. CONST lens_override x1 y1 a) f g"
  "_ulens_get x y" == "CONST uop (CONST lens_get y) x"
  "x ∈_u A" == "CONST bop (∈) x A"

syntax ― ‹ Tuples ›
  "_utuple"     :: "('a, 'α) uexpr ==> utuple_args ==> ('a * 'b, 'α) uexpr" (‹(1'(_,/ _')_u)›)
  "_utuple_arg"  :: "('a, 'α) uexpr ==> utuple_args" (‹_›)
  "_utuple_args" :: "('a, 'α) uexpr => utuple_args ==> utuple_args"     (‹_,/ _›)
  "_uunit"      :: "('a, 'α) uexpr" (‹'(')_u›)
  "_ufst"       :: "('a × 'b, 'α) uexpr ==> ('a, 'α) uexpr" (‹π₁'(_')›)
  "_usnd"       :: "('a × 'b, 'α) uexpr ==> ('b, 'α) uexpr" (‹π₂'(_')›)

translations
  "()_u"      == "«()¬"
  "(x, y)_u"  == "CONST bop (CONST Pair) x y"
  "_utuple x (_utuple_args y z)" == "_utuple x (_utuple_arg (_utuple y z))"
  "π₁(x)"    == "CONST uop CONST fst x"
  "π₂(x)"    == "CONST uop CONST snd x"

syntax ― ‹ Orders ›
  "_uless"      :: "logic ==> logic ==> logic" (infix ‹<\<^sub>u› 50)
  "_uleq"       :: "logic ==> logic ==> logic" (infix ‹≤_u› 50)
  "_ugreat"     :: "logic ==> logic ==> logic" (infix ‹>_u› 50)
  "_ugeq"       :: "logic ==> logic ==> logic" (infix ‹≥_u› 50)

translations
  "x <_u y"   == "CONST bop (<) x y"
  "x ≤_u y"   == "CONST bop (≤) x y"
  "x >_u y"   => "y <_u x"
  "x ≥_u y"   => "y ≤_u x"

subsection ‹ Evaluation laws for expressions ›
  
text ‹ The following laws show how to evaluate the core expressions constructs in terms of which
 the above definitions are defined. Thus, using these theorems together, we can convert any UTP
 expression into a pure HOL expression. All these theorems are marked as \emph{ueval} theorems
 which can be used for evaluation. ›
  
lemma lit_ueval [ueval]: "[«x¬]_eb = x"
  by (transfer, simp)

lemma var_ueval [ueval]: "[var x]_eb = get b"
  by (transfer, simp)

lemma uop_ueval [ueval]: "[uop f x]_eb = f ([x]_eb)"
  by (transfer, simp)

lemma bop_ueval [ueval]: "[bop f x y]_eb = f ([x]_eb) ([y]_eb)"
  by (transfer, simp)

lemma trop_ueval [ueval]: "[trop f x y z]_eb = f ([x]_eb) ([y]_eb) ([z]_eb)"
  by (transfer, simp)

lemma qtop_ueval [ueval]: "[qtop f x y z w]_eb = f ([x]_eb) ([y]_eb) ([z]_eb) ([w]_eb)"
  by (transfer, simp)

subsection ‹ Misc laws ›

text ‹ We also prove a few useful algebraic and expansion laws for expressions. ›
  
lemma uop_const [simp]: "uop id u = u"
  by (transfer, simp)

lemma bop_const_1 [simp]: "bop (λx y. y) u v = v"
  by (transfer, simp)

lemma bop_const_2 [simp]: "bop (λx y. x) u v = u"
  by (transfer, simp)

lemma uexpr_fst [simp]: "π₁((e, f)_u) = e"
  by (transfer, simp)

lemma uexpr_snd [simp]: "π₂((e, f)_u) = f"
  by (transfer, simp)

subsection ‹ Literalise tactics ›

text ‹ The following tactic converts literal HOL expressions to UTP expressions and vice-versa
 via a collection of simplification rules. The two tactics are called "literalise", which
 converts UTP to expressions to HOL expressions -- i.e. it pushes them into literals --
 and unliteralise that reverses this. We collect the equations in a theorem attribute
 called "lit\_simps". ›
        
lemma lit_fun_simps [lit_simps]:
  "«i x y z u¬ = qtop i «x¬ «y¬ «z¬ «u¬"
  "«h x y z¬ = trop h «x¬ «y¬ «z¬"
  "«g x y¬ = bop g «x¬ «y¬"
  "«f x¬ = uop f «x¬"
  by (transfer, simp)+

text ‹ The following two theorems also set up interpretation of numerals, meaning a UTP numeral
 can always be converted to a HOL numeral. ›
    
lemma numeral_uexpr_rep_eq [ueval]: "[numeral x]_e b = numeral x"
  apply (induct x)
    apply (simp add: lit.rep_eq one_uexpr_def)
   apply (simp add: bop.rep_eq numeral_Bit0 plus_uexpr_def)
  apply (simp add: bop.rep_eq lit.rep_eq numeral_code(3) one_uexpr_def plus_uexpr_def)
  done

lemma numeral_uexpr_simp: "numeral x = «numeral x¬"
  by (simp add: uexpr_eq_iff numeral_uexpr_rep_eq lit.rep_eq)

lemma lit_zero [lit_simps]: "«0¬ = 0" by (simp add:uexpr_defs)
lemma lit_one [lit_simps]: "«1¬ = 1" by (simp add: uexpr_defs)
lemma lit_plus [lit_simps]: "«x + y¬ = «x¬ + «y¬" by (simp add: uexpr_defs, transfer, simp)
lemma lit_numeral [lit_simps]: "«numeral n¬ = numeral n" by (simp add: numeral_uexpr_simp)

text ‹ In general unliteralising converts function applications to corresponding expression
 liftings. Since some operators, like + and *, have specific operators we also have to
 use @{thm uexpr_defs} in reverse to correctly interpret these. Moreover, numerals must be handled
 separately by first simplifying them and then converting them into UTP expression numerals;
 hence the following two simplification rules. ›

lemma lit_numeral_1: "uop numeral x = Abs_uexpr (λb. numeral ([x]_e b))"
  by (simp add: uop_def)

lemma lit_numeral_2: "Abs_uexpr (λ b. numeral v) = numeral v"
  by (metis lit.abs_eq lit_numeral)
  
method literalise = (unfold lit_simps[THEN sym])
method unliteralise = (unfold lit_simps uexpr_defs[THEN sym];
                     (unfold lit_numeral_1 ; (unfold uexpr_defs ueval); (unfold lit_numeral_2))?)+
                   
text ‹ The following tactic can be used to evaluate literal expressions. It first literalises UTP
 expressions, that is pushes as many operators into literals as possible. Then it tries to simplify,
 and final unliteralises at the end. ›

method uexpr_simp uses simps = ((literalise)?, simp add: lit_norm simps, (unliteralise)?)

(* Example *)
  
lemma "(1::(int, 'α) uexpr) + «2¬ = 4 ⟷ «3¬ = 4"
  apply (literalise)
  apply (uexpr_simp) oops

end