# Theory Extend

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

Extending of state setsExtending of state sets
function f (forget)    maps the extended state to the original state
function g (forgotten) maps the extended state to the "extending part"
*)

section‹Extending State Sets›

theory Extend imports Guar begin

definition
(*MOVE to Relation.thy?*)
Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
where "Restrict A r = r ∩ (A × UNIV)"

definition
good_map :: "['a*'b => 'c] => bool"
where "good_map h ⟷ surj h & (∀x y. fst (inv h (h (x,y))) = x)"
(*Using the locale constant "f", this is  f (h (x,y))) = x*)

definition
extend_set :: "['a*'b => 'c, 'a set] => 'c set"
where "extend_set h A = h ` (A × UNIV)"

definition
project_set :: "['a*'b => 'c, 'c set] => 'a set"
where "project_set h C = {x. ∃y. h(x,y) ∈ C}"

definition
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
where "extend_act h = (%act. ⋃(s,s') ∈ act. ⋃y. {(h(s,y), h(s',y))})"

definition
project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
where "project_act h act = {(x,x'). ∃y y'. (h(x,y), h(x',y')) ∈ act}"

definition
extend :: "['a*'b => 'c, 'a program] => 'c program"
where "extend h F = mk_program (extend_set h (Init F),
extend_act h ` Acts F,
project_act h -` AllowedActs F)"

definition
(*Argument C allows weak safety laws to be projected*)
project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
where "project h C F =
mk_program (project_set h (Init F),
project_act h ` Restrict C ` Acts F,
{act. Restrict (project_set h C) act :
project_act h ` Restrict C ` AllowedActs F})"

locale Extend =
fixes f     :: "'c => 'a"
and g     :: "'c => 'b"
and h     :: "'a*'b => 'c"    (*isomorphism between 'a * 'b and 'c *)
and slice :: "['c set, 'b] => 'a set"
assumes
good_h:  "good_map h"
defines f_def: "f z == fst (inv h z)"
and g_def: "g z == snd (inv h z)"
and slice_def: "slice Z y == {x. h(x,y) ∈ Z}"

(** These we prove OUTSIDE the locale. **)

subsection‹Restrict›
(*MOVE to Relation.thy?*)

lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x ∈ A)"
by (unfold Restrict_def, blast)

lemma Restrict_UNIV [simp]: "Restrict UNIV = id"
apply (rule ext)
done

lemma Restrict_empty [simp]: "Restrict {} r = {}"

lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A ∩ B) r"
by (unfold Restrict_def, blast)

lemma Restrict_triv: "Domain r ⊆ A ==> Restrict A r = r"
by (unfold Restrict_def, auto)

lemma Restrict_subset: "Restrict A r ⊆ r"
by (unfold Restrict_def, auto)

lemma Restrict_eq_mono:
"[| A ⊆ B;  Restrict B r = Restrict B s |]
==> Restrict A r = Restrict A s"
by (unfold Restrict_def, blast)

