Theory Sorted_Terms

section ‹Sorted Terms›

theory Sorted_Terms
  imports Sorted_Sets "First_Order_Terms.Term"
begin

subsection ‹Overloaded Notations›

consts vars :: "'a ⇒ 'b set"

adhoc_overloading vars vars_term

consts map_vars :: "('a ⇒ 'b) ⇒ 'c ⇒ 'd"

adhoc_overloading map_vars "map_term (λx. x)"

lemma map_term_eq_Var: "map_term F V s = Var y ⟷ (∃x. s = Var x ∧ y = V x)"
  by (cases s, auto)

lemma map_vars_id_iff: "map_vars f s = s ⟷ (∀x ∈ vars_term s. f x = x)"
  by (induct s, auto simp: list_eq_iff_nth_eq all_set_conv_all_nth)

lemma map_var_term_id[simp]: "map_term (λx. x) id = id" by (auto simp: id_def[symmetric] term.map_id)

lemma map_term_eq_Fun:
  "map_term F V s = Fun g ts ⟷ (∃f ss. s = Fun f ss ∧ g = F f ∧ ts = map (map_term F V) ss)"
  by (cases s, auto)

declare domIff[iff del]

subsection ‹Sorted Signatures and Sorted Sets of Terms›

text ‹We view a sorted signature as a partial map 
that assigns an output sort to the pair of a function symbol and a list of input sorts.›

type_synonym ('f,'s) ssig = "'f × 's list ⇀ 's"

definition fun_hastype :: "'f ⇒ 's ⇒ 't ⇒ ('f × 's ⇀ 't) ⇒ bool"
  (‹(_ : /_ /→ /_ in/ _)› [50,61,61,50]50)
  where "f : σ → τ in F ≡ F (f,σ) = Some τ"

lemmas fun_hastypeI = fun_hastype_def[unfolded atomize_eq, THEN iffD2]
lemmas fun_hastypeD = fun_hastype_def[unfolded atomize_eq, THEN iffD1]

lemma fun_hastype_imp_dom[simp]:
  assumes "f : σ → τ in F" shows "(f,σ) ∈ dom F"
  using assms by (auto simp: fun_hastype_def domIff)

lemma in_dom_fun_hastypeE:
  assumes "(f,σ) ∈ dom F" and "⋀τ. f : σ → τ in F ⟹ thesis" shows thesis
  using assms by (auto simp: fun_hastype_def dom_def)

lemma fun_has_same_type:
  assumes "f : σ → τ in F" and "f : σ → τ' in F" shows "τ = τ'"
  using assms by (auto simp: fun_hastype_def)

lemma fun_hastype_empty[simp]: "¬ f : σ → τ in ∅"
  by (auto simp: fun_hastype_def)

lemma fun_hastype_upd: "f : σ → τ in F((f',σ') ↦ τ') ⟷
  (if f = f' ∧ σ = σ' then τ = τ' else f : σ → τ in F)"
  by (auto simp: fun_hastype_def)

lemma fun_hastype_restrict: "f : σ → τ in F |` S ⟷ (f,σ) ∈ S ∧ f : σ → τ in F"
  by (auto simp: restrict_map_def fun_hastype_def)

lemma subssigI: assumes "⋀f σ τ. f : σ → τ in F ⟹ f : σ → τ in F'"
  shows "F ⊆⇩m F'"
  using assms by (auto simp: map_le_def fun_hastype_def dom_def)

lemma subssigD: assumes FF: "F ⊆⇩m F'" and "f : σ → τ in F" shows "f : σ → τ in F'"
  using assms by (auto simp: map_le_def fun_hastype_def dom_def)

text ‹The sorted set of terms:›

primrec Term (‹𝒯'(_,_')›) where
  "𝒯(F,V) (Var v) = V v"
| "𝒯(F,V) (Fun f ss) =
  (case those (map 𝒯(F,V) ss) of None ⇒ None | Some σs ⇒ F (f,σs))"

lemma Var_hastype[simp]: "Var v : σ in 𝒯(F,V) ⟷ v : σ in V"
  by (auto simp: hastype_def)

lemma Fun_hastype:
  "Fun f ss : τ in 𝒯(F,V) ⟷ (∃σs. f : σs → τ in F ∧ ss :⇩l σs in 𝒯(F,V))"
  apply (unfold hastype_list_iff_those)
  by (auto simp: fun_hastype_def hastype_def split:option.split_asm)

lemma Fun_in_dom_imp_arg_in_dom: "Fun f ss ∈ dom 𝒯(F,V) ⟹ s ∈ set ss ⟹ s ∈ dom 𝒯(F,V)"
  by (auto simp: in_dom_iff_ex_type Fun_hastype list_all2_conv_all_nth in_set_conv_nth)

lemma Fun_hastypeI: "f : σs → τ in F ⟹ ss :⇩l σs in 𝒯(F,V) ⟹ Fun f ss : τ in 𝒯(F,V)"
  by (auto simp: Fun_hastype)

lemma hastype_in_Term_induct[case_names Var Fun, induct pred]:
  assumes s: "s : σ in 𝒯(F,V)"
    and V: "⋀v σ. v : σ in V ⟹ P (Var v) σ"
    and F: "⋀f ss σs τ.
        f : σs → τ in F ⟹ ss :⇩l σs in 𝒯(F,V) ⟹ list_all2 P ss σs ⟹ P (Fun f ss) τ"
  shows "P s σ"
proof (insert s, induct s arbitrary: σ rule:term.induct)
  case (Var v σ)
  with V[of v σ] show ?case by auto
next
  case (Fun f ss τ)
  then obtain σs where f: "f : σs → τ in F" and ss: "ss :⇩l σs in 𝒯(F,V)" by (auto simp:Fun_hastype)
  show ?case
  proof (rule F[OF f ss], unfold list_all2_conv_all_nth, safe)
    from ss show len: "length ss = length σs" by (auto dest: list_all2_lengthD)
    fix i assume i: "i < length ss"
    with ss have *: "ss ! i : σs ! i in 𝒯(F,V)" by (auto simp: list_all2_conv_all_nth)
    from i have ssi: "ss ! i ∈ set ss" by auto
    from Fun(1)[OF this *]
    show "P (ss ! i) (σs ! i)".
  qed
