Theory M

theory M
imports TermsAndClauses Sig
begin  


subsection‹Well-typed (well-formed) terms, clauses, literals and problems›

context Signature begin

text‹The type of a term›
fun tpOf where
"tpOf (Var x) = tpOfV x"
|
"tpOf (Fn f Tl) = resOf f"

(* Well-typed terms *)
fun wt where
"wt (Var x) ⟷ True"
|
"wt (Fn f Tl) ⟷
 wtFsym f ∧ list_all wt Tl ∧ arOf f = map tpOf Tl"

(* Well-typed atoms (atomic formulas) *)
fun wtA where
"wtA (Eq T1 T2) ⟷ wt T1 ∧ wt T2 ∧ tpOf T1 = tpOf T2"
|
"wtA (Pr p Tl) ⟷
 wtPsym p ∧ list_all wt Tl ∧ parOf p = map tpOf Tl"

(* Well-typed literals *)
fun wtL where
"wtL (Pos a) ⟷ wtA a"
|
"wtL (Neg a) ⟷ wtA a"

(* Well-typed clauses *)
definition "wtC ≡ list_all wtL"

lemma wtC_append[simp]: "wtC (c1 @ c2) ⟷ wtC c1 ∧ wtC c2"
unfolding wtC_def by simp

(* Well-typed problems *)
definition "wtPB Φ ≡ ∀ c ∈ Φ. wtC c"

lemma wtPB_Un[simp]: "wtPB (Φ1 ∪ Φ2) ⟷ wtPB Φ1 ∧ wtPB Φ2"
unfolding wtPB_def by auto

lemma wtPB_UN[simp]: "wtPB (⋃ i ∈ I. Φ i) ⟷ (∀ i ∈ I. wtPB (Φ i))"
unfolding wtPB_def by auto

lemma wtPB_sappend[simp]:
assumes "wtPB Φ1" and "wtPB Φ2"  shows "wtPB (Φ1 @@ Φ2)"
using assms unfolding wtPB_def sappend_def by auto

(* Well-typed substitutions *)
definition "wtSB π ≡ ∀ x. wt (π x) ∧ tpOf (π x) = tpOfV x"

lemma wtSB_wt[simp]: "wtSB π ⟹ wt (π x)"
unfolding wtSB_def by auto

lemma wtSB_tpOf[simp]: "wtSB π ⟹ tpOf (π x) = tpOfV x"
unfolding wtSB_def by auto

lemma wt_tpOf_subst:
assumes "wtSB π" and "wt T"
shows "wt (subst π T) ∧ tpOf (subst π T) = tpOf T"
using assms apply(induct T) by (auto simp add: list_all_iff)

lemmas wt_subst[simp] = wt_tpOf_subst[THEN conjunct1]
lemmas tpOf_subst[simp] = wt_tpOf_subst[THEN conjunct2]

lemma wtSB_o:
assumes 1: "wtSB π1" and 2: "wtSB π2"
shows "wtSB (subst π1 o π2)"
using 2 unfolding wtSB_def using 1 by auto

(* Getting variable terms for given types: *)
definition "getTvars σl ≡ map Var (getVars σl)"

lemma length_getTvars[simp]: "length (getTvars σl) = length σl"
unfolding getTvars_def by auto

lemma wt_getTvars[simp]: "list_all wt (getTvars σl)"
unfolding list_all_length getTvars_def by simp

lemma wt_nth_getTvars[simp]:
"i < length σl ⟹ wt (getTvars σl ! i)"
unfolding getTvars_def by auto

lemma map_tpOf_getTvars[simp]: "map tpOf (getTvars σl) = σl"
unfolding getTvars_def unfolding list_eq_iff by auto

lemma tpOf_nth_getTvars[simp]:
"i < length σl ⟹ tpOf (getTvars σl ! i) = σl ! i"
unfolding getTvars_def by auto

end (* context Signature *)


subsection ‹Structures›

text‹We split a structre into a ``type structure'' that interprets the types 
and the rest of the structure that interprets the function and relation symbols.›

text‹Type structures:›

locale Tstruct =
fixes intT :: "'tp ⇒ 'univ ⇒ bool"
assumes NE_intT: "NE (intT σ)"

text‹Environment:›

type_synonym ('tp,'univ) env = "'tp ⇒ var ⇒ 'univ"

text‹Structures:›

