Theory Rhombus_HOL_Semantics

(* SPDX-License-Identifier: 0BSD *)
(* Original semantic model over the imported Isabelle/HOL-ZF framework. *)

theory Rhombus_HOL_Semantics
  imports "../core/Rhombus_HOL_Kernel"
begin

section ‹Set-theoretic frames›

text ‹The semantic frame uses carrier arguments rather than syntax- or valuation-dependent interpretation fields.›

record frame =
  tyop_denote :: "hname ⇒ ZF list ⇒ ZF"
  const_scheme :: "hname ⇒ htype option"
  const_denote :: "hname ⇒ (hname ⇒ ZF) ⇒ ZF"

definition zfalse :: ZF where "zfalse = Empty"
definition ztrue :: ZF where "ztrue = Singleton Empty"
definition zbool :: ZF where "zbool = Upair zfalse ztrue"

definition zeq :: "ZF ⇒ ZF" where
  "zeq A = Lambda A (λx. Lambda A (λy. if x = y then ztrue else zfalse))"

definition inhabited :: "ZF ⇒ bool" where
  "inhabited A ⟷ (∃x. Elem x A)"

definition frame_wf :: "frame ⇒ bool" where
  "frame_wf F ⟷
    (∀n args. n ≠ NFun ⟶ n ≠ NBool ⟶ list_all inhabited args ⟶
      inhabited (tyop_denote F n args)) ∧
    (∀n generic ρ σ. const_scheme F n = Some generic ⟶
      (∀v. type_var_occurs v generic ⟶ ρ v = σ v) ⟶
      const_denote F n ρ = const_denote F n σ)"

lemma ztrue_neq_zfalse: "ztrue ≠ zfalse"
  by (auto simp: ztrue_def zfalse_def Singleton_def Upair_nonEmpty)

lemma zfalse_in_zbool [simp]: "Elem zfalse zbool"
  by (simp add: zbool_def Upair)

lemma ztrue_in_zbool [simp]: "Elem ztrue zbool"
  by (simp add: zbool_def Upair)

lemma elem_zbool_iff [simp]:
  "Elem z zbool ⟷ z = zfalse ∨ z = ztrue"
  by (simp add: zbool_def Upair)

section ‹Type interpretation›

fun interp_type :: "frame ⇒ (hname ⇒ ZF) ⇒ htype ⇒ ZF" where
  "interp_type F ρ (TyVar n) = ρ n"
| "interp_type F ρ (TyApp n args) =
    (if n = NFun then
       (case map (interp_type F ρ) args of [A, B] ⇒ Fun A B | _ ⇒ zbool)
     else if n = NBool then zbool
     else tyop_denote F n (map (interp_type F ρ) args))"

lemma interp_type_bool_ty [simp]:
  "interp_type F ρ bool_ty = zbool"
  by (simp add: bool_ty_def)

definition subst_valuation ::
  "frame ⇒ (hname ⇒ ZF) ⇒ (hname ⇒ htype option) ⇒ hname ⇒ ZF" where
  "subst_valuation F ρ θ n =
    (case θ n of None ⇒ ρ n | Some ty ⇒ interp_type F ρ ty)"

lemma interp_type_subst:
  "interp_type F ρ (type_subst θ ty) =
    interp_type F (subst_valuation F ρ θ) ty"
proof (induction ty)
  case (TyVar n)
  then show ?case by (simp add: subst_valuation_def split: option.splits)
next
  case (TyApp n args)
  have maps: "map (λx. interp_type F ρ (type_subst θ x)) args =
      map (interp_type F (subst_valuation F ρ θ)) args"
    using TyApp.IH by (intro map_cong) auto
  show ?case
    by (simp only: type_subst.simps interp_type.simps map_map o_def maps; simp)
qed

lemma interp_type_cong_occurs:
  assumes "∀v. type_var_occurs v ty ⟶ ρ v = σ v"
  shows "interp_type F ρ ty = interp_type F σ ty"
  using assms
proof (induction ty)
  case (TyVar n)
  then show ?case by simp
next
  case (TyApp n args)
  have maps: "map (interp_type F ρ) args = map (interp_type F σ) args"
    using TyApp by (intro map_cong) (auto simp: list_ex_iff)
  show ?case by (simp only: interp_type.simps maps)
qed

definition compose_type_subst ::
  "(hname ⇒ htype option) ⇒ (hname ⇒ htype option) ⇒ hname ⇒ htype option" where
  "compose_type_subst outer inner v =
    (case inner v of None ⇒ outer v | Some ty ⇒ Some (type_subst outer ty))"

lemma type_subst_compose:
  "type_subst (compose_type_subst outer inner) ty =
    type_subst outer (type_subst inner ty)"
  by (induction ty)
    (auto simp: compose_type_subst_def split: option.splits)

lemma subst_valuation_compose:
  "subst_valuation F ρ (compose_type_subst outer inner) v =
    subst_valuation F (subst_valuation F ρ outer) inner v"
  by (auto simp: compose_type_subst_def subst_valuation_def interp_type_subst
      split: option.splits)

lemma type_subst_semantic_agree:
  assumes equal: "type_subst θ ty = type_subst σ ty"
    and occurs: "type_var_occurs v ty"
  shows "subst_valuation F ρ θ v = subst_valuation F ρ σ v"
  using equal occurs
proof (induction ty)
  case (TyVar n)
  then show ?case
    by (cases "θ n"; cases "σ n")
      (auto simp: subst_valuation_def)
next
  case (TyApp n args)
  then obtain arg where arg: "arg ∈ set args" "type_var_occurs v arg"
    by (auto simp: list_ex_iff)
  have arg_equal: "type_subst θ arg = type_subst σ arg"
    using TyApp.prems(1) arg(1) by simp
  show ?case using TyApp.IH[OF arg(1) arg_equal arg(2)] .
qed

section ‹Term interpretation›

definition type_valuation_ok :: "(hname ⇒ ZF) ⇒ bool" where
  "type_valuation_ok ρ ⟷ (∀n. inhabited (ρ n))"

datatype equality_instance =
    Equality_Instance htype
  | Ill_Typed_Equality
  | Other_Constant_Type

fun classify_equality_type :: "htype ⇒ equality_instance" where
  "classify_equality_type
      (TyApp NFun [a, TyApp NFun [b, TyApp NBool []]]) =
     (if a = b then Equality_Instance a else Ill_Typed_Equality)"
| "classify_equality_type _ = Other_Constant_Type"

lemma classify_equality_instance:
  "classify_equality_type ty = Equality_Instance a ⟹
    ty = TyApp NFun [a, TyApp NFun [a, TyApp NBool []]]"
  by (induction ty rule: classify_equality_type.induct)
    (auto split: if_splits)

definition const_sem ::
  "frame ⇒ (hname ⇒ ZF) ⇒ hname ⇒ htype ⇒ ZF" where
  "const_sem F ρ n ty =
    (if n = NEq then
       (case classify_equality_type ty of
          Equality_Instance a ⇒ zeq (interp_type F ρ a)
        | Ill_Typed_Equality ⇒ Empty
        | Other_Constant_Type ⇒ Empty)
     else case const_scheme F n of
       None ⇒ Empty
     | Some generic ⇒
         (case type_match generic ty (λ_. None) of
            None ⇒ Empty
          | Some θ ⇒ const_denote F n (subst_valuation F ρ θ)))"

