Renaming
Require Export modal_formulas propositional_formulas.
Section Renaming.
Variable V : Type.
Variable L : modal_operators.
need a decidable equality for the limit_subst results
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].