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›

context Abstract_Task 
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