lemma const_sem_non_equality:
  assumes "n ≠ NEq" "const_scheme F n = Some generic"
    "type_match generic ty (λ_. None) = Some θ"
  shows "const_sem F ρ n ty = const_denote F n (subst_valuation F ρ θ)"
  using assms by (simp add: const_sem_def)

lemma equality_match_shape_early:
  assumes "type_match (mk_fun (TyVar NAlpha)
      (mk_fun (TyVar NAlpha) bool_ty)) ty (λ_. None) ≠ None"
  shows "∃a. ty = mk_fun a (mk_fun a bool_ty)"
proof (cases ty)
  case (TyVar n)
  then show ?thesis using assms
    by (simp add: type_match_def mk_fun_def bool_ty_def)
next
  case (TyApp n args)
  have ty_def: "ty = TyApp n args" using TyApp .
  have len: "n = NFun ∧ length args = 2"
    using assms TyApp
    by (auto simp: type_match_def mk_fun_def bool_ty_def split: if_splits)
  obtain a rest where first: "args = a # rest"
    using len by (cases args) auto
  obtain b where args: "args = [a, b]"
    using len first by (cases rest) auto
  have match: "type_match (mk_fun (TyVar NAlpha)
      (mk_fun (TyVar NAlpha) bool_ty)) (TyApp NFun [a, b])
      (λ_. None) ≠ None"
    using assms TyApp len args by simp
  show ?thesis
  proof (cases b)
    case (TyVar bn)
    then show ?thesis using match TyApp len args
      by (auto simp: type_match_def mk_fun_def bool_ty_def
          split: option.splits if_splits)
  next
    case (TyApp m inner)
    have inner_len: "m = NFun ∧ length inner = 2"
      using match TyApp
      by (auto simp: type_match_def mk_fun_def bool_ty_def split: if_splits)
    obtain c rest' where first': "inner = c # rest'"
      using inner_len by (cases inner) auto
    obtain d where inner: "inner = [c, d]"
      using inner_len first' by (cases rest') auto
    show ?thesis using match ty_def len args TyApp inner_len inner
      by (cases d)
         (auto simp: type_match_def mk_fun_def bool_ty_def
           split: htype.splits hname.splits list.splits option.splits if_splits)
  qed
qed

fun nat_lit_denote :: "frame ⇒ (hname ⇒ ZF) ⇒ nat ⇒ ZF" where
  "nat_lit_denote F ρ 0 = const_sem F ρ nat_zero_name nat_aty"
| "nat_lit_denote F ρ (Suc n) =
     app (const_sem F ρ nat_succ_name nat_sty) (nat_lit_denote F ρ n)"

fun eval_term ::
  "frame ⇒ (hname ⇒ ZF) ⇒ ((hname × htype) ⇒ ZF) ⇒ ZF list ⇒ hterm ⇒ ZF" where
  "eval_term F ρ ν env (FVar n ty) = ν (n, ty)"
| "eval_term F ρ ν env (BVar i ty) = (if i < length env then env ! i else Empty)"
| "eval_term F ρ ν env (Const n ty) = const_sem F ρ n ty"
| "eval_term F ρ ν env (NatLit n) = nat_lit_denote F ρ n"
| "eval_term F ρ ν env (Comb f x) =
     app (eval_term F ρ ν env f) (eval_term F ρ ν env x)"
