Completed a substantial portion of the port of UTP Designs. The imper…

…ative program notation is still outstanding.

utp_des_core.thy

@@ -1,3 +1,5 @@
+section \<open> Design Signature and Core Laws \<close>
+
 theory utp_des_core
   imports UTP2.utp_wlp UTP2.utp_theory
 begin 
@@ -8,7 +10,6 @@ alphabet des_vars =
 type_synonym ('s\<^sub>1, 's\<^sub>2) des_rel = "('s\<^sub>1 des_vars_scheme, 's\<^sub>2 des_vars_scheme) urel"
 type_synonym ('s\<^sub>1) des_hrel = "('s\<^sub>1, 's\<^sub>1) des_rel"
 
-
 notation des_vars.more\<^sub>L ("\<^bold>v\<^sub>D")
 
 syntax
@@ -114,4 +115,8 @@ translations
   "P\<^sup>f" \<rightharpoonup> "_subst P (CONST False) (_svid_post (CONST ok))"
   "P\<^sup>t" \<rightharpoonup> "_subst P (CONST True) (_svid_post (CONST ok))"
 
+lemma state_subst_design [usubst]:
+  "(\<sigma> \<up>\<^sub>s \<^bold>v\<^sub>D\<^sup><) \<dagger> (P \<turnstile>\<^sub>r Q) = ((\<sigma> \<up>\<^sub>s \<^bold>v\<^sup><) \<dagger> P) \<turnstile>\<^sub>r ((\<sigma> \<up>\<^sub>s \<^bold>v\<^sup><) \<dagger> Q)"
+  by (pred_auto)
+
 end

utp_des_healths.thy

@@ -180,11 +180,6 @@ proof -
     by (metis H1_USUP image_image)
 qed
 
-(*
-lemma msubst_H1: "(\<And>x. P x is H1) \<Longrightarrow> P x\<lbrakk>x\<rightarrow>v\<rbrakk> is H1"
-  by (rel_auto)
-*)
-
 subsection \<open> H2: A specification cannot require non-termination \<close>
 
 definition J :: "'\<alpha> des_hrel" where 
@@ -238,25 +233,6 @@ theorem H2_equivalence:
   "P is H2 \<longleftrightarrow> `(P\<^sup>f \<longrightarrow> P\<^sup>t)`"
   by (pred_auto, (metis (full_types))+)
 
-(*
-proof -
-  have "(P = (P ;; J)) \<longleftrightarrow> (P = (P\<^sup>f \<or> (P\<^sup>t \<and> ok\<^sup>>)))"
-    by (simp add: J_split)
-  also have "... \<longleftrightarrow> `\<lbrakk>(P \<longleftrightarrow> P\<^sup>f \<or> P\<^sup>t \<and> (ok\<^sup>>)\<^sub>e)\<^sup>f \<and> (P \<longleftrightarrow> P\<^sup>f \<or> P\<^sup>t \<and> (ok\<^sup>>)\<^sub>e)\<rbrakk>\<^sub>P`"
-    by rel_auto
-  also have "... = `\<lbrakk>(P\<^sup>f \<longleftrightarrow> P\<^sup>f) \<and> (P\<^sup>t \<longleftrightarrow> P\<^sup>f \<or> P\<^sup>t)\<rbrakk>\<^sub>P`"
-    apply pred_auto
-    by metis+
-  also have "... = `\<lbrakk>P\<^sup>t \<longleftrightarrow> (P\<^sup>f \<or> P\<^sup>t)\<rbrakk>\<^sub>P`"
-    by (pred_auto)
-  also have "... = `P\<^sup>f \<longrightarrow> P\<^sup>t`"
-    by (pred_auto)
-  finally show ?thesis
-    using H2_def Healthy_def'
-    by (metis (no_types, lifting) SEXP_def conj_refine_left iff_pred_def pred_ba.boolean_algebra.conj_one_right pred_ba.inf_le2 pred_ba.sup.absorb2 pred_ba.sup.orderE pred_impl_laws(5) pred_set rel_eq_iff taut_def true_false_pred_expr(1))
-qed
-*)
-
 lemma H2_equiv:
   "P is H2 \<longleftrightarrow> P\<^sup>t \<sqsubseteq> P\<^sup>f"
   by (simp add: H2_equivalence pred_refine_iff, expr_simp)
@@ -279,10 +255,8 @@ theorem H2_idem:
   "H2(H2(P)) = H2(P)"
   by (metis H2_def J_idem seqr_assoc)
 
-(*
 theorem H2_Continuous: "Continuous H2"
-  by (rel_auto)
-*)
+  by pred_auto
 
 theorem H2_not_okay: "H2 (\<not>ok\<^sup><) = (\<not>ok\<^sup><)"
 proof -
@@ -338,7 +312,6 @@ qed
 
 subsection \<open> Designs as $H1$-$H2$ predicates \<close>
 
-
 abbreviation H1_H2 :: "('\<alpha>, '\<beta>) des_rel \<Rightarrow> ('\<alpha>, '\<beta>) des_rel" ("\<^bold>H") where
 "H1_H2 P \<equiv> H1 (H2 P)"
 
@@ -364,15 +337,6 @@ theorem H1_H2_is_design:
   shows "P = (\<not> P\<^sup>f) \<turnstile> P\<^sup>t"
   using assms by (metis H1_H2_eq_design Healthy_def)
 
-(*
-lemma aext_arestr' [alpha]:
-  fixes P :: "'a \<leftrightarrow> 'b"
-  assumes "$a \<sharp> P"
-  shows "(P \<down> a) \<up> a = P"
-  apply rel_auto  
-  by (rel_simp, metis assms lens_override_def)
-*)
-
 theorem H1_H2_eq_rdesign:
   "\<^bold>H(P) = pre\<^sub>D(P) \<turnstile>\<^sub>r post\<^sub>D(P)"
 proof -
@@ -406,7 +370,8 @@ lemma H1_H2_refinement:
   shows "P \<sqsubseteq> Q \<longleftrightarrow> (`pre\<^sub>D(P) \<longrightarrow> pre\<^sub>D(Q)` \<and> `pre\<^sub>D(P) \<and> post\<^sub>D(Q) \<longrightarrow> post\<^sub>D(P)`)"
   using assms
   apply (simp only:rdesign_refinement[symmetric])
-  by (metis H1_H2_eq_rdesign Healthy_if)
+  apply (metis H1_H2_eq_rdesign Healthy_if)
+  done
 
 lemma H1_H2_refines:
   assumes "P is \<^bold>H" "Q is \<^bold>H" "P \<sqsubseteq> Q"
@@ -421,13 +386,11 @@ lemma H1_H2_idempotent: "\<^bold>H (\<^bold>H P) = \<^bold>H P"
 lemma H1_H2_Idempotent [closure]: "Idempotent \<^bold>H"
   by (simp add: Idempotent_def H1_H2_idempotent)
 
-(*
-lemma H1_H2_monotonic [closure]: "Monotone \<^bold>H"
-  by (simp add: H1_monotone H2_def mono_def seqr_mono)
+lemma H1_H2_monotonic [closure]: "Monotonic \<^bold>H"
+  by (simp add: Continuous_Monotonic H1_Continuous H1_H2_comp H2_Continuous Monotonic_comp)
 
 lemma H1_H2_Continuous [closure]: "Continuous \<^bold>H"
   by (simp add: Continuous_comp H1_Continuous H1_H2_comp H2_Continuous)
-*)
 
 lemma H1_H2_false: "\<^bold>H false = \<top>\<^sub>D"
   by (pred_auto)
@@ -465,8 +428,6 @@ qed
 lemma H1_H2_left_unit: "P is \<^bold>H \<Longrightarrow> II\<^sub>D ;; P = P"
   by (metis H1_H2_eq_rdesign Healthy_def' rdesign_left_unit)
 
-thm design_is_H1_H2
-
 lemma UINF_H1_H2_closed [closure]:
   assumes "A \<noteq> {}" "\<forall> P \<in> A. P is \<^bold>H"
   shows "(\<Sqinter> A) is H1_H2"
@@ -689,11 +650,6 @@ theorem H3_ndesign: "H3(p \<turnstile>\<^sub>n Q) = (p \<turnstile>\<^sub>n Q)"
 theorem ndesign_is_H3 [closure]: "p \<turnstile>\<^sub>n Q is H3"
   by (simp add: H3_ndesign Healthy_def)
 
-(*
-lemma msubst_pre_H3: "(\<And>x. P x is H3) \<Longrightarrow> P x\<lbrakk>x\<rightarrow>\<lceil>v\<rceil>\<^sub><\<rbrakk> is H3"
-  by (rel_auto)
-*)
-
 subsection \<open> Normal Designs as $H1$-$H3$ predicates \<close>
 
 text \<open> A normal design~\cite{Guttman2010} refers only to initial state variables in the precondition. \<close>
@@ -731,10 +687,6 @@ lemma H1_H3_monotonic [closure]: "Monotonic \<^bold>N"
 lemma H1_H3_Continuous [closure]: "Continuous \<^bold>N"
   by (simp add: Continuous_comp H1_Continuous H1_H3_comp H3_Continuous)
 
-interpretation normal_design_thy: utp_theory_continuous "\<^bold>N"
-  rewrites "le (utp_order \<^bold>N) = (\<sqsubseteq>)" and "carrier normal_design_thy.thy_order = \<lbrakk>\<^bold>N\<rbrakk>\<^sub>H"
-  by (unfold_locales, simp_all add: closure)
-
 lemma H1_H3_false: "\<^bold>N false = \<top>\<^sub>D"
   by (pred_auto)
 
@@ -860,11 +812,6 @@ lemma USUP_mem_H1_H3_closed [closure]:
   "\<lbrakk> \<And> i. i \<in> I \<Longrightarrow> P i is \<^bold>N \<rbrakk> \<Longrightarrow> (\<Squnion> i\<in>I. P i) is \<^bold>N"
   by (rule H1_H3_intro; simp add: H1_H3_impl_H2 USUP_mem_H1_H2_closed H3_unrest_out_alpha preD_USUP_mem unrest_INF_SUP(2))
 
-(*
-lemma msubst_pre_H1_H3 [closure]: "(\<And>x. P x is \<^bold>N) \<Longrightarrow> P x\<lbrakk>x\<rightarrow>\<lceil>v\<rceil>\<^sub><\<rbrakk> is \<^bold>N"
-  by (metis H1_H3_right_unit H3_def Healthy_if Healthy_intro msubst_H1 msubst_pre_H3)
-*)
-
 subsection \<open> H4: Feasibility \<close>
 
 definition H4 :: "('\<alpha>, '\<beta>) des_rel \<Rightarrow> ('\<alpha>, '\<beta>) des_rel" where

utp_des_hoare.thy

@@ -0,0 +1,37 @@
+subsection \<open> Design Hoare Logic \<close>
+
+theory utp_des_hoare
+  imports utp_des_prog
+begin
+
+definition HoareD :: "'s pred \<Rightarrow> 's des_hrel \<Rightarrow> 's pred \<Rightarrow> bool" ("{_}_{_}\<^sub>D") where
+[pred, ndes_simp]: "HoareD p S q = ((p \<turnstile>\<^sub>n q\<^sup>>) \<sqsubseteq> S)"
+
+lemma assigns_hoare_d [hoare_safe]: "`p \<longrightarrow> \<sigma> \<dagger> q` \<Longrightarrow> {p}\<langle>\<sigma>\<rangle>\<^sub>D{q}\<^sub>D"
+  by pred_auto
+
+lemma skip_hoare_d: "{p}II\<^sub>D{p}\<^sub>D"
+  by (pred_auto)
+
+lemma assigns_backward_hoare_d: 
+  "{\<sigma> \<dagger> p}\<langle>\<sigma>\<rangle>\<^sub>D{p}\<^sub>D"
+  by pred_auto
+
+lemma seq_hoare_d: 
+  assumes "C is \<^bold>N" "D is \<^bold>N" "{p}C{q}\<^sub>D" "{q}D{r}\<^sub>D"
+  shows "{p}C ;; D{r}\<^sub>D"
+proof -
+  obtain c\<^sub>1 C\<^sub>2 where C: "C = c\<^sub>1 \<turnstile>\<^sub>n C\<^sub>2"
+    by (metis assms(1) ndesign_form)
+  obtain d\<^sub>1 D\<^sub>2 where D: "D = d\<^sub>1 \<turnstile>\<^sub>n D\<^sub>2"
+    by (metis assms(2) ndesign_form)
+  from assms(3-4) show ?thesis
+    apply (simp add: C D)
+    apply (ndes_simp)
+    apply (simp add: ndesign_refinement)
+    apply (pred_auto)
+    apply blast
+    done
+qed
+
+end

utp_des_laws.thy

@@ -30,24 +30,12 @@ lemma lift_des_skip_dr_unit [simp]:
 lemma lift_des_skip_dr_unit_unrest: "$ok\<^sup>> \<sharp> P \<Longrightarrow> (P ;; II \<up> more\<^sub>L\<^sup>2) = P"
   by (pred_auto)
 
-(*
-lemma state_subst_design [usubst]:
-  "\<lceil>\<sigma> \<oplus>\<^sub>s \<Sigma>\<^sub>D\<rceil>\<^sub>s \<dagger> (P \<turnstile>\<^sub>r Q) = (\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> P) \<turnstile>\<^sub>r (\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> Q)"
-  by (rel_auto)
-*)
-
 lemma get_unrest_subst [usubst_eval]: "\<lbrakk> vwb_lens x; $x \<sharp>\<^sub>s \<sigma> \<rbrakk> \<Longrightarrow> get\<^bsub>x\<^esub> (\<sigma> s) = get\<^bsub>x\<^esub> s"
   by (expr_simp, metis vwb_lens_wb wb_lens.get_put wb_lens_weak weak_lens.view_determination)
 
 lemma design_subst [usubst]:
   "\<lbrakk> $ok\<^sup>< \<sharp>\<^sub>s \<sigma>; $ok\<^sup>> \<sharp>\<^sub>s \<sigma> \<rbrakk> \<Longrightarrow> \<sigma> \<dagger> (P \<turnstile> Q) = (\<sigma> \<dagger> P) \<turnstile> (\<sigma> \<dagger> Q)"
   by (simp add: pred, subst_eval, simp add: subst_app_def)
-
-(*
-lemma design_msubst [usubst]:
-  "(P(x) \<turnstile> Q(x))\<lbrakk>x\<rightarrow>v\<rbrakk> = (P(x)\<lbrakk>x\<rightarrow>v\<rbrakk> \<turnstile> Q(x)\<lbrakk>x\<rightarrow>v\<rbrakk>)"
-  by (rel_auto)
-*)
 
 lemma design_ok_false [usubst]: "(P \<turnstile> Q)\<lbrakk>False/ok\<^sup><\<rbrakk> = true"
   by pred_auto
@@ -138,15 +126,15 @@ theorem rdesign_composition_cond:
   shows "((p1 \<turnstile>\<^sub>r Q1) ;; (P2 \<turnstile>\<^sub>r Q2)) = ((p1 \<and> \<not> (Q1 ;; (\<not> P2))) \<turnstile>\<^sub>r (Q1 ;; Q2))"
   using assms by pred_auto
 
-theorem design_composition_wp:
+theorem design_composition_wlp:
   fixes p1 p2 :: "'a des_vars_scheme \<Rightarrow> bool"
   assumes
     "$ok \<sharp> p1" "$ok \<sharp> p2"
     "$ok\<^sup>< \<sharp> Q1" "$ok\<^sup>> \<sharp> Q1" "$ok\<^sup>< \<sharp> Q2" "$ok\<^sup>> \<sharp> Q2"
   shows "((p1\<^sup>< \<turnstile> Q1) ;; (p2\<^sup>< \<turnstile> Q2)) = ((p1 \<and> Q1 wlp p2)\<^sup>< \<turnstile> (Q1 ;; Q2))"
   unfolding design_def by (pred_auto assms: assms, metis+)
 
-theorem rdesign_composition_wp:
+theorem rdesign_composition_wlp:
   "((p1\<^sup>< \<turnstile>\<^sub>r Q1) ;; (p2\<^sup>< \<turnstile>\<^sub>r Q2)) = ((p1 \<and> Q1 wlp p2)\<^sup>< \<turnstile>\<^sub>r (Q1 ;; Q2))"
   by (pred_auto)
 
@@ -249,7 +237,6 @@ next
   qed
 qed
 
-
 subsection \<open> Preconditions and Postconditions \<close>
 
 theorem design_npre:
@@ -375,7 +362,7 @@ theorem design_refinement:
   assumes
     "$ok\<^sup>< \<sharp> P1" "$ok\<^sup>> \<sharp> P1" "$ok\<^sup>< \<sharp> P2" "$ok\<^sup>> \<sharp> P2"
     "$ok\<^sup>< \<sharp> Q1" "$ok\<^sup>> \<sharp> Q1" "$ok\<^sup>< \<sharp> Q2" "$ok\<^sup>> \<sharp> Q2"
-  shows "((P1 \<turnstile> Q1) \<sqsubseteq> (P2 \<turnstile> Q2)) \<longleftrightarrow> `(P1 \<longrightarrow> P2) \<and> (P1 \<and> Q2 \<longrightarrow> Q1)`"
+  shows "(P1 \<turnstile> Q1 \<sqsubseteq> P2 \<turnstile> Q2) \<longleftrightarrow> `(P1 \<longrightarrow> P2) \<and> (P1 \<and> Q2 \<longrightarrow> Q1)`"
   by (pred_auto assms: assms; metis)
 
 theorem rdesign_refinement:
@@ -402,12 +389,10 @@ lemma rdesign_refine_intro':
   shows "P1 \<turnstile>\<^sub>r Q1 \<sqsubseteq> P2 \<turnstile>\<^sub>r Q2"
   using assms by (pred_auto)
 
-
 lemma ndesign_refinement: 
   "p1 \<turnstile>\<^sub>n Q1 \<sqsubseteq> p2 \<turnstile>\<^sub>n Q2 \<longleftrightarrow> (`p1 \<longrightarrow> p2` \<and> `p1\<^sup>< \<and> Q2 \<longrightarrow> Q1`)"
   by pred_auto
 
-
 lemma ndesign_refinement': 
   "p1 \<turnstile>\<^sub>n Q1 \<sqsubseteq> p2 \<turnstile>\<^sub>n Q2 \<longleftrightarrow> (`p1 \<longrightarrow> p2` \<and> Q1 \<sqsubseteq> \<questiondown>p1? ;; Q2)"
   by (simp add: ndesign_refinement, pred_auto)