lemma Restrict_imageI:
"[| s ∈ RR;  Restrict A r = Restrict A s |]
==> Restrict A r ∈ Restrict A ` RR"
by (unfold Restrict_def image_def, auto)

lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A ∩ Domain r"
by blast

lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A ∩ B)"
by blast

(*Possibly easier than reasoning about "inv h"*)
lemma good_mapI:
assumes surj_h: "surj h"
and prem:   "!! x x' y y'. h(x,y) = h(x',y') ==> x=x'"
shows "good_map h"
apply (safe intro!: surj_h)
apply (rule prem)
apply (subst surjective_pairing [symmetric])
apply (subst surj_h [THEN surj_f_inv_f])
apply (rule refl)
done

lemma good_map_is_surj: "good_map h ==> surj h"
by (unfold good_map_def, auto)

(*A convenient way of finding a closed form for inv h*)
lemma fst_inv_equalityI:
assumes surj_h: "surj h"
and prem:   "!! x y. g (h(x,y)) = x"
shows "fst (inv h z) = g z"
by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)

subsection‹Trivial properties of f, g, h›

context Extend
begin

lemma f_h_eq [simp]: "f(h(x,y)) = x"
by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])

lemma h_inject1 [dest]: "h(x,y) = h(x',y') ==> x=x'"
apply (drule_tac f = f in arg_cong)
apply (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
done

lemma h_f_g_equiv: "h(f z, g z) == z"
good_h [unfolded good_map_def, THEN conjunct1, THEN surj_f_inv_f])

lemma h_f_g_eq: "h(f z, g z) = z"

lemma split_extended_all:
"(!!z. PROP P z) == (!!u y. PROP P (h (u, y)))"
proof
assume allP: "⋀z. PROP P z"
fix u y
show "PROP P (h (u, y))" by (rule allP)
next
assume allPh: "⋀u y. PROP P (h(u,y))"
fix z
have Phfgz: "PROP P (h (f z, g z))" by (rule allPh)
show "PROP P z" by (rule Phfgz [unfolded h_f_g_equiv])
qed

end

subsection‹@{term extend_set}: basic properties›

lemma project_set_iff [iff]:
"(x ∈ project_set h C) = (∃y. h(x,y) ∈ C)"

lemma extend_set_mono: "A ⊆ B ==> extend_set h A ⊆ extend_set h B"
by (unfold extend_set_def, blast)

context Extend
begin

lemma mem_extend_set_iff [iff]: "z ∈ extend_set h A = (f z ∈ A)"
apply (unfold extend_set_def)
apply (force intro: h_f_g_eq [symmetric])
done

lemma extend_set_strict_mono [iff]:
"(extend_set h A ⊆ extend_set h B) = (A ⊆ B)"
by (unfold extend_set_def, force)

lemma (in -) extend_set_empty [simp]: "extend_set h {} = {}"
by (unfold extend_set_def, auto)

lemma extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}"
by auto

lemma extend_set_sing: "extend_set h {x} = {s. f s = x}"
by auto

lemma extend_set_inverse [simp]: "project_set h (extend_set h C) = C"
by (unfold extend_set_def, auto)

lemma extend_set_project_set: "C ⊆ extend_set h (project_set h C)"
apply (unfold extend_set_def)
apply (auto simp add: split_extended_all, blast)
done

lemma inj_extend_set: "inj (extend_set h)"
apply (rule inj_on_inverseI)
apply (rule extend_set_inverse)
done

lemma extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
apply (unfold extend_set_def)
done

subsection‹@{term project_set}: basic properties›

(*project_set is simply image!*)
lemma project_set_eq: "project_set h C = f ` C"
by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)

(*Converse appears to fail*)
lemma project_set_I: "!!z. z ∈ C ==> f z ∈ project_set h C"

subsection‹More laws›

(*Because A and B could differ on the "other" part of the state,
cannot generalize to
project_set h (A ∩ B) = project_set h A ∩ project_set h B
*)
lemma project_set_extend_set_Int: "project_set h ((extend_set h A) ∩ B) = A ∩ (project_set h B)"
by auto

(*Unused, but interesting?*)
lemma project_set_extend_set_Un: "project_set h ((extend_set h A) ∪ B) = A ∪ (project_set h B)"
by auto

lemma (in -) project_set_Int_subset:
"project_set h (A ∩ B) ⊆ (project_set h A) ∩ (project_set h B)"
by auto

lemma extend_set_Un_distrib: "extend_set h (A ∪ B) = extend_set h A ∪ extend_set h B"
by auto

lemma extend_set_Int_distrib: "extend_set h (A ∩ B) = extend_set h A ∩ extend_set h B"
by auto

lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (⋂x ∈ A. extend_set h (B x))"
by auto

lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
by auto

lemma extend_set_Union: "extend_set h (⋃A) = (⋃X ∈ A. extend_set h X)"
by blast

lemma extend_set_subset_Compl_eq: "(extend_set h A ⊆ - extend_set h B) = (A ⊆ - B)"
by (auto simp: extend_set_def)

subsection‹@{term extend_act}›

