Theory TermsAndClauses

section‹Syntax of Terms and Clauses›
theory TermsAndClauses
imports Preliminaries
begin

text
‹These are used for both unsorted and many-sorted FOL, the difference being that,
for the latter, the signature will fix a variable typing.›

text‹Terms:›

datatype 'fsym trm =
  Var var |
  Fn 'fsym "'fsym trm list"

text‹Atomic formulas (atoms):›

datatype ('fsym, 'psym) atm =
  Eq "'fsym trm" "'fsym trm" |
  Pr 'psym "'fsym trm list"

text‹Literals:›

datatype ('fsym, 'psym) lit =
  Pos "('fsym, 'psym) atm" |
  Neg "('fsym, 'psym) atm"

text‹Clauses:›

type_synonym ('fsym, 'psym) cls = "('fsym, 'psym) lit list"

text‹Problems:›

type_synonym ('fsym, 'psym) prob = "('fsym, 'psym) cls set"

lemma trm_induct[case_names Var Fn, induct type: trm]:
assumes "⋀ x. φ (Var x)"
and "⋀ f Tl. list_all φ Tl ⟹ φ (Fn f Tl)"
shows "φ T"
using assms unfolding list_all_iff by (rule trm.induct) metis

fun vars where
"vars (Var x) = {x}"
|
"vars (Fn f Tl) = ⋃ (vars ` (set Tl))"

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

fun varsL where
"varsL (Pos at) = varsA at"
|
"varsL (Neg at) = varsA at"

definition "varsC c = ⋃ (set (map varsL c))"

definition "varsPB Φ = ⋃ {varsC c | c. c ∈ Φ}"

text‹Substitution:›

fun subst where
"subst π (Var x) = π x"
|
"subst π (Fn f Tl) = Fn f (map (subst π) Tl)"

fun substA where
"substA π (Eq T1 T2) = Eq (subst π T1) (subst π T2)"
|
"substA π (Pr p Tl) = Pr p (map (subst π) Tl)"

fun substL where
"substL π (Pos at) = Pos (substA π at)"
|
"substL π (Neg at) = Neg (substA π at)"

definition "substC π c = map (substL π) c"

definition "substPB π Φ = {substC π c | c. c ∈ Φ}"

lemma subst_cong:
assumes "⋀ x. x ∈ vars T ⟹ π1 x = π2 x"
shows "subst π1 T = subst π2 T"
using assms by (induct T, auto simp add: list_all_iff)

lemma substA_congA:
assumes "⋀ x. x ∈ varsA at ⟹ π1 x = π2 x"
shows "substA π1 at = substA π2 at"
using assms subst_cong[of _ π1 π2]
by (cases at, fastforce+)

lemma substL_congL:
assumes "⋀ x. x ∈ varsL l ⟹ π1 x = π2 x"
shows "substL π1 l = substL π2 l"
using assms substA_congA[of _ π1 π2] by (cases l, auto)

lemma substC_congC:
assumes "⋀ x. x ∈ varsC c ⟹ π1 x = π2 x"
shows "substC π1 c = substC π2 c"
using substL_congL[of _ π1 π2] assms unfolding substC_def varsC_def
by (induct c, auto)

lemma substPB_congPB:
assumes "⋀ x. x ∈ varsPB Φ ⟹ π1 x = π2 x"
shows "substPB π1 Φ = substPB π2 Φ"
using substC_congC[of _ π1 π2] assms unfolding substPB_def varsPB_def
by simp_all (metis (lifting) substC_congC) 

lemma vars_subst:
"vars (subst π T) = (⋃ x ∈ vars T. vars (π x))"
by (induct T) (auto simp add: list_all_iff)

lemma varsA_substA:
"varsA (substA π at) = (⋃ x ∈ varsA at. vars (π x))"
using vars_subst[of π] by (cases at, auto)

lemma varsL_substL:
"varsL (substL π l) = (⋃ x ∈ varsL l. vars (π x))"
using varsA_substA[of π] by (cases l, auto)

lemma varsC_substC:
"varsC (substC π c) = (⋃ x ∈ varsC c. vars (π x))"
apply(induct c) unfolding substC_def varsC_def
  apply fastforce
  unfolding substC_def varsC_def map_map set_map
  unfolding comp_def varsL_substL by blast

lemma varsPB_Un[simp]: "varsPB (Φ1 ∪ Φ2) = varsPB Φ1 ∪ varsPB Φ2"
unfolding varsPB_def by auto

lemma varsC_append[simp]: "varsC (c1 @ c2) = varsC c1 ∪ varsC c2"
unfolding varsC_def by auto

lemma varsPB_sappend_incl[simp]:
"varsPB (Φ1 @@ Φ2) ⊆  varsPB Φ1 ∪ varsPB Φ2"
by (unfold varsPB_def sappend_def, fastforce)

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

lemma varsPB_substPB:
"varsPB (substPB π Φ) = (⋃ x ∈ varsPB Φ. vars (π x))" (is "_ = ?K")
proof safe
  fix x assume "x ∈ varsPB (substPB π Φ)"
  then obtain c where "c ∈ Φ" and "x ∈ varsC (substC π c)"
  unfolding varsPB_def substPB_def by auto
  thus "x ∈ ?K" unfolding varsC_substC varsPB_def by auto
next
  fix x y assume "y ∈ varsPB Φ" and x: "x ∈ vars (π y)"
  then obtain c where c: "c ∈ Φ" and "y ∈ varsC c" unfolding varsPB_def by auto
  hence "x ∈ varsC (substC π c)" using x unfolding varsC_substC by auto
  thus "x ∈ varsPB (substPB π Φ)" using c unfolding varsPB_def substPB_def by auto
qed

lemma subst_o:
"subst (subst π1 o π2) T = subst π1 (subst π2 T)"
apply(induct T) by (auto simp add: list_all_iff)

lemma o_subst:
"subst π1 o subst π2 = subst (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding subst_o[symmetric] ..

lemma substA_o:
"substA (subst π1 o π2) at = substA π1 (substA π2 at)"
using subst_o[of π1 π2] by (cases at, auto)

lemma o_substA:
"substA π1 o substA π2 = substA (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substA_o[symmetric] ..

lemma substL_o:
"substL (subst π1 o π2) l = substL π1 (substL π2 l)"
using substA_o[of π1 π2] by (cases l, auto)

lemma o_substL:
"substL π1 o substL π2 = substL (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substL_o[symmetric] ..

lemma substC_o:
"substC (subst π1 o π2) c = substC π1 (substC π2 c)"
using substL_o[of π1 π2] unfolding substC_def by (induct c, auto)

lemma o_substC:
"substC π1 o substC π2 = substC (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substC_o[symmetric] ..

lemma substPB_o:
"substPB (subst π1 o π2) Φ = substPB π1 (substPB π2 Φ)"
using substC_o[of π1 π2] unfolding substPB_def by auto

lemma o_substPB:
"substPB π1 o substPB π2 = substPB (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substPB_o[symmetric] ..

lemma finite_vars: "finite (vars T)"
by(induct T, auto simp add: list_all_iff)

lemma finite_varsA: "finite (varsA at)"
using finite_vars by (cases at, auto)

lemma finite_varsL: "finite (varsL l)"
using finite_varsA by (cases l, auto)

lemma finite_varsC: "finite (varsC c)"
using finite_varsL unfolding varsC_def by (induct c, auto)

lemma finite_varsPB: "finite Φ ⟹ finite (varsPB Φ)"
using finite_varsC unfolding varsPB_def by (auto intro!: finite_Union)

end