Theory Mcalc2

section ‹The Second Monotonicity Calculus›
theory Mcalc2
imports Mono
begin



subsection‹Extension policies›

text‹Extension policy: copy, true or false extension:›

datatype epol = Cext | Text | Fext

text‹Problem with infinite knowledge and predicate-extension policy:›

locale ProblemIkPol = 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
+ fixes (* the predicate-extension policy *) pol :: "'tp ⇒ 'psym ⇒ epol"
and (* guard of a variable occurring in a certain literal of a certain clause: *)
    grdOf ::
"('fsym, 'psym) cls ⇒ ('fsym, 'psym) lit ⇒ var ⇒ ('fsym, 'psym) lit"


context ProblemIkPol begin

subsection‹Naked variables›

fun nv2T where
"nv2T (Var x) = {x}"
|
"nv2T (Fn f Tl) = {}"

fun nv2L where
"nv2L (Pos (Eq T1 T2)) = nv2T T1 ∪ nv2T T2"
|
"nv2L (Neg (Eq T1 T2)) = {}"
|
"nv2L (Pos (Pr p Tl)) = {x ∈ ⋃ (set (map nv2T Tl)) . pol (tpOfV x) p = Fext}"
|
"nv2L (Neg (Pr p Tl)) = {x ∈ ⋃ (set (map nv2T Tl)) . pol (tpOfV x) p = Text}"

definition "nv2C c ≡ ⋃ (set (map nv2L c))"

lemma in_nv2T: "x ∈ nv2T T ⟷ T = Var x"
apply(cases T)
  apply (metis equals0D nv2T.simps singleton_iff)
  by simp

lemma nv2T_vars[simp]: "x ∈ nv2T T ⟹ x ∈ vars T"
by (induct T, auto split: if_splits)

lemma nv2L_varsL[simp]:
assumes "x ∈ nv2L l" shows "x ∈ varsL l"
proof (cases l)
  case (Pos at)
  show ?thesis proof(cases at)
    case (Pr p Tl) thus ?thesis using assms unfolding Pos
    apply(cases "pol (tpOfV x) p", simp_all) by (metis nv2T_vars)
  qed(insert assms, unfold Pos, auto)
next
  case (Neg at)
  show ?thesis proof(cases at)
    case (Pr p Tl) thus ?thesis using assms unfolding Neg
    apply(cases "pol (tpOfV x) p", simp_all) by (metis nv2T_vars)
  qed(insert assms, unfold Neg, auto)
qed

lemma nv2C_varsC[simp]: "x ∈ nv2C c ⟹ x ∈ varsC c"
unfolding varsC_def nv2C_def by (induct c, auto)

subsection‹The calculus›

text‹The notion of a literal being a guard for a (typed) variable:›

fun isGuard :: "var ⇒ ('fsym,'psym) lit ⇒ bool" where
"isGuard x (Pos (Eq T1 T2)) ⟷ False"
|
"isGuard x (Neg (Eq T1 T2)) ⟷
 (T1 = Var x ∧ (∃ f Tl. T2 = Fn f Tl)) ∨
 (T2 = Var x ∧ (∃ f Tl. T1 = Fn f Tl))"
|
"isGuard x (Pos (Pr p Tl)) ⟷ x ∈ ⋃ (set (map nv2T Tl)) ∧ pol (tpOfV x) p = Text"
|
"isGuard x (Neg (Pr p Tl)) ⟷ x ∈ ⋃ (set (map nv2T Tl)) ∧ pol (tpOfV x) p = Fext"


text‹The monotonicity calculus from the Classen et. al. paper, applied
to non-infinite types only: it checks that any variable in any literal of any clause
is indeed guarded by its guard:›

inductive mcalc2 (infix ‹⊢2› 40) where
 [simp]: "infTp σ ⟹ σ ⊢2 c"
|[simp]: "(⋀ l x. ⟦l ∈ set c; x ∈ nv2L l; tpOfV x = σ⟧
         ⟹ isGuard x (grdOf c l x)) ⟹ σ ⊢2 c"

lemma mcalc2_iff:
"σ ⊢2 c ⟷
 infTp σ ∨ (∀ l x. l ∈ set c ∧ x ∈ nv2L l ∧ tpOfV x = σ ⟶ isGuard x (grdOf c l x))"
unfolding mcalc2.simps by auto

end (* context ProblemIk *)

locale ProblemIkPolMcalc2 = ProblemIkPol wtFsym wtPsym arOf resOf parOf Φ infTp pol grdOf
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and infTp and pol and grdOf
+ assumes
(* well-definednedd of the guard: *)
    grdOf: "⋀ c l x. ⟦c ∈ Φ; l ∈ set c; x ∈ nv2L l; ¬ infTp (tpOfV x)⟧
                     ⟹ grdOf c l x ∈ set c"
and mcalc2: "⋀ σ c. c ∈ Φ ⟹ σ ⊢2 c"
begin
lemma wtL_grdOf[simp]:
assumes "c ∈ Φ" and "l ∈ set c" and "x ∈ nv2L l" and "¬ infTp (tpOfV x)"
shows "wtL (grdOf c l x)"
using grdOf[OF assms] by (metis assms list_all_iff wtC_def wtPB_def wt_Φ)
end

locale ModelIkPolMcalc2 =
ModelIk wtFsym wtPsym arOf resOf parOf Φ infTp intT intF intP +
ProblemIkPolMcalc2 wtFsym wtPsym arOf resOf parOf Φ infTp pol grdOf
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and infTp pol and grdOf and intT and intF and intP


end