# Theory ELT

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

leadsTo strengthened with a specification of the allowable sets transient parts

TRY INSTEAD (to get rid of the {} and to gain strong induction)

elt :: "['a set set, 'a program, 'a set] => ('a set) set"

inductive "elt CC F B"
intros

Weaken:  "A <= B ==> A : elt CC F B"

ETrans:  "[| F : A ensures A';  A-A' : CC;  A' : elt CC F B |]
==> A : elt CC F B"

Union:  "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B"

monos Pow_mono
*)

section‹Progress Under Allowable Sets›

theory ELT imports Project begin

inductive_set
(*LEADS-TO constant for the inductive definition*)
elt :: "['a set set, 'a program] => ('a set * 'a set) set"
for CC :: "'a set set" and F :: "'a program"
where

Basis:  "[| F ∈ A ensures B;  A-B ∈ (insert {} CC) |] ==> (A,B) ∈ elt CC F"

| Trans:  "[| (A,B) ∈ elt CC F;  (B,C) ∈ elt CC F |] ==> (A,C) ∈ elt CC F"

| Union:  "∀A∈S. (A,B) ∈ elt CC F ==> (Union S, B) ∈ elt CC F"

definition
(*the set of all sets determined by f alone*)
givenBy :: "['a => 'b] => 'a set set"
where "givenBy f = range (%B. f-` B)"

definition
(*visible version of the LEADS-TO relation*)
leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
where "leadsETo A CC B = {F. (A,B) ∈ elt CC F}"

definition
LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
where "LeadsETo A CC B =
{F. F ∈ (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}"

(*** givenBy ***)

lemma givenBy_id [simp]: "givenBy id = UNIV"
by (unfold givenBy_def, auto)

lemma givenBy_eq_all: "(givenBy v) = {A. ∀x∈A. ∀y. v x = v y ⟶ y ∈ A}"
apply (unfold givenBy_def, safe)
apply (rule_tac [2] x = "v ` _" in image_eqI, auto)
done

lemma givenByI: "(⋀x y. [| x ∈ A;  v x = v y |] ==> y ∈ A) ==> A ∈ givenBy v"
by (subst givenBy_eq_all, blast)

lemma givenByD: "[| A ∈ givenBy v;  x ∈ A;  v x = v y |] ==> y ∈ A"
by (unfold givenBy_def, auto)

lemma empty_mem_givenBy [iff]: "{} ∈ givenBy v"
by (blast intro!: givenByI)

lemma givenBy_imp_eq_Collect: "A ∈ givenBy v ==> ∃P. A = {s. P(v s)}"
apply (rule_tac x = "λn. ∃s. v s = n ∧ s ∈ A" in exI)
apply blast
done

lemma Collect_mem_givenBy: "{s. P(v s)} ∈ givenBy v"
by (unfold givenBy_def, best)

lemma givenBy_eq_Collect: "givenBy v = {A. ∃P. A = {s. P(v s)}}"
by (blast intro: Collect_mem_givenBy givenBy_imp_eq_Collect)

(*preserving v preserves properties given by v*)
lemma preserves_givenBy_imp_stable:
"[| F ∈ preserves v;  D ∈ givenBy v |] ==> F ∈ stable D"
by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)

lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v"
apply best
done

lemma givenBy_DiffI:
"[| A ∈ givenBy v;  B ∈ givenBy v |] ==> A-B ∈ givenBy v"
apply safe
apply (rule_tac x = "%z. R z & ~ Q z" for R Q in exI)
unfolding set_diff_eq
apply auto
done

"[| F ∈ A ensures B;  A-B ∈ insert {} CC |] ==> F ∈ A leadsTo[CC] B"
apply (blast intro: elt.Basis)
done

"[| F ∈ A leadsTo[CC] B;  F ∈ B leadsTo[CC] C |] ==> F ∈ A leadsTo[CC] C"
apply (blast intro: elt.Trans)
done

(*Useful with cancellation, disjunction*)
"F ∈ A leadsTo[CC] (A' ∪ A') ⟹ F ∈ A leadsTo[CC] A'"

"F ∈ A leadsTo[CC] (A' ∪ C ∪ C) ==> F ∈ A leadsTo[CC] (A' Un C)"

