Theory MLSS_Calculus

theory MLSS_Calculus
  imports "HOL-Library.Sublist" MLSS_Semantics MLSS_Typing_Defs
begin

section ‹A Tableau Calculus for MLSS›
text ‹
  In this theory, we define a tableau calculus for MLSS.
›

subsection ‹Closedness›

fun member_seq :: "'a pset_term ⇒ 'a pset_atom list ⇒ 'a pset_term ⇒ bool" where
  "member_seq s [] t ⟷ s = t"
| "member_seq s ((s' ∈s u) # cs) t ⟷ s = s' ∧ member_seq u cs t"
| "member_seq _ _ _ ⟷ False"

fun member_cycle :: "'a pset_atom list ⇒ bool" where
  "member_cycle ((s ∈s t) # cs) = member_seq s ((s ∈s t) # cs) s"
| "member_cycle _ = False"

inductive bclosed :: "'a branch ⇒ bool" where
  contr: "⟦ φ ∈ set b; Neg φ ∈ set b ⟧ ⟹ bclosed b"
| memEmpty: "AT (t ∈s (∅ n)) ∈ set b ⟹ bclosed b"
| neqSelf: "AF (t =s t) ∈ set b ⟹ bclosed b"
| memberCycle: "⟦ member_cycle cs; set cs ⊆ Atoms (set b) ⟧ ⟹ bclosed b"

abbreviation "bopen b ≡ ¬ bclosed b"

subsection ‹Linear Expansion Rules›

fun tlvl_terms :: "'a pset_atom ⇒ 'a pset_term set" where
  "tlvl_terms (t1 ∈s t2) = {t1, t2}"
| "tlvl_terms (t1 =s t2) = {t1, t2}"

lemma tlvl_intros[intro, simp]:
  "t1 ∈ tlvl_terms (t1 ∈s t2)"
  "t2 ∈ tlvl_terms (t2 ∈s t1)"
  "t1 ∈ tlvl_terms (t1 =s t2)"
  "t2 ∈ tlvl_terms (t2 =s t1)"
  by auto
  
fun subst_tlvl :: "'a pset_term ⇒ 'a pset_term ⇒ 'a pset_atom ⇒ 'a pset_atom" where
  "subst_tlvl t1 t2 (s1 ∈s s2) =
    (if s1 = t1 then t2 else s1) ∈s (if s2 = t1 then t2 else s2)"
| "subst_tlvl t1 t2 (s1 =s s2) =
    (if s1 = t1 then t2 else s1) =s (if s2 = t1 then t2 else s2)"

inductive lexpands_fm :: "'a branch ⇒ 'a branch ⇒ bool" where
  "And p q ∈ set b ⟹ lexpands_fm [p, q] b"
| "Neg (Or p q) ∈ set b ⟹ lexpands_fm [Neg p, Neg q] b"
| "⟦ Or p q ∈ set b; Neg p ∈ set b ⟧ ⟹ lexpands_fm [q] b"
| "⟦ Or p q ∈ set b; Neg q ∈ set b ⟧ ⟹ lexpands_fm [p] b"
| "⟦ Neg (And p q) ∈ set b; p ∈ set b ⟧ ⟹ lexpands_fm [Neg q] b"
| "⟦ Neg (And p q) ∈ set b; q ∈ set b ⟧ ⟹ lexpands_fm [Neg p] b"
| "Neg (Neg p) ∈ set b ⟹ lexpands_fm [p] b"

inductive lexpands_un :: "'a branch ⇒ 'a branch ⇒ bool" where
  "AF (s ∈s t1 ⊔s t2) ∈ set b ⟹ lexpands_un [AF (s ∈s t1), AF (s ∈s t2)] b"
| "⟦ AT (s ∈s t1) ∈ set b; t1 ⊔s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_un [AT (s ∈s t1 ⊔s t2)] b"
| "⟦ AT (s ∈s t2) ∈ set b; t1 ⊔s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_un [AT (s ∈s t1 ⊔s t2)] b"
| "⟦ AT (s ∈s t1 ⊔s t2) ∈ set b; AF (s ∈s t1) ∈ set b ⟧
    ⟹ lexpands_un [AT (s ∈s t2)] b"
