# Theory Natural_Deduction

```theory Natural_Deduction
imports
Abstract_Completeness.Abstract_Completeness
Abstract_Rules
Entailment
begin

text ‹Our formalization of natural deduction builds on @{theory Abstract_Completeness.Abstract_Completeness} and refines and
concretizes the structure given there as follows
▪ The judgements are entailments consisting of a finite set of assumptions and a conclusion, which
are abstract formulas in the sense of @{theory Incredible_Proof_Machine.Abstract_Formula}.
▪ The abstract rules given in @{theory Incredible_Proof_Machine.Abstract_Rules} are used to decide the validity of a
step in the derivation.
›

text ‹A single setep in the derivation can either be the axiom rule, the cut rule, or one
of the given rules in @{theory Incredible_Proof_Machine.Abstract_Rules}.›

datatype 'rule NatRule = Axiom | NatRule 'rule | Cut

text ‹The following locale is still abstract in the set of rules (‹nat_rule›), but implements
the bookkeeping logic for assumptions, the @{term Axiom} rule and the @{term Cut} rule.›

locale ND_Rules_Inst =
Abstract_Formulas freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP
for freshenLC :: "nat ⇒ 'var ⇒ 'var"
and renameLCs :: "('var ⇒ 'var) ⇒ 'form ⇒ 'form"
and lconsts :: "'form ⇒ 'var set"
and closed :: "'form ⇒ bool"
and subst :: "'subst ⇒ 'form ⇒ 'form"
and subst_lconsts :: "'subst ⇒ 'var set"
and subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)"
and anyP :: "'form" +

fixes nat_rule :: "'rule ⇒ 'form ⇒ ('form, 'var) antecedent fset ⇒ bool"
and rules :: "'rule stream"
begin

text ‹
▪ An application of the @{term Axiom} rule is valid if the conclusion is among the assumptions.
▪ An application of a @{term NatRule} is more complicated. This requires some natural number
‹a› to rename local variables, and some instantiation ‹s›. It checks that
▪ none of the local variables occur in the context of the judgement.
▪ none of the local variables occur in the instantiation.
Together, this implements the usual freshness side-conditions.
Furthermore, for every antecedent of the rule, the (correctly renamed and instantiated)
hypotheses need to be added to the context.
▪ The @{term Cut} rule is again easy.
›
inductive eff :: "'rule NatRule ⇒ 'form entailment ⇒ 'form entailment fset ⇒ bool" where
"con |∈| Γ
⟹ eff Axiom (Γ ⊢ con) {||}"
|"nat_rule rule c ants
⟹ (⋀ ant f. ant |∈| ants ⟹ f |∈| Γ ⟹ freshenLC a ` (a_fresh ant) ∩ lconsts f = {})
⟹ (⋀ ant. ant |∈| ants ⟹ freshenLC a ` (a_fresh ant) ∩ subst_lconsts s = {})
⟹ eff (NatRule rule)
(Γ ⊢ subst s (freshen a c))
((λant. ((λp. subst s (freshen a p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen a (a_conc ant)))) |`| ants) "
|"eff Cut (Γ ⊢ c') {| (Γ ⊢ c')|}"

inductive_simps eff_Cut_simps[simp]: "eff Cut (Γ ⊢ c) S"

sublocale RuleSystem_Defs where
eff = eff and rules = "Cut ## Axiom ## smap NatRule rules".
end

text ‹Now we instantiate the above locale. We duplicate each abstract rule (which can have multiple
consequents) for each consequent, as the natural deduction formulation can only handle a single
consequent per rule›

begin
inductive natEff_Inst where
"c ∈ set (consequent r) ⟹ natEff_Inst (r,c) c (f_antecedent r)"

definition n_rules where
"n_rules = flat (smap (λr. map (λc. (r,c)) (consequent r)) rules)"

sublocale ND_Rules_Inst _ _ _ _ _ _ _ _ natEff_Inst n_rules ..

text ‹A task is solved if for every conclusion, there is a well-formed and finite tree that proves
this conclusion, using only assumptions given in the task.›

definition solved where
"solved ⟷ (∀ c. c |∈| conc_forms ⟶ (∃ Γ t. fst (root t) = (Γ ⊢ c) ∧ Γ |⊆| ass_forms ∧ wf t ∧ tfinite t))"
end

end
```