locale Struct = Signature wtFsym wtPsym arOf resOf parOf +
                Tstruct intT
for wtFsym and wtPsym
and arOf :: "'fsym ⇒ 'tp list"
and resOf :: "'fsym ⇒ 'tp"
and parOf :: "'psym ⇒ 'tp list"
and intT :: "'tp ⇒ 'univ ⇒ bool"
+
fixes
    intF :: "'fsym ⇒ 'univ list ⇒ 'univ"
and intP :: "'psym ⇒ 'univ list ⇒ bool"
assumes
intF: "⟦wtFsym f; list_all2 intT (arOf f) al⟧ ⟹ intT (resOf f) (intF f al)"
and
dummy: "intP = intP"
begin

text‹Well-typed environment:›

definition "wtE ξ ≡ ∀ x. intT (tpOfV x) (ξ x)"

lemma wtTE_intT[simp]: "wtE ξ ⟹ intT (tpOfV x) (ξ x)"
unfolding wtE_def dom_def by auto

(* Picking an element from the domain of a given type: *)
definition "pickT σ ≡ SOME a. intT σ a"

lemma pickT[simp]: "intT σ (pickT σ)"
unfolding pickT_def apply(rule someI_ex) using NE_intT by auto

text‹Picking a well-typed environment:›

definition
"pickE (xl::var list) al ≡
 SOME ξ. wtE ξ ∧ (∀ i < length xl. ξ (xl!i) = al!i)"

lemma ex_pickE:
assumes "length xl = length al"
and "distinct xl" and "⋀ i. i < length xl ⟹ intT (tpOfV (xl!i)) (al!i)"
shows "∃ ξ. wtE ξ ∧ (∀ i < length xl. ξ (xl!i) = al!i)"
using assms
proof(induct rule: list_induct2)
  case Nil show ?case apply(rule exI[of _ "λ x. pickT (tpOfV x)"])
  unfolding wtE_def by auto
