Theory Syntax

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⇩1; value v⇩2 ⟧ ⟹ value (Pair v⇩1 v⇩2)" |
"value v ⟹ value (Roll v)" |
"value (Hash _)" |
"value (Hashed _ _)"

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

equivariance "value"

lemma value_inv[simp]:
  "¬ value (Let e⇩1 x e⇩2)"
  "¬ value (App v v')"
  "¬ value (Case v v⇩1 v⇩2)"
  "¬ 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⇩1 e⇩2)"
inductive_cases value_Roll_inv[elim]: "value (Roll e)"

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

end