Theory utp_meta_subst

section ‹ Meta-level Substitution ›

theory utp_meta_subst
imports utp_subst utp_tactics
begin

text ‹ Meta substitution substitutes a HOL variable in a UTP expression for another UTP expression.
  It is analogous to UTP substitution, but acts on functions. ›
  
lift_definition msubst :: "('b ⇒ ('a, 'α) uexpr) ⇒ ('b, 'α) uexpr ⇒ ('a, 'α) uexpr"
is "λ F v b. F (v b) b" .
  
update_uexpr_rep_eq_thms ― ‹ Reread @{text rep_eq} theorems. ›
    
syntax
  "_msubst"   :: "logic ⇒ pttrn ⇒ logic ⇒ logic" ("(_⟦_→_⟧)" [990,0,0] 991)

translations
  "_msubst P x v" == "CONST msubst (λ x. P) v"
     
lemma msubst_lit [usubst]: "«x»⟦x→v⟧ = v"
  by (pred_auto)

lemma msubst_const [usubst]: "P⟦x→v⟧ = P"
  by (pred_auto) 

lemma msubst_pair [usubst]: "(P x y)⟦(x, y) → (e, f)⇩u⟧ = (P x y)⟦x → e⟧⟦y → f⟧"
  by (rel_auto)

lemma msubst_lit_2_1 [usubst]: "«x»⟦(x,y)→(u,v)⇩u⟧ = u"
  by (pred_auto)

lemma msubst_lit_2_2 [usubst]: "«y»⟦(x,y)→(u,v)⇩u⟧ = v"
  by (pred_auto)

lemma msubst_lit' [usubst]: "«y»⟦x→v⟧ = «y»"
  by (pred_auto)

lemma msubst_lit'_2 [usubst]: "«z»⟦(x,y)→v⟧ = «z»"
  by (pred_auto)
 
lemma msubst_uop [usubst]: "(uop f (v x))⟦x→u⟧ = uop f ((v x)⟦x→u⟧)"
  by (rel_auto)

lemma msubst_uop_2 [usubst]: "(uop f (v x y))⟦(x,y)→u⟧ = uop f ((v x y)⟦(x,y)→u⟧)"
  by (pred_simp, pred_simp)
 
lemma msubst_bop [usubst]: "(bop f (v x) (w x))⟦x→u⟧ = bop f ((v x)⟦x→u⟧) ((w x)⟦x→u⟧)"
  by (rel_auto)

lemma msubst_bop_2 [usubst]: "(bop f (v x y) (w x y))⟦(x,y)→u⟧ = bop f ((v x y)⟦(x,y)→u⟧) ((w x y)⟦(x,y)→u⟧)"
  by (pred_simp, pred_simp)

lemma msubst_var [usubst]:
  "(utp_expr.var x)⟦y→u⟧ = utp_expr.var x"
  by (pred_simp)

lemma msubst_var_2 [usubst]:
  "(utp_expr.var x)⟦(y,z)→u⟧ = utp_expr.var x"
  by (pred_simp)+
        
lemma msubst_unrest [unrest]: "⟦ ⋀ v. x ♯ P(v); x ♯ k ⟧ ⟹ x ♯ P(v)⟦v→k⟧"
  by (pred_auto)
  
end