# 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))
next
case (Uni p)
have ‹?case = ((∀y. ⟦λm. (y ⨟ E(n := x)) m, F, G⟧ p) = (∀y. ⟦y ⨟ E, F, G⟧ p))›