(*Can't strengthen it to
((h(s,y), h(s',y')) ∈ extend_act h act) = ((s, s') ∈ act & y=y')
because h doesn't have to be injective in the 2nd argument*)
lemma mem_extend_act_iff [iff]: "((h(s,y), h(s',y)) ∈ extend_act h act) = ((s, s') ∈ act)"
by (auto simp: extend_act_def)

(*Converse fails: (z,z') would include actions that changed the g-part*)
lemma extend_act_D: "(z, z') ∈ extend_act h act ==> (f z, f z') ∈ act"
by (auto simp: extend_act_def)

lemma extend_act_inverse [simp]: "project_act h (extend_act h act) = act"
unfolding extend_act_def project_act_def by blast

lemma project_act_extend_act_restrict [simp]:
"project_act h (Restrict C (extend_act h act)) =
Restrict (project_set h C) act"
unfolding extend_act_def project_act_def by blast

lemma subset_extend_act_D: "act' ⊆ extend_act h act ==> project_act h act' ⊆ act"
unfolding extend_act_def project_act_def by force

lemma inj_extend_act: "inj (extend_act h)"
apply (rule inj_on_inverseI)
apply (rule extend_act_inverse)
done

lemma extend_act_Image [simp]:
"extend_act h act `` (extend_set h A) = extend_set h (act `` A)"
unfolding extend_set_def extend_act_def by force

lemma extend_act_strict_mono [iff]:
"(extend_act h act' ⊆ extend_act h act) = (act'<=act)"
by (auto simp: extend_act_def)

lemma [iff]: "(extend_act h act = extend_act h act') = (act = act')"
by (rule inj_extend_act [THEN inj_eq])

lemma (in -) Domain_extend_act:
"Domain (extend_act h act) = extend_set h (Domain act)"
unfolding extend_set_def extend_act_def by force

lemma extend_act_Id [simp]: "extend_act h Id = Id"
unfolding extend_act_def by (force intro: h_f_g_eq [symmetric])

lemma project_act_I:  "!!z z'. (z, z') ∈ act ==> (f z, f z') ∈ project_act h act"
unfolding project_act_def by (force simp add: split_extended_all)

lemma project_act_Id [simp]: "project_act h Id = Id"
unfolding project_act_def by force

lemma Domain_project_act: "Domain (project_act h act) = project_set h (Domain act)"
unfolding project_act_def by (force simp add: split_extended_all)

subsection‹extend›

text‹Basic properties›

lemma (in -) Init_extend [simp]:
"Init (extend h F) = extend_set h (Init F)"
by (auto simp: extend_def)

lemma (in -) Init_project [simp]:
"Init (project h C F) = project_set h (Init F)"
by (auto simp: project_def)

lemma Acts_extend [simp]: "Acts (extend h F) = (extend_act h ` Acts F)"

lemma AllowedActs_extend [simp]:
"AllowedActs (extend h F) = project_act h -` AllowedActs F"

lemma (in -) Acts_project [simp]:
"Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)"
by (auto simp add: project_def image_iff)

lemma AllowedActs_project [simp]:
"AllowedActs(project h C F) =
{act. Restrict (project_set h C) act
∈ project_act h ` Restrict C ` AllowedActs F}"
apply (simp (no_asm) add: project_def image_iff)
apply (subst insert_absorb)
apply (auto intro!: bexI [of _ Id] simp add: project_act_def)
done

lemma Allowed_extend: "Allowed (extend h F) = project h UNIV -` Allowed F"

lemma extend_SKIP [simp]: "extend h SKIP = SKIP"
apply (unfold SKIP_def)
apply (rule program_equalityI, auto)
done

lemma (in -) project_set_UNIV [simp]: "project_set h UNIV = UNIV"
by auto

lemma (in -) project_set_Union: "project_set h (⋃A) = (⋃X ∈ A. project_set h X)"
by blast

(*Converse FAILS: the extended state contributing to project_set h C
may not coincide with the one contributing to project_act h act*)
lemma (in -) project_act_Restrict_subset:
"project_act h (Restrict C act) ⊆ Restrict (project_set h C) (project_act h act)"

lemma project_act_Restrict_Id_eq: "project_act h (Restrict C Id) = Restrict (project_set h C) Id"

lemma project_extend_eq:
"project h C (extend h F) =
mk_program (Init F, Restrict (project_set h C) ` Acts F,
{act. Restrict (project_set h C) act
∈ project_act h ` Restrict C `
(project_act h -` AllowedActs F)})"
apply (rule program_equalityI)
apply simp
done

lemma extend_inverse [simp]:
"project h UNIV (extend h F) = F"
subset_UNIV [THEN subset_trans, THEN Restrict_triv])
apply (rule program_equalityI)
apply (simp_all (no_asm))
apply (subst insert_absorb)
apply (simp (no_asm) add: bexI [of _ Id])
apply auto
using project_act_Id apply blast
apply (rename_tac "act")
apply (rule_tac x = "extend_act h act" in exI)
apply simp
done

lemma inj_extend: "inj (extend h)"
apply (rule inj_on_inverseI)
apply (rule extend_inverse)
done

lemma extend_Join [simp]: "extend h (F⊔G) = extend h F⊔extend h G"
apply (rule program_equalityI)
done

lemma extend_JN [simp]: "extend h (JOIN I F) = (⨆i ∈ I. extend h (F i))"
apply (rule program_equalityI)
done

(** These monotonicity results look natural but are UNUSED **)

lemma extend_mono: "F ≤ G ==> extend h F ≤ extend h G"

lemma project_mono: "F ≤ G ==> project h C F ≤ project h C G"

lemma all_total_extend: "all_total F ==> all_total (extend h F)"

subsection‹Safety: co, stable›

lemma extend_constrains:
"(extend h F ∈ (extend_set h A) co (extend_set h B)) =
(F ∈ A co B)"

lemma extend_stable:
"(extend h F ∈ stable (extend_set h A)) = (F ∈ stable A)"

lemma extend_invariant:
"(extend h F ∈ invariant (extend_set h A)) = (F ∈ invariant A)"

(*Projects the state predicates in the property satisfied by  extend h F.
Converse fails: A and B may differ in their extra variables*)
lemma extend_constrains_project_set:
"extend h F ∈ A co B ==> F ∈ (project_set h A) co (project_set h B)"
by (auto simp add: constrains_def, force)

lemma extend_stable_project_set:
"extend h F ∈ stable A ==> F ∈ stable (project_set h A)"

subsection‹Weak safety primitives: Co, Stable›

lemma reachable_extend_f: "p ∈ reachable (extend h F) ==> f p ∈ reachable F"
by (induct set: reachable) (auto intro: reachable.intros simp add: extend_act_def image_iff)

lemma h_reachable_extend: "h(s,y) ∈ reachable (extend h F) ==> s ∈ reachable F"
by (force dest!: reachable_extend_f)

lemma reachable_extend_eq: "reachable (extend h F) = extend_set h (reachable F)"
apply (unfold extend_set_def)
apply (rule equalityI)
apply (force intro: h_f_g_eq [symmetric] dest!: reachable_extend_f, clarify)
apply (erule reachable.induct)
apply (force intro: reachable.intros)+
done

lemma extend_Constrains:
"(extend h F ∈ (extend_set h A) Co (extend_set h B)) =
(F ∈ A Co B)"
by (simp add: Constrains_def reachable_extend_eq extend_constrains
extend_set_Int_distrib [symmetric])

lemma extend_Stable: "(extend h F ∈ Stable (extend_set h A)) = (F ∈ Stable A)"

lemma extend_Always: "(extend h F ∈ Always (extend_set h A)) = (F ∈ Always A)"

(** Safety and "project" **)

(** projection: monotonicity for safety **)

lemma (in -) project_act_mono:
"D ⊆ C ==>
project_act h (Restrict D act) ⊆ project_act h (Restrict C act)"

lemma project_constrains_mono:
"[| D ⊆ C; project h C F ∈ A co B |] ==> project h D F ∈ A co B"
apply (drule project_act_mono, blast)
done

lemma project_stable_mono:
"[| D ⊆ C;  project h C F ∈ stable A |] ==> project h D F ∈ stable A"

(*Key lemma used in several proofs about project and co*)
lemma project_constrains:
"(project h C F ∈ A co B)  =
(F ∈ (C ∩ extend_set h A) co (extend_set h B) & A ⊆ B)"
apply (unfold constrains_def)
apply (auto intro!: project_act_I simp add: ball_Un)
apply (force intro!: project_act_I dest!: subsetD)
(*the <== direction*)
apply (unfold project_act_def)
apply (force dest!: subsetD)
done

lemma project_stable: "(project h UNIV F ∈ stable A) = (F ∈ stable (extend_set h A))"

lemma project_stable_I: "F ∈ stable (extend_set h A) ==> project h C F ∈ stable A"
apply (drule project_stable [THEN iffD2])
apply (blast intro: project_stable_mono)
done

lemma Int_extend_set_lemma:
"A ∩ extend_set h ((project_set h A) ∩ B) = A ∩ extend_set h B"

(*Strange (look at occurrences of C) but used in leadsETo proofs*)
lemma project_constrains_project_set:
"G ∈ C co B ==> project h C G ∈ project_set h C co project_set h B"
by (simp add: constrains_def project_def project_act_def, blast)

lemma project_stable_project_set:
"G ∈ stable C ==> project h C G ∈ stable (project_set h C)"

subsection‹Progress: transient, ensures›

lemma extend_transient:
"(extend h F ∈ transient (extend_set h A)) = (F ∈ transient A)"
by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)