| "⟦ AT (s ∈s t1 ⊔s t2) ∈ set b; AF (s ∈s t2) ∈ set b ⟧
    ⟹ lexpands_un [AT (s ∈s t1)] b"
| "⟦ AF (s ∈s t1) ∈ set b; AF (s ∈s t2) ∈ set b; t1 ⊔s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_un [AF (s ∈s t1 ⊔s t2)] b"

inductive lexpands_int :: "'a branch ⇒ 'a branch ⇒ bool" where
  "AT (s ∈s t1 ⊓s t2) ∈ set b ⟹ lexpands_int [AT (s ∈s t1), AT (s ∈s t2)] b"
| "⟦ AF (s ∈s t1) ∈ set b; t1 ⊓s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_int [AF (s ∈s t1 ⊓s t2)] b"
| "⟦ AF (s ∈s t2) ∈ set b; t1 ⊓s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_int [AF (s ∈s t1 ⊓s t2)] b"
| "⟦ AF (s ∈s t1 ⊓s t2) ∈ set b; AT (s ∈s t1) ∈ set b ⟧
    ⟹ lexpands_int [AF (s ∈s t2)] b"
| "⟦ AF (s ∈s t1 ⊓s t2) ∈ set b; AT (s ∈s t2) ∈ set b ⟧
    ⟹ lexpands_int [AF (s ∈s t1)] b"
| "⟦ AT (s ∈s t1) ∈ set b; AT (s ∈s t2) ∈ set b; t1 ⊓s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_int [AT (s ∈s t1 ⊓s t2)] b"

inductive lexpands_diff :: "'a branch ⇒ 'a branch ⇒ bool" where
  "AT (s ∈s t1 -s t2) ∈ set b ⟹ lexpands_diff [AT (s ∈s t1), AF (s ∈s t2)] b"
| "⟦ AF (s ∈s t1) ∈ set b; t1 -s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_diff [AF (s ∈s t1 -s t2)] b"
| "⟦ AT (s ∈s t2) ∈ set b; t1 -s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_diff [AF (s ∈s t1 -s t2)] b"
| "⟦ AF (s ∈s t1 -s t2) ∈ set b; AT (s ∈s t1) ∈ set b ⟧
    ⟹ lexpands_diff [AT (s ∈s t2)] b"
| "⟦ AF (s ∈s t1 -s t2) ∈ set b; AF (s ∈s t2) ∈ set b ⟧
    ⟹ lexpands_diff [AF (s ∈s t1)] b"
| "⟦ AT (s ∈s t1) ∈ set b; AF (s ∈s t2) ∈ set b; t1 -s t2 ∈ subterms (last b) ⟧
    ⟹ lexpands_diff [AT (s ∈s t1 -s t2)] b"

inductive lexpands_single :: "'a branch ⇒ 'a branch ⇒ bool" where
  "Single t1 ∈ subterms (last b) ⟹ lexpands_single [AT (t1 ∈s Single t1)] b"
| "AT (s ∈s Single t1) ∈ set b ⟹ lexpands_single [AT (s =s t1)] b"
| "AF (s ∈s Single t1) ∈ set b ⟹ lexpands_single [AF (s =s t1)] b"

inductive lexpands_eq :: "'a branch ⇒ 'a branch ⇒ bool" where
  "⟦ AT (t1 =s t2) ∈ set b; AT l ∈ set b; t1 ∈ tlvl_terms l ⟧
    ⟹ lexpands_eq [AT (subst_tlvl t1 t2 l)] b"
| "⟦ AT (t1 =s t2) ∈ set b; AF l ∈ set b; t1 ∈ tlvl_terms l ⟧
    ⟹ lexpands_eq [AF (subst_tlvl t1 t2 l)] b"
| "⟦ AT (t1 =s t2) ∈ set b; AT l ∈ set b; t2 ∈ tlvl_terms l ⟧
    ⟹ lexpands_eq [AT (subst_tlvl t2 t1 l)] b"
| "⟦ AT (t1 =s t2) ∈ set b; AF l ∈ set b; t2 ∈ tlvl_terms l ⟧
    ⟹ lexpands_eq [AF (subst_tlvl t2 t1 l)] b"