(*The Union introduction rule as we should have liked to state it*)
"(⋀A. A ∈ S ⟹ F ∈ A leadsTo[CC] B) ⟹ F ∈ (⋃S) leadsTo[CC] B"
apply (blast intro: elt.Union)
done

"(⋀i. i ∈ I ⟹ F ∈ (A i) leadsTo[CC] B)
==> F ∈ (UN i:I. A i) leadsTo[CC] B"
done

(*The INDUCTION rule as we should have liked to state it*)
"[| F ∈ za leadsTo[CC] zb;
!!A B. [| F ∈ A ensures B;  A-B ∈ insert {} CC |] ==> P A B;
!!A B C. [| F ∈ A leadsTo[CC] B; P A B; F ∈ B leadsTo[CC] C; P B C |]
==> P A C;
!!B S. ∀A∈S. F ∈ A leadsTo[CC] B & P A B ==> P (⋃S) B
|] ==> P za zb"
apply (drule CollectD)
apply (erule elt.induct, blast+)
done

(** New facts involving leadsETo **)

apply safe
prefer 3 apply (blast intro: leadsETo_Union)
prefer 2 apply (blast intro: leadsETo_Trans)
apply blast
done

"[| F ∈ A leadsTo[CC] B;  F ∈ B leadsTo[DD] C |]
==> F ∈ A leadsTo[CC Un DD] C"

"(!!A. A ∈ S ==> F ∈ (A Int C) leadsTo[CC] B)
==> F ∈ (⋃S Int C) leadsTo[CC] B"
apply (simp only: Int_Union_Union)
apply (blast intro: elt.Union)
done

(*Binary union introduction rule*)
"[| F ∈ A leadsTo[CC] C; F ∈ B leadsTo[CC] C |]
==> F ∈ (A Un B) leadsTo[CC] C"
using leadsETo_Union [of "{A, B}" F CC C] by auto

"(⋀x. x ∈ A ==> F ∈ {x} leadsTo[CC] B) ⟹ F ∈ A leadsTo[CC] B"
by (subst UN_singleton [symmetric], rule leadsETo_UN, blast)

Diff_eq_empty_iff [THEN iffD2])

(** Weakening laws **)

"[| F ∈ A leadsTo[CC] A';  A'<=B' |] ==> F ∈ A leadsTo[CC] B'"

"[| F ∈ A leadsTo[CC] A'; B<=A |] ==> F ∈ B leadsTo[CC] A'"

(*Distributes over binary unions*)
"F ∈ (A Un B) leadsTo[CC] C  =

"F ∈ (UN i:I. A i) leadsTo[CC] B  =
(∀i∈I. F ∈ (A i) leadsTo[CC] B)"

"F ∈ (⋃S) leadsTo[CC] B  =  (∀A∈S. F ∈ A leadsTo[CC] B)"

"[| F ∈ A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC |]
==> F ∈ B leadsTo[CC] B'"
apply (drule leadsETo_mono [THEN subsetD], assumption)
apply (blast del: subsetCE
done

"[| F ∈ A leadsTo[CC] A';  CC <= givenBy v |]
==> F ∈ A leadsTo[givenBy v] A'"

(*Set difference*)
"[| F ∈ (A-B) leadsTo[CC] C; F ∈ B leadsTo[CC] C |]
==> F ∈ A leadsTo[CC] C"

(*Binary union version*)
"[| F ∈ A leadsTo[CC] A';  F ∈ B leadsTo[CC] B' |]
==> F ∈ (A Un B) leadsTo[CC] (A' Un B')"

(** The cancellation law **)

"[| F ∈ A leadsTo[CC] (A' Un B); F ∈ B leadsTo[CC] B' |]
==> F ∈ A leadsTo[CC] (A' Un B')"

"[| F ∈ A leadsTo[CC] (B Un A'); F ∈ B leadsTo[CC] B' |]
==> F ∈ A leadsTo[CC] (B' Un A')"
done

"[| F ∈ A leadsTo[CC] (B Un A'); F ∈ (B-A') leadsTo[CC] B' |]
==> F ∈ A leadsTo[CC] (B' Un A')"
prefer 2 apply assumption
apply simp_all
done

(** PSP: Progress-Safety-Progress **)

(*Special case of PSP: Misra's "stable conjunction"*)
lemma e_psp_stable:
"[| F ∈ A leadsTo[CC] A';  F ∈ stable B;  ∀C∈CC. C Int B ∈ CC |]
==> F ∈ (A Int B) leadsTo[CC] (A' Int B)"
apply (unfold stable_def)
prefer 3 apply (blast intro: leadsETo_Union_Int)
prefer 2 apply (blast intro: leadsETo_Trans)
prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric])
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric]
Int_Un_distrib2 [symmetric])
apply (blast intro: transient_strengthen constrains_Int)
done

