Require Export modal_formulas propositional_formulas.

Section Renaming.

  Variable V : Type.
  Variable L : modal_operators.

  Variable v_eq : eq_type V.

  Definition renaming(sigma : lambda_subst V L) : Prop :=
    ∀(v : V), prop_form (sigma v).

  Lemma renaming_id_subst : renaming (id_subst).

  Lemma rank_renaming : ∀(sigma : lambda_subst V L),
    renaming sigma → rank_subst 1 sigma.

  Lemma rank_sequent_renaming :
    ∀(s : sequent V L)(n : nat)(sigma : lambda_subst V L),
      renaming sigma →
      rank_sequent n s →
        rank_sequent n (subst_sequent sigma s).

  Lemma propositional_renaming :
    ∀(s : sequent V L)(sigma : lambda_subst V L),
      renaming sigma →
      propositional_sequent s →
        propositional_sequent (subst_sequent sigma s).

  Lemma renaming_subst_compose :
    ∀(sigma rho : lambda_subst V L),
      renaming sigma →
      renaming rho →
        renaming (subst_compose sigma rho).

  Lemma prop_form_renaming :
    ∀(sigma : lambda_subst V L)(f : lambda_formula V L),
      renaming sigma →
      neg_form_maybe prop_form f →
        neg_form_maybe prop_form (subst_form sigma f).

  Lemma prop_sequent_renaming :
    ∀(sigma : lambda_subst V L)(s : sequent V L),
      renaming sigma →
      prop_sequent s →
        prop_sequent (subst_sequent sigma s).

  Lemma prop_form_subst_simple_modal_form :
    ∀(f : lambda_formula V L)(sigma : lambda_subst V L)(v : V),
      In v (prop_var_formula f) →
      simple_modal_form f →
      simple_modal_form (subst_form sigma f) →
        prop_form (sigma v).

  Lemma prop_form_subst_neg_simple_modal_form :
    ∀(f : lambda_formula V L)(sigma : lambda_subst V L)(v : V),
      In v (prop_var_formula f) →
      neg_form_maybe simple_modal_form f →
      neg_form_maybe simple_modal_form (subst_form sigma f) →
        prop_form (sigma v).

  Lemma renaming_limit_subst_simple_modal_sequent :
    ∀(s : sequent V L)(sigma : lambda_subst V L),
      simple_modal_sequent s →
      simple_modal_sequent (subst_sequent sigma s) →
        renaming (limit_subst v_eq (prop_var_sequent s) sigma).

  Lemma simple_modal_form_renaming :
    ∀(sigma : lambda_subst V L)(f : lambda_formula V L),
      renaming sigma →
      simple_modal_form f →
        simple_modal_form (subst_form sigma f).

  Lemma neg_simple_modal_form_renaming :
    ∀(sigma : lambda_subst V L)(f : lambda_formula V L),
      renaming sigma →
      neg_form_maybe simple_modal_form f →
        neg_form_maybe simple_modal_form (subst_form sigma f).

  Lemma simple_modal_sequent_renaming :
    ∀(sigma : lambda_subst V L)(s : sequent V L),
      renaming sigma →
      simple_modal_sequent s →
        simple_modal_sequent (subst_sequent sigma s).

  Definition rename_of_fun(f : V → V) : lambda_subst V L :=
    fun(v : V) ⇒ lf_prop (f v).

  Lemma renaming_rename_of_fun : ∀(f : V → V),
    renaming (rename_of_fun f).

  Lemma rename_of_id : rename_of_fun id = id_subst.

End Renaming.

Implicit Arguments renaming [V L].
Implicit Arguments rename_of_fun [V L].
Implicit Arguments renaming_rename_of_fun [V L].