Theory Mono

section‹Monotonicity›
theory Mono imports CM begin


subsection‹Fullness and infiniteness›

text‹In a structure, a full type is one that contains all elements of univ (the fixed countable universe):›

definition (in Tstruct) "full σ ≡ ∀ d. intT σ d"

locale FullStruct = F? : Struct +
assumes full: "full σ"
begin
lemma full2[simp]: "intT σ d"
using full unfolding full_def by simp

lemma full_True: "intT = (λ σ D. True)"
apply(intro ext) by auto
end

locale FullModel =
F? : Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP +
F? : FullStruct wtFsym wtPsym arOf resOf parOf intT intF intP
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and intT and intF and intP

text‹An infinite structure is one with all carriers infinite:›

locale InfStruct = I? : Struct +
assumes inf: "infinite {a. intT σ a}"

locale InfModel =
I? : Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP +
I? : InfStruct wtFsym wtPsym arOf resOf parOf intT intF intP
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and intT and intF and intP

context Problem begin
abbreviation "SStruct ≡ Struct wtFsym wtPsym arOf resOf"
abbreviation "FFullStruct ≡ FullStruct wtFsym wtPsym arOf resOf"
abbreviation "IInfStruct ≡ InfStruct wtFsym wtPsym arOf resOf"

abbreviation "MModel ≡ Model wtFsym wtPsym arOf resOf parOf Φ"
abbreviation "FFullModel ≡ FullModel wtFsym wtPsym arOf resOf parOf Φ"
abbreviation "IInfModel ≡ InfModel wtFsym wtPsym arOf resOf parOf Φ"
end

text‹Problem that deduces some infiniteness constraints:›

locale ProblemIk = Ik? : Problem wtFsym wtPsym arOf resOf parOf Φ
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ
+
fixes infTp :: "'tp ⇒ bool"
(* infTp assumes that Φ implies infiniteness on the infTp-marked types,
i.e., any model of Φ is infinite on these types: *)
assumes infTp:
"⋀ σ intT intF intP (a::univ). ⟦infTp σ; MModel intT intF intP⟧ ⟹ infinite {a. intT σ a}"

locale ModelIk =
Ik? : ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp +
Ik? : Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and infTp and intT and intF and intP
begin
lemma infTp_infinite[simp]: "infTp σ ⟹ infinite {a. intT σ a}"
apply(rule ProblemIk.infTp[of wtFsym wtPsym arOf resOf parOf Φ infTp])
apply unfold_locales by simp
end


subsection‹Monotonicity›

context Problem begin
(* Monotonicity: *)
definition
"monot ≡
 (∃ intT intF intP. MModel intT intF intP)
 ⟶
 (∃ intTI intFI intPI. IInfModel intTI intFI intPI)"
end

locale MonotProblem = Problem +
assumes monot: monot

locale MonotProblemIk =
MonotProblem wtFsym wtPsym arOf resOf parOf Φ +
ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list" and resOf and parOf and Φ and infTp

context MonotProblem
begin

definition "MI_pred K ≡ IInfModel (fst3 K) (snd3 K) (trd3 K)"

definition "MI ≡ SOME K. MI_pred K"

lemma MI_pred:
assumes "MModel intT intF intP"
shows "∃ K. MI_pred K"
proof-
  obtain T F R where "MI_pred (T,F,R)"
  using monot assms unfolding monot_def MI_pred_def by auto
  thus ?thesis by blast
qed

lemma MI_pred_MI:
assumes "MModel intT intF intP"
shows "MI_pred MI"
using MI_pred[OF assms] unfolding MI_def by (rule someI_ex)

definition "intTI ≡ fst3 MI"
definition "intFI ≡ snd3 MI"
definition "intPI ≡ trd3 MI"

lemma InfModel_intTI_intFI_intPI:
assumes "MModel intT intF intP"
shows "IInfModel intTI intFI intPI"
using MI_pred_MI[OF assms]
unfolding MI_pred_def intFI_def intPI_def intTI_def .

end (* context MonotProblem *)

locale MonotModel = M? : MonotProblem + M? : Model