lemma e_psp_stable2:
"[| F ∈ A leadsTo[CC] A'; F ∈ stable B;  ∀C∈CC. C Int B ∈ CC |]
==> F ∈ (B Int A) leadsTo[CC] (B Int A')"
by (simp (no_asm_simp) add: e_psp_stable Int_ac)

lemma e_psp:
"[| F ∈ A leadsTo[CC] A'; F ∈ B co B';
∀C∈CC. C Int B Int B' ∈ CC |]
==> F ∈ (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))"
prefer 3 apply (blast intro: leadsETo_Union_Int)
(*Transitivity case has a delicate argument involving "cancellation"*)
prefer 2
apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset)
(*Basis case*)
apply (blast intro: psp_ensures)
apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'")
apply auto
done

lemma e_psp2:
"[| F ∈ A leadsTo[CC] A'; F ∈ B co B';
∀C∈CC. C Int B Int B' ∈ CC |]
==> F ∈ (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))"

(*** Special properties involving the parameter [CC] ***)

(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
"[| F ∈ (A leadsTo[givenBy v] B);  G ∈ preserves v;
F⊔G ∈ stable C |]
==> F⊔G ∈ ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
prefer 3
apply (subst Int_Union)
prefer 2
apply (auto simp add: Diff_eq_empty_iff [THEN iffD2]
Int_Diff ensures_def givenBy_eq_Collect)
prefer 3 apply (blast intro: transient_strengthen)
apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
apply (unfold stable_def)
apply (blast intro: constrains_Int [THEN constrains_weaken])+
done

(** strong **)

apply safe
prefer 3 apply (blast intro: leadsTo_Union)
prefer 2 apply (blast intro: leadsTo_Trans, blast)
done

apply safe
(*right-to-left case*)
prefer 3 apply (blast intro: leadsETo_Union)
prefer 2 apply (blast intro: leadsETo_Trans, blast)
done

(**** weak ****)

{F. F ∈ (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC]
(reachable F Int B)}"
apply (blast dest: e_psp_stable2 intro: leadsETo_weaken)
done

(*** Introduction rules: Basis, Trans, Union ***)

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

"(⋀A. A ∈ S ⟹ F ∈ A LeadsTo[CC] B) ⟹ F ∈ (⋃S) LeadsTo[CC] B"
apply (subst Int_Union)
done

"(⋀i. i ∈ I ⟹ F ∈ (A i) LeadsTo[CC] B)
⟹ F ∈ (UN i:I. A i) LeadsTo[CC] B"
done

(*Binary union introduction rule*)
"[| F ∈ A LeadsTo[CC] C; F ∈ B LeadsTo[CC] C |]
==> F ∈ (A Un B) LeadsTo[CC] C"
using LeadsETo_Union [of "{A, B}" F CC C] by auto

(*Lets us look at the starting state*)
"(⋀s. s ∈ A ==> F ∈ {s} LeadsTo[CC] B) ⟹ F ∈ A LeadsTo[CC] B"
by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)

"A <= B ⟹ F ∈ A LeadsTo[CC] B"
done

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

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

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

done

(*Postcondition can be strengthened to (reachable F Int B) *)
lemma reachable_ensures:
"F ∈ A ensures B ⟹ F ∈ (reachable F Int A) ensures B"
apply (rule stable_ensures_Int [THEN ensures_weaken_R], auto)
done

lemma lel_lemma:
"F ∈ A leadsTo B ⟹ F ∈ (reachable F Int A) leadsTo[Pow(reachable F)] B"
apply (blast intro: reachable_ensures)
apply (subst Int_Union)
done

apply safe
(*right-to-left case*)
apply (blast intro: lel_lemma [THEN leadsETo_weaken])
done

(**** EXTEND/PROJECT PROPERTIES ****)

context Extend
begin

