imports Abstract_Completeness Abstract_Rules Entailment

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 (@{text 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 @{text a} to rename local variables, and some instantiation @{text 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