context MonotModel begin

lemma InfModelI: "IInfModel intTI intFI intPI"
apply(rule MonotProblem.InfModel_intTI_intFI_intPI)
apply standard
done

end

(* Trivial fact: Any monotonic problem that has a model also has an infinite model: *)
sublocale MonotModel < InfModel where
intT = intTI and intF = intFI and intP = intPI
using InfModelI .


context InfModel begin

definition "toFull σ ≡ SOME F. bij_betw F {a::univ. intT σ a} (UNIV::univ set)"
definition "fromFull σ ≡ inv_into {a::univ. intT σ a} (toFull σ)"

definition "intTF σ a ≡ True"
definition "intFF f al ≡ toFull (resOf f) (intF f (map2 fromFull (arOf f) al))"
definition "intPF p al ≡ intP p (map2 fromFull (parOf p) al)"

lemma intTF: "intTF σ a"
unfolding intTF_def by auto

lemma ex_toFull: "∃ F. bij_betw F {a::univ. intT σ a} (UNIV::univ set)"
by (metis inf card_of_ordIso card_of_UNIV countable_univ UnE
          countable_infinite not_ordLeq_ordLess ordLeq_ordLess_Un_ordIso)

lemma toFull: "bij_betw (toFull σ) {a. intT σ a} UNIV"
by (metis (lifting) ex_toFull someI_ex toFull_def)

lemma toFull_fromFull[simp]: "toFull σ (fromFull σ a) = a"
by (metis UNIV_I bij_betw_inv_into_right fromFull_def toFull)

lemma fromFull_toFull[simp]: "intT σ a ⟹ fromFull σ (toFull σ a) = a"
by (metis CollectI bij_betw_inv_into_left toFull fromFull_def)

lemma fromFull_inj[simp]: "fromFull σ a = fromFull σ b ⟷ a = b"
by (metis toFull_fromFull)

lemma toFull_inj[simp]:
assumes "intT σ a" and "intT σ b"
shows "toFull σ a = toFull σ b ⟷ a = b"
by (metis assms fromFull_toFull)

lemma fromFull[simp]: "intT σ (fromFull σ a)"
unfolding fromFull_def
apply(rule inv_into_into[of a "toFull σ" "{a. intT σ a}", simplified])
using toFull unfolding bij_betw_def by auto

lemma toFull_iff_fromFull:
assumes "intT σ a"
shows "toFull σ a = b ⟷ a = fromFull σ b"
by (metis assms fromFull_toFull toFull_fromFull)

lemma Tstruct: "Tstruct intTF"
apply(unfold_locales) unfolding intTF_def by simp

lemma FullStruct: "FullStruct wtFsym wtPsym arOf resOf intTF intFF intPF"
apply (unfold_locales) unfolding intTF_def Tstruct.full_def[OF Tstruct] by auto

end (* locale InfModel *)

sublocale InfModel < FullStruct
where intT = intTF and intF = intFF and intP = intPF
using FullStruct .


context InfModel begin

definition "kE ξ ≡ λ x. fromFull (tpOfV x) (ξ x)"

lemma kE[simp]: "kE ξ x = fromFull (tpOfV x) (ξ x)"
unfolding kE_def by simp

lemma wtE[simp]: "F.wtE ξ"
unfolding F.wtE_def by simp

lemma kE_wtE[simp]: "I.wtE (kE ξ)"
unfolding I.wtE_def kE_def by simp