lemma givenBy_o_eq_extend_set:
"givenBy (v o f) = extend_set h ` (givenBy v)"
apply (rule equalityI, best)
apply blast
done

lemma givenBy_eq_extend_set: "givenBy f = range (extend_set h)"

lemma extend_set_givenBy_I:
"D ∈ givenBy v ==> extend_set h D ∈ givenBy (v o f)"
apply (simp (no_asm_use) add: givenBy_eq_all, blast)
done

==> extend h F ∈ (extend_set h A) leadsTo[extend_set h ` CC]
(extend_set h B)"
apply (force intro: subset_imp_ensures
done

(*This version's stronger in the "ensures" precondition
BUT there's no ensures_weaken_L*)
lemma Join_project_ensures_strong:
"[| project h C G ∉ transient (project_set h C Int (A-B)) |
project_set h C Int (A - B) = {};
extend h F⊔G ∈ stable C;
F⊔project h C G ∈ (project_set h C Int A) ensures B |]
==> extend h F⊔G ∈ (C Int extend_set h A) ensures (extend_set h B)"
apply (subst Int_extend_set_lemma [symmetric])
apply (rule Join_project_ensures)
done

(*NOT WORKING.  MODIFY AS IN Project.thy
lemma pld_lemma:
"[| extend h F⊔G : stable C;
F⊔project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;
G : preserves (v o f) |]
==> extend h F⊔G :
(C Int extend_set h (project_set h C Int A))
leadsTo[(%D. C Int extend_set h D)`givenBy v]  (extend_set h B)"
prefer 3
prefer 2
txt{*Base case is hard*}
apply auto
prefer 2
apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
apply (rule Join_project_ensures_strong)
apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
done

"[| extend h F⊔G : stable C;
F⊔project h C G :
(project_set h C Int A)
leadsTo[(%D. project_set h C Int D)`givenBy v] B;
G : preserves (v o f) |]
==> extend h F⊔G : (C Int extend_set h A)
leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
done

"[| F⊔project h UNIV G : A leadsTo[givenBy v] B;
G : preserves (v o f) |]
==> extend h F⊔G : (extend_set h A)
leadsTo[givenBy (v o f)] (extend_set h B)"
apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto)
apply (rule givenBy_o_eq_extend_set [THEN equalityD2])
done

"[| F⊔project h (reachable (extend h F⊔G)) G
G : preserves (v o f) |]
==> extend h F⊔G :
(extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)"
apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma])
apply (erule leadsETo_mono [THEN [2] rev_subsetD])
apply (blast intro: extend_set_givenBy_I)
done

"(ALL G. extend h F ok G --> G : preserves (v o f))
==> extending (%G. UNIV) h F
(extend_set h A leadsTo[givenBy (v o f)] extend_set h B)
apply (unfold extending_def)
done

"(ALL G. extend h F ok G --> G : preserves (v o f))
==> extending (%G. reachable (extend h F⊔G)) h F
(extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)
apply (unfold extending_def)
done
*)

(*** leadsETo in the precondition ***)

(*Lemma for the Trans case*)
lemma pli_lemma:
"[| extend h F⊔G ∈ stable C;
F⊔project h C G
∈ project_set h C Int project_set h A leadsTo project_set h B |]
==> F⊔project h C G
∈ project_set h C Int project_set h A leadsTo
project_set h C Int project_set h B"
apply (auto simp add: project_stable_project_set extend_stable_project_set)
done

"[| extend h F⊔G ∈ stable C;
extend h F⊔G ∈
(C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]
==> F⊔project h C G
∈ (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
prefer 3
apply (simp only: Int_UN_distrib project_set_Union)
prefer 2 apply (blast intro: leadsTo_Trans pli_lemma)
apply (blast intro: ensures_extend_set_imp_project_ensures)
done

"extend h F⊔G ∈ (extend_set h A) leadsTo[givenBy f] (extend_set h B)
⟹ F⊔project h UNIV G ∈ A leadsTo B"
done

"extend h F⊔G ∈ (extend_set h A) LeadsTo[givenBy f] (extend_set h B)
⟹ F⊔project h (reachable (extend h F⊔G)) G
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
done

"projecting (λG. UNIV) h F
(extend_set h A leadsTo[givenBy f] extend_set h B)
apply (unfold projecting_def)
done