Theory Sig

section ‹Many-Typed (Many-Sorted) First-Order Logic›
theory Sig imports Preliminaries
begin

text‹In this formalization, we call ``types" what the first-order logic community usually calls ``sorts".› 


subsection‹Signatures› 

locale Signature =
fixes
    wtFsym :: "'fsym ⇒ bool"
and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf :: "'fsym ⇒ 'tp"
and parOf :: "'psym ⇒ 'tp list"
assumes
    countable_tp: "countable (UNIV :: 'tp set)"
and countable_wtFsym: "countable {f::'fsym. wtFsym f}"
and countable_wtPsym: "countable {p::'psym. wtPsym p}"
begin

text‹Partitioning of the variables in countable sets for each type:›

definition tpOfV_pred :: "(var ⇒ 'tp) ⇒ bool" where
"tpOfV_pred f ≡ ∀ σ. infinite (f -` {σ})"

definition "tpOfV ≡ SOME f. tpOfV_pred f"

lemma infinite_fst_vimage:
"infinite ((fst :: 'a × nat ⇒ 'a) -` {a})" (is "infinite (?f -` {a})")
proof-
  have "?f -` {a} = {(a,n::nat) | n . True}" (is "_ = ?A") by auto
  moreover
  {have 0: "?A = range (Pair a)" by auto
   have "infinite ?A" unfolding 0 apply(rule range_inj_infinite)
   unfolding inj_on_def by auto
  }
  ultimately show ?thesis by auto
qed

lemma tpOfV_pred: "∃ f. tpOfV_pred f"
proof-
  define Ut Uv where "Ut = (UNIV :: 'tp set)" and "Uv = (UNIV :: var set)"
  define Unt where "Unt = (UNIV :: nat set)"
  define U2 where "U2 = (UNIV :: ('tp × nat) set)"
  have U2: "U2 ≡ Ut × Unt" unfolding Ut_def Unt_def U2_def UNIV_Times_UNIV .
  have "|U2| =o |Unt × Ut|" unfolding U2 by (metis card_of_Times_commute)
  also have "|Unt × Ut| =o |Unt|"
  apply(rule card_of_Times_infinite_simps(1)) unfolding Ut_def Unt_def
  apply (metis nat_not_finite)
  apply (metis UNIV_not_empty)
  by (metis countable_card_of_nat countable_tp)
  also have "|Unt| =o |Uv|" apply(rule ordIso_symmetric)
  unfolding Unt_def Uv_def using card_of_var card_of_nat[THEN ordIso_symmetric]
  by(rule ordIso_transitive)
  finally have "|U2| =o |Uv|" .
  hence "|Uv| =o |U2|" by(rule ordIso_symmetric)
  then obtain g where g: "bij_betw g Uv U2" unfolding card_of_ordIso[symmetric] by blast
  show ?thesis apply(rule exI[of _ "fst o g"]) unfolding tpOfV_pred_def apply safe
  unfolding vimage_comp [symmetric] apply (drule finite_vimageD)
  using g unfolding bij_betw_def Uv_def U2_def by (auto simp: infinite_fst_vimage)
qed

lemma tpOfV_pred_tpOfV: "tpOfV_pred tpOfV"
using tpOfV_pred unfolding tpOfV_def by (rule someI_ex)

lemma tpOfV: "infinite (tpOfV -` {σ})"
using tpOfV_pred_tpOfV unfolding tpOfV_pred_def by auto

definition "tpart1 V ≡ ⋃ σ. part1 (V ∩ tpOfV -` {σ})"
definition "tpart2 V ≡ ⋃ σ. part2 (V ∩ tpOfV -` {σ})"
definition "tinfinite V ≡ ∀ σ. infinite (V ∩ tpOfV -` {σ})"

lemma tinfinite_var[simp,intro]: "tinfinite (UNIV :: var set)"
unfolding tinfinite_def using tpOfV by auto

lemma tinifnite_singl[simp]:
assumes "tinfinite V"  shows "tinfinite (V - {x})"
unfolding tinfinite_def proof safe
  fix σ assume 0: "finite ((V - {x}) ∩ tpOfV -` {σ})"
  have "finite ((V ∩ tpOfV -` {σ}) - {x})" apply(rule finite_subset[OF _ 0]) by auto
  thus False using assms unfolding tinfinite_def by auto
qed

lemma tpart1_Un_tpart2[simp]:
assumes "tinfinite V" shows "tpart1 V ∪ tpart2 V = V"
using assms part1_Un_part2 unfolding tinfinite_def tpart1_def tpart2_def
unfolding UN_Un_distrib[symmetric] by blast

