(* Author: Matthias Brun,   ETH Zürich, 2019 *)
(* Author: Dmitriy Traytel, ETH Zürich, 2019 *)

section ‹Syntax of $\lambda\bullet$›

(*<*)
theory Syntax
  imports Nominal2_Lemmas
begin
(*>*)

typedecl hash
instantiation hash :: pure
begin
definition permute_hash :: "perm → hash → hash" where
  "permute_hash π h = h"
instance proof qed (simp_all add: permute_hash_def)
end

atom_decl var

nominal_datatype "term" =
  Unit |
  Var var |
  Lam x::var t::"term" binds x in t |
  Rec x::var t::"term" binds x in t |
  Inj1 "term" |
  Inj2 "term" |
  Pair "term" "term" |
  Let "term" x::var t::"term" binds x in t |
  App "term" "term" |
  Case "term" "term" "term" |
  Prj1 "term" |
  Prj2 "term" |
  Roll "term" |
  Unroll "term" |
  Auth "term" |
  Unauth "term" |
  Hash hash |
  Hashed hash "term"

atom_decl tvar

nominal_datatype ty =
  One |
  Fun ty ty |
  Sum ty ty |
  Prod ty ty |
  Mu α::tvar τ::ty binds α in τ |
  Alpha tvar |
  AuthT ty

lemma no_tvars_in_term[simp]: "atom (x :: tvar) ♯ (t :: term)"
  by (induct t rule: term.induct) auto

lemma no_vars_in_ty[simp]: "atom (x :: var) ♯ (τ :: ty)"
  by (induct τ rule: ty.induct) auto

inductive "value" :: "term → bool" where
  "value Unit" |
  "value (Var _)" |
  "value (Lam _ _)" |
  "value (Rec _ _)" |
  "value v ==> value (Inj1 v)" |
  "value v ==> value (Inj2 v)" |
  "[ value v₁; value v₂ ] ==> value (Pair v₁ v₂)" |
  "value v ==> value (Roll v)" |
  "value (Hash _)" |
  "value v ==> value (Hashed _ v)"

declare value.intros[simp]
declare value.intros[intro]

equivariance "value"

lemma value_inv[simp]:
  "¬ value (Let e₁ x e₂)"
  "¬ value (App v v')"
  "¬ value (Case v v₁ v₂)"
  "¬ value (Prj1 v)"
  "¬ value (Prj2 v)"
  "¬ value (Unroll v)"
  "¬ value (Auth v)"
  "¬ value (Unauth v)"
  using value.cases by fastforce+

inductive_cases value_Inj1_inv[elim]: "value (Inj1 e)"
inductive_cases value_Inj2_inv[elim]: "value (Inj2 e)"
inductive_cases value_Pair_inv[elim]: "value (Pair e₁ e₂)"
inductive_cases value_Roll_inv[elim]: "value (Roll e)"
inductive_cases value_Hashed_inv[elim]: "value (Hashed h e)"

abbreviation closed :: "term → bool" where
  "closed t ≡ (∀x::var. atom x ♯ t)"

(*<*)
end
(*>*)