Theory Expressions

section ‹ Expressions ›

theory Expressions
  imports Variables
  keywords "expr_constructor" "expr_function" :: "thy_decl_block"
begin

subsection ‹ Types and Constructs ›

named_theorems expr_defs and named_expr_defs

text ‹ An expression is represented simply as a function from the state space @{typ "'s"} to
  the return type @{typ "'a"}, which is the simplest shallow model for Isabelle/HOL. 

  The aim of this theory is to provide transparent conversion between this representation 
  and a more intuitive expression syntax. For example, an expression @{term "x + y"} where 
  $x$ and $y$ are both state variables, can be represented by @{term "λ s. get⇘x⇙ s + get⇘y⇙ s"} 
  when both variables are modelled using lenses. Rather than having to write $\lambda$-terms 
  directly, it is more convenient to hide this threading of state behind a parser. We introduce
  the expression bracket syntax, @{text "(_)e"} to support this.
›

type_synonym ('a, 's) expr = "'s ⇒ 'a"

text ‹ The following constructor is used to syntactically mark functions that actually
  denote expressions. It is semantically vacuous. ›

definition SEXP :: "('s ⇒ 'a) ⇒ ('a, 's) expr" ("[_]e") where
[expr_defs]: "SEXP x = x"

lemma SEXP_apply [simp]: "SEXP e s = (e s)" by (simp add: SEXP_def)

lemma SEXP_idem [simp]: "[[e]e]e = [e]e" by (simp add: SEXP_def)

text ‹ We can create the core constructs of a simple expression language as indicated below. ›

abbreviation (input) var :: "('a ⟹ 's) ⇒ ('a, 's) expr" where
"var x ≡ (λ s. get⇘x⇙ s)"

abbreviation (input) lit :: "'a ⇒ ('a, 's) expr" where
"lit k ≡ (λ s. k)"

abbreviation (input) uop :: "('a ⇒ 'b) ⇒ ('a, 's) expr ⇒ ('b, 's) expr" where
"uop f e ≡ (λ s. f (e s))"

abbreviation (input) bop 
  :: "('a ⇒ 'b ⇒ 'c) ⇒ ('a, 's) expr ⇒ ('b, 's) expr ⇒ ('c, 's) expr" where
"bop f e1 e2 ≡ (λ s. f (e1 s) (e2 s))"

definition taut :: "(bool, 's) expr ⇒ bool" where
[expr_defs]: "taut e = (∀ s. e s)"

definition expr_select :: "('a, 's) expr ⇒ ('b ⟹ 'a) ⇒ ('b, 's) expr" where
[expr_defs, code_unfold]: "expr_select e x = (λ s. get⇘x⇙ (e s))"

definition expr_if :: "('a, 's) expr ⇒ (bool, 's) expr ⇒ ('a, 's) expr ⇒ ('a, 's) expr" where
[expr_defs, code_unfold]: "expr_if P b Q = (λ s. if (b s) then P s else Q s)"

subsection ‹ Lifting Parser and Printer ›

text ‹ The lifting parser creates a parser directive that converts an expression to a 
  @{const SEXP} boxed $\lambda$-term that gives it a semantics. A pretty printer converts
  a boxed $\lambda$-term back to an expression. ›

nonterminal sexp

text ‹ We create some syntactic constants and define parse and print translations for them. ›

syntax
  "_sexp_state"      :: "id"
  "_sexp_quote"      :: "logic ⇒ logic" ("'(_')e")
  ― ‹ Convert the expression to a lambda term, but do not box it. ›
  "_sexp_quote_1way" :: "logic ⇒ logic" ("'(_')e")
  "_sexp_lit"        :: "logic ⇒ logic" ("«_»")
  "_sexp_var"        :: "svid ⇒ logic" ("$_" [990] 990)
  "_sexp_evar"       :: "id_position ⇒ logic" ("@_" [999] 999)
  "_sexp_evar"       :: "logic ⇒ logic" ("@'(_')" [999] 999)
  "_sexp_pqt"        :: "logic ⇒ sexp" ("[_]e")
  "_sexp_taut"       :: "logic ⇒ logic" ("`_`")
  "_sexp_select"     :: "logic ⇒ svid ⇒ logic" ("_:_" [1000, 999] 1000)
  "_sexp_if"         :: "logic ⇒ logic ⇒ logic ⇒ logic" ("(3_ ◃ _ ▹/ _)" [52,0,53] 52)

