Theory Constrains
section‹Weak Safety Properties›
theory Constrains
imports UNITY
begin
consts traces :: "[i, i] ⇒ i"
inductive
domains
"traces(init, acts)" <=
"(init ∪ (⋃act∈acts. field(act)))*list(⋃act∈acts. field(act))"
intros
Init: "s: init ⟹ <s,[]> ∈ traces(init,acts)"
Acts: "⟦act:acts; ⟨s,evs⟩ ∈ traces(init,acts); <s,s'>: act⟧
⟹ <s', Cons(s,evs)> ∈ traces(init, acts)"
type_intros list.intros UnI1 UnI2 UN_I fieldI2 fieldI1
consts reachable :: "i⇒i"
inductive
domains
"reachable(F)" ⊆ "Init(F) ∪ (⋃act∈Acts(F). field(act))"
intros
Init: "s:Init(F) ⟹ s:reachable(F)"
Acts: "⟦act: Acts(F); s:reachable(F); <s,s'>: act⟧
⟹ s':reachable(F)"
type_intros UnI1 UnI2 fieldI2 UN_I
definition
Constrains :: "[i,i] ⇒ i" (infixl ‹Co› 60) where
"A Co B ≡ {F:program. F:(reachable(F) ∩ A) co B}"
definition
op_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
Always :: "i ⇒ i" where
"Always(A) ≡ initially(A) ∩ Stable(A)"
lemma reachable_type: "reachable(F) ⊆ state"
apply (cut_tac F = F in Init_type)
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = F in reachable.dom_subset, blast)
done
lemma st_set_reachable: "st_set(reachable(F))"
unfolding st_set_def
apply (rule reachable_type)
done
declare st_set_reachable [iff]
lemma reachable_Int_state: "reachable(F) ∩ state = reachable(F)"
by (cut_tac reachable_type, auto)
declare reachable_Int_state [iff]
lemma state_Int_reachable: "state ∩ reachable(F) = reachable(F)"
by (cut_tac reachable_type, auto)
declare state_Int_reachable [iff]
lemma reachable_equiv_traces:
"F ∈ program ⟹ reachable(F)={s ∈ state. ∃evs. ⟨s,evs⟩:traces(Init(F), Acts(F))}"
apply (rule equalityI, safe)
apply (blast dest: reachable_type [THEN subsetD])
apply (erule_tac [2] traces.induct)
apply (erule reachable.induct)
apply (blast intro: reachable.intros traces.intros)+
done
lemma Init_into_reachable: "Init(F) ⊆ reachable(F)"
by (blast intro: reachable.intros)
lemma stable_reachable: "⟦F ∈ program; G ∈ program;
Acts(G) ⊆ Acts(F)⟧ ⟹ G ∈ stable(reachable(F))"
apply (blast intro: stableI constrainsI st_setI
reachable_type [THEN subsetD] reachable.intros)
done
declare stable_reachable [intro!]
declare stable_reachable [simp]
lemma invariant_reachable:
"F ∈ program ⟹ F ∈ invariant(reachable(F))"
unfolding invariant_def initially_def
apply (blast intro: reachable_type [THEN subsetD] reachable.intros)
done
lemma invariant_includes_reachable: "F ∈ invariant(A) ⟹ reachable(F) ⊆ A"
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = F in Init_type)
apply (cut_tac F = F in reachable_type)
apply (simp (no_asm_use) add: stable_def constrains_def invariant_def initially_def)
apply (rule subsetI)
apply (erule reachable.induct)
apply (blast intro: reachable.intros)+
done
lemma constrains_reachable_Int: "F ∈ B co B'⟹F:(reachable(F) ∩ B) co (reachable(F) ∩ B')"
apply (frule constrains_type [THEN subsetD])
apply (frule stable_reachable [OF _ _ subset_refl])
apply (simp_all add: stable_def constrains_Int)
done
lemma Constrains_eq_constrains:
"A Co B = {F ∈ program. F:(reachable(F) ∩ A) co (reachable(F) ∩ B)}"
unfolding Constrains_def
apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD]
intro: constrains_weaken)
done
lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection]
lemma constrains_imp_Constrains: "F ∈ A co A' ⟹ F ∈ A Co A'"
unfolding Constrains_def
apply (blast intro: constrains_weaken_L dest: constrainsD2)
done
lemma ConstrainsI:
"⟦⋀act s s'. ⟦act ∈ Acts(F); <s,s'>:act; s ∈ A⟧ ⟹ s':A';
F ∈ program⟧
⟹ F ∈ A Co A'"
apply (auto simp add: Constrains_def constrains_def st_set_def)
apply (blast dest: reachable_type [THEN subsetD])
done
lemma Constrains_type:
"A Co B ⊆ program"
apply (unfold Constrains_def, blast)
done
lemma Constrains_empty: "F ∈ 0 Co B ⟷ F ∈ program"
by (auto dest: Constrains_type [THEN subsetD]
intro: constrains_imp_Constrains)
declare Constrains_empty [iff]
lemma Constrains_state: "F ∈ A Co state ⟷ F ∈ program"
unfolding Constrains_def
apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains)
done
declare Constrains_state [iff]
lemma Constrains_weaken_R:
"⟦F ∈ A Co A'; A'<=B'⟧ ⟹ F ∈ A Co B'"
unfolding Constrains_def2
apply (blast intro: constrains_weaken_R)
done
lemma Constrains_weaken_L:
"⟦F ∈ A Co A'; B<=A⟧ ⟹ F ∈ B Co A'"
unfolding Constrains_def2
apply (blast intro: constrains_weaken_L st_set_subset)
done
lemma Constrains_weaken:
"⟦F ∈ A Co A'; B<=A; A'<=B'⟧ ⟹ F ∈ B Co B'"
unfolding Constrains_def2
apply (blast intro: constrains_weaken st_set_subset)
done
lemma Constrains_Un:
"⟦F ∈ A Co A'; F ∈ B Co B'⟧ ⟹ F ∈ (A ∪ B) Co (A' ∪ B')"
apply (unfold Constrains_def2, auto)
apply (simp add: Int_Un_distrib)
apply (blast intro: constrains_Un)
done
lemma Constrains_UN:
"⟦(⋀i. i ∈ I⟹F ∈ A(i) Co A'(i)); F ∈ program⟧
⟹ F:(⋃i ∈ I. A(i)) Co (⋃i ∈ I. A'(i))"
by (auto intro: constrains_UN simp del: UN_simps
simp add: Constrains_def2 Int_UN_distrib)
lemma Constrains_Int:
"⟦F ∈ A Co A'; F ∈ B Co B'⟧⟹ F:(A ∩ B) Co (A' ∩ B')"
unfolding Constrains_def
apply (subgoal_tac "reachable (F) ∩ (A ∩ B) = (reachable (F) ∩ A) ∩ (reachable (F) ∩ B) ")
apply (auto intro: constrains_Int)
done
lemma Constrains_INT:
"⟦(⋀i. i ∈ I ⟹F ∈ A(i) Co A'(i)); F ∈ program⟧
⟹ F:(⋂i ∈ I. A(i)) Co (⋂i ∈ I. A'(i))"
apply (simp (no_asm_simp) del: INT_simps add: Constrains_def INT_extend_simps)
apply (rule constrains_INT)
apply (auto simp add: Constrains_def)
done
lemma Constrains_imp_subset: "F ∈ A Co A' ⟹ reachable(F) ∩ A ⊆ A'"
unfolding Constrains_def
apply (blast dest: constrains_imp_subset)
done
lemma Constrains_trans:
"⟦F ∈ A Co B; F ∈ B Co C⟧ ⟹ F ∈ A Co C"
unfolding Constrains_def2
apply (blast intro: constrains_trans constrains_weaken)
done
lemma Constrains_cancel:
"⟦F ∈ A Co (A' ∪ B); F ∈ B Co B'⟧ ⟹ F ∈ A Co (A' ∪ B')"
unfolding Constrains_def2
apply (simp (no_asm_use) add: Int_Un_distrib)
apply (blast intro: constrains_cancel)
done
lemma stable_imp_Stable:
"F ∈ stable(A) ⟹ F ∈ Stable(A)"
unfolding stable_def Stable_def
apply (erule constrains_imp_Constrains)
done
lemma Stable_eq: "⟦F ∈ Stable(A); A = B⟧ ⟹ F ∈ Stable(B)"
by blast
lemma Stable_eq_stable:
"F ∈ Stable(A) ⟷ (F ∈ stable(reachable(F) ∩ A))"
apply (auto dest: constrainsD2 simp add: Stable_def stable_def Constrains_def2)
done
lemma StableI: "F ∈ A Co A ⟹ F ∈ Stable(A)"
by (unfold Stable_def, assumption)
lemma StableD: "F ∈ Stable(A) ⟹ F ∈ A Co A"
by (unfold Stable_def, assumption)
lemma Stable_Un:
"⟦F ∈ Stable(A); F ∈ Stable(A')⟧ ⟹ F ∈ Stable(A ∪ A')"
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_Constrains_Un:
"⟦F ∈ Stable(C); F ∈ A Co (C ∪ A')⟧
⟹ F ∈ (C ∪ A) Co (C ∪ A')"
unfolding Stable_def
apply (blast intro: Constrains_Un [THEN Constrains_weaken_R])
done
lemma Stable_Constrains_Int:
"⟦F ∈ Stable(C); F ∈ (C ∩ A) Co A'⟧
⟹ F ∈ (C ∩ A) Co (C ∩ A')"
unfolding Stable_def
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
done
lemma Stable_UN:
"⟦(⋀i. i ∈ I ⟹ F ∈ Stable(A(i))); F ∈ program⟧
⟹ F ∈ Stable (⋃i ∈ I. A(i))"
apply (simp add: Stable_def)
apply (blast intro: Constrains_UN)
done
lemma Stable_INT:
"⟦(⋀i. i ∈ I ⟹ F ∈ Stable(A(i))); F ∈ program⟧
⟹ F ∈ Stable (⋂i ∈ I. A(i))"
apply (simp add: Stable_def)
apply (blast intro: Constrains_INT)
done
lemma Stable_reachable: "F ∈ program ⟹F ∈ Stable (reachable(F))"
apply (simp (no_asm_simp) add: Stable_eq_stable Int_absorb)
done
lemma Stable_type: "Stable(A) ⊆ program"
unfolding Stable_def
apply (rule Constrains_type)
done
lemma Elimination:
"⟦∀m ∈ M. F ∈ ({s ∈ A. x(s) = m}) Co (B(m)); F ∈ program⟧
⟹ F ∈ ({s ∈ A. x(s):M}) Co (⋃m ∈ M. B(m))"
apply (unfold Constrains_def, auto)
apply (rule_tac A1 = "reachable (F) ∩ A"
in UNITY.elimination [THEN constrains_weaken_L])
apply (auto intro: constrains_weaken_L)
done
lemma Elimination2:
"⟦∀m ∈ M. F ∈ {s ∈ state. x(s) = m} Co B(m); F ∈ program⟧
⟹ F ∈ {s ∈ state. x(s):M} Co (⋃m ∈ M. B(m))"
apply (blast intro: Elimination)
done
lemma Unless_type: "A Unless B <=program"
unfolding op_Unless_def
apply (rule Constrains_type)
done
lemma AlwaysI:
"⟦Init(F)<=A; F ∈ Stable(A)⟧ ⟹ F ∈ Always(A)"
unfolding Always_def initially_def
apply (frule Stable_type [THEN subsetD], auto)
done
lemma AlwaysD: "F ∈ Always(A) ⟹ Init(F)<=A ∧ F ∈ Stable(A)"
by (simp add: Always_def initially_def)
lemmas AlwaysE = AlwaysD [THEN conjE]
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
lemma Always_includes_reachable: "F ∈ Always(A) ⟹ reachable(F) ⊆ A"
apply (simp (no_asm_use) add: Stable_def Constrains_def constrains_def Always_def initially_def)
apply (rule subsetI)
apply (erule reachable.induct)
apply (blast intro: reachable.intros)+
done
lemma invariant_imp_Always:
"F ∈ invariant(A) ⟹ F ∈ Always(A)"
unfolding Always_def invariant_def Stable_def stable_def
apply (blast intro: constrains_imp_Constrains)
done
lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
lemma Always_eq_invariant_reachable: "Always(A) = {F ∈ program. F ∈ invariant(reachable(F) ∩ A)}"
apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def)
apply (rule equalityI, auto)
apply (blast intro: reachable.intros reachable_type)
done
lemma Always_eq_includes_reachable: "Always(A) = {F ∈ program. reachable(F) ⊆ A}"
apply (rule equalityI, safe)
apply (auto dest: invariant_includes_reachable
simp add: subset_Int_iff invariant_reachable Always_eq_invariant_reachable)
done
lemma Always_type: "Always(A) ⊆ program"
by (unfold Always_def initially_def, auto)
lemma Always_state_eq: "Always(state) = program"
apply (rule equalityI)
apply (auto dest: Always_type [THEN subsetD] reachable_type [THEN subsetD]
simp add: Always_eq_includes_reachable)
done
declare Always_state_eq [simp]
lemma state_AlwaysI: "F ∈ program ⟹ F ∈ Always(state)"
by (auto dest: reachable_type [THEN subsetD]
simp add: Always_eq_includes_reachable)
lemma Always_eq_UN_invariant: "st_set(A) ⟹ Always(A) = (⋃I ∈ Pow(A). invariant(I))"
apply (simp (no_asm) add: Always_eq_includes_reachable)
apply (rule equalityI, auto)
apply (blast intro: invariantI rev_subsetD [OF _ Init_into_reachable]
rev_subsetD [OF _ invariant_includes_reachable]
dest: invariant_type [THEN subsetD])+
done
lemma Always_weaken: "⟦F ∈ Always(A); A ⊆ B⟧ ⟹ F ∈ Always(B)"
by (auto simp add: Always_eq_includes_reachable)
lemmas Int_absorb2 = subset_Int_iff [unfolded iff_def, THEN conjunct1, THEN mp]
lemma Always_Constrains_pre: "F ∈ Always(I) ⟹ (F:(I ∩ A) Co A') ⟷ (F ∈ A Co A')"
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric])
done
lemma Always_Constrains_post: "F ∈ Always(I) ⟹ (F ∈ A Co (I ∩ A')) ⟷(F ∈ A Co A')"
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric])
done
lemma Always_ConstrainsI: "⟦F ∈ Always(I); F ∈ (I ∩ A) Co A'⟧ ⟹ F ∈ A Co A'"
by (blast intro: Always_Constrains_pre [THEN iffD1])
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
lemma Always_Constrains_weaken:
"⟦F ∈ Always(C); F ∈ A Co A'; C ∩ B<=A; C ∩ A'<=B'⟧⟹F ∈ B Co B'"
apply (rule Always_ConstrainsI)
apply (drule_tac [2] Always_ConstrainsD, simp_all)
apply (blast intro: Constrains_weaken)
done
lemma Always_Int_distrib: "Always(A ∩ B) = Always(A) ∩ Always(B)"
by (auto simp add: Always_eq_includes_reachable)
lemma Always_INT_distrib: "i ∈ I⟹Always(⋂i ∈ I. A(i)) = (⋂i ∈ I. Always(A(i)))"
apply (rule equalityI)
apply (auto simp add: Inter_iff Always_eq_includes_reachable)
done
lemma Always_Int_I: "⟦F ∈ Always(A); F ∈ Always(B)⟧ ⟹ F ∈ Always(A ∩ B)"
apply (simp (no_asm_simp) add: Always_Int_distrib)
done
lemma Always_Diff_Un_eq: "⟦F ∈ Always(A)⟧ ⟹ (F ∈ Always(C-A ∪ B)) ⟷ (F ∈ Always(B))"
by (auto simp add: Always_eq_includes_reachable)
lemmas Always_thin = thin_rl [of "F ∈ Always(A)"] for F A
named_theorems program "program definitions"
ML
‹
fun Always_Int_tac ctxt =
dresolve_tac ctxt @{thms Always_Int_I} THEN'
assume_tac ctxt THEN'
eresolve_tac ctxt @{thms Always_thin};
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
fun constrains_tac ctxt =
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac ctxt 1),
REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
ORELSE
resolve_tac ctxt [@{thm StableI}, @{thm stableI},
@{thm constrains_imp_Constrains}] 1),
resolve_tac ctxt @{thms constrainsI} 1,
rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
REPEAT (force_tac ctxt 2),
full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>‹program›)) 1,
ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})),
ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})),
ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac ctxt),
ALLGOALS (clarify_tac ctxt)]);
fun always_tac ctxt i =
resolve_tac ctxt @{thms AlwaysI} i THEN
force_tac ctxt i
THEN constrains_tac ctxt i;
›
method_setup safety = ‹
Scan.succeed (SIMPLE_METHOD' o constrains_tac)›
"for proving safety properties"
method_setup always = ‹
Scan.succeed (SIMPLE_METHOD' o always_tac)›
"for proving invariants"
end