(* Title: HOL/UNITY/Union.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs.
*)
section\<open>Unions of Programs\<close>
theory Union imports SubstAx FP begin
(*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *)
definition
ok :: "['a program, 'a program] => bool" (infixl "ok" 65)
where "F ok G == Acts F \ AllowedActs G &
Acts G \<subseteq> AllowedActs F"
(*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *)
definition
OK :: "['a set, 'a => 'b program] => bool"
where "OK I F = (\i \ I. \j \ I-{i}. Acts (F i) \ AllowedActs (F j))"
definition
JOIN :: "['a set, 'a => 'b program] => 'b program"
where "JOIN I F = mk_program (\i \ I. Init (F i), \i \ I. Acts (F i),
\<Inter>i \<in> I. AllowedActs (F i))"
definition
Join :: "['a program, 'a program] => 'a program" (infixl "\" 65)
where "F \ G = mk_program (Init F \ Init G, Acts F \ Acts G,
AllowedActs F \<inter> AllowedActs G)"
definition SKIP :: "'a program" ("\")
where "\ = mk_program (UNIV, {}, UNIV)"
(*Characterizes safety properties. Used with specifying Allowed*)
definition
safety_prop :: "'a program set => bool"
where "safety_prop X \ SKIP \ X \ (\G. Acts G \ \(Acts ` X) \ G \ X)"
syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\_./ _)" 10)
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\_\_./ _)" 10)
translations
"\x \ A. B" == "CONST JOIN A (\x. B)"
"\x y. B" == "\x. \y. B"
"\x. B" == "CONST JOIN (CONST UNIV) (\x. B)"
subsection\<open>SKIP\<close>
lemma Init_SKIP [simp]: "Init SKIP = UNIV"
by (simp add: SKIP_def)
lemma Acts_SKIP [simp]: "Acts SKIP = {Id}"
by (simp add: SKIP_def)
lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV"
by (auto simp add: SKIP_def)
lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
by (force elim: reachable.induct intro: reachable.intros)
subsection\<open>SKIP and safety properties\<close>
lemma SKIP_in_constrains_iff [iff]: "(SKIP \ A co B) = (A \ B)"
by (unfold constrains_def, auto)
lemma SKIP_in_Constrains_iff [iff]: "(SKIP \ A Co B) = (A \ B)"
by (unfold Constrains_def, auto)
lemma SKIP_in_stable [iff]: "SKIP \ stable A"
by (unfold stable_def, auto)
declare SKIP_in_stable [THEN stable_imp_Stable, iff]
subsection\<open>Join\<close>
lemma Init_Join [simp]: "Init (F\G) = Init F \ Init G"
by (simp add: Join_def)
lemma Acts_Join [simp]: "Acts (F\G) = Acts F \ Acts G"
by (auto simp add: Join_def)
lemma AllowedActs_Join [simp]:
"AllowedActs (F\G) = AllowedActs F \ AllowedActs G"
by (auto simp add: Join_def)
subsection\<open>JN\<close>
lemma JN_empty [simp]: "(\i\{}. F i) = SKIP"
by (unfold JOIN_def SKIP_def, auto)
lemma JN_insert [simp]: "(\i \ insert a I. F i) = (F a)\(\i \ I. F i)"
apply (rule program_equalityI)
apply (auto simp add: JOIN_def Join_def)
done
lemma Init_JN [simp]: "Init (\i \ I. F i) = (\i \ I. Init (F i))"
by (simp add: JOIN_def)
lemma Acts_JN [simp]: "Acts (\i \ I. F i) = insert Id (\i \ I. Acts (F i))"
by (auto simp add: JOIN_def)
lemma AllowedActs_JN [simp]:
"AllowedActs (\i \ I. F i) = (\i \ I. AllowedActs (F i))"
by (auto simp add: JOIN_def)
lemma JN_cong [cong]:
"[| I=J; !!i. i \ J ==> F i = G i |] ==> (\i \ I. F i) = (\i \ J. G i)"
by (simp add: JOIN_def)
subsection\<open>Algebraic laws\<close>
lemma Join_commute: "F\G = G\F"
by (simp add: Join_def Un_commute Int_commute)
lemma Join_assoc: "(F\G)\H = F\(G\H)"
by (simp add: Un_ac Join_def Int_assoc insert_absorb)
lemma Join_left_commute: "A\(B\C) = B\(A\C)"
by (simp add: Un_ac Int_ac Join_def insert_absorb)
lemma Join_SKIP_left [simp]: "SKIP\F = F"
apply (unfold Join_def SKIP_def)
apply (rule program_equalityI)
apply (simp_all (no_asm) add: insert_absorb)
done
lemma Join_SKIP_right [simp]: "F\SKIP = F"
apply (unfold Join_def SKIP_def)
apply (rule program_equalityI)
apply (simp_all (no_asm) add: insert_absorb)
done
lemma Join_absorb [simp]: "F\F = F"
apply (unfold Join_def)
apply (rule program_equalityI, auto)
done
lemma Join_left_absorb: "F\(F\G) = F\G"
apply (unfold Join_def)
apply (rule program_equalityI, auto)
done
(*Join is an AC-operator*)
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
subsection\<open>Laws Governing \<open>\<Squnion>\<close>\<close>
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
lemma JN_absorb: "k \ I ==> F k\(\i \ I. F i) = (\i \ I. F i)"
by (auto intro!: program_equalityI)
lemma JN_Un: "(\i \ I \ J. F i) = ((\i \ I. F i)\(\i \ J. F i))"
by (auto intro!: program_equalityI)
lemma JN_constant: "(\i \ I. c) = (if I={} then SKIP else c)"
by (rule program_equalityI, auto)
lemma JN_Join_distrib:
"(\i \ I. F i\G i) = (\i \ I. F i) \ (\i \ I. G i)"
by (auto intro!: program_equalityI)
lemma JN_Join_miniscope:
"i \ I ==> (\i \ I. F i\G) = ((\i \ I. F i)\G)"
by (auto simp add: JN_Join_distrib JN_constant)
(*Used to prove guarantees_JN_I*)
lemma JN_Join_diff: "i \ I ==> F i\JOIN (I - {i}) F = JOIN I F"
apply (unfold JOIN_def Join_def)
apply (rule program_equalityI, auto)
done
subsection\<open>Safety: co, stable, FP\<close>
(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B. So an
alternative precondition is A \<subseteq> B, but most proofs using this rule require
I to be nonempty for other reasons anyway.*)
lemma JN_constrains:
"i \ I ==> (\i \ I. F i) \ A co B = (\i \ I. F i \ A co B)"
by (simp add: constrains_def JOIN_def, blast)
lemma Join_constrains [simp]:
"(F\G \ A co B) = (F \ A co B & G \ A co B)"
by (auto simp add: constrains_def Join_def)
lemma Join_unless [simp]:
"(F\G \ A unless B) = (F \ A unless B & G \ A unless B)"
by (simp add: unless_def)
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
*)
lemma Join_constrains_weaken:
"[| F \ A co A'; G \ B co B' |]
==> F\<squnion>G \<in> (A \<inter> B) co (A' \<union> B')"
by (simp, blast intro: constrains_weaken)
(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*)
lemma JN_constrains_weaken:
"[| \i \ I. F i \ A i co A' i; i \ I |]
==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
apply (simp (no_asm_simp) add: JN_constrains)
apply (blast intro: constrains_weaken)
done
lemma JN_stable: "(\i \ I. F i) \ stable A = (\i \ I. F i \ stable A)"
by (simp add: stable_def constrains_def JOIN_def)
lemma invariant_JN_I:
"[| !!i. i \ I ==> F i \ invariant A; i \ I |]
==> (\<Squnion>i \<in> I. F i) \<in> invariant A"
by (simp add: invariant_def JN_stable, blast)
lemma Join_stable [simp]:
"(F\G \ stable A) =
(F \<in> stable A & G \<in> stable A)"
by (simp add: stable_def)
lemma Join_increasing [simp]:
"(F\G \ increasing f) =
(F \<in> increasing f & G \<in> increasing f)"
by (auto simp add: increasing_def)
lemma invariant_JoinI:
"[| F \ invariant A; G \ invariant A |]
==> F\<squnion>G \<in> invariant A"
by (auto simp add: invariant_def)
lemma FP_JN: "FP (\i \ I. F i) = (\i \ I. FP (F i))"
by (simp add: FP_def JN_stable INTER_eq)
subsection\<open>Progress: transient, ensures\<close>
lemma JN_transient:
"i \ I ==>
(\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)"
by (auto simp add: transient_def JOIN_def)
lemma Join_transient [simp]:
"F\G \ transient A =
(F \<in> transient A | G \<in> transient A)"
by (auto simp add: bex_Un transient_def Join_def)
lemma Join_transient_I1: "F \ transient A ==> F\G \ transient A"
by simp
lemma Join_transient_I2: "G \ transient A ==> F\G \ transient A"
by simp
(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
lemma JN_ensures:
"i \ I ==>
(\<Squnion>i \<in> I. F i) \<in> A ensures B =
((\<forall>i \<in> I. F i \<in> (A-B) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))"
by (auto simp add: ensures_def JN_constrains JN_transient)
lemma Join_ensures:
"F\G \ A ensures B =
(F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &
(F \<in> transient (A-B) | G \<in> transient (A-B)))"
by (auto simp add: ensures_def)
lemma stable_Join_constrains:
"[| F \ stable A; G \ A co A' |]
==> F\<squnion>G \<in> A co A'"
apply (unfold stable_def constrains_def Join_def)
apply (simp add: ball_Un, blast)
done
(*Premise for G cannot use Always because F \<in> Stable A is weaker than
G \<in> stable A *)
lemma stable_Join_Always1:
"[| F \ stable A; G \ invariant A |] ==> F\G \ Always A"
apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
apply (force intro: stable_Int)
done
(*As above, but exchanging the roles of F and G*)
lemma stable_Join_Always2:
"[| F \ invariant A; G \ stable A |] ==> F\G \ Always A"
apply (subst Join_commute)
apply (blast intro: stable_Join_Always1)
done
lemma stable_Join_ensures1:
"[| F \ stable A; G \ A ensures B |] ==> F\G \ A ensures B"
apply (simp (no_asm_simp) add: Join_ensures)
apply (simp add: stable_def ensures_def)
apply (erule constrains_weaken, auto)
done
(*As above, but exchanging the roles of F and G*)
lemma stable_Join_ensures2:
"[| F \ A ensures B; G \ stable A |] ==> F\G \ A ensures B"
apply (subst Join_commute)
apply (blast intro: stable_Join_ensures1)
done
subsection\<open>the ok and OK relations\<close>
lemma ok_SKIP1 [iff]: "SKIP ok F"
by (simp add: ok_def)
lemma ok_SKIP2 [iff]: "F ok SKIP"
by (simp add: ok_def)
lemma ok_Join_commute:
"(F ok G & (F\G) ok H) = (G ok H & F ok (G\H))"
by (auto simp add: ok_def)
lemma ok_commute: "(F ok G) = (G ok F)"
by (auto simp add: ok_def)
lemmas ok_sym = ok_commute [THEN iffD1]
lemma ok_iff_OK:
"OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\G) ok H)"
apply (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
all_conj_distrib)
apply blast
done
lemma ok_Join_iff1 [iff]: "F ok (G\H) = (F ok G & F ok H)"
by (auto simp add: ok_def)
lemma ok_Join_iff2 [iff]: "(G\H) ok F = (G ok F & H ok F)"
by (auto simp add: ok_def)
(*useful? Not with the previous two around*)
lemma ok_Join_commute_I: "[| F ok G; (F\G) ok H |] ==> F ok (G\H)"
by (auto simp add: ok_def)
lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\i \ I. F ok G i)"
by (auto simp add: ok_def)
lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (\i \ I. G i ok F)"
by (auto simp add: ok_def)
lemma OK_iff_ok: "OK I F = (\i \ I. \j \ I-{i}. (F i) ok (F j))"
by (auto simp add: ok_def OK_def)
lemma OK_imp_ok: "[| OK I F; i \ I; j \ I; i \ j|] ==> (F i) ok (F j)"
by (auto simp add: OK_iff_ok)
subsection\<open>Allowed\<close>
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
by (auto simp add: Allowed_def)
lemma Allowed_Join [simp]: "Allowed (F\G) = Allowed F \ Allowed G"
by (auto simp add: Allowed_def)
lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\i \ I. Allowed (F i))"
by (auto simp add: Allowed_def)
lemma ok_iff_Allowed: "F ok G = (F \ Allowed G & G \ Allowed F)"
by (simp add: ok_def Allowed_def)
lemma OK_iff_Allowed: "OK I F = (\i \ I. \j \ I-{i}. F i \ Allowed(F j))"
by (auto simp add: OK_iff_ok ok_iff_Allowed)
subsection\<open>\<^term>\<open>safety_prop\<close>, for reasoning about
given instances of "ok"\<close>
lemma safety_prop_Acts_iff:
"safety_prop X ==> (Acts G \ insert Id (\(Acts ` X))) = (G \ X)"
by (auto simp add: safety_prop_def)
lemma safety_prop_AllowedActs_iff_Allowed:
"safety_prop X ==> (\(Acts ` X) \ AllowedActs F) = (X \ Allowed F)"
by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
lemma Allowed_eq:
"safety_prop X ==> Allowed (mk_program (init, acts, \(Acts ` X))) = X"
by (simp add: Allowed_def safety_prop_Acts_iff)
(*For safety_prop to hold, the property must be satisfiable!*)
lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \ B)"
by (simp add: safety_prop_def constrains_def, blast)
lemma safety_prop_stable [iff]: "safety_prop (stable A)"
by (simp add: stable_def)
lemma safety_prop_Int [simp]:
"safety_prop X \ safety_prop Y \ safety_prop (X \ Y)"
proof (clarsimp simp add: safety_prop_def)
fix G
assume "\G. Acts G \ (\x\X. Acts x) \ G \ X"
then have X: "Acts G \ (\x\X. Acts x) \ G \ X" by blast
assume "\G. Acts G \ (\x\Y. Acts x) \ G \ Y"
then have Y: "Acts G \ (\x\Y. Acts x) \ G \ Y" by blast
assume Acts: "Acts G \ (\x\X \ Y. Acts x)"
with X and Y show "G \ X \ G \ Y" by auto
qed
lemma safety_prop_INTER [simp]:
"(\i. i \ I \ safety_prop (X i)) \ safety_prop (\i\I. X i)"
proof (clarsimp simp add: safety_prop_def)
fix G and i
assume "\i. i \ I \ \ \ X i \
(\<forall>G. Acts G \<subseteq> (\<Union>x\<in>X i. Acts x) \<longrightarrow> G \<in> X i)"
then have *: "i \ I \ Acts G \ (\x\X i. Acts x) \ G \ X i"
by blast
assume "i \ I"
moreover assume "Acts G \ (\j\\i\I. X i. Acts j)"
ultimately have "Acts G \ (\i\X i. Acts i)"
by auto
with * \<open>i \<in> I\<close> show "G \<in> X i" by blast
qed
lemma safety_prop_INTER1 [simp]:
"(\i. safety_prop (X i)) \ safety_prop (\i. X i)"
by (rule safety_prop_INTER) simp
lemma def_prg_Allowed:
"[| F == mk_program (init, acts, \(Acts ` X)) ; safety_prop X |]
==> Allowed F = X"
by (simp add: Allowed_eq)
lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F"
by (simp add: Allowed_def)
lemma def_total_prg_Allowed:
"[| F = mk_total_program (init, acts, \(Acts ` X)) ; safety_prop X |]
==> Allowed F = X"
by (simp add: mk_total_program_def def_prg_Allowed)
lemma def_UNION_ok_iff:
"[| F = mk_program(init,acts,\(Acts ` X)); safety_prop X |]
==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
by (auto simp add: ok_def safety_prop_Acts_iff)
text\<open>The union of two total programs is total.\<close>
lemma totalize_Join: "totalize F\totalize G = totalize (F\G)"
by (simp add: program_equalityI totalize_def Join_def image_Un)
lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F\G)"
by (simp add: all_total_def, blast)
lemma totalize_JN: "(\i \ I. totalize (F i)) = totalize(\i \ I. F i)"
by (simp add: program_equalityI totalize_def JOIN_def image_UN)
lemma all_total_JN: "(!!i. i\I ==> all_total (F i)) ==> all_total(\i\I. F i)"
by (simp add: all_total_iff_totalize totalize_JN [symmetric])
end
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