ML_file ‹Lift_Expr.ML›

text ‹ We create a number of attributes for configuring the way the parser works. › 

declare [[pretty_print_exprs=true]]


text ‹ We can toggle pretty printing of $\lambda$ expressions using @{attribute pretty_print_exprs}. ›

declare [[literal_variables=false]]

text ‹ Expressions, of course, can contain variables. However, a variable can denote one of
  three things: (1) a state variable (i.e. a lens); (2) a placeholder for a value (i.e. a
  HOL literal); and (3) a placeholder for another expression. The attribute @{attribute literal_variables}
  selects option (2) as the default behaviour when true, and option (3) when false. ›

expr_constructor expr_select
expr_constructor expr_if

text ‹ Some constants should not be lifted, since they are effectively constructors for expressions.
  The command @{command expr_constructor} allows us to specify such constants to not be lifted.
  This being the case, the arguments are left unlifted, unless included in a list of numbers
  before the constant name. The state is passed as the final argument to expression constructors.
›

parse_translation ‹ 
  [(@{syntax_const "_sexp_state"}, fn ctx => fn term => Syntax.free Lift_Expr.state_id),
   (@{syntax_const "_sexp_quote"}
   , fn ctx => fn terms =>
      case terms of
        [Const (@{const_syntax SEXP}, t) $ e] => Const (@{const_name SEXP}, t) $ e |
        [e] =>
            Syntax.const @{const_name SEXP} $ Lift_Expr.mk_lift_expr ctx dummyT e),
   (@{syntax_const "_sexp_quote_1way"}
   , fn ctx => fn terms =>
      case terms of
        [e] => Lift_Expr.mk_lift_expr ctx dummyT e)]
›

print_translation ‹
  [(@{const_syntax "SEXP"}
   , fn ctx => fn ts =>
     if not (Config.get ctx Lift_Expr.pretty_print_exprs)
     then Term.list_comb (Syntax.const @{syntax_const "_sexp_pqt"}, ts)
     else
     Syntax.const @{syntax_const "_sexp_quote"} 
     $ Lift_Expr.print_expr ctx (betapply ((hd ts), Syntax.const @{syntax_const "_sexp_state"})))]
›

translations
  "_sexp_var x" => "get⇘x⇙ _sexp_state"
  "_sexp_taut p" == "CONST taut (p)e"
  "_sexp_select e x" == "CONST expr_select (e)e x"
  "_sexp_if P b Q" == "CONST expr_if P (b)e Q"
  "_sexp_var (_svid_tuple (_of_svid_list (x +L y)))" <= "_sexp_var (x +L y)"

text ‹ The main directive is the $e$ subscripted brackets, @{term "(e)e"}. This converts the 
  expression $e$ to a boxed $\lambda$ term. Essentially, the behaviour is as follows:

  \begin{enumerate}
    \item a new $\lambda$ abstraction over the state variable $s$ is wrapped around $e$;
    \item every occurrence of a free lens @{term "$x"} in $e$ is replaced by @{term "get⇘x⇙ s"};
    \item every occurrence of an expression variable @{term "e"} is replaced by @{term "e s"};
    \item every occurrence of any other free variable is left unchanged.
  \end{enumerate}

  The pretty printer does this in reverse. ›

text ‹ Below is a grammar category for lifted expressions. ›

nonterminal sexpr

syntax "_sexpr" :: "logic ⇒ sexpr" ("_")

parse_translation ‹
  [(@{syntax_const "_sexpr"}, fn ctx => fn [e] => 
    Syntax.const @{const_name SEXP} 
            $ (lambda (Syntax.free Lift_Expr.state_id) 
                      (Lift_Expr.lift_expr ctx dummyT (Term_Position.strip_positions e))))]
