|
(* Title: ZF/UNITY/SubstAx.thy
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
Theory ported from HOL.
*)
section\<open>Weak LeadsTo relation (restricted to the set of reachable states)\<close>
theory SubstAx
imports WFair Constrains
begin
definition
(* The definitions below are not `conventional', but yield simpler rules *)
Ensures :: "[i,i] => i" (infixl \<open>Ensures\<close> 60) where
"A Ensures B == {F \ program. F \ (reachable(F) \ A) ensures (reachable(F) \ B) }"
definition
LeadsTo :: "[i, i] => i" (infixl \<open>\<longmapsto>w\<close> 60) where
"A \w B == {F \ program. F:(reachable(F) \ A) \ (reachable(F) \ B)}"
(*Resembles the previous definition of LeadsTo*)
(* Equivalence with the HOL-like definition *)
lemma LeadsTo_eq:
"st_set(B)==> A \w B = {F \ program. F:(reachable(F) \ A) \ B}"
apply (unfold 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)
(*** Specialized laws for handling invariants ***)
(** Conjoining an Always property **)
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')"
apply (unfold LeadsTo_def)
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
done
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
lemma Always_LeadsToI: "[| F \ Always(C); F \ (C \ A) \w A' |] ==> F \ A \w A'"
by (blast intro: Always_LeadsTo_pre [THEN iffD1])
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
lemma Always_LeadsToD: "[| F \ Always(C); F \ A \w A' |] ==> F \ A \w (C \ A')"
by (blast intro: Always_LeadsTo_post [THEN iffD2])
(*** Introduction rules \<in> Basis, Trans, Union ***)
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
(*** Derived rules ***)
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
(*Useful with cancellation, disjunction*)
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:(\<Union>i \<in> I. A(i)) \<longmapsto>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
(*Binary union introduction rule*)
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
(*Lets us look at the starting state*)
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'"
apply (unfold LeadsTo_def)
apply (auto intro: leadsTo_weaken_R)
done
lemma LeadsTo_weaken_L: "[| F \ A \w A'; B \ A |] ==> F \ B \w A'"
apply (unfold 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 \<in> B \<longmapsto>w B'"
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
done
(** Two theorems for "proof lattices" **)
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 \<in> (A \<union> B) \<longmapsto>w C"
apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
done
(** Distributive laws **)
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)
(** More rules using the premise "Always(I)" **)
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 \<in> transient (I \<inter> (A-A')) |]
==> F \<in> A \<longmapsto>w A'"
apply (rule Always_LeadsToI, assumption)
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
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 \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w (\<Union>i \<in> I. A'(i))"
apply (rule LeadsTo_Union, auto)
apply (blast intro: LeadsTo_weaken_R)
done
(*Binary union version*)
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)
(** The cancellation law **)
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
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
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
(** PSP \<in> Progress-Safety-Progress **)
(*Special case of PSP \<in> Misra's "stable conjunction"*)
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')"
apply (unfold op_Unless_def)
apply (drule PSP, assumption)
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
done
(*** Induction rules ***)
(** Meta or object quantifier ????? **)
lemma LeadsTo_wf_induct: "[| wf(r);
\<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto>w
((A \<inter> f-``(converse(r) `` {m})) \<union> B);
field(r)<=I; A<=f-``I; F \<in> program |]
==> F \<in> A \<longmapsto>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 \<in> program |] ==> F \<in> A \<longmapsto>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
(******
To be ported ??? I am not sure.
integ_0_le_induct
LessThan_bounded_induct
GreaterThan_bounded_induct
*****)
(*** Completion \<in> Binary and General Finite versions ***)
lemma Completion: "[| F \ A \w (A' \ C); F \ A' Co (A' \ C);
F \<in> B \<longmapsto>w (B' \<union> C); F \<in> B' Co (B' \<union> C) |]
==> F \<in> (A \<inter> B) \<longmapsto>w ((A' \<inter> B') \<union> 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 |]
==> (\<forall>i \<in> I. F \<in> (A(i)) \<longmapsto>w (A'(i) \<union> C)) \<longrightarrow>
(\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) \<union> C)) \<longrightarrow>
F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> 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 \<in> I ==> F \<in> A'(i) Co (A'(i) \<union> C);
F \<in> program |]
==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)"
by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
lemma Stable_completion:
"[| F \ A \w A'; F \ Stable(A');
F \<in> B \<longmapsto>w B'; F \<in> Stable(B') |]
==> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')"
apply (unfold 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 \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i));
(!!i. i \<in> I ==>F \<in> Stable(A'(i))); F \<in> program |]
==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))"
apply (unfold 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 \<open>
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac ctxt 1),
eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\<open>program\<close>)) 2,
Rule_Insts.res_inst_tac ctxt
[((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ctxt addsimps [@{thm domain_def}]) 3,
(* proving the domain part *)
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)]);
\<close>
method_setup ensures = \<open>
Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
\<close> "for proving progress properties"
end
¤ Dauer der Verarbeitung: 0.24 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.
|