| "⟦ AT (s ∈s t) ∈ set b; AF (s' ∈s t) ∈ set b ⟧
    ⟹ lexpands_eq [AF (s =s s')] b"

fun polarise :: "bool ⇒ 'a fm ⇒ 'a fm" where
  "polarise True φ = φ"
| "polarise False φ = Neg φ"

lemma lexpands_eq_induct'[consumes 1, case_names subst neq]:
  assumes "lexpands_eq b' b"
  assumes "⋀t1 t2 t1' t2' p l b. 
      ⟦ AT (t1 =s t2) ∈ set b; polarise p (Atom l) ∈ set b;
       (t1', t2') ∈ {(t1, t2), (t2, t1)}; t1' ∈ tlvl_terms l ⟧
      ⟹ P [polarise p (Atom (subst_tlvl t1' t2' l))] b"
  assumes "⋀s t s' b. ⟦ AT (s ∈s t) ∈ set b; AF (s' ∈s t) ∈ set b ⟧ ⟹ P [AF (s =s s')] b"
  shows "P b' b"
  using assms(1)
  apply(induction rule: lexpands_eq.induct)
  by (metis assms(2-) insertI1 insertI2 polarise.simps)+

inductive lexpands :: "'a branch ⇒ 'a branch ⇒ bool" where
  "lexpands_fm b' b ⟹ lexpands b' b"
| "lexpands_un b' b ⟹ lexpands b' b"
| "lexpands_int b' b ⟹ lexpands b' b"
| "lexpands_diff b' b ⟹ lexpands b' b"
| "lexpands_single b' b ⟹ lexpands b' b"
| "lexpands_eq b' b ⟹ lexpands b' b"

lemma lexpands_induct[consumes 1]:
  assumes "lexpands b' b"
  shows "
    (⋀p q b. And p q ∈ set b ⟹ P [p, q] b) ⟹
    (⋀p q b. Neg (Or p q) ∈ set b ⟹ P [Neg p, Neg q] b) ⟹
    (⋀p q b. Or p q ∈ set b ⟹ Neg p ∈ set b ⟹ P [q] b) ⟹
    (⋀p q b. Or p q ∈ set b ⟹ Neg q ∈ set b ⟹ P [p] b) ⟹
    (⋀p q b. Neg (And p q) ∈ set b ⟹ p ∈ set b ⟹ P [Neg q] b) ⟹
    (⋀p q b. Neg (And p q) ∈ set b ⟹ q ∈ set b ⟹ P [Neg p] b) ⟹
    (⋀p b. Neg (Neg p) ∈ set b ⟹ P [p] b) ⟹
    (⋀s t1 t2 b. AF (s ∈s t1 ⊔s t2) ∈ set b ⟹ P [AF (s ∈s t1), AF (s ∈s t2)] b) ⟹
    (⋀s t1 b t2. AT (s ∈s t1) ∈ set b ⟹ t1 ⊔s t2 ∈ subterms (last b) ⟹ P [AT (s ∈s t1 ⊔s t2)] b) ⟹
    (⋀s t2 b t1. AT (s ∈s t2) ∈ set b ⟹ t1 ⊔s t2 ∈ subterms (last b) ⟹ P [AT (s ∈s t1 ⊔s t2)] b) ⟹
    (⋀s t1 t2 b. AT (s ∈s t1 ⊔s t2) ∈ set b ⟹ AF (s ∈s t1) ∈ set b ⟹ P [AT (s ∈s t2)] b) ⟹
    (⋀s t1 t2 b. AT (s ∈s t1 ⊔s t2) ∈ set b ⟹ AF (s ∈s t2) ∈ set b ⟹ P [AT (s ∈s t1)] b) ⟹
    (⋀s t1 b t2. AF (s ∈s t1) ∈ set b ⟹ AF (s ∈s t2) ∈ set b ⟹ t1 ⊔s t2 ∈ subterms (last b) ⟹ P [AF (s ∈s t1 ⊔s t2)] b) ⟹
    (⋀s t1 t2 b. AT (s ∈s t1 ⊓s t2) ∈ set b ⟹ P [AT (s ∈s t1), AT (s ∈s t2)] b) ⟹
    (⋀s t1 b t2. AF (s ∈s t1) ∈ set b ⟹ t1 ⊓s t2 ∈ subterms (last b) ⟹ P [AF (s ∈s t1 ⊓s t2)] b) ⟹
    (⋀s t2 b t1. AF (s ∈s t2) ∈ set b ⟹ t1 ⊓s t2 ∈ subterms (last b) ⟹ P [AF (s ∈s t1 ⊓s t2)] b) ⟹
    (⋀s t1 t2 b. AF (s ∈s t1 ⊓s t2) ∈ set b ⟹ AT (s ∈s t1) ∈ set b ⟹ P [AF (s ∈s t2)] b) ⟹
    (⋀s t1 t2 b. AF (s ∈s t1 ⊓s t2) ∈ set b ⟹ AT (s ∈s t2) ∈ set b ⟹ P [AF (s ∈s t1)] b) ⟹
    (⋀s t1 b t2. AT (s ∈s t1) ∈ set b ⟹ AT (s ∈s t2) ∈ set b ⟹ t1 ⊓s t2 ∈ subterms (last b) ⟹ P [AT (s ∈s t1 ⊓s t2)] b) ⟹
    (⋀s t1 t2 b. AT (s ∈s t1 -s t2) ∈ set b ⟹ P [AT (s ∈s t1),  AF (s ∈s t2)] b) ⟹
    (⋀s t1 b t2. AF (s ∈s t1) ∈ set b ⟹ t1 -s t2 ∈ subterms (last b) ⟹ P [AF (s ∈s t1 -s t2)] b) ⟹
    (⋀s t2 b t1. AT (s ∈s t2) ∈ set b ⟹ t1 -s t2 ∈ subterms (last b) ⟹ P [AF (s ∈s t1 -s t2)] b) ⟹
    (⋀s t1 t2 b. AF (s ∈s t1 -s t2) ∈ set b ⟹ AT (s ∈s t1) ∈ set b ⟹ P [AT (s ∈s t2)] b) ⟹
    (⋀s t1 t2 b. AF (s ∈s t1 -s t2) ∈ set b ⟹ AF (s ∈s t2) ∈ set b ⟹ P [AF (s ∈s t1)] b) ⟹
    (⋀s t1 b t2. AT (s ∈s t1) ∈ set b ⟹ AF (s ∈s t2) ∈ set b ⟹ t1 -s t2 ∈ subterms (last b) ⟹ P [AT (s ∈s t1 -s t2)] b) ⟹
    (⋀t1 b. Single t1 ∈ subterms (last b) ⟹ P [AT (t1 ∈s Single t1)] b) ⟹
    (⋀s t1 b. AT (s ∈s Single t1) ∈ set b ⟹ P [AT (s =s t1)] b) ⟹
    (⋀s t1 b. AF (s ∈s Single t1) ∈ set b ⟹ P [AF (s =s t1)] b) ⟹
    (⋀t1 t2 b l. AT (t1 =s t2) ∈ set b ⟹ AT l ∈ set b ⟹ t1 ∈ tlvl_terms l ⟹ P [AT (subst_tlvl t1 t2 l)] b) ⟹
    (⋀t1 t2 b l. AT (t1 =s t2) ∈ set b ⟹ AF l ∈ set b ⟹ t1 ∈ tlvl_terms l ⟹ P [AF (subst_tlvl t1 t2 l)] b) ⟹
    (⋀t1 t2 b l. AT (t1 =s t2) ∈ set b ⟹ AT l ∈ set b ⟹ t2 ∈ tlvl_terms l ⟹ P [AT (subst_tlvl t2 t1 l)] b) ⟹
    (⋀t1 t2 b l. AT (t1 =s t2) ∈ set b ⟹ AF l ∈ set b ⟹ t2 ∈ tlvl_terms l ⟹ P [AF (subst_tlvl t2 t1 l)] b) ⟹  
    (⋀s t b s'. AT (s ∈s t) ∈ set b ⟹ AF (s' ∈s t) ∈ set b ⟹ P [AF (s =s s')] b) ⟹ P b' b"
  using assms
  apply(induction rule: lexpands.induct)
  subgoal apply(induction rule: lexpands_fm.induct) by metis+
  subgoal apply(induction rule: lexpands_un.induct) by metis+
  subgoal apply(induction rule: lexpands_int.induct) by metis+
  subgoal apply(induction rule: lexpands_diff.induct) by metis+
  subgoal apply(induction rule: lexpands_single.induct) by metis+
  subgoal apply(induction rule: lexpands_eq.induct) by metis+
  done


subsection ‹Fulfilling Expansion Rules›

inductive bexpands_nowit :: "'a branch set ⇒ 'a branch ⇒ bool" where
  "⟦ Or p q ∈ set b;
     p ∉ set b; Neg p ∉ set b ⟧
    ⟹ bexpands_nowit {[p], [Neg p]} b"
| "⟦ Neg (And p q) ∈ set b;
     Neg p ∉ set b; p ∉ set b ⟧
    ⟹ bexpands_nowit {[Neg p], [p]} b"
| "⟦ AT (s ∈s t1 ⊔s t2) ∈ set b; t1 ⊔s t2 ∈ subterms (last b);
     AT (s ∈s t1) ∉ set b; AF (s ∈s t1) ∉ set b ⟧
    ⟹ bexpands_nowit {[AT (s ∈s t1)], [AF (s ∈s t1)]} b"
| "⟦ AT (s ∈s t1) ∈ set b; t1 ⊓s t2 ∈ subterms (last b);
     AT (s ∈s t2) ∉ set b; AF (s ∈s t2) ∉ set b ⟧
    ⟹ bexpands_nowit {[AT (s ∈s t2)], [AF (s ∈s t2)]} b"
| "⟦ AT (s ∈s t1) ∈ set b; t1 -s t2 ∈ subterms (last b);
     AT (s ∈s t2) ∉ set b; AF (s ∈s t2) ∉ set b ⟧
    ⟹ bexpands_nowit {[AT (s ∈s t2)], [AF (s ∈s t2)]} b"

inductive bexpands_wit ::
  "'a pset_term ⇒ 'a pset_term ⇒ 'a ⇒ 'a branch set ⇒ 'a branch ⇒ bool" for t1 t2 x where
  "⟦ AF (t1 =s t2) ∈ set b; t1 ∈ subterms (last b); t2 ∈ subterms (last b);
     ∄x. AT (x ∈s t1) ∈ set b ∧ AF (x ∈s t2) ∈ set b;
     ∄x. AT (x ∈s t2) ∈ set b ∧ AF (x ∈s t1) ∈ set b;
     x ∉ vars b; ¬ urelem (last b) t1; ¬ urelem (last b) t2 ⟧
    ⟹ bexpands_wit t1 t2 x {[AT (Var x ∈s t1), AF (Var x ∈s t2)],
                              [AT (Var x ∈s t2), AF (Var x ∈s t1)]} b"

inductive_cases bexpands_wit_cases[consumes 1]: "bexpands_wit t1 t2 x bs' b"

lemma bexpands_witD:
  assumes "bexpands_wit t1 t2 x bs' b"
  shows "bs' = {[AT (Var x ∈s t1), AF (Var x ∈s t2)],
               [AT (Var x ∈s t2), AF (Var x ∈s t1)]}"
        "AF (t1 =s t2) ∈ set b" "t1 ∈ subterms (last b)" "t2 ∈ subterms (last b)"
        "∄x. AT (x ∈s t1) ∈ set b ∧ AF (x ∈s t2) ∈ set b"
        "∄x. AT (x ∈s t2) ∈ set b ∧ AF (x ∈s t1) ∈ set b"
        "¬ urelem (last b) t1" "¬ urelem (last b) t2"
        "x ∉ vars b"
  using bexpands_wit.cases[OF assms] by metis+

inductive bexpands :: "'a branch set ⇒ 'a branch ⇒ bool" where
  "bexpands_nowit bs' b ⟹ bexpands bs' b"
| "bexpands_wit t1 t2 x bs' b ⟹ bexpands bs' b"

lemma bexpands_disjnt:
  assumes "bexpands bs' b" "b' ∈ bs'"
  shows "set b ∩ set b' = {}"
  using assms
proof(induction bs' b rule: bexpands.induct)
  case (1 bs b)
  then show ?case
    by (induction rule: bexpands_nowit.induct) (auto intro: list.set_intros(1))
next
  case (2 t1 t2 x bs b)
  then show ?case
  proof(induction rule: bexpands_wit.induct)
    case (1 b)
    from ‹x ∉ vars b›
    have "AT (Var x ∈s t1) ∉ set b" "AF (Var x ∈s t1) ∉ set b"
      unfolding vars_branch_def by auto
    with 1 show ?case
      by (auto intro: list.set_intros(1) simp: disjnt_iff vars_fm_vars_branchI)
  qed
qed

lemma bexpands_branch_not_Nil:
  assumes "bexpands bs' b" "b' ∈ bs'"
  shows "b' ≠ []"
  using assms
proof(induction bs' b rule: bexpands.induct)
  case (1 bs' b)
  then show ?case
    by (induction rule: bexpands_nowit.induct) auto
next
  case (2 t1 t2 x bs' b)
  then show ?case
    by (induction rule: bexpands_wit.induct) auto
qed

lemma bexpands_nonempty: "bexpands bs' b ⟹ bs' ≠ {}"
proof(induction rule: bexpands.induct)
  case (1 bs' b)
  then show ?case by (induction rule: bexpands_nowit.induct) auto
next
  case (2 t1 t2 x bs' b)
  then show ?case by (induction rule: bexpands_wit.induct) auto
qed

lemma bexpands_strict_mono:
  assumes "bexpands bs' b" "b' ∈ bs'"
  shows "set b ⊂ set (b' @ b)"
  using bexpands_disjnt[OF assms] bexpands_branch_not_Nil[OF assms]
  by (simp add: less_le) (metis Un_Int_eq(1) set_empty2)

inductive_cases bexpands_cases[consumes 1, case_names no_param param]: "bexpands bs b"


subsection ‹Expansion Closure›

inductive expandss :: "'a branch ⇒ 'a branch ⇒ bool" where
  "expandss b b"
| "lexpands b3 b2 ⟹ set b2 ⊂ set (b3 @ b2) ⟹ expandss b2 b1 ⟹ expandss (b3 @ b2) b1"
| "bexpands bs b2 ⟹ b3 ∈ bs ⟹ expandss b2 b1 ⟹ expandss (b3 @ b2) b1"

lemma expandss_trans: "expandss b3 b2 ⟹ expandss b2 b1 ⟹ expandss b3 b1"
  by (induction rule: expandss.induct) (auto simp: expandss.intros)

lemma expandss_suffix:
  "expandss b1 b2 ⟹ suffix b2 b1"
  apply(induction rule: expandss.induct)
    apply(auto simp: suffix_appendI)
  done

lemmas expandss_mono = set_mono_suffix[OF expandss_suffix]

lemma expandss_last_eq[simp]:
  "expandss b' b ⟹ b ≠ [] ⟹ last b' = last b"
  by (metis expandss_suffix last_appendR suffix_def)

lemma expandss_not_Nil:
  "expandss b' b ⟹ b ≠ [] ⟹ b' ≠ []"
  using expandss_suffix suffix_bot.extremum_uniqueI by blast


subsection ‹Well-Formed Branch›

definition "wf_branch b ≡ ∃φ. expandss b [φ]"

lemma wf_branch_singleton[simp]: "wf_branch [φ]"
  unfolding wf_branch_def using expandss.intros(1) by blast

lemma wf_branch_not_Nil[simp, intro?]: "wf_branch b ⟹ b ≠ []"
  unfolding wf_branch_def
  using expandss_suffix suffix_bot.extremum_uniqueI by blast

lemma wf_branch_expandss: "wf_branch b ⟹ expandss b' b ⟹ wf_branch b'"
  using expandss_trans wf_branch_def by blast

lemma wf_branch_lexpands:
  "wf_branch b ⟹ lexpands b' b ⟹ set b ⊂ set (b' @ b) ⟹ wf_branch (b' @ b)"
  by (metis expandss.simps wf_branch_expandss)

end