›

subsection ‹ Reasoning ›

lemma expr_eq_iff: "P = Q ⟷ `P = Q`"
  by (simp add: taut_def fun_eq_iff)

lemma refine_iff_implies: "P ≤ Q ⟷ `P ⟶ Q`"
  by (simp add: le_fun_def taut_def)

lemma taut_True [simp]: "`True` = True"
  by (simp add: taut_def)

lemma taut_False [simp]: "`False` = False"
  by (simp add: taut_def)

lemma tautI: "⟦ ⋀ s. P s ⟧ ⟹ taut P"
  by (simp add: taut_def)

named_theorems expr_simps

text ‹ Lemmas to help automation of expression reasoning ›

lemma fst_case_sum [simp]: "fst (case p of Inl x ⇒ (a1 x, a2 x) | Inr x ⇒ (b1 x, b2 x)) = (case p of Inl x ⇒ a1 x | Inr x ⇒ b1 x)"
  by (simp add: sum.case_eq_if)

lemma snd_case_sum [simp]: "snd (case p of Inl x ⇒ (a1 x, a2 x) | Inr x ⇒ (b1 x, b2 x)) = (case p of Inl x ⇒ a2 x | Inr x ⇒ b2 x)"
  by (simp add: sum.case_eq_if)

lemma sum_case_apply [simp]: "(case p of Inl x ⇒ f x | Inr x ⇒ g x) y = (case p of Inl x ⇒ f x y | Inr x ⇒ g x y)"
  by (simp add: sum.case_eq_if)

text ‹ Proof methods for simplifying shallow expressions to HOL terms. The first retains the lens
  structure, and the second removes it when alphabet lenses are present.  ›

method expr_lens_simp uses add = 
  ((simp add: expr_simps)? ― ‹ Perform any possible simplifications retaining the lens structure ›
   ;((simp add: fun_eq_iff prod.case_eq_if expr_defs named_expr_defs lens_defs add)? ; ― ‹ Explode the rest ›
     (simp add: expr_defs named_expr_defs lens_defs add)?))

method expr_simp uses add = (expr_lens_simp add: alpha_splits add)

text ‹ Methods for dealing with tautologies ›

method expr_lens_taut uses add = 
  (rule tautI;
   expr_lens_simp add: add)

method expr_taut uses add = 
  (rule tautI;
   expr_simp add: add; 
   rename_alpha_vars?)

text ‹ A method for simplifying shallow expressions to HOL terms and applying @{method auto} ›

method expr_auto uses add =
  (expr_simp add: add; 
   (auto simp add: alpha_splits lens_defs add)?; 
   (rename_alpha_vars)? ― ‹ Rename any logical variables with v subscripts ›
  )

subsection ‹ Algebraic laws ›

lemma expr_if_idem [simp]: "P ◃ b ▹ P = P"
  by expr_auto

lemma expr_if_sym: "P ◃ b ▹ Q = Q ◃ ¬b ▹ P"
  by expr_auto

lemma expr_if_assoc: "(P ◃ b ▹ Q) ◃ c ▹ R = P ◃ b ∧ c ▹ (Q ◃ c ▹ R)"
  by expr_auto

lemma expr_if_distr: "P ◃ b ▹ (Q ◃ c ▹ R) = (P ◃ b ▹ Q) ◃ c ▹ (P ◃ b ▹ R)"
  by expr_auto

lemma expr_if_true [simp]: "P ◃ True ▹ Q = P"
  by expr_auto

lemma expr_if_false [simp]: "P ◃ False ▹ Q = Q"
  by expr_auto

lemma expr_if_reach [simp]: "P ◃ b ▹ (Q ◃ b ▹ R) = P ◃ b ▹ R"
  by expr_auto

lemma expr_if_disj [simp]: "P ◃ b ▹ (P ◃ c ▹ Q) = P ◃ b ∨ c ▹ Q"
  by expr_auto

lemma SEXP_expr_if: "[expr_if P b Q]e = expr_if P b Q"
  by (simp add: SEXP_def)

end