# Theory SubstAx

theory SubstAx
imports WFair Constrains
```(*  Title:      HOL/UNITY/SubstAx.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Weak LeadsTo relation (restricted to the set of reachable states)
*)

section‹Weak Progress›

theory SubstAx imports WFair Constrains begin

definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where
"A Ensures B == {F. F ∈ (reachable F ∩ A) ensures B}"

definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where
"A LeadsTo B == {F. F ∈ (reachable F ∩ A) leadsTo B}"

text‹Resembles the previous definition of LeadsTo›
"A LeadsTo B = {F. F ∈ (reachable F ∩ A) leadsTo (reachable F ∩ B)}"
apply (blast dest: psp_stable2 intro: leadsTo_weaken)
done

subsection‹Specialized laws for handling invariants›

(** Conjoining an Always property **)

"F ∈ Always INV ==> (F ∈ (INV ∩ A) LeadsTo A') = (F ∈ A LeadsTo A')"
Int_assoc [symmetric])

"F ∈ Always INV ==> (F ∈ A LeadsTo (INV ∩ A')) = (F ∈ A LeadsTo A')"
Int_assoc [symmetric])

(* [| F ∈ Always C;  F ∈ (C ∩ A) LeadsTo A' |] ==> F ∈ A LeadsTo A' *)

(* [| F ∈ Always INV;  F ∈ A LeadsTo A' |] ==> F ∈ A LeadsTo (INV ∩ A') *)

subsection‹Introduction rules: Basis, Trans, Union›

done

"[| F ∈ A LeadsTo B;  F ∈ B LeadsTo C |] ==> F ∈ A LeadsTo C"
done

"(!!A. A ∈ S ==> F ∈ A LeadsTo B) ==> F ∈ (⋃S) LeadsTo B"
apply (subst Int_Union)
done

subsection‹Derived rules›

text‹Useful with cancellation, disjunction›
"F ∈ A LeadsTo (A' ∪ A') ==> F ∈ A LeadsTo A'"

"F ∈ A LeadsTo (A' ∪ C ∪ C) ==> F ∈ A LeadsTo (A' ∪ C)"

"(!!i. i ∈ I ==> F ∈ (A i) LeadsTo B) ==> F ∈ (⋃i ∈ I. A i) LeadsTo B"
done

text‹Binary union introduction rule›
"[| F ∈ A LeadsTo C; F ∈ B LeadsTo C |] ==> F ∈ (A ∪ B) LeadsTo C"
using LeadsTo_UN [of "{A, B}" F id C] by auto

text‹Lets us look at the starting state›
"(!!s. s ∈ A ==> F ∈ {s} LeadsTo B) ==> F ∈ A LeadsTo B"
by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)

done

"[| F ∈ A LeadsTo A';  A' ⊆ B' |] ==> F ∈ A LeadsTo B'"
done

"[| F ∈ A LeadsTo A';  B ⊆ A |]
==> F ∈ B LeadsTo A'"
done

"[| F ∈ A LeadsTo A';
B  ⊆ A;   A' ⊆ B' |]
==> F ∈ B LeadsTo B'"

"[| F ∈ Always C;  F ∈ A LeadsTo A';
C ∩ B ⊆ A;   C ∩ A' ⊆ B' |]
==> F ∈ B LeadsTo B'"

(** Two theorems for "proof lattices" **)

"[| F ∈ A LeadsTo B;  F ∈ B LeadsTo C |]
==> F ∈ (A ∪ B) LeadsTo C"

(** Distributive laws **)

"(F ∈ (A ∪ B) LeadsTo C)  = (F ∈ A LeadsTo C & F ∈ B LeadsTo C)"

"(F ∈ (⋃i ∈ I. A i) LeadsTo B)  =  (∀i ∈ I. F ∈ (A i) LeadsTo B)"

"(F ∈ (⋃S) LeadsTo B)  =  (∀A ∈ S. F ∈ A LeadsTo B)"

(** More rules using the premise "Always INV" **)

lemma LeadsTo_Basis: "F ∈ A Ensures B ==> F ∈ A LeadsTo B"

lemma EnsuresI:
"[| F ∈ (A-B) Co (A ∪ B);  F ∈ transient (A-B) |]
==> F ∈ A Ensures B"
apply (blast intro: ensuresI constrains_weaken transient_strengthen)
done

"[| F ∈ Always INV;
F ∈ (INV ∩ (A-A')) Co (A ∪ A');
F ∈ transient (INV ∩ (A-A')) |]
==> F ∈ A LeadsTo A'"
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done

text‹Set difference: maybe combine with ‹leadsTo_weaken_L›??
This is the most useful form of the "disjunction" rule›
"[| F ∈ (A-B) LeadsTo C;  F ∈ (A ∩ B) LeadsTo C |]
==> F ∈ A LeadsTo C"

"(!! i. i ∈ I ==> F ∈ (A i) LeadsTo (A' i))
==> F ∈ (⋃i ∈ I. A i) LeadsTo (⋃i ∈ I. A' i)"
done

text‹Version with no index set›
"(!!i. F ∈ (A i) LeadsTo (A' i)) ==> F ∈ (⋃i. A i) LeadsTo (⋃i. A' i)"

text‹Version with no index set›
"∀i. F ∈ (A i) LeadsTo (A' i)
==> F ∈ (⋃i. A i) LeadsTo (⋃i. A' i)"

text‹Binary union version›
"[| F ∈ A LeadsTo A'; F ∈ B LeadsTo B' |]
==> F ∈ (A ∪ B) LeadsTo (A' ∪ B')"

(** The cancellation law **)

"[| F ∈ A LeadsTo (A' ∪ B); F ∈ B LeadsTo B' |]
==> F ∈ A LeadsTo (A' ∪ B')"

"[| F ∈ A LeadsTo (A' ∪ B); F ∈ (B-A') LeadsTo B' |]
==> F ∈ A LeadsTo (A' ∪ B')"
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
done

"[| F ∈ A LeadsTo (B ∪ A'); F ∈ B LeadsTo B' |]
==> F ∈ A LeadsTo (B' ∪ A')"
done

"[| F ∈ A LeadsTo (B ∪ A'); F ∈ (B-A') LeadsTo B' |]
==> F ∈ A LeadsTo (B' ∪ A')"
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
done

text‹The impossibility law›

text‹The set "A" may be non-empty, but it contains no reachable states›
lemma LeadsTo_empty: "[|F ∈ A LeadsTo {}; all_total F|] ==> F ∈ Always (-A)"
done

subsection‹PSP: Progress-Safety-Progress›

text‹Special case of PSP: Misra's "stable conjunction"›
lemma PSP_Stable:
"[| F ∈ A LeadsTo A';  F ∈ Stable B |]
==> F ∈ (A ∩ B) LeadsTo (A' ∩ B)"
apply (drule psp_stable, assumption)
done

lemma PSP_Stable2:
"[| F ∈ A LeadsTo A'; F ∈ Stable B |]
==> F ∈ (B ∩ A) LeadsTo (B ∩ A')"

lemma PSP:
"[| F ∈ A LeadsTo A'; F ∈ B Co B' |]
==> F ∈ (A ∩ B') LeadsTo ((A' ∩ B) ∪ (B' - B))"
apply (blast dest: psp intro: leadsTo_weaken)
done

lemma PSP2:
"[| F ∈ A LeadsTo A'; F ∈ B Co B' |]
==> F ∈ (B' ∩ A) LeadsTo ((B ∩ A') ∪ (B' - B))"

lemma PSP_Unless:
"[| F ∈ A LeadsTo A'; F ∈ B Unless B' |]
==> F ∈ (A ∩ B) LeadsTo ((A' ∩ B) ∪ B')"
apply (unfold Unless_def)
apply (drule PSP, assumption)
done

"[| F ∈ Stable A;  F ∈ transient C;
F ∈ Always (-A ∪ B ∪ C) |] ==> F ∈ A LeadsTo B"
prefer 2
apply (erule
done

subsection‹Induction rules›

(** Meta or object quantifier ????? **)
"[| wf r;
∀m. F ∈ (A ∩ f-`{m}) LeadsTo
((A ∩ f-`(r^-1 `` {m})) ∪ B) |]
==> F ∈ A LeadsTo B"
done

lemma Bounded_induct:
"[| wf r;
∀m ∈ I. F ∈ (A ∩ f-`{m}) LeadsTo
((A ∩ f-`(r^-1 `` {m})) ∪ B) |]
==> F ∈ A LeadsTo ((A - (f-`I)) ∪ B)"
apply (case_tac "m ∈ I")
done

