definition"constrains" :: "[i, i] \ i" (infixl \co\ 60) where "A co B \ {F \ program. (\act \ Acts(F). act``A\B) \ st_set(A)}" \<comment> \<open>the condition \<^term>\<open>st_set(A)\<close> makes the definition slightly
stronger than the HOL one\<close>
definition unless :: "[i, i] \ i" (infixl \unless\ 60) where "A unless B \ (A - B) co (A \ B)"
definition
stable :: "i\i" where "stable(A) \ A co A"
definition
strongest_rhs :: "[i, i] \ i" where "strongest_rhs(F, A) \ \({B \ Pow(state). F \ A co B})"
definition
invariant :: "i \ i" where "invariant(A) \ initially(A) \ stable(A)"
lemma Acts_type: "Acts(F)\Pow(state*state)" by (simp add: RawActs_type Acts_def)
lemma AllowedActs_type: "AllowedActs(F) \ Pow(state*state)" by (simp add: RawAllowedActs_type AllowedActs_def)
text\<open>Needed in Behaviors\<close> lemma ActsD: "\act \ Acts(F); \ act\ \ s \ state \ s' \ state" by (blast dest: Acts_type [THEN subsetD])
lemma AllowedActsD: "\act \ AllowedActs(F); \ act\ \ s \ state \ s' \ state" by (blast dest: AllowedActs_type [THEN subsetD])
subsection\<open>Simplification rules involving \<^term>\<open>state\<close>, \<^term>\<open>Init\<close>, \<^term>\<open>Acts\<close>, and \<^term>\<open>AllowedActs\<close>\<close>
text\<open>But are they really needed?\<close>
lemma state_subset_is_Init_iff [iff]: "state \ Init(F) \ Init(F)=state" by (cut_tac F = F in Init_type, auto)
lemma Pow_state_times_state_is_subset_Acts_iff [iff]: "Pow(state*state) \ Acts(F) \ Acts(F)=Pow(state*state)" by (cut_tac F = F in Acts_type, auto)
lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]: "Pow(state*state) \ AllowedActs(F) \ AllowedActs(F)=Pow(state*state)" by (cut_tac F = F in AllowedActs_type, auto)
subsubsection\<open>Eliminating \<open>\<inter> state\<close> from expressions\<close>
lemma Init_Int_state [simp]: "Init(F) \ state = Init(F)" by (cut_tac F = F in Init_type, blast)
lemma state_Int_Init [simp]: "state \ Init(F) = Init(F)" by (cut_tac F = F in Init_type, blast)
lemma Acts_Int_Pow_state_times_state [simp]: "Acts(F) \ Pow(state*state) = Acts(F)" by (cut_tac F = F in Acts_type, blast)
lemma state_times_state_Int_Acts [simp]: "Pow(state*state) \ Acts(F) = Acts(F)" by (cut_tac F = F in Acts_type, blast)
lemma AllowedActs_Int_Pow_state_times_state [simp]: "AllowedActs(F) \ Pow(state*state) = AllowedActs(F)" by (cut_tac F = F in AllowedActs_type, blast)
lemma state_times_state_Int_AllowedActs [simp]: "Pow(state*state) \ AllowedActs(F) = AllowedActs(F)" by (cut_tac F = F in AllowedActs_type, blast)
lemma def_prg_Init: "F \ mk_program (init,acts,allowed) \ Init(F) = init \ state" by auto
lemma def_prg_Acts: "F \ mk_program (init,acts,allowed) \<Longrightarrow> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))" by auto
lemma def_prg_AllowedActs: "F \ mk_program (init,acts,allowed) \<Longrightarrow> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" by auto
lemma def_prg_simps: "\F \ mk_program (init,acts,allowed)\ \<Longrightarrow> Init(F) = init \<inter> state \<and>
Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) \<and>
AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" by auto
text\<open>An action is expanded only if a pair of states is being tested against it\<close> lemma def_act_simp: "\act \ { \ A*B. P(s, s')}\ \<Longrightarrow> (<s,s'> \<in> act) \<longleftrightarrow> (<s,s'> \<in> A*B \<and> P(s, s'))" by auto
text\<open>A set is expanded only if an element is being tested against it\<close> lemma def_set_simp: "A \ B \ (x \ A) \ (x \ B)" by auto
subsection\<open>The Constrains Operator\<close>
lemma constrains_type: "A co B \ program" by (force simp add: constrains_def)
lemma constrainsI: "\(\act s s'. \act: Acts(F); \ act; s \ A\ \ s' \ A');
F \<in> program; st_set(A)\<rbrakk> \<Longrightarrow> F \<in> A co A'" by (force simp add: constrains_def)
lemma constrainsD: "F \ A co B \ \act \ Acts(F). act``A\B" by (force simp add: constrains_def)
lemma constrainsD2: "F \ A co B \ F \ program \ st_set(A)" by (force simp add: constrains_def)
lemma constrains_empty [iff]: "F \ 0 co B \ F \ program" by (force simp add: constrains_def st_set_def)
lemma constrains_empty2 [iff]: "(F \ A co 0) \ (A=0 \ F \ program)" by (force simp add: constrains_def st_set_def)
lemma constrains_state [iff]: "(F \ state co B) \ (state\B \ F \ program)" apply (cut_tac F = F in Acts_type) apply (force simp add: constrains_def st_set_def) done
lemma constrains_state2 [iff]: "F \ A co state \ (F \ program \ st_set(A))" apply (cut_tac F = F in Acts_type) apply (force simp add: constrains_def st_set_def) done
text\<open>monotonic in 2nd argument\<close> lemma constrains_weaken_R: "\F \ A co A'; A'\B'\ \ F \ A co B'" apply (unfold constrains_def, blast) done
text\<open>anti-monotonic in 1st argument\<close> lemma constrains_weaken_L: "\F \ A co A'; B\A\ \ F \ B co A'" apply (unfold constrains_def st_set_def, blast) done
lemma constrains_weaken: "\F \ A co A'; B\A; A'\B'\ \ F \ B co B'" apply (drule constrains_weaken_R) apply (drule_tac [2] constrains_weaken_L, blast+) done
subsection\<open>Constrains and Union\<close>
lemma constrains_Un: "\F \ A co A'; F \ B co B'\ \ F \ (A \ B) co (A' \ B')" by (auto simp add: constrains_def st_set_def, force)
lemma constrains_UN: "\\i. i \ I \ F \ A(i) co A'(i); F \ program\ \<Longrightarrow> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))" by (force simp add: constrains_def st_set_def)
lemma constrains_Un_distrib: "(A \ B) co C = (A co C) \ (B co C)" by (force simp add: constrains_def st_set_def)
lemma constrains_UN_distrib: "i \ I \ (\i \ I. A(i)) co B = (\i \ I. A(i) co B)" by (force simp add: constrains_def st_set_def)
subsection\<open>Constrains and Intersection\<close>
lemma constrains_Int_distrib: "C co (A \ B) = (C co A) \ (C co B)" by (force simp add: constrains_def st_set_def)
lemma constrains_INT_distrib: "x \ I \ A co (\i \ I. B(i)) = (\i \ I. A co B(i))" by (force simp add: constrains_def st_set_def)
lemma constrains_Int: "\F \ A co A'; F \ B co B'\ \ F \ (A \ B) co (A' \ B')" by (force simp add: constrains_def st_set_def)
lemma constrains_INT [rule_format]: "\\i \ I. F \ A(i) co A'(i); F \ program\ \<Longrightarrow> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))" apply (case_tac "I=0") apply (simp add: Inter_def) apply (erule not_emptyE) apply (auto simp add: constrains_def st_set_def, blast) apply (drule bspec, assumption, force) done
(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *) lemma constrains_All: "\\z. F:{s \ state. P(s, z)} co {s \ state. Q(s, z)}; F \ program\\
F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}" by (unfold constrains_def, blast)
lemma constrains_imp_subset: "\F \ A co A'\ \ A \ A'" by (unfold constrains_def st_set_def, force)
text\<open>The reasoning is by subsets since "co" refers to single actions
only. So this rule isn't that useful.\
lemma constrains_trans: "\F \ A co B; F \ B co C\ \ F \ A co C" by (unfold constrains_def st_set_def, auto, blast)
lemma constrains_cancel: "\F \ A co (A' \ B); F \ B co B'\ \ F \ A co (A' \ B')" apply (drule_tac A = B in constrains_imp_subset) apply (blast intro: constrains_weaken_R) done
subsection\<open>The Unless Operator\<close>
lemma unless_type: "A unless B \ program" by (force simp add: unless_def constrains_def)
lemma unlessI: "\F \ (A-B) co (A \ B)\ \ F \ A unless B" unfolding unless_def apply (blast dest: constrainsD2) done
lemma unlessD: "F :A unless B \ F \ (A-B) co (A \ B)" by (unfold unless_def, auto)
lemma stable_UN: "\\i. i\I \ F \ stable(A(i)); F \ program\ \<Longrightarrow> F \<in> stable (\<Union>i \<in> I. A(i))" unfolding stable_def apply (blast intro: constrains_UN) done
lemma stable_Int: "\F \ stable(A); F \ stable(A')\ \ F \ stable (A \ A')" unfolding stable_def apply (blast intro: constrains_Int) done
lemma stable_INT: "\\i. i \ I \ F \ stable(A(i)); F \ program\ \<Longrightarrow> F \<in> stable (\<Inter>i \<in> I. A(i))" unfolding stable_def apply (blast intro: constrains_INT) done
lemma stable_All: "\\z. F \ stable({s \ state. P(s, z)}); F \ program\ \<Longrightarrow> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})" unfolding stable_def apply (rule constrains_All, auto) done
lemma stable_constrains_Un: "\F \ stable(C); F \ A co (C \ A')\ \ F \ (C \ A) co (C \ A')" apply (unfold stable_def constrains_def st_set_def, auto) apply (blast dest!: bspec) done
lemma stable_constrains_Int: "\F \ stable(C); F \ (C \ A) co A'\ \ F \ (C \ A) co (C \ A')" by (unfold stable_def constrains_def st_set_def, blast)
(* \<lbrakk>F \<in> stable(C); F \<in> (C \<inter> A) co A\<rbrakk> \<Longrightarrow> F \<in> stable(C \<inter> A) *) lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI]
lemma invariantI: "\Init(F)\A; F \ stable(A)\ \ F \ invariant(A)" unfolding invariant_def initially_def apply (frule stable_type [THEN subsetD], auto) done
lemma invariantD: "F \ invariant(A) \ Init(F)\A \ F \ stable(A)" by (unfold invariant_def initially_def, auto)
lemma invariantD2: "F \ invariant(A) \ F \ program \ st_set(A)" unfolding invariant_def apply (blast dest: stableD2) done
text\<open>Could also say \<^term>\<open>invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)\<close>\<close> lemma invariant_Int: "\F \ invariant(A); F \ invariant(B)\ \ F \ invariant(A \ B)" unfolding invariant_def initially_def apply (simp add: stable_Int, blast) done
subsection\<open>The Elimination Theorem\<close>
(** The "free" m has become universally quantified! Should the premise be \<And>m instead of \<forall>m ? Would make it harder
to use in forward proof. **)
text\<open>The general case is easier to prove than the special case!\<close> lemma"elimination": "\\m \ M. F \ {s \ A. x(s) = m} co B(m); F \ program\ \<Longrightarrow> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" by (auto simp add: constrains_def st_set_def, blast)
text\<open>As above, but for the special case of A=state\<close> lemma elimination2: "\\m \ M. F \ {s \ state. x(s) = m} co B(m); F \ program\ \<Longrightarrow> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" by (rule UNITY.elimination, auto)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
