theory Abstract_Rules imports Abstract_Formula begin text ‹ Next, we can define a logic, by giving a set of rules. In order to connect to the AFP entry Abstract Completeness, the set of rules is a stream; the only relevant effect of this is that the set is guaranteed to be non-empty and at most countable. This has no further significance in our development. Each antecedent of a rule consists of ▪ a set of fresh variables ▪ a set of hypotheses that may be used in proving the conclusion of the antecedent and ▪ the conclusion of the antecedent. Our rules allow for multiple conclusions (but must have at least one). In order to prove the completeness (but incidentally not to prove correctness) of the incredible proof graphs, there are some extra conditions about the fresh variables in a rule. ▪ These need to be disjoint for different antecedents. ▪ They need to list all local variables occurring in either the hypothesis and the conclusion. ▪ The conclusions of a rule must not contain any local variables. › datatype ('form, 'var) antecedent = Antecedent (a_hyps: "'form fset") (a_conc: "'form") (a_fresh: "'var set") abbreviation plain_ant :: "'form ⇒ ('form, 'var) antecedent" where "plain_ant f ≡ Antecedent {||} f {}" locale Abstract_Rules = 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 antecedent :: "'rule ⇒ ('form, 'var) antecedent list" and consequent :: "'rule ⇒ 'form list" and rules :: "'rule stream" assumes no_empty_conclusions: "∀xs∈sset rules. consequent xs ≠ []" assumes no_local_consts_in_consequences: "∀xs∈sset rules. ⋃(lconsts ` (set (consequent xs))) = {}" assumes no_multiple_local_consts: "⋀ r i i' . r ∈ sset rules ⟹ i < length (antecedent r) ⟹ i' < length (antecedent r) ⟹ a_fresh (antecedent r ! i) ∩ a_fresh (antecedent r ! i') = {} ∨ i = i'" assumes all_local_consts_listed: "⋀ r p. r ∈ sset rules ⟹ p ∈ set (antecedent r) ⟹ lconsts (a_conc p) ∪ (⋃(lconsts ` fset (a_hyps p))) ⊆ a_fresh p " begin definition f_antecedent :: "'rule ⇒ ('form, 'var) antecedent fset" where "f_antecedent r = fset_from_list (antecedent r)" definition "f_consequent r = fset_from_list (consequent r)" end text ‹ Finally, an abstract task specifies what a specific proof should prove. In particular, it gives a set of assumptions that may be used, and lists the conclusions that need to be proven. Both assumptions and conclusions are closed expressions that may not be changed by substitutions. › locale Abstract_Task = Abstract_Rules freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP antecedent consequent rules 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" and antecedent :: "'rule ⇒ ('form, 'var) antecedent list" and consequent :: "'rule ⇒ 'form list" and rules :: "'rule stream" + fixes assumptions :: "'form list" fixes conclusions :: "'form list" assumes assumptions_closed: "⋀ a. a ∈ set assumptions ⟹ closed a" assumes conclusions_closed: "⋀ c. c ∈ set conclusions ⟹ closed c" begin definition ass_forms where "ass_forms = fset_from_list assumptions" definition conc_forms where "conc_forms = fset_from_list conclusions" lemma mem_ass_forms[simp]: "a |∈| ass_forms ⟷ a ∈ set assumptions" by (auto simp add: ass_forms_def) lemma mem_conc_forms[simp]: "a |∈| conc_forms ⟷ a ∈ set conclusions" by (auto simp add: conc_forms_def) lemma subst_freshen_assumptions[simp]: assumes "pf ∈ set assumptions" shows "subst s (freshen a pf) = pf " using assms assumptions_closed by (simp add: closed_no_lconsts freshen_def rename_closed subst_closed) lemma subst_freshen_conclusions[simp]: assumes "pf ∈ set conclusions" shows "subst s (freshen a pf) = pf " using assms conclusions_closed by (simp add: closed_no_lconsts freshen_def rename_closed subst_closed) lemma subst_freshen_in_ass_formsI: assumes "pf ∈ set assumptions" shows "subst s (freshen a pf) |∈| ass_forms" using assms by simp lemma subst_freshen_in_conc_formsI: assumes "pf ∈ set conclusions" shows "subst s (freshen a pf) |∈| conc_forms" using assms by simp end end