lemma extend_ensures:
"(extend h F ∈ (extend_set h A) ensures (extend_set h B)) =
(F ∈ A ensures B)"
by (simp add: ensures_def extend_constrains extend_transient
extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])

==> extend h F ∈ (extend_set h A) leadsTo (extend_set h B)"
done

subsection‹Proving the converse takes some doing!›

lemma slice_iff [iff]: "(x ∈ slice C y) = (h(x,y) ∈ C)"

lemma slice_Union: "slice (⋃S) y = (⋃x ∈ S. slice x y)"
by auto

lemma slice_extend_set: "slice (extend_set h A) y = A"
by auto

lemma project_set_is_UN_slice: "project_set h A = (⋃y. slice A y)"
by auto

lemma extend_transient_slice:
"extend h F ∈ transient A ==> F ∈ transient (slice A y)"
by (auto simp: transient_def)

(*Converse?*)
lemma extend_constrains_slice:
"extend h F ∈ A co B ==> F ∈ (slice A y) co (slice B y)"

lemma extend_ensures_slice:
"extend h F ∈ A ensures B ==> F ∈ (slice A y) ensures (project_set h B)"
apply (auto simp add: ensures_def extend_constrains extend_transient)
apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen])
apply (erule extend_constrains_slice [THEN constrains_weaken], auto)
done

