simplify newlines

This commit is contained in:
Frédéric Tuong 2018-02-08 18:13:11 -05:00
parent c1cbda69d2
commit c93361eca4
10 changed files with 1990 additions and 1990 deletions

View File

@ -1,7 +1,7 @@
The folder src contains the *.thy theories for the formalization of C semantics.
The set of *.thy files provides a formal framework for implementing imperative programs ins general and C programs in particular.
The framework follows the terminology and the methodology of the informal language IMP, presented in the textbook of Glynn Winskel.
The folder src contains the *.thy theories for the formalization of C semantics.
The set of *.thy files provides a formal framework for implementing imperative programs ins general and C programs in particular.
The framework follows the terminology and the methodology of the informal language IMP, presented in the textbook of Glynn Winskel.

View File

@ -1,12 +1,12 @@
session "orca-model" = "HOL" +
description {*Shallow embedded orca*}
options [quick_and_dirty, document = pdf, document_output = "."]
theories
"features_test"
"theories/utp_fault_designs"
files "document/root.tex"
session "orca-model" = "HOL" +
description {*Shallow embedded orca*}
options [quick_and_dirty, document = pdf, document_output = "."]
theories
"features_test"
"theories/utp_fault_designs"
files "document/root.tex"

View File

@ -1,458 +1,458 @@
section "Auxiliary algebraic laws for abrupt designs"
theory algebraic_laws_abrupt_aux
imports "../../../theories/Abrupt/utp_abrupt_designs"
begin
named_theorems uabr_simpl and uabr_cond and uabr_comp and uabr_lens
subsection {*THM setup*}
declare design_condr[urel_cond]
subsection {*abrupt alphabet behavior*}
lemma assigns_abr_alpha:
"(abrupt :== (\<not> &abrupt)) = (\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R \<and> $abrupt\<acute> =\<^sub>u (\<not>$abrupt) \<and> $ok =\<^sub>u $ok\<acute>)"
"(ok :== (\<not> &ok)) = (\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R \<and> $abrupt\<acute> =\<^sub>u $abrupt \<and> $ok =\<^sub>u (\<not>$ok\<acute>))"
by rel_auto+
lemma vwb_of_abrupt[simp]:
"vwb_lens ok" "vwb_lens abrupt"
by simp_all
lemma unrest_pre_out\<alpha>_abr[unrest]: "out\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub><"
by (transfer, auto simp add: out\<alpha>_def lens_prod_def)
lemma unrest_post_in\<alpha>_abr[unrest]: "in\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub>>"
by (transfer, auto simp add: in\<alpha>_def lens_prod_def)
lemma unrest_ok_abrupt_rel_uexpr_lift_cpa[unrest]:
"$ok \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R" "$ok\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
"$abrupt \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R" "$abrupt\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by (pred_auto)+
lemma unrest_ok_abrupt_rel_usubst_lift_cpa[unrest]:
"$ok\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R" "$ok \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R"
"$abrupt\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R" "$abrupt \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R"
by rel_auto+
lemma unrest_in_out_rel_ok_abrupt_res_abr [unrest]:
"$ok \<sharp> (P \<restriction>\<^sub>\<alpha> ok)" "$ok\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> ok)"
"$abrupt \<sharp> (P \<restriction>\<^sub>\<alpha> abrupt)" "$abrupt\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> abrupt)"
by (simp_all add: rel_var_res_def unrest)
lemma uabr_alphabet_unrest[unrest]:(*FIXEME:These laws should be generated automatically by alphabet backend since all the fields of alphabet are independant*)
"$ok\<acute> \<sharp> $abrupt\<acute>" "$ok \<sharp> $abrupt"
"$ok\<acute> \<sharp> $abrupt" "$ok \<sharp> $abrupt\<acute>"
"$abrupt\<acute> \<sharp> $ok\<acute>" "$abrupt \<sharp> $ok "
"$abrupt \<sharp> $ok\<acute>" "$abrupt\<acute> \<sharp> $ok"
by pred_simp+
lemma cpa_ord [usubst]:
"$ok \<prec>\<^sub>v $ok\<acute>" "$abrupt \<prec>\<^sub>v $abrupt\<acute>" "$ok \<prec>\<^sub>v $abrupt\<acute>"
"$ok \<prec>\<^sub>v $abrupt" "$ok\<acute> \<prec>\<^sub>v $abrupt\<acute>" "$ok\<acute> \<prec>\<^sub>v $abrupt"
by (simp_all add: var_name_ord_def)
lemma rel_usubst_lift_cpa_in_out_abrupt_ok[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> $abrupt = $abrupt" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$abrupt) = (\<not>$abrupt)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> ($ok) = ($ok)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$ok) = (\<not>$ok)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> ($abrupt\<acute>) = (($abrupt\<acute>))" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$abrupt\<acute>) = (\<not>$abrupt\<acute>)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> ($ok\<acute>) = ($ok\<acute>)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$ok\<acute>) = (\<not>$ok\<acute>)"
by (simp_all add: usubst unrest)
lemma abrupt_ok_simpl[uabr_comp]:
"($abrupt ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = $abrupt" "(\<not>$ok ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$ok)"
"($abrupt ;; (P \<turnstile> Q)) = $abrupt" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"(\<not>$abrupt ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$abrupt)" "(\<not>$ok ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$ok)"
"(\<not>$abrupt ;; (P \<turnstile> Q)) = (\<not>$abrupt)" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"($abrupt\<acute> ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = $abrupt\<acute>"
"(\<not>$abrupt\<acute> ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$abrupt\<acute>)"
by rel_auto+
lemma simpl_abr_in_ok:
"Simpl\<^sub>A\<^sub>B\<^sub>R ($ok) = ((\<not>$abrupt \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_abr_our_ok:
"Simpl\<^sub>A\<^sub>B\<^sub>R ($ok\<acute>) =
((\<not>$abrupt \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_abr_in_abrupt:
"Simpl\<^sub>A\<^sub>B\<^sub>R ($abrupt) =
((\<not>$abrupt \<and> ($ok \<Rightarrow>($ok\<acute> \<and> $abrupt))) \<or> ($abrupt \<and> II))"
by rel_auto
lemma simpl_abr_alr_def:
"Simpl\<^sub>A\<^sub>B\<^sub>R (P) =
((\<not>$abrupt \<and> ($ok \<Rightarrow>($ok\<acute> \<and> P))) \<or> ($abrupt \<and> II))"
by rel_auto
subsection {*Healthiness condition behavior*}
lemma rel_usubst_cpa_c3_abr[usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows "\<sigma> \<dagger> C3_abr(P) = (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> (\<not>$abrupt) \<triangleright> (\<sigma> \<dagger> II))"
using assms unfolding C3_abr_def
by (simp add: usubst)
lemma Simpl_abr_idem[simp]: "Simpl\<^sub>A\<^sub>B\<^sub>R(Simpl\<^sub>A\<^sub>B\<^sub>R(P)) = Simpl\<^sub>A\<^sub>B\<^sub>R(P)"
by (rel_auto)
lemma simpl_abr_Idempotent: "Idempotent Simpl\<^sub>A\<^sub>B\<^sub>R"
by (simp add: Idempotent_def)
lemma Simpl_abr_mono: "P \<sqsubseteq> Q \<Longrightarrow> Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<sqsubseteq> Simpl\<^sub>A\<^sub>B\<^sub>R(Q)"
by (rel_auto)
lemma simpl_abr_Monotonic: "Monotonic Simpl\<^sub>A\<^sub>B\<^sub>R"
by (simp add: Monotonic_def Simpl_abr_mono)
lemma simpl_abr_def:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P) = ((\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> P) \<triangleleft> \<not>$abrupt \<triangleright> II)"
unfolding C3_abr_def ..
lemma simpl_abr_condr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P \<triangleleft> b \<triangleright> Q) = (Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<triangleleft> b \<triangleright> Simpl\<^sub>A\<^sub>B\<^sub>R(Q))"
unfolding simpl_abr_def
by (simp add: urel_cond)
lemma simpl_abr_skip_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R(SKIP\<^sub>A\<^sub>B\<^sub>R) = (SKIP\<^sub>A\<^sub>B\<^sub>R)"
by (simp add: urel_cond urel_defs)
lemma simpl_abr_throw_abr:
"Simpl\<^sub>A\<^sub>B\<^sub>R(THROW\<^sub>A\<^sub>B\<^sub>R) = ((\<not>$abrupt) \<and> ($ok \<Rightarrow>($ok\<acute> \<and> $abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) \<or> ($abrupt \<and> II))"
by rel_auto
lemma simpl_abr_assign_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R(\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) = (\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R)"
by (simp add: urel_cond urel_defs)
lemma simpl_abr_throw_abr_comp_abrupt[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; Simpl\<^sub>A\<^sub>B\<^sub>R Q) \<triangleleft> $abrupt \<triangleright> II)) = Simpl\<^sub>A\<^sub>B\<^sub>R Q"
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_throw_abr_comp_abrupt_cond_throw_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; THROW\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = Simpl\<^sub>A\<^sub>B\<^sub>R THROW\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_throw_abr_comp_abrupt_cond_skip_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = SKIP\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_throw_abr_comp_abrupt_cond_assigns_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; Simpl\<^sub>A\<^sub>B\<^sub>R Q) \<triangleleft> $abrupt \<triangleright> II)) =
Simpl\<^sub>A\<^sub>B\<^sub>R Q"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt_cond_skip_abr[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
SKIP\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt_cond_throw_abr[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; THROW\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
C3_abr THROW\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt_cond_assigns_abr[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
(*lemma [uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; THROW\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
(\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> ($abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) "
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma throw_abr_comp_abrupt_cond_skip_abr[uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
(\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<not>$abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) "
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma [uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
(\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<not>$abrupt\<acute> \<and> \<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R)) "
apply pred_simp
apply rel_simp
apply safe
apply auto
done*)
lemma [uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = (true) "
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_form:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P) = (((\<not>$abrupt) \<and> (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (P))) \<or> ($abrupt \<and> II))"
by rel_auto
lemma abrupt_simpl_abr[uabr_simpl]:
"($abrupt \<and> Simpl\<^sub>A\<^sub>B\<^sub>R(P)) = ($abrupt \<and>II)"
by rel_auto
lemma nabrupt_simpl_abr[uabr_simpl]:
"(\<not>$abrupt \<and> Simpl\<^sub>A\<^sub>B\<^sub>R(P)) = (\<not>$abrupt \<and> (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (P)))"
by (rel_auto)
definition design_abr_sup :: "('\<alpha>,'\<beta>) rel_cpa set \<Rightarrow> ('\<alpha>,'\<beta>) rel_cpa" ("\<Sqinter>\<^sub>A\<^sub>B\<^sub>R_" [900] 900) where
"\<Sqinter>\<^sub>A\<^sub>B\<^sub>R A = (if (A = {}) then \<top>\<^sub>A\<^sub>B\<^sub>R else \<Sqinter> A)"
lemma simpl_abr_Continuous: "Continuous Simpl\<^sub>A\<^sub>B\<^sub>R"
unfolding Continuous_def SUP_def apply rel_simp
unfolding SUP_def
apply transfer apply auto
done
lemma simpl_abr_R3_conj:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P \<and> Q) = (Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<and> Simpl\<^sub>A\<^sub>B\<^sub>R(Q))"
by (rel_auto)
lemma simpl_abr_disj:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P \<or> Q) = (Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<or> Simpl\<^sub>A\<^sub>B\<^sub>R(Q))"
by (rel_auto)
lemma Simpl_abr_USUP:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>A\<^sub>B\<^sub>R(\<Sqinter> i \<in> A \<bullet> P(i)) = (\<Sqinter> i \<in> A \<bullet> Simpl\<^sub>A\<^sub>B\<^sub>R(P(i)))"
using assms by (rel_auto)
lemma design_abr_sup_non_empty [simp]:
"A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^sub>A\<^sub>B\<^sub>R A = \<Sqinter> A"
by (simp add: design_abr_sup_def)
subsection {*Signature behavior*}
lemma design_top_abr:
"(P \<turnstile> Q) \<sqsubseteq> \<top>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)
lemma design_abr_sup_empty [simp]:
"\<Sqinter>\<^sub>A\<^sub>B\<^sub>R {} = \<top>\<^sub>A\<^sub>B\<^sub>R"
by (simp add: design_abr_sup_def)
abbreviation design_inf :: "('\<alpha>, '\<beta>) rel_des set \<Rightarrow> ('\<alpha>, '\<beta>) rel_des" ("\<Squnion>\<^sub>A\<^sub>B\<^sub>R_" [900] 900) where
"\<Squnion>\<^sub>A\<^sub>B\<^sub>R A \<equiv> \<Squnion> A"
lemma design_bottom_abr:
"\<bottom>\<^sub>A\<^sub>B\<^sub>R \<sqsubseteq> (P \<turnstile> Q)"
by simp
lemma Simpl_abr_bottom_abr:
"\<bottom>\<^sub>A\<^sub>B\<^sub>R \<sqsubseteq> Simpl\<^sub>A\<^sub>B\<^sub>R (P)"
by simp
lemma Simpl_abr_UINF:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>A\<^sub>B\<^sub>R(\<Squnion> i \<in> A \<bullet> P(i)) = (\<Squnion> i \<in> A \<bullet> Simpl\<^sub>A\<^sub>B\<^sub>R(P(i)))"
using assms by (rel_auto)
lemma skip_cpa_def:
"II = (\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R \<and> $abrupt =\<^sub>u $abrupt\<acute> \<and> $ok =\<^sub>u $ok\<acute>)"
by rel_auto
lemma skip_lift_cpa_def:
"\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R = ($\<Sigma>\<^sub>A\<^sub>B\<^sub>R\<acute> =\<^sub>u $\<Sigma>\<^sub>A\<^sub>B\<^sub>R)"
by rel_auto
lemma seqr_abrupt_true [usubst]: "(P ;; Q) \<^sub>a\<^sub>t = (P \<^sub>a\<^sub>t ;; Q)"
by (rel_auto)
lemma seqr_abrupt_false [usubst]: "(P ;; Q) \<^sub>a\<^sub>f = (P \<^sub>a\<^sub>f ;; Q)"
by (rel_auto)
lemma rel_usubst_lift_cpa_uexpr_lift_cpa[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>\<sigma> \<dagger> P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma usubst_lift_cpa_assigns_lift_cpa [usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>\<langle>\<rho> \<circ> \<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by (simp add: usubst)
lemma usubst_lift_cpa_pre_uexpr_lift_cpa[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub>< = \<lceil>\<sigma> \<dagger> b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub><"
by (simp add: usubst)
lemma rel_usubst_lift_cpa_design[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (Q \<turnstile> P)) = (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> Q) \<turnstile> (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> P)"
by (simp add: usubst unrest)
lemma usubst_cpa_true[usubst]: "\<sigma> \<dagger> \<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma usubst_cpa_false[usubst]: "\<sigma> \<dagger> \<lceil>false\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>false\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma rel_usubst_cpa_skip_cpa[usubst]:
"(\<sigma> \<dagger> II) = ((\<sigma> \<dagger> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R) \<and> \<sigma> \<dagger> $abrupt =\<^sub>u \<sigma> \<dagger> $abrupt\<acute> \<and> \<sigma> \<dagger> $ok =\<^sub>u \<sigma> \<dagger> $ok\<acute>)"
by (simp add: usubst unrest skip_cpa_def)
lemma usubst_lift_cpa_skip_lift_cpa[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R) = \<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R"
unfolding skip_r_def
by (simp add: usubst_lift_cpa_assigns_lift_cpa)
lemma usubst_cpa_skip_cpa [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"(\<sigma> \<dagger> SKIP\<^sub>A\<^sub>B\<^sub>R) = (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<sigma> \<dagger> ((\<not>$abrupt\<acute>) \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) \<triangleleft> \<sigma> \<dagger> (\<not>$abrupt) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding skip_abr_def
using [[simp_trace]]
by (simp add: usubst)
lemma usubst_cpa_throw_cpa [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"(\<sigma> \<dagger> THROW\<^sub>A\<^sub>B\<^sub>R) = (\<sigma> \<dagger> (\<not>$abrupt) \<turnstile> (\<sigma> \<dagger> ($abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)))"
using assms unfolding throw_abr_def
by (simp add: usubst)
lemma usubst_cpa_assigns_cpa [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"\<sigma> \<dagger> \<langle>\<rho>\<rangle>\<^sub>A\<^sub>B\<^sub>R = (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<sigma> \<dagger> ((\<not>$abrupt\<acute>) \<and> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R)) \<triangleleft> \<sigma> \<dagger> (\<not>$abrupt) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding assigns_abr_def
by (simp add: usubst)
lemma simpl_comp_left_distr:
"(C3_abr (P) ;; R) = ((P;;R) \<triangleleft> \<not>$abrupt \<triangleright> (II ;; R))"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma c3_abr_comp_semir:
"(C3_abr(P) ;; C3_abr(R)) = C3_abr (P ;; C3_abr(R))"
by rel_auto
lemma c3_abr_comp_simpl[uabr_comp]:
"(C3_abr(P) ;; C3_abr(R)) = ((P ;; C3_abr(R)) \<triangleleft> \<not>$abrupt \<triangleright> (II))"
by rel_auto
lemma simpl_abr_comp_semir:
"(Simpl\<^sub>A\<^sub>B\<^sub>R(P) ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R)) = Simpl\<^sub>A\<^sub>B\<^sub>R ((\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> P) ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R))"
by rel_auto
theorem design_top_abr_left_zero[uabr_comp]:
"(\<top>\<^sub>A\<^sub>B\<^sub>R ;; (P \<turnstile> Q)) = \<top>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)
theorem Simpl_abr_top_abr_left_zero[uabr_comp]:
"(\<top>\<^sub>A\<^sub>B\<^sub>R ;; Simpl\<^sub>A\<^sub>B\<^sub>R (P)) = \<top>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)
lemma assigns_lift_cpa_comp_rel_cpa[uabr_comp]:
assumes "$ok \<sharp> P" "$abrupt \<sharp> P"
shows "(\<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R ;; P) = (\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> P)"
apply (insert assms)
apply pred_simp
apply rel_blast
done
lemma lift_des_skip_dr_unit_abr [uabr_comp]:
"(\<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R ;; \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R) = \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
"(\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R ;; \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R) = \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)+
lemma skip_cpa_left_comp_simpl[uabr_comp]:
"(SKIP\<^sub>A\<^sub>B\<^sub>R ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R)) = (Simpl\<^sub>A\<^sub>B\<^sub>R(R))"
by rel_auto
lemma skip_cpa_right_comp_simpl[uabr_comp]:
"(Simpl\<^sub>A\<^sub>B\<^sub>R(R) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) = (Simpl\<^sub>A\<^sub>B\<^sub>R(R))"
by rel_auto
lemma throw_cpa_left_comp_simpl[uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R)) = (THROW\<^sub>A\<^sub>B\<^sub>R)"
by rel_auto
lemma assign_abr_alt_def:
"\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R = Simpl\<^sub>A\<^sub>B\<^sub>R (\<not>$abrupt\<acute> \<and> \<lceil>\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> II\<rceil>\<^sub>A\<^sub>B\<^sub>R)"
by rel_auto
lemma assign_abr_left_comp_c3[uabr_comp]:
"\<langle>a\<rangle>\<^sub>A\<^sub>B\<^sub>R ;; C3_abr (P \<turnstile> Q) = C3_abr (\<lceil>a\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> (P \<turnstile> Q))"
by rel_auto
lemma assigns_abr_comp[uabr_comp]:
"(\<langle>f\<rangle>\<^sub>A\<^sub>B\<^sub>R ;; \<langle>g\<rangle>\<^sub>A\<^sub>B\<^sub>R) = \<langle>g \<circ> f\<rangle>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma usubst_cpa_des_cond_abr [usubst]:
"\<lbrakk>$ok \<sharp> \<sigma>; $ok\<acute> \<sharp> \<sigma> \<rbrakk> \<Longrightarrow>
\<sigma> \<dagger> (R \<turnstile> bif b then P else Q eif) =
(\<sigma> \<dagger> R \<turnstile> (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub>< \<triangleright> \<sigma> \<dagger> Q))"
by (simp add: usubst)
lemma comp_cond_abr_left_distr[uabr_comp]:
"((bif b then Simpl\<^sub>A\<^sub>B\<^sub>R P else Simpl\<^sub>A\<^sub>B\<^sub>R Q eif) ;; Simpl\<^sub>A\<^sub>B\<^sub>R R) =
(bif b then (Simpl\<^sub>A\<^sub>B\<^sub>R P ;; Simpl\<^sub>A\<^sub>B\<^sub>R R) else (Simpl\<^sub>A\<^sub>B\<^sub>R Q ;; Simpl\<^sub>A\<^sub>B\<^sub>R R) eif)"
apply (simp add: usubst uabr_comp)
apply pred_simp
apply rel_simp
apply auto
done
lemma if_mono:
"\<lbrakk> P\<^sub>1 \<sqsubseteq> P\<^sub>2; Q\<^sub>1 \<sqsubseteq> Q\<^sub>2 \<rbrakk> \<Longrightarrow> (bif b then P\<^sub>1 else Q\<^sub>1 eif) \<sqsubseteq> (bif b then P\<^sub>2 else Q\<^sub>2 eif)"
by rel_auto
subsection {*While abrupt usubst*}
subsection {*block abrupt usubst*}
subsection {*Catch abrupt usubst*}
section "Auxiliary algebraic laws for abrupt designs"
theory algebraic_laws_abrupt_aux
imports "../../../theories/Abrupt/utp_abrupt_designs"
begin
named_theorems uabr_simpl and uabr_cond and uabr_comp and uabr_lens
subsection {*THM setup*}
declare design_condr[urel_cond]
subsection {*abrupt alphabet behavior*}
lemma assigns_abr_alpha:
"(abrupt :== (\<not> &abrupt)) = (\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R \<and> $abrupt\<acute> =\<^sub>u (\<not>$abrupt) \<and> $ok =\<^sub>u $ok\<acute>)"
"(ok :== (\<not> &ok)) = (\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R \<and> $abrupt\<acute> =\<^sub>u $abrupt \<and> $ok =\<^sub>u (\<not>$ok\<acute>))"
by rel_auto+
lemma vwb_of_abrupt[simp]:
"vwb_lens ok" "vwb_lens abrupt"
by simp_all
lemma unrest_pre_out\<alpha>_abr[unrest]: "out\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub><"
by (transfer, auto simp add: out\<alpha>_def lens_prod_def)
lemma unrest_post_in\<alpha>_abr[unrest]: "in\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub>>"
by (transfer, auto simp add: in\<alpha>_def lens_prod_def)
lemma unrest_ok_abrupt_rel_uexpr_lift_cpa[unrest]:
"$ok \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R" "$ok\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
"$abrupt \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R" "$abrupt\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by (pred_auto)+
lemma unrest_ok_abrupt_rel_usubst_lift_cpa[unrest]:
"$ok\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R" "$ok \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R"
"$abrupt\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R" "$abrupt \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R"
by rel_auto+
lemma unrest_in_out_rel_ok_abrupt_res_abr [unrest]:
"$ok \<sharp> (P \<restriction>\<^sub>\<alpha> ok)" "$ok\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> ok)"
"$abrupt \<sharp> (P \<restriction>\<^sub>\<alpha> abrupt)" "$abrupt\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> abrupt)"
by (simp_all add: rel_var_res_def unrest)
lemma uabr_alphabet_unrest[unrest]:(*FIXEME:These laws should be generated automatically by alphabet backend since all the fields of alphabet are independant*)
"$ok\<acute> \<sharp> $abrupt\<acute>" "$ok \<sharp> $abrupt"
"$ok\<acute> \<sharp> $abrupt" "$ok \<sharp> $abrupt\<acute>"
"$abrupt\<acute> \<sharp> $ok\<acute>" "$abrupt \<sharp> $ok "
"$abrupt \<sharp> $ok\<acute>" "$abrupt\<acute> \<sharp> $ok"
by pred_simp+
lemma cpa_ord [usubst]:
"$ok \<prec>\<^sub>v $ok\<acute>" "$abrupt \<prec>\<^sub>v $abrupt\<acute>" "$ok \<prec>\<^sub>v $abrupt\<acute>"
"$ok \<prec>\<^sub>v $abrupt" "$ok\<acute> \<prec>\<^sub>v $abrupt\<acute>" "$ok\<acute> \<prec>\<^sub>v $abrupt"
by (simp_all add: var_name_ord_def)
lemma rel_usubst_lift_cpa_in_out_abrupt_ok[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> $abrupt = $abrupt" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$abrupt) = (\<not>$abrupt)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> ($ok) = ($ok)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$ok) = (\<not>$ok)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> ($abrupt\<acute>) = (($abrupt\<acute>))" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$abrupt\<acute>) = (\<not>$abrupt\<acute>)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> ($ok\<acute>) = ($ok\<acute>)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (\<not>$ok\<acute>) = (\<not>$ok\<acute>)"
by (simp_all add: usubst unrest)
lemma abrupt_ok_simpl[uabr_comp]:
"($abrupt ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = $abrupt" "(\<not>$ok ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$ok)"
"($abrupt ;; (P \<turnstile> Q)) = $abrupt" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"(\<not>$abrupt ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$abrupt)" "(\<not>$ok ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$ok)"
"(\<not>$abrupt ;; (P \<turnstile> Q)) = (\<not>$abrupt)" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"($abrupt\<acute> ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = $abrupt\<acute>"
"(\<not>$abrupt\<acute> ;; Simpl\<^sub>A\<^sub>B\<^sub>R P) = (\<not>$abrupt\<acute>)"
by rel_auto+
lemma simpl_abr_in_ok:
"Simpl\<^sub>A\<^sub>B\<^sub>R ($ok) = ((\<not>$abrupt \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_abr_our_ok:
"Simpl\<^sub>A\<^sub>B\<^sub>R ($ok\<acute>) =
((\<not>$abrupt \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_abr_in_abrupt:
"Simpl\<^sub>A\<^sub>B\<^sub>R ($abrupt) =
((\<not>$abrupt \<and> ($ok \<Rightarrow>($ok\<acute> \<and> $abrupt))) \<or> ($abrupt \<and> II))"
by rel_auto
lemma simpl_abr_alr_def:
"Simpl\<^sub>A\<^sub>B\<^sub>R (P) =
((\<not>$abrupt \<and> ($ok \<Rightarrow>($ok\<acute> \<and> P))) \<or> ($abrupt \<and> II))"
by rel_auto
subsection {*Healthiness condition behavior*}
lemma rel_usubst_cpa_c3_abr[usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows "\<sigma> \<dagger> C3_abr(P) = (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> (\<not>$abrupt) \<triangleright> (\<sigma> \<dagger> II))"
using assms unfolding C3_abr_def
by (simp add: usubst)
lemma Simpl_abr_idem[simp]: "Simpl\<^sub>A\<^sub>B\<^sub>R(Simpl\<^sub>A\<^sub>B\<^sub>R(P)) = Simpl\<^sub>A\<^sub>B\<^sub>R(P)"
by (rel_auto)
lemma simpl_abr_Idempotent: "Idempotent Simpl\<^sub>A\<^sub>B\<^sub>R"
by (simp add: Idempotent_def)
lemma Simpl_abr_mono: "P \<sqsubseteq> Q \<Longrightarrow> Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<sqsubseteq> Simpl\<^sub>A\<^sub>B\<^sub>R(Q)"
by (rel_auto)
lemma simpl_abr_Monotonic: "Monotonic Simpl\<^sub>A\<^sub>B\<^sub>R"
by (simp add: Monotonic_def Simpl_abr_mono)
lemma simpl_abr_def:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P) = ((\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> P) \<triangleleft> \<not>$abrupt \<triangleright> II)"
unfolding C3_abr_def ..
lemma simpl_abr_condr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P \<triangleleft> b \<triangleright> Q) = (Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<triangleleft> b \<triangleright> Simpl\<^sub>A\<^sub>B\<^sub>R(Q))"
unfolding simpl_abr_def
by (simp add: urel_cond)
lemma simpl_abr_skip_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R(SKIP\<^sub>A\<^sub>B\<^sub>R) = (SKIP\<^sub>A\<^sub>B\<^sub>R)"
by (simp add: urel_cond urel_defs)
lemma simpl_abr_throw_abr:
"Simpl\<^sub>A\<^sub>B\<^sub>R(THROW\<^sub>A\<^sub>B\<^sub>R) = ((\<not>$abrupt) \<and> ($ok \<Rightarrow>($ok\<acute> \<and> $abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) \<or> ($abrupt \<and> II))"
by rel_auto
lemma simpl_abr_assign_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R(\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) = (\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R)"
by (simp add: urel_cond urel_defs)
lemma simpl_abr_throw_abr_comp_abrupt[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; Simpl\<^sub>A\<^sub>B\<^sub>R Q) \<triangleleft> $abrupt \<triangleright> II)) = Simpl\<^sub>A\<^sub>B\<^sub>R Q"
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_throw_abr_comp_abrupt_cond_throw_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; THROW\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = Simpl\<^sub>A\<^sub>B\<^sub>R THROW\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_throw_abr_comp_abrupt_cond_skip_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = SKIP\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_throw_abr_comp_abrupt_cond_assigns_abr[uabr_simpl]:
"Simpl\<^sub>A\<^sub>B\<^sub>R (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; Simpl\<^sub>A\<^sub>B\<^sub>R Q) \<triangleleft> $abrupt \<triangleright> II)) =
Simpl\<^sub>A\<^sub>B\<^sub>R Q"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt_cond_skip_abr[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
SKIP\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt_cond_throw_abr[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; THROW\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
C3_abr THROW\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma C3_abr_throw_abr_comp_abrupt_cond_assigns_abr[uabr_simpl]:
"C3_abr (THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R"
apply pred_simp
apply rel_simp
apply safe
apply auto
done
(*lemma [uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; THROW\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
(\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> ($abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) "
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma throw_abr_comp_abrupt_cond_skip_abr[uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
(\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<not>$abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) "
apply pred_simp
apply rel_simp
apply safe
apply auto
done
lemma [uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) =
(\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<not>$abrupt\<acute> \<and> \<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R)) "
apply pred_simp
apply rel_simp
apply safe
apply auto
done*)
lemma [uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; ((abrupt:== (\<not> &abrupt) ;; \<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R) \<triangleleft> $abrupt \<triangleright> II)) = (true) "
apply pred_simp
apply rel_simp
apply auto
done
lemma simpl_abr_form:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P) = (((\<not>$abrupt) \<and> (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (P))) \<or> ($abrupt \<and> II))"
by rel_auto
lemma abrupt_simpl_abr[uabr_simpl]:
"($abrupt \<and> Simpl\<^sub>A\<^sub>B\<^sub>R(P)) = ($abrupt \<and>II)"
by rel_auto
lemma nabrupt_simpl_abr[uabr_simpl]:
"(\<not>$abrupt \<and> Simpl\<^sub>A\<^sub>B\<^sub>R(P)) = (\<not>$abrupt \<and> (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (P)))"
by (rel_auto)
definition design_abr_sup :: "('\<alpha>,'\<beta>) rel_cpa set \<Rightarrow> ('\<alpha>,'\<beta>) rel_cpa" ("\<Sqinter>\<^sub>A\<^sub>B\<^sub>R_" [900] 900) where
"\<Sqinter>\<^sub>A\<^sub>B\<^sub>R A = (if (A = {}) then \<top>\<^sub>A\<^sub>B\<^sub>R else \<Sqinter> A)"
lemma simpl_abr_Continuous: "Continuous Simpl\<^sub>A\<^sub>B\<^sub>R"
unfolding Continuous_def SUP_def apply rel_simp
unfolding SUP_def
apply transfer apply auto
done
lemma simpl_abr_R3_conj:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P \<and> Q) = (Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<and> Simpl\<^sub>A\<^sub>B\<^sub>R(Q))"
by (rel_auto)
lemma simpl_abr_disj:
"Simpl\<^sub>A\<^sub>B\<^sub>R(P \<or> Q) = (Simpl\<^sub>A\<^sub>B\<^sub>R(P) \<or> Simpl\<^sub>A\<^sub>B\<^sub>R(Q))"
by (rel_auto)
lemma Simpl_abr_USUP:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>A\<^sub>B\<^sub>R(\<Sqinter> i \<in> A \<bullet> P(i)) = (\<Sqinter> i \<in> A \<bullet> Simpl\<^sub>A\<^sub>B\<^sub>R(P(i)))"
using assms by (rel_auto)
lemma design_abr_sup_non_empty [simp]:
"A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^sub>A\<^sub>B\<^sub>R A = \<Sqinter> A"
by (simp add: design_abr_sup_def)
subsection {*Signature behavior*}
lemma design_top_abr:
"(P \<turnstile> Q) \<sqsubseteq> \<top>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)
lemma design_abr_sup_empty [simp]:
"\<Sqinter>\<^sub>A\<^sub>B\<^sub>R {} = \<top>\<^sub>A\<^sub>B\<^sub>R"
by (simp add: design_abr_sup_def)
abbreviation design_inf :: "('\<alpha>, '\<beta>) rel_des set \<Rightarrow> ('\<alpha>, '\<beta>) rel_des" ("\<Squnion>\<^sub>A\<^sub>B\<^sub>R_" [900] 900) where
"\<Squnion>\<^sub>A\<^sub>B\<^sub>R A \<equiv> \<Squnion> A"
lemma design_bottom_abr:
"\<bottom>\<^sub>A\<^sub>B\<^sub>R \<sqsubseteq> (P \<turnstile> Q)"
by simp
lemma Simpl_abr_bottom_abr:
"\<bottom>\<^sub>A\<^sub>B\<^sub>R \<sqsubseteq> Simpl\<^sub>A\<^sub>B\<^sub>R (P)"
by simp
lemma Simpl_abr_UINF:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>A\<^sub>B\<^sub>R(\<Squnion> i \<in> A \<bullet> P(i)) = (\<Squnion> i \<in> A \<bullet> Simpl\<^sub>A\<^sub>B\<^sub>R(P(i)))"
using assms by (rel_auto)
lemma skip_cpa_def:
"II = (\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R \<and> $abrupt =\<^sub>u $abrupt\<acute> \<and> $ok =\<^sub>u $ok\<acute>)"
by rel_auto
lemma skip_lift_cpa_def:
"\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R = ($\<Sigma>\<^sub>A\<^sub>B\<^sub>R\<acute> =\<^sub>u $\<Sigma>\<^sub>A\<^sub>B\<^sub>R)"
by rel_auto
lemma seqr_abrupt_true [usubst]: "(P ;; Q) \<^sub>a\<^sub>t = (P \<^sub>a\<^sub>t ;; Q)"
by (rel_auto)
lemma seqr_abrupt_false [usubst]: "(P ;; Q) \<^sub>a\<^sub>f = (P \<^sub>a\<^sub>f ;; Q)"
by (rel_auto)
lemma rel_usubst_lift_cpa_uexpr_lift_cpa[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>\<sigma> \<dagger> P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma usubst_lift_cpa_assigns_lift_cpa [usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>\<langle>\<rho> \<circ> \<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by (simp add: usubst)
lemma usubst_lift_cpa_pre_uexpr_lift_cpa[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub>< = \<lceil>\<sigma> \<dagger> b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub><"
by (simp add: usubst)
lemma rel_usubst_lift_cpa_design[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> (Q \<turnstile> P)) = (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> Q) \<turnstile> (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>A\<^sub>B\<^sub>R \<dagger> P)"
by (simp add: usubst unrest)
lemma usubst_cpa_true[usubst]: "\<sigma> \<dagger> \<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma usubst_cpa_false[usubst]: "\<sigma> \<dagger> \<lceil>false\<rceil>\<^sub>A\<^sub>B\<^sub>R = \<lceil>false\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma rel_usubst_cpa_skip_cpa[usubst]:
"(\<sigma> \<dagger> II) = ((\<sigma> \<dagger> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R) \<and> \<sigma> \<dagger> $abrupt =\<^sub>u \<sigma> \<dagger> $abrupt\<acute> \<and> \<sigma> \<dagger> $ok =\<^sub>u \<sigma> \<dagger> $ok\<acute>)"
by (simp add: usubst unrest skip_cpa_def)
lemma usubst_lift_cpa_skip_lift_cpa[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R) = \<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R"
unfolding skip_r_def
by (simp add: usubst_lift_cpa_assigns_lift_cpa)
lemma usubst_cpa_skip_cpa [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"(\<sigma> \<dagger> SKIP\<^sub>A\<^sub>B\<^sub>R) = (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<sigma> \<dagger> ((\<not>$abrupt\<acute>) \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)) \<triangleleft> \<sigma> \<dagger> (\<not>$abrupt) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding skip_abr_def
using [[simp_trace]]
by (simp add: usubst)
lemma usubst_cpa_throw_cpa [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"(\<sigma> \<dagger> THROW\<^sub>A\<^sub>B\<^sub>R) = (\<sigma> \<dagger> (\<not>$abrupt) \<turnstile> (\<sigma> \<dagger> ($abrupt\<acute> \<and> \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R)))"
using assms unfolding throw_abr_def
by (simp add: usubst)
lemma usubst_cpa_assigns_cpa [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"\<sigma> \<dagger> \<langle>\<rho>\<rangle>\<^sub>A\<^sub>B\<^sub>R = (\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> (\<sigma> \<dagger> ((\<not>$abrupt\<acute>) \<and> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R)) \<triangleleft> \<sigma> \<dagger> (\<not>$abrupt) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding assigns_abr_def
by (simp add: usubst)
lemma simpl_comp_left_distr:
"(C3_abr (P) ;; R) = ((P;;R) \<triangleleft> \<not>$abrupt \<triangleright> (II ;; R))"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma c3_abr_comp_semir:
"(C3_abr(P) ;; C3_abr(R)) = C3_abr (P ;; C3_abr(R))"
by rel_auto
lemma c3_abr_comp_simpl[uabr_comp]:
"(C3_abr(P) ;; C3_abr(R)) = ((P ;; C3_abr(R)) \<triangleleft> \<not>$abrupt \<triangleright> (II))"
by rel_auto
lemma simpl_abr_comp_semir:
"(Simpl\<^sub>A\<^sub>B\<^sub>R(P) ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R)) = Simpl\<^sub>A\<^sub>B\<^sub>R ((\<lceil>true\<rceil>\<^sub>A\<^sub>B\<^sub>R \<turnstile> P) ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R))"
by rel_auto
theorem design_top_abr_left_zero[uabr_comp]:
"(\<top>\<^sub>A\<^sub>B\<^sub>R ;; (P \<turnstile> Q)) = \<top>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)
theorem Simpl_abr_top_abr_left_zero[uabr_comp]:
"(\<top>\<^sub>A\<^sub>B\<^sub>R ;; Simpl\<^sub>A\<^sub>B\<^sub>R (P)) = \<top>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)
lemma assigns_lift_cpa_comp_rel_cpa[uabr_comp]:
assumes "$ok \<sharp> P" "$abrupt \<sharp> P"
shows "(\<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>A\<^sub>B\<^sub>R ;; P) = (\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> P)"
apply (insert assms)
apply pred_simp
apply rel_blast
done
lemma lift_des_skip_dr_unit_abr [uabr_comp]:
"(\<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R ;; \<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R) = \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
"(\<lceil>II\<rceil>\<^sub>A\<^sub>B\<^sub>R ;; \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R) = \<lceil>P\<rceil>\<^sub>A\<^sub>B\<^sub>R"
by (rel_auto)+
lemma skip_cpa_left_comp_simpl[uabr_comp]:
"(SKIP\<^sub>A\<^sub>B\<^sub>R ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R)) = (Simpl\<^sub>A\<^sub>B\<^sub>R(R))"
by rel_auto
lemma skip_cpa_right_comp_simpl[uabr_comp]:
"(Simpl\<^sub>A\<^sub>B\<^sub>R(R) ;; SKIP\<^sub>A\<^sub>B\<^sub>R) = (Simpl\<^sub>A\<^sub>B\<^sub>R(R))"
by rel_auto
lemma throw_cpa_left_comp_simpl[uabr_comp]:
"(THROW\<^sub>A\<^sub>B\<^sub>R ;; Simpl\<^sub>A\<^sub>B\<^sub>R(R)) = (THROW\<^sub>A\<^sub>B\<^sub>R)"
by rel_auto
lemma assign_abr_alt_def:
"\<langle>\<sigma>\<rangle>\<^sub>A\<^sub>B\<^sub>R = Simpl\<^sub>A\<^sub>B\<^sub>R (\<not>$abrupt\<acute> \<and> \<lceil>\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> II\<rceil>\<^sub>A\<^sub>B\<^sub>R)"
by rel_auto
lemma assign_abr_left_comp_c3[uabr_comp]:
"\<langle>a\<rangle>\<^sub>A\<^sub>B\<^sub>R ;; C3_abr (P \<turnstile> Q) = C3_abr (\<lceil>a\<rceil>\<^sub>s\<^sub>A\<^sub>B\<^sub>R \<dagger> (P \<turnstile> Q))"
by rel_auto
lemma assigns_abr_comp[uabr_comp]:
"(\<langle>f\<rangle>\<^sub>A\<^sub>B\<^sub>R ;; \<langle>g\<rangle>\<^sub>A\<^sub>B\<^sub>R) = \<langle>g \<circ> f\<rangle>\<^sub>A\<^sub>B\<^sub>R"
by rel_auto
lemma usubst_cpa_des_cond_abr [usubst]:
"\<lbrakk>$ok \<sharp> \<sigma>; $ok\<acute> \<sharp> \<sigma> \<rbrakk> \<Longrightarrow>
\<sigma> \<dagger> (R \<turnstile> bif b then P else Q eif) =
(\<sigma> \<dagger> R \<turnstile> (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> \<lceil>b\<rceil>\<^sub>A\<^sub>B\<^sub>R\<^sub>< \<triangleright> \<sigma> \<dagger> Q))"
by (simp add: usubst)
lemma comp_cond_abr_left_distr[uabr_comp]:
"((bif b then Simpl\<^sub>A\<^sub>B\<^sub>R P else Simpl\<^sub>A\<^sub>B\<^sub>R Q eif) ;; Simpl\<^sub>A\<^sub>B\<^sub>R R) =
(bif b then (Simpl\<^sub>A\<^sub>B\<^sub>R P ;; Simpl\<^sub>A\<^sub>B\<^sub>R R) else (Simpl\<^sub>A\<^sub>B\<^sub>R Q ;; Simpl\<^sub>A\<^sub>B\<^sub>R R) eif)"
apply (simp add: usubst uabr_comp)
apply pred_simp
apply rel_simp
apply auto
done
lemma if_mono:
"\<lbrakk> P\<^sub>1 \<sqsubseteq> P\<^sub>2; Q\<^sub>1 \<sqsubseteq> Q\<^sub>2 \<rbrakk> \<Longrightarrow> (bif b then P\<^sub>1 else Q\<^sub>1 eif) \<sqsubseteq> (bif b then P\<^sub>2 else Q\<^sub>2 eif)"
by rel_auto
subsection {*While abrupt usubst*}
subsection {*block abrupt usubst*}
subsection {*Catch abrupt usubst*}
end

View File

@ -1,450 +1,450 @@
section "Algebraic laws for abrupt designs"
theory algebraic_laws_fault
imports algebraic_laws_fault_aux
begin
(*TODO: add laws for assigns when composed with try catch...*)
subsection"Simpset configuration"
declare urel_comp [uflt_comp]
declare urel_cond [uflt_cond]
subsection"Skip"
text{*In this section we introduce the algebraic laws of programming related to the SKIP
statement.*}
lemma true_left_zero_skip_cpf_abr[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; true) = (true)"
by rel_auto
lemma true_lift_flt_right_zero_skip_flt[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; \<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T) = (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma false_lift_flt_right_zero[uflt_comp]:
"(P ;; \<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T) = (\<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma skip_flt_left_unit_assigns_flt[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; \<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T) = (\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma top_flt_right_zero_skip_flt[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; \<top>\<^sub>F\<^sub>L\<^sub>T) = (\<top>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma ivar_left_zero_skip_flt[uflt_comp]:
"($x ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = $x"
by rel_auto
lemma top_flt_left_zero_skip_flt[uflt_comp]:
"(\<top>\<^sub>F\<^sub>L\<^sub>T ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = (\<top>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma skip_flt_idem [uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = SKIP\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma skip_flt_alpha_eq:
"SKIP\<^sub>F\<^sub>L\<^sub>T = Simpl\<^sub>F\<^sub>L\<^sub>T (\<not>$fault\<acute> \<and> ($\<Sigma>\<^sub>F\<^sub>L\<^sub>T\<acute> =\<^sub>u $\<Sigma>\<^sub>F\<^sub>L\<^sub>T))"
by rel_auto
lemma simpl_pre_skip_flt_post:
"(Simpl\<^sub>F\<^sub>L\<^sub>T \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>< \<and> SKIP\<^sub>F\<^sub>L\<^sub>T) = (SKIP\<^sub>F\<^sub>L\<^sub>T \<and> Simpl\<^sub>F\<^sub>L\<^sub>T \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>>)"
by rel_auto
lemma simpl_pre_skip_flt_var:
fixes x :: "(bool, ('b) cpf) uvar"
shows "(Simpl\<^sub>F\<^sub>L\<^sub>T $x \<and> SKIP\<^sub>F\<^sub>L\<^sub>T) = (SKIP\<^sub>F\<^sub>L\<^sub>T \<and> Simpl\<^sub>F\<^sub>L\<^sub>T $x\<acute>)"
by rel_auto
lemma skip_flt_post_left_unit[uflt_comp]:
"(S \<turnstile> (SKIP\<^sub>F\<^sub>L\<^sub>T;; Q)) = (S \<turnstile> Q)"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma simpl_flt_post_left_unit[uflt_comp]:
"(S \<turnstile> (Simpl\<^sub>F\<^sub>L\<^sub>T (\<not>$fault\<acute> \<and> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T);; Q)) = (S \<turnstile> Q)"
apply pred_simp
apply rel_simp
apply transfer
apply auto
done
subsection {*Assignment Laws*}
text{*In this section we introduce the algebraic laws of programming related to the assignment
statement.*}
lemma design_post_seqr_assigns_flt_condr_fault_L6_left[urel_cond]:
"((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> $fault \<triangleright> Q))) \<triangleleft> \<not> $fault \<triangleright> R) =
((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; Q)) \<triangleleft> \<not> $fault \<triangleright> R)"
unfolding assigns_flt_def
apply pred_simp
apply fastforce
done
lemma design_post_seqr_assigns_flt_condr_not_fault_L6_left[urel_cond]:
"((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> \<not> $fault \<triangleright> Q))) \<triangleleft> $fault \<triangleright> R) =
((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; Q)) \<triangleleft> $fault \<triangleright> R)"
unfolding assigns_flt_def
apply pred_simp
apply rel_simp
apply fastforce
done
lemma design_post_seqr_assigns_flt_condr_fault_L6_right[urel_cond]:
"(R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> $fault \<triangleright> Q)))) =
(R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; P)))"
unfolding assigns_flt_def
apply pred_simp
apply rel_simp
apply fastforce
done
lemma design_post_seqr_assigns_flt_condr_not_fault_L6_right[urel_cond]:
"(R \<triangleleft> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> \<not> $fault \<triangleright> Q)))) =
(R \<triangleleft> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; P)) )"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma rcond_not_fault_subst_cancel_design_post_right[urel_cond]:
"R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; P)) =
R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault\<acute>) ;; P))"
apply pred_simp
apply rel_simp
done
lemma usubst_flt_cancel [usubst]:
assumes 1:"weak_lens v"
shows "($v)\<lbrakk>\<lceil>expr\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub></$v\<rbrakk>= \<lceil>expr\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
using 1
by rel_auto
lemma usubst_flt_lift_cancel[usubst]:
assumes 1:"weak_lens v"
shows "\<lceil>($v)\<lbrakk>\<lceil>expr\<rceil>\<^sub></$v\<rbrakk>\<rceil>\<^sub>F\<^sub>L\<^sub>T= \<lceil>expr\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
using 1
by rel_auto
lemma assigns_flt_id [uflt_simpl]:
"SKIP\<^sub>F\<^sub>L\<^sub>T = \<langle>id\<rangle>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
lemma assign_test[uflt_comp]:
assumes 1:"mwb_lens x"
shows "(x \<Midarrow> \<guillemotleft>u\<guillemotright> ;; x \<Midarrow> \<guillemotleft>v\<guillemotright>) = (x \<Midarrow> \<guillemotleft>v\<guillemotright>)"
using 1
by (simp add: usubst uflt_comp )
lemma assign_flt_left_comp_subst[uflt_comp]:
"(x \<Midarrow> u ;; Simpl\<^sub>F\<^sub>L\<^sub>T(\<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> \<lceil>Q\<rceil>\<^sub>F\<^sub>L\<^sub>T)) = Simpl\<^sub>F\<^sub>L\<^sub>T(\<lceil>P\<lbrakk>\<lceil>u\<rceil>\<^sub></$x\<rbrakk>\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> \<lceil>Q\<lbrakk>\<lceil>u\<rceil>\<^sub></$x\<rbrakk>\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by (simp add: uflt_comp usubst)
lemma assign_flt_twice[uflt_comp]:
assumes "mwb_lens x" and "x \<sharp> f"
shows "(x \<Midarrow> e ;; x \<Midarrow> f) = (x \<Midarrow> f)"
using assms
by (simp add: uflt_comp usubst)
lemma assign_flt_commute:
assumes "x \<bowtie> y" "x \<sharp> f" "y \<sharp> e"
shows "(x \<Midarrow> e ;; y \<Midarrow> f) = (y \<Midarrow> f ;; x \<Midarrow> e)"
using assms
by (simp add: uflt_comp usubst usubst_upd_comm)
lemma assign_flt_cond_flt[uflt_comp]: (*needs more laws to be automatic*)
fixes x :: "('a, '\<alpha>) uvar"
shows "(x \<Midarrow> e ;; (bif b then Simpl\<^sub>F\<^sub>L\<^sub>T P else Simpl\<^sub>F\<^sub>L\<^sub>T Q eif)) =
(bif (b\<lbrakk>e/x\<rbrakk>) then (x \<Midarrow> e ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) else (x \<Midarrow> e ;; Simpl\<^sub>F\<^sub>L\<^sub>T Q) eif)"
apply (simp add: usubst uflt_comp)
apply rel_auto
done
lemma assign_flt_uop1[uflt_comp]:
assumes 1: "mwb_lens v"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (uop F (&v))) = (v \<Midarrow> (uop F e1))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_bop1[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2"
shows "(v \<Midarrow> e1 ;; v \<Midarrow>(bop bp (&v) e2)) = (v \<Midarrow> (bop bp e1 e2))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_bop2[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (bop bp e2 (&v))) = (v \<Midarrow> (bop bp e2 e1))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_trop1[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (trop tp (&v) e2 e3)) =
(v \<Midarrow> (trop tp e1 e2 e3))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_trop2[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (trop tp e2 (&v) e3)) =
(v \<Midarrow> (trop tp e2 e1 e3))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_trop3[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (trop tp e2 e3 (&v))) =
(v \<Midarrow> (trop tp e2 e3 e1))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop1[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp (&v) e2 e3 e4)) =
(v \<Midarrow> (qtop tp e1 e2 e3 e4))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop2[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp e2 (&v) e3 e4)) =
(v \<Midarrow> (qtop tp e2 e1 e3 e4))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop3[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp e2 e3 (&v) e4)) =
(v \<Midarrow> (qtop tp e2 e3 e1 e4))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop4[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp e2 e3 e4 (&v))) =
(v \<Midarrow> (qtop tp e2 e3 e4 e1))"
by (simp add: usubst uflt_comp assms)
text {*In the sequel we define assignment laws proposed by Hoare*}
lemma assign_flt_vwb_skip_flt[uflt_comp]:
assumes 1: "vwb_lens v"
shows "(v \<Midarrow> &v) = SKIP\<^sub>F\<^sub>L\<^sub>T"
by (simp add: assms usubst uflt_simpl)
lemma assign_flt_simultaneous:
assumes 1: "vwb_lens var2"
and 2: "var1 \<bowtie> var2"
shows "var1, var2 \<Midarrow> exp, &var2 = var1 \<Midarrow> exp"
by (simp add: assms usubst_upd_comm usubst)
lemma assign_flt_seq[uflt_comp]:
assumes 1: "vwb_lens var2"
shows"(var1 \<Midarrow> exp);; (var2 \<Midarrow> &var2) = (var1 \<Midarrow> exp)"
by (simp add: assms usubst uflt_comp)
lemma assign_flt_cond_flt_uop[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v"
shows "bif uop F exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif uop F (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms weak_lens.put_get)+
done
lemma assign_flt_cond_bop1[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2"
shows "bif bop bp exp exp2 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif bop bp (&v) exp2 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_bop2[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2"
shows "bif bop bp exp2 exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif bop bp exp2 (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_trop1[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3"
shows "bif trop bp exp exp2 exp3 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif trop bp (&v) exp2 exp3 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_trop2[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3"
shows "bif trop bp exp2 exp exp3 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif trop bp exp2 (&v) exp3 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_trop3[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3"
shows "bif trop bp exp2 exp3 exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;;Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif trop bp exp2 exp3 (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop1[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4: "v \<sharp> exp4"
shows "bif qtop bp exp exp2 exp3 exp4 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp (&v) exp2 exp3 exp4 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop2[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4:"v \<sharp> exp4"
shows "bif qtop bp exp2 exp exp3 exp4 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp exp2 (&v) exp3 exp4 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop3[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4: "v \<sharp> exp4"
shows "bif qtop bp exp2 exp3 exp exp4 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp exp2 exp3 (&v) exp4 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop4[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4: "v \<sharp> exp4"
shows "bif qtop bp exp2 exp3 exp4 exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp exp2 exp3 exp4 (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl)
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_If [uflt_cond]:
"(bif bexp then (v \<Midarrow> exp1) else (v \<Midarrow> exp2) eif) =
(v \<Midarrow> (exp1 \<triangleleft> bexp \<triangleright> exp2))"
by rel_auto
subsection {*While laws*}
text{*In this section we introduce the algebraic laws of programming related to the while
statement.*}
theorem while_unfold:
"while b do P od = (bif b then (P ;; while b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
proof -
have m:"mono (\<lambda>X. bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (auto intro: monoI seqr_mono if_mono)
have "(while b do P od) = (\<nu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_def)
also have "... = (bif b then (P ;; (\<nu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (subst lfp_unfold,simp_all add:m )
also have "... = (bif b then (P ;; while b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_def)
finally show ?thesis .
qed
(*lemma while_true:
shows "(while true do P od) = \<top>\<^sub>A\<^sub>B\<^sub>R"
apply (simp add: While_def alpha)
apply (rule antisym)
apply (simp_all)
apply (rule conjI)
apply (rule lfp_lowerbound)
apply (simp add: C3_abr_def design_def cond_def)
apply rel_auto
apply (frule cond_mono)
done*)
lemma while_false:
shows "(while false do P od) = SKIP\<^sub>F\<^sub>L\<^sub>T"
proof -
have "(while false do P od) = bif false then (P ;; while false do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif"
using while_unfold[of _ P] by simp
also have "... = SKIP\<^sub>F\<^sub>L\<^sub>T" by rel_blast
finally show ?thesis .
qed
lemma while_inv_unfold:
"while b invr p do P od = (bif b then (P ;; while b invr p do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
unfolding While_inv_def using while_unfold
by auto
theorem while_bot_unfold:
"while\<^sub>\<bottom> b do P od = (bif b then (P ;; while\<^sub>\<bottom> b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
proof -
have m:"mono (\<lambda>X. bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (auto intro: monoI seqr_mono if_mono)
have "(while\<^sub>\<bottom> b do P od) = (\<mu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_bot_def)
also have "... = (bif b then (P ;; (\<mu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (subst gfp_unfold, simp_all add: m)
also have "... = (bif b then (P ;; while\<^sub>\<bottom> b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_bot_def)
finally show ?thesis .
qed
theorem while_bot_false: "while\<^sub>\<bottom> false do P od = SKIP\<^sub>F\<^sub>L\<^sub>T"
by (simp add: While_bot_def mu_const alpha)
theorem while_bot_true: "while\<^sub>\<bottom> true do P od = (\<mu> X \<bullet> (P ;; X))"
by (simp add: While_bot_def alpha)
subsection {*assume laws*}
lemma assume_twice[uflt_comp]: "(b\<^sup>\<top>\<^sup>C ;; c\<^sup>\<top>\<^sup>C) = (b \<and> c)\<^sup>\<top>\<^sup>C"
apply pred_simp
apply auto
apply (rel_simp)+
apply blast
apply (rel_simp)+
apply (metis (full_types))
done
lemma assert_twice[uflt_comp]: "(b\<^sub>\<bottom>\<^sub>C ;; c\<^sub>\<bottom>\<^sub>C) = (b \<and> c)\<^sub>\<bottom>\<^sub>C"
apply pred_simp
apply auto
apply (rel_simp)+
apply blast
apply (rel_simp)+
apply (metis (full_types))
done
subsection {*Try Catch laws*}
(*see utp_hoare_helper*)
section "Algebraic laws for abrupt designs"
theory algebraic_laws_fault
imports algebraic_laws_fault_aux
begin
(*TODO: add laws for assigns when composed with try catch...*)
subsection"Simpset configuration"
declare urel_comp [uflt_comp]
declare urel_cond [uflt_cond]
subsection"Skip"
text{*In this section we introduce the algebraic laws of programming related to the SKIP
statement.*}
lemma true_left_zero_skip_cpf_abr[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; true) = (true)"
by rel_auto
lemma true_lift_flt_right_zero_skip_flt[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; \<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T) = (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma false_lift_flt_right_zero[uflt_comp]:
"(P ;; \<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T) = (\<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma skip_flt_left_unit_assigns_flt[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; \<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T) = (\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma top_flt_right_zero_skip_flt[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; \<top>\<^sub>F\<^sub>L\<^sub>T) = (\<top>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma ivar_left_zero_skip_flt[uflt_comp]:
"($x ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = $x"
by rel_auto
lemma top_flt_left_zero_skip_flt[uflt_comp]:
"(\<top>\<^sub>F\<^sub>L\<^sub>T ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = (\<top>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma skip_flt_idem [uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = SKIP\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma skip_flt_alpha_eq:
"SKIP\<^sub>F\<^sub>L\<^sub>T = Simpl\<^sub>F\<^sub>L\<^sub>T (\<not>$fault\<acute> \<and> ($\<Sigma>\<^sub>F\<^sub>L\<^sub>T\<acute> =\<^sub>u $\<Sigma>\<^sub>F\<^sub>L\<^sub>T))"
by rel_auto
lemma simpl_pre_skip_flt_post:
"(Simpl\<^sub>F\<^sub>L\<^sub>T \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>< \<and> SKIP\<^sub>F\<^sub>L\<^sub>T) = (SKIP\<^sub>F\<^sub>L\<^sub>T \<and> Simpl\<^sub>F\<^sub>L\<^sub>T \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>>)"
by rel_auto
lemma simpl_pre_skip_flt_var:
fixes x :: "(bool, ('b) cpf) uvar"
shows "(Simpl\<^sub>F\<^sub>L\<^sub>T $x \<and> SKIP\<^sub>F\<^sub>L\<^sub>T) = (SKIP\<^sub>F\<^sub>L\<^sub>T \<and> Simpl\<^sub>F\<^sub>L\<^sub>T $x\<acute>)"
by rel_auto
lemma skip_flt_post_left_unit[uflt_comp]:
"(S \<turnstile> (SKIP\<^sub>F\<^sub>L\<^sub>T;; Q)) = (S \<turnstile> Q)"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma simpl_flt_post_left_unit[uflt_comp]:
"(S \<turnstile> (Simpl\<^sub>F\<^sub>L\<^sub>T (\<not>$fault\<acute> \<and> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T);; Q)) = (S \<turnstile> Q)"
apply pred_simp
apply rel_simp
apply transfer
apply auto
done
subsection {*Assignment Laws*}
text{*In this section we introduce the algebraic laws of programming related to the assignment
statement.*}
lemma design_post_seqr_assigns_flt_condr_fault_L6_left[urel_cond]:
"((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> $fault \<triangleright> Q))) \<triangleleft> \<not> $fault \<triangleright> R) =
((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; Q)) \<triangleleft> \<not> $fault \<triangleright> R)"
unfolding assigns_flt_def
apply pred_simp
apply fastforce
done
lemma design_post_seqr_assigns_flt_condr_not_fault_L6_left[urel_cond]:
"((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> \<not> $fault \<triangleright> Q))) \<triangleleft> $fault \<triangleright> R) =
((S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; Q)) \<triangleleft> $fault \<triangleright> R)"
unfolding assigns_flt_def
apply pred_simp
apply rel_simp
apply fastforce
done
lemma design_post_seqr_assigns_flt_condr_fault_L6_right[urel_cond]:
"(R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> $fault \<triangleright> Q)))) =
(R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; P)))"
unfolding assigns_flt_def
apply pred_simp
apply rel_simp
apply fastforce
done
lemma design_post_seqr_assigns_flt_condr_not_fault_L6_right[urel_cond]:
"(R \<triangleleft> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; (P \<triangleleft> \<not> $fault \<triangleright> Q)))) =
(R \<triangleleft> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; P)) )"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma rcond_not_fault_subst_cancel_design_post_right[urel_cond]:
"R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T;; P)) =
R \<triangleleft> \<not> $fault \<triangleright> (S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault\<acute>) ;; P))"
apply pred_simp
apply rel_simp
done
lemma usubst_flt_cancel [usubst]:
assumes 1:"weak_lens v"
shows "($v)\<lbrakk>\<lceil>expr\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub></$v\<rbrakk>= \<lceil>expr\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
using 1
by rel_auto
lemma usubst_flt_lift_cancel[usubst]:
assumes 1:"weak_lens v"
shows "\<lceil>($v)\<lbrakk>\<lceil>expr\<rceil>\<^sub></$v\<rbrakk>\<rceil>\<^sub>F\<^sub>L\<^sub>T= \<lceil>expr\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
using 1
by rel_auto
lemma assigns_flt_id [uflt_simpl]:
"SKIP\<^sub>F\<^sub>L\<^sub>T = \<langle>id\<rangle>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
lemma assign_test[uflt_comp]:
assumes 1:"mwb_lens x"
shows "(x \<Midarrow> \<guillemotleft>u\<guillemotright> ;; x \<Midarrow> \<guillemotleft>v\<guillemotright>) = (x \<Midarrow> \<guillemotleft>v\<guillemotright>)"
using 1
by (simp add: usubst uflt_comp )
lemma assign_flt_left_comp_subst[uflt_comp]:
"(x \<Midarrow> u ;; Simpl\<^sub>F\<^sub>L\<^sub>T(\<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> \<lceil>Q\<rceil>\<^sub>F\<^sub>L\<^sub>T)) = Simpl\<^sub>F\<^sub>L\<^sub>T(\<lceil>P\<lbrakk>\<lceil>u\<rceil>\<^sub></$x\<rbrakk>\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> \<lceil>Q\<lbrakk>\<lceil>u\<rceil>\<^sub></$x\<rbrakk>\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by (simp add: uflt_comp usubst)
lemma assign_flt_twice[uflt_comp]:
assumes "mwb_lens x" and "x \<sharp> f"
shows "(x \<Midarrow> e ;; x \<Midarrow> f) = (x \<Midarrow> f)"
using assms
by (simp add: uflt_comp usubst)
lemma assign_flt_commute:
assumes "x \<bowtie> y" "x \<sharp> f" "y \<sharp> e"
shows "(x \<Midarrow> e ;; y \<Midarrow> f) = (y \<Midarrow> f ;; x \<Midarrow> e)"
using assms
by (simp add: uflt_comp usubst usubst_upd_comm)
lemma assign_flt_cond_flt[uflt_comp]: (*needs more laws to be automatic*)
fixes x :: "('a, '\<alpha>) uvar"
shows "(x \<Midarrow> e ;; (bif b then Simpl\<^sub>F\<^sub>L\<^sub>T P else Simpl\<^sub>F\<^sub>L\<^sub>T Q eif)) =
(bif (b\<lbrakk>e/x\<rbrakk>) then (x \<Midarrow> e ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) else (x \<Midarrow> e ;; Simpl\<^sub>F\<^sub>L\<^sub>T Q) eif)"
apply (simp add: usubst uflt_comp)
apply rel_auto
done
lemma assign_flt_uop1[uflt_comp]:
assumes 1: "mwb_lens v"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (uop F (&v))) = (v \<Midarrow> (uop F e1))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_bop1[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2"
shows "(v \<Midarrow> e1 ;; v \<Midarrow>(bop bp (&v) e2)) = (v \<Midarrow> (bop bp e1 e2))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_bop2[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (bop bp e2 (&v))) = (v \<Midarrow> (bop bp e2 e1))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_trop1[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (trop tp (&v) e2 e3)) =
(v \<Midarrow> (trop tp e1 e2 e3))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_trop2[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (trop tp e2 (&v) e3)) =
(v \<Midarrow> (trop tp e2 e1 e3))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_trop3[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (trop tp e2 e3 (&v))) =
(v \<Midarrow> (trop tp e2 e3 e1))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop1[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp (&v) e2 e3 e4)) =
(v \<Midarrow> (qtop tp e1 e2 e3 e4))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop2[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp e2 (&v) e3 e4)) =
(v \<Midarrow> (qtop tp e2 e1 e3 e4))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop3[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp e2 e3 (&v) e4)) =
(v \<Midarrow> (qtop tp e2 e3 e1 e4))"
by (simp add: usubst uflt_comp assms)
lemma assign_flt_qtop4[uflt_comp]:
assumes 1: "mwb_lens v" and 2:"v \<sharp> e2" and 3:"v \<sharp> e3" and 4:"v \<sharp> e4"
shows "(v \<Midarrow> e1 ;; v \<Midarrow> (qtop tp e2 e3 e4 (&v))) =
(v \<Midarrow> (qtop tp e2 e3 e4 e1))"
by (simp add: usubst uflt_comp assms)
text {*In the sequel we define assignment laws proposed by Hoare*}
lemma assign_flt_vwb_skip_flt[uflt_comp]:
assumes 1: "vwb_lens v"
shows "(v \<Midarrow> &v) = SKIP\<^sub>F\<^sub>L\<^sub>T"
by (simp add: assms usubst uflt_simpl)
lemma assign_flt_simultaneous:
assumes 1: "vwb_lens var2"
and 2: "var1 \<bowtie> var2"
shows "var1, var2 \<Midarrow> exp, &var2 = var1 \<Midarrow> exp"
by (simp add: assms usubst_upd_comm usubst)
lemma assign_flt_seq[uflt_comp]:
assumes 1: "vwb_lens var2"
shows"(var1 \<Midarrow> exp);; (var2 \<Midarrow> &var2) = (var1 \<Midarrow> exp)"
by (simp add: assms usubst uflt_comp)
lemma assign_flt_cond_flt_uop[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v"
shows "bif uop F exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif uop F (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms weak_lens.put_get)+
done
lemma assign_flt_cond_bop1[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2"
shows "bif bop bp exp exp2 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif bop bp (&v) exp2 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_bop2[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2"
shows "bif bop bp exp2 exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif bop bp exp2 (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_trop1[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3"
shows "bif trop bp exp exp2 exp3 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif trop bp (&v) exp2 exp3 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_trop2[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3"
shows "bif trop bp exp2 exp exp3 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif trop bp exp2 (&v) exp3 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_trop3[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3"
shows "bif trop bp exp2 exp3 exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;;Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif trop bp exp2 exp3 (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop1[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4: "v \<sharp> exp4"
shows "bif qtop bp exp exp2 exp3 exp4 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp (&v) exp2 exp3 exp4 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop2[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4:"v \<sharp> exp4"
shows "bif qtop bp exp2 exp exp3 exp4 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp exp2 (&v) exp3 exp4 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop3[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4: "v \<sharp> exp4"
shows "bif qtop bp exp2 exp3 exp exp4 then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp exp2 exp3 (&v) exp4 then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl )
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_qtop4[uflt_comp]: (*needs more laws to be automatic*)
assumes 1: "weak_lens v" and 2: "v \<sharp> exp2" and 3: "v \<sharp> exp3" and 4: "v \<sharp> exp4"
shows "bif qtop bp exp2 exp3 exp4 exp then (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C1) else (v \<Midarrow> exp ;; Simpl\<^sub>F\<^sub>L\<^sub>T C2) eif =
v \<Midarrow> exp ;; bif qtop bp exp2 exp3 exp4 (&v) then Simpl\<^sub>F\<^sub>L\<^sub>T C1 else Simpl\<^sub>F\<^sub>L\<^sub>T C2 eif"
apply (simp add: assms usubst uflt_comp uflt_simpl)
apply pred_simp
apply rel_simp
apply auto
apply (metis assms unrest_upred.rep_eq weak_lens.put_get)+
done
lemma assign_flt_cond_If [uflt_cond]:
"(bif bexp then (v \<Midarrow> exp1) else (v \<Midarrow> exp2) eif) =
(v \<Midarrow> (exp1 \<triangleleft> bexp \<triangleright> exp2))"
by rel_auto
subsection {*While laws*}
text{*In this section we introduce the algebraic laws of programming related to the while
statement.*}
theorem while_unfold:
"while b do P od = (bif b then (P ;; while b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
proof -
have m:"mono (\<lambda>X. bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (auto intro: monoI seqr_mono if_mono)
have "(while b do P od) = (\<nu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_def)
also have "... = (bif b then (P ;; (\<nu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (subst lfp_unfold,simp_all add:m )
also have "... = (bif b then (P ;; while b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_def)
finally show ?thesis .
qed
(*lemma while_true:
shows "(while true do P od) = \<top>\<^sub>A\<^sub>B\<^sub>R"
apply (simp add: While_def alpha)
apply (rule antisym)
apply (simp_all)
apply (rule conjI)
apply (rule lfp_lowerbound)
apply (simp add: C3_abr_def design_def cond_def)
apply rel_auto
apply (frule cond_mono)
done*)
lemma while_false:
shows "(while false do P od) = SKIP\<^sub>F\<^sub>L\<^sub>T"
proof -
have "(while false do P od) = bif false then (P ;; while false do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif"
using while_unfold[of _ P] by simp
also have "... = SKIP\<^sub>F\<^sub>L\<^sub>T" by rel_blast
finally show ?thesis .
qed
lemma while_inv_unfold:
"while b invr p do P od = (bif b then (P ;; while b invr p do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
unfolding While_inv_def using while_unfold
by auto
theorem while_bot_unfold:
"while\<^sub>\<bottom> b do P od = (bif b then (P ;; while\<^sub>\<bottom> b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
proof -
have m:"mono (\<lambda>X. bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (auto intro: monoI seqr_mono if_mono)
have "(while\<^sub>\<bottom> b do P od) = (\<mu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_bot_def)
also have "... = (bif b then (P ;; (\<mu> X \<bullet> bif b then (P ;; X) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (subst gfp_unfold, simp_all add: m)
also have "... = (bif b then (P ;; while\<^sub>\<bottom> b do P od) else SKIP\<^sub>F\<^sub>L\<^sub>T eif)"
by (simp add: While_bot_def)
finally show ?thesis .
qed
theorem while_bot_false: "while\<^sub>\<bottom> false do P od = SKIP\<^sub>F\<^sub>L\<^sub>T"
by (simp add: While_bot_def mu_const alpha)
theorem while_bot_true: "while\<^sub>\<bottom> true do P od = (\<mu> X \<bullet> (P ;; X))"
by (simp add: While_bot_def alpha)
subsection {*assume laws*}
lemma assume_twice[uflt_comp]: "(b\<^sup>\<top>\<^sup>C ;; c\<^sup>\<top>\<^sup>C) = (b \<and> c)\<^sup>\<top>\<^sup>C"
apply pred_simp
apply auto
apply (rel_simp)+
apply blast
apply (rel_simp)+
apply (metis (full_types))
done
lemma assert_twice[uflt_comp]: "(b\<^sub>\<bottom>\<^sub>C ;; c\<^sub>\<bottom>\<^sub>C) = (b \<and> c)\<^sub>\<bottom>\<^sub>C"
apply pred_simp
apply auto
apply (rel_simp)+
apply blast
apply (rel_simp)+
apply (metis (full_types))
done
subsection {*Try Catch laws*}
(*see utp_hoare_helper*)
end

View File

@ -1,346 +1,346 @@
section "Auxiliary algebraic laws for abrupt designs"
theory algebraic_laws_fault_aux
imports "../../../theories/Fault/utp_fault_designs"
begin
named_theorems uflt_simpl and uflt_cond and uflt_comp and uflt_lens
subsection {*THM setup*}
declare design_condr[urel_cond]
subsection {*abrupt alphabet behavior*}
lemma assigns_flt_alpha:
"(fault :== (\<not> &fault)) = (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault\<acute> =\<^sub>u (\<not>$fault) \<and> $ok =\<^sub>u $ok\<acute>)"
"(ok :== (\<not> &ok)) = (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault\<acute> =\<^sub>u $fault \<and> $ok =\<^sub>u (\<not>$ok\<acute>))"
by rel_auto+
lemma vwb_of_fault[simp]:
"vwb_lens ok" "vwb_lens fault"
by simp_all
lemma unrest_pre_out\<alpha>_flt[unrest]: "out\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
by (transfer, auto simp add: out\<alpha>_def lens_prod_def)
lemma unrest_post_in\<alpha>_flt[unrest]: "in\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>>"
by (transfer, auto simp add: in\<alpha>_def lens_prod_def)
lemma unrest_ok_fault_rel_uexpr_lift_cpf[unrest]:
"$ok \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T" "$ok\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
"$fault \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T" "$fault\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by (pred_auto)+
lemma unrest_ok_fault_rel_usubst_lift_cpf[unrest]:
"$ok\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T" "$ok \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T"
"$fault\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T" "$fault \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T"
by rel_auto+
lemma unrest_in_out_rel_ok_fault_res_flt [unrest]:
"$ok \<sharp> (P \<restriction>\<^sub>\<alpha> ok)" "$ok\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> ok)"
"$fault \<sharp> (P \<restriction>\<^sub>\<alpha> fault)" "$fault\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> fault)"
by (simp_all add: rel_var_res_def unrest)
lemma uflt_alphabet_unrest[unrest]:(*FIXEME:These laws should be generated automatically by alphabet backend since all the fields of alphabet are independant*)
"$ok\<acute> \<sharp> $fault\<acute>" "$ok \<sharp> $fault"
"$ok\<acute> \<sharp> $x" "$ok \<sharp> $fault\<acute>"
"$fault\<acute> \<sharp> $ok\<acute>" "$fault \<sharp> $ok "
"$fault \<sharp> $ok\<acute>" "$fault\<acute> \<sharp> $x"
by pred_simp+
lemma cpf_ord [usubst]:
"$ok \<prec>\<^sub>v $ok\<acute>" "$abrupt \<prec>\<^sub>v $abrupt\<acute>" "$ok \<prec>\<^sub>v $abrupt\<acute>"
"$ok \<prec>\<^sub>v $abrupt" "$ok\<acute> \<prec>\<^sub>v $abrupt\<acute>" "$ok\<acute> \<prec>\<^sub>v $abrupt"
by (simp_all add: var_name_ord_def)
lemma rel_usubst_lift_cpf_in_out_fault_ok[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> $fault = $fault" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$fault) = (\<not>$fault)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> ($ok) = ($ok)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$ok) = (\<not>$ok)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> ($fault\<acute>) = (($fault\<acute>))" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$fault\<acute>) = (\<not>$fault\<acute>)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> ($ok\<acute>) = ($ok\<acute>)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$ok\<acute>) = (\<not>$ok\<acute>)"
by (simp_all add: usubst unrest)
lemma abrupt_ok_simpl[uflt_comp]:
"($fault ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = $fault" "(\<not>$ok ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$ok)"
"($fault ;; (P \<turnstile> Q)) = $fault" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"(\<not>$fault ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$fault)" "(\<not>$ok ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$ok)"
"(\<not>$fault ;; (P \<turnstile> Q)) = (\<not>$fault)" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"($fault\<acute> ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = $fault\<acute>"
"(\<not>$fault\<acute> ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$fault\<acute>)"
by rel_auto+
lemma simpl_flt_in_ok:
"Simpl\<^sub>F\<^sub>L\<^sub>T ($ok) = ((\<not>$fault \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_flt_our_ok:
"Simpl\<^sub>F\<^sub>L\<^sub>T ($ok\<acute>) = ((\<not>$fault \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_flt_in_abrupt:
"Simpl\<^sub>F\<^sub>L\<^sub>T ($fault) = ((\<not>$fault \<and> ($ok \<Rightarrow>($ok\<acute> \<and> $fault))) \<or> ($fault \<and> II))"
by rel_auto
lemma simpl_flt_alt_def:
"Simpl\<^sub>F\<^sub>L\<^sub>T (P) = ((\<not>$fault \<and> ($ok \<Rightarrow>($ok\<acute> \<and> P))) \<or> ($fault \<and> II))"
by rel_auto
subsection {*Healthiness condition behavior*}
lemma rel_usubst_cpf_c3_flt[usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows "\<sigma> \<dagger> C3_flt(P) = (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> (\<not>$fault) \<triangleright> (\<sigma> \<dagger> II))"
using assms unfolding C3_flt_def
by (simp add: usubst)
lemma Simpl_flt_idem[simp]: "Simpl\<^sub>F\<^sub>L\<^sub>T(Simpl\<^sub>F\<^sub>L\<^sub>T(P)) = Simpl\<^sub>F\<^sub>L\<^sub>T(P)"
by (rel_auto)
lemma simpl_flt_Idempotent: "Idempotent Simpl\<^sub>F\<^sub>L\<^sub>T"
by (simp add: Idempotent_def)
lemma Simpl_flt_mono: "P \<sqsubseteq> Q \<Longrightarrow> Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<sqsubseteq> Simpl\<^sub>F\<^sub>L\<^sub>T(Q)"
by (rel_auto)
lemma simpl_flt_Monotonic: "Monotonic Simpl\<^sub>F\<^sub>L\<^sub>T"
by (simp add: Monotonic_def Simpl_flt_mono)
lemma simpl_flt_def:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P) = ((\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> P) \<triangleleft> \<not>$fault \<triangleright> II)"
unfolding C3_flt_def ..
lemma simpl_flt_condr[uflt_simpl]:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P \<triangleleft> b \<triangleright> Q) = (Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<triangleleft> b \<triangleright> Simpl\<^sub>F\<^sub>L\<^sub>T(Q))"
unfolding simpl_flt_def
by (simp add: urel_cond)
lemma simpl_abr_skip_abr[uflt_simpl]:
"Simpl\<^sub>F\<^sub>L\<^sub>T(SKIP\<^sub>F\<^sub>L\<^sub>T) = (SKIP\<^sub>F\<^sub>L\<^sub>T)"
by (simp add: urel_cond urel_defs)
lemma simpl_flt_assign_flt[uflt_simpl]:
"Simpl\<^sub>F\<^sub>L\<^sub>T(\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T) = (\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T)"
by (simp add: urel_cond urel_defs)
lemma simpl_flt_form:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P) = (((\<not>$fault) \<and> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (P))) \<or> ($fault \<and> II))"
by rel_auto
lemma abrupt_simpl_flt[uflt_simpl]:
"($fault \<and> Simpl\<^sub>F\<^sub>L\<^sub>T(P)) = ($fault \<and>II)"
by rel_auto
lemma nabrupt_simpl_flt[uflt_simpl]:
"(\<not>$fault \<and> Simpl\<^sub>F\<^sub>L\<^sub>T(P)) = (\<not>$fault \<and> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (P)))"
by (rel_auto)
definition design_flt_sup :: "('\<alpha>,'\<beta>) rel_cpf set \<Rightarrow> ('\<alpha>,'\<beta>) rel_cpf" ("\<Sqinter>\<^sub>F\<^sub>L\<^sub>T_" [900] 900) where
"\<Sqinter>\<^sub>F\<^sub>L\<^sub>T A = (if (A = {}) then \<top>\<^sub>F\<^sub>L\<^sub>T else \<Sqinter> A)"
lemma simpl_flt_Continuous: "Continuous Simpl\<^sub>F\<^sub>L\<^sub>T"
unfolding Continuous_def SUP_def apply rel_simp
unfolding SUP_def
apply transfer apply auto
done
lemma simpl_flt_R3_conj:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P \<and> Q) = (Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<and> Simpl\<^sub>F\<^sub>L\<^sub>T(Q))"
by (rel_auto)
lemma simpl_flt_disj:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P \<or> Q) = (Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<or> Simpl\<^sub>F\<^sub>L\<^sub>T(Q))"
by (rel_auto)
lemma Simpl_flt_USUP:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>F\<^sub>L\<^sub>T(\<Sqinter> i \<in> A \<bullet> P(i)) = (\<Sqinter> i \<in> A \<bullet> Simpl\<^sub>F\<^sub>L\<^sub>T(P(i)))"
using assms by (rel_auto)
lemma design_flt_sup_non_empty [simp]:
"A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^sub>F\<^sub>L\<^sub>T A = \<Sqinter> A"
by (simp add: design_flt_sup_def)
subsection {*Signature behavior*}
lemma design_top_flt:
"(P \<turnstile> Q) \<sqsubseteq> \<top>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
lemma design_flt_sup_empty [simp]:
"\<Sqinter>\<^sub>F\<^sub>L\<^sub>T {} = \<top>\<^sub>F\<^sub>L\<^sub>T"
by (simp add: design_flt_sup_def)
abbreviation design_inf :: "('\<alpha>, '\<beta>) rel_des set \<Rightarrow> ('\<alpha>, '\<beta>) rel_des" ("\<Squnion>\<^sub>F\<^sub>L\<^sub>T_" [900] 900) where
"\<Squnion>\<^sub>F\<^sub>L\<^sub>T A \<equiv> \<Squnion> A"
lemma design_bottom_flt:
"\<bottom>\<^sub>F\<^sub>L\<^sub>T \<sqsubseteq> (P \<turnstile> Q)"
by simp
lemma Simpl_flt_UINF:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>F\<^sub>L\<^sub>T(\<Squnion> i \<in> A \<bullet> P(i)) = (\<Squnion> i \<in> A \<bullet> Simpl\<^sub>F\<^sub>L\<^sub>T(P(i)))"
using assms by (rel_auto)
lemma skip_cpf_def:
"II = (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault =\<^sub>u $fault\<acute> \<and> $ok =\<^sub>u $ok\<acute>)"
by rel_auto
lemma skip_lift_flt_def:
"\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T = ($\<Sigma>\<^sub>F\<^sub>L\<^sub>T\<acute> =\<^sub>u $\<Sigma>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma seqr_fault_true [usubst]:
"(P ;; Q) \<^sub>f\<^sub>t = (P \<^sub>f\<^sub>t ;; Q)"
by (rel_auto)
lemma seqr_fault_false [usubst]:
"(P ;; Q) \<^sub>f\<^sub>f = (P \<^sub>f\<^sub>f ;; Q)"
by (rel_auto)
lemma rel_usubst_lift_cpf_uexpr_lift_cpf[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>\<sigma> \<dagger> P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma usubst_lift_cpf_assigns_lift_cpf [usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>\<langle>\<rho> \<circ> \<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by (simp add: usubst)
lemma usubst_lift_cpf_pre_uexpr_lift_cpf[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>< = \<lceil>\<sigma> \<dagger> b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
by (simp add: usubst)
lemma rel_usubst_lift_cpf_design[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (Q \<turnstile> P)) = (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> Q) \<turnstile> (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> P)"
by (simp add: usubst unrest)
lemma usubst_cpf_true[usubst]:
"\<sigma> \<dagger> \<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma usubst_cpf_false[usubst]:
"\<sigma> \<dagger> \<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma rel_usubst_cpf_skip_cpf[usubst]:
"(\<sigma> \<dagger> II) = ((\<sigma> \<dagger> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T) \<and> \<sigma> \<dagger> $fault =\<^sub>u \<sigma> \<dagger> $fault\<acute> \<and> \<sigma> \<dagger> $ok =\<^sub>u \<sigma> \<dagger> $ok\<acute>)"
by (simp add: usubst unrest skip_cpf_def)
lemma usubst_lift_cpf_skip_lift_cpf[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T) = \<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T"
unfolding skip_r_def
by (simp add: usubst_lift_cpf_assigns_lift_cpf)
lemma usubst_cpf_skip_cpf [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"(\<sigma> \<dagger> SKIP\<^sub>F\<^sub>L\<^sub>T) = (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<sigma> \<dagger> (\<not>$fault\<acute> \<and> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T)) \<triangleleft> \<sigma> \<dagger> (\<not>$fault) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding skip_flt_def
by (simp add: usubst)
lemma usubst_cpf_assigns_cpf [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"\<sigma> \<dagger> \<langle>\<rho>\<rangle>\<^sub>F\<^sub>L\<^sub>T = (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<sigma> \<dagger> ((\<not>$fault\<acute>) \<and> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T)) \<triangleleft> \<sigma> \<dagger> (\<not>$fault) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding assigns_flt_def
by (simp add: usubst)
lemma c3_flt_comp_left_distr:
"(C3_flt (P) ;; R) = ((P;;R) \<triangleleft> \<not>$fault \<triangleright> (II ;; R))"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma c3_flt_comp_semir:
"(C3_flt(P) ;; C3_flt(R)) = C3_flt (P ;; C3_flt(R))"
by rel_auto
lemma c3_flt_comp_simpl[uflt_comp]:
"(C3_flt(P) ;; C3_flt(R)) = ((P ;; C3_flt(R)) \<triangleleft> \<not>$fault \<triangleright> (II))"
by rel_auto
lemma simpl_flt_comp_semir:
"(Simpl\<^sub>F\<^sub>L\<^sub>T(P) ;; Simpl\<^sub>F\<^sub>L\<^sub>T(R)) = Simpl\<^sub>F\<^sub>L\<^sub>T ((\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> P) ;; Simpl\<^sub>F\<^sub>L\<^sub>T(R))"
by rel_auto
theorem design_top_flt_left_zero[uflt_comp]:
"(\<top>\<^sub>F\<^sub>L\<^sub>T ;; (P \<turnstile> Q)) = \<top>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
theorem Simpl_flt_top_flt_left_zero[uflt_comp]:
"(\<top>\<^sub>F\<^sub>L\<^sub>T ;; Simpl\<^sub>F\<^sub>L\<^sub>T (P)) = \<top>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
lemma assigns_lift_cpf_comp_rel_cpf[uflt_comp]:
assumes "$ok \<sharp> P" "$fault \<sharp> P"
shows "(\<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T ;; P) = (\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> P)"
apply (insert assms)
apply pred_simp
apply rel_blast
done
lemma lift_des_skip_dr_unit_flt [uflt_comp]:
"(\<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T ;; \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T) = \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
"(\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T ;; \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T) = \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)+
lemma skip_cpf_left_comp_simpl[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; Simpl\<^sub>F\<^sub>L\<^sub>T(R)) = (Simpl\<^sub>F\<^sub>L\<^sub>T(R))"
by rel_auto
lemma skip_cpf_right_comp_simpl[uflt_comp]:
"(Simpl\<^sub>F\<^sub>L\<^sub>T(R) ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = (Simpl\<^sub>F\<^sub>L\<^sub>T(R))"
by rel_auto
lemma assign_flt_alt_def:
"\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T = Simpl\<^sub>F\<^sub>L\<^sub>T (\<not>$fault\<acute> \<and> \<lceil>\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> II\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma assign_flt_left_comp_c3[uflt_comp]:
"\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T ;; C3_flt (P \<turnstile> Q) = C3_flt (\<lceil>a\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> (P \<turnstile> Q))"
by rel_auto
lemma assigns_flt_comp[uflt_comp]:
"(\<langle>f\<rangle>\<^sub>F\<^sub>L\<^sub>T ;; \<langle>g\<rangle>\<^sub>F\<^sub>L\<^sub>T) = \<langle>g \<circ> f\<rangle>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma usubst_cpf_des_cond_flt [usubst]:
"\<lbrakk>$ok \<sharp> \<sigma>; $ok\<acute> \<sharp> \<sigma> \<rbrakk> \<Longrightarrow>
\<sigma> \<dagger> (R \<turnstile> bif b then P else Q eif) =
(\<sigma> \<dagger> R \<turnstile> (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>< \<triangleright> \<sigma> \<dagger> Q))"
by (simp add: usubst)
lemma comp_cond_flt_left_distr[uflt_comp]:
"((bif b then Simpl\<^sub>F\<^sub>L\<^sub>T P else Simpl\<^sub>F\<^sub>L\<^sub>T Q eif) ;; Simpl\<^sub>F\<^sub>L\<^sub>T R) =
(bif b then (Simpl\<^sub>F\<^sub>L\<^sub>T P ;; Simpl\<^sub>F\<^sub>L\<^sub>T R) else (Simpl\<^sub>F\<^sub>L\<^sub>T Q ;; Simpl\<^sub>F\<^sub>L\<^sub>T R) eif)"
apply pred_simp
apply rel_simp
done
lemma if_mono:
"\<lbrakk> P\<^sub>1 \<sqsubseteq> P\<^sub>2; Q\<^sub>1 \<sqsubseteq> Q\<^sub>2 \<rbrakk> \<Longrightarrow> (bif b then P\<^sub>1 else Q\<^sub>1 eif) \<sqsubseteq> (bif b then P\<^sub>2 else Q\<^sub>2 eif)"
by rel_auto
lemma design_post_seqr_rcond_left_not_ivar[urel_cond]:
"S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>) ;; P \<triangleleft> \<not> $x \<triangleright> Q) =
S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>);; Q)"
apply pred_simp
apply fastforce
done
lemma design_post_seqr_rcond_left_ivar [urel_cond]:
"S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>) ;; P \<triangleleft> $x \<triangleright> Q) =
S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>);; P)"
apply pred_simp
apply fastforce
done
subsection {*While abrupt usubst*}
subsection {*block abrupt usubst*}
subsection {*Catch abrupt usubst*}
section "Auxiliary algebraic laws for abrupt designs"
theory algebraic_laws_fault_aux
imports "../../../theories/Fault/utp_fault_designs"
begin
named_theorems uflt_simpl and uflt_cond and uflt_comp and uflt_lens
subsection {*THM setup*}
declare design_condr[urel_cond]
subsection {*abrupt alphabet behavior*}
lemma assigns_flt_alpha:
"(fault :== (\<not> &fault)) = (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault\<acute> =\<^sub>u (\<not>$fault) \<and> $ok =\<^sub>u $ok\<acute>)"
"(ok :== (\<not> &ok)) = (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault\<acute> =\<^sub>u $fault \<and> $ok =\<^sub>u (\<not>$ok\<acute>))"
by rel_auto+
lemma vwb_of_fault[simp]:
"vwb_lens ok" "vwb_lens fault"
by simp_all
lemma unrest_pre_out\<alpha>_flt[unrest]: "out\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
by (transfer, auto simp add: out\<alpha>_def lens_prod_def)
lemma unrest_post_in\<alpha>_flt[unrest]: "in\<alpha> \<sharp> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>>"
by (transfer, auto simp add: in\<alpha>_def lens_prod_def)
lemma unrest_ok_fault_rel_uexpr_lift_cpf[unrest]:
"$ok \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T" "$ok\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
"$fault \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T" "$fault\<acute> \<sharp> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by (pred_auto)+
lemma unrest_ok_fault_rel_usubst_lift_cpf[unrest]:
"$ok\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T" "$ok \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T"
"$fault\<acute> \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T" "$fault \<sharp> \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T"
by rel_auto+
lemma unrest_in_out_rel_ok_fault_res_flt [unrest]:
"$ok \<sharp> (P \<restriction>\<^sub>\<alpha> ok)" "$ok\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> ok)"
"$fault \<sharp> (P \<restriction>\<^sub>\<alpha> fault)" "$fault\<acute> \<sharp> (P \<restriction>\<^sub>\<alpha> fault)"
by (simp_all add: rel_var_res_def unrest)
lemma uflt_alphabet_unrest[unrest]:(*FIXEME:These laws should be generated automatically by alphabet backend since all the fields of alphabet are independant*)
"$ok\<acute> \<sharp> $fault\<acute>" "$ok \<sharp> $fault"
"$ok\<acute> \<sharp> $x" "$ok \<sharp> $fault\<acute>"
"$fault\<acute> \<sharp> $ok\<acute>" "$fault \<sharp> $ok "
"$fault \<sharp> $ok\<acute>" "$fault\<acute> \<sharp> $x"
by pred_simp+
lemma cpf_ord [usubst]:
"$ok \<prec>\<^sub>v $ok\<acute>" "$abrupt \<prec>\<^sub>v $abrupt\<acute>" "$ok \<prec>\<^sub>v $abrupt\<acute>"
"$ok \<prec>\<^sub>v $abrupt" "$ok\<acute> \<prec>\<^sub>v $abrupt\<acute>" "$ok\<acute> \<prec>\<^sub>v $abrupt"
by (simp_all add: var_name_ord_def)
lemma rel_usubst_lift_cpf_in_out_fault_ok[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> $fault = $fault" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$fault) = (\<not>$fault)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> ($ok) = ($ok)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$ok) = (\<not>$ok)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> ($fault\<acute>) = (($fault\<acute>))" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$fault\<acute>) = (\<not>$fault\<acute>)"
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> ($ok\<acute>) = ($ok\<acute>)" "\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (\<not>$ok\<acute>) = (\<not>$ok\<acute>)"
by (simp_all add: usubst unrest)
lemma abrupt_ok_simpl[uflt_comp]:
"($fault ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = $fault" "(\<not>$ok ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$ok)"
"($fault ;; (P \<turnstile> Q)) = $fault" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"(\<not>$fault ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$fault)" "(\<not>$ok ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$ok)"
"(\<not>$fault ;; (P \<turnstile> Q)) = (\<not>$fault)" "(\<not>$ok ;; (P \<turnstile> Q)) = (\<not>$ok)"
"($fault\<acute> ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = $fault\<acute>"
"(\<not>$fault\<acute> ;; Simpl\<^sub>F\<^sub>L\<^sub>T P) = (\<not>$fault\<acute>)"
by rel_auto+
lemma simpl_flt_in_ok:
"Simpl\<^sub>F\<^sub>L\<^sub>T ($ok) = ((\<not>$fault \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_flt_our_ok:
"Simpl\<^sub>F\<^sub>L\<^sub>T ($ok\<acute>) = ((\<not>$fault \<and> ($ok \<Rightarrow>$ok\<acute>)) \<or> (II))"
by rel_auto
lemma simpl_flt_in_abrupt:
"Simpl\<^sub>F\<^sub>L\<^sub>T ($fault) = ((\<not>$fault \<and> ($ok \<Rightarrow>($ok\<acute> \<and> $fault))) \<or> ($fault \<and> II))"
by rel_auto
lemma simpl_flt_alt_def:
"Simpl\<^sub>F\<^sub>L\<^sub>T (P) = ((\<not>$fault \<and> ($ok \<Rightarrow>($ok\<acute> \<and> P))) \<or> ($fault \<and> II))"
by rel_auto
subsection {*Healthiness condition behavior*}
lemma rel_usubst_cpf_c3_flt[usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows "\<sigma> \<dagger> C3_flt(P) = (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> (\<not>$fault) \<triangleright> (\<sigma> \<dagger> II))"
using assms unfolding C3_flt_def
by (simp add: usubst)
lemma Simpl_flt_idem[simp]: "Simpl\<^sub>F\<^sub>L\<^sub>T(Simpl\<^sub>F\<^sub>L\<^sub>T(P)) = Simpl\<^sub>F\<^sub>L\<^sub>T(P)"
by (rel_auto)
lemma simpl_flt_Idempotent: "Idempotent Simpl\<^sub>F\<^sub>L\<^sub>T"
by (simp add: Idempotent_def)
lemma Simpl_flt_mono: "P \<sqsubseteq> Q \<Longrightarrow> Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<sqsubseteq> Simpl\<^sub>F\<^sub>L\<^sub>T(Q)"
by (rel_auto)
lemma simpl_flt_Monotonic: "Monotonic Simpl\<^sub>F\<^sub>L\<^sub>T"
by (simp add: Monotonic_def Simpl_flt_mono)
lemma simpl_flt_def:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P) = ((\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> P) \<triangleleft> \<not>$fault \<triangleright> II)"
unfolding C3_flt_def ..
lemma simpl_flt_condr[uflt_simpl]:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P \<triangleleft> b \<triangleright> Q) = (Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<triangleleft> b \<triangleright> Simpl\<^sub>F\<^sub>L\<^sub>T(Q))"
unfolding simpl_flt_def
by (simp add: urel_cond)
lemma simpl_abr_skip_abr[uflt_simpl]:
"Simpl\<^sub>F\<^sub>L\<^sub>T(SKIP\<^sub>F\<^sub>L\<^sub>T) = (SKIP\<^sub>F\<^sub>L\<^sub>T)"
by (simp add: urel_cond urel_defs)
lemma simpl_flt_assign_flt[uflt_simpl]:
"Simpl\<^sub>F\<^sub>L\<^sub>T(\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T) = (\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T)"
by (simp add: urel_cond urel_defs)
lemma simpl_flt_form:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P) = (((\<not>$fault) \<and> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (P))) \<or> ($fault \<and> II))"
by rel_auto
lemma abrupt_simpl_flt[uflt_simpl]:
"($fault \<and> Simpl\<^sub>F\<^sub>L\<^sub>T(P)) = ($fault \<and>II)"
by rel_auto
lemma nabrupt_simpl_flt[uflt_simpl]:
"(\<not>$fault \<and> Simpl\<^sub>F\<^sub>L\<^sub>T(P)) = (\<not>$fault \<and> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (P)))"
by (rel_auto)
definition design_flt_sup :: "('\<alpha>,'\<beta>) rel_cpf set \<Rightarrow> ('\<alpha>,'\<beta>) rel_cpf" ("\<Sqinter>\<^sub>F\<^sub>L\<^sub>T_" [900] 900) where
"\<Sqinter>\<^sub>F\<^sub>L\<^sub>T A = (if (A = {}) then \<top>\<^sub>F\<^sub>L\<^sub>T else \<Sqinter> A)"
lemma simpl_flt_Continuous: "Continuous Simpl\<^sub>F\<^sub>L\<^sub>T"
unfolding Continuous_def SUP_def apply rel_simp
unfolding SUP_def
apply transfer apply auto
done
lemma simpl_flt_R3_conj:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P \<and> Q) = (Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<and> Simpl\<^sub>F\<^sub>L\<^sub>T(Q))"
by (rel_auto)
lemma simpl_flt_disj:
"Simpl\<^sub>F\<^sub>L\<^sub>T(P \<or> Q) = (Simpl\<^sub>F\<^sub>L\<^sub>T(P) \<or> Simpl\<^sub>F\<^sub>L\<^sub>T(Q))"
by (rel_auto)
lemma Simpl_flt_USUP:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>F\<^sub>L\<^sub>T(\<Sqinter> i \<in> A \<bullet> P(i)) = (\<Sqinter> i \<in> A \<bullet> Simpl\<^sub>F\<^sub>L\<^sub>T(P(i)))"
using assms by (rel_auto)
lemma design_flt_sup_non_empty [simp]:
"A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^sub>F\<^sub>L\<^sub>T A = \<Sqinter> A"
by (simp add: design_flt_sup_def)
subsection {*Signature behavior*}
lemma design_top_flt:
"(P \<turnstile> Q) \<sqsubseteq> \<top>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
lemma design_flt_sup_empty [simp]:
"\<Sqinter>\<^sub>F\<^sub>L\<^sub>T {} = \<top>\<^sub>F\<^sub>L\<^sub>T"
by (simp add: design_flt_sup_def)
abbreviation design_inf :: "('\<alpha>, '\<beta>) rel_des set \<Rightarrow> ('\<alpha>, '\<beta>) rel_des" ("\<Squnion>\<^sub>F\<^sub>L\<^sub>T_" [900] 900) where
"\<Squnion>\<^sub>F\<^sub>L\<^sub>T A \<equiv> \<Squnion> A"
lemma design_bottom_flt:
"\<bottom>\<^sub>F\<^sub>L\<^sub>T \<sqsubseteq> (P \<turnstile> Q)"
by simp
lemma Simpl_flt_UINF:
assumes "A \<noteq> {}"
shows "Simpl\<^sub>F\<^sub>L\<^sub>T(\<Squnion> i \<in> A \<bullet> P(i)) = (\<Squnion> i \<in> A \<bullet> Simpl\<^sub>F\<^sub>L\<^sub>T(P(i)))"
using assms by (rel_auto)
lemma skip_cpf_def:
"II = (\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $fault =\<^sub>u $fault\<acute> \<and> $ok =\<^sub>u $ok\<acute>)"
by rel_auto
lemma skip_lift_flt_def:
"\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T = ($\<Sigma>\<^sub>F\<^sub>L\<^sub>T\<acute> =\<^sub>u $\<Sigma>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma seqr_fault_true [usubst]:
"(P ;; Q) \<^sub>f\<^sub>t = (P \<^sub>f\<^sub>t ;; Q)"
by (rel_auto)
lemma seqr_fault_false [usubst]:
"(P ;; Q) \<^sub>f\<^sub>f = (P \<^sub>f\<^sub>f ;; Q)"
by (rel_auto)
lemma rel_usubst_lift_cpf_uexpr_lift_cpf[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>\<sigma> \<dagger> P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma usubst_lift_cpf_assigns_lift_cpf [usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>\<langle>\<rho> \<circ> \<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by (simp add: usubst)
lemma usubst_lift_cpf_pre_uexpr_lift_cpf[usubst]:
"\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>< = \<lceil>\<sigma> \<dagger> b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub><"
by (simp add: usubst)
lemma rel_usubst_lift_cpf_design[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> (Q \<turnstile> P)) = (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> Q) \<turnstile> (\<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>F\<^sub>L\<^sub>T \<dagger> P)"
by (simp add: usubst unrest)
lemma usubst_cpf_true[usubst]:
"\<sigma> \<dagger> \<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma usubst_cpf_false[usubst]:
"\<sigma> \<dagger> \<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T = \<lceil>false\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma rel_usubst_cpf_skip_cpf[usubst]:
"(\<sigma> \<dagger> II) = ((\<sigma> \<dagger> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T) \<and> \<sigma> \<dagger> $fault =\<^sub>u \<sigma> \<dagger> $fault\<acute> \<and> \<sigma> \<dagger> $ok =\<^sub>u \<sigma> \<dagger> $ok\<acute>)"
by (simp add: usubst unrest skip_cpf_def)
lemma usubst_lift_cpf_skip_lift_cpf[usubst]:
"(\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T) = \<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T"
unfolding skip_r_def
by (simp add: usubst_lift_cpf_assigns_lift_cpf)
lemma usubst_cpf_skip_cpf [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"(\<sigma> \<dagger> SKIP\<^sub>F\<^sub>L\<^sub>T) = (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<sigma> \<dagger> (\<not>$fault\<acute> \<and> \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T)) \<triangleleft> \<sigma> \<dagger> (\<not>$fault) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding skip_flt_def
by (simp add: usubst)
lemma usubst_cpf_assigns_cpf [usubst]:
assumes "$ok \<sharp> \<sigma>" "$ok\<acute> \<sharp> \<sigma> "
shows
"\<sigma> \<dagger> \<langle>\<rho>\<rangle>\<^sub>F\<^sub>L\<^sub>T = (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<sigma> \<dagger> ((\<not>$fault\<acute>) \<and> \<lceil>\<langle>\<rho>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T)) \<triangleleft> \<sigma> \<dagger> (\<not>$fault) \<triangleright> (\<sigma> \<dagger> (II)))"
using assms unfolding assigns_flt_def
by (simp add: usubst)
lemma c3_flt_comp_left_distr:
"(C3_flt (P) ;; R) = ((P;;R) \<triangleleft> \<not>$fault \<triangleright> (II ;; R))"
apply pred_simp
apply rel_simp
apply fastforce
done
lemma c3_flt_comp_semir:
"(C3_flt(P) ;; C3_flt(R)) = C3_flt (P ;; C3_flt(R))"
by rel_auto
lemma c3_flt_comp_simpl[uflt_comp]:
"(C3_flt(P) ;; C3_flt(R)) = ((P ;; C3_flt(R)) \<triangleleft> \<not>$fault \<triangleright> (II))"
by rel_auto
lemma simpl_flt_comp_semir:
"(Simpl\<^sub>F\<^sub>L\<^sub>T(P) ;; Simpl\<^sub>F\<^sub>L\<^sub>T(R)) = Simpl\<^sub>F\<^sub>L\<^sub>T ((\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> P) ;; Simpl\<^sub>F\<^sub>L\<^sub>T(R))"
by rel_auto
theorem design_top_flt_left_zero[uflt_comp]:
"(\<top>\<^sub>F\<^sub>L\<^sub>T ;; (P \<turnstile> Q)) = \<top>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
theorem Simpl_flt_top_flt_left_zero[uflt_comp]:
"(\<top>\<^sub>F\<^sub>L\<^sub>T ;; Simpl\<^sub>F\<^sub>L\<^sub>T (P)) = \<top>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)
lemma assigns_lift_cpf_comp_rel_cpf[uflt_comp]:
assumes "$ok \<sharp> P" "$fault \<sharp> P"
shows "(\<lceil>\<langle>\<sigma>\<rangle>\<^sub>a\<rceil>\<^sub>F\<^sub>L\<^sub>T ;; P) = (\<lceil>\<sigma>\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> P)"
apply (insert assms)
apply pred_simp
apply rel_blast
done
lemma lift_des_skip_dr_unit_flt [uflt_comp]:
"(\<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T ;; \<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T) = \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
"(\<lceil>II\<rceil>\<^sub>F\<^sub>L\<^sub>T ;; \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T) = \<lceil>P\<rceil>\<^sub>F\<^sub>L\<^sub>T"
by (rel_auto)+
lemma skip_cpf_left_comp_simpl[uflt_comp]:
"(SKIP\<^sub>F\<^sub>L\<^sub>T ;; Simpl\<^sub>F\<^sub>L\<^sub>T(R)) = (Simpl\<^sub>F\<^sub>L\<^sub>T(R))"
by rel_auto
lemma skip_cpf_right_comp_simpl[uflt_comp]:
"(Simpl\<^sub>F\<^sub>L\<^sub>T(R) ;; SKIP\<^sub>F\<^sub>L\<^sub>T) = (Simpl\<^sub>F\<^sub>L\<^sub>T(R))"
by rel_auto
lemma assign_flt_alt_def:
"\<langle>\<sigma>\<rangle>\<^sub>F\<^sub>L\<^sub>T = Simpl\<^sub>F\<^sub>L\<^sub>T (\<not>$fault\<acute> \<and> \<lceil>\<lceil>\<sigma>\<rceil>\<^sub>s \<dagger> II\<rceil>\<^sub>F\<^sub>L\<^sub>T)"
by rel_auto
lemma assign_flt_left_comp_c3[uflt_comp]:
"\<langle>a\<rangle>\<^sub>F\<^sub>L\<^sub>T ;; C3_flt (P \<turnstile> Q) = C3_flt (\<lceil>a\<rceil>\<^sub>s\<^sub>F\<^sub>L\<^sub>T \<dagger> (P \<turnstile> Q))"
by rel_auto
lemma assigns_flt_comp[uflt_comp]:
"(\<langle>f\<rangle>\<^sub>F\<^sub>L\<^sub>T ;; \<langle>g\<rangle>\<^sub>F\<^sub>L\<^sub>T) = \<langle>g \<circ> f\<rangle>\<^sub>F\<^sub>L\<^sub>T"
by rel_auto
lemma usubst_cpf_des_cond_flt [usubst]:
"\<lbrakk>$ok \<sharp> \<sigma>; $ok\<acute> \<sharp> \<sigma> \<rbrakk> \<Longrightarrow>
\<sigma> \<dagger> (R \<turnstile> bif b then P else Q eif) =
(\<sigma> \<dagger> R \<turnstile> (\<sigma> \<dagger> P \<triangleleft> \<sigma> \<dagger> \<lceil>b\<rceil>\<^sub>F\<^sub>L\<^sub>T\<^sub>< \<triangleright> \<sigma> \<dagger> Q))"
by (simp add: usubst)
lemma comp_cond_flt_left_distr[uflt_comp]:
"((bif b then Simpl\<^sub>F\<^sub>L\<^sub>T P else Simpl\<^sub>F\<^sub>L\<^sub>T Q eif) ;; Simpl\<^sub>F\<^sub>L\<^sub>T R) =
(bif b then (Simpl\<^sub>F\<^sub>L\<^sub>T P ;; Simpl\<^sub>F\<^sub>L\<^sub>T R) else (Simpl\<^sub>F\<^sub>L\<^sub>T Q ;; Simpl\<^sub>F\<^sub>L\<^sub>T R) eif)"
apply pred_simp
apply rel_simp
done
lemma if_mono:
"\<lbrakk> P\<^sub>1 \<sqsubseteq> P\<^sub>2; Q\<^sub>1 \<sqsubseteq> Q\<^sub>2 \<rbrakk> \<Longrightarrow> (bif b then P\<^sub>1 else Q\<^sub>1 eif) \<sqsubseteq> (bif b then P\<^sub>2 else Q\<^sub>2 eif)"
by rel_auto
lemma design_post_seqr_rcond_left_not_ivar[urel_cond]:
"S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>) ;; P \<triangleleft> \<not> $x \<triangleright> Q) =
S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>);; Q)"
apply pred_simp
apply fastforce
done
lemma design_post_seqr_rcond_left_ivar [urel_cond]:
"S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>) ;; P \<triangleleft> $x \<triangleright> Q) =
S \<turnstile> (\<lceil>true\<rceil>\<^sub>F\<^sub>L\<^sub>T \<turnstile> (\<lceil>R\<rceil>\<^sub>F\<^sub>L\<^sub>T \<and> $x\<acute>);; P)"
apply pred_simp
apply fastforce
done
subsection {*While abrupt usubst*}
subsection {*block abrupt usubst*}
subsection {*Catch abrupt usubst*}
end

View File

@ -1,12 +1,12 @@
session "orca-model" = "HOL" +
description {*Shallow embedded orca*}
options [quick_and_dirty, document = pdf, document_output = "."]
theories
"features_test"
"theories/utp_fault_designs"
files "document/root.tex"
session "orca-model" = "HOL" +
description {*Shallow embedded orca*}
options [quick_and_dirty, document = pdf, document_output = "."]
theories
"features_test"
"theories/utp_fault_designs"
files "document/root.tex"

View File

@ -1,5 +1,5 @@
Orca is a programming language and a verifier based on Isabelle/UTP.
For more details on Isabelle/UTP see:
https://www-users.cs.york.ac.uk/~simonf/utp-isabelle/
Orca is a programming language and a verifier based on Isabelle/UTP.
For more details on Isabelle/UTP see:
https://www-users.cs.york.ac.uk/~simonf/utp-isabelle/

View File

@ -1,13 +1,13 @@
For the purposes of the license agreement in the file LICENSE, a
'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
who is listed as an author in one of the source files of this Isabelle
distribution.
Contributors to Orca
--------------------
* Yakoub Nemouchi, Virginia Tech, USA
* Peter Lammich, Virginia Tech, USA
Technische Universität München, Germany
* Simon Foster, University of York, UK
* Burkhart Wolff, LRI, Univ. Paris-Sud, CNRS, CentraleSupélec, Université Paris-Saclay, France
* Frédéric Tuong, Virginia Tech, USA
For the purposes of the license agreement in the file LICENSE, a
'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
who is listed as an author in one of the source files of this Isabelle
distribution.
Contributors to Orca
--------------------
* Yakoub Nemouchi, Virginia Tech, USA
* Peter Lammich, Virginia Tech, USA
Technische Universität München, Germany
* Simon Foster, University of York, UK
* Burkhart Wolff, LRI, Univ. Paris-Sud, CNRS, CentraleSupélec, Université Paris-Saclay, France
* Frédéric Tuong, Virginia Tech, USA

328
LICENSE
View File

@ -1,165 +1,165 @@
GNU LESSER GENERAL PUBLIC LICENSE
Version 3, 29 June 2007
Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
Everyone is permitted to copy and distribute verbatim copies
of this license document, but changing it is not allowed.
This version of the GNU Lesser General Public License incorporates
the terms and conditions of version 3 of the GNU General Public
License, supplemented by the additional permissions listed below.
0. Additional Definitions.
As used herein, "this License" refers to version 3 of the GNU Lesser
General Public License, and the "GNU GPL" refers to version 3 of the GNU
General Public License.
"The Library" refers to a covered work governed by this License,
other than an Application or a Combined Work as defined below.
An "Application" is any work that makes use of an interface provided
by the Library, but which is not otherwise based on the Library.
Defining a subclass of a class defined by the Library is deemed a mode
of using an interface provided by the Library.
A "Combined Work" is a work produced by combining or linking an
Application with the Library. The particular version of the Library
with which the Combined Work was made is also called the "Linked
Version".
The "Minimal Corresponding Source" for a Combined Work means the
Corresponding Source for the Combined Work, excluding any source code
for portions of the Combined Work that, considered in isolation, are
based on the Application, and not on the Linked Version.
The "Corresponding Application Code" for a Combined Work means the
object code and/or source code for the Application, including any data
and utility programs needed for reproducing the Combined Work from the
Application, but excluding the System Libraries of the Combined Work.
1. Exception to Section 3 of the GNU GPL.
You may convey a covered work under sections 3 and 4 of this License
without being bound by section 3 of the GNU GPL.
2. Conveying Modified Versions.
If you modify a copy of the Library, and, in your modifications, a
facility refers to a function or data to be supplied by an Application
that uses the facility (other than as an argument passed when the
facility is invoked), then you may convey a copy of the modified
version:
a) under this License, provided that you make a good faith effort to
ensure that, in the event an Application does not supply the
function or data, the facility still operates, and performs
whatever part of its purpose remains meaningful, or
b) under the GNU GPL, with none of the additional permissions of
this License applicable to that copy.
3. Object Code Incorporating Material from Library Header Files.
The object code form of an Application may incorporate material from
a header file that is part of the Library. You may convey such object
code under terms of your choice, provided that, if the incorporated
material is not limited to numerical parameters, data structure
layouts and accessors, or small macros, inline functions and templates
(ten or fewer lines in length), you do both of the following:
a) Give prominent notice with each copy of the object code that the
Library is used in it and that the Library and its use are
covered by this License.
b) Accompany the object code with a copy of the GNU GPL and this license
document.
4. Combined Works.
You may convey a Combined Work under terms of your choice that,
taken together, effectively do not restrict modification of the
portions of the Library contained in the Combined Work and reverse
engineering for debugging such modifications, if you also do each of
the following:
a) Give prominent notice with each copy of the Combined Work that
the Library is used in it and that the Library and its use are
covered by this License.
b) Accompany the Combined Work with a copy of the GNU GPL and this license
document.
c) For a Combined Work that displays copyright notices during
execution, include the copyright notice for the Library among
these notices, as well as a reference directing the user to the
copies of the GNU GPL and this license document.
d) Do one of the following:
0) Convey the Minimal Corresponding Source under the terms of this
License, and the Corresponding Application Code in a form
suitable for, and under terms that permit, the user to
recombine or relink the Application with a modified version of
the Linked Version to produce a modified Combined Work, in the
manner specified by section 6 of the GNU GPL for conveying
Corresponding Source.
1) Use a suitable shared library mechanism for linking with the
Library. A suitable mechanism is one that (a) uses at run time
a copy of the Library already present on the user's computer
system, and (b) will operate properly with a modified version
of the Library that is interface-compatible with the Linked
Version.
e) Provide Installation Information, but only if you would otherwise
be required to provide such information under section 6 of the
GNU GPL, and only to the extent that such information is
necessary to install and execute a modified version of the
Combined Work produced by recombining or relinking the
Application with a modified version of the Linked Version. (If
you use option 4d0, the Installation Information must accompany
the Minimal Corresponding Source and Corresponding Application
Code. If you use option 4d1, you must provide the Installation
Information in the manner specified by section 6 of the GNU GPL
for conveying Corresponding Source.)
5. Combined Libraries.
You may place library facilities that are a work based on the
Library side by side in a single library together with other library
facilities that are not Applications and are not covered by this
License, and convey such a combined library under terms of your
choice, if you do both of the following:
a) Accompany the combined library with a copy of the same work based
on the Library, uncombined with any other library facilities,
conveyed under the terms of this License.
b) Give prominent notice with the combined library that part of it
is a work based on the Library, and explaining where to find the
accompanying uncombined form of the same work.
6. Revised Versions of the GNU Lesser General Public License.
The Free Software Foundation may publish revised and/or new versions
of the GNU Lesser General Public License from time to time. Such new
versions will be similar in spirit to the present version, but may
differ in detail to address new problems or concerns.
Each version is given a distinguishing version number. If the
Library as you received it specifies that a certain numbered version
of the GNU Lesser General Public License "or any later version"
applies to it, you have the option of following the terms and
conditions either of that published version or of any later version
published by the Free Software Foundation. If the Library as you
received it does not specify a version number of the GNU Lesser
General Public License, you may choose any version of the GNU Lesser
General Public License ever published by the Free Software Foundation.
If the Library as you received it specifies that a proxy can decide
whether future versions of the GNU Lesser General Public License shall
apply, that proxy's public statement of acceptance of any version is
permanent authorization for you to choose that version for the
GNU LESSER GENERAL PUBLIC LICENSE
Version 3, 29 June 2007
Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
Everyone is permitted to copy and distribute verbatim copies
of this license document, but changing it is not allowed.
This version of the GNU Lesser General Public License incorporates
the terms and conditions of version 3 of the GNU General Public
License, supplemented by the additional permissions listed below.
0. Additional Definitions.
As used herein, "this License" refers to version 3 of the GNU Lesser
General Public License, and the "GNU GPL" refers to version 3 of the GNU
General Public License.
"The Library" refers to a covered work governed by this License,
other than an Application or a Combined Work as defined below.
An "Application" is any work that makes use of an interface provided
by the Library, but which is not otherwise based on the Library.
Defining a subclass of a class defined by the Library is deemed a mode
of using an interface provided by the Library.
A "Combined Work" is a work produced by combining or linking an
Application with the Library. The particular version of the Library
with which the Combined Work was made is also called the "Linked
Version".
The "Minimal Corresponding Source" for a Combined Work means the
Corresponding Source for the Combined Work, excluding any source code
for portions of the Combined Work that, considered in isolation, are
based on the Application, and not on the Linked Version.
The "Corresponding Application Code" for a Combined Work means the
object code and/or source code for the Application, including any data
and utility programs needed for reproducing the Combined Work from the
Application, but excluding the System Libraries of the Combined Work.
1. Exception to Section 3 of the GNU GPL.
You may convey a covered work under sections 3 and 4 of this License
without being bound by section 3 of the GNU GPL.
2. Conveying Modified Versions.
If you modify a copy of the Library, and, in your modifications, a
facility refers to a function or data to be supplied by an Application
that uses the facility (other than as an argument passed when the
facility is invoked), then you may convey a copy of the modified
version:
a) under this License, provided that you make a good faith effort to
ensure that, in the event an Application does not supply the
function or data, the facility still operates, and performs
whatever part of its purpose remains meaningful, or
b) under the GNU GPL, with none of the additional permissions of
this License applicable to that copy.
3. Object Code Incorporating Material from Library Header Files.
The object code form of an Application may incorporate material from
a header file that is part of the Library. You may convey such object
code under terms of your choice, provided that, if the incorporated
material is not limited to numerical parameters, data structure
layouts and accessors, or small macros, inline functions and templates
(ten or fewer lines in length), you do both of the following:
a) Give prominent notice with each copy of the object code that the
Library is used in it and that the Library and its use are
covered by this License.
b) Accompany the object code with a copy of the GNU GPL and this license
document.
4. Combined Works.
You may convey a Combined Work under terms of your choice that,
taken together, effectively do not restrict modification of the
portions of the Library contained in the Combined Work and reverse
engineering for debugging such modifications, if you also do each of
the following:
a) Give prominent notice with each copy of the Combined Work that
the Library is used in it and that the Library and its use are
covered by this License.
b) Accompany the Combined Work with a copy of the GNU GPL and this license
document.
c) For a Combined Work that displays copyright notices during
execution, include the copyright notice for the Library among
these notices, as well as a reference directing the user to the
copies of the GNU GPL and this license document.
d) Do one of the following:
0) Convey the Minimal Corresponding Source under the terms of this
License, and the Corresponding Application Code in a form
suitable for, and under terms that permit, the user to
recombine or relink the Application with a modified version of
the Linked Version to produce a modified Combined Work, in the
manner specified by section 6 of the GNU GPL for conveying
Corresponding Source.
1) Use a suitable shared library mechanism for linking with the
Library. A suitable mechanism is one that (a) uses at run time
a copy of the Library already present on the user's computer
system, and (b) will operate properly with a modified version
of the Library that is interface-compatible with the Linked
Version.
e) Provide Installation Information, but only if you would otherwise
be required to provide such information under section 6 of the
GNU GPL, and only to the extent that such information is
necessary to install and execute a modified version of the
Combined Work produced by recombining or relinking the
Application with a modified version of the Linked Version. (If
you use option 4d0, the Installation Information must accompany
the Minimal Corresponding Source and Corresponding Application
Code. If you use option 4d1, you must provide the Installation
Information in the manner specified by section 6 of the GNU GPL
for conveying Corresponding Source.)
5. Combined Libraries.
You may place library facilities that are a work based on the
Library side by side in a single library together with other library
facilities that are not Applications and are not covered by this
License, and convey such a combined library under terms of your
choice, if you do both of the following:
a) Accompany the combined library with a copy of the same work based
on the Library, uncombined with any other library facilities,
conveyed under the terms of this License.
b) Give prominent notice with the combined library that part of it
is a work based on the Library, and explaining where to find the
accompanying uncombined form of the same work.
6. Revised Versions of the GNU Lesser General Public License.
The Free Software Foundation may publish revised and/or new versions
of the GNU Lesser General Public License from time to time. Such new
versions will be similar in spirit to the present version, but may
differ in detail to address new problems or concerns.
Each version is given a distinguishing version number. If the
Library as you received it specifies that a certain numbered version
of the GNU Lesser General Public License "or any later version"
applies to it, you have the option of following the terms and
conditions either of that published version or of any later version
published by the Free Software Foundation. If the Library as you
received it does not specify a version number of the GNU Lesser
General Public License, you may choose any version of the GNU Lesser
General Public License ever published by the Free Software Foundation.
If the Library as you received it specifies that a proxy can decide
whether future versions of the GNU Lesser General Public License shall
apply, that proxy's public statement of acceptance of any version is
permanent authorization for you to choose that version for the
Library.