Theory ProverLemmas

section ‹Lemmas about the prover›

theory ProverLemmas imports Prover begin

text ‹This theory contains a number of lemmas about the prover.
  We will need these when proving soundness and completeness.›

subsection ‹SeCaV lemmas›
text ‹We need a few lemmas about the SeCaV system.›

text ‹Incrementing variable indices does not change the function names in term or a list of terms.›
lemma paramst_liftt [simp]:
  ‹paramst (liftt t) = paramst t› ‹paramsts (liftts ts) = paramsts ts›
  by (induct t and ts rule: liftt.induct liftts.induct) auto

text ‹Subterms do not contain any functions except those in the original term›
lemma paramst_sub_term:
  ‹paramst (sub_term m s t) ⊆ paramst s ∪ paramst t›
  ‹paramsts (sub_list m s l) ⊆ paramst s ∪ paramsts l›
  by (induct t and l rule: sub_term.induct sub_list.induct) auto

text ‹Substituting a variable for a term does not introduce function names not in that term›
lemma params_sub: ‹params (sub m t p) ⊆ paramst t ∪ params p›
proof (induct p arbitrary: m t)
  case (Pre x1 x2)
  then show ?case
    using paramst_sub_term(2) by simp
qed fastforce+

abbreviation ‹paramss z ≡ ⋃p ∈ set z. params p›

text ‹If a function name is fresh, it is not in the list of function names in the sequent›
lemma news_paramss: ‹news i z ⟷ i ∉ paramss z›
  by (induct z) auto

text ‹If a list of terms is a subset of another, the set of function names in it is too›
lemma paramsts_subset: ‹set A ⊆ set B ⟹ paramsts A ⊆ paramsts B›
  by (induct A) auto

text ‹Substituting a variable by a term does not change the depth of a formula
  (only the term size changes)›
lemma size_sub [simp]: ‹size (sub i t p) = size p›
  by (induct p arbitrary: i t) auto

subsection ‹Fairness›
text ‹While fairness of the rule stream should be pretty trivial (since we are simply repeating a
  static list of rules forever), the proof is a bit involved.›

text ‹This function tells us what rule comes next in the stream.›
primrec next_rule :: ‹rule ⇒ rule› where
  ‹next_rule NegNeg = AlphaImp›
| ‹next_rule AlphaImp = AlphaDis›
| ‹next_rule AlphaDis = AlphaCon›
| ‹next_rule AlphaCon = DeltaExi›
| ‹next_rule DeltaExi = DeltaUni›
| ‹next_rule DeltaUni = BetaImp›
| ‹next_rule BetaImp = BetaDis›
| ‹next_rule BetaDis = BetaCon›
| ‹next_rule BetaCon = GammaExi›
| ‹next_rule GammaExi = GammaUni›
| ‹next_rule GammaUni = NegNeg›

text ‹This function tells us the index of a rule in the list of rules to repeat.›
primrec rule_index :: ‹rule ⇒ nat› where
  ‹rule_index NegNeg = 0›
| ‹rule_index AlphaImp = 1›
| ‹rule_index AlphaDis = 2›
| ‹rule_index AlphaCon = 3›
| ‹rule_index DeltaExi = 4›
| ‹rule_index DeltaUni = 5›
| ‹rule_index BetaImp = 6›
| ‹rule_index BetaDis = 7›
| ‹rule_index BetaCon = 8›
| ‹rule_index GammaExi = 9›
| ‹rule_index GammaUni = 10›

text ‹The list of rules does not have any duplicates.
  This is important because we can then look up rules by their index.›
lemma distinct_rulesList: ‹distinct rulesList›
  unfolding rulesList_def by simp

text ‹If you cycle a list, it repeats every ‹length› elements.›
lemma cycle_nth: ‹xs ≠ [] ⟹ cycle xs !! n = xs ! (n mod length xs)›
  by (metis cycle.sel(1) hd_rotate_conv_nth rotate_conv_mod sdrop_cycle sdrop_simps(1))

text ‹The rule index function can actually be used to look up rules in the list.›
lemma nth_rule_index: ‹rulesList ! (rule_index r) = r›
  unfolding rulesList_def by (cases r) simp_all

