Theory Designs

section‹Designs›

theory Designs
imports Relations
begin

text ‹In UTP, in order to explicitly record the termination of a program, 
a subset of alphabetized relations is introduced. These relations are called 
designs and their alphabet should contain the special boolean observational variable ok. 
It is used to record the start and termination of a program.›

subsection‹Definitions›

text ‹In the following, the definitions of designs alphabets, designs and 
healthiness (well-formedness) conditions are given. The healthiness conditions of
designs are defined by $H1$, $H2$, $H3$ and $H4$.›

record alpha_d = ok::bool

type_synonym 'α alphabet_d  = "'α alpha_d_scheme alphabet"
type_synonym 'α relation_d = "'α alphabet_d relation"

definition design::"'α relation_d ⇒ 'α relation_d ⇒ 'α relation_d" (‹'(_ ⊢ _')›)
where " (P ⊢ Q) ≡ λ (A, A') .  (ok A ∧ P (A,A')) ⟶ (ok A' ∧ Q (A,A'))"

definition skip_d :: "'α relation_d" (‹Πd›)
where "Πd ≡ (true ⊢ Πr)"

definition J
where "J  ≡  λ (A, A') . (ok A  ⟶  ok A') ∧ more A = more A'"

type_synonym 'α Healthiness_condition = "'α relation ⇒ 'α relation"

definition 
Healthy::"'α relation ⇒ 'α Healthiness_condition ⇒ bool" (‹_ is _ healthy›)
where "P is H healthy ≡ (P = H P)"

lemma Healthy_def': "P is H healthy = (H P = P)"
  unfolding Healthy_def by auto

definition H1::"('α alphabet_d) Healthiness_condition"
where "H1 (P)  ≡  (ok o fst  ⟶ P)"

definition H2::"('α alphabet_d) Healthiness_condition"
where "H2 (P)  ≡  P ;; J"

definition H3::"('α alphabet_d) Healthiness_condition"
where "H3 (P)  ≡  P ;; Πd"

definition H4::"('α alphabet_d) Healthiness_condition"
where "H4 (P)  ≡  ((P;;true) ⟷ true)"

definition σf::"'α relation_d ⇒ 'α relation_d"
where "σf D ≡ λ (A, A') . D (A, A'⦇ok:=False⦈)"

definition σt::"'α relation_d ⇒ 'α relation_d"
where "σt D ≡ λ (A, A') . D (A, A'⦇ok:=True⦈)"

definition OKAY::"'α relation_d"
where "OKAY ≡ λ (A, A') . ok A"

definition OKAY'::"'α relation_d"
where "OKAY' ≡ λ (A, A') . ok A'"

lemmas design_defs = design_def skip_d_def J_def Healthy_def H1_def H2_def H3_def
                     H4_def σf_def σt_def OKAY_def OKAY'_def

subsection‹Proofs›

text ‹Proof of theorems and properties of designs and their healthiness conditions 
are given in the following.›

lemma t_comp_lz_d: "(true;;(P ⊢ Q)) = true"
  apply (auto simp: fun_eq_iff design_defs)
  apply (rule_tac b="b⦇ok:=False⦈" in comp_intro, auto)
done

lemma pi_comp_left_unit: "(Πd;;(P ⊢ Q)) = (P ⊢ Q)"
by (auto simp: fun_eq_iff design_defs)

theorem t3_1_4_2: 
"((P1 ⊢ Q1) ◃ b ▹ (P2 ⊢ Q2)) = ((P1 ◃ b ▹ P2) ⊢ (Q1 ◃ b ▹ Q2))"
by (auto simp: fun_eq_iff design_defs split: cond_splits)

lemma conv_conj_distr: "σt (P ∧ Q) = (σt P ∧ σt Q)"
by (auto simp: design_defs fun_eq_iff)

lemma conv_disj_distr: "σt (P ∨ Q) = (σt P ∨ σt Q)"
by (auto simp: design_defs fun_eq_iff)

lemma conv_imp_distr: "σt (P ⟶ Q) = ((σt P) ⟶ σt Q)"
by (auto simp: design_defs fun_eq_iff)

lemma conv_not_distr: "σt (¬ P) = (¬(σt P))"
by (auto simp: design_defs fun_eq_iff)

lemma div_conj_distr: "σf (P ∧ Q) = (σf P ∧ σf Q)"
by (auto simp: design_defs fun_eq_iff)

lemma div_disj_distr: "σf (P ∨ Q) = (σf P ∨ σf Q)"
by (auto simp: design_defs fun_eq_iff)

lemma div_imp_distr: "σf (P ⟶ Q) = ((σf P) ⟶ σf Q)"
by (auto simp: design_defs fun_eq_iff)

