Load Sec2_EqualityMemberships.

Definition substitution := variable -> name.

Definition substitutions := list substitution.

Definition null : name := Pub "null".

Definition subs_empty : substitution :=
  (fun _ => null).

Definition update (sigma : substitution)
                   (v : variable ) (n : name) :=
  fun x' => if beq_string v x' then n else sigma x'.

Notation "v '!->' n" := (update subs_empty v n) (at level 100).
Notation "v '!->' n ';' sigma" := (update sigma v n)
                              (at level 100, n at next level, right associativity).

Definition compose (sigma1 : substitution) (sigma2 : substitution) : variable -> name :=
  fun v => if (beq_name (sigma1 v) null) then (sigma2 v) else (sigma1 v).

Definition substsAgree (sigma1 : substitution) (sigma2 : substitution) : Prop :=
  forall x, sigma1 x = null \/ sigma2 x = null \/ sigma1 x=sigma2 x.

Lemma agreeSubstComposeOrder : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall x, compose sigma1 sigma2 x = compose sigma2 sigma1 x.

Definition exampleSubs := "ltkA" !-> Fresh_S "ltkA"; subs_empty.

Fixpoint applySubBaseTerm (sigma:substitution) (t:baseTerm) : baseTerm :=
  match t with
  | Var v => if (beq_name (sigma v) null) then (Var v) else Name (sigma v)
  | Name n => Name n
  end.

Definition applySubBaseTerms (sigma:substitution) (ts:baseTerms) : baseTerms
     := map (applySubBaseTerm sigma) ts.

Fixpoint applySubTerm (sigma:substitution) (t:term) : term :=
  match t with
  | Func f bts => Func f (applySubBaseTerms sigma bts)
  | Bterm bt => Bterm (applySubBaseTerm sigma bt)
  end.

Definition applySubTerms : substitution -> terms -> terms
     := fun sigma => map (applySubTerm sigma).

Fixpoint applySubActionLabel (sigma:substitution) (lb:actionLabel) : actionLabel :=
  match lb with
   | ActLabel n ts => ActLabel n (applySubTerms sigma ts)
  end.

Definition applySubLabel (sigma:substitution) (lb:label) : label :=
  match lb with
    | BasicLabel ll => BasicLabel (map ( applySubActionLabel sigma) ll)
    | LoggedLabel lg ll => LoggedLabel (applySubActionLabel sigma lg) (map (applySubActionLabel sigma) ll)
    | LoggedSIDLabel t lg ll => LoggedSIDLabel (applySubBaseTerm sigma t)(applySubActionLabel sigma lg) (map (applySubActionLabel sigma) ll)
  end.

Fixpoint applySubFact (sigma:substitution) (f:fact) : fact :=
match f with
  | IN terms => IN (applySubTerms sigma terms)
  | OUT terms => OUT (applySubTerms sigma terms)
  | K terms => K (applySubTerms sigma terms)
  | STATE name terms => STATE name (applySubTerms sigma terms)
  | FR_P freshName => FR_P (applySubBaseTerm sigma freshName)
  end.

Definition applySubFacts : substitution -> facts -> facts
     := fun sigma => map (applySubFact sigma).

Fixpoint applySubRule (sigma:substitution) (r:rule) : rule :=
match r with
  | RuleSetup f1 l f2 => RuleSetup (applySubFacts sigma f1) (applySubLabel sigma l) (applySubFacts sigma f2)
  | RuleProto f1 l f2 => RuleProto (applySubFacts sigma f1) (applySubLabel sigma l) (applySubFacts sigma f2)
end.

Definition applySubRuleList : substitution -> ruleList -> ruleList := fun sigma => map (applySubRule sigma).

Definition applySubRuleLists : substitution -> list ruleList -> list ruleList := fun sigma => map (applySubRuleList sigma).

Definition applySubTrace : substitution -> trace -> trace := fun sigma => map (applySubLabel sigma).

Definition applySubTraces : substitution -> list trace -> list trace := fun sigma => map (applySubTrace sigma).

Lemma agreeSubstComposeOrderBaseTerm : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall bt, applySubBaseTerm (compose sigma1 sigma2) bt
                                            = applySubBaseTerm (compose sigma2 sigma1) bt.

Lemma agreeSubstComposeOrderBaseTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall bt, applySubBaseTerms (compose sigma1 sigma2) bt
                                            = applySubBaseTerms (compose sigma2 sigma1) bt.

Lemma agreeSubstComposeOrderTerm : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerm (compose sigma1 sigma2) tm
                                            = applySubTerm (compose sigma2 sigma1) tm.

Lemma agreeSubstComposeOrderTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerms (compose sigma1 sigma2) tm
                                            = applySubTerms (compose sigma2 sigma1) tm.

Lemma agreeSubstComposeOrderActionLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall al, applySubActionLabel (compose sigma1 sigma2) al
                                            = applySubActionLabel (compose sigma2 sigma1) al.

Lemma agreeSubstComposeOrderLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall l, applySubLabel (compose sigma1 sigma2) l
                                            = applySubLabel (compose sigma2 sigma1) l.

Lemma agreeSubstComposeOrderTrace : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall t, applySubTrace (compose sigma1 sigma2) t
                                            = applySubTrace (compose sigma2 sigma1) t.