lemma rule_index_bnd: ‹rule_index r < length rulesList›
  unfolding rulesList_def by (cases r) simp_all

lemma unique_rule_index:
  assumes ‹n < length rulesList› ‹rulesList ! n = r›
  shows ‹n = rule_index r›
  using assms nth_rule_index distinct_rulesList rule_index_bnd nth_eq_iff_index_eq by metis

text ‹The rule indices repeat in the stream each cycle.›
lemma rule_index_mod:
  assumes ‹rules !! n = r›
  shows ‹n mod length rulesList = rule_index r›
proof -
  have *: ‹rulesList ! (n mod length rulesList) = r›
    using assms cycle_nth unfolding rules_def rulesList_def by (metis list.distinct(1))
  then show ?thesis
    using distinct_rulesList * unique_rule_index
    by (cases r) (metis length_greater_0_conv list.discI rulesList_def
        unique_euclidean_semiring_numeral_class.pos_mod_bound)+
qed

text ‹We need some lemmas about the modulo function to show that the rules repeat at the right rate.›
lemma mod_hit:
  fixes k :: nat
  assumes ‹0 < k›
  shows ‹∀i < k. ∃n > m. n mod k = i›
proof safe
  fix i
  let ?n = ‹(1 + m) * k + i›
  assume ‹i < k›
  then have ‹?n mod k = i›
    by (metis mod_less mod_mult_self3)
  moreover have ‹?n > m›
    using assms
    by (metis One_nat_def Suc_eq_plus1_left Suc_leI add.commute add_lessD1 less_add_one
        mult.right_neutral nat_mult_less_cancel1 order_le_less trans_less_add1 zero_less_one)
  ultimately show ‹∃n > m. n mod k = i›
    by fast
qed

lemma mod_suff:
  assumes ‹∀(n :: nat) > m. P (n mod k)› ‹0 < k›
  shows ‹∀i < k. P i›
  using assms mod_hit by blast

text ‹It is always possible to find an index after some point that results in any given rule.›
lemma rules_repeat: ‹∃n > m. rules !! n = r›
proof (rule ccontr)
  assume ‹¬ (∃n > m. rules !! n = r)›
  then have ‹¬ (∃n > m. n mod length rulesList = rule_index r)›
    using rule_index_mod nth_rule_index by metis
  then have ‹∀n > m. n mod length rulesList ≠ rule_index r›
    by blast
  moreover have ‹length rulesList > 0›
    unfolding rulesList_def by simp
  ultimately have ‹∀k < length rulesList. k ≠ rule_index r›
    using mod_suff[where P=‹λa. a ≠ rule_index r›] by blast
  then show False
    using rule_index_bnd by blast
qed

text ‹It is possible to find such an index no matter where in the stream we start.›
lemma rules_repeat_sdrop: ‹∃n. (sdrop k rules) !! n = r›
  using rules_repeat by (metis less_imp_add_positive sdrop_snth)

text ‹Using the lemma above, we prove that the stream of rules is fair by coinduction.›
lemma fair_rules: ‹fair rules›
proof -
  { fix r assume ‹r ∈ R›
    then obtain m where r: ‹r = rules !! m› unfolding sset_range by blast
    { fix n :: nat and rs let ?rules = ‹λn. sdrop n rules›
      assume ‹n > 0›
      then have ‹alw (ev (holds ((=) r))) (rs @- ?rules n)›
      proof (coinduction arbitrary: n rs)
        case alw
        show ?case
        proof (rule exI[of _ ‹rs @- ?rules n›], safe)
          show ‹∃n' rs'. stl (rs @- ?rules n) = rs' @- ?rules n' ∧ n' > 0›
          proof (cases rs)
            case Nil then show ?thesis unfolding alw
              by (metis sdrop_simps(2) shift.simps(1) zero_less_Suc)
          qed (auto simp: alw intro: exI[of _ n])
        next
          have ‹ev (holds ((=) r)) (sdrop n rules)›
            unfolding ev_holds_sset using rules_repeat_sdrop by (metis snth_sset)
          then show ‹ev (holds ((=) r)) (rs @- sdrop n rules)›
            unfolding ev_holds_sset by simp
        qed
      qed
    }
  }
  then show ‹fair rules› unfolding fair_def
    by (metis (full_types) alw_iff_sdrop ev_holds_sset neq0_conv order_refl sdrop.simps(1)
        stake_sdrop)
