Additional substitution extension law

isabelle-utp · Jan 17, 2025 · 747730b · 747730b
1 parent 30a15eb
commit 747730b
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Extension.thy b/Extension.thy
@@ -96,6 +96,9 @@ lemma apply_subst_ext [alpha]:
   "vwb_lens x \<Longrightarrow> (\<sigma> \<dagger> e) \<up> x = (\<sigma> \<up>\<^sub>s x) \<dagger> (e \<up> x)"
   by (expr_auto)
 
+lemma subst_aext_compose [alpha]: "(\<sigma> \<up>\<^sub>s x) \<up>\<^sub>s y = \<sigma> \<up>\<^sub>s y:x"
+  by (expr_simp)
+
 lemma subst_aext_comp [usubst]:
   "vwb_lens a \<Longrightarrow> (\<sigma> \<up>\<^sub>s a) \<circ>\<^sub>s (\<rho> \<up>\<^sub>s a) = (\<sigma> \<circ>\<^sub>s \<rho>) \<up>\<^sub>s a"
   by expr_auto