Theory Semantics

section ‹Semantics›

theory Semantics imports Syntax begin

subsection ‹Definition›

type_synonym 'a var_denot = nat  'a
type_synonym 'a fun_denot = nat  'a list  'a
type_synonym 'a pre_denot = nat  'a list  bool

primrec semantics_tm :: 'a var_denot  'a fun_denot  tm  'a (_, _) where
  E, F (#n) = E n
| E, F (f ts) = F f (map E, F ts)

primrec semantics_fm :: 'a var_denot  'a fun_denot  'a pre_denot  fm  bool
  (_, _, _) where
  _, _, _  = False
| E, F, G (P ts) = G P (map E, F ts)
| E, F, G (p  q) = (E, F, G p  E, F, G q)
| E, F, G (p) = (x. x  E, F, G p)

fun sc :: ('a var_denot × 'a fun_denot × 'a pre_denot)  sequent  bool where
  sc (E, F, G) (A, B) = ((p [∈] A. E, F, G p)  (q [∈] B. E, F, G q))

subsection ‹Substitution›

lemma add_env_semantics [simp]: E, F ((t  s) n) = (E, F t  λm. E, F (s m)) n
  by (induct n) simp_all

lemma lift_lemma [simp]: x  E, F (lift_tm t) = E, F t
  by (induct t) (auto cong: map_cong)

lemma sub_tm_semantics [simp]: E, F (sub_tm s t) = λn. E, F (s n), F t
  by (induct t) (auto cong: map_cong)

lemma sub_fm_semantics [simp]: E, F, G (sub_fm s p) = λn. E, F (s n), F, G p
  by (induct p arbitrary: E s) (auto cong: map_cong)

subsection ‹Variables›

lemma upd_vars_tm [simp]: n [∉] vars_tm t  E(n := x), F t = E, F t
  by (induct t) (auto cong: map_cong)

lemma add_upd_commute [simp]: (y  E(n := x)) m = ((y  E)(Suc n := x)) m
  by (induct m) simp_all

lemma upd_vars_fm [simp]: max_list (vars_fm p) < n  E(n := x), F, G p = E, F, G p
proof (induct p arbitrary: E n)
  case (Pre P ts)
  moreover have max_list (concat (map vars_tm ts)) < n
    using Pre.prems max_list_concat by simp
  then have n [∉] concat (map vars_tm ts)
    using max_list_in by blast
  then have t [∈] ts. n [∉] vars_tm t
    by simp
  ultimately show ?case
    using upd_vars_tm by (metis list.map_cong semantics_fm.simps(2))
  case (Uni p)
  have ?case = ((y. λm. (y  E(n := x)) m, F, G p) = (y. y  E, F, G p))
    by (simp add: fun_upd_def)
  then show ?case
    using Uni by simp
qed (auto simp: max_list_append cong: map_cong)