Require Export rules.

Section Admissibility.

  Variable V : Type.
  Variable L : modal_operators.

  Variable rules : set (sequent_rule V L).
  Variable hypotheses : set (sequent V L).

  Definition admissible(r : sequent_rule V L) : Prop :=
    every_nth (provable rules hypotheses) (assumptions r) →
      provable rules hypotheses (conclusion r).

  Definition admissible_rule_set(rs : set (sequent_rule V L)) : Prop :=
    ∀(r : sequent_rule V L), rs r → admissible r.

  Lemma admissible_prop :
    ∀(rs : set (sequent_rule V L))(s : sequent V L),
      admissible_rule_set rs →
        (provable rules hypotheses s ↔
           provable (union rs rules) hypotheses s).

  Definition depth_preserving_admissible(r : sequent_rule V L) : Prop :=
    ∀(n : nat),
      every_nth (provable_at_depth rules hypotheses n) (assumptions r) →
        provable_at_depth rules hypotheses n (conclusion r).

  Definition depth_preserving_admissible_rule_set
                                       (rs : set (sequent_rule V L)) : Prop :=
    ∀(r : sequent_rule V L), rs r →
      depth_preserving_admissible r.

  Lemma admissible_depth_preserving_admissible :
    ∀(rs : set (sequent_rule V L)),
      depth_preserving_admissible_rule_set rs → admissible_rule_set rs.

  Lemma delete_depth_admissible_rule :
    ∀(r : sequent_rule V L)(n : nat)(s : sequent V L),
      depth_preserving_admissible r →
      provable_at_depth (add r rules) hypotheses n s →
        provable_at_depth rules hypotheses n s.

  Lemma depth_admissible_prop :
    ∀(r : sequent_rule V L)(s : sequent V L)(n : nat),
      depth_preserving_admissible r →
        (provable_at_depth rules hypotheses n s ↔
           provable_at_depth (add r rules) hypotheses n s).

End Admissibility.

Implicit Arguments admissible [V L].
Implicit Arguments admissible_rule_set [V L].
Implicit Arguments depth_preserving_admissible [V L].
Implicit Arguments depth_preserving_admissible_rule_set [V L].