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))›
    by (simp add: fun_upd_def)
  then show ?case
    using Uni by simp
qed (auto simp: max_list_append cong: map_cong)

end