qed

subsection ‹Substitution›
text ‹We need some lemmas about substitution of variables for terms for the Delta and Gamma rules.›

text ‹If a term is a subterm of another, so are all of its subterms.›
lemma subtermTm_le: ‹t ∈ set (subtermTm s) ⟹ set (subtermTm t) ⊆ set (subtermTm s)›
  by (induct s) auto

text ‹Trying to substitute a variable that is not in the term does nothing (contrapositively).›
lemma sub_term_const_transfer:
  ‹sub_term m (Fun a []) t ≠ sub_term m s t ⟹
    Fun a [] ∈ set (subtermTm (sub_term m (Fun a []) t))›
  ‹sub_list m (Fun a []) ts ≠ sub_list m s ts ⟹
    Fun a [] ∈ (⋃t ∈ set (sub_list m (Fun a []) ts). set (subtermTm t))›
proof (induct t and ts rule: sub_term.induct sub_list.induct)
  case (Var x)
  then show ?case
    by (metis list.set_intros(1) sub_term.simps(1) subtermTm.simps(1))
qed auto

text ‹If substituting different terms makes a difference, then the substitution has an effect.›
lemma sub_const_transfer:
  assumes ‹sub m (Fun a []) p ≠ sub m t p›
  shows ‹Fun a [] ∈ set (subtermFm (sub m (Fun a []) p))›
  using assms
proof (induct p arbitrary: m t)
  case (Pre i l)
  then show ?case
    using sub_term_const_transfer(2) by simp
qed auto

text ‹If the list of subterms is empty for all formulas in a sequent, constant 0 is used instead.›
lemma set_subterms:
  fixes z
  defines ‹ts ≡ ⋃p ∈ set z. set (subtermFm p)›
  shows ‹set (subterms z) = (if ts = {} then {Fun 0 []} else ts)›
proof -
  have *: ‹set (remdups (concat (map subtermFm z))) = (⋃p ∈ set z. set (subtermFm p))›
    by (induct z) auto
  then show ?thesis
  proof (cases ‹ts = {}›)
    case True
    then show ?thesis
      unfolding subterms_def ts_def using *
      by (metis list.simps(15) list.simps(4) set_empty)
  next
    case False
    then show ?thesis
      unfolding subterms_def ts_def using *
      by (metis empty_set list.exhaust list.simps(5))
  qed
qed

text ‹The parameters and the subterm functions respect each other.›
lemma paramst_subtermTm:
  ‹∀i ∈ paramst t. ∃l. Fun i l ∈ set (subtermTm t)›
  ‹∀i ∈ paramsts ts. ∃l. Fun i l ∈ (⋃t ∈ set ts. set (subtermTm t))›
  by (induct t and ts rule: paramst.induct paramsts.induct) fastforce+

lemma params_subtermFm: ‹∀i ∈ params p. ∃l. Fun i l ∈ set (subtermFm p)›
proof (induct p)
  case (Pre x1 x2)
  then show ?case
    using paramst_subtermTm by simp
qed auto

lemma subtermFm_subset_params: ‹set (subtermFm p) ⊆ set A ⟹ params p ⊆ paramsts A›
  using params_subtermFm by force

subsection ‹Custom cases›
text ‹Some proofs are more efficient with some custom case lemmas.›

lemma Neg_exhaust
  [case_names Pre Imp Dis Con Exi Uni NegPre NegImp NegDis NegCon NegExi NegUni NegNeg]:
  assumes
    ‹⋀i ts. x = Pre i ts ⟹ P›
    ‹⋀p q. x = Imp p q ⟹ P›
    ‹⋀p q. x = Dis p q ⟹ P›
    ‹⋀p q. x = Con p q ⟹ P›
    ‹⋀p. x = Exi p ⟹ P›
    ‹⋀p. x = Uni p ⟹ P›
    ‹⋀i ts. x = Neg (Pre i ts) ⟹ P›
    ‹⋀p q. x = Neg (Imp p q) ⟹ P›
    ‹⋀p q. x = Neg (Dis p q) ⟹ P›
    ‹⋀p q. x = Neg (Con p q) ⟹ P›
    ‹⋀p. x = Neg (Exi p) ⟹ P›
    ‹⋀p. x = Neg (Uni p) ⟹ P›
    ‹⋀p. x = Neg (Neg p) ⟹ P›
  shows P
  using assms
