A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
(* Title: HOL/UNITY/Extend.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
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"
*)
header{*Extending State Sets*}
theory Extend = Guar:
constdefs
(*MOVE to Relation.thy?*)
Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
"Restrict A r == r \<inter> (A <*> UNIV)"
good_map :: "['a*'b => 'c] => bool"
"good_map h == surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
(*Using the locale constant "f", this is f (h (x,y))) = x*)
extend_set :: "['a*'b => 'c, 'a set] => 'c set"
"extend_set h A == h ` (A <*> UNIV)"
project_set :: "['a*'b => 'c, 'c set] => 'a set"
"project_set h C == {x. \<exists>y. h(x,y) \<in> C}"
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
"extend_act h == %act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))}"
project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
"project_act h act == {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),
extend_act h ` Acts F,
project_act h -` AllowedActs F)"
(*Argument C allows weak safety laws to be projected*)
project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
"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) \<in> 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 \<in> A)"
by (unfold Restrict_def, blast)
lemma Restrict_UNIV [simp]: "Restrict UNIV = id"
apply (rule ext)
apply (auto simp add: Restrict_def)
done
lemma Restrict_empty [simp]: "Restrict {} r = {}"
by (auto simp add: Restrict_def)
lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A \<inter> B) r"
by (unfold Restrict_def, blast)
lemma Restrict_triv: "Domain r \<subseteq> A ==> Restrict A r = r"
by (unfold Restrict_def, auto)
lemma Restrict_subset: "Restrict A r \<subseteq> r"
by (unfold Restrict_def, auto)
lemma Restrict_eq_mono:
"[| A \<subseteq> B; Restrict B r = Restrict B s |]
==> Restrict A r = Restrict A s"
by (unfold Restrict_def, blast)
lemma Restrict_imageI:
"[| s \<in> RR; Restrict A r = Restrict A s |]
==> Restrict A r \<in> Restrict A ` RR"
by (unfold Restrict_def image_def, auto)
lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A \<inter> Domain r"
by blast
lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> 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 (simp add: good_map_def)
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"
apply (unfold inv_def)
apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE])
apply (rule someI2)
apply (drule_tac [2] f = g in arg_cong)
apply (auto simp add: prem)
done
subsection{*Trivial properties of f, g, h*}
lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x"
by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
lemma (in Extend) 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 (in Extend) h_f_g_equiv: "h(f z, g z) == z"
by (simp add: f_def g_def
good_h [unfolded good_map_def, THEN conjunct1, THEN surj_f_inv_f])
lemma (in Extend) h_f_g_eq: "h(f z, g z) = z"
by (simp add: h_f_g_equiv)
lemma (in Extend) split_extended_all:
"(!!z. PROP P z) == (!!u y. PROP P (h (u, y)))"
proof
assume allP: "\<And>z. PROP P z"
fix u y
show "PROP P (h (u, y))" by (rule allP)
next
assume allPh: "\<And>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
subsection{*@{term extend_set}: basic properties*}
lemma project_set_iff [iff]:
"(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
by (simp add: project_set_def)
lemma extend_set_mono: "A \<subseteq> B ==> extend_set h A \<subseteq> extend_set h B"
by (unfold extend_set_def, blast)
lemma (in Extend) mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)"
apply (unfold extend_set_def)
apply (force intro: h_f_g_eq [symmetric])
done
lemma (in Extend) extend_set_strict_mono [iff]:
"(extend_set h A \<subseteq> extend_set h B) = (A \<subseteq> B)"
by (unfold extend_set_def, force)
lemma extend_set_empty [simp]: "extend_set h {} = {}"
by (unfold extend_set_def, auto)
lemma (in Extend) extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}"
by auto
lemma (in Extend) extend_set_sing: "extend_set h {x} = {s. f s = x}"
by auto
lemma (in Extend) extend_set_inverse [simp]:
"project_set h (extend_set h C) = C"
by (unfold extend_set_def, auto)
lemma (in Extend) extend_set_project_set:
"C \<subseteq> extend_set h (project_set h C)"
apply (unfold extend_set_def)
apply (auto simp add: split_extended_all, blast)
done
lemma (in Extend) inj_extend_set: "inj (extend_set h)"
apply (rule inj_on_inverseI)
apply (rule extend_set_inverse)
done
lemma (in Extend) extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
apply (unfold extend_set_def)
apply (auto simp add: split_extended_all)
done
subsection{*@{term project_set}: basic properties*}
(*project_set is simply image!*)
lemma (in Extend) 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 (in Extend) project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C"
by (auto simp add: split_extended_all)
subsection{*More laws*}
(*Because A and B could differ on the "other" part of the state,
cannot generalize to
project_set h (A \<inter> B) = project_set h A \<inter> project_set h B
*)
lemma (in Extend) project_set_extend_set_Int:
"project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)"
by auto
(*Unused, but interesting?*)
lemma (in Extend) project_set_extend_set_Un:
"project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)"
by auto
lemma project_set_Int_subset:
"project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)"
by auto
lemma (in Extend) extend_set_Un_distrib:
"extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B"
by auto
lemma (in Extend) extend_set_Int_distrib:
"extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
by auto
lemma (in Extend) extend_set_INT_distrib:
"extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
by auto
lemma (in Extend) extend_set_Diff_distrib:
"extend_set h (A - B) = extend_set h A - extend_set h B"
by auto
lemma (in Extend) extend_set_Union:
"extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
by blast
lemma (in Extend) extend_set_subset_Compl_eq:
"(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
by (unfold extend_set_def, auto)
subsection{*@{term extend_act}*}
(*Can't strengthen it to
((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
because h doesn't have to be injective in the 2nd argument*)
lemma (in Extend) mem_extend_act_iff [iff]:
"((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"
by (unfold extend_act_def, auto)
(*Converse fails: (z,z') would include actions that changed the g-part*)
lemma (in Extend) extend_act_D:
"(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act"
by (unfold extend_act_def, auto)
lemma (in Extend) extend_act_inverse [simp]:
"project_act h (extend_act h act) = act"
by (unfold extend_act_def project_act_def, blast)
lemma (in Extend) project_act_extend_act_restrict [simp]:
"project_act h (Restrict C (extend_act h act)) =
Restrict (project_set h C) act"
by (unfold extend_act_def project_act_def, blast)
lemma (in Extend) subset_extend_act_D:
"act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act"
by (unfold extend_act_def project_act_def, force)
lemma (in Extend) inj_extend_act: "inj (extend_act h)"
apply (rule inj_on_inverseI)
apply (rule extend_act_inverse)
done
lemma (in Extend) extend_act_Image [simp]:
"extend_act h act `` (extend_set h A) = extend_set h (act `` A)"
by (unfold extend_set_def extend_act_def, force)
lemma (in Extend) extend_act_strict_mono [iff]:
"(extend_act h act' \<subseteq> extend_act h act) = (act'<=act)"
by (unfold extend_act_def, auto)
declare (in Extend) inj_extend_act [THEN inj_eq, iff]
(*This theorem is (extend_act h act' = extend_act h act) = (act'=act) *)
lemma Domain_extend_act:
"Domain (extend_act h act) = extend_set h (Domain act)"
by (unfold extend_set_def extend_act_def, force)
lemma (in Extend) extend_act_Id [simp]:
"extend_act h Id = Id"
apply (unfold extend_act_def)
apply (force intro: h_f_g_eq [symmetric])
done
lemma (in Extend) project_act_I:
"!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act"
apply (unfold project_act_def)
apply (force simp add: split_extended_all)
done
lemma (in Extend) project_act_Id [simp]: "project_act h Id = Id"
by (unfold project_act_def, force)
lemma (in Extend) Domain_project_act:
"Domain (project_act h act) = project_set h (Domain act)"
apply (unfold project_act_def)
apply (force simp add: split_extended_all)
done
subsection{*extend*}
text{*Basic properties*}
lemma Init_extend [simp]:
"Init (extend h F) = extend_set h (Init F)"
by (unfold extend_def, auto)
lemma Init_project [simp]:
"Init (project h C F) = project_set h (Init F)"
by (unfold project_def, auto)
lemma (in Extend) Acts_extend [simp]:
"Acts (extend h F) = (extend_act h ` Acts F)"
by (simp add: extend_def insert_Id_image_Acts)
lemma (in Extend) AllowedActs_extend [simp]:
"AllowedActs (extend h F) = project_act h -` AllowedActs F"
by (simp add: extend_def insert_absorb)
lemma 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 (in Extend) AllowedActs_project [simp]:
"AllowedActs(project h C F) =
{act. Restrict (project_set h C) act
\<in> 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 (in Extend) Allowed_extend:
"Allowed (extend h F) = project h UNIV -` Allowed F"
apply (simp (no_asm) add: AllowedActs_extend Allowed_def)
apply blast
done
lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
apply (unfold SKIP_def)
apply (rule program_equalityI, auto)
done
lemma project_set_UNIV [simp]: "project_set h UNIV = UNIV"
by auto
lemma project_set_Union:
"project_set h (Union A) = (\<Union>X \<in> 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 Extend) project_act_Restrict_subset:
"project_act h (Restrict C act) \<subseteq>
Restrict (project_set h C) (project_act h act)"
by (auto simp add: project_act_def)
lemma (in Extend) project_act_Restrict_Id_eq:
"project_act h (Restrict C Id) = Restrict (project_set h C) Id"
by (auto simp add: project_act_def)
lemma (in Extend) 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
\<in> project_act h ` Restrict C `
(project_act h -` AllowedActs F)})"
apply (rule program_equalityI)
apply simp
apply (simp add: image_eq_UN)
apply (simp add: project_def)
done
lemma (in Extend) extend_inverse [simp]:
"project h UNIV (extend h F) = F"
apply (simp (no_asm_simp) add: project_extend_eq image_eq_UN
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
apply (rename_tac "act")
apply (rule_tac x = "extend_act h act" in bexI, auto)
done
lemma (in Extend) inj_extend: "inj (extend h)"
apply (rule inj_on_inverseI)
apply (rule extend_inverse)
done
lemma (in Extend) extend_Join [simp]:
"extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
apply (rule program_equalityI)
apply (simp (no_asm) add: extend_set_Int_distrib)
apply (simp add: image_Un, auto)
done
lemma (in Extend) extend_JN [simp]:
"extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))"
apply (rule program_equalityI)
apply (simp (no_asm) add: extend_set_INT_distrib)
apply (simp add: image_UN, auto)
done
(** These monotonicity results look natural but are UNUSED **)
lemma (in Extend) extend_mono: "F \<le> G ==> extend h F \<le> extend h G"
by (force simp add: component_eq_subset)
lemma (in Extend) project_mono: "F \<le> G ==> project h C F \<le> project h C G"
by (simp add: component_eq_subset, blast)
lemma (in Extend) all_total_extend: "all_total F ==> all_total (extend h F)"
by (simp add: all_total_def Domain_extend_act)
subsection{*Safety: co, stable*}
lemma (in Extend) extend_constrains:
"(extend h F \<in> (extend_set h A) co (extend_set h B)) =
(F \<in> A co B)"
by (simp add: constrains_def)
lemma (in Extend) extend_stable:
"(extend h F \<in> stable (extend_set h A)) = (F \<in> stable A)"
by (simp add: stable_def extend_constrains)
lemma (in Extend) extend_invariant:
"(extend h F \<in> invariant (extend_set h A)) = (F \<in> invariant A)"
by (simp add: invariant_def extend_stable)
(*Projects the state predicates in the property satisfied by extend h F.
Converse fails: A and B may differ in their extra variables*)
lemma (in Extend) extend_constrains_project_set:
"extend h F \<in> A co B ==> F \<in> (project_set h A) co (project_set h B)"
by (auto simp add: constrains_def, force)
lemma (in Extend) extend_stable_project_set:
"extend h F \<in> stable A ==> F \<in> stable (project_set h A)"
by (simp add: stable_def extend_constrains_project_set)
subsection{*Weak safety primitives: Co, Stable*}
lemma (in Extend) reachable_extend_f:
"p \<in> reachable (extend h F) ==> f p \<in> reachable F"
apply (erule reachable.induct)
apply (auto intro: reachable.intros simp add: extend_act_def image_iff)
done
lemma (in Extend) h_reachable_extend:
"h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F"
by (force dest!: reachable_extend_f)
lemma (in Extend) 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 (in Extend) extend_Constrains:
"(extend h F \<in> (extend_set h A) Co (extend_set h B)) =
(F \<in> A Co B)"
by (simp add: Constrains_def reachable_extend_eq extend_constrains
extend_set_Int_distrib [symmetric])
lemma (in Extend) extend_Stable:
"(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)"
by (simp add: Stable_def extend_Constrains)
lemma (in Extend) extend_Always:
"(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)"
by (simp (no_asm_simp) add: Always_def extend_Stable)
(** Safety and "project" **)
(** projection: monotonicity for safety **)
lemma project_act_mono:
"D \<subseteq> C ==>
project_act h (Restrict D act) \<subseteq> project_act h (Restrict C act)"
by (auto simp add: project_act_def)
lemma (in Extend) project_constrains_mono:
"[| D \<subseteq> C; project h C F \<in> A co B |] ==> project h D F \<in> A co B"
apply (auto simp add: constrains_def)
apply (drule project_act_mono, blast)
done
lemma (in Extend) project_stable_mono:
"[| D \<subseteq> C; project h C F \<in> stable A |] ==> project h D F \<in> stable A"
by (simp add: stable_def project_constrains_mono)
(*Key lemma used in several proofs about project and co*)
lemma (in Extend) project_constrains:
"(project h C F \<in> A co B) =
(F \<in> (C \<inter> extend_set h A) co (extend_set h B) & A \<subseteq> 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 (in Extend) project_stable:
"(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))"
apply (unfold stable_def)
apply (simp (no_asm) add: project_constrains)
done
lemma (in Extend) project_stable_I:
"F \<in> stable (extend_set h A) ==> project h C F \<in> stable A"
apply (drule project_stable [THEN iffD2])
apply (blast intro: project_stable_mono)
done
lemma (in Extend) Int_extend_set_lemma:
"A \<inter> extend_set h ((project_set h A) \<inter> B) = A \<inter> extend_set h B"
by (auto simp add: split_extended_all)
(*Strange (look at occurrences of C) but used in leadsETo proofs*)
lemma project_constrains_project_set:
"G \<in> C co B ==> project h C G \<in> 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 \<in> stable C ==> project h C G \<in> stable (project_set h C)"
by (simp add: stable_def project_constrains_project_set)
subsection{*Progress: transient, ensures*}
lemma (in Extend) extend_transient:
"(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)
lemma (in Extend) extend_ensures:
"(extend h F \<in> (extend_set h A) ensures (extend_set h B)) =
(F \<in> A ensures B)"
by (simp add: ensures_def extend_constrains extend_transient
extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])
lemma (in Extend) leadsTo_imp_extend_leadsTo:
"F \<in> A leadsTo B
==> extend h F \<in> (extend_set h A) leadsTo (extend_set h B)"
apply (erule leadsTo_induct)
apply (simp add: leadsTo_Basis extend_ensures)
apply (blast intro: leadsTo_Trans)
apply (simp add: leadsTo_UN extend_set_Union)
done
subsection{*Proving the converse takes some doing!*}
lemma (in Extend) slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
by (simp (no_asm) add: slice_def)
lemma (in Extend) slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
by auto
lemma (in Extend) slice_extend_set: "slice (extend_set h A) y = A"
by auto
lemma (in Extend) project_set_is_UN_slice:
"project_set h A = (\<Union>y. slice A y)"
by auto
lemma (in Extend) extend_transient_slice:
"extend h F \<in> transient A ==> F \<in> transient (slice A y)"
by (unfold transient_def, auto)
(*Converse?*)
lemma (in Extend) extend_constrains_slice:
"extend h F \<in> A co B ==> F \<in> (slice A y) co (slice B y)"
by (auto simp add: constrains_def)
lemma (in Extend) extend_ensures_slice:
"extend h F \<in> A ensures B ==> F \<in> (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
lemma (in Extend) leadsTo_slice_project_set:
"\<forall>y. F \<in> (slice B y) leadsTo CU ==> F \<in> (project_set h B) leadsTo CU"
apply (simp (no_asm) add: project_set_is_UN_slice)
apply (blast intro: leadsTo_UN)
done
lemma (in Extend) extend_leadsTo_slice [rule_format]:
"extend h F \<in> AU leadsTo BU
==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
apply (erule leadsTo_induct)
apply (blast intro: extend_ensures_slice leadsTo_Basis)
apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
apply (simp add: leadsTo_UN slice_Union)
done
lemma (in Extend) extend_leadsTo:
"(extend h F \<in> (extend_set h A) leadsTo (extend_set h B)) =
(F \<in> A leadsTo B)"
apply safe
apply (erule_tac [2] leadsTo_imp_extend_leadsTo)
apply (drule extend_leadsTo_slice)
apply (simp add: slice_extend_set)
done
lemma (in Extend) extend_LeadsTo:
"(extend h F \<in> (extend_set h A) LeadsTo (extend_set h B)) =
(F \<in> A LeadsTo B)"
by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
extend_set_Int_distrib [symmetric])
subsection{*preserves*}
lemma (in Extend) project_preserves_I:
"G \<in> preserves (v o f) ==> project h C G \<in> 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 (in Extend) project_preserves_id_I:
"G \<in> preserves f ==> project h C G \<in> preserves id"
by (simp add: project_preserves_I)
lemma (in Extend) extend_preserves:
"(extend h G \<in> preserves (v o f)) = (G \<in> preserves v)"
by (auto simp add: preserves_def extend_stable [symmetric]
extend_set_eq_Collect)
lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)"
by (auto simp add: preserves_def extend_def extend_act_def stable_def
constrains_def g_def)
subsection{*Guarantees*}
lemma (in Extend) project_extend_Join:
"project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
apply (rule program_equalityI)
apply (simp add: project_set_extend_set_Int)
apply (simp add: image_eq_UN UN_Un, auto)
done
lemma (in Extend) extend_Join_eq_extend_D:
"(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
apply (drule_tac f = "project h UNIV" in arg_cong)
apply (simp add: project_extend_Join)
done
(** Strong precondition and postcondition; only useful when
the old and new state sets are in bijection **)
lemma (in Extend) ok_extend_imp_ok_project:
"extend h F ok G ==> F ok project h UNIV G"
apply (auto simp add: ok_def)
apply (drule subsetD)
apply (auto intro!: rev_image_eqI)
done
lemma (in Extend) ok_extend_iff: "(extend h F ok extend h G) = (F ok G)"
apply (simp add: ok_def, safe)
apply (force+)
done
lemma (in Extend) 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 (in Extend) guarantees_imp_extend_guarantees:
"F \<in> X guarantees Y ==>
extend h F \<in> (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 (in Extend) extend_guarantees_imp_guarantees:
"extend h F \<in> (extend h ` X) guarantees (extend h ` Y)
==> F \<in> X guarantees Y"
apply (auto simp add: guar_def)
apply (drule_tac x = "extend h G" in spec)
apply (simp del: extend_Join
add: extend_Join [symmetric] ok_extend_iff
inj_extend [THEN inj_image_mem_iff])
done
lemma (in Extend) extend_guarantees_eq:
"(extend h F \<in> (extend h ` X) guarantees (extend h ` Y)) =
(F \<in> X guarantees Y)"
by (blast intro: guarantees_imp_extend_guarantees
extend_guarantees_imp_guarantees)
end