# HG changeset patch
# User paulson
# Date 944043624 -3600
# Node ID 296b03b79505cd9f5fda4cd1597136b2cbc08b7c
# Parent  0e4434d55df9e6dbf08f468a62c045800f032e95
new generalized leads-to theory

diff -r 0e4434d55df9 -r 296b03b79505 src/HOL/UNITY/ELT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/ELT.ML	Wed Dec 01 11:20:24 1999 +0100
@@ -0,0 +1,556 @@
+(*  Title:      HOL/UNITY/ELT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+leadsTo strengthened with a specification of the allowable sets transient parts
+*)
+
+Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
+by Safe_tac;
+by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
+by Auto_tac;
+qed "givenBy_eq_all";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
+by (Blast_tac 1);
+by Auto_tac;
+qed "givenBy_eq_Collect";
+
+val prems =
+Goal "(!!x y. [|  x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
+by (stac givenBy_eq_all 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "givenByI";
+
+Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
+by Auto_tac;
+qed "givenByD";
+
+Goal "{} : givenBy v";
+by (blast_tac (claset() addSIs [givenByI]) 1);
+qed "empty_mem_givenBy";
+
+AddIffs [empty_mem_givenBy];
+
+Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "givenBy_imp_eq_Collect";
+
+Goalw [givenBy_def] "EX P. A = {s. P(v s)} ==> A: givenBy v";
+by (Best_tac 1);
+qed "eq_Collect_imp_givenBy";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (blast_tac (claset() addIs [eq_Collect_imp_givenBy,
+			       givenBy_imp_eq_Collect]) 1);
+qed "givenBy_eq_eq_Collect";
+
+Goal "(funPair f g) o h = funPair (f o h) (g o h)";
+by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
+qed "funPair_o_distrib";
+
+
+(** Standard leadsTo rules **)
+
+Goalw [leadsETo_def] "[| F: A ensures B;  A-B: CC |] ==> F : A leadsTo[CC] B";
+by (blast_tac (claset() addIs [elt.Basis]) 1);
+qed "leadsETo_Basis";
+
+Goalw [leadsETo_def]
+     "[| F : A leadsTo[CC] B;  F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C";
+by (blast_tac (claset() addIs [elt.Trans]) 1);
+qed "leadsETo_Trans";
+
+(*Useful with cancellation, disjunction*)
+Goal "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "leadsETo_Un_duplicate";
+
+Goal "F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "leadsETo_Un_duplicate2";
+
+(*The Union introduction rule as we should have liked to state it*)
+val prems = Goalw [leadsETo_def]
+    "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B";
+by (blast_tac (claset() addIs [elt.Union] addDs prems) 1);
+qed "leadsETo_Union";
+
+val prems = Goal
+    "(!!i. i : I ==> F : (A i) leadsTo[CC] B) \
+\    ==> F : (UN i:I. A i) leadsTo[CC] B";
+by (stac (Union_image_eq RS sym) 1);
+by (blast_tac (claset() addIs leadsETo_Union::prems) 1);
+qed "leadsETo_UN";
+
+(*The INDUCTION rule as we should have liked to state it*)
+val major::prems = Goalw [leadsETo_def]
+  "[| F : za leadsTo[CC] zb;  \
+\     !!A B. [| F : A ensures B;  A-B : 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. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B \
+\  |] ==> P za zb";
+by (rtac (major RS CollectD RS elt.induct) 1);
+by (REPEAT (blast_tac (claset() addIs prems) 1));
+qed "leadsETo_induct";
+
+
+(** New facts involving leadsETo **)
+
+Goal "CC' <= CC ==> (A leadsTo[CC'] B) <= (A leadsTo[CC] B)";
+by Safe_tac;
+by (etac leadsETo_induct 1);
+by (blast_tac (claset() addIs [leadsETo_Union]) 3);
+by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
+by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
+qed "leadsETo_mono";
+
+
+val prems = Goalw [leadsETo_def]
+ "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) ==> F : (Union S Int C) leadsTo[CC] B";
+by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
+by (blast_tac (claset() addIs [elt.Union] addDs prems) 1);
+qed "leadsETo_Union_Int";
+
+(*Binary union introduction rule*)
+Goal "[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |] ==> F : (A Un B) leadsTo[CC] C";
+by (stac Un_eq_Union 1);
+by (blast_tac (claset() addIs [leadsETo_Union]) 1);
+qed "leadsETo_Un";
+
+val prems = 
+Goal "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B";
+by (stac (UN_singleton RS sym) 1 THEN rtac leadsETo_UN 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "single_leadsETo_I";
+
+
+Goal "[| A<=B;  {}:CC |]  ==> F : A leadsTo[CC] B";
+by (asm_simp_tac (simpset() addsimps [subset_imp_ensures RS leadsETo_Basis,
+				      Diff_eq_empty_iff RS iffD2]) 1);
+qed "subset_imp_leadsETo";
+
+bind_thm ("empty_leadsETo", empty_subsetI RS subset_imp_leadsETo);
+Addsimps [empty_leadsETo];
+
+
+(** Weakening laws all require {}:CC **)
+
+Goal "[| F : A leadsTo[CC] A';  A'<=B';  {}:CC |] ==> F : A leadsTo[CC] B'";
+by (blast_tac (claset() addIs [subset_imp_leadsETo, leadsETo_Trans]) 1);
+qed "leadsETo_weaken_R";
+
+Goal "[| F : A leadsTo[CC] A'; B<=A;  {}:CC |] ==> F : B leadsTo[CC] A'";
+by (blast_tac (claset() addIs [leadsETo_Trans, subset_imp_leadsETo]) 1);
+qed_spec_mp "leadsETo_weaken_L";
+
+(*Distributes over binary unions*)
+Goal "{} : CC ==> \
+\ F : (A Un B) leadsTo[CC] C  =  (F : A leadsTo[CC] C & F : B leadsTo[CC] C)";
+by (blast_tac (claset() addIs [leadsETo_Un, leadsETo_weaken_L]) 1);
+qed "leadsETo_Un_distrib";
+
+Goal "{} : CC ==> \
+\   F : (UN i:I. A i) leadsTo[CC] B  =  (ALL i : I. F : (A i) leadsTo[CC] B)";
+by (blast_tac (claset() addIs [leadsETo_UN, leadsETo_weaken_L]) 1);
+qed "leadsETo_UN_distrib";
+
+Goal "{} : CC \
+\     ==> F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)";
+by (blast_tac (claset() addIs [leadsETo_Union, leadsETo_weaken_L]) 1);
+qed "leadsETo_Union_distrib";
+
+Goal "[| F : A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC;  {}:CC |] \
+\     ==> F : B leadsTo[CC] B'";
+by (dtac (impOfSubs leadsETo_mono) 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [leadsETo_weaken_R, leadsETo_weaken_L,
+			       leadsETo_Trans]) 1);
+qed "leadsETo_weaken";
+
+Goal "[| F : A leadsTo[CC] A';  CC <= givenBy v |] \
+\     ==> F : A leadsTo[givenBy v] A'";
+by (blast_tac (claset() addIs [empty_mem_givenBy, leadsETo_weaken]) 1);
+qed "leadsETo_givenBy";
+
+
+(*Set difference*)
+Goal "[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C;  {}:CC |] \
+\     ==> F : A leadsTo[CC] C";
+by (blast_tac (claset() addIs [leadsETo_Un, leadsETo_weaken]) 1);
+qed "leadsETo_Diff";
+
+
+(** Meta or object quantifier ???
+    see ball_constrains_UN in UNITY.ML***)
+
+val prems = goal thy
+   "[| !! i. i:I ==> F : (A i) leadsTo[CC] (A' i);  {}:CC |] \
+\   ==> F : (UN i:I. A i) leadsTo[CC] (UN i:I. A' i)";
+by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
+by (blast_tac (claset() addIs [leadsETo_Union, leadsETo_weaken_R] 
+                        addIs prems) 1);
+qed "leadsETo_UN_UN";
+
+(*Binary union version*)
+Goal "[| F : A leadsTo[CC] A';  F : B leadsTo[CC] B';  {}:CC |] \
+\     ==> F : (A Un B) leadsTo[CC] (A' Un B')";
+by (blast_tac (claset() addIs [leadsETo_Un, 
+			       leadsETo_weaken_R]) 1);
+qed "leadsETo_Un_Un";
+
+
+(** The cancellation law **)
+
+Goal "[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B';  {}:CC |] \
+\     ==> F : A leadsTo[CC] (A' Un B')";
+by (blast_tac (claset() addIs [leadsETo_Un_Un, 
+			       subset_imp_leadsETo, leadsETo_Trans]) 1);
+qed "leadsETo_cancel2";
+
+Goal "[| F : A leadsTo[CC] (A' Un B); F : (B-A') leadsTo[CC] B';  {}:CC |] \
+\     ==> F : A leadsTo[CC] (A' Un B')";
+by (rtac leadsETo_cancel2 1);
+by (assume_tac 2);
+by (ALLGOALS Asm_simp_tac);
+qed "leadsETo_cancel_Diff2";
+
+Goal "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B';  {}:CC |] \
+\   ==> F : A leadsTo[CC] (B' Un A')";
+by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
+by (blast_tac (claset() addSIs [leadsETo_cancel2]) 1);
+qed "leadsETo_cancel1";
+
+Goal "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B';  {}:CC |] \
+\   ==> F : A leadsTo[CC] (B' Un A')";
+by (rtac leadsETo_cancel1 1);
+by (assume_tac 2);
+by (ALLGOALS Asm_simp_tac);
+qed "leadsETo_cancel_Diff1";
+
+
+(** The impossibility law **)
+
+Goal "F : A leadsTo[CC] B ==> B={} --> A={}";
+by (etac leadsETo_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
+by (Blast_tac 1);
+val lemma = result() RS mp;
+
+Goal "F : A leadsTo[CC] {} ==> A={}";
+by (blast_tac (claset() addSIs [lemma]) 1);
+qed "leadsETo_empty";
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction"*)
+Goalw [stable_def]
+   "[| F : A leadsTo[CC] A';  F : stable B;  ALL C:CC. C Int B : CC |] \
+\   ==> F : (A Int B) leadsTo[CC] (A' Int B)";
+by (etac leadsETo_induct 1);
+by (blast_tac (claset() addIs [leadsETo_Union_Int]) 3);
+by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
+by (rtac leadsETo_Basis 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [ensures_def, 
+			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [Diff_Int_distrib2 RS sym]) 2);
+by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
+qed "e_psp_stable";
+
+Goal "[| F : A leadsTo[CC] A'; F : stable B;  ALL C:CC. C Int B : CC |] \
+\     ==> F : (B Int A) leadsTo[CC] (B Int A')";
+by (asm_simp_tac (simpset() addsimps e_psp_stable::Int_ac) 1);
+qed "e_psp_stable2";
+
+Goal "[| F : A leadsTo[CC] A'; F : B co B';  \
+\        ALL C:CC. C Int B Int B' : CC;  {}:CC |] \
+\     ==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))";
+by (etac leadsETo_induct 1);
+by (blast_tac (claset() addIs [leadsETo_Union_Int]) 3);
+(*Transitivity case has a delicate argument involving "cancellation"*)
+by (rtac leadsETo_Un_duplicate2 2);
+by (etac leadsETo_cancel_Diff1 2);
+by (assume_tac 3);
+by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
+by (blast_tac (claset() addIs [leadsETo_weaken_L] 
+                        addDs [constrains_imp_subset]) 2);
+(*Basis case*)
+by (rtac leadsETo_Basis 1);
+by (blast_tac (claset() addIs [psp_ensures]) 1);
+by (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'" 1);
+by Auto_tac;
+qed "e_psp";
+
+Goal "[| F : A leadsTo[CC] A'; F : B co B';  \
+\        ALL C:CC. C Int B Int B' : CC;  {}:CC |] \
+\     ==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))";
+by (asm_full_simp_tac (simpset() addsimps e_psp::Int_ac) 1);
+qed "e_psp2";
+
+
+(*** Special properties involving the parameter [CC] ***)
+
+(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
+Goal "[| F: (A leadsTo[givenBy v] B);  F Join G : v localTo[C] F;  \
+\        F Join G : stable C |] \
+\     ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) `` givenBy v] B)";
+by (etac leadsETo_induct 1);
+by (stac Int_Union 3);
+by (blast_tac (claset() addIs [leadsETo_UN]) 3);
+by (blast_tac (claset() addIs [e_psp_stable2 RS leadsETo_weaken_L, 
+			       leadsETo_Trans]) 2);
+by (rtac leadsETo_Basis 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [Int_Diff, ensures_def, stable_def,
+				  givenBy_eq_Collect,
+				  Join_localTo, 
+				  Join_constrains, Join_transient]));
+by (blast_tac (claset() addIs [transient_strengthen]) 3);
+by (blast_tac (claset() addDs [constrains_localTo_constrains]
+			addIs [constrains_Int RS constrains_weaken]) 2);
+by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
+qed "gen_leadsETo_localTo_imp_Join_leadsETo";
+
+(*USED???
+  Could replace this proof by instantiation of the one above with C=UNIV*)
+Goal "[| F: (A leadsTo[givenBy v] B);  F Join G : v localTo[UNIV] F |] \
+\     ==> F Join G : (A leadsTo[givenBy v] B)";
+by (etac leadsETo_induct 1);
+by (blast_tac (claset() addIs [leadsETo_Union]) 3);
+by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
+by (rtac leadsETo_Basis 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [ensures_def, givenBy_eq_Collect,
+				  Join_localTo, 
+				  Join_constrains, Join_transient]));
+by (force_tac (claset() addDs [constrains_localTo_constrains], simpset()) 1);
+qed "leadsETo_localTo_imp_Join_leadsETo";
+
+(*useful??*)
+Goal "[| F Join G : (A leadsTo[CC] B);  ALL C:CC. G : stable C |] \
+\     ==> F: (A leadsTo[CC] B)";
+by (etac leadsETo_induct 1);
+by (blast_tac (claset() addIs [leadsETo_Union]) 3);
+by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
+by (rtac leadsETo_Basis 1);
+by (case_tac "A <= B" 1);
+by (etac subset_imp_ensures 1);
+by (auto_tac (claset() addIs [constrains_weaken],
+	      simpset() addsimps [stable_def, ensures_def, 
+				  Join_constrains, Join_transient]));
+by (REPEAT (thin_tac "?F : ?A co ?B" 1));
+by (etac transientE 1);
+by (rewtac constrains_def);
+by (blast_tac (claset() addSDs [bspec]) 1);
+qed "Join_leadsETo_stable_imp_leadsETo";
+
+
+
+(**** EXTEND/PROJECT PROPERTIES ****)
+
+Open_locale "Extend";
+
+(*Here h and f are locale constants*)
+Goal "extend_set h `` (givenBy v) <= (givenBy (v o f))";
+by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "extend_set_givenBy_subset";
+
+Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "extend_set_givenBy_I";
+
+
+Goal "F : A leadsTo[CC] B \
+\     ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
+\                      (extend_set h B)";
+by (etac leadsETo_induct 1);
+by (asm_simp_tac (simpset() addsimps [leadsETo_UN, extend_set_Union]) 3);
+by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
+by (asm_simp_tac (simpset() addsimps [leadsETo_Basis, extend_ensures,
+				      extend_set_Diff_distrib RS sym]) 1);
+qed "leadsETo_imp_extend_leadsETo";
+
+(*NOW OBSOLETE: SEE BELOW !! Generalizes the version proved in Project.ML*)
+Goalw [LOCALTO_def, transient_def, Diff_def]
+     "[| G : (v o f) localTo[C] extend h F;  project h C G : transient D;  \
+\        D : givenBy v |]    \
+\     ==> F : transient D";
+by (auto_tac (claset(), 
+	      simpset() addsimps [givenBy_eq_Collect]));
+by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
+by Auto_tac; 
+by (rtac bexI 1);
+by (assume_tac 2);
+by (Blast_tac 1);
+by (case_tac "{s. P (v s)} = {}" 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [stable_def, constrains_def]));
+by (subgoal_tac
+    "ALL z. Restrict C act ^^ {s. v (f s) = z} <= {s. v (f s) = z}" 1);
+by (blast_tac (claset() addSDs [bspec]) 2);
+by (thin_tac "ALL z. ?P z" 1);
+by (subgoal_tac "project_act h (Restrict C act) ^^ {s. P (v s)} <= {s. P (v s)}" 1);
+by (Clarify_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
+by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 2);
+by (blast_tac (claset() addSDs [subsetD]) 1);
+qed "localTo_project_transient_transient";
+
+
+Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
+by (auto_tac (claset() addIs [project_set_I], 
+	      simpset()));
+qed "Int_extend_set_lemma";
+
+Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
+by (full_simp_tac (simpset() addsimps [constrains_def, project_def, 
+				       project_act_def, project_set_def]) 1);
+by (Blast_tac 1);
+qed "project_constrains_project_set";
+
+Goal "G : stable C ==> project h C G : stable (project_set h C)";
+by (asm_full_simp_tac (simpset() addsimps [stable_def, 
+					   project_constrains_project_set]) 1);
+qed "project_stable_project_set";
+
+(*!! Generalizes the version proved in Project.ML*)
+Goalw [LOCALTO_def, transient_def, Diff_def]
+     "[| G : (v o f) localTo[C] extend h F;  \
+\        project h C G : transient (C' Int D);  \
+\        project h C G : stable C';  \
+\        D : givenBy v;  (C' Int D) <= D |]    \
+\     ==> F : transient (C' Int D)";
+by (auto_tac (claset(), 
+	      simpset() addsimps [givenBy_eq_Collect]));
+by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
+by Auto_tac; 
+by (rtac bexI 1);
+by (assume_tac 2);
+by (Blast_tac 1);
+by (case_tac "(C' Int {s. P (v s)}) = {}" 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [stable_def, constrains_def]));
+by (subgoal_tac
+    "ALL z. Restrict C act ^^ {s. v (f s) = z} <= {s. v (f s) = z}" 1);
+by (blast_tac (claset() addSDs [bspec]) 2);
+by (thin_tac "ALL z. ?P z" 1);
+by (subgoal_tac "project_act h (Restrict C act) ^^ (C' Int {s. P (v s)}) <= (C' Int {s. P (v s)})" 1);
+by (Clarify_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
+by (thin_tac "(C' Int {s. P (v s)}) <= Domain ?A" 2);
+by (thin_tac "?A <= -C' Un ?B" 2);
+by (rtac conjI 2);
+by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 3);
+by (Blast_tac 2);
+by (blast_tac (claset() addSDs [subsetD]) 1);
+qed "localTo_project_transient_transient";
+
+(*This version's stronger in the "ensures" precondition
+  BUT there's no ensures_weaken_L*)
+Goal "[| project h C G : transient (project_set h C Int (A-B)) --> \
+\          F : transient (project_set h C Int (A-B));  \
+\        extend h F Join G : stable C;  \
+\        F Join project h C G : (project_set h C Int A) ensures B |] \
+\     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
+by (stac (Int_extend_set_lemma RS sym) 1);
+by (rtac Join_project_ensures 1);
+by (auto_tac (claset(), simpset() addsimps [Int_Diff]));
+qed "Join_project_ensures_strong";
+
+Goal "[| extend h F Join G : stable C;  \
+\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
+\        G : (v o f) localTo[C] extend h F |] \
+\     ==> extend h F Join 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)";
+by (etac leadsETo_induct 1);
+by (asm_simp_tac (simpset() delsimps UN_simps
+		  addsimps [Int_UN_distrib, leadsETo_UN, extend_set_Union]) 3);
+by (blast_tac (claset() addIs [e_psp_stable2 RS leadsETo_weaken_L, 
+			       leadsETo_Trans]) 2);
+by (Clarify_tac 1);
+by (rtac leadsETo_Basis 1);
+by (etac rev_image_eqI 2);
+by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma,
+				      extend_set_Diff_distrib RS sym]) 2);
+by (rtac Join_project_ensures_strong 1);
+by (auto_tac (claset() addIs [localTo_project_transient_transient,
+			      project_stable_project_set], 
+	      simpset() addsimps [Int_left_absorb, Join_stable]));
+by (asm_simp_tac
+    (simpset() addsimps [stable_ensures_Int RS ensures_weaken_R,
+			 Int_lower2, project_stable_project_set,
+			 Join_stable, extend_stable_project_set]) 1);
+val lemma = result();
+
+Goal "[| extend h F Join G : stable C;  \
+\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
+\        G : (v o f) localTo[C] extend h F |] \
+\     ==> extend h F Join G : (C Int extend_set h A) \
+\           leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
+by (rtac (lemma RS leadsETo_weaken) 1);
+by (auto_tac (claset() addIs [project_set_I], simpset()));
+qed "project_leadsETo_lemma";
+
+Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B;    \
+\        G : (v o f) localTo[UNIV] extend h F |]  \
+\     ==> extend h F Join G : (extend_set h A) \
+\           leadsTo[givenBy (v o f)] (extend_set h B)";
+by (rtac (make_elim project_leadsETo_lemma) 1);
+by Auto_tac;
+by (etac leadsETo_givenBy 1);
+by (rtac extend_set_givenBy_subset 1);
+qed "project_leadsETo_D";
+
+Goal "[| F Join project h (reachable (extend h F Join G)) G \
+\            : A LeadsTo[givenBy v] B;    \
+\        G : (v o f) LocalTo extend h F |] \
+\     ==> extend h F Join G : \
+\           (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)";
+by (rtac (make_elim (subset_refl RS stable_reachable RS 
+		     project_leadsETo_lemma)) 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [LeadsETo_def, LocalTo_def]));
+by (asm_full_simp_tac 
+    (simpset() addsimps [project_set_reachable_extend_eq RS sym]) 1);
+by (etac (impOfSubs leadsETo_mono) 1);
+by (blast_tac (claset() addIs [extend_set_givenBy_I]) 1);
+qed "project_LeadsETo_D";
+
+Goalw [extending_def]
+     "extending (%G. UNIV) h F \
+\               ((v o f) localTo[UNIV] extend h F) \
+\               (extend_set h A leadsTo[givenBy (v o f)] extend_set h B) \
+\               (A leadsTo[givenBy v] B)";
+by (auto_tac (claset(), 
+	      simpset() addsimps [project_leadsETo_D, Join_localTo]));
+qed "extending_leadsETo";
+
+
+Goalw [extending_def]
+     "extending (%G. reachable (extend h F Join G)) h F \
+\               ((v o f) LocalTo extend h F) \
+\               (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) \
+\               (A LeadsTo[givenBy v]  B)";
+
+by (force_tac (claset() addIs [project_LeadsETo_D],
+	       simpset()addsimps [LocalTo_def, Join_assoc RS sym, 
+				  Join_localTo]) 1);
+qed "extending_LeadsETo";
+
+
+Close_locale "Extend";
+
+
diff -r 0e4434d55df9 -r 296b03b79505 src/HOL/UNITY/ELT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/ELT.thy	Wed Dec 01 11:20:24 1999 +0100
@@ -0,0 +1,48 @@
+(*  Title:      HOL/UNITY/ELT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+leadsTo strengthened with a specification of the allowable sets transient parts
+*)
+
+ELT = Project +
+
+consts
+
+  (*LEADS-TO constant for the inductive definition*)
+  elt :: "['a set set, 'a program] => ('a set * 'a set) set"
+
+
+inductive "elt CC F"
+  intrs 
+
+    Basis  "[| F : A ensures B;  A-B : CC |] ==> (A,B) : elt CC F"
+
+    Trans  "[| (A,B) : elt CC F;  (B,C) : elt CC F |] ==> (A,C) : elt CC F"
+
+    Union  "{(A,B) | A. A: S} : Pow (elt CC F) ==> (Union S, B) : elt CC F"
+
+  monos Pow_mono
+
+
+constdefs
+
+  (*the set of all sets determined by f alone*)
+  givenBy :: "['a => 'b] => 'a set set"
+    "givenBy f == range (%B. f-`` B)"
+
+  funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
+    "funPair f g == %x. (f x, g x)"
+
+  (*visible version of the LEADS-TO relation*)
+  leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
+                                        ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
+    "leadsETo A CC B == {F. (A,B) : elt CC F}"
+
+  LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
+                                        ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80)
+    "LeadsETo A CC B ==
+      {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) `` CC] B}"
+
+end