Theory Abstract_Rules

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