qed

lemma in_dom_Term_induct[case_names Var Fun, induct pred]:
  assumes s: "s ∈ dom 𝒯(F,V)"
  assumes V: "⋀v σ. v : σ in V ⟹ P (Var v)"
  assumes F: "⋀f ss σs τ.
    f : σs → τ in F ⟹ ss :⇩l σs in 𝒯(F,V) ⟹ ∀s ∈ set ss. P s ⟹ P (Fun f ss)"
  shows "P s"
proof-
  from s obtain σ where "s : σ in 𝒯(F,V)" by (auto elim!:in_dom_hastypeE)
  then show ?thesis
    by (induct rule: hastype_in_Term_induct, auto intro!: V F simp: list_all2_indep2)
qed

lemma Term_mono_left: assumes FF: "F ⊆⇩m F'" shows "𝒯(F,V) ⊆⇩m 𝒯(F',V)"
proof (intro subssetI, elim hastype_in_Term_induct, goal_cases)
  case (1 a σ v σ')
  then show ?case by auto
next
  case (2 a σ f ss σs τ)
  then show ?case
    by (auto intro!:exI[of _ σs] dest!: subssigD[OF FF] simp: Fun_hastype)
qed

lemmas hastype_in_Term_mono_left = Term_mono_left[THEN subssetD]

lemmas dom_Term_mono_left = Term_mono_left[THEN map_le_implies_dom_le]

lemma Term_mono_right: assumes VV: "V ⊆⇩m V'" shows "𝒯(F,V) ⊆⇩m 𝒯(F,V')"
proof (intro subssetI, elim hastype_in_Term_induct, goal_cases)
  case (1 a σ v σ')
  with VV show ?case by (auto dest!:subssetD)
next
  case (2 a σ f ss σs τ)
  then show ?case
    by (auto intro!:exI[of _ σs] simp: Fun_hastype)
qed

lemmas hastype_in_Term_mono_right = Term_mono_right[THEN subssetD]

lemmas dom_Term_mono_right = Term_mono_right[THEN map_le_implies_dom_le]

lemmas Term_mono = map_le_trans[OF Term_mono_left Term_mono_right]

lemmas hastype_in_Term_mono = Term_mono[THEN subssetD]

lemmas dom_Term_mono = Term_mono[THEN map_le_implies_dom_le]

lemma hastype_in_Term_restrict_vars: "s : σ in 𝒯(F, V |` vars s) ⟷ s : σ in 𝒯(F,V)"
  (is "?l s ⟷ ?r s")
proof (rule iffI)
  assume "?l s"
  from hastype_in_Term_mono_right[OF restrict_submap this]
  show "?r s".
next
  show "?r s ⟹ ?l s"
  proof (induct rule: hastype_in_Term_induct)
    case (Var v σ)
    then show ?case by (auto simp:hastype_restrict)
  next
    case (Fun f ss σs τ)
    have "ss :⇩l σs in 𝒯(F,V |` vars (Fun f ss))"
      apply (rule list.rel_mono_strong[OF Fun(3) hastype_in_Term_mono_right])
      by (auto intro: restrict_map_mono_right)
    with Fun show ?case
      by (auto simp:Fun_hastype)
  qed
qed

lemma hastype_in_Term_imp_vars: "s : σ in 𝒯(F,V) ⟹ v ∈ vars s ⟹ v ∈ dom V"
proof (induct s σ rule: hastype_in_Term_induct)
  case (Var v σ)
  then show ?case by auto
next
  case (Fun f ss σs τ)
  then obtain i where i: "i < length ss" and v: "v ∈ vars (ss!i)" by (auto simp:in_set_conv_nth)
  from Fun(3) i v
  show ?case by (auto simp: list_all2_conv_all_nth)
qed

lemma in_dom_Term_imp_vars: "s ∈ dom 𝒯(F,V) ⟹ v ∈ vars s ⟹ v ∈ dom V"
  by (auto elim!: in_dom_hastypeE simp: hastype_in_Term_imp_vars)

lemma hastype_in_Term_imp_vars_subset: "t : s in 𝒯(F,V) ⟹ vars t ⊆ dom V" 
  by (auto dest: hastype_in_Term_imp_vars)

interpretation Var: sorted_map Var V "𝒯(F,V)" for F V by (auto intro!: sorted_mapI)


subsection ‹Sorted Algebras›

locale sorted_algebra_syntax =
  fixes F :: "('f,'s) ssig" and A :: "'a ⇀ 's" and I :: "'f ⇒ 'a list ⇒ 'a"

locale sorted_algebra = sorted_algebra_syntax +
  assumes sort_matches: "f : σs → τ in F ⟹ as :⇩l σs in A ⟹ I f as : τ in A"
begin

context
  fixes α V
  assumes α: "α :⇩s V → A"
begin

lemma eval_hastype:
  assumes s: "s : σ in 𝒯(F,V)" shows "I⟦s⟧α : σ in A"
  by (insert s, induct s σ rule: hastype_in_Term_induct,
      auto simp: sorted_mapD[OF α] intro!: sort_matches simp: list_all2_conv_all_nth)

interpretation eval: sorted_map "λs. I⟦s⟧α" "𝒯(F,V)" A
  by (auto intro!: sorted_mapI eval_hastype)

lemmas eval_sorted_map = eval.sorted_map_axioms
lemmas eval_dom = eval.in_dom
lemmas map_eval_hastype = eval.sorted_map_list
lemmas eval_has_same_type = eval.target_has_same_type
lemmas eval_dom_iff_hastype = eval.target_dom_iff_hastype
lemmas dom_iff_hastype = eval.source_dom_iff_hastype

end

lemmas eval_hastype_vars =
  eval_hastype[OF _ hastype_in_Term_restrict_vars[THEN iffD2]]

lemmas eval_has_same_type_vars =
  eval_has_same_type[OF _ hastype_in_Term_restrict_vars[THEN iffD2]]

end

lemma sorted_algebra_cong:
  assumes "F = F'" and "A = A'"
    and "⋀f σs τ as. f : σs → τ in F' ⟹ as :⇩l σs in A' ⟹ I f as = I' f as"
  shows "sorted_algebra F A I = sorted_algebra F' A' I'"
  using assms by (auto simp: sorted_algebra_def)

subsubsection ‹Term Algebras›

text ‹The sorted set of terms constitutes a sorted algebra, in which
evaluation is substitution.›

interpretation "term": sorted_algebra F "𝒯(F,V)" Fun for F V
  apply (unfold_locales)
  by (auto simp: Fun_hastype)

text ‹Sorted substitution preserves type:›

lemma subst_hastype: "θ :⇩s X → 𝒯(F,V) ⟹ s : σ in 𝒯(F,X) ⟹ s⋅θ : σ in 𝒯(F,V)"
  using term.eval_hastype.

lemmas subst_hastype_imp_dom_iff = term.dom_iff_hastype
lemmas subst_hastype_vars = term.eval_hastype_vars
lemmas subst_has_same_type = term.eval_has_same_type
lemmas subst_same_vars = eval_same_vars[of _ _ _ Fun]
lemmas subst_map_vars = eval_map_vars[of Fun]
lemmas subst_o = eval_o[of Fun]
lemmas subst_sorted_map = term.eval_sorted_map
lemmas map_subst_hastype = term.map_eval_hastype

lemma subst_compose_sorted_map:
  assumes "θ :⇩s X → 𝒯(F,Y)" and "ρ :⇩s Y → 𝒯(F,Z)"
  shows "θ ∘⇩s ρ :⇩s X → 𝒯(F,Z)"
  using assms by (simp add: sorted_map_def subst_compose subst_hastype)

lemma subst_hastype_iff_vars:
  assumes "∀x∈vars s. ∀σ. θ x : σ in 𝒯(F,W) ⟷ x : σ in V"
  shows "s ⋅ θ : σ in 𝒯(F,W) ⟷ s : σ in 𝒯(F,V)"
proof (insert assms, induct s arbitrary: σ)
  case (Var x)
  then show ?case by (auto intro!: hastypeI)
next
  case (Fun f ss τ)
  then show ?case by (simp add:Fun_hastype list_all2_conv_all_nth cong:map_cong)
qed

lemma subst_in_dom_imp_var_in_dom:
  assumes "s⋅θ ∈ dom 𝒯(F,V)" and "x ∈ vars s" shows "θ x ∈ dom 𝒯(F,V)"
  using assms
proof (induction s)
  case (Var v)
  then show ?case by auto
next
  case (Fun f ss)
  then obtain s where s: "s ∈ set ss" and "s⋅θ : dom 𝒯(F,V)" and xs: "x ∈ vars s"
    by (auto dest!: Fun_in_dom_imp_arg_in_dom)
  from Fun.IH[OF this]
  show ?case.
qed

lemma subst_sorted_map_restrict_vars:
  assumes θ: "θ :⇩s X → 𝒯(F,V)" and WV: "W ⊆⇩m V" and sθ: "s⋅θ ∈ dom 𝒯(F,W)"
  shows "θ :⇩s X |` vars s → 𝒯(F,W)"
proof (safe intro!: sorted_mapI dest!: hastype_restrict[THEN iffD1])
  fix x σ assume xs: "x ∈ vars s" and xσ: "x : σ in X"
  from sorted_mapD[OF θ xσ] have xθσ: "θ x : σ in 𝒯(F,V)" by auto
  from subst_in_dom_imp_var_in_dom[OF sθ xs]
  obtain σ' where "θ x : σ' in 𝒯(F,W)" by (auto simp: in_dom_iff_ex_type)
  with hastype_in_Term_mono[OF map_le_refl WV this] xθσ
  show "θ x : σ in 𝒯(F,W)" by (auto simp: has_same_type)
qed

subsubsection ‹Homomorphisms›

locale sorted_distributive =
  sort_preserving φ A + source: sorted_algebra F A I for F φ A I J +
  assumes distrib: "f : σs → τ in F ⟹ as :⇩l σs in A ⟹ φ (I f as) = J f (map φ as)"
begin

lemma distrib_eval:
  assumes α: "α :⇩s V → A" and s: "s : σ in 𝒯(F,V)"
  shows "φ (I⟦s⟧α) = J⟦s⟧(φ ∘ α)"
proof (insert s, induct rule: hastype_in_Term_induct)
  case (Var v σ)
  then show ?case by auto
next
  case (Fun f ss σs τ)
  note ty = source.map_eval_hastype[OF α Fun(2)]
  from Fun(3)[unfolded list_all2_indep2] distrib[OF Fun(1) ty]
  show ?case by (auto simp: o_def cong:map_cong)
qed

text ‹The image of a distributive map forms a sorted algebra.›

sublocale image: sorted_algebra F "φ `⇧s A" J
proof (unfold_locales)
  fix f σs τ bs
  assume f: "f : σs → τ in F" and bs: "bs :⇩l σs in φ `⇧s A"
  from bs[unfolded hastype_list_in_image]
  obtain as where as: "as :⇩l σs in A" and asbs: "map φ as = bs" by auto
  show "J f bs : τ in φ `⇧s A"
    apply (rule hastype_in_imageI)
    apply (fact source.sort_matches[OF f as])
    by (auto simp: distrib[OF f as] asbs)
qed

end

lemma sorted_distributive_cong:
  fixes A A' :: "'a ⇀ 's" and φ :: "'a ⇒ 'b" and I :: "'f ⇒ 'a list ⇒ 'a"
  assumes φ: "⋀a σ. a : σ in A ⟹ φ a = φ' a"
    and A: "A = A'"
    and I: "⋀f σs τ as. f : σs → τ in F ⟹ as :⇩l σs in A ⟹ I f as = I' f as"
    and J: "⋀f σs τ as. f : σs → τ in F ⟹ as :⇩l σs in A ⟹ J f (map φ as) = J' f (map φ as)"
  shows "sorted_distributive F φ A I J = sorted_distributive F φ' A' I' J'"
proof-
  { fix A A' :: "'a ⇀ 's" and φ φ' :: "'a ⇒ 'b" and I I' :: "'f ⇒ 'a list ⇒ 'a" and J J' :: "'f ⇒ 'b list ⇒ 'b"
    assume φ: "⋀a σ. a : σ in A ⟹ φ a = φ' a"
    have map_eq: "as :⇩l σs in A ⟹ map φ as = map φ' as" for as σs
      by (auto simp: list_eq_iff_nth_eq φ dest:list_all2_nthD)
    { assume A: "A = A'"
        and I: "⋀f σs τ as. f : σs → τ in F ⟹ as :⇩l σs in A' ⟹ I f as = I' f as"
        and J: "⋀f σs τ as. f : σs → τ in F ⟹ as :⇩l σs in A' ⟹ J f (map φ as) = J' f (map φ as)"
      { assume hom: "sorted_distributive F φ' A' I' J'"
        from hom interpret sorted_distributive F φ' A' I' J'.
        interpret I: sorted_algebra F A I
          using source.sort_matches A I by (auto intro!: sorted_algebra.intro)
        have "sorted_distributive F φ A I J"
        proof (intro sorted_distributive.intro sorted_distributive_axioms.intro
              I.sorted_algebra_axioms)
          show "sort_preserving φ A" using sort_preserving_axioms[folded A] φ
            by (simp cong: sort_preserving_cong)
          fix f σs τ as
          assume f: "f : σs → τ in F" and as: "as :⇩l σs in A"
          from distrib[OF f as[unfolded A]] φ as I.sort_matches[OF f as]
            I[OF f as[unfolded A]] 
          show "φ (I f as) = J f (map φ as)" by (auto simp: map_eq[symmetric] A intro!: J[OF f, symmetric])
        qed
      }
    }
    note this map_eq
  }
  note * = this(1) and map_eq = this(2)
  from map_eq[unfolded atomize_imp atomize_all, folded atomize_imp] φ
  have map_eq: "as :⇩l σs in A ⟹ map φ as = map φ' as" for as σs by metis
  show ?thesis
  proof (rule iffI)
    assume pre: "sorted_distributive F φ A I J"
    show "sorted_distributive F φ' A' I' J'"
      apply (rule *[rotated -1, OF pre])
      using assms by (auto simp: map_eq)
  next
    assume pre: "sorted_distributive F φ' A' I' J'"
    show "sorted_distributive F φ A I J"
      apply (rule *[rotated -1, OF pre])
      using assms by auto
  qed
qed

lemma sorted_distributive_o:
  assumes "sorted_distributive F φ A I J" and "sorted_distributive F ψ (φ `⇧s A) J K"
  shows "sorted_distributive F (ψ ∘ φ) A I K"
proof-
  interpret φ: sorted_distributive F φ A I J + ψ: sorted_distributive F ψ "φ`⇧sA" J K using assms.
  interpret sort_preserving "ψ∘φ" A by (rule sort_preserving_o; unfold_locales)
  show ?thesis
    apply (unfold_locales)
    by (simp add: φ.distrib ψ.distrib[OF _ φ.to_image.sorted_map_list])
qed

locale sorted_homomorphism = sorted_distributive F φ A I J + sorted_map φ A B +
  target: sorted_algebra F B J for F φ A I B J
begin
end

lemma sorted_homomorphism_o:
  assumes "sorted_homomorphism F φ A I B J" and "sorted_homomorphism F ψ B J C K"
  shows "sorted_homomorphism F (ψ ∘ φ) A I C K"
proof-
  interpret φ: sorted_homomorphism F φ A I B J + ψ: sorted_homomorphism F ψ B J C K using assms.
  interpret sorted_map "ψ ∘ φ" A C
    using sorted_map_o[OF φ.sorted_map_axioms ψ.sorted_map_axioms].
  show ?thesis
    apply (unfold_locales)
    by (simp add: φ.distrib ψ.distrib[OF _ φ.sorted_map_list])
qed

context sorted_algebra begin

context fixes α V assumes sorted: "α :⇩s V → A"
begin

text ‹ The term algebra is free in all @{term F}-algebras;
that is, every assignment @{term ‹α :⇩s V → A›} is extended to a homomorphism @{term ‹λs. I⟦s⟧α›}. ›

interpretation sorted_map α V A using sorted.

interpretation eval: sorted_map ‹λs. I⟦s⟧α› ‹𝒯(F,V)› A using eval_sorted_map[OF sorted].

interpretation eval: sorted_homomorphism F ‹λs. I⟦s⟧α› ‹𝒯(F,V)› Fun A I
  apply (unfold_locales) by auto

lemmas eval_sorted_homomorphism = eval.sorted_homomorphism_axioms

end

end

lemma sorted_homomorphism_cong:
  fixes A A' :: "'a ⇀ 's" and φ :: "'a ⇒ 'b" and I :: "'f ⇒ 'a list ⇒ 'a"
  assumes φ: "⋀a σ. a : σ in A ⟹ φ a = φ' a"
    and A: "A = A'"
    and I: "⋀f σs τ as. f : σs → τ in F ⟹ as :⇩l σs in A ⟹ I f as = I' f as"
    and B: "B = B'"
    and J: "⋀f σs τ bs. f : σs → τ in F ⟹ bs :⇩l σs in B ⟹ J f bs = J' f bs"
  shows "sorted_homomorphism F φ A I B J = sorted_homomorphism F φ' A' I' B' J'" (is "?l ⟷ ?r")
proof
  assume ?l
  then interpret sorted_homomorphism F φ A I B J.
  have J': "as :⇩l σs in A' ⟹ J f (map φ as) = J' f (map φ as)" if f: "f : σs → τ in F" for f σs τ as
    apply (rule J[OF f]) using A B sorted_map_list by auto
  note * = sorted_distributive_cong[THEN iffD1, rotated -1, OF sorted_distributive_axioms]
  show ?r
    apply (intro sorted_homomorphism.intro *)
    using assms J' sorted_map_axioms target.sorted_algebra_axioms
    by (simp_all cong: sorted_map_cong sorted_algebra_cong)
next
  assume ?r
  then interpret sorted_homomorphism F φ' A' I' B' J'.
  have J': "as :⇩l σs in A' ⟹ J f (map φ' as) = J' f (map φ' as)" if f: "f : σs → τ in F" for f σs τ as
    apply (rule J[OF f]) using A B sorted_map_list φ by auto
  note * = sorted_distributive_cong[THEN iffD1, rotated -1, OF sorted_distributive_axioms]
  note 2 = sorted_map_cong[THEN iffD1, rotated -1, OF sorted_map_axioms]
  show ?l
    apply (intro sorted_homomorphism.intro * 2)
    using assms J' target.sorted_algebra_axioms
    by (simp_all cong: sorted_distributive_cong sorted_algebra_cong)
qed

context sort_preserving begin

lemma sort_preserving_map_vars: "sort_preserving (map_vars f) 𝒯(F,A)"
proof
  fix a b σ τ
  assume a: "a : σ in 𝒯(F,A)" and b: "b : τ in 𝒯(F,A)" and eq: "map_vars f a = map_vars f b"
  from a b eq show "σ = τ"
  proof (induct arbitrary: τ b)
    case (Var x σ)
    then show ?case by (cases b, auto simp: same_value_imp_same_type)
  next
    case IH: (Fun ff ss σs σ)
    show ?case
    proof (cases b)
      case (Var y)
      with IH show ?thesis by auto
    next
      case (Fun gg tt)
      with IH have eq: "map (map_vars f) ss = map (map_vars f) tt" by (auto simp: id_def)
      from arg_cong[OF this, of length] have lensstt: "length ss = length tt" by auto
      with IH obtain τs where ff2: "ff : τs → τ in F" and tt: "tt :⇩l τs in 𝒯(F,A)"
        by (auto simp: Fun Fun_hastype)
      from IH have lenss: "length ss = length σs" by (auto simp: list_all2_lengthD)
      have "σs = τs"
      proof (unfold list_eq_iff_nth_eq, safe)
        from lensstt tt IH show len2: "length σs = length τs" by (auto simp: list_all2_lengthD)
        fix i assume "i < length σs"
        with lenss have i: "i < length ss" by auto
        show "σs ! i = τs ! i"
        proof(rule list_all2_nthD[OF IH(3) i, rule_format])
          from i lenss lensstt arg_cong[OF eq, of "λxs. xs!i"]
          show "map_vars f (ss ! i) = map_vars f (tt ! i)" by auto
          from i lensstt list_all2_nthD[OF tt]
          show "tt ! i : τs ! i in 𝒯(F,A)" by auto
        qed
      qed
      with ff2 Fun IH.hyps(1) show "σ = τ" by (auto simp: fun_hastype_def)
    qed
  qed
qed

lemma map_vars_image_Term: "map_vars f `⇧s 𝒯(F,A) = 𝒯(F,f `⇧s A)" (is "?L = ?R")
proof (intro sset_eqI)
  interpret map_vars: sort_preserving "map_term (λx. x) f" "𝒯(F,A)" using sort_preserving_map_vars.
  fix a σ
  show "a : σ in ?L ⟷ a : σ in ?R"
  proof (induct a arbitrary: σ)
    case (Var x)
    then show ?case 
      by (auto simp: map_vars.hastype_in_image map_term_eq_Var hastype_in_image)
        (metis Var_hastype)
  next
    case IH: (Fun ff as)
    show ?case
    proof (unfold Fun_hastype map_vars.hastype_in_image map_term_eq_Fun, safe dest!: Fun_hastype[THEN iffD1])
      fix ss σs
      assume as: "as = map (map_vars f) ss" and ff: "ff : σs → σ in F" and ss: "ss :⇩l σs in 𝒯(F,A)"
      from ss have "map (map_vars f) ss :⇩l σs in map_vars f `⇧s 𝒯(F,A)"
        by (auto simp: map_vars.hastype_list_in_image)
      with IH[unfolded as]
      have "map (map_vars f) ss :⇩l σs in 𝒯(F,f `⇧s A)"
        by (auto simp: list_all2_conv_all_nth)
      with ff
      show "∃σs. ff : σs → σ in F ∧ map (map_vars f) ss :⇩l σs in 𝒯(F,f `⇧s A)" by auto
    next
      fix σs assume ff: "ff : σs → σ in F" and as: "as :⇩l σs in 𝒯(F,f `⇧s A)"
      with IH have "as :⇩l σs in map_vars f `⇧s 𝒯(F,A)"
        by (auto simp: map_vars.hastype_in_image list_all2_conv_all_nth)
      then obtain ss where ss: "ss :⇩l σs in 𝒯(F,A)" and as: "as = map (map_vars f) ss"
        by (auto simp: map_vars.hastype_list_in_image)
      from ss ff have a: "Fun ff ss : σ in 𝒯(F,A)" by (auto simp: Fun_hastype)
      show "∃a. a : σ in 𝒯(F,A) ∧ (∃fa ss. a = Fun fa ss ∧ ff = fa ∧ as = map (map_vars f) ss)"
        apply (rule exI[of _ "Fun ff ss"])
        using a as by auto
    qed
  qed
qed

end

context sorted_map begin

lemma sorted_map_map_vars: "map_vars f :⇩s 𝒯(F,A) → 𝒯(F,B)"
proof-
  interpret map_vars: sort_preserving ‹map_vars f› ‹𝒯(F,A)› using sort_preserving_map_vars.
  show ?thesis
    apply (unfold map_vars.sorted_map_iff_image_subset)
    apply (unfold map_vars_image_Term)
    apply (rule Term_mono_right)
    using image_subsset.
qed

end

subsection ‹Lifting Sorts›

text ‹By `uni-sorted' we mean the situation where there is only one sort @{term "()"}.
This situation is isomorphic to sets.›
definition "unisorted A a ≡ if a ∈ A then Some () else None"

lemma unisorted_eq_Some[simp]: "unisorted A a = Some σ ⟷ a ∈ A"
  and unisorted_eq_None[simp]: "unisorted A a = None ⟷ a ∉ A"
  and hastype_in_unisorted[simp]: "a : σ in unisorted A ⟷ a ∈ A"
  by (auto simp: unisorted_def hastype_def)

lemma hastype_list_in_unisorted[simp]: "as :⇩l σs in unisorted A ⟷ length as = length σs ∧ set as ⊆ A"
  by (auto simp: list_all2_conv_all_nth dest: all_nth_imp_all_set)

lemma dom_unisorted[simp]: "dom (unisorted A) = A"
  by (auto simp: unisorted_def domIff split:if_split_asm)

lemma unisorted_map[simp]:
  "f :⇩s unisorted A → τ ⟷ f : A → dom τ"
  "f :⇩s σ → unisorted B ⟷ f : dom σ → B"
  by (auto simp: sorted_map_def hastype_def domIff)

lemma image_unisorted[simp]: "f `⇧s unisorted A = unisorted (f ` A)"
  by (auto intro!:sset_eqI simp: hastype_def sorted_image_def safe_The_eq_Some) 

definition unisorted_sig :: "('f×nat) set ⇒ ('f,unit) ssig"
  where "unisorted_sig F ≡ λ(f,σs). if (f, length σs) ∈ F then Some () else None"

lemma in_unisorted_sig[simp]: "f : σs → τ in unisorted_sig F ⟷ (f,length σs) ∈ F"
  by (auto simp: unisorted_sig_def fun_hastype_def)

inductive_set uTerm (‹𝔗'(_,_')› [1,1]1000) for F V where
  "Var v ∈ 𝔗(F,V)" if "v ∈ V"
| "∀s ∈ set ss. s ∈ 𝔗(F,V) ⟹ Fun f ss ∈ 𝔗(F,V)" if "(f,length ss) ∈ F"

lemma Var_in_Term[simp]: "Var x ∈ 𝔗(F,V) ⟷ x ∈ V"
    using uTerm.cases by (auto intro: uTerm.intros)

lemma Fun_in_Term[simp]: "Fun f ss ∈ 𝔗(F,V) ⟷ (f,length ss) ∈ F ∧ set ss ⊆ 𝔗(F,V)"
  apply (unfold subset_iff)
  apply (fold Ball_def)
  by (metis (no_types, lifting) term.distinct(1) term.inject(2) uTerm.simps)

lemma hastype_in_unisorted_Term[simp]:
  "s : σ in 𝒯(unisorted_sig F, unisorted V) ⟷ s ∈ 𝔗(F,V)"
proof (induct s)
case (Var x)
  then show ?case by auto
next
  case (Fun f ss)
  then show ?case
    by (auto simp: in_dom_iff_ex_type Fun_hastype list_all2_indep2
        intro!: exI[of _ "replicate (length ss) ()"])
qed

lemma unisorted_Term: "𝒯(unisorted_sig F, unisorted V) = unisorted 𝔗(F,V)"
  by (auto intro!: sset_eqI)

locale algebra =
  fixes F :: "('f × nat) set" and A :: "'a set" and I
  assumes closed: "(f, length as) ∈ F ⟹ set as ⊆ A ⟹ I f as ∈ A"
begin
end

lemma unisorted_algebra: "sorted_algebra (unisorted_sig F) (unisorted A) I ⟷ algebra F A I"
  (is "?l ⟷ ?r")
proof
  assume "?r"
  then interpret algebra.
  show ?l
    apply unfold_locales by (auto simp: list_all2_indep2 intro!: closed)
next
  assume ?l
  then interpret sorted_algebra ‹unisorted_sig F› ‹unisorted A› I.
  show ?r
  proof unfold_locales
    fix f as assume f: "(f, length as) ∈ F" and asA: "set as ⊆ A"
    from f have "f : replicate (length as) () → () in unisorted_sig F" by auto
    from sort_matches[OF this] asA
    show "I f as ∈ A" by auto
  qed
qed

context algebra begin

interpretation unisorted: sorted_algebra ‹unisorted_sig F› ‹unisorted A› I
  apply (unfold unisorted_algebra)..

lemma eval_closed: "α : V → A ⟹ s ∈ 𝔗(F,V) ⟹ I⟦s⟧α ∈ A"
  using unisorted.eval_hastype[of α "unisorted V"] by simp

end

locale distributive =
  source: algebra F A I for F φ A I J +
  assumes distrib: "(f, length as) ∈ F ⟹ set as ⊆ A ⟹ φ (I f as) = J f (map φ as)"

lemma unisorted_distributive:
  "sorted_distributive (unisorted_sig F) φ (unisorted A) I J ⟷
   distributive F φ A I J" (is "?l ⟷ ?r")
proof
  assume ?r
  then interpret distributive.
  show ?l
    apply (intro sorted_distributive.intro unisorted_algebra[THEN iffD2])
    apply (unfold_locales)
    by (auto intro!: distrib simp: list_all2_same_right)
next
  assume ?l
  then interpret sorted_distributive ‹unisorted_sig F› φ ‹unisorted A› I J.
  from source.sorted_algebra_axioms
  interpret source: algebra F A I by (unfold unisorted_algebra)
  show ?r
  proof unfold_locales
    fix f as
    show "(f, length as) ∈ F ⟹ set as ⊆ A ⟹ φ (I f as) = J f (map φ as)"
      using distrib[of f "replicate (length as) ()" _ as]
      by auto
  qed
qed

locale homomorphism =
  distributive F φ A I J + target: algebra F B J for F φ A I B J +
  assumes funcset: "φ : A → B"

lemma unisorted_homomorphism:
  "sorted_homomorphism (unisorted_sig F) φ (unisorted A) I (unisorted B) J ⟷
   homomorphism F φ A I B J" (is "?l ⟷ ?r")
  by (auto simp: sorted_homomorphism_def unisorted_distributive unisorted_algebra
      homomorphism_def homomorphism_axioms_def)

lemma homomorphism_cong:
  assumes φ: "⋀a. a ∈ A ⟹ φ a = φ' a"
    and A: "A = A'"
    and I: "⋀f as. (f, length as) ∈ F ⟹ I f as = I' f as"
    and B: "B = B'"
    and J: "⋀f bs. (f, length bs) ∈ F ⟹ J f bs = J' f bs"
  shows "homomorphism F φ A I B J = homomorphism F φ' A' I' B' J'"
proof-
  note sorted_homomorphism_cong
    [where F = "unisorted_sig F" and A = "unisorted A" and A' = "unisorted A'" and B = "unisorted B" and B' = "unisorted B'"]
  note * = this[unfolded unisorted_homomorphism]
  show ?thesis apply (rule *)
    by (auto simp: A B φ I J list_all2_same_right)
qed

context algebra begin

interpretation unisorted: sorted_algebra ‹unisorted_sig F› ‹unisorted A› I
  apply (unfold unisorted_algebra)..

lemma eval_homomorphism: "α : V → A ⟹ homomorphism F (λs. I⟦s⟧α) 𝔗(F,V) Fun A I"
  apply (fold unisorted_homomorphism)
  apply (fold unisorted_Term)
  apply (rule unisorted.eval_sorted_homomorphism)
  by auto

end

context homomorphism begin

interpretation unisorted: sorted_homomorphism ‹unisorted_sig F› φ ‹unisorted A› I ‹unisorted B› J
  apply (unfold unisorted_homomorphism)..

lemma distrib_eval: "α : V → A ⟹ s ∈ 𝔗(F,V) ⟹ φ (I⟦s⟧α) = J⟦s⟧(φ ∘ α)"
  using unisorted.distrib_eval[of _ "unisorted V"] by simp

end

text ‹By `unsorted' we mean the situation where any element has the unique type @{term "()"}.›

lemma Term_UNIV[simp]: "𝔗(UNIV,UNIV) = UNIV"
proof-
  have "s ∈ 𝔗(UNIV,UNIV)" for s by (induct s, auto)
  then show ?thesis by auto
qed

text ‹When the carrier is unsorted, any interpretation forms an algebra.›

interpretation unsorted: algebra UNIV UNIV I
  rewrites "⋀a. a ∈ UNIV ⟷ True"
    and "⋀P0. (True ⟹ P0) ≡ Trueprop P0"
    and "⋀P0. (True ⟹ PROP P0) ≡ PROP P0"
    and "⋀P0 P1. (True ⟹ PROP P1 ⟹ P0) ≡ (PROP P1 ⟹ P0)" 
  for F I
 apply unfold_locales by auto

interpretation unsorted.eval: homomorphism UNIV "λs. I⟦s⟧α" UNIV Fun UNIV I
  rewrites "⋀a. a ∈ UNIV ⟷ True"
    and "⋀X. X ⊆ UNIV ⟷ True"
    and "⋀P0. (True ⟹ P0) ≡ Trueprop P0"
    and "⋀P0. (True ⟹ PROP P0) ≡ PROP P0"
    and "⋀P0 P1. (True ⟹ PROP P1 ⟹ P0) ≡ (PROP P1 ⟹ P0)"
  for I
  using unsorted.eval_homomorphism[of _ UNIV] by auto

text ‹Evaluation distributes over evaluations in the term algebra, i.e., substitutions.›
lemma subst_eval: "I⟦s⋅θ⟧α = I⟦s⟧(λx. I⟦θ x⟧α)"
  using unsorted.eval.distrib_eval[of _ UNIV, unfolded o_def]
  by auto

lemmas subst_subst = subst_eval[of Fun]

subsubsection ‹Collecting Variables via Evaluation›

definition "var_list_term t ≡ (λf. concat)⟦t⟧(λv. [v])"

lemma var_list_Fun[simp]: "var_list_term (Fun f ss) = concat (map var_list_term ss)"
  and var_list_Var[simp]: "var_list_term (Var x) = [x]"
  by (simp_all add: var_list_term_def[abs_def])

lemma set_var_list[simp]: "set (var_list_term s) = vars s"
  by (induct s, auto simp: var_list_term_def)

lemma eval_subset_Un_vars:
  assumes "∀f as. foo (I f as) ⊆ ⋃(foo ` set as)"
  shows "foo (I⟦s⟧α) ⊆ (⋃x∈vars_term s. foo (α x))"
proof (induct s)
  case (Var x)
  show ?case by simp
next
  case (Fun f ss)
  have "foo (I⟦Fun f ss⟧α) = foo (I f (map (λs. I⟦s⟧α) ss))" by simp
  also note assms[rule_format]
  also have "⋃ (foo ` set (map (λs. I⟦s⟧α) ss)) = (⋃s∈set ss. foo (I⟦s⟧α))" by simp
  also have "… ⊆ (⋃s ∈ set ss. (⋃ x ∈ vars_term s. foo (α x)))"
    apply (rule UN_mono)
    using Fun by auto
  finally show ?case by simp
qed

subsubsection ‹Ground terms›

lemma hastype_in_Term_empty_imp_vars: "s : σ in 𝒯(F,∅) ⟹ vars s = {}" 
  by (auto dest: hastype_in_Term_imp_vars_subset)

lemma hastype_in_Term_empty_imp_vars_subst: "s : σ in 𝒯(F,∅) ⟹ vars (s⋅θ) = {}"
  by (auto simp: vars_term_subst_apply_term hastype_in_Term_empty_imp_vars)

lemma ground_Term_iff: "s : σ in 𝒯(F,V) ∧ ground s ⟷ s : σ in 𝒯(F,∅)"
  using hastype_in_Term_restrict_vars[of s σ F V]
  by (auto simp: hastype_in_Term_empty_imp_vars ground_vars_term_empty)

lemma hastype_in_Term_empty_imp_subst:
  "s : σ in 𝒯(F,∅) ⟹ s⋅θ : σ in 𝒯(F,V)"
  by (rule subst_hastype, auto)

locale subsignature = fixes F G :: "('f,'s) ssig" assumes subssig: "F ⊆⇩m G"
begin

lemmas Term_subsset = Term_mono_left[OF subssig]
lemmas hastype_in_Term_sub = Term_subsset[THEN subssetD]

lemma subsignature: "f : σs → τ in F ⟹ f : σs → τ in G"
  using subssig by (auto dest: subssigD)

end

locale subsignature_algebra = subsignature + super: sorted_algebra G
begin

sublocale sorted_algebra F A I
  apply unfold_locales
  using super.sort_matches[OF subssigD[OF subssig]] by auto

end

locale subalgebra = sorted_algebra F A I + super: sorted_algebra G B J +
  subsignature F G
  for F :: "('f,'s) ssig" and A :: "'a ⇀ 's" and I
  and G :: "('f,'s) ssig" and B :: "'a ⇀ 's" and J +
  assumes subcar: "A ⊆⇩m B"
  assumes subintp: "f : σs → τ in F ⟹ as :⇩l σs in A ⟹ I f as = J f as"
begin

lemma subcarrier: "a : σ in A ⟹ a : σ in B"
  using subcar by (auto dest: subssetD)

lemma subeval:
  assumes s: "s : σ in 𝒯(F,V)" and α: "α :⇩s V → A" shows "J⟦s⟧α = I⟦s⟧α"
proof (insert s, induct rule: hastype_in_Term_induct)
  case (Var v σ)
  then show ?case by auto
next
  case (Fun f ss σs τ)
  then show ?case
    by (auto simp: list_all2_indep2 cong:map_cong intro!:subintp[symmetric] map_eval_hastype α)
qed

end

lemma term_subalgebra:
  assumes FG: "F ⊆⇩m G" and VW: "V ⊆⇩m W"
  shows "subalgebra F 𝒯(F,V) Fun G 𝒯(G,W) Fun"
  apply unfold_locales
  using FG VW Term_mono[OF FG VW] by auto


text ‹ An algebra where every element has a representation: ›
locale sorted_algebra_constant = sorted_algebra_syntax +
  fixes const
  assumes vars_const[simp]: "⋀d. vars (const d) = {}"
  assumes eval_const[simp]: "⋀d α. I⟦const d⟧α = d"
begin

lemma eval_subst_const[simp]: "I⟦e⋅(const∘α)⟧β = I⟦e⟧α"
  by (induct e, auto simp:o_def intro!:arg_cong[of _ _ "I _"])

lemma eval_upd_as_subst: "I⟦e⟧α(x:=a) = I⟦e ⋅ Var(x:=const a)⟧α"
  by (induct e, auto simp: o_def intro: arg_cong[of _ _ "I _"])

end

context sorted_algebra_syntax begin

definition "constant_at f σs i ≡
  ∀as b. as :⇩l σs in A ⟶ A b = A (as!i) ⟶ I f (as[i:=b]) = I f as"

lemma constant_atI[intro]:
  assumes "⋀as b. as :⇩l σs in A ⟹ A b = A (as!i) ⟹ I f (as[i:=b]) = I f as"
  shows "constant_at f σs i" using assms by (auto simp: constant_at_def)

lemma constant_atD:
  "constant_at f σs i ⟹ as :⇩l σs in A ⟹ A b = A (as!i) ⟹ I f (as[i:=b]) = I f as"
  by (auto simp: constant_at_def)

lemma constant_atE[elim]:
  assumes "constant_at f σs i"
    and "(⋀as b. as :⇩l σs in A ⟹ A b = A (as!i) ⟹ I f (as[i:=b]) = I f as) ⟹ thesis"
  shows thesis using assms by (auto simp: constant_at_def)

definition "constant_term_on s x ≡ ∀α a. I⟦s⟧α(x:=a) = I⟦s⟧α"

lemma constant_term_onI:
  assumes "⋀α a. I⟦s⟧α(x:=a) = I⟦s⟧α" shows "constant_term_on s x"
  using assms by (auto simp: constant_term_on_def)

lemma constant_term_onD:
  assumes "constant_term_on s x" shows "I⟦s⟧α(x:=a) = I⟦s⟧α"
  using assms by (auto simp: constant_term_on_def)

lemma constant_term_onE:
  assumes "constant_term_on s x" and "(⋀α a. I⟦s⟧α(x:=a) = I⟦s⟧α) ⟹ thesis"
  shows thesis using assms by (auto simp: constant_term_on_def)

lemma constant_term_on_extra_var: "x ∉ vars s ⟹ constant_term_on s x"
  by (auto intro!: constant_term_onI simp: eval_with_fresh_var)

lemma constant_term_on_eq:
  assumes st: "I⟦s⟧ = I⟦t⟧" and s: "constant_term_on s x" shows "constant_term_on t x"
  using s fun_cong[OF st] by (auto simp: constant_term_on_def)

definition "constant_term s ≡ ∀x. constant_term_on s x"

lemma constant_termI: assumes "⋀x. constant_term_on s x" shows "constant_term s"
  using assms by (auto simp: constant_term_def)

lemma ground_imp_constant: "vars s = {} ⟹ constant_term s"
  by (auto intro!: constant_termI constant_term_on_extra_var)

end

end