Quelle  utp_meta_subst.thy

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)

syntax_consts
  "_msubst" == msubst

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