Theory SubstAx
section‹Weak LeadsTo relation (restricted to the set of reachable states)›
theory SubstAx
imports WFair Constrains
begin
definition
Ensures :: "[i,i] ⇒ i" (infixl ‹Ensures› 60) where
"A Ensures B ≡ {F ∈ program. F ∈ (reachable(F) ∩ A) ensures (reachable(F) ∩ B) }"
definition
LeadsTo :: "[i, i] ⇒ i" (infixl ‹⟼w› 60) where
"A ⟼w B ≡ {F ∈ program. F:(reachable(F) ∩ A) ⟼ (reachable(F) ∩ B)}"
lemma LeadsTo_eq:
"st_set(B)⟹ A ⟼w B = {F ∈ program. F:(reachable(F) ∩ A) ⟼ B}"
unfolding LeadsTo_def
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
done
lemma LeadsTo_type: "A ⟼w B <=program"
by (unfold LeadsTo_def, auto)
lemma Always_LeadsTo_pre: "F ∈ Always(I) ⟹ (F:(I ∩ A) ⟼w A') ⟷ (F ∈ A ⟼w A')"
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
lemma Always_LeadsTo_post: "F ∈ Always(I) ⟹ (F ∈ A ⟼w (I ∩ A')) ⟷ (F ∈ A ⟼w A')"
unfolding LeadsTo_def
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
done
lemma Always_LeadsToI: "⟦F ∈ Always(C); F ∈ (C ∩ A) ⟼w A'⟧ ⟹ F ∈ A ⟼w A'"
by (blast intro: Always_LeadsTo_pre [THEN iffD1])
lemma Always_LeadsToD: "⟦F ∈ Always(C); F ∈ A ⟼w A'⟧ ⟹ F ∈ A ⟼w (C ∩ A')"
by (blast intro: Always_LeadsTo_post [THEN iffD2])
lemma LeadsTo_Basis: "F ∈ A Ensures B ⟹ F ∈ A ⟼w B"
by (auto simp add: Ensures_def LeadsTo_def)
lemma LeadsTo_Trans:
"⟦F ∈ A ⟼w B; F ∈ B ⟼w C⟧ ⟹ F ∈ A ⟼w C"
apply (simp (no_asm_use) add: LeadsTo_def)
apply (blast intro: leadsTo_Trans)
done
lemma LeadsTo_Union:
"⟦(⋀A. A ∈ S ⟹ F ∈ A ⟼w B); F ∈ program⟧⟹F ∈ ⋃(S) ⟼w B"
apply (simp add: LeadsTo_def)
apply (subst Int_Union_Union2)
apply (rule leadsTo_UN, auto)
done
lemma leadsTo_imp_LeadsTo: "F ∈ A ⟼ B ⟹ F ∈ A ⟼w B"
apply (frule leadsToD2, clarify)
apply (simp (no_asm_simp) add: LeadsTo_eq)
apply (blast intro: leadsTo_weaken_L)
done
lemma LeadsTo_Un_duplicate: "F ∈ A ⟼w (A' ∪ A') ⟹ F ∈ A ⟼w A'"
by (simp add: Un_ac)
lemma LeadsTo_Un_duplicate2:
"F ∈ A ⟼w (A' ∪ C ∪ C) ⟹ F ∈ A ⟼w (A' ∪ C)"
by (simp add: Un_ac)
lemma LeadsTo_UN:
"⟦(⋀i. i ∈ I ⟹ F ∈ A(i) ⟼w B); F ∈ program⟧
⟹F:(⋃i ∈ I. A(i)) ⟼w B"
apply (simp add: LeadsTo_def)
apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)
apply (rule leadsTo_UN, auto)
done
lemma LeadsTo_Un:
"⟦F ∈ A ⟼w C; F ∈ B ⟼w C⟧ ⟹ F ∈ (A ∪ B) ⟼w C"
apply (subst Un_eq_Union)
apply (rule LeadsTo_Union)
apply (auto dest: LeadsTo_type [THEN subsetD])
done
lemma single_LeadsTo_I:
"⟦(⋀s. s ∈ A ⟹ F:{s} ⟼w B); F ∈ program⟧⟹F ∈ A ⟼w B"
apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)
done
lemma subset_imp_LeadsTo: "⟦A ⊆ B; F ∈ program⟧ ⟹ F ∈ A ⟼w B"
apply (simp (no_asm_simp) add: LeadsTo_def)
apply (blast intro: subset_imp_leadsTo)
done
lemma empty_LeadsTo: "F ∈ 0 ⟼w A ⟷ F ∈ program"
by (auto dest: LeadsTo_type [THEN subsetD]
intro: empty_subsetI [THEN subset_imp_LeadsTo])
declare empty_LeadsTo [iff]
lemma LeadsTo_state: "F ∈ A ⟼w state ⟷ F ∈ program"
by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
declare LeadsTo_state [iff]
lemma LeadsTo_weaken_R: "⟦F ∈ A ⟼w A'; A'<=B'⟧ ⟹ F ∈ A ⟼w B'"
unfolding LeadsTo_def
apply (auto intro: leadsTo_weaken_R)
done
lemma LeadsTo_weaken_L: "⟦F ∈ A ⟼w A'; B ⊆ A⟧ ⟹ F ∈ B ⟼w A'"
unfolding LeadsTo_def
apply (auto intro: leadsTo_weaken_L)
done
lemma LeadsTo_weaken: "⟦F ∈ A ⟼w A'; B<=A; A'<=B'⟧ ⟹ F ∈ B ⟼w B'"
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
lemma Always_LeadsTo_weaken:
"⟦F ∈ Always(C); F ∈ A ⟼w A'; C ∩ B ⊆ A; C ∩ A' ⊆ B'⟧
⟹ F ∈ B ⟼w B'"
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
done
lemma LeadsTo_Un_post: "F ∈ A ⟼w B ⟹ F:(A ∪ B) ⟼w B"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_Un subset_imp_LeadsTo)
lemma LeadsTo_Trans_Un: "⟦F ∈ A ⟼w B; F ∈ B ⟼w C⟧
⟹ F ∈ (A ∪ B) ⟼w C"
apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
done
lemma LeadsTo_Un_distrib: "(F ∈ (A ∪ B) ⟼w C) ⟷ (F ∈ A ⟼w C ∧ F ∈ B ⟼w C)"
by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
lemma LeadsTo_UN_distrib: "(F ∈ (⋃i ∈ I. A(i)) ⟼w B) ⟷ (∀i ∈ I. F ∈ A(i) ⟼w B) ∧ F ∈ program"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_UN LeadsTo_weaken_L)
lemma LeadsTo_Union_distrib: "(F ∈ ⋃(S) ⟼w B) ⟷ (∀A ∈ S. F ∈ A ⟼w B) ∧ F ∈ program"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_Union LeadsTo_weaken_L)
lemma EnsuresI: "⟦F:(A-B) Co (A ∪ B); F ∈ transient (A-B)⟧ ⟹ F ∈ A Ensures B"
apply (simp add: Ensures_def Constrains_eq_constrains)
apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2)
done
lemma Always_LeadsTo_Basis: "⟦F ∈ Always(I); F ∈ (I ∩ (A-A')) Co (A ∪ A');
F ∈ transient (I ∩ (A-A'))⟧
⟹ F ∈ A ⟼w A'"
apply (rule Always_LeadsToI, assumption)
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done
lemma LeadsTo_Diff:
"⟦F ∈ (A-B) ⟼w C; F ∈ (A ∩ B) ⟼w C⟧ ⟹ F ∈ A ⟼w C"
by (blast intro: LeadsTo_Un LeadsTo_weaken)
lemma LeadsTo_UN_UN:
"⟦(⋀i. i ∈ I ⟹ F ∈ A(i) ⟼w A'(i)); F ∈ program⟧
⟹ F ∈ (⋃i ∈ I. A(i)) ⟼w (⋃i ∈ I. A'(i))"
apply (rule LeadsTo_Union, auto)
apply (blast intro: LeadsTo_weaken_R)
done
lemma LeadsTo_Un_Un:
"⟦F ∈ A ⟼w A'; F ∈ B ⟼w B'⟧ ⟹ F:(A ∪ B) ⟼w (A' ∪ B')"
by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
lemma LeadsTo_cancel2: "⟦F ∈ A ⟼w(A' ∪ B); F ∈ B ⟼w B'⟧ ⟹ F ∈ A ⟼w (A' ∪ B')"
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
lemma Un_Diff: "A ∪ (B - A) = A ∪ B"
by auto
lemma LeadsTo_cancel_Diff2: "⟦F ∈ A ⟼w (A' ∪ B); F ∈ (B-A') ⟼w B'⟧ ⟹ F ∈ A ⟼w (A' ∪ B')"
apply (rule LeadsTo_cancel2)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: Un_Diff)
done
lemma LeadsTo_cancel1: "⟦F ∈ A ⟼w (B ∪ A'); F ∈ B ⟼w B'⟧ ⟹ F ∈ A ⟼w (B' ∪ A')"
apply (simp add: Un_commute)
apply (blast intro!: LeadsTo_cancel2)
done
lemma Diff_Un2: "(B - A) ∪ A = B ∪ A"
by auto
lemma LeadsTo_cancel_Diff1: "⟦F ∈ A ⟼w (B ∪ A'); F ∈ (B-A') ⟼w B'⟧ ⟹ F ∈ A ⟼w (B' ∪ A')"
apply (rule LeadsTo_cancel1)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: Diff_Un2)
done
lemma LeadsTo_empty: "F ∈ A ⟼w 0 ⟹ F ∈ Always (state -A)"
apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
apply (cut_tac reachable_type)
apply (auto dest!: leadsTo_empty)
done
lemma PSP_Stable: "⟦F ∈ A ⟼w A'; F ∈ Stable(B)⟧⟹ F:(A ∩ B) ⟼w (A' ∩ B)"
apply (simp add: LeadsTo_def Stable_eq_stable, clarify)
apply (drule psp_stable, assumption)
apply (simp add: Int_ac)
done
lemma PSP_Stable2: "⟦F ∈ A ⟼w A'; F ∈ Stable(B)⟧ ⟹ F ∈ (B ∩ A) ⟼w (B ∩ A')"
apply (simp (no_asm_simp) add: PSP_Stable Int_ac)
done
lemma PSP: "⟦F ∈ A ⟼w A'; F ∈ B Co B'⟧⟹ F ∈ (A ∩ B') ⟼w ((A' ∩ B) ∪ (B' - B))"
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
apply (blast dest: psp intro: leadsTo_weaken)
done
lemma PSP2: "⟦F ∈ A ⟼w A'; F ∈ B Co B'⟧⟹ F:(B' ∩ A) ⟼w ((B ∩ A') ∪ (B' - B))"
by (simp (no_asm_simp) add: PSP Int_ac)
lemma PSP_Unless:
"⟦F ∈ A ⟼w A'; F ∈ B Unless B'⟧⟹ F:(A ∩ B) ⟼w ((A' ∩ B) ∪ B')"
unfolding op_Unless_def
apply (drule PSP, assumption)
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
done
lemma LeadsTo_wf_induct: "⟦wf(r);
∀m ∈ I. F ∈ (A ∩ f-``{m}) ⟼w
((A ∩ f-``(converse(r) `` {m})) ∪ B);
field(r)<=I; A<=f-``I; F ∈ program⟧
⟹ F ∈ A ⟼w B"
apply (simp (no_asm_use) add: LeadsTo_def)
apply auto
apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe)
apply (drule_tac [2] x = m in bspec, safe)
apply (rule_tac [2] A' = "reachable (F) ∩ (A ∩ f -`` (converse (r) ``{m}) ∪ B) " in leadsTo_weaken_R)
apply (auto simp add: Int_assoc)
done
lemma LessThan_induct: "⟦∀m ∈ nat. F:(A ∩ f-``{m}) ⟼w ((A ∩ f-``m) ∪ B);
A<=f-``nat; F ∈ program⟧ ⟹ F ∈ A ⟼w B"
apply (rule_tac A1 = nat and f1 = "λx. x" in wf_measure [THEN LeadsTo_wf_induct])
apply (simp_all add: nat_measure_field)
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
done
lemma Completion: "⟦F ∈ A ⟼w (A' ∪ C); F ∈ A' Co (A' ∪ C);
F ∈ B ⟼w (B' ∪ C); F ∈ B' Co (B' ∪ C)⟧
⟹ F ∈ (A ∩ B) ⟼w ((A' ∩ B') ∪ C)"
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib)
apply (blast intro: completion leadsTo_weaken)
done
lemma Finite_completion_aux:
"⟦I ∈ Fin(X);F ∈ program⟧
⟹ (∀i ∈ I. F ∈ (A(i)) ⟼w (A'(i) ∪ C)) ⟶
(∀i ∈ I. F ∈ (A'(i)) Co (A'(i) ∪ C)) ⟶
F ∈ (⋂i ∈ I. A(i)) ⟼w ((⋂i ∈ I. A'(i)) ∪ C)"
apply (erule Fin_induct)
apply (auto simp del: INT_simps simp add: Inter_0)
apply (rule Completion, auto)
apply (simp del: INT_simps add: INT_extend_simps)
apply (blast intro: Constrains_INT)
done
lemma Finite_completion:
"⟦I ∈ Fin(X); ⋀i. i ∈ I ⟹ F ∈ A(i) ⟼w (A'(i) ∪ C);
⋀i. i ∈ I ⟹ F ∈ A'(i) Co (A'(i) ∪ C);
F ∈ program⟧
⟹ F ∈ (⋂i ∈ I. A(i)) ⟼w ((⋂i ∈ I. A'(i)) ∪ C)"
by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
lemma Stable_completion:
"⟦F ∈ A ⟼w A'; F ∈ Stable(A');
F ∈ B ⟼w B'; F ∈ Stable(B')⟧
⟹ F ∈ (A ∩ B) ⟼w (A' ∩ B')"
unfolding Stable_def
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
prefer 5
apply blast
apply auto
done
lemma Finite_stable_completion:
"⟦I ∈ Fin(X);
(⋀i. i ∈ I ⟹ F ∈ A(i) ⟼w A'(i));
(⋀i. i ∈ I ⟹F ∈ Stable(A'(i))); F ∈ program⟧
⟹ F ∈ (⋂i ∈ I. A(i)) ⟼w (⋂i ∈ I. A'(i))"
unfolding Stable_def
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
apply (rule_tac [3] subset_refl, auto)
done
ML ‹
fun ensures_tac ctxt sact =
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac ctxt 1),
eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
ORELSE
REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>‹program›)) 2,
Rule_Insts.res_inst_tac ctxt
[((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
simp_tac (ctxt addsimps [@{thm domain_def}]) 3,
clarify_tac ctxt 3,
dresolve_tac ctxt @{thms swap} 3, force_tac ctxt 4,
resolve_tac ctxt @{thms ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,
asm_full_simp_tac ctxt 3, resolve_tac ctxt @{thms conjI} 3, simp_tac ctxt 4,
REPEAT (resolve_tac ctxt @{thms state_update_type} 3),
constrains_tac ctxt 1,
ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac (ctxt addsimps [@{thm st_set_def}])),
ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_lr_simp_tac ctxt)]);
›
method_setup ensures = ‹
Args.goal_spec -- Scan.lift Parse.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
› "for proving progress properties"
end