proof (induct x)
  case (Neg p)
  then show ?case
    by (cases p) simp_all
qed simp_all

lemma parts_exhaust
  [case_names AlphaDis AlphaImp AlphaCon BetaDis BetaImp BetaCon
    DeltaUni DeltaExi NegNeg GammaExi GammaUni Other]:
  assumes
    ‹⋀p q. r = AlphaDis ⟹ x = Dis p q ⟹ P›
    ‹⋀p q. r = AlphaImp ⟹ x = Imp p q ⟹ P›
    ‹⋀p q. r = AlphaCon ⟹ x = Neg (Con p q) ⟹ P›
    ‹⋀p q. r = BetaDis ⟹ x = Neg (Dis p q) ⟹ P›
    ‹⋀p q. r = BetaImp ⟹ x = Neg (Imp p q) ⟹ P›
    ‹⋀p q. r = BetaCon ⟹ x = Con p q ⟹ P›
    ‹⋀p. r = DeltaUni ⟹ x = Uni p ⟹ P›
    ‹⋀p. r = DeltaExi ⟹ x = Neg (Exi p) ⟹ P›
    ‹⋀p. r = NegNeg ⟹ x = Neg (Neg p) ⟹ P›
    ‹⋀p. r = GammaExi ⟹ x = Exi p ⟹ P›
    ‹⋀p. r = GammaUni ⟹ x = Neg (Uni p) ⟹ P›
    ‹∀A. parts A r x = [[x]] ⟹ P›
  shows P
  using assms
proof (cases r)
  case BetaCon
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (Con p q)
    then show ?thesis
      using BetaCon assms by blast
  qed (simp_all add: parts_def)
next
  case BetaImp
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegImp p q)
    then show ?thesis
      using BetaImp assms by blast
  qed (simp_all add: parts_def)
next
  case DeltaUni
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (Uni p)
    then show ?thesis
      using DeltaUni assms by fast
  qed (simp_all add: parts_def)
next
  case DeltaExi
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegExi p)
    then show ?thesis
      using DeltaExi assms by fast
  qed (simp_all add: parts_def)
next
  case n: NegNeg
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegNeg p)
    then show ?thesis
      using n assms by fast
  qed (simp_all add: parts_def)
next
  case GammaExi
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (Exi p)
    then show ?thesis
      using GammaExi assms by fast
  qed (simp_all add: parts_def)
next
  case GammaUni
  then show ?thesis
    using assms
  proof (cases x rule: Neg_exhaust)
    case (NegUni p)
    then show ?thesis
      using GammaUni assms by fast
  qed (simp_all add: parts_def)
qed (cases x rule: Neg_exhaust, simp_all add: parts_def)+

subsection ‹Unaffected formulas›
text ‹We need some lemmas to show that formulas to which rules do not apply are not lost.›

text ‹This function returns True if the rule applies to the formula, and False otherwise.›
definition affects :: ‹rule ⇒ fm ⇒ bool› where
  ‹affects r p ≡ case (r, p) of
    (AlphaDis, Dis _ _) ⇒ True
  | (AlphaImp, Imp _ _) ⇒ True
  | (AlphaCon, Neg (Con _ _)) ⇒ True
  | (BetaCon, Con _ _) ⇒ True
  | (BetaImp, Neg (Imp _ _)) ⇒ True
  | (BetaDis, Neg (Dis _ _)) ⇒ True
  | (DeltaUni, Uni _) ⇒ True
  | (DeltaExi, Neg (Exi _)) ⇒ True
  | (NegNeg, Neg (Neg _)) ⇒ True
  | (GammaExi, Exi _) ⇒ False
  | (GammaUni, Neg (Uni _)) ⇒ False
  | (_,  _) ⇒ False›

text ‹If a rule does not affect a formula, that formula will be in the sequent obtained after
  applying the rule.›
