Require Export formulas.

Section Propositional_formulas.

  Variable V : Type.
  Variable L : modal_operators.

  Definition propositional(f : lambda_formula V L) : Prop :=
    rank_formula 1 f.

  Lemma propositional_lf_prop : ∀(v : V),
    propositional (lf_prop v).

  Lemma propositional_neg : ∀(f : lambda_formula V L),
    propositional (lf_neg f) → propositional f.

  Lemma propositional_neg_inv : ∀(f : lambda_formula V L),
    propositional f → propositional (lf_neg f).

  Lemma propositional_lf_and : ∀(f1 f2 : lambda_formula V L),
    propositional f1 →
    propositional f2 →
      propositional (lf_and f1 f2).

  Lemma propositional_and_left : ∀(f1 f2 : lambda_formula V L),
    propositional (lf_and f1 f2) → propositional f1.

  Lemma propositional_and_right : ∀(f1 f2 : lambda_formula V L),
    propositional (lf_and f1 f2) → propositional f2.

  Lemma propositional_tcc_modal :
    ∀{X : Type}(op : operator L)
          (args : counted_list (lambda_formula V L) (arity L op)),
      propositional (lf_modal op args) → X.

  Lemma propositional_lambda_or :
    ∀(f1 f2 : lambda_formula V L),
      propositional f1 →
      propositional f2 →
        propositional (lambda_or f1 f2).


  Definition propositional_sequent(s : sequent V L) : Prop :=
    rank_sequent 1 s.

  Lemma propositional_sequent_empty : propositional_sequent [].

  Lemma propositional_sequent_head :
    ∀(s : sequent V L)(f : lambda_formula V L),
      propositional_sequent (f :: s) → propositional f.

  Lemma propositional_sequent_tail :
    ∀(s : sequent V L)(f : lambda_formula V L),
      propositional_sequent (f :: s) → propositional_sequent s.

  Lemma propositional_or_formula :
    ∀(nonempty_v : V)(s : sequent V L),
      propositional_sequent s →
        propositional (or_formula_of_sequent s nonempty_v).

  Lemma propositional_sequent_cons :
    ∀(s : sequent V L)(f : lambda_formula V L),
      propositional f →
      propositional_sequent s →
        propositional_sequent (f :: s).

  Lemma propositional_sequent_append :
    ∀(sl sr : sequent V L),
      propositional_sequent sl →
      propositional_sequent sr →
        propositional_sequent (sl ++ sr).

  Lemma propositional_sequent_append_left :
    ∀(sl sr : sequent V L),
      propositional_sequent (sl ++ sr) →
        propositional_sequent sl.

  Lemma propositional_sequent_append_right :
    ∀(sl sr : sequent V L),
      propositional_sequent (sl ++ sr) →
        propositional_sequent sr.

  Lemma propositional_sequent_cons_append :
    ∀(l1 l2 : sequent V L)(f1 f2 : lambda_formula V L),
      (propositional f1 → propositional f2) →
      propositional_sequent (l1 ++ f1 :: l2) →
        propositional_sequent (l1 ++ f2 :: l2).

  Lemma prop_form_is_propositional : ∀(f : lambda_formula V L),
    prop_form f → propositional f.

  Lemma prop_sequent_is_propositional : ∀(s : sequent V L),
    prop_sequent s → propositional_sequent s.

End Propositional_formulas.

Implicit Arguments propositional [[V] [L]].
Implicit Arguments propositional_neg [V L].
Implicit Arguments propositional_and_left [V L].
Implicit Arguments propositional_and_right [V L].
Implicit Arguments propositional_tcc_modal [V L X].
Implicit Arguments propositional_sequent [[V] [L]].
Implicit Arguments propositional_sequent_tail [V L].
Implicit Arguments propositional_lambda_or [V L].
Implicit Arguments propositional_sequent_append_right [V L].
Implicit Arguments propositional_sequent_head [V L].
Implicit Arguments propositional_sequent_append [V L].
Implicit Arguments propositional_or_formula [V L].
Implicit Arguments prop_sequent_is_propositional [V L].