lemma LessThan_induct:
"(!!m::nat. F ∈ (A ∩ f-`{m}) LeadsTo ((A ∩ f-`(lessThan m)) ∪ B))
==> F ∈ A LeadsTo B"
by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)

text‹Integer version.  Could generalize from 0 to any lower bound›
lemma integ_0_le_induct:
"[| F ∈ Always {s. (0::int) ≤ f s};
!! z. F ∈ (A ∩ {s. f s = z}) LeadsTo
((A ∩ {s. f s < z}) ∪ B) |]
==> F ∈ A LeadsTo B"
apply (rule_tac f = "nat o f" in LessThan_induct)
apply (auto simp add: nat_eq_iff nat_less_iff)
done

lemma LessThan_bounded_induct:
"!!l::nat. ∀m ∈ greaterThan l.
F ∈ (A ∩ f-`{m}) LeadsTo ((A ∩ f-`(lessThan m)) ∪ B)
==> F ∈ A LeadsTo ((A ∩ (f-`(atMost l))) ∪ B)"
apply (simp only: Diff_eq [symmetric] vimage_Compl
Compl_greaterThan [symmetric])
apply (rule wf_less_than [THEN Bounded_induct], simp)
done

lemma GreaterThan_bounded_induct:
"!!l::nat. ∀m ∈ lessThan l.
F ∈ (A ∩ f-`{m}) LeadsTo ((A ∩ f-`(greaterThan m)) ∪ B)
==> F ∈ A LeadsTo ((A ∩ (f-`(atLeast l))) ∪ B)"
apply (rule_tac f = f and f1 = "%k. l - k"
in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
apply (case_tac "m<l")
done

subsection‹Completion: Binary and General Finite versions›

lemma Completion:
"[| F ∈ A LeadsTo (A' ∪ C);  F ∈ A' Co (A' ∪ C);
F ∈ B LeadsTo (B' ∪ C);  F ∈ B' Co (B' ∪ C) |]
==> F ∈ (A ∩ B) LeadsTo ((A' ∩ B') ∪ C)"
done

lemma Finite_completion_lemma:
"finite I
==> (∀i ∈ I. F ∈ (A i) LeadsTo (A' i ∪ C)) -->
(∀i ∈ I. F ∈ (A' i) Co (A' i ∪ C)) -->
F ∈ (⋂i ∈ I. A i) LeadsTo ((⋂i ∈ I. A' i) ∪ C)"
apply (erule finite_induct, auto)
apply (rule Completion)
prefer 4
apply (simp only: INT_simps [symmetric])
apply (rule Constrains_INT, auto)
done

lemma Finite_completion:
"[| finite I;
!!i. i ∈ I ==> F ∈ (A i) LeadsTo (A' i ∪ C);
!!i. i ∈ I ==> F ∈ (A' i) Co (A' i ∪ C) |]
==> F ∈ (⋂i ∈ I. A i) LeadsTo ((⋂i ∈ I. A' i) ∪ C)"
by (blast intro: Finite_completion_lemma [THEN mp, THEN mp])

lemma Stable_completion:
"[| F ∈ A LeadsTo A';  F ∈ Stable A';
F ∈ B LeadsTo B';  F ∈ Stable B' |]
==> F ∈ (A ∩ B) LeadsTo (A' ∩ B')"
apply (unfold Stable_def)
apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R])
apply (force+)
done

lemma Finite_stable_completion:
"[| finite I;
!!i. i ∈ I ==> F ∈ (A i) LeadsTo (A' i);
!!i. i ∈ I ==> F ∈ Stable (A' i) |]
==> F ∈ (⋂i ∈ I. A i) LeadsTo (⋂i ∈ I. A' i)"
apply (unfold Stable_def)
apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
apply (simp_all, blast+)
done

end
```