next
  case (Cons x xl a al)
  then obtain ξ where 1: "wtE ξ" and 2: "∀ i < length xl. ξ (xl!i) = al!i" by force
  define ξ' where "ξ' x' = (if x = x' then a else ξ x')" for x'
  show ?case
  proof(rule exI[of _ ξ'], unfold wtE_def, safe)
    fix x' show "intT (tpOfV x') (ξ' x')"
    using 1 Cons.prems(2)[of 0] unfolding ξ'_def by auto
  next
    fix i assume i: "i < length (x # xl)"
    thus "ξ' ((x # xl) ! i) = (a # al) ! i"
    proof(cases i)
      case (Suc j) hence j: "j < length xl" using i by auto
      have "¬ x = (x # xl) ! i" using Suc i Cons.prems(1) by auto
      thus ?thesis using Suc using j Cons.prems(1) Cons.hyps 2 unfolding ξ'_def by auto
    qed(insert Cons.prems(1) Cons.hyps 2, unfold ξ'_def, simp)
  qed
qed

lemma wtE_pickE_pickE:
assumes "length xl = length al"
and "distinct xl" and "⋀ i. i < length xl ⟹ intT (tpOfV (xl!i)) (al!i)"
shows "wtE (pickE xl al) ∧ (∀ i. i < length xl ⟶ pickE xl al (xl!i) = al!i)"
proof-
  let ?phi = "λ ξ. wtE ξ ∧ (∀ i < length xl. ξ (xl!i) = al!i)"
  show ?thesis unfolding pickE_def apply(rule someI_ex[of ?phi])
  using ex_pickE[OF assms] by simp
qed

lemmas wtE_pickE[simp] = wtE_pickE_pickE[THEN conjunct1]

lemma pickE[simp]:
assumes "length xl = length al"
and "distinct xl" and "⋀ i. i < length xl ⟹ intT (tpOfV (xl!i)) (al!i)"
and "i < length xl"
shows "pickE xl al (xl!i) = al!i"
using assms wtE_pickE_pickE by auto

definition "pickAnyE ≡ pickE [] []"

lemma wtE_pickAnyE[simp]: "wtE pickAnyE"
unfolding pickAnyE_def by (rule wtE_pickE) auto

(* Interpretation of terms: *)
fun int where
"int ξ (Var x) = ξ x"
|
"int ξ (Fn f Tl) = intF f (map (int ξ) Tl)"

(* Satisfaction of atoms: *)
fun satA where
"satA ξ (Eq T1 T2) ⟷ int ξ T1 = int ξ T2"
|
"satA ξ (Pr p Tl) ⟷ intP p (map (int ξ) Tl)"

(* Satisfaction literals: *)
fun satL where
"satL ξ (Pos a) ⟷ satA ξ a"
|
"satL ξ (Neg a) ⟷ ¬ satA ξ a"

(* Satisfaction of clauses: *)
definition "satC ξ ≡ list_ex (satL ξ)"

lemma satC_append[simp]: "satC ξ (c1 @ c2) ⟷ satC ξ c1 ∨ satC ξ c2"
unfolding satC_def by auto

lemma satC_iff_set: "satC ξ c ⟷ (∃ l ∈ set c. satL ξ l)"
unfolding satC_def Bex_set[symmetric] ..

(* satisfaction of problems *)
definition "satPB ξ Φ ≡ ∀ c ∈ Φ. satC ξ c"

lemma satPB_Un[simp]: "satPB ξ (Φ1 ∪ Φ2) ⟷ satPB ξ Φ1 ∧ satPB ξ Φ2"
unfolding satPB_def by auto

lemma satPB_UN[simp]: "satPB ξ (⋃ i ∈ I. Φ i) ⟷ (∀ i ∈ I. satPB ξ (Φ i))"
unfolding satPB_def by auto

lemma satPB_sappend[simp]: "satPB ξ (Φ1 @@ Φ2) ⟷ satPB ξ Φ1 ∨ satPB ξ Φ2"
unfolding satPB_def sappend_def by (fastforce simp: satC_append)

definition "SAT Φ ≡ ∀ ξ. wtE ξ ⟶ satPB ξ Φ"

lemma SAT_UN[simp]: "SAT (⋃ i ∈ I. Φ i) ⟷ (∀ i ∈ I. SAT (Φ i))"
unfolding SAT_def by auto

text‹Soundness of typing w.r.t. interpretation:›

lemma wt_int:
assumes wtE: "wtE ξ" and wt: "wt T"
shows "intT (tpOf T) (int ξ T)"
using wt apply(induct T) using wtE
by (auto intro!: intF simp add: list_all2_map_map)

lemma int_cong:
assumes "⋀x. x ∈ vars T ⟹ ξ1 x = ξ2 x"
shows "int ξ1 T = int ξ2 T"
using assms proof(induct T)
  case (Fn f Tl)
  hence 1: "map (int ξ1) Tl = map (int ξ2) Tl"
  unfolding list_all_iff by (auto intro: map_ext)
  show ?case apply simp by (metis 1)
qed auto

lemma satA_cong:
assumes "⋀x. x ∈ varsA at ⟹ ξ1 x = ξ2 x"
shows "satA ξ1 at ⟷ satA ξ2 at"
using assms int_cong[of _ ξ1 ξ2]
apply(cases at) apply(fastforce intro!: int_cong[of _ ξ1 ξ2])
apply simp by (metis (opaque_lifting, mono_tags) map_eq_conv)

lemma satL_cong:
assumes "⋀ x. x ∈ varsL l ⟹ ξ1 x = ξ2 x"
shows "satL ξ1 l ⟷ satL ξ2 l"
using assms satA_cong[of _ ξ1 ξ2] by (cases l, auto)

lemma satC_cong:
assumes "⋀ x. x ∈ varsC c ⟹ ξ1 x = ξ2 x"
shows "satC ξ1 c ⟷ satC ξ2 c"
using assms satL_cong[of _ ξ1 ξ2] unfolding satC_def varsC_def
apply (induct c) by (fastforce intro!: satL_cong[of _ ξ1 ξ2])+

lemma satPB_cong:
assumes "⋀ x. x ∈ varsPB Φ ⟹ ξ1 x = ξ2 x"
shows "satPB ξ1 Φ ⟷ satPB ξ2 Φ"
by (force simp: satPB_def varsPB_def intro!: satC_cong ball_cong assms)

lemma int_o:
"int (int ξ o ρ) T = int ξ (subst ρ T)"
apply(induct T) apply simp_all unfolding list_all_iff o_def
using map_ext by (metis (lifting, no_types))

lemmas int_subst = int_o[symmetric]

lemma int_o_subst:
"int ξ o subst ρ = int (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding int_o[symmetric] ..

lemma satA_o:
"satA (int ξ o ρ) at = satA ξ (substA ρ at)"
by (cases at, simp_all add: int_o_subst int_o[of ξ ρ])

lemmas satA_subst = satA_o[symmetric]

lemma satA_o_subst:
"satA ξ o substA ρ = satA (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satA_o[symmetric] ..

lemma satL_o:
"satL (int ξ o ρ) l = satL ξ (substL ρ l)"
using satA_o[of ξ ρ] by (cases l, simp_all)

lemmas satL_subst = satL_o[symmetric]

lemma satL_o_subst:
"satL ξ o substL ρ = satL (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satL_o[symmetric] ..

lemma satC_o:
"satC (int ξ o ρ) c = satC ξ (substC ρ c)"
using satL_o[of ξ ρ] unfolding satC_def substC_def by (induct c, auto)

lemmas satC_subst = satC_o[symmetric]

lemma satC_o_subst:
"satC ξ o substC ρ = satC (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satC_o[symmetric] ..

lemma satPB_o:
"satPB (int ξ o ρ) Φ = satPB ξ (substPB ρ Φ)"
using satC_o[of ξ ρ] unfolding satPB_def substPB_def by auto

lemmas satPB_subst = satPB_o[symmetric]

lemma satPB_o_subst:
"satPB ξ o substPB ρ = satPB (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satPB_o[symmetric] ..

lemma wtE_o:
assumes 1: "wtE ξ" and 2: "wtSB ρ"
shows "wtE (int ξ o ρ)"
unfolding wtE_def proof
  fix x have 0: "tpOfV x = tpOf (ρ x)" using 2 by auto
  show "intT (tpOfV x) ((int ξ ∘ ρ) x)" apply(subst 0) unfolding comp_def
  apply(rule wt_int[OF 1]) using 2 by auto
qed

(* fixme: unify compE and int ξ o ρ, since they are the same *)
definition "compE ρ ξ x ≡ int ξ (ρ x)"

lemma wtE_compE:
assumes "wtSB ρ" and "wtE ξ"  shows "wtE (compE ρ ξ)"
unfolding wtE_def using assms wt_int
unfolding wtSB_def compE_def by fastforce

lemma compE_upd: "compE (ρ (x := T)) ξ = (compE ρ ξ) (x := int ξ T)"
unfolding compE_def[abs_def] by auto

end (* context Struct *)


context Signature begin

(* The function symbols of: *)

fun fsyms where
"fsyms (Var x) = {}"
|
"fsyms (Fn f Tl) = {f} ∪ ⋃ (set (map fsyms Tl))"

fun fsymsA where
"fsymsA (Eq T1 T2) = fsyms T1 ∪ fsyms T2"
|
"fsymsA (Pr p Tl) = ⋃ (set (map fsyms Tl))"

fun fsymsL where
"fsymsL (Pos at) = fsymsA at"
|
"fsymsL (Neg at) = fsymsA at"

definition "fsymsC c = ⋃ (set (map fsymsL c))"

definition "fsymsPB Φ = ⋃ {fsymsC c | c. c ∈ Φ}"

lemma fsyms_int_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "⋀ f. f ∈ fsyms T ⟹ intF1 f = intF2 f"
shows "Struct.int intF1 ξ T = Struct.int intF2 ξ T"
using 0 proof(induct T)
  case (Fn f Tl)
  hence 1: "map (Struct.int intF1 ξ) Tl = map (Struct.int intF2 ξ) Tl"
  unfolding list_all_iff map_ext by auto
  show ?case 
  using Fn Struct.int.simps[OF S1, of ξ] Struct.int.simps[OF S2, of ξ] apply simp
  using 1 by metis
qed (auto simp: Struct.int.simps[OF S1, of ξ] Struct.int.simps[OF S2, of ξ])

lemma fsyms_satA_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "⋀ f. f ∈ fsymsA at ⟹ intF1 f = intF2 f"
shows "Struct.satA intF1 intP ξ at ⟷ Struct.satA intF2 intP ξ at"
using 0 fsyms_int_cong[OF S1 S2]
apply(cases at)
apply(fastforce intro!: fsyms_int_cong[OF S1 S2, of _ ξ]
                simp: Struct.satA.simps[OF S1, of ξ] Struct.satA.simps[OF S2, of ξ])
apply (simp add: Struct.satA.simps[OF S1, of ξ] Struct.satA.simps[OF S2, of ξ])
by (metis (opaque_lifting, mono_tags) map_eq_conv)

lemma fsyms_satL_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "⋀ f. f ∈ fsymsL l ⟹ intF1 f = intF2 f"
shows "Struct.satL intF1 intP ξ l ⟷ Struct.satL intF2 intP ξ l"
using 0 fsyms_satA_cong[OF S1 S2]
by (cases l, auto simp: Struct.satL.simps[OF S1, of ξ] Struct.satL.simps[OF S2, of ξ])

lemma fsyms_satC_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "⋀ f. f ∈ fsymsC c ⟹ intF1 f = intF2 f"
shows "Struct.satC intF1 intP ξ c ⟷ Struct.satC intF2 intP ξ c"
using 0 fsyms_satL_cong[OF S1 S2]
unfolding Struct.satC_def[OF S1] Struct.satC_def[OF S2] fsymsC_def
apply (induct c) by (fastforce intro!: fsyms_satL_cong[OF S1 S2])+

lemma fsyms_satPB_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "⋀ f. f ∈ fsymsPB Φ ⟹ intF1 f = intF2 f"
shows "Struct.satPB intF1 intP ξ Φ ⟷ Struct.satPB intF2 intP ξ Φ"
by (force simp: Struct.satPB_def[OF S1] Struct.satPB_def[OF S2] fsymsPB_def
          intro!: fsyms_satC_cong[OF S1 S2] ball_cong 0)

lemma fsymsPB_Un[simp]: "fsymsPB (Φ1 ∪ Φ2) = fsymsPB Φ1 ∪ fsymsPB Φ2"
unfolding fsymsPB_def by auto

lemma fsymsC_append[simp]: "fsymsC (c1 @ c2) = fsymsC c1 ∪ fsymsC c2"
unfolding fsymsC_def by auto

lemma fsymsPB_sappend_incl[simp]:
"fsymsPB (Φ1 @@ Φ2) ⊆  fsymsPB Φ1 ∪ fsymsPB Φ2"
by (unfold fsymsPB_def sappend_def, fastforce)

lemma fsymsPB_sappend[simp]:
assumes 1: "Φ1 ≠ {}" and 2: "Φ2 ≠ {}"
shows "fsymsPB (Φ1 @@ Φ2) = fsymsPB Φ1 ∪ fsymsPB Φ2"
proof safe
  fix x
  {assume "x ∈ fsymsPB Φ1"
   then obtain c1 c2 where "x ∈ fsymsC c1" and "c1 ∈ Φ1" and "c2 ∈ Φ2"
   using 2 unfolding fsymsPB_def by auto
   thus "x ∈ fsymsPB (Φ1 @@ Φ2)" unfolding sappend_def fsymsPB_def by fastforce
  }
  {assume "x ∈ fsymsPB Φ2"
   then obtain c1 c2 where "x ∈ fsymsC c2" and "c1 ∈ Φ1" and "c2 ∈ Φ2"
   using 1 unfolding fsymsPB_def by auto
   thus "x ∈ fsymsPB (Φ1 @@ Φ2)" unfolding sappend_def fsymsPB_def by fastforce
  }
qed(unfold fsymsPB_def sappend_def, fastforce)

lemma Struct_upd:
assumes "Struct wtFsym wtPsym arOf resOf intT intF intP"
and "⋀ al. list_all2 intT (arOf ef) al ⟹ intT (resOf ef) (EF al)"
shows "Struct wtFsym wtPsym arOf resOf intT (intF (ef := EF)) intP"
apply standard using assms
unfolding Struct_def Struct_axioms_def Tstruct_def by auto

end (* context Signature *)


subsection‹Problems›

text‹A problem is a potentially infinitary formula in clausal form, i.e., 
a potentially infinite conjunction of clauses.›

locale Problem = Signature wtFsym wtPsym arOf resOf parOf
for wtFsym wtPsym
and arOf :: "'fsym ⇒ 'tp list"
and resOf :: "'fsym ⇒ 'tp"
and parOf :: "'psym ⇒ 'tp list"
+
fixes Φ :: "('fsym, 'psym) prob"
assumes wt_Φ: "wtPB Φ"


subsection‹Models of a problem›

text‹Model of a problem:›

locale Model = Problem + Struct +
assumes SAT: "SAT Φ"
begin
lemma sat_Φ: "wtE ξ ⟹ satPB ξ Φ"
using SAT unfolding SAT_def by auto
end


end