From f00bbbd9fc7cafcfd3629921b442ab964077f467 Mon Sep 17 00:00:00 2001
From: Simon Foster <simondf@gmail.com>
Date: Fri, 24 Jan 2025 14:25:38 +0000
Subject: [PATCH] Added some commentary, and using alphabet extension.

---
 utp_des_core.thy | 22 ++++++++++++++++++++++
 utp_des_laws.thy |  5 +++++
 utp_des_prog.thy | 11 ++++-------
 3 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/utp_des_core.thy b/utp_des_core.thy
index 21c2621..1a434ac 100644
--- a/utp_des_core.thy
+++ b/utp_des_core.thy
@@ -4,6 +4,11 @@ theory utp_des_core
   imports UTP2.utp
 begin 
 
+text \<open> UTP designs~\cite{Cavalcanti04,Hoare&98} are a subset of the alphabetised relations that
+  use a boolean observational variable $ok$ to record the start and termination of a program. For 
+  more information on designs please see Chapter 3 of the UTP book~\cite{Hoare&98}, or
+  the more accessible designs tutorial~\cite{Cavalcanti04}. \<close>
+
 alphabet des_vars = 
   ok :: bool
 
@@ -18,6 +23,23 @@ syntax
 translations
   "_svid_des_alpha" => "CONST des_vars.more\<^sub>L"
 
+text \<open> Define the lens functor for designs \<close>
+  
+definition lmap_des_vars :: "('\<alpha> \<Longrightarrow> '\<beta>) \<Rightarrow> ('\<alpha> des_vars_scheme \<Longrightarrow> '\<beta> des_vars_scheme)" ("lmap\<^sub>D")
+where [lens_defs]: "lmap_des_vars = lmap[des_vars]"
+
+syntax "_lmap_des_vars" :: "svid \<Rightarrow> svid" ("lmap\<^sub>D[_]")
+translations "_lmap_des_vars a" => "CONST lmap_des_vars a"
+
+lemma lmap_des_vars: "vwb_lens f \<Longrightarrow> vwb_lens (lmap_des_vars f)"
+  by (unfold_locales, auto simp add: lens_defs alpha_defs)
+
+lemma lmap_id: "lmap\<^sub>D 1\<^sub>L = 1\<^sub>L"
+  by (simp add: lens_defs alpha_defs fun_eq_iff)
+
+lemma lmap_comp: "lmap\<^sub>D (f ;\<^sub>L g) = lmap\<^sub>D f ;\<^sub>L lmap\<^sub>D g"
+  by (simp add: lens_defs alpha_defs fun_eq_iff)
+
 text \<open> The following notations define liftings from non-design predicates into design
   predicates using alphabet extensions. \<close>
 
diff --git a/utp_des_laws.thy b/utp_des_laws.thy
index c0f7ab2..1948ffa 100644
--- a/utp_des_laws.thy
+++ b/utp_des_laws.thy
@@ -1,7 +1,12 @@
+section \<open> Design Theorems and Laws \<close>
+
 theory utp_des_laws
   imports utp_des_core
 begin 
 
+text \<open> Two named theorem sets exist are created to group theorems that, respectively, provide
+  pre-postcondition definitions, and simplify operators to their normal design form. \<close>
+
 named_theorems ndes and ndes_simp
 
 subsection \<open> Lifting, Unrestriction, and Substitution \<close>
diff --git a/utp_des_prog.thy b/utp_des_prog.thy
index 00546b1..a689a5b 100644
--- a/utp_des_prog.thy
+++ b/utp_des_prog.thy
@@ -95,24 +95,21 @@ subsection \<open> Frames and Extensions \<close>
 definition des_frame :: "('\<alpha> \<Longrightarrow> '\<beta>) \<Rightarrow> '\<beta> des_hrel \<Rightarrow> '\<beta> des_hrel" where
 [pred]: "des_frame x P = $(ok,\<^bold>v\<^sub>D:x):[P]"
 
-(*
 definition des_frame_ext :: "('\<alpha> \<Longrightarrow> '\<beta>) \<Rightarrow> '\<alpha> des_hrel \<Rightarrow> '\<beta> des_hrel" where
-[pred]: "des_frame_ext a P = des_frame a (rel_aext P (lmap\<^sub>D a))"
+[pred]: "des_frame_ext a P = des_frame a (P \<up>\<^sub>2 lmap\<^sub>D[a])"
 
 syntax
   "_des_frame"     :: "salpha \<Rightarrow> logic \<Rightarrow> logic" ("_:[_]\<^sub>D" [99,0] 100)
-  "_des_frame_ext" :: "salpha \<Rightarrow> logic \<Rightarrow> logic" ("_:[_]\<^sub>D\<^sup>+" [99,0] 100)
+  "_des_frame_ext" :: "svid \<Rightarrow> logic \<Rightarrow> logic" ("_:[_]\<^sub>D\<^sup>+" [99,0] 100)
 
 translations
   "_des_frame x P" => "CONST des_frame x P"
   "_des_frame (_salphaset (_salphamk x)) P" <= "CONST des_frame x P"
-  "_des_frame_ext x P" => "CONST des_frame_ext x P"
-  "_des_frame_ext (_salphaset (_salphamk x)) P" <= "CONST des_frame_ext x P"
+  "_des_frame_ext x P" == "CONST des_frame_ext x P"
 
 lemma lmapD_rel_aext_ndes [ndes_simp]:
-  "(p \<turnstile>\<^sub>n Q) \<oplus>\<^sub>r lmap\<^sub>D[a] = (p \<oplus>\<^sub>p a \<turnstile>\<^sub>n Q \<oplus>\<^sub>r a)"
+  "(p \<turnstile>\<^sub>n Q) \<up>\<^sub>2 lmap\<^sub>D[a] = (p \<up> a) \<turnstile>\<^sub>n (Q \<up>\<^sub>2 a)"
   by (pred_auto)
-*)
 
 subsection \<open> Alternation \<close>