Theory Psi_Calculi.Close_Subst

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Close_Subst
  imports Agent
begin

context substPsi
begin

definition closeSubst :: "('b::fs_name × ('a::fs_name, 'b, 'c::fs_name) psi × ('a, 'b, 'c) psi) set ⇒ ('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
where "closeSubst Rel ≡ {(Ψ, P, Q) | Ψ P Q. (∀σ. wellFormedSubst σ ⟶ (Ψ, P[<σ>], Q[<σ>]) ∈ Rel)}"

lemma closeSubstI:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "⋀σ. wellFormedSubst σ ⟹ (Ψ, P[<σ>], Q[<σ>]) ∈ Rel"

  shows "(Ψ, P, Q) ∈ closeSubst Rel"
using assms
by(unfold closeSubst_def) auto

lemma closeSubstE:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   σ :: "(name list × 'a list) list"

  assumes "(Ψ, P, Q) ∈ closeSubst Rel"
  and     "wellFormedSubst σ"

  shows "(Ψ, P[<σ>], Q[<σ>]) ∈ Rel"
using assms
by(unfold closeSubst_def) auto

lemma closeSubstClosed:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   p :: "name prm"

  assumes "eqvt Rel"
  and     "(Ψ, P, Q) ∈ closeSubst Rel"

  shows "(p ∙ Ψ, p ∙ P, p ∙ Q) ∈ closeSubst Rel"
proof(rule closeSubstI)
  fix σ
  assume "wellFormedSubst(σ::(name list × 'a list) list)"
  with ‹(Ψ, P, Q) ∈ closeSubst Rel› ‹wellFormedSubst σ›
  have "(Ψ, P[<(rev p ∙ σ)>], Q[<(rev p ∙ σ)>]) ∈ Rel"
    by(rule_tac closeSubstE) auto
  hence "(p ∙ Ψ, p ∙ (P[<(rev p ∙ σ)>]), p ∙ (Q[<(rev p ∙ σ)>])) ∈ Rel"
    by(drule_tac p=p in eqvtI[OF ‹eqvt Rel›]) (simp add: eqvts)
  thus "(p ∙ Ψ, (p ∙ P)[<σ>], (p ∙ Q)[<σ>]) ∈ Rel"
    by(simp del: seqSubs_def add: eqvts)
qed

lemma closeSubstEqvt:
  assumes "eqvt Rel"

  shows "eqvt(closeSubst Rel)"
proof(auto simp add: eqvt_def)
  fix Ψ P Q p
  assume "(Ψ, P, Q) ∈ closeSubst Rel"
  thus "((p::name prm) ∙ Ψ, p ∙ P, p ∙ Q) ∈ closeSubst Rel"
    by(drule_tac p=p in closeSubstClosed[OF ‹eqvt Rel›]) (simp add: eqvts)
qed

lemma closeSubstUnfold:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   σ :: "(name list × 'a list) list"

  assumes "(Ψ, P, Q) ∈ closeSubst Rel"
  and     "wellFormedSubst σ"

  shows "(Ψ, P[<σ>], Q[<σ>]) ∈ closeSubst Rel"
proof(rule closeSubstI)
  fix σ'::"(name list × 'a list) list"
  assume "wellFormedSubst σ'"
  with ‹wellFormedSubst σ› have "wellFormedSubst(σ@σ')" by simp
  with ‹(Ψ, P, Q) ∈ closeSubst Rel› have "(Ψ, P[<(σ@σ')>], Q[<(σ@σ')>]) ∈ Rel"
    by(rule closeSubstE)
  thus "(Ψ, P[<σ>][<σ'>], Q[<σ>][<σ'>]) ∈ Rel"
    by simp
qed

end

end