lemma div_not_distr: "σf (¬ P) = (¬(σf P))"
by (auto simp: design_defs fun_eq_iff)

lemma ok_conv: "σt OKAY = OKAY"
by (auto simp: design_defs fun_eq_iff)

lemma ok_div: "σf OKAY = OKAY"
by (auto simp: design_defs fun_eq_iff)

lemma ok'_conv: "σt OKAY' = true"
by (auto simp: design_defs fun_eq_iff)

lemma ok'_div: "σf OKAY' = false"
by (auto simp: design_defs fun_eq_iff)

lemma H2_J_1:
 assumes A: "P is H2 healthy"
 shows "[(λ (A, A'). (P(A, A'⦇ok := False⦈) ⟶ P(A, A'⦇ok := True⦈)))]"
using A by (auto simp: design_defs fun_eq_iff)

lemma H2_J_2_a : "P (a,b) ⟶ (P ;; J) (a,b)"
  unfolding J_def by auto

lemma ok_or_not_ok : "⟦P(a, b⦇ok := True⦈); P(a, b⦇ok := False⦈)⟧ ⟹ P(a, b)"
  apply (case_tac "ok b")
  apply (subgoal_tac "b⦇ok:=True⦈ = b")
  apply (simp_all)
  apply (subgoal_tac "b⦇ok:=False⦈ = b")
  apply (simp_all)
done

lemma H2_J_2_b :
  assumes A: "[(λ (A, A'). (P(A, A'⦇ok := False⦈) ⟶ P(A, A'⦇ok := True⦈)))]"
  and B : "(P ;; J) (a,b)"
  shows "P (a,b)"
  using B
  apply (auto simp: design_defs fun_eq_iff)
  apply (case_tac "ok b")
  apply (subgoal_tac "b = ba⦇ok:=True⦈", auto intro!: A[simplified, rule_format])
  apply (rule_tac s=ba and t="ba⦇ok:=False⦈" in subst, simp_all)
  apply (subgoal_tac "b = ba", simp_all)
  apply (case_tac "ok ba")
  apply (subgoal_tac "b = ba", simp_all)
  apply (subgoal_tac "b = ba⦇ok:=True⦈", auto intro!: A[simplified, rule_format])
  apply (rule_tac s=ba and t="ba⦇ok:=False⦈" in subst, simp_all)
done  

lemma H2_J_2 :
  assumes A: "[(λ (A, A'). (P(A, A'⦇ok := False⦈) ⟶ P(A, A'⦇ok := True⦈)))]"
  shows "P is H2 healthy "
  apply (auto simp add: H2_def Healthy_def fun_eq_iff)
  apply (simp add: H2_J_2_a)
  apply (rule H2_J_2_b [OF A])
  apply auto
  done

lemma H2_J: 
"[λ (A, A'). P(A, A'⦇ok := False⦈) ⟶ P(A, A'⦇ok := True⦈)] = P is H2 healthy"
using H2_J_1 H2_J_2 by blast

lemma design_eq1: "(P ⊢ Q) = (P ⊢ P ∧ Q)"
by (rule ext) (auto simp: design_defs)

lemma H1_idem: "H1 o H1 = H1"
by (auto simp: design_defs fun_eq_iff)

lemma H1_idem2: "(H1 (H1 P)) = (H1 P)"
by (simp add: H1_idem[simplified fun_eq_iff Fun.comp_def, rule_format] fun_eq_iff)

lemma H2_idem: "H2 o H2 = H2"  
by (auto simp: design_defs fun_eq_iff)
  
lemma H2_idem2: "(H2 (H2 P)) = (H2 P)"
by (simp add: H2_idem[simplified fun_eq_iff Fun.comp_def, rule_format] fun_eq_iff)

lemma H1_H2_commute: "H1 o H2 = H2 o H1"
by (auto simp: design_defs fun_eq_iff split: cond_splits)

lemma H1_H2_commute2: "H1 (H2 P) = H2 (H1 P)"
by (simp add: H1_H2_commute[simplified fun_eq_iff Fun.comp_def, rule_format] fun_eq_iff)

lemma alpha_d_eqD: "r = r' ⟹ ok r = ok r' ∧ alpha_d.more r = alpha_d.more r'"
by (auto simp: alpha_d.equality)

lemma design_H1: "(P ⊢ Q) is H1 healthy"
by (auto simp: design_defs fun_eq_iff)

lemma design_H2: 
"(∀ a b. P (a, b⦇ok := True⦈) ⟶ P (a, b⦇ok := False⦈)) ⟹ (P ⊢ Q) is H2 healthy"
by (rule H2_J_2) (auto simp: design_defs fun_eq_iff)

end