lemma parts_preserves_unaffected:
  assumes ‹¬ affects r p› ‹z' ∈ set (parts A r p)›
  shows ‹p ∈ set z'›
  using assms unfolding affects_def
  by (cases r p rule: parts_exhaust) (simp_all add: parts_def)

text ‹The ‹list_prod› function computes the Cartesian product.›
lemma list_prod_is_cartesian:
  ‹set (list_prod hs ts) = {h @ t |h t. h ∈ set hs ∧ t ∈ set ts}›
  by (induct ts) auto

text ‹The ‹children› function produces the Cartesian product of the branches from the first formula
and the branches from the rest of the sequent.›
lemma set_children_Cons:
  ‹set (children A r (p # z)) =
    {hs @ ts |hs ts. hs ∈ set (parts A r p) ∧
      ts ∈ set (children (remdups (A @ subtermFms (concat (parts A r p)))) r z)}›
  using list_prod_is_cartesian by (metis children.simps(2))

text ‹The ‹children› function does not change unaffected formulas.›
lemma children_preserves_unaffected:
  assumes ‹p ∈ set z› ‹¬ affects r p› ‹z' ∈ set (children A r z)›
  shows ‹p ∈ set z'›
  using assms parts_preserves_unaffected set_children_Cons
  by (induct z arbitrary: A z') auto

text ‹The ‹effect› function does not change unaffected formulas.›
lemma effect_preserves_unaffected:
  assumes ‹p ∈ set z› and ‹¬ affects r p› and ‹(B, z') |∈| effect r (A, z)›
  shows ‹p ∈ set z'›
  using assms children_preserves_unaffected
  unfolding effect_def
  by (smt (verit, best) Pair_inject femptyE fimageE fset_of_list_elem old.prod.case)

subsection ‹Affected formulas›
text ‹We need some lemmas to show that formulas to which rules do apply are decomposed into their
  constituent parts correctly.›

text ‹If a formula occurs in a sequent on a child branch generated by ‹children›, it was part of
  the current sequent.›
lemma parts_in_children:
  assumes ‹p ∈ set z› ‹z' ∈ set (children A r z)›
  shows ‹∃B xs. set A ⊆ set B ∧ xs ∈ set (parts B r p) ∧ set xs ⊆ set z'›
  using assms
proof (induct z arbitrary: A z')
  case (Cons a _)
  then show ?case
  proof (cases ‹a = p›)
    case True
    then show ?thesis
      using Cons(3) set_children_Cons by fastforce
  next
    case False
    then show ?thesis
      using Cons set_children_Cons
      by (smt (verit, del_insts) le_sup_iff mem_Collect_eq set_ConsD set_append set_remdups subset_trans sup_ge2)
  qed
qed simp

text ‹If ‹effect› contains something, then the input sequent is not an axiom.›
lemma ne_effect_not_branchDone: ‹(B, z') |∈| effect r (A, z) ⟹ ¬ branchDone z›
  by (cases ‹branchDone z›) simp_all

text ‹The ‹effect› function decomposes formulas in the sequent using the ‹parts› function.
  (Unless the sequent is an axiom, in which case no child branches are generated.)›
lemma parts_in_effect:
  assumes ‹p ∈ set z› and ‹(B, z') |∈| effect r (A, z)›
  shows ‹∃C xs. set A ⊆ set C ∧ xs ∈ set (parts C r p) ∧ set xs ⊆ set z'›
  using assms parts_in_children ne_effect_not_branchDone
  by (smt (verit, ccfv_threshold) Pair_inject effect.simps fimageE fset_of_list_elem le_sup_iff
      set_append set_remdups)

text ‹Specifically, this applied to the double negation elimination rule and the GammaUni rule.›
corollary ‹Neg (Neg p) ∈ set z ⟹ (B, z') |∈| effect NegNeg (A, z) ⟹ p ∈ set z'›
  using parts_in_effect unfolding parts_def by fastforce

corollary ‹Neg (Uni p) ∈ set z ⟹ (B, z') |∈| effect GammaUni (A, z) ⟹
    set (map (λt. Neg (sub 0 t p)) A) ⊆ set z'›
  using parts_in_effect unfolding parts_def by fastforce

text ‹If the sequent is not an axiom, and the rule and sequent match, all of the child branches
  generated by ‹children› will be included in the proof tree.›
lemma eff_children:
  assumes ‹¬ branchDone z› ‹eff r (A, z) ss›
  shows ‹∀z' ∈ set (children (remdups (A @ subtermFms z)) r z). ∃B. (B, z') |∈| ss›
  using assms unfolding eff_def using fset_of_list_elem by fastforce

subsection ‹Generating new function names›
text ‹We need to show that the ‹generateNew› function actually generates new function names.
  This requires a few lemmas about the interplay between ‹max› and ‹foldr›.›

lemma foldr_max:
  fixes xs :: ‹nat list›
  shows ‹foldr max xs 0 = (if xs = [] then 0 else Max (set xs))›
  by (induct xs) simp_all

lemma Suc_max_new:
  fixes xs :: ‹nat list›
  shows ‹Suc (foldr max xs 0) ∉ set xs›
proof (cases xs)
  case (Cons x xs)
  then have ‹foldr max (x # xs) 0 = Max (set (x # xs))›
    using foldr_max by simp
  then show ?thesis
    using Cons by (metis List.finite_set Max.insert add_0 empty_iff list.set(2) max_0_1(2)
        n_not_Suc_n nat_add_max_left plus_1_eq_Suc remdups.simps(2) set_remdups)
qed simp

lemma listFunTm_paramst: ‹set (listFunTm t) = paramst t› ‹set (listFunTms ts) = paramsts ts›
  by (induct t and ts rule: paramst.induct paramsts.induct) auto

subsection ‹Finding axioms›

text ‹The ‹branchDone› function correctly determines whether a sequent is an axiom.›
lemma branchDone_contradiction: ‹branchDone z ⟷ (∃p. p ∈ set z ∧ Neg p ∈ set z)›
  by (induct z rule: branchDone.induct) auto

subsection ‹Subterms›
text ‹We need a few lemmas about the behaviour of our subterm functions.›

text ‹Any term is a subterm of itself.›
lemma subtermTm_refl [simp]: ‹t ∈ set (subtermTm t)›
  by (induct t) simp_all

text ‹The arguments of a predicate are subterms of it.›
lemma subterm_Pre_refl: ‹set ts ⊆ set (subtermFm (Pre n ts))›
  by (induct ts) auto

text ‹The arguments of function are subterms of it.›
lemma subterm_Fun_refl: ‹set ts ⊆ set (subtermTm (Fun n ts))›
  by (induct ts) auto

text ‹This function computes the predicates in a formula.
  We will use this function to help prove the final lemma in this section.›
primrec preds :: ‹fm ⇒ fm set› where
  ‹preds (Pre n ts) = {Pre n ts}›
| ‹preds (Imp p q) = preds p ∪ preds q›
| ‹preds (Dis p q) = preds p ∪ preds q›
| ‹preds (Con p q) = preds p ∪ preds q›
| ‹preds (Exi p) = preds p›
| ‹preds (Uni p) = preds p›
| ‹preds (Neg p) = preds p›

text ‹If a term is a subterm of a formula, it is a subterm of some predicate in the formula.›
lemma subtermFm_preds: ‹t ∈ set (subtermFm p) ⟷ (∃pre ∈ preds p. t ∈ set (subtermFm pre))›
  by (induct p) auto

lemma preds_shape: ‹pre ∈ preds p ⟹ ∃n ts. pre = Pre n ts›
  by (induct p) auto

text ‹If a function is a subterm of a formula, so are the arguments of that function.›
lemma fun_arguments_subterm:
  assumes ‹Fun n ts ∈ set (subtermFm p)›
  shows ‹set ts ⊆ set (subtermFm p)›
proof -
  obtain pre where pre: ‹pre ∈ preds p› ‹Fun n ts ∈ set (subtermFm pre)›
    using assms subtermFm_preds by blast
  then obtain n' ts' where ‹pre = Pre n' ts'›
    using preds_shape by blast
  then have ‹set ts ⊆ set (subtermFm pre)›
    using subtermTm_le pre by force
  then have ‹set ts ⊆ set (subtermFm p)›
    using pre subtermFm_preds by blast
  then show ?thesis
    by blast
qed

end