"∀y. F ∈ (slice B y) leadsTo CU ==> F ∈ (project_set h B) leadsTo CU"
done

"extend h F ∈ AU leadsTo BU
==> ∀y. F ∈ (slice AU y) leadsTo (project_set h BU)"
apply (blast intro: extend_ensures_slice)
done

"(extend h F ∈ (extend_set h A) leadsTo (extend_set h B)) =
apply safe
done

"(extend h F ∈ (extend_set h A) LeadsTo (extend_set h B)) =
extend_set_Int_distrib [symmetric])

subsection‹preserves›

lemma project_preserves_I:
"G ∈ preserves (v o f) ==> project h C G ∈ preserves v"
by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)

(*to preserve f is to preserve the whole original state*)
lemma project_preserves_id_I:
"G ∈ preserves f ==> project h C G ∈ preserves id"

lemma extend_preserves:
"(extend h G ∈ preserves (v o f)) = (G ∈ preserves v)"
by (auto simp add: preserves_def extend_stable [symmetric]
extend_set_eq_Collect)

lemma inj_extend_preserves: "inj h ==> (extend h G ∈ preserves g)"
by (auto simp add: preserves_def extend_def extend_act_def stable_def
constrains_def g_def)

subsection‹Guarantees›

lemma project_extend_Join: "project h UNIV ((extend h F)⊔G) = F⊔(project h UNIV G)"
apply (rule program_equalityI)
apply (auto simp add: project_set_extend_set_Int image_iff)
apply (metis Un_iff extend_act_inverse image_iff)
apply (metis Un_iff extend_act_inverse image_iff)
done

lemma extend_Join_eq_extend_D:
"(extend h F)⊔G = extend h H ==> H = F⊔(project h UNIV G)"
apply (drule_tac f = "project h UNIV" in arg_cong)
done

(** Strong precondition and postcondition; only useful when
the old and new state sets are in bijection **)

lemma ok_extend_imp_ok_project: "extend h F ok G ==> F ok project h UNIV G"
apply (drule subsetD)
apply (auto intro!: rev_image_eqI)
done

lemma ok_extend_iff: "(extend h F ok extend h G) = (F ok G)"
apply force+
done

lemma OK_extend_iff: "OK I (%i. extend h (F i)) = (OK I F)"
apply (unfold OK_def, safe)
apply (drule_tac x = i in bspec)
apply (drule_tac [2] x = j in bspec)
apply force+
done

lemma guarantees_imp_extend_guarantees:
"F ∈ X guarantees Y ==>
extend h F ∈ (extend h ` X) guarantees (extend h ` Y)"
apply (rule guaranteesI, clarify)
apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D
guaranteesD)
done

lemma extend_guarantees_imp_guarantees:
"extend h F ∈ (extend h ` X) guarantees (extend h ` Y)
==> F ∈ X guarantees Y"
apply (drule_tac x = "extend h G" in spec)
apply (simp del: extend_Join