lemma kE_int_toFull:
assumes ξ: "I.wtE (kE ξ)" and T: "wt T"
shows "toFull (tpOf T) (I.int (kE ξ) T) = F.int ξ T"
using T proof(induct T)
  case (Fn f Tl)
  have 0: "map (I.int (kE ξ)) Tl =
           map2 fromFull (arOf f) (map (F.int ξ) Tl)"
  (is "map ?F Tl = map2 fromFull (arOf f) (map ?H Tl)"
   is "?L = ?R")
  proof(rule nth_equalityI)
    have l: "length Tl = length (arOf f)" using Fn by simp
    thus "length ?L = length ?R" by simp
    fix i assume "i < length ?L"  hence i: "i < length Tl" by simp
    let ?toFull = "toFull (arOf f!i)"   let ?fromFull = "fromFull (arOf f!i)"
    have tp: "tpOf (Tl ! i) = arOf f ! i" using Fn(2) i unfolding list_all_length by auto
    have wt: "wt (Tl!i)" using Fn i by (auto simp: list_all_iff)
    have "intT (arOf f!i) (?F (Tl!i))" using I.wt_int[OF ξ wt] unfolding tp .
    moreover have "?toFull (?F (Tl!i)) = ?H (Tl!i)"
      using Fn tp i by (auto simp: list_all_iff kE_def)
    ultimately have "?F (Tl!i) = fromFull (arOf f!i) (?H (Tl!i))"
      using toFull_iff_fromFull by blast
    thus "?L!i = ?R!i" using l i by simp
  qed
  show ?case unfolding I.int.simps F.int.simps tpOf.simps unfolding intFF_def 0 ..
qed simp

lemma kE_int[simp]:
assumes ξ: "I.wtE (kE ξ)" and T: "wt T"
shows "I.int (kE ξ) T = fromFull (tpOf T) (F.int ξ T)"
using kE_int_toFull[OF assms]
unfolding toFull_iff_fromFull[OF I.wt_int[OF ξ T]] .

lemma map_kE_int[simp]:
  assumes ξ: "I.wtE (kE ξ)" and T: "list_all wt Tl"
  shows "map (I.int (kE ξ)) Tl = map2 fromFull (map tpOf Tl) (map (F.int ξ) Tl)"
  apply(rule nth_equalityI)
   apply (metis (lifting) length_map length_map2)
  by (metis T ξ kE_int length_map list_all_length nth_map nth_map2)

lemma kE_satA[simp]:
assumes at: "wtA at" and ξ: "I.wtE (kE ξ)"
shows "I.satA (kE ξ) at ⟷ F.satA ξ at"
using assms by (cases at, auto simp add: intPF_def)

lemma kE_satL[simp]:
assumes l: "wtL l" and ξ: "I.wtE (kE ξ)"
shows "I.satL (kE ξ) l ⟷ F.satL ξ l"
using assms by (cases l, auto)

lemma kE_satC[simp]:
assumes c: "wtC c" and ξ: "I.wtE (kE ξ)"
shows "I.satC (kE ξ) c ⟷ F.satC ξ c"
unfolding I.satC_def F.satC_def
using assms by(induct c, auto simp add: wtC_def)

lemma kE_satPB:
assumes ξ: "I.wtE (kE ξ)"  shows "F.satPB ξ Φ"
using I.sat_Φ[OF assms]
using wt_Φ assms unfolding I.satPB_def F.satPB_def
by (auto simp add: wtPB_def)

lemma F_SAT: "F.SAT Φ"
unfolding F.SAT_def using kE_satPB kE_wtE by auto

lemma FullModel: "FullModel wtFsym wtPsym arOf resOf parOf Φ intTF intFF intPF"
apply (unfold_locales) using F_SAT .

end (* context InfModel *)

sublocale InfModel < FullModel where
intT = intTF and intF = intFF and intP = intPF
using FullModel .


context MonotProblem begin

definition "intTF ≡ InfModel.intTF"
definition "intFF ≡ InfModel.intFF arOf resOf intTI intFI"
definition "intPF ≡ InfModel.intPF parOf intTI intPI"

text‹Strengthening of the infiniteness condition for monotonicity,
replacing infininetess by fullness:›

theorem FullModel_intTF_intFF_intPF:
assumes "MModel intT intF intP"
shows "FFullModel intTF intFF intPF"
unfolding intTF_def intFF_def intPF_def
apply(rule InfModel.FullModel) using InfModel_intTI_intFI_intPI[OF assms] .

end (* context MonotProblem *)

sublocale MonotModel < FullModel where
intT = intTF and intF = intFF and intP = intPF
using FullModel .

end