lemma tpart1_Int_tpart2[simp]:
assumes "tinfinite V" shows "tpart1 V ∩ tpart2 V = {}"
using assms part1_Int_part2 unfolding tinfinite_def tpart1_def tpart2_def
unfolding Int_UN_distrib2 apply auto apply (case_tac "xa = xb", auto)
using part1_su part2_su by blast (* fixme: clean proof *)

lemma tpart1_su:
assumes "tinfinite V"  shows "tpart1 V ⊆ V"
using assms unfolding tinfinite_def tpart1_def
using part1_su by (auto intro: UN_least)

lemma tpart1_in:
assumes "tinfinite V" and "x ∈ tpart1 V" shows "x ∈ V"
using assms tpart1_su by auto

lemma tinfinite_tpart1[simp]:
assumes "tinfinite V"
shows "tinfinite (tpart1 V)"
unfolding tinfinite_def tpart1_def proof safe
  fix σ assume
  "finite ((⋃σ'. part1 (V ∩ tpOfV -` {σ'})) ∩ tpOfV -` {σ})" (is "finite ?A")
  moreover have "?A = part1 (V ∩ tpOfV -` {σ})"
  using assms part1_su unfolding tinfinite_def by auto
  moreover have "infinite ..."
  using assms infinite_part1 unfolding tinfinite_def by auto
  ultimately show False by auto
qed

lemma tinfinite_tpart2[simp]:
assumes "tinfinite V"
shows "tinfinite (tpart2 V)"
unfolding tinfinite_def tpart2_def proof safe
  fix σ assume
  "finite ((⋃σ'. part2 (V ∩ tpOfV -` {σ'})) ∩ tpOfV -` {σ})" (is "finite ?A")
  moreover have "?A = part2 (V ∩ tpOfV -` {σ})"
  using assms part2_su unfolding tinfinite_def by auto
  moreover have "infinite ..."
  using assms infinite_part2 unfolding tinfinite_def by auto
  ultimately show False by auto
qed

lemma tpart2_su:
assumes "tinfinite V"  shows "tpart2 V ⊆ V"
using assms unfolding tinfinite_def tpart2_def
using part2_su by (auto intro: UN_least)

lemma tpart2_in:
assumes "tinfinite V" and "x ∈ tpart2 V" shows "x ∈ V"
using assms tpart2_su by auto

text‹Typed-pick: picking a variable of a given type›

definition "tpick σ V ≡ pick (V ∩ tpOfV -` {σ})"

lemma tinfinite_ex: "tinfinite V ⟹ ∃ x ∈ V. tpOfV x = σ"
unfolding tinfinite_def using infinite_imp_nonempty by auto

lemma tpick: assumes "tinfinite V" shows "tpick σ V ∈ V ∩ tpOfV -` {σ}"
proof-
  obtain x where "x ∈ V ∧ tpOfV x = σ"
  using tinfinite_ex[OF assms] by auto
  hence "x ∈ V ∩ tpOfV -` {σ}" by blast
  thus ?thesis unfolding tpick_def by (rule pick)
qed

lemma tpick_in[simp]: "tinfinite V ⟹ tpick σ V ∈ V"
and tpOfV_tpick[simp]: "tinfinite V ⟹ tpOfV (tpick σ V) = σ"
using tpick by auto

lemma finite_tinfinite:
assumes "finite V"
shows "tinfinite (UNIV - V)"
using assms infinite_var unfolding tinfinite_def
by (metis Diff_Int2 Diff_Int_distrib2 Int_UNIV_left finite_Diff2 tpOfV)

(* get variable terms for the given types: *)
fun getVars where
"getVars [] = []"
|
"getVars (σ # σl) =
 (let xl = getVars σl in (tpick σ (UNIV - set xl)) # xl)"

lemma distinct_getVars: "distinct (getVars σl)"
using tpick_in[OF finite_tinfinite] by (induct σl, auto simp: Let_def)

lemma length_getVars[simp]: "length (getVars σl) = length σl"
by(induct σl, auto simp: Let_def)

lemma map_tpOfV_getVars[simp]: "map tpOfV (getVars σl) = σl"
using tpOfV_tpick[OF finite_tinfinite] by (induct σl, auto simp: Let_def)

lemma tpOfV_getVars_nth[simp]:
assumes "i < length σl"  shows "tpOfV (getVars σl ! i) = σl ! i"
using assms using map_tpOfV_getVars by (metis length_getVars nth_map)


end (* context Signature *)


end