| "eval_term F ρ ν env (Abs aty body) =
     Lambda (interp_type F ρ aty) (λx. eval_term F ρ ν (x # env) body)"

definition free_valuation_ok ::
  "frame ⇒ (hname ⇒ ZF) ⇒ ((hname × htype) ⇒ ZF) ⇒ bool" where
  "free_valuation_ok F ρ ν ⟷
    (∀n ty. Elem (ν (n, ty)) (interp_type F ρ ty))"

definition bound_valuation_ok ::
  "frame ⇒ (hname ⇒ ZF) ⇒ htype list ⇒ ZF list ⇒ bool" where
  "bound_valuation_ok F ρ tys env ⟷
    length tys = length env ∧
    (∀i < length tys. Elem (env ! i) (interp_type F ρ (tys ! i)))"

definition const_interpretation_ok ::
  "frame ⇒ htheory ⇒ (hname ⇒ ZF) ⇒ bool" where
  "const_interpretation_ok F thy ρ ⟷
    (∀n generic σ. type_valuation_ok σ ⟶
      const_tab thy n = Some generic ⟶
      const_scheme F n = Some generic ∧
      Elem (const_denote F n σ) (interp_type F σ generic))"lemma zeq_apply:
  assumes "Elem x A" "Elem y A"
  shows "app (app (zeq A) x) y = (if x = y then ztrue else zfalse)"
  using assms by (simp add: zeq_def Lambda_app)

lemma zeq_in_fun: "Elem (zeq A) (Fun A (Fun A zbool))"
  by (simp add: zeq_def Elem_Lambda_Fun)

lemma app_in_fun:
  assumes "Elem f (Fun A B)" "Elem x A"
  shows "Elem (app f x) B"
proof -
  have pf: "isFun f" using assms(1)
    by (auto simp: Fun_def Sep PFun_def)
  have dom: "Domain f = A" using assms(1)
    by (simp add: Fun_def Sep)
  have "Elem (app f x) (Range f)"
    using assms(2) pf dom fun_value_in_range by simp
  then show ?thesis using Fun_Range[OF assms(1)]
    by (auto simp: subset_def)
qed

lemma interp_type_inhabited_any:
  assumes frame_ok: "frame_wf F" and type_ok: "type_valuation_ok ρ"
  shows "inhabited (interp_type F ρ ty)"
proof (induction ty)
  case (TyVar n)
  then show ?case using type_ok by (simp add: type_valuation_ok_def)
next
  case (TyApp n args)
  let ?vals = "map (interp_type F ρ) args"
  have vals_inh: "list_all inhabited ?vals"
    using TyApp.IH by (auto simp: list_all_iff)
  have bool_inh: "inhabited zbool"
    unfolding inhabited_def using zfalse_in_zbool by blast
  show ?case
  proof (cases "n = NFun")
    case True
    show ?thesis
    proof (cases ?vals)
      case Nil
      then show ?thesis using True bool_inh by simp
    next
      case (Cons A rest)
      have vals1: "?vals = A # rest" using Cons .
      show ?thesis
      proof (cases rest)
        case Nil
        then show ?thesis using True vals1 bool_inh by simp
      next
        case (Cons B tail)
        have rest1: "rest = B # tail" using Cons .
        show ?thesis
        proof (cases tail)
          case Nil
          obtain y where y: "Elem y B"
            using vals_inh vals1 rest1 Nil
            by (auto simp: inhabited_def list_all_iff)
          have fun_member: "Elem (Lambda A (λ_. y)) (Fun A B)"
            using y by (simp add: Elem_Lambda_Fun)
          show ?thesis using True vals1 rest1 Nil fun_member
            by (auto simp: inhabited_def)
        next
          case (Cons C more)
          then show ?thesis using True vals1 rest1 bool_inh by simp
        qed
      qed
    qed  next
    case False
    have not_fun: "n ≠ NFun" using False .
    show ?thesis
    proof (cases "n = NBool")
      case True
      then show ?thesis using not_fun bool_inh by simp
    next
      case False
      then show ?thesis using not_fun frame_ok vals_inh
        by (auto simp: frame_wf_def)
    qed
  qed
qed

lemma subst_valuation_ok:
  assumes frame_ok: "frame_wf F" and type_ok: "type_valuation_ok ρ"
  shows "type_valuation_ok (subst_valuation F ρ θ)"
proof (unfold type_valuation_ok_def, intro allI)
  fix n
  show "inhabited (subst_valuation F ρ θ n)"
  proof (cases "θ n")
    case None
    then show ?thesis using type_ok
      by (simp add: subst_valuation_def type_valuation_ok_def)
  next
    case (Some ty)
    then show ?thesis using interp_type_inhabited_any[OF frame_ok type_ok, of ty]
      by (simp add: subst_valuation_def)
  qed
qed

lemma interp_type_inhabited:
  assumes "wf_theory thy" "frame_wf F" "type_valuation_ok ρ"
    "check_type thy ty"
  shows "inhabited (interp_type F ρ ty)"
  using assms
proof (induction ty)
  case (TyVar n)
  then show ?case by (simp add: type_valuation_ok_def)
next
  case (TyApp n args)
  have arg_inh: "list_all inhabited (map (interp_type F ρ) args)"
    using TyApp.IH TyApp.prems by (auto simp: list_all_iff)
  show ?case
  proof (cases "n = NFun")
    case True
    have len: "length args = 2"
      using True TyApp.prems by (simp add: wf_theory_def)
    obtain a rest where args1: "args = a # rest"
      using len by (cases args) auto
    obtain b where args: "args = [a, b]"
      using len args1 by (cases rest) auto
    obtain y where y: "Elem y (interp_type F ρ b)"
      using arg_inh unfolding args inhabited_def by auto
    have "Elem (Lambda (interp_type F ρ a) (λ_. y))
        (Fun (interp_type F ρ a) (interp_type F ρ b))"
      using y by (simp add: Elem_Lambda_Fun)
    then show ?thesis using True args by (auto simp: inhabited_def)
  next
    case not_fun: False
    show ?thesis
    proof (cases "n = NBool")
      case True
      have "length args = 0"
        using True TyApp.prems by (simp add: wf_theory_def)
      then have args: "args = []" by simp
      have zb: "inhabited zbool"
        unfolding inhabited_def using zfalse_in_zbool by blast
      show ?thesis using True not_fun zb by (simp add: args)
    next
      case False
      then show ?thesis using TyApp.prems not_fun arg_inh
        by (auto simp: frame_wf_def)
    qed
  qed
qed

lemma bound_valuation_cons:
  assumes "bound_valuation_ok F ρ tys env"
    "Elem x (interp_type F ρ ty)"
  shows "bound_valuation_ok F ρ (ty # tys) (x # env)"
  using assms by (auto simp: bound_valuation_ok_def nth_Cons split: nat.splits)

lemma type_of_comb_Some:
  assumes "type_of (Comb f x) = Some r"
  shows "∃d. type_of f = Some (mk_fun d r) ∧ type_of x = Some d"
  using assms
  by (auto simp: mk_fun_def
      split: htype.splits hname.splits option.splits list.splits if_splits)

lemma non_eq_const_sem_type:
  assumes frame_ok: "frame_wf F" and type_ok: "type_valuation_ok ρ"
    and const_ok: "const_interpretation_ok F thy ρ"
    and distinct: "n ≠ NEq"
    and checked: "check_open_term thy env (Const n ty)"
  shows "Elem (const_sem F ρ n ty) (interp_type F ρ ty)"
proof -
  obtain generic where tab: "const_tab thy n = Some generic"
    using checked by (auto split: option.splits)
  obtain θ where match: "type_match generic ty (λ_. None) = Some θ"
    using checked tab by (auto split: option.splits)
  have sigma_ok: "type_valuation_ok (subst_valuation F ρ θ)"
    using subst_valuation_ok[OF frame_ok type_ok] .
  have scheme: "const_scheme F n = Some generic"
    and member: "Elem (const_denote F n (subst_valuation F ρ θ))
      (interp_type F (subst_valuation F ρ θ) generic)"
    using const_ok sigma_ok tab by (auto simp: const_interpretation_ok_def)
  have instantiated: "type_subst θ generic = ty"
    using type_match_sound[OF match] .
  have carrier: "interp_type F (subst_valuation F ρ θ) generic =
      interp_type F ρ ty"
  proof -
    have "interp_type F (subst_valuation F ρ θ) generic =
        interp_type F ρ (type_subst θ generic)"
      using interp_type_subst[of F ρ θ generic] by simp
    then show ?thesis using instantiated by simp
  qed
  show ?thesis using distinct scheme match member carrier
    by (simp add: const_sem_def)
qed

lemma eval_type_sound:
  assumes thy_wf: "wf_theory thy" and frame_ok: "frame_wf F"
    and type_ok: "type_valuation_ok ρ"
    and free_ok: "free_valuation_ok F ρ ν"
    and const_ok: "const_interpretation_ok F thy ρ"
    and bound_ok: "bound_valuation_ok F ρ tys env"
    and checked: "check_open_term thy tys t"
    and typeof: "type_of t = Some ty"
  shows "Elem (eval_term F ρ ν env t) (interp_type F ρ ty)"
  using bound_ok checked typeof
proof (induction t arbitrary: tys env ty)
  case (FVar n u)
  then show ?case using free_ok by (auto simp: free_valuation_ok_def)
next
  case (BVar i u)
  then show ?case by (auto simp: bound_valuation_ok_def)
next
  case (Const n u)
  have result_ty: "u = ty" using Const.prems(3) by simp
  show ?case
  proof (cases "n = NEq")
    case True
    have match: "type_match (mk_fun (TyVar NAlpha)
        (mk_fun (TyVar NAlpha) bool_ty)) u (λ_. None) ≠ None"
      using Const.prems(2) thy_wf True by (simp add: wf_theory_def)
    obtain a where shape: "u = mk_fun a (mk_fun a bool_ty)"
      using equality_match_shape_early[OF match] by blast
    have classified: "classify_equality_type ty = Equality_Instance a"
      using shape result_ty by (simp add: mk_fun_def bool_ty_def)
    have carrier: "interp_type F ρ ty =
        Fun (interp_type F ρ a) (Fun (interp_type F ρ a) zbool)"
      using shape result_ty by (simp add: mk_fun_def bool_ty_def)
    show ?thesis using True result_ty classified carrier
        zeq_in_fun[of "interp_type F ρ a"]
      by (simp add: const_sem_def)
  next
    case False
    obtain generic where tab: "const_tab thy n = Some generic"
      using Const.prems(2) by (auto split: option.splits)
    obtain θ where match: "type_match generic u (λ_. None) = Some θ"
      using Const.prems(2) tab by (auto split: option.splits)
    have sigma_ok: "type_valuation_ok (subst_valuation F ρ θ)"
      using subst_valuation_ok[OF frame_ok type_ok] .
    have scheme: "const_scheme F n = Some generic"
      and member: "Elem (const_denote F n (subst_valuation F ρ θ))
        (interp_type F (subst_valuation F ρ θ) generic)"
      using const_ok sigma_ok tab by (auto simp: const_interpretation_ok_def)    have instantiated: "type_subst θ generic = u"
      using type_match_sound[OF match] .
    have carrier: "interp_type F (subst_valuation F ρ θ) generic =
        interp_type F ρ u"
    proof -
      have "interp_type F (subst_valuation F ρ θ) generic =
          interp_type F ρ (type_subst θ generic)"
        using interp_type_subst[of F ρ θ generic] by simp
      then show ?thesis using instantiated by simp
    qed
    show ?thesis using False result_ty scheme match member carrier
      by (simp add: const_sem_def)
  qed
next
  case (NatLit n)
  have result_ty: "ty = nat_aty" using NatLit.prems(3) by simp
  have zero_checked: "check_open_term thy tys (Const nat_zero_name nat_aty)"
    using NatLit.prems(2) by (simp add: type_match_def nat_aty_def)
  have succ_checked: "check_open_term thy tys (Const nat_succ_name nat_sty)"
    using NatLit.prems(2) thy_wf
    by (simp add: type_match_def nat_aty_def nat_sty_def mk_fun_def wf_theory_def)
  have zero_in: "Elem (const_sem F ρ nat_zero_name nat_aty)
      (interp_type F ρ nat_aty)"
    using non_eq_const_sem_type[OF frame_ok type_ok const_ok,
        of nat_zero_name tys nat_aty] zero_checked
    by (simp add: nat_zero_name_def)
  have succ_in: "Elem (const_sem F ρ nat_succ_name nat_sty)
      (Fun (interp_type F ρ nat_aty) (interp_type F ρ nat_aty))"
    using non_eq_const_sem_type[OF frame_ok type_ok const_ok,
        of nat_succ_name tys nat_sty] succ_checked
    by (simp add: nat_succ_name_def nat_sty_def mk_fun_def)
  show ?case unfolding result_ty
  proof (induction n)
    case 0
    then show ?case using zero_in by simp
  next
    case (Suc n)
    then show ?case using app_in_fun[OF succ_in] by simp
  qed
next
  case (Comb f x)
  obtain d where parts:
      "type_of f = Some (mk_fun d ty)" "type_of x = Some d"
    using type_of_comb_Some[OF Comb.prems(3)] by blast
  have f_checked: "check_open_term thy tys f" and
       x_checked: "check_open_term thy tys x"
    using Comb.prems(2) by auto
  have f_in: "Elem (eval_term F ρ ν env f)
      (Fun (interp_type F ρ d) (interp_type F ρ ty))"
    using Comb.IH(1)[OF Comb.prems(1) f_checked parts(1)]
    by (simp add: mk_fun_def)
  have x_in: "Elem (eval_term F ρ ν env x) (interp_type F ρ d)"
    using Comb.IH(2)[OF Comb.prems(1) x_checked parts(2)] .
  show ?case using app_in_fun[OF f_in x_in] by simp
next
  case (Abs aty body)
  then obtain bty where body_ty: "type_of body = Some bty"
      and result: "ty = mk_fun aty bty"
    by (auto split: option.splits)
  have body_checked: "check_open_term thy (aty # tys) body"
    using Abs.prems by simp
  have body_sem: "∀x. Elem x (interp_type F ρ aty) ⟶
      Elem (eval_term F ρ ν (x # env) body) (interp_type F ρ bty)"
  proof (intro allI impI)
    fix x
    assume x: "Elem x (interp_type F ρ aty)"
    have extended: "bound_valuation_ok F ρ (aty # tys) (x # env)"
      using bound_valuation_cons[OF Abs.prems(1) x] .
    show "Elem (eval_term F ρ ν (x # env) body) (interp_type F ρ bty)"
      using Abs.IH[OF extended body_checked body_ty] .
  qed
  show ?case using body_sem result
    by (simp add: mk_fun_def Elem_Lambda_Fun)
qed

section ‹Semantic substitution›

definition env_agree :: "htype list ⇒ ZF list ⇒ ZF list ⇒ bool" where
  "env_agree tys xs ys ⟷
    length tys ≤ length xs ∧ length tys ≤ length ys ∧
    (∀i < length tys. xs ! i = ys ! i)"

lemma env_agree_cons:
  assumes "env_agree tys xs ys"
  shows "env_agree (ty # tys) (x # xs) (x # ys)"
  using assms by (auto simp: env_agree_def nth_Cons split: nat.splits)

lemma eval_env_cong:
  assumes "check_open_term thy tys t" "env_agree tys xs ys"
  shows "eval_term F ρ ν xs t = eval_term F ρ ν ys t"
  using assms
proof (induction t arbitrary: tys xs ys)
  case (BVar i ty)
  then show ?case by (auto simp: env_agree_def)
next
  case (Comb f x)
  have f: "eval_term F ρ ν xs f = eval_term F ρ ν ys f"
    using Comb.IH(1) Comb.prems by auto
  have x: "eval_term F ρ ν xs x = eval_term F ρ ν ys x"
    using Comb.IH(2) Comb.prems by auto
  show ?case using f x by simp
next
  case (Abs aty body)
  have pointwise: "eval_term F ρ ν (z # xs) body =
      eval_term F ρ ν (z # ys) body" for z
    using Abs.IH env_agree_cons Abs.prems by auto
  show ?case using pointwise by (simp add: Lambda_ext)
qed auto

lemma eval_closed_env:
  assumes "check_term thy t"
  shows "eval_term F ρ ν env t = eval_term F ρ ν [] t"
  using eval_env_cong[of thy "[]" t env "[]" F ρ ν] assms
  by (simp add: check_term_def env_agree_def)

lemma eval_beta_subst_general:
  assumes body: "check_open_term thy (prefix @ [aty]) t"
    and prefix: "length prefix = j" "length vals = j"
    and arg: "check_term thy s"
  shows "eval_term F ρ ν vals (shift (-1) j (subst_at j s t)) =
    eval_term F ρ ν (vals @ [eval_term F ρ ν [] s]) t"
  using body prefix
proof (induction t arbitrary: prefix vals j)
  case (FVar n ty)
  then show ?case by simp
next
  case (BVar i ty)
  have inserted_shift: "shift (int j) 0 s = s"
    using shift_closed[OF arg] .
  have removed_shift: "shift (-1) j s = s"
    using shift_closed[OF arg] .
  show ?case using BVar.prems eval_closed_env[OF arg, of F ρ ν vals]
    by (auto simp: inserted_shift removed_shift nth_append split: if_splits)
next
  case (Const n ty)
  then show ?case by simp
next
  case (NatLit n)
  then show ?case by simp
next
  case (Comb f x)
  have checks: "check_open_term thy (prefix @ [aty]) f"
      "check_open_term thy (prefix @ [aty]) x"
    using Comb.prems(1) by auto
  have f: "eval_term F ρ ν vals (shift (-1) j (subst_at j s f)) =
      eval_term F ρ ν (vals @ [eval_term F ρ ν [] s]) f"
    using Comb.IH(1)[OF checks(1) Comb.prems(2) Comb.prems(3)] .
  have x: "eval_term F ρ ν vals (shift (-1) j (subst_at j s x)) =
      eval_term F ρ ν (vals @ [eval_term F ρ ν [] s]) x"
    using Comb.IH(2)[OF checks(2) Comb.prems(2) Comb.prems(3)] .
  show ?case using f x by simp
next
  case (Abs bty body)
  have checked: "check_open_term thy ((bty # prefix) @ [aty]) body"
    using Abs.prems by simp
  have lengths: "length (bty # prefix) = Suc j" "length (z # vals) = Suc j" for z
    using Abs.prems by simp_all
  have pointwise: "eval_term F ρ ν (z # vals)
      (shift (-1) (Suc j) (subst_at (Suc j) s body)) =
      eval_term F ρ ν ((z # vals) @ [eval_term F ρ ν [] s]) body" for z
    using Abs.IH[OF checked lengths] .
  show ?case using pointwise by (simp add: Lambda_ext)
qed

lemma eval_subst_bvar:
  assumes "check_open_term thy [aty] body" "check_term thy arg"
  shows "eval_term F ρ ν [] (subst_bvar arg body) =
    eval_term F ρ ν [eval_term F ρ ν [] arg] body"
  using eval_beta_subst_general[of thy "[]" aty body 0 "[]" arg F ρ ν]
    assms by (simp add: subst_bvar_def)

lemma eval_abstract_at:
  assumes "j < length env" "env ! j = ν (n, ty)"
  shows "eval_term F ρ ν env (abstract_at j n ty t) =
    eval_term F ρ ν env t"
  using assms
proof (induction t arbitrary: j env)
  case (FVar m u)
  then show ?case by auto
next
  case (BVar i u)
  then show ?case by simp
next
  case (Const m u)
  then show ?case by simp
next
  case (NatLit n)
  then show ?case by simp
next
  case (Comb f x)
  then show ?case by simp
next
  case (Abs aty body)
  have rec: "eval_term F ρ ν (z # env)
      (abstract_at (Suc j) n ty body) =
      eval_term F ρ ν (z # env) body" for z
    using Abs.IH[of "Suc j" "z # env"] Abs.prems
    by (simp add: nth_Cons)
  show ?case using rec by (simp add: Lambda_ext)
qed

lemma eval_abstract_fvar:
  assumes "check_term thy t"
  shows "eval_term F ρ ν [ν (n, ty)] (abstract_fvar n ty t) =
    eval_term F ρ ν [] t"
proof -
  have abstract: "eval_term F ρ ν [ν (n, ty)] (abstract_at 0 n ty t) =
      eval_term F ρ ν [ν (n, ty)] t"
    using eval_abstract_at[of 0 "[ν (n, ty)]" ν n ty F ρ t] by simp
  have closed: "eval_term F ρ ν [ν (n, ty)] t = eval_term F ρ ν [] t"
    using eval_closed_env[OF assms, of F ρ ν "[ν (n, ty)]"] .
  show ?thesis using abstract closed by (simp add: abstract_fvar_def)
qed

definition semantic_fvar_subst ::
  "frame ⇒ (hname ⇒ ZF) ⇒ ((hname × htype) ⇒ ZF) ⇒
    (hterm × (hname × htype)) list ⇒ (hname × htype) ⇒ ZF" where
  "semantic_fvar_subst F ρ ν θ key =
    (case lookup_fvar θ (fst key) (snd key) of
       None ⇒ ν key
     | Some rep ⇒ eval_term F ρ ν [] rep)"

lemma eval_inst_fvar_at:
  assumes "wf_term_subst thy θ"
  shows "eval_term F ρ ν env (inst_fvar_at θ depth t) =
    eval_term F ρ (semantic_fvar_subst F ρ ν θ) env t"
  using assms
proof (induction t arbitrary: depth env)
  case (FVar n ty)
  show ?case
  proof (cases "lookup_fvar θ n ty")
    case None
    then show ?thesis by (simp add: semantic_fvar_subst_def)
  next
    case (Some rep)
    have checked: "check_term thy rep"
      using lookup_fvar_wf[OF FVar.prems Some] by blast
    have "shift (int depth) 0 rep = rep" using shift_closed[OF checked] .
    then show ?thesis using eval_closed_env[OF checked, of F ρ ν env] Some
      by (simp add: semantic_fvar_subst_def)
  qed
next
  case (Abs aty body)
  have rec: "eval_term F ρ ν (z # env)
      (inst_fvar_at θ (Suc depth) body) =
      eval_term F ρ (semantic_fvar_subst F ρ ν θ) (z # env) body" for z
    using Abs.IH Abs.prems by blast
  show ?case using rec by (simp add: Lambda_ext)
qed auto

lemma eval_inst_fvar:
  assumes "wf_term_subst thy θ"
  shows "eval_term F ρ ν [] (inst_fvar θ t) =
    eval_term F ρ (semantic_fvar_subst F ρ ν θ) [] t"
  using eval_inst_fvar_at[OF assms, where F=F and ρ=ρ and ν=ν
      and env="[]" and depth=0 and t=t]
  by (simp add: inst_fvar_def)

section ‹Semantic type instantiation›

lemma equality_match_shape:
  assumes "type_match (mk_fun (TyVar NAlpha)
      (mk_fun (TyVar NAlpha) bool_ty)) ty (λ_. None) ≠ None"
  shows "∃a. ty = mk_fun a (mk_fun a bool_ty)"
proof (cases ty)
  case (TyVar n)
  then show ?thesis using assms
    by (simp add: type_match_def mk_fun_def bool_ty_def)
next
  case (TyApp n args)
  have ty_def: "ty = TyApp n args" using TyApp .
  have len: "n = NFun ∧ length args = 2"
    using assms TyApp
    by (auto simp: type_match_def mk_fun_def bool_ty_def split: if_splits)
  obtain a rest where first: "args = a # rest"
    using len by (cases args) auto
  obtain b where args: "args = [a, b]"
    using len first by (cases rest) auto
  have match: "type_match (mk_fun (TyVar NAlpha)
      (mk_fun (TyVar NAlpha) bool_ty)) (TyApp NFun [a, b])
      (λ_. None) ≠ None"
    using assms TyApp len args by simp
  show ?thesis
  proof (cases b)
    case (TyVar bn)
    then show ?thesis using match TyApp len args
      by (auto simp: type_match_def mk_fun_def bool_ty_def
          split: option.splits if_splits)
  next
    case (TyApp m inner)
    have inner_len: "m = NFun ∧ length inner = 2"
      using match TyApp
      by (auto simp: type_match_def mk_fun_def bool_ty_def split: if_splits)
    obtain c rest' where first': "inner = c # rest'"
      using inner_len by (cases inner) auto
    obtain d where inner: "inner = [c, d]"
      using inner_len first' by (cases rest') auto
    show ?thesis using match ty_def len args TyApp inner_len inner
      by (cases d)
         (auto simp: type_match_def mk_fun_def bool_ty_def
           split: htype.splits hname.splits list.splits option.splits if_splits)
  qed
qed

definition semantic_type_fvars ::
  "(hname ⇒ htype option) ⇒ ((hname × htype) ⇒ ZF) ⇒
    (hname × htype) ⇒ ZF" where
  "semantic_type_fvars θ ν key = ν (fst key, type_subst θ (snd key))"

lemma const_sem_type_subst:
  assumes thy_wf: "wf_theory thy" and frame_ok: "frame_wf F"
    and subst_ok: "type_subst_ok thy outer"
    and const_ok: "const_interpretation_ok F thy ρ"
    and checked: "check_open_term thy [] (Const n ty)"
  shows "const_sem F ρ n (type_subst outer ty) =
    const_sem F (subst_valuation F ρ outer) n ty"
proof (cases "n = NEq")
  case True
  have match: "type_match (mk_fun (TyVar NAlpha)
      (mk_fun (TyVar NAlpha) bool_ty)) ty (λ_. None) ≠ None"
    using checked thy_wf True by (simp add: wf_theory_def)
  obtain a where shape: "ty = mk_fun a (mk_fun a bool_ty)"
    using equality_match_shape[OF match] by blast
  show ?thesis using True shape
    by (simp add: const_sem_def mk_fun_def bool_ty_def interp_type_subst)
next
  case False
  obtain generic where tab: "const_tab thy n = Some generic"
    using checked by (auto split: option.splits)
  obtain inner where inner_match:
      "type_match generic ty (λ_. None) = Some inner"
    using checked tab by (auto split: option.splits)
  have inst_checked: "check_open_term thy []
      (Const n (type_subst outer ty))"
    using subst_ok checked by (auto simp: type_subst_ok_def)
  obtain combined where combined_match:
      "type_match generic (type_subst outer ty) (λ_. None) = Some combined"
    using inst_checked tab by (auto split: option.splits)
  have trivial_ok: "type_valuation_ok (λ_. zbool)"
    by (auto simp: type_valuation_ok_def inhabited_def)
  have scheme: "const_scheme F n = Some generic"
    using const_ok trivial_ok tab by (auto simp: const_interpretation_ok_def)  have inner_eq: "type_subst inner generic = ty"
    using type_match_sound[OF inner_match] .
  have combined_eq: "type_subst combined generic = type_subst outer ty"
    using type_match_sound[OF combined_match] .
  have composed_eq: "type_subst (compose_type_subst outer inner) generic =
      type_subst outer ty"
    using inner_eq by (simp add: type_subst_compose)
  have valuations_agree: "∀v. type_var_occurs v generic ⟶
      subst_valuation F ρ combined v =
      subst_valuation F ρ (compose_type_subst outer inner) v"
    using type_subst_semantic_agree[OF trans[OF combined_eq sym[OF composed_eq]]]
    by blast
  have denotation_eq: "const_denote F n (subst_valuation F ρ combined) =
      const_denote F n (subst_valuation F ρ (compose_type_subst outer inner))"
    using frame_ok scheme valuations_agree by (auto simp: frame_wf_def)
  have compose_val: "subst_valuation F ρ (compose_type_subst outer inner) =
      subst_valuation F (subst_valuation F ρ outer) inner"
    by (rule ext, rule subst_valuation_compose)
  show ?thesis using False scheme inner_match combined_match denotation_eq compose_val
    by (simp add: const_sem_def)
qed

lemma nat_lit_denote_type_subst:
  assumes thy_wf: "wf_theory thy" and frame_ok: "frame_wf F"
    and subst_ok: "type_subst_ok thy θ"
    and const_ok: "const_interpretation_ok F thy ρ"
    and checked: "check_open_term thy envty (NatLit n)"
  shows "nat_lit_denote F ρ n =
    nat_lit_denote F (subst_valuation F ρ θ) n"
proof -
  have zero_checked: "check_open_term thy [] (Const nat_zero_name nat_aty)"
    using checked by (simp add: type_match_def nat_aty_def)
  have succ_checked: "check_open_term thy [] (Const nat_succ_name nat_sty)"
    using checked thy_wf
    by (simp add: type_match_def nat_aty_def nat_sty_def mk_fun_def wf_theory_def)
  have zero_eq: "const_sem F ρ nat_zero_name nat_aty =
      const_sem F (subst_valuation F ρ θ) nat_zero_name nat_aty"
    using const_sem_type_subst[OF thy_wf frame_ok subst_ok const_ok zero_checked]
    by simp
  have succ_eq: "const_sem F ρ nat_succ_name nat_sty =
      const_sem F (subst_valuation F ρ θ) nat_succ_name nat_sty"
    using const_sem_type_subst[OF thy_wf frame_ok subst_ok const_ok succ_checked]
    by (simp add: nat_sty_def mk_fun_def)
  show ?thesis
  proof (induction n)
    case 0
    then show ?case using zero_eq by simp
  next
    case (Suc n)
    then show ?case using succ_eq by simp
  qed
qed

lemma eval_inst_type:
  assumes thy_wf: "wf_theory thy" and frame_ok: "frame_wf F"
    and subst_ok: "type_subst_ok thy θ"
    and const_ok: "const_interpretation_ok F thy ρ"
    and checked: "check_open_term thy envty t"
  shows "eval_term F ρ ν env (inst_type θ t) =
    eval_term F (subst_valuation F ρ θ) (semantic_type_fvars θ ν) env t"
  using checked
proof (induction t arbitrary: envty env)
  case (FVar n ty)
  then show ?case by (simp add: semantic_type_fvars_def)
next
  case (BVar i ty)
  then show ?case by simp
next
  case (Const n ty)
  have closed: "check_open_term thy [] (Const n ty)"
    using Const.prems by simp
  show ?case using const_sem_type_subst[OF thy_wf frame_ok subst_ok const_ok closed]
    by simp
next
  case (NatLit n)
  show ?case using nat_lit_denote_type_subst[OF thy_wf frame_ok subst_ok const_ok NatLit.prems]
    by simp
next
  case (Comb f x)
  have checks: "check_open_term thy envty f" "check_open_term thy envty x"
    using Comb.prems by auto
  have f: "eval_term F ρ ν env (inst_type θ f) =
      eval_term F (subst_valuation F ρ θ) (semantic_type_fvars θ ν) env f"
    using Comb.IH(1)[OF checks(1)] .
  have x: "eval_term F ρ ν env (inst_type θ x) =
      eval_term F (subst_valuation F ρ θ) (semantic_type_fvars θ ν) env x"
    using Comb.IH(2)[OF checks(2)] .
  show ?case using f x by simp
next
  case (Abs aty body)
  have body_checked: "check_open_term thy (aty # envty) body"
    using Abs.prems by simp
  have pointwise: "eval_term F ρ ν (z # env) (inst_type θ body) =
      eval_term F (subst_valuation F ρ θ) (semantic_type_fvars θ ν)
        (z # env) body" for z
    using Abs.IH[OF body_checked] .
  show ?case using pointwise interp_type_subst[of F ρ θ aty]
    by (simp add: Lambda_ext)
qed

section ‹Valuation transport›

lemma free_valuation_update:
  assumes "free_valuation_ok F ρ ν" "Elem z (interp_type F ρ ty)"
  shows "free_valuation_ok F ρ (ν((n, ty) := z))"
  using assms
  by (auto simp: free_valuation_ok_def)

lemma eval_not_vfree_update:
  assumes "¬ vfree_in n ty t"
  shows "eval_term F ρ (ν((n, ty) := z)) env t = eval_term F ρ ν env t"
  using assms
proof (induction t arbitrary: env)
  case (FVar m u)
  then show ?case by (cases "m = n"; cases "u = ty"; simp)
next
  case (BVar i u)
  then show ?case by simp
next
  case (Const m u)
  then show ?case by simp
next
  case (NatLit k)
  then show ?case by simp
next
  case (Comb f x)
  then show ?case by simp
next
  case (Abs aty body)
  have body_free: "¬ vfree_in n ty body" using Abs.prems by simp
  have pointwise: "eval_term F ρ (ν((n, ty) := z)) (x # env) body =
      eval_term F ρ ν (x # env) body" for x
    using Abs.IH[OF body_free, of "x # env"] .
  show ?case
  proof (simp only: eval_term.simps Lambda_ext, intro conjI allI impI)
    show "interp_type F ρ aty = interp_type F ρ aty" by simp
  next
    fix x
    assume "Elem x (interp_type F ρ aty)"
    show "eval_term F ρ (ν((n, ty) := z)) (x # env) body =
      eval_term F ρ ν (x # env) body" using pointwise .
  qed
qed

lemma semantic_fvar_subst_ok:
  assumes thy_wf: "wf_theory thy" and frame_ok: "frame_wf F"
    and type_ok: "type_valuation_ok ρ"
    and free_ok: "free_valuation_ok F ρ ν"
    and const_ok: "const_interpretation_ok F thy ρ"
    and subst_ok: "wf_term_subst thy θ"
  shows "free_valuation_ok F ρ (semantic_fvar_subst F ρ ν θ)"
proof (unfold free_valuation_ok_def, intro allI)
  fix n ty
  show "Elem (semantic_fvar_subst F ρ ν θ (n, ty)) (interp_type F ρ ty)"
  proof (cases "lookup_fvar θ n ty")
    case None
    then show ?thesis using free_ok
      by (simp add: semantic_fvar_subst_def free_valuation_ok_def)
  next
    case (Some rep)
    have rep: "check_term thy rep ∧ type_of rep = Some ty"
      using lookup_fvar_wf[OF subst_ok Some] .
    have empty: "bound_valuation_ok F ρ [] []"
      by (simp add: bound_valuation_ok_def)
    have "Elem (eval_term F ρ ν [] rep) (interp_type F ρ ty)"
      using eval_type_sound[OF thy_wf frame_ok type_ok free_ok const_ok empty]
        rep unfolding check_term_def by blast
    then show ?thesis using Some by (simp add: semantic_fvar_subst_def)
  qed
qed

lemma semantic_type_fvars_ok:
  assumes "free_valuation_ok F ρ ν"
  shows "free_valuation_ok F (subst_valuation F ρ θ)
    (semantic_type_fvars θ ν)"
  using assms
  by (auto simp: free_valuation_ok_def semantic_type_fvars_def
      interp_type_subst[symmetric])

section ‹Sequents and models›

definition holds ::
  "frame ⇒ (hname ⇒ ZF) ⇒ ((hname × htype) ⇒ ZF) ⇒ hterm ⇒ bool" where
  "holds F ρ ν p ⟷ eval_term F ρ ν [] p = ztrue"

definition valid_sequent :: "frame ⇒ htheory ⇒ hterm list ⇒ hterm ⇒ bool" where
  "valid_sequent F thy hs c ⟷
    (∀ρ ν. type_valuation_ok ρ ⟶ const_interpretation_ok F thy ρ ⟶
      free_valuation_ok F ρ ν ⟶
      (∀h∈set hs. holds F ρ ν h) ⟶ holds F ρ ν c)"

definition models_theory :: "frame ⇒ htheory ⇒ bool" where
  "models_theory F thy ⟷
    frame_wf F ∧
    (∀ρ. type_valuation_ok ρ ⟶ const_interpretation_ok F thy ρ) ∧
    (∀th∈set (axiom_list thy). valid_sequent F thy (hyps th) (concl th)) ∧
    (∀n th. def_tab thy n = Some th ⟶
      valid_sequent F thy (hyps th) (concl th))"

definition semantically_valid :: "htheory ⇒ hthm ⇒ bool" where
  "semantically_valid thy th ⟷
    wf_thm thy th ∧
    (∀F. models_theory F thy ⟶ valid_sequent F thy (hyps th) (concl th))"

lemma set_hyp_insert [simp]: "set (hyp_insert h hs) = insert h (set hs)"
  by (auto simp: hyp_insert_def)

lemma set_hyp_union [simp]:
  "set (hyp_union a b) = set a ∪ set b"
  unfolding hyp_union_def
  by (induction b arbitrary: a) auto

lemma set_hyp_remove [simp]:
  "set (hyp_remove h hs) = set hs - {h}"
  by (auto simp: hyp_remove_def)

lemma set_rehash_hyps [simp]: "set (rehash_hyps hs) = set hs"
  unfolding rehash_hyps_def
  by (induction hs rule: rev_induct) auto

lemma eval_eq_term:
  assumes thy_wf: "wf_theory thy" and frame_ok: "frame_wf F"
    and type_ok: "type_valuation_ok ρ"
    and free_ok: "free_valuation_ok F ρ ν"
    and const_ok: "const_interpretation_ok F thy ρ"
    and left: "check_term thy l" "type_of l = Some ty"
    and right: "check_term thy r" "type_of r = Some ty"
  shows "eval_term F ρ ν [] (eq_term ty l r) =
    (if eval_term F ρ ν [] l = eval_term F ρ ν [] r then ztrue else zfalse)"
proof -
  have empty: "bound_valuation_ok F ρ [] []"
    by (simp add: bound_valuation_ok_def)
  have l_in: "Elem (eval_term F ρ ν [] l) (interp_type F ρ ty)"
    using eval_type_sound[OF thy_wf frame_ok type_ok free_ok const_ok empty]
      left unfolding check_term_def by blast
  have r_in: "Elem (eval_term F ρ ν [] r) (interp_type F ρ ty)"
    using eval_type_sound[OF thy_wf frame_ok type_ok free_ok const_ok empty]
      right unfolding check_term_def by blast
  show ?thesis using zeq_apply[OF l_in r_in]
    by (simp add: const_sem_def eq_term_def eq_const_def mk_fun_def bool_ty_def)
qed

lemma holds_eq_iff:
  assumes "wf_theory thy" "frame_wf F" "type_valuation_ok ρ"
    "free_valuation_ok F ρ ν" "const_interpretation_ok F thy ρ"
    "check_term thy l" "type_of l = Some ty"
    "check_term thy r" "type_of r = Some ty"
  shows "holds F ρ ν (eq_term ty l r) ⟷
    eval_term F ρ ν [] l = eval_term F ρ ν [] r"
  using eval_eq_term[OF assms] ztrue_neq_zfalse
  by (auto simp: holds_def)

lemma subst_valuation_cong_on_instance:
  assumes instantiated: "type_subst θ generic = ty"
    and agree: "⋀w. type_var_occurs w ty ⟹ ρ w = σ w"
    and source: "type_var_occurs v generic"
  shows "subst_valuation F ρ θ v = subst_valuation F σ θ v"
proof (cases "θ v")
  case None
  have occurrence: "type_var_occurs v ty"
    using type_subst_component_occurs[OF source, where θ=θ and w=v]
      None instantiated by simp
  show ?thesis using None agree[OF occurrence]
    by (simp add: subst_valuation_def)
next
  case (Some component)
  have component_agree: "⋀w. type_var_occurs w component ⟹ ρ w = σ w"
  proof -
    fix w
    assume in_component: "type_var_occurs w component"
    have "type_var_occurs w ty"
      using type_subst_component_occurs[OF source, where θ=θ and w=w]
        Some in_component instantiated by simp    then show "ρ w = σ w" by (rule agree)
  qed
  have interp: "interp_type F ρ component = interp_type F σ component"
    using interp_type_cong_occurs component_agree by blast
  show ?thesis using Some interp by (simp add: subst_valuation_def)
qed
lemma const_sem_cong_type_vars:
  assumes frame_ok: "frame_wf F"
    and agree: "⋀v. v ∈ set (type_vars ty) ⟹ ρ v = σ v"
  shows "const_sem F ρ n ty = const_sem F σ n ty"
proof (cases "n = NEq")
  case True
  show ?thesis
  proof (cases "classify_equality_type ty")
    case (Equality_Instance a)
    have shape: "ty = mk_fun a (mk_fun a bool_ty)"
      using classify_equality_instance[OF Equality_Instance]
      by (simp add: mk_fun_def bool_ty_def)
    have a_agree: "⋀v. type_var_occurs v a ⟹ ρ v = σ v"
      using agree shape set_type_vars by (auto simp: mk_fun_def bool_ty_def)
    have carrier: "interp_type F ρ a = interp_type F σ a"
      using interp_type_cong_occurs a_agree by blast
    show ?thesis using True Equality_Instance carrier
      by (simp add: const_sem_def)
  qed (simp_all add: True const_sem_def)
next
  case False
  show ?thesis
  proof (cases "const_scheme F n")
    case None
    then show ?thesis using False by (simp add: const_sem_def)
  next
    case (Some generic)
    have scheme: "const_scheme F n = Some generic" using Some .
    show ?thesis
    proof (cases "type_match generic ty (λ_. None)")
      case None
      then show ?thesis using False scheme by (simp add: const_sem_def)
    next
      case (Some θ)
      have match: "type_match generic ty (λ_. None) = Some θ" using Some .
      have instantiated: "type_subst θ generic = ty"
        using type_match_sound[OF match] .
      have target_agree: "⋀v. type_var_occurs v ty ⟹ ρ v = σ v"
        using agree set_type_vars by auto
      have valuation_agree: "⋀v. type_var_occurs v generic ⟹
          subst_valuation F ρ θ v = subst_valuation F σ θ v"
      proof -
        fix v
        assume source: "type_var_occurs v generic"
        show "subst_valuation F ρ θ v = subst_valuation F σ θ v"
          using subst_valuation_cong_on_instance[where F=F and ρ=ρ and σ=σ
              and θ=θ and generic=generic and ty=ty and v=v,
              OF instantiated target_agree source] .
      qed
      have extensional: "∀r s. (∀v. type_var_occurs v generic ⟶ r v = s v) ⟶
          const_denote F n r = const_denote F n s"
        using frame_ok scheme by (auto simp: frame_wf_def)
      have denote: "const_denote F n (subst_valuation F ρ θ) =
          const_denote F n (subst_valuation F σ θ)"
        using extensional valuation_agree by blast
      have lhs: "const_sem F ρ n ty =
          const_denote F n (subst_valuation F ρ θ)"
        using const_sem_non_equality[OF False scheme match] .
      have rhs: "const_sem F σ n ty =
          const_denote F n (subst_valuation F σ θ)"
        using const_sem_non_equality[OF False scheme match] .
      show ?thesis using lhs rhs denote by simp
    qed  qed
qed

lemma interp_type_cong_type_vars:
  assumes "⋀v. v ∈ set (type_vars ty) ⟹ ρ v = σ v"
  shows "interp_type F ρ ty = interp_type F σ ty"
  using assms interp_type_cong_occurs set_type_vars by auto

lemma nat_lit_denote_cong_type_vars:
  assumes frame_ok: "frame_wf F"
  shows "nat_lit_denote F ρ n = nat_lit_denote F σ n"
proof (induction n)
  case 0
  show ?case
    by (simp only: nat_lit_denote.simps;
        rule const_sem_cong_type_vars[OF frame_ok])
       (simp add: nat_aty_def type_vars_def)
next
  case (Suc n)
  have succ: "const_sem F ρ nat_succ_name nat_sty =
      const_sem F σ nat_succ_name nat_sty"
    by (rule const_sem_cong_type_vars[OF frame_ok])
       (simp add: nat_sty_def nat_aty_def mk_fun_def type_vars_def)
  then show ?case using Suc.IH by simp
qed

lemma eval_term_cong_type_vars:
  assumes frame_ok: "frame_wf F"
    and agree: "⋀v. v ∈ set (term_type_vars t) ⟹ ρ v = σ v"
  shows "eval_term F ρ ν env t = eval_term F σ ν env t"
  using agree
proof (induction t arbitrary: env)
  case (FVar n ty)
  then show ?case by simp
next
  case (BVar i ty)
  then show ?case by simp
next
  case (Const n ty)
  have type_agree: "⋀v. v ∈ set (type_vars ty) ⟹ ρ v = σ v"
    using Const.prems by simp
  show ?case using const_sem_cong_type_vars[OF frame_ok type_agree] by simp
next
  case (NatLit n)
  show ?case using nat_lit_denote_cong_type_vars[OF frame_ok, of ρ n σ]
    by simp
next
  case (Comb f x)
  have f: "eval_term F ρ ν env f = eval_term F σ ν env f"
    using Comb.IH(1) Comb.prems by auto
  have x: "eval_term F ρ ν env x = eval_term F σ ν env x"
    using Comb.IH(2) Comb.prems by auto
  show ?case using f x by simp
next
  case (Abs ty body)
  have type_agree: "⋀v. v ∈ set (type_vars ty) ⟹ ρ v = σ v"
    using Abs.prems by auto
  have carrier: "interp_type F ρ ty = interp_type F σ ty"
    using interp_type_cong_type_vars[OF type_agree] .
  have body: "⋀z. eval_term F ρ ν (z # env) body =
      eval_term F σ ν (z # env) body"
    using Abs.IH Abs.prems by auto
  show ?case using carrier body by simp
qed

lemma eval_term_cong_free_vars:
  assumes agree: "⋀key. key ∈ set (free_vars t) ⟹ ν key = μ key"
  shows "eval_term F ρ ν env t = eval_term F ρ μ env t"
  using agree
proof (induction t arbitrary: env)
  case (FVar n ty)
  then show ?case by simp
next
  case (BVar i ty)
  then show ?case by simp
next
  case (Const n ty)
  then show ?case by simp
next
  case (NatLit n)
  then show ?case by simp
next
  case (Comb f x)
  then show ?case by auto
next
  case (Abs ty body)
  have body: "⋀z. eval_term F ρ ν (z # env) body =
      eval_term F ρ μ (z # env) body"
    using Abs.IH Abs.prems by auto
  show ?case using body by simp
qed

lemma eval_term_closed_free_valuation:
  assumes closed: "free_vars t = []"
  shows "eval_term F ρ ν env t = eval_term F ρ μ env t"
proof (rule eval_term_cong_free_vars)
  fix key
  assume "key ∈ set (free_vars t)"
  then show "ν key = μ key" using closed by simp
qed

end