src/HOL/UNITY/Extend.thy

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