Quelle  Designs.thy

section‹Designs›

theory Designs
imports Relations
begin

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

subsection‹Definitions›

text ‹In the following, the definitions of designs alphabets, designs and
  (well-formedness) conditions are given. The healthiness conditions of
  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
  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