# 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 AlphaCon = DeltaExi›
| ‹next_rule DeltaExi = DeltaUni›
| ‹next_rule DeltaUni = BetaImp›
| ‹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 AlphaCon = 3›
| ‹rule_index DeltaExi = 4›
| ‹rule_index DeltaUni = 5›
| ‹rule_index BetaImp = 6›
| ‹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
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
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
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
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
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
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
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
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 (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)
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
```