--- a/src/HOL/IsaMakefile Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/IsaMakefile Wed Jan 29 11:02:08 2003 +0100
@@ -381,36 +381,24 @@
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
- UNITY/UNITY_Main.thy UNITY/Comp.ML UNITY/Comp.thy \
- UNITY/Detects.thy \
- UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \
+ UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
+ UNITY/Comp.ML UNITY/Comp.thy UNITY/Detects.thy UNITY/ELT.thy \
UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \
UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
- UNITY/Guar.ML UNITY/Guar.thy \
- UNITY/Lift_prog.thy \
- UNITY/ListOrder.thy \
- UNITY/PPROD.thy \
- UNITY/Project.ML UNITY/Project.thy \
- UNITY/Rename.ML UNITY/Rename.thy \
+ UNITY/Guar.ML UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \
+ UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \
UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML \
- UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML \
- UNITY/WFair.thy \
- UNITY/Simple/Channel.thy \
- UNITY/Simple/Common.thy \
- UNITY/Simple/Deadlock.thy \
- UNITY/Simple/Lift.thy \
- UNITY/Simple/Mutex.thy \
+ UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \
+ UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \
+ UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy \
- UNITY/Simple/Network.thy \
- UNITY/Simple/Reach.thy \
- UNITY/Simple/Reachability.thy \
- UNITY/Simple/Token.thy \
+ UNITY/Simple/Network.thy\
+ UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \
UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \
- UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy \
- UNITY/Comp/Handshake.thy \
+ UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \
UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy \
UNITY/Comp/TimerArray.thy
--- a/src/HOL/UNITY/ELT.ML Tue Jan 28 22:53:39 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,678 +0,0 @@
-(* 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
-*)
-
-(*** givenBy ***)
-
-Goalw [givenBy_def] "givenBy id = UNIV";
-by Auto_tac;
-qed "givenBy_id";
-Addsimps [givenBy_id];
-
-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";
-
-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] "{s. P(v s)} : givenBy v";
-by (Best_tac 1);
-qed "Collect_mem_givenBy";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (blast_tac (claset() addIs [Collect_mem_givenBy,
- givenBy_imp_eq_Collect]) 1);
-qed "givenBy_eq_Collect";
-
-(*preserving v preserves properties given by v*)
-Goal "[| F : preserves v; D : givenBy v |] ==> F : stable D";
-by (force_tac (claset(),
- simpset() addsimps [impOfSubs preserves_subset_stable,
- givenBy_eq_Collect]) 1);
-qed "preserves_givenBy_imp_stable";
-
-Goal "givenBy (w o v) <= givenBy v";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_subset";
-
-Goal "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v";
-by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
-by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
-qed "givenBy_DiffI";
-
-
-(** Standard leadsTo rules **)
-
-Goalw [leadsETo_def]
- "[| F: A ensures B; A-B: insert {} CC |] ==> F : A leadsTo[CC] B";
-by (blast_tac (claset() addIs [elt.Basis]) 1);
-qed "leadsETo_Basis";
-AddIs [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 : 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. 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";
-
-Goal "[| F : A leadsTo[CC] B; F : B leadsTo[DD] C |] \
-\ ==> F : A leadsTo[CC Un DD] C";
-by (blast_tac (claset() addIs [impOfSubs leadsETo_mono, leadsETo_Trans]) 1);
-qed "leadsETo_Trans_Un";
-
-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 ==> 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 **)
-
-Goal "[| F : A leadsTo[CC] A'; A'<=B' |] ==> 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 |] ==> 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 "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 "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 "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 |] \
-\ ==> F : B leadsTo[CC] B'";
-by (dtac (impOfSubs leadsETo_mono) 1);
-by (assume_tac 1);
-by (blast_tac (claset() delrules [subsetCE]
- 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 |] \
-\ ==> F : A leadsTo[CC] C";
-by (blast_tac (claset() addIs [leadsETo_Un, leadsETo_weaken]) 1);
-qed "leadsETo_Diff";
-
-
-(*Binary union version*)
-Goal "[| F : A leadsTo[CC] A'; F : B leadsTo[CC] B' |] \
-\ ==> 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' |] \
-\ ==> 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] (B Un A'); F : B leadsTo[CC] B' |] \
-\ ==> 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' |] \
-\ ==> 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 (force_tac (claset(),
- simpset() addsimps [Diff_Int_distrib2 RS sym]) 2);
-by (asm_full_simp_tac
- (simpset() addsimps [ensures_def,
- Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
-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 |] \
-\ ==> 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 (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 |] \
-\ ==> 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); G : preserves v; \
-\ 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 [Diff_eq_empty_iff RS iffD2,
- Int_Diff, ensures_def,
- givenBy_eq_Collect, Join_transient]));
-by (blast_tac (claset() addIs [transient_strengthen]) 3);
-by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable)));
-by (rewtac stable_def);
-by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 2);
-by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
-qed "gen_leadsETo_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_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";
-
-(**** Relationship with traditional "leadsTo", strong & weak ****)
-
-(** strong **)
-
-Goal "(A leadsTo[CC] B) <= (A leadsTo B)";
-by Safe_tac;
-by (etac leadsETo_induct 1);
-by (blast_tac (claset() addIs [leadsTo_Union]) 3);
-by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
-by (Blast_tac 1);
-qed "leadsETo_subset_leadsTo";
-
-Goal "(A leadsTo[UNIV] B) = (A leadsTo B)";
-by Safe_tac;
-by (etac (impOfSubs leadsETo_subset_leadsTo) 1);
-(*right-to-left case*)
-by (etac leadsTo_induct 1);
-by (blast_tac (claset() addIs [leadsETo_Union]) 3);
-by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
-by (Blast_tac 1);
-qed "leadsETo_UNIV_eq_leadsTo";
-
-(**** weak ****)
-
-Goalw [LeadsETo_def]
- "A LeadsTo[CC] B = \
-\ {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] \
-\ (reachable F Int B)}";
-by (blast_tac (claset() addDs [e_psp_stable2] addIs [leadsETo_weaken]) 1);
-qed "LeadsETo_eq_leadsETo";
-
-(*** Introduction rules: Basis, Trans, Union ***)
-
-Goal "[| F : A LeadsTo[CC] B; F : B LeadsTo[CC] C |] \
-\ ==> F : A LeadsTo[CC] C";
-by (asm_full_simp_tac (simpset() addsimps [LeadsETo_eq_leadsETo]) 1);
-by (blast_tac (claset() addIs [leadsETo_Trans]) 1);
-qed "LeadsETo_Trans";
-
-val prems = Goalw [LeadsETo_def]
- "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B";
-by (Simp_tac 1);
-by (stac Int_Union 1);
-by (blast_tac (claset() addIs [leadsETo_UN] 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 (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
-by (blast_tac (claset() addIs (LeadsETo_Union::prems)) 1);
-qed "LeadsETo_UN";
-
-(*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";
-
-(*Lets us look at the starting state*)
-val prems =
-Goal "(!!s. s : A ==> F : {s} 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 ==> F : A LeadsTo[CC] B";
-by (simp_tac (simpset() addsimps [LeadsETo_def]) 1);
-by (blast_tac (claset() addIs [subset_imp_leadsETo]) 1);
-qed "subset_imp_LeadsETo";
-
-bind_thm ("empty_LeadsETo", empty_subsetI RS subset_imp_LeadsETo);
-
-Goal "[| F : A LeadsTo[CC] A'; A' <= B' |] ==> F : A LeadsTo[CC] B'";
-by (full_simp_tac (simpset() addsimps [LeadsETo_def]) 1);
-by (blast_tac (claset() addIs [leadsETo_weaken_R]) 1);
-qed_spec_mp "LeadsETo_weaken_R";
-
-Goal "[| F : A LeadsTo[CC] A'; B <= A |] ==> F : B LeadsTo[CC] A'";
-by (full_simp_tac (simpset() addsimps [LeadsETo_def]) 1);
-by (blast_tac (claset() addIs [leadsETo_weaken_L]) 1);
-qed_spec_mp "LeadsETo_weaken_L";
-
-Goal "[| F : A LeadsTo[CC'] A'; \
-\ B <= A; A' <= B'; CC' <= CC |] \
-\ ==> F : B LeadsTo[CC] B'";
-by (full_simp_tac (simpset() addsimps [LeadsETo_def]) 1);
-by (blast_tac (claset() addIs [leadsETo_weaken]) 1);
-qed "LeadsETo_weaken";
-
-Goalw [LeadsETo_def, LeadsTo_def] "(A LeadsTo[CC] B) <= (A LeadsTo B)";
-by (blast_tac (claset() addIs [impOfSubs leadsETo_subset_leadsTo]) 1);
-qed "LeadsETo_subset_LeadsTo";
-
-(*Postcondition can be strengthened to (reachable F Int B) *)
-Goal "F : A ensures B ==> F : (reachable F Int A) ensures B";
-by (rtac (stable_ensures_Int RS ensures_weaken_R) 1);
-by Auto_tac;
-qed "reachable_ensures";
-
-Goal "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B";
-by (etac leadsTo_induct 1);
-by (stac Int_Union 3);
-by (blast_tac (claset() addIs [leadsETo_UN]) 3);
-by (blast_tac (claset() addDs [e_psp_stable2]
- addIs [leadsETo_Trans, leadsETo_weaken_L]) 2);
-by (blast_tac (claset() addIs [reachable_ensures, leadsETo_Basis]) 1);
-val lemma = result();
-
-Goal "(A LeadsTo[UNIV] B) = (A LeadsTo B)";
-by Safe_tac;
-by (etac (impOfSubs LeadsETo_subset_LeadsTo) 1);
-(*right-to-left case*)
-by (rewrite_goals_tac [LeadsETo_def, LeadsTo_def]);
-by (fast_tac (claset() addEs [lemma RS leadsETo_weaken]) 1);
-qed "LeadsETo_UNIV_eq_LeadsTo";
-
-
-(**** EXTEND/PROJECT PROPERTIES ****)
-
-Open_locale "Extend";
-
-(*givenBy laws that need to be in the locale*)
-
-Goal "givenBy (v o f) = extend_set h ` (givenBy v)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_eq_extend_set";
-
-Goal "givenBy f = range (extend_set h)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_eq_extend_set";
-
-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 (force_tac (claset() addIs [leadsETo_Basis, subset_imp_ensures],
- simpset() addsimps [extend_ensures,
- extend_set_Diff_distrib RS sym]) 1);
-qed "leadsETo_imp_extend_leadsETo";
-
-
-
-(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
-Goal "[| G : preserves (v o f); project h C G : transient D; \
-\ D : givenBy v |] ==> D={}";
-by (rtac stable_transient_empty 1);
-by (assume_tac 2);
-(*If addIs then PROOF FAILED at depth 2*)
-by (blast_tac (claset() addSIs [preserves_givenBy_imp_stable,
- project_preserves_I]) 1);
-result();
-
-
-(*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)) | \
-\ 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";
-
-(*Generalizes preserves_project_transient_empty*)
-Goal "[| G : preserves (v o f); \
-\ project h C G : transient (C' Int D); \
-\ project h C G : stable C'; D : givenBy v |] \
-\ ==> C' Int D = {}";
-by (rtac stable_transient_empty 1);
-by (assume_tac 2);
-(*If addIs then PROOF FAILED at depth 3*)
-by (blast_tac (claset() addSIs [stable_Int, preserves_givenBy_imp_stable,
- project_preserves_I]) 1);
-qed "preserves_o_project_transient_empty";
-
-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 : preserves (v o 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 Auto_tac;
-by (force_tac (claset() addIs [leadsETo_Basis, subset_imp_ensures],
- simpset()) 1);
-by (rtac leadsETo_Basis 1);
-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() addDs [preserves_o_project_transient_empty]
- addIs [project_stable_project_set],
- simpset() addsimps [Int_left_absorb]));
-by (asm_simp_tac
- (simpset() addsimps [stable_ensures_Int RS ensures_weaken_R,
- Int_lower2, project_stable_project_set,
- 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 : preserves (v o 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(),
- simpset() addsimps [split_extended_all]));
-qed "project_leadsETo_D_lemma";
-
-Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B; \
-\ G : preserves (v o 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_D_lemma) 1);
-by (stac stable_UNIV 1);
-by Auto_tac;
-by (etac leadsETo_givenBy 1);
-by (rtac (givenBy_o_eq_extend_set RS equalityD2) 1);
-qed "project_leadsETo_D";
-
-Goal "[| F Join project h (reachable (extend h F Join G)) G \
-\ : A LeadsTo[givenBy v] B; \
-\ G : preserves (v o 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_D_lemma)) 1);
-by (auto_tac (claset(),
- simpset() addsimps [LeadsETo_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]
- "(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) \
-\ (A leadsTo[givenBy v] B)";
-by (auto_tac (claset(), simpset() addsimps [project_leadsETo_D]));
-qed "extending_leadsETo";
-
-
-Goalw [extending_def]
- "(ALL G. extend h F ok G --> G : preserves (v o f)) \
-\ ==> extending (%G. reachable (extend h F Join G)) h F \
-\ (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) \
-\ (A LeadsTo[givenBy v] B)";
-by (blast_tac (claset() addIs [project_LeadsETo_D]) 1);
-qed "extending_LeadsETo";
-
-
-(*** leadsETo in the precondition ***)
-
-(*Lemma for the Trans case*)
-Goal "[| extend h F Join G : stable C; \
-\ F Join project h C G \
-\ : project_set h C Int project_set h A leadsTo project_set h B |] \
-\ ==> F Join project h C G \
-\ : project_set h C Int project_set h A leadsTo \
-\ project_set h C Int project_set h B";
-by (rtac (psp_stable2 RS leadsTo_weaken_L) 1);
-by (auto_tac (claset(),
- simpset() addsimps [project_stable_project_set,
- extend_stable_project_set]));
-val lemma = result();
-
-Goal "[| extend h F Join G : stable C; \
-\ extend h F Join G : \
-\ (C Int A) leadsTo[(%D. C Int D)`givenBy f] B |] \
-\ ==> F Join project h C G \
-\ : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)";
-by (etac leadsETo_induct 1);
-by (asm_simp_tac (HOL_ss addsimps [Int_UN_distrib, project_set_Union]) 3);
-by (blast_tac (claset() addIs [leadsTo_UN]) 3);
-by (blast_tac (claset() addIs [leadsTo_Trans, lemma]) 2);
-by (asm_full_simp_tac
- (simpset() addsimps [givenBy_eq_extend_set]) 1);
-by (rtac leadsTo_Basis 1);
-by (blast_tac (claset() addIs [ensures_extend_set_imp_project_ensures]) 1);
-
-qed "project_leadsETo_I_lemma";
-
-Goal "extend h F Join G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)\
-\ ==> F Join project h UNIV G : A leadsTo B";
-by (rtac (project_leadsETo_I_lemma RS leadsTo_weaken) 1);
-by Auto_tac;
-qed "project_leadsETo_I";
-
-Goal "extend h F Join G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B)\
-\ ==> F Join project h (reachable (extend h F Join G)) G \
-\ : A LeadsTo B";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def, LeadsETo_def]) 1);
-by (rtac (project_leadsETo_I_lemma RS leadsTo_weaken) 1);
-by (auto_tac (claset(),
- simpset() addsimps [project_set_reachable_extend_eq RS sym]));
-qed "project_LeadsETo_I";
-
-Goalw [projecting_def]
- "projecting (%G. UNIV) h F \
-\ (extend_set h A leadsTo[givenBy f] extend_set h B) \
-\ (A leadsTo B)";
-by (force_tac (claset() addDs [project_leadsETo_I], simpset()) 1);
-qed "projecting_leadsTo";
-
-Goalw [projecting_def]
- "projecting (%G. reachable (extend h F Join G)) h F \
-\ (extend_set h A LeadsTo[givenBy f] extend_set h B) \
-\ (A LeadsTo B)";
-by (force_tac (claset() addDs [project_LeadsETo_I], simpset()) 1);
-qed "projecting_LeadsTo";
-
-Close_locale "Extend";
-
-
--- a/src/HOL/UNITY/ELT.thy Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/UNITY/ELT.thy Wed Jan 29 11:02:08 2003 +0100
@@ -10,19 +10,19 @@
elt :: "['a set set, 'a program, 'a set] => ('a set) set"
inductive "elt CC F B"
- intrs
+ intros
- Weaken "A <= B ==> A : elt CC F B"
+ 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"
+ 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"
+ Union: "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B"
monos Pow_mono
*)
-ELT = Project +
+theory ELT = Project:
consts
@@ -31,13 +31,13 @@
inductive "elt CC F"
- intrs
+ intros
- Basis "[| F : A ensures B; A-B : (insert {} CC) |] ==> (A,B) : elt CC F"
+ 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"
+ Trans: "[| (A,B) : elt CC F; (B,C) : elt CC F |] ==> (A,C) : elt CC F"
- Union "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
+ Union: "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
constdefs
@@ -56,4 +56,662 @@
"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. ALL x:A. ALL y. v x = v y --> y: A}"
+apply (unfold givenBy_def, safe)
+apply (rule_tac [2] x = "v ` ?u" 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 ==> EX P. A = {s. P(v s)}"
+apply (rule_tac x = "%n. EX s. v s = n & s : A" in exI)
+apply (simp (no_asm_use) add: givenBy_eq_all)
+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. EX 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"
+apply (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect)
+done
+
+lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v"
+apply (simp (no_asm) add: givenBy_eq_Collect)
+apply best
+done
+
+lemma givenBy_DiffI:
+ "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v"
+apply (simp (no_asm_use) add: givenBy_eq_Collect)
+apply safe
+apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
+apply (tactic "deepen_tac (set_cs addSIs [equalityI]) 0 1")
+done
+
+
+(** Standard leadsTo rules **)
+
+lemma leadsETo_Basis [intro]:
+ "[| F: A ensures B; A-B: insert {} CC |] ==> F : A leadsTo[CC] B"
+apply (unfold leadsETo_def)
+apply (blast intro: elt.Basis)
+done
+
+lemma leadsETo_Trans:
+ "[| F : A leadsTo[CC] B; F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C"
+apply (unfold leadsETo_def)
+apply (blast intro: elt.Trans)
+done
+
+
+(*Useful with cancellation, disjunction*)
+lemma leadsETo_Un_duplicate:
+ "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'"
+apply (simp add: Un_ac)
+done
+
+lemma leadsETo_Un_duplicate2:
+ "F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)"
+by (simp add: Un_ac)
+
+(*The Union introduction rule as we should have liked to state it*)
+lemma leadsETo_Union:
+ "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B"
+apply (unfold leadsETo_def)
+apply (blast intro: elt.Union)
+done
+
+lemma leadsETo_UN:
+ "(!!i. i : I ==> F : (A i) leadsTo[CC] B)
+ ==> F : (UN i:I. A i) leadsTo[CC] B"
+apply (subst Union_image_eq [symmetric])
+apply (blast intro: leadsETo_Union)
+done
+
+(*The INDUCTION rule as we should have liked to state it*)
+lemma leadsETo_induct:
+ "[| 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. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B
+ |] ==> P za zb"
+apply (unfold leadsETo_def)
+apply (drule CollectD)
+apply (erule elt.induct, blast+)
+done
+
+
+(** New facts involving leadsETo **)
+
+lemma leadsETo_mono: "CC' <= CC ==> (A leadsTo[CC'] B) <= (A leadsTo[CC] B)"
+apply safe
+apply (erule leadsETo_induct)
+prefer 3 apply (blast intro: leadsETo_Union)
+prefer 2 apply (blast intro: leadsETo_Trans)
+apply (blast intro: leadsETo_Basis)
+done
+
+lemma leadsETo_Trans_Un:
+ "[| F : A leadsTo[CC] B; F : B leadsTo[DD] C |]
+ ==> F : A leadsTo[CC Un DD] C"
+by (blast intro: leadsETo_mono [THEN subsetD] leadsETo_Trans)
+
+lemma leadsETo_Union_Int:
+ "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B)
+ ==> F : (Union S Int C) leadsTo[CC] B"
+apply (unfold leadsETo_def)
+apply (simp only: Int_Union_Union)
+apply (blast intro: elt.Union)
+done
+
+(*Binary union introduction rule*)
+lemma leadsETo_Un:
+ "[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |]
+ ==> F : (A Un B) leadsTo[CC] C"
+apply (subst Un_eq_Union)
+apply (blast intro: leadsETo_Union)
+done
+
+lemma single_leadsETo_I:
+ "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
+apply (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
+done
+
+
+lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B"
+by (simp add: subset_imp_ensures [THEN leadsETo_Basis] Diff_eq_empty_iff [THEN iffD2])
+
+lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp]
+
+
+
+(** Weakening laws **)
+
+lemma leadsETo_weaken_R:
+ "[| F : A leadsTo[CC] A'; A'<=B' |] ==> F : A leadsTo[CC] B'"
+apply (blast intro: subset_imp_leadsETo leadsETo_Trans)
+done
+
+lemma leadsETo_weaken_L [rule_format (no_asm)]:
+ "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
+apply (blast intro: leadsETo_Trans subset_imp_leadsETo)
+done
+
+(*Distributes over binary unions*)
+lemma leadsETo_Un_distrib:
+ "F : (A Un B) leadsTo[CC] C =
+ (F : A leadsTo[CC] C & F : B leadsTo[CC] C)"
+apply (blast intro: leadsETo_Un leadsETo_weaken_L)
+done
+
+lemma leadsETo_UN_distrib:
+ "F : (UN i:I. A i) leadsTo[CC] B =
+ (ALL i : I. F : (A i) leadsTo[CC] B)"
+apply (blast intro: leadsETo_UN leadsETo_weaken_L)
+done
+
+lemma leadsETo_Union_distrib:
+ "F : (Union S) leadsTo[CC] B = (ALL A : S. F : A leadsTo[CC] B)"
+apply (blast intro: leadsETo_Union leadsETo_weaken_L)
+done
+
+lemma leadsETo_weaken:
+ "[| 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 intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
+done
+
+lemma leadsETo_givenBy:
+ "[| F : A leadsTo[CC] A'; CC <= givenBy v |]
+ ==> F : A leadsTo[givenBy v] A'"
+by (blast intro: empty_mem_givenBy leadsETo_weaken)
+
+
+(*Set difference*)
+lemma leadsETo_Diff:
+ "[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C |]
+ ==> F : A leadsTo[CC] C"
+by (blast intro: leadsETo_Un leadsETo_weaken)
+
+
+(*Binary union version*)
+lemma leadsETo_Un_Un:
+ "[| F : A leadsTo[CC] A'; F : B leadsTo[CC] B' |]
+ ==> F : (A Un B) leadsTo[CC] (A' Un B')"
+by (blast intro: leadsETo_Un leadsETo_weaken_R)
+
+
+(** The cancellation law **)
+
+lemma leadsETo_cancel2:
+ "[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B' |]
+ ==> F : A leadsTo[CC] (A' Un B')"
+by (blast intro: leadsETo_Un_Un subset_imp_leadsETo leadsETo_Trans)
+
+lemma leadsETo_cancel1:
+ "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B' |]
+ ==> F : A leadsTo[CC] (B' Un A')"
+apply (simp add: Un_commute)
+apply (blast intro!: leadsETo_cancel2)
+done
+
+lemma leadsETo_cancel_Diff1:
+ "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]
+ ==> F : A leadsTo[CC] (B' Un A')"
+apply (rule leadsETo_cancel1)
+prefer 2 apply assumption
+apply (simp_all (no_asm_simp))
+done
+
+
+(** The impossibility law **)
+
+lemma leadsETo_empty_lemma: "F : A leadsTo[CC] B ==> B={} --> A={}"
+apply (erule leadsETo_induct)
+apply (simp_all (no_asm_simp))
+apply (unfold ensures_def constrains_def transient_def, blast)
+done
+
+lemma leadsETo_empty: "F : A leadsTo[CC] {} ==> A={}"
+by (blast intro!: leadsETo_empty_lemma [THEN mp])
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction"*)
+lemma e_psp_stable:
+ "[| F : A leadsTo[CC] A'; F : stable B; ALL C:CC. C Int B : CC |]
+ ==> F : (A Int B) leadsTo[CC] (A' Int B)"
+apply (unfold stable_def)
+apply (erule leadsETo_induct)
+prefer 3 apply (blast intro: leadsETo_Union_Int)
+prefer 2 apply (blast intro: leadsETo_Trans)
+apply (rule leadsETo_Basis)
+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; ALL 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';
+ ALL C:CC. C Int B Int B' : CC |]
+ ==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))"
+apply (erule leadsETo_induct)
+prefer 3 apply (blast intro: leadsETo_Union_Int)
+(*Transitivity case has a delicate argument involving "cancellation"*)
+apply (rule_tac [2] leadsETo_Un_duplicate2)
+apply (erule_tac [2] leadsETo_cancel_Diff1)
+prefer 2
+ apply (simp add: Int_Diff Diff_triv)
+ apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset)
+(*Basis case*)
+apply (rule leadsETo_Basis)
+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';
+ ALL C:CC. C Int B Int B' : CC |]
+ ==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))"
+by (simp add: e_psp Int_ac)
+
+
+(*** Special properties involving the parameter [CC] ***)
+
+(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
+lemma gen_leadsETo_imp_Join_leadsETo:
+ "[| F: (A leadsTo[givenBy v] B); G : preserves v;
+ F Join G : stable C |]
+ ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
+apply (erule leadsETo_induct)
+ prefer 3
+ apply (subst Int_Union)
+ apply (blast intro: leadsETo_UN)
+prefer 2
+ apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
+apply (rule leadsETo_Basis)
+apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] Int_Diff ensures_def givenBy_eq_Collect Join_transient)
+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
+
+(*useful??*)
+lemma Join_leadsETo_stable_imp_leadsETo:
+ "[| F Join G : (A leadsTo[CC] B); ALL C:CC. G : stable C |]
+ ==> F: (A leadsTo[CC] B)"
+apply (erule leadsETo_induct)
+prefer 3 apply (blast intro: leadsETo_Union)
+prefer 2 apply (blast intro: leadsETo_Trans)
+apply (rule leadsETo_Basis)
+apply (case_tac "A <= B")
+apply (erule subset_imp_ensures)
+apply (auto intro: constrains_weaken simp add: stable_def ensures_def Join_transient)
+apply (erule_tac V = "?F : ?A co ?B" in thin_rl)+
+apply (erule transientE)
+apply (unfold constrains_def)
+apply (blast dest!: bspec)
+done
+
+(**** Relationship with traditional "leadsTo", strong & weak ****)
+
+(** strong **)
+
+lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)"
+apply safe
+apply (erule leadsETo_induct)
+prefer 3 apply (blast intro: leadsTo_Union)
+prefer 2 apply (blast intro: leadsTo_Trans, blast)
+done
+
+lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)"
+apply safe
+apply (erule leadsETo_subset_leadsTo [THEN subsetD])
+(*right-to-left case*)
+apply (erule leadsTo_induct)
+prefer 3 apply (blast intro: leadsETo_Union)
+prefer 2 apply (blast intro: leadsETo_Trans, blast)
+done
+
+(**** weak ****)
+
+lemma LeadsETo_eq_leadsETo:
+ "A LeadsTo[CC] B =
+ {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC]
+ (reachable F Int B)}"
+apply (unfold LeadsETo_def)
+apply (blast dest: e_psp_stable2 intro: leadsETo_weaken)
+done
+
+(*** Introduction rules: Basis, Trans, Union ***)
+
+lemma LeadsETo_Trans:
+ "[| F : A LeadsTo[CC] B; F : B LeadsTo[CC] C |]
+ ==> F : A LeadsTo[CC] C"
+apply (simp add: LeadsETo_eq_leadsETo)
+apply (blast intro: leadsETo_Trans)
+done
+
+lemma LeadsETo_Union:
+ "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
+apply (simp add: LeadsETo_def)
+apply (subst Int_Union)
+apply (blast intro: leadsETo_UN)
+done
+
+lemma LeadsETo_UN:
+ "(!!i. i : I ==> F : (A i) LeadsTo[CC] B)
+ ==> F : (UN i:I. A i) LeadsTo[CC] B"
+apply (simp only: Union_image_eq [symmetric])
+apply (blast intro: LeadsETo_Union)
+done
+
+(*Binary union introduction rule*)
+lemma LeadsETo_Un:
+ "[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]
+ ==> F : (A Un B) LeadsTo[CC] C"
+apply (subst Un_eq_Union)
+apply (blast intro: LeadsETo_Union)
+done
+
+(*Lets us look at the starting state*)
+lemma single_LeadsETo_I:
+ "(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B"
+apply (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
+done
+
+lemma subset_imp_LeadsETo:
+ "A <= B ==> F : A LeadsTo[CC] B"
+apply (simp (no_asm) add: LeadsETo_def)
+apply (blast intro: subset_imp_leadsETo)
+done
+
+lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
+
+lemma LeadsETo_weaken_R [rule_format (no_asm)]:
+ "[| F : A LeadsTo[CC] A'; A' <= B' |] ==> F : A LeadsTo[CC] B'"
+apply (simp (no_asm_use) add: LeadsETo_def)
+apply (blast intro: leadsETo_weaken_R)
+done
+
+lemma LeadsETo_weaken_L [rule_format (no_asm)]:
+ "[| F : A LeadsTo[CC] A'; B <= A |] ==> F : B LeadsTo[CC] A'"
+apply (simp (no_asm_use) add: LeadsETo_def)
+apply (blast intro: leadsETo_weaken_L)
+done
+
+lemma LeadsETo_weaken:
+ "[| F : A LeadsTo[CC'] A';
+ B <= A; A' <= B'; CC' <= CC |]
+ ==> F : B LeadsTo[CC] B'"
+apply (simp (no_asm_use) add: LeadsETo_def)
+apply (blast intro: leadsETo_weaken)
+done
+
+lemma LeadsETo_subset_LeadsTo: "(A LeadsTo[CC] B) <= (A LeadsTo B)"
+apply (unfold LeadsETo_def LeadsTo_def)
+apply (blast intro: leadsETo_subset_leadsTo [THEN subsetD])
+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 (erule leadsTo_induct)
+ apply (blast intro: reachable_ensures leadsETo_Basis)
+ apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
+apply (subst Int_Union)
+apply (blast intro: leadsETo_UN)
+done
+
+lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)"
+apply safe
+apply (erule LeadsETo_subset_LeadsTo [THEN subsetD])
+(*right-to-left case*)
+apply (unfold LeadsETo_def LeadsTo_def)
+apply (fast elim: lel_lemma [THEN leadsETo_weaken])
+done
+
+
+(**** EXTEND/PROJECT PROPERTIES ****)
+
+lemma (in Extend) givenBy_o_eq_extend_set: "givenBy (v o f) = extend_set h ` (givenBy v)"
+apply (simp (no_asm) add: givenBy_eq_Collect)
+apply best
+done
+
+lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
+apply (simp (no_asm) add: givenBy_eq_Collect)
+apply best
+done
+
+lemma (in Extend) extend_set_givenBy_I:
+ "D : givenBy v ==> extend_set h D : givenBy (v o f)"
+apply (simp (no_asm_use) add: givenBy_eq_all)
+apply blast
+done
+
+lemma (in Extend) leadsETo_imp_extend_leadsETo:
+ "F : A leadsTo[CC] B
+ ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]
+ (extend_set h B)"
+apply (erule leadsETo_induct)
+ apply (force intro: leadsETo_Basis subset_imp_ensures
+ simp add: extend_ensures extend_set_Diff_distrib [symmetric])
+ apply (blast intro: leadsETo_Trans)
+apply (simp add: leadsETo_UN extend_set_Union)
+done
+
+
+
+(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
+lemma (in Extend)
+ "[| G : preserves (v o f); project h C G : transient D;
+ D : givenBy v |] ==> D={}"
+apply (rule stable_transient_empty)
+ prefer 2 apply assumption
+(*If addIs then PROOF FAILED at depth 2*)
+apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)
+done
+
+
+(*This version's stronger in the "ensures" precondition
+ BUT there's no ensures_weaken_L*)
+lemma (in Extend) 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 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)"
+apply (subst Int_extend_set_lemma [symmetric])
+apply (rule Join_project_ensures)
+apply (auto simp add: Int_Diff)
+done
+
+(*Generalizes preserves_project_transient_empty*)
+lemma (in Extend) preserves_o_project_transient_empty:
+ "[| G : preserves (v o f);
+ project h C G : transient (C' Int D);
+ project h C G : stable C'; D : givenBy v |]
+ ==> C' Int D = {}"
+apply (rule stable_transient_empty)
+prefer 2 apply assumption
+(*Fragile proof. Was just a single blast call.
+ If just "intro" then PROOF FAILED at depth 3*)
+apply (rule stable_Int)
+ apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)+
+done
+
+lemma (in Extend) pld_lemma:
+ "[| 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 : preserves (v o 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)"
+apply (erule leadsETo_induct)
+ prefer 3
+ apply (simp del: UN_simps add: Int_UN_distrib leadsETo_UN extend_set_Union)
+ prefer 2
+ apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
+txt{*Base case is hard*}
+apply auto
+apply (force intro: leadsETo_Basis subset_imp_ensures)
+apply (rule leadsETo_Basis)
+ prefer 2
+ apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
+apply (rule Join_project_ensures_strong)
+apply (auto dest: preserves_o_project_transient_empty 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
+
+lemma (in Extend) project_leadsETo_D_lemma:
+ "[| 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 : preserves (v o 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)"
+apply (rule pld_lemma [THEN leadsETo_weaken])
+apply (auto simp add: split_extended_all)
+done
+
+lemma (in Extend) project_leadsETo_D:
+ "[| F Join project h UNIV G : A leadsTo[givenBy v] B;
+ G : preserves (v o f) |]
+ ==> extend h F Join 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 (erule leadsETo_givenBy)
+apply (rule givenBy_o_eq_extend_set [THEN equalityD2])
+done
+
+lemma (in Extend) project_LeadsETo_D:
+ "[| F Join project h (reachable (extend h F Join G)) G
+ : A LeadsTo[givenBy v] B;
+ G : preserves (v o f) |]
+ ==> extend h F Join 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 (auto simp add: LeadsETo_def)
+ apply (erule leadsETo_mono [THEN [2] rev_subsetD])
+ apply (blast intro: extend_set_givenBy_I)
+apply (simp add: project_set_reachable_extend_eq [symmetric])
+done
+
+lemma (in Extend) extending_leadsETo:
+ "(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)
+ (A leadsTo[givenBy v] B)"
+apply (unfold extending_def)
+apply (auto simp add: project_leadsETo_D)
+done
+
+lemma (in Extend) extending_LeadsETo:
+ "(ALL G. extend h F ok G --> G : preserves (v o f))
+ ==> extending (%G. reachable (extend h F Join G)) h F
+ (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)
+ (A LeadsTo[givenBy v] B)"
+apply (unfold extending_def)
+apply (blast intro: project_LeadsETo_D)
+done
+
+
+(*** leadsETo in the precondition ***)
+
+(*Lemma for the Trans case*)
+lemma (in Extend) pli_lemma:
+ "[| extend h F Join G : stable C;
+ F Join project h C G
+ : project_set h C Int project_set h A leadsTo project_set h B |]
+ ==> F Join project h C G
+ : project_set h C Int project_set h A leadsTo
+ project_set h C Int project_set h B"
+apply (rule psp_stable2 [THEN leadsTo_weaken_L])
+apply (auto simp add: project_stable_project_set extend_stable_project_set)
+done
+
+lemma (in Extend) project_leadsETo_I_lemma:
+ "[| extend h F Join G : stable C;
+ extend h F Join G :
+ (C Int A) leadsTo[(%D. C Int D)`givenBy f] B |]
+ ==> F Join project h C G
+ : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
+apply (erule leadsETo_induct)
+ prefer 3
+ apply (simp only: Int_UN_distrib project_set_Union)
+ apply (blast intro: leadsTo_UN)
+ prefer 2 apply (blast intro: leadsTo_Trans pli_lemma)
+apply (simp add: givenBy_eq_extend_set)
+apply (rule leadsTo_Basis)
+apply (blast intro: ensures_extend_set_imp_project_ensures)
+done
+
+lemma (in Extend) project_leadsETo_I:
+ "extend h F Join G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
+ ==> F Join project h UNIV G : A leadsTo B"
+apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
+done
+
+lemma (in Extend) project_LeadsETo_I:
+ "extend h F Join G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B)
+ ==> F Join project h (reachable (extend h F Join G)) G
+ : A LeadsTo B"
+apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def)
+apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken])
+apply (auto simp add: project_set_reachable_extend_eq [symmetric])
+done
+
+lemma (in Extend) projecting_leadsTo:
+ "projecting (%G. UNIV) h F
+ (extend_set h A leadsTo[givenBy f] extend_set h B)
+ (A leadsTo B)"
+apply (unfold projecting_def)
+apply (force dest: project_leadsETo_I)
+done
+
+lemma (in Extend) projecting_LeadsTo:
+ "projecting (%G. reachable (extend h F Join G)) h F
+ (extend_set h A LeadsTo[givenBy f] extend_set h B)
+ (A LeadsTo B)"
+apply (unfold projecting_def)
+apply (force dest: project_LeadsETo_I)
+done
+
end
--- a/src/HOL/UNITY/Extend.ML Tue Jan 28 22:53:39 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,795 +0,0 @@
-(* Title: HOL/UNITY/Extend.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Extending 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"
-*)
-
-(** These we prove OUTSIDE the locale. **)
-
-
-(*** Restrict [MOVE to Relation.thy?] ***)
-
-Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)";
-by (Blast_tac 1);
-qed "Restrict_iff";
-AddIffs [Restrict_iff];
-
-Goal "Restrict UNIV = id";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
-qed "Restrict_UNIV";
-Addsimps [Restrict_UNIV];
-
-Goal "Restrict {} r = {}";
-by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
-qed "Restrict_empty";
-Addsimps [Restrict_empty];
-
-Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r";
-by (Blast_tac 1);
-qed "Restrict_Int";
-Addsimps [Restrict_Int];
-
-Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r";
-by Auto_tac;
-qed "Restrict_triv";
-
-Goalw [Restrict_def] "Restrict A r <= r";
-by Auto_tac;
-qed "Restrict_subset";
-
-Goalw [Restrict_def]
- "[| A <= B; Restrict B r = Restrict B s |] \
-\ ==> Restrict A r = Restrict A s";
-by (Blast_tac 1);
-qed "Restrict_eq_mono";
-
-Goalw [Restrict_def, image_def]
- "[| s : RR; Restrict A r = Restrict A s |] \
-\ ==> Restrict A r : Restrict A ` RR";
-by Auto_tac;
-qed "Restrict_imageI";
-
-Goal "Domain (Restrict A r) = A Int Domain r";
-by (Blast_tac 1);
-qed "Domain_Restrict";
-
-Goal "(Restrict A r) `` B = r `` (A Int B)";
-by (Blast_tac 1);
-qed "Image_Restrict";
-
-Addsimps [Domain_Restrict, Image_Restrict];
-
-
-Goal "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F";
-by (blast_tac (claset() addIs [sym RS image_eqI]) 1);
-qed "insert_Id_image_Acts";
-
-(*Possibly easier than reasoning about "inv h"*)
-val [surj_h,prem] =
-Goalw [good_map_def]
- "[| surj h; !! x x' y y'. h(x,y) = h(x',y') ==> x=x' |] ==> good_map h";
-by (safe_tac (claset() addSIs [surj_h]));
-by (rtac prem 1);
-by (stac (surjective_pairing RS sym) 1);
-by (stac (surj_h RS surj_f_inv_f) 1);
-by (rtac refl 1);
-qed "good_mapI";
-
-Goalw [good_map_def] "good_map h ==> surj h";
-by Auto_tac;
-qed "good_map_is_surj";
-
-(*A convenient way of finding a closed form for inv h*)
-val [surj,prem] = Goalw [inv_def]
- "[| surj h; !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z";
-by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1);
-by (rtac someI2 1);
-by (dres_inst_tac [("f", "g")] arg_cong 2);
-by (auto_tac (claset(), simpset() addsimps [prem]));
-qed "fst_inv_equalityI";
-
-
-Open_locale "Extend";
-
-val slice_def = thm "slice_def";
-
-(*** Trivial properties of f, g, h ***)
-
-val good_h = rewrite_rule [good_map_def] (thm "good_h");
-val surj_h = good_h RS conjunct1;
-
-val f_def = thm "f_def";
-val g_def = thm "g_def";
-
-Goal "f(h(x,y)) = x";
-by (simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1);
-qed "f_h_eq";
-Addsimps [f_h_eq];
-
-Goal "h(x,y) = h(x',y') ==> x=x'";
-by (dres_inst_tac [("f", "fst o inv h")] arg_cong 1);
-(*FIXME: If locales worked properly we could put just "f" above*)
-by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1);
-qed "h_inject1";
-AddDs [h_inject1];
-
-Goal "h(f z, g z) = z";
-by (simp_tac (simpset() addsimps [f_def, g_def, surj_h RS surj_f_inv_f]) 1);
-qed "h_f_g_eq";
-
-
-(** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
-
-val cT = TFree ("'c", HOLogic.typeS);
-
-(* "PROP P x == PROP P (h (f x, g x))" *)
-val lemma1 = Thm.combination
- (Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT))))
- (Drule.unvarify (h_f_g_eq RS sym RS eq_reflection));
-
-val prems = Goalw [lemma1] "(!!u y. PROP P (h (u, y))) ==> PROP P x";
-by (resolve_tac prems 1);
-val lemma2 = result();
-
-val prems = Goal "(!!u y. PROP P (h (u, y))) ==> (!!z. PROP P z)";
-by (rtac lemma2 1);
-by (resolve_tac prems 1);
-val lemma3 = result();
-
-val prems = Goal "(!!z. PROP P z) ==> (!!u y. PROP P (h (u, y)))";
-(*not needed for proof, but prevents generalization over h, 'c, etc.*)
-by (cut_facts_tac [surj_h] 1);
-by (resolve_tac prems 1);
-val lemma4 = result();
-
-val split_extended_all = Thm.equal_intr lemma4 lemma3;
-
-
-(*** extend_set: basic properties ***)
-
-Goal "(x : project_set h C) = (EX y. h(x,y) : C)";
-by (simp_tac (simpset() addsimps [project_set_def]) 1);
-qed "project_set_iff";
-
-AddIffs [project_set_iff];
-
-Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
-by (Blast_tac 1);
-qed "extend_set_mono";
-
-Goalw [extend_set_def] "z : extend_set h A = (f z : A)";
-by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1);
-qed "mem_extend_set_iff";
-
-AddIffs [mem_extend_set_iff];
-
-Goalw [extend_set_def] "(extend_set h A <= extend_set h B) = (A <= B)";
-by (Force_tac 1);
-qed "extend_set_strict_mono";
-AddIffs [extend_set_strict_mono];
-
-Goalw [extend_set_def] "extend_set h {} = {}";
-by Auto_tac;
-qed "extend_set_empty";
-Addsimps [extend_set_empty];
-
-Goal "extend_set h {s. P s} = {s. P (f s)}";
-by Auto_tac;
-qed "extend_set_eq_Collect";
-
-Goal "extend_set h {x} = {s. f s = x}";
-by Auto_tac;
-qed "extend_set_sing";
-
-Goalw [extend_set_def] "project_set h (extend_set h C) = C";
-by Auto_tac;
-qed "extend_set_inverse";
-Addsimps [extend_set_inverse];
-
-Goalw [extend_set_def] "C <= extend_set h (project_set h C)";
-by (auto_tac (claset(),
- simpset() addsimps [split_extended_all]));
-by (Blast_tac 1);
-qed "extend_set_project_set";
-
-Goal "inj (extend_set h)";
-by (rtac inj_on_inverseI 1);
-by (rtac extend_set_inverse 1);
-qed "inj_extend_set";
-
-Goalw [extend_set_def] "extend_set h UNIV = UNIV";
-by (auto_tac (claset(),
- simpset() addsimps [split_extended_all]));
-qed "extend_set_UNIV_eq";
-Addsimps [standard extend_set_UNIV_eq];
-
-(*** project_set: basic properties ***)
-
-(*project_set is simply image!*)
-Goal "project_set h C = f ` C";
-by (auto_tac (claset() addIs [f_h_eq RS sym],
- simpset() addsimps [split_extended_all]));
-qed "project_set_eq";
-
-(*Converse appears to fail*)
-Goal "!!z. z : C ==> f z : project_set h C";
-by (auto_tac (claset(),
- simpset() addsimps [split_extended_all]));
-qed "project_set_I";
-
-
-(*** More laws ***)
-
-(*Because A and B could differ on the "other" part of the state,
- cannot generalize to
- project_set h (A Int B) = project_set h A Int project_set h B
-*)
-Goal "project_set h ((extend_set h A) Int B) = A Int (project_set h B)";
-by Auto_tac;
-qed "project_set_extend_set_Int";
-
-(*Unused, but interesting?*)
-Goal "project_set h ((extend_set h A) Un B) = A Un (project_set h B)";
-by Auto_tac;
-qed "project_set_extend_set_Un";
-
-Goal "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
-by Auto_tac;
-qed "project_set_Int_subset";
-
-Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B";
-by Auto_tac;
-qed "extend_set_Un_distrib";
-
-Goal "extend_set h (A Int B) = extend_set h A Int extend_set h B";
-by Auto_tac;
-qed "extend_set_Int_distrib";
-
-Goal "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))";
-by Auto_tac;
-qed "extend_set_INT_distrib";
-
-Goal "extend_set h (A - B) = extend_set h A - extend_set h B";
-by Auto_tac;
-qed "extend_set_Diff_distrib";
-
-Goal "extend_set h (Union A) = (UN X:A. extend_set h X)";
-by (Blast_tac 1);
-qed "extend_set_Union";
-
-Goalw [extend_set_def] "(extend_set h A <= - extend_set h B) = (A <= - B)";
-by Auto_tac;
-qed "extend_set_subset_Compl_eq";
-
-
-(*** 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*)
-Goalw [extend_act_def]
- "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";
-by Auto_tac;
-qed "mem_extend_act_iff";
-AddIffs [mem_extend_act_iff];
-
-(*Converse fails: (z,z') would include actions that changed the g-part*)
-Goalw [extend_act_def]
- "(z, z') : extend_act h act ==> (f z, f z') : act";
-by Auto_tac;
-qed "extend_act_D";
-
-Goalw [extend_act_def, project_act_def]
- "project_act h (extend_act h act) = act";
-by (Blast_tac 1);
-qed "extend_act_inverse";
-Addsimps [extend_act_inverse];
-
-Goalw [extend_act_def, project_act_def]
- "project_act h (Restrict C (extend_act h act)) = \
-\ Restrict (project_set h C) act";
-by (Blast_tac 1);
-qed "project_act_extend_act_restrict";
-Addsimps [project_act_extend_act_restrict];
-
-Goalw [extend_act_def, project_act_def]
- "act' <= extend_act h act ==> project_act h act' <= act";
-by (Force_tac 1);
-qed "subset_extend_act_D";
-
-Goal "inj (extend_act h)";
-by (rtac inj_on_inverseI 1);
-by (rtac extend_act_inverse 1);
-qed "inj_extend_act";
-
-Goalw [extend_set_def, extend_act_def]
- "extend_act h act `` (extend_set h A) = extend_set h (act `` A)";
-by (Force_tac 1);
-qed "extend_act_Image";
-Addsimps [extend_act_Image];
-
-Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)";
-by Auto_tac;
-qed "extend_act_strict_mono";
-
-AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq];
-(*The latter theorem is (extend_act h act' = extend_act h act) = (act'=act) *)
-
-Goalw [extend_set_def, extend_act_def]
- "Domain (extend_act h act) = extend_set h (Domain act)";
-by (Force_tac 1);
-qed "Domain_extend_act";
-
-Goalw [extend_act_def]
- "extend_act h Id = Id";
-by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1);
-qed "extend_act_Id";
-
-Goalw [project_act_def]
- "!!z z'. (z, z') : act ==> (f z, f z') : project_act h act";
-by (force_tac (claset(),
- simpset() addsimps [split_extended_all]) 1);
-qed "project_act_I";
-
-Goalw [project_act_def] "project_act h Id = Id";
-by (Force_tac 1);
-qed "project_act_Id";
-
-Goalw [project_act_def]
- "Domain (project_act h act) = project_set h (Domain act)";
-by (force_tac (claset(),
- simpset() addsimps [split_extended_all]) 1);
-qed "Domain_project_act";
-
-Addsimps [extend_act_Id, project_act_Id];
-
-
-(**** extend ****)
-
-(*** Basic properties ***)
-
-Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)";
-by Auto_tac;
-qed "Init_extend";
-Addsimps [Init_extend];
-
-Goalw [project_def] "Init (project h C F) = project_set h (Init F)";
-by Auto_tac;
-qed "Init_project";
-Addsimps [Init_project];
-
-Goal "Acts (extend h F) = (extend_act h ` Acts F)";
-by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
-qed "Acts_extend";
-Addsimps [Acts_extend];
-
-Goal "AllowedActs (extend h F) = project_act h -` AllowedActs F";
-by (simp_tac (simpset() addsimps [extend_def, insert_absorb]) 1);
-qed "AllowedActs_extend";
-Addsimps [AllowedActs_extend];
-
-Goal "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)";
-by (auto_tac (claset(),
- simpset() addsimps [project_def, image_iff]));
-qed "Acts_project";
-Addsimps [Acts_project];
-
-Goal "AllowedActs(project h C F) = \
-\ {act. Restrict (project_set h C) act \
-\ : project_act h ` Restrict C ` AllowedActs F}";
-by (simp_tac (simpset() addsimps [project_def, image_iff]) 1);
-by (stac insert_absorb 1);
-by (auto_tac (claset() addSIs [inst "x" "Id" bexI],
- simpset() addsimps [project_act_def]));
-qed "AllowedActs_project";
-Addsimps [AllowedActs_project];
-
-Goal "Allowed (extend h F) = project h UNIV -` Allowed F";
-by (simp_tac (simpset() addsimps [AllowedActs_extend, Allowed_def]) 1);
-by (Blast_tac 1);
-qed "Allowed_extend";
-
-Goalw [SKIP_def] "extend h SKIP = SKIP";
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "extend_SKIP";
-Addsimps [export extend_SKIP];
-
-Goal "project_set h UNIV = UNIV";
-by Auto_tac;
-qed "project_set_UNIV";
-Addsimps [project_set_UNIV];
-
-Goal "project_set h (Union A) = (UN X:A. project_set h X)";
-by (Blast_tac 1);
-qed "project_set_Union";
-
-(*Converse FAILS: the extended state contributing to project_set h C
- may not coincide with the one contributing to project_act h act*)
-Goal "project_act h (Restrict C act) <= \
-\ Restrict (project_set h C) (project_act h act)";
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));
-qed "project_act_Restrict_subset";
-
-
-Goal "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));
-qed "project_act_Restrict_Id_eq";
-
-Goal "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)})";
-by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [project_def]) 1);
-qed "project_extend_eq";
-
-Goal "project h UNIV (extend h F) = F";
-by (asm_simp_tac (simpset() addsimps [project_extend_eq, image_eq_UN,
- subset_UNIV RS subset_trans RS Restrict_triv]) 1);
-by (rtac program_equalityI 1);
-by (ALLGOALS Simp_tac);
-by (stac insert_absorb 1);
-by (simp_tac (simpset() addsimps [inst "x" "Id" bexI]) 1);
-by Auto_tac;
-by (rename_tac "act" 1);
-by (res_inst_tac [("x","extend_act h act")] bexI 1);
-by Auto_tac;
-qed "extend_inverse";
-Addsimps [extend_inverse];
-
-Goal "inj (extend h)";
-by (rtac inj_on_inverseI 1);
-by (rtac extend_inverse 1);
-qed "inj_extend";
-
-Goal "extend h (F Join G) = extend h F Join extend h G";
-by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_Un]) 2);
-by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1);
-by Auto_tac;
-qed "extend_Join";
-Addsimps [extend_Join];
-
-Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))";
-by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_UN]) 2);
-by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1);
-by Auto_tac;
-qed "extend_JN";
-Addsimps [extend_JN];
-
-(** These monotonicity results look natural but are UNUSED **)
-
-Goal "F <= G ==> extend h F <= extend h G";
-by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by Auto_tac;
-qed "extend_mono";
-
-Goal "F <= G ==> project h C F <= project h C G";
-by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by (Blast_tac 1);
-qed "project_mono";
-
-
-(*** Safety: co, stable ***)
-
-Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
-\ (F : A co B)";
-by (simp_tac (simpset() addsimps [constrains_def]) 1);
-qed "extend_constrains";
-
-Goal "(extend h F : stable (extend_set h A)) = (F : stable A)";
-by (asm_simp_tac (simpset() addsimps [stable_def, extend_constrains]) 1);
-qed "extend_stable";
-
-Goal "(extend h F : invariant (extend_set h A)) = (F : invariant A)";
-by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
-qed "extend_invariant";
-
-(*Projects the state predicates in the property satisfied by extend h F.
- Converse fails: A and B may differ in their extra variables*)
-Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
-by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-by (Force_tac 1);
-qed "extend_constrains_project_set";
-
-Goal "extend h F : stable A ==> F : stable (project_set h A)";
-by (asm_full_simp_tac
- (simpset() addsimps [stable_def, extend_constrains_project_set]) 1);
-qed "extend_stable_project_set";
-
-
-(*** Weak safety primitives: Co, Stable ***)
-
-Goal "p : reachable (extend h F) ==> f p : reachable F";
-by (etac reachable.induct 1);
-by (auto_tac
- (claset() addIs reachable.intrs,
- simpset() addsimps [extend_act_def, image_iff]));
-qed "reachable_extend_f";
-
-Goal "h(s,y) : reachable (extend h F) ==> s : reachable F";
-by (force_tac (claset() addSDs [reachable_extend_f], simpset()) 1);
-qed "h_reachable_extend";
-
-Goalw [extend_set_def]
- "reachable (extend h F) = extend_set h (reachable F)";
-by (rtac equalityI 1);
-by (force_tac (claset() addIs [h_f_g_eq RS sym]
- addSDs [reachable_extend_f],
- simpset()) 1);
-by (Clarify_tac 1);
-by (etac reachable.induct 1);
-by (ALLGOALS (force_tac (claset() addIs reachable.intrs,
- simpset())));
-qed "reachable_extend_eq";
-
-Goal "(extend h F : (extend_set h A) Co (extend_set h B)) = \
-\ (F : A Co B)";
-by (simp_tac
- (simpset() addsimps [Constrains_def, reachable_extend_eq,
- extend_constrains, extend_set_Int_distrib RS sym]) 1);
-qed "extend_Constrains";
-
-Goal "(extend h F : Stable (extend_set h A)) = (F : Stable A)";
-by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1);
-qed "extend_Stable";
-
-Goal "(extend h F : Always (extend_set h A)) = (F : Always A)";
-by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1);
-qed "extend_Always";
-
-
-(** Safety and "project" **)
-
-(** projection: monotonicity for safety **)
-
-Goal "D <= C ==> \
-\ project_act h (Restrict D act) <= project_act h (Restrict C act)";
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));
-qed "project_act_mono";
-
-Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
-by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-by (dtac project_act_mono 1);
-by (Blast_tac 1);
-qed "project_constrains_mono";
-
-Goal "[| D <= C; project h C F : stable A |] ==> project h D F : stable A";
-by (asm_full_simp_tac
- (simpset() addsimps [stable_def, project_constrains_mono]) 1);
-qed "project_stable_mono";
-
-(*Key lemma used in several proofs about project and co*)
-Goalw [constrains_def]
- "(project h C F : A co B) = \
-\ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
-by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
-by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
-(*the <== direction*)
-by (rewtac project_act_def);
-by (force_tac (claset() addSDs [subsetD], simpset()) 1);
-qed "project_constrains";
-
-Goalw [stable_def]
- "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
-by (simp_tac (simpset() addsimps [project_constrains]) 1);
-qed "project_stable";
-
-Goal "F : stable (extend_set h A) ==> project h C F : stable A";
-by (dtac (project_stable RS iffD2) 1);
-by (blast_tac (claset() addIs [project_stable_mono]) 1);
-qed "project_stable_I";
-
-Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
-by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
-qed "Int_extend_set_lemma";
-
-(*Strange (look at occurrences of C) but used in leadsETo proofs*)
-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]) 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";
-
-
-(*** Progress: transient, ensures ***)
-
-Goal "(extend h F : transient (extend_set h A)) = (F : transient A)";
-by (auto_tac (claset(),
- simpset() addsimps [transient_def, extend_set_subset_Compl_eq,
- Domain_extend_act]));
-qed "extend_transient";
-
-Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \
-\ (F : A ensures B)";
-by (simp_tac
- (simpset() addsimps [ensures_def, extend_constrains, extend_transient,
- extend_set_Un_distrib RS sym,
- extend_set_Diff_distrib RS sym]) 1);
-qed "extend_ensures";
-
-Goal "F : A leadsTo B \
-\ ==> extend h F : (extend_set h A) leadsTo (extend_set h B)";
-by (etac leadsTo_induct 1);
-by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
-by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
-by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, extend_ensures]) 1);
-qed "leadsTo_imp_extend_leadsTo";
-
-(*** Proving the converse takes some doing! ***)
-
-Goal "(x : slice C y) = (h(x,y) : C)";
-by (simp_tac (simpset() addsimps [slice_def]) 1);
-qed "slice_iff";
-
-AddIffs [slice_iff];
-
-Goal "slice (Union S) y = (UN x:S. slice x y)";
-by Auto_tac;
-qed "slice_Union";
-
-Goal "slice (extend_set h A) y = A";
-by Auto_tac;
-qed "slice_extend_set";
-
-Goal "project_set h A = (UN y. slice A y)";
-by Auto_tac;
-qed "project_set_is_UN_slice";
-
-Goalw [transient_def] "extend h F : transient A ==> F : transient (slice A y)";
-by Auto_tac;
-by (rtac bexI 1);
-by Auto_tac;
-by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1);
-qed "extend_transient_slice";
-
-(*Converse?*)
-Goal "extend h F : A co B ==> F : (slice A y) co (slice B y)";
-by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-qed "extend_constrains_slice";
-
-Goal "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)";
-by (auto_tac (claset(),
- simpset() addsimps [ensures_def, extend_constrains,
- extend_transient]));
-by (etac (extend_transient_slice RS transient_strengthen) 2);
-by (etac (extend_constrains_slice RS constrains_weaken) 1);
-by Auto_tac;
-qed "extend_ensures_slice";
-
-Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU";
-by (simp_tac (simpset() addsimps [project_set_is_UN_slice]) 1);
-by (blast_tac (claset() addIs [leadsTo_UN]) 1);
-qed "leadsTo_slice_project_set";
-
-Goal "extend h F : AU leadsTo BU \
-\ ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)";
-by (etac leadsTo_induct 1);
-by (asm_simp_tac (simpset() addsimps [leadsTo_UN, slice_Union]) 3);
-by (blast_tac (claset() addIs [leadsTo_slice_project_set, leadsTo_Trans]) 2);
-by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1);
-qed_spec_mp "extend_leadsTo_slice";
-
-Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \
-\ (F : A leadsTo B)";
-by Safe_tac;
-by (etac leadsTo_imp_extend_leadsTo 2);
-by (dtac extend_leadsTo_slice 1);
-by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
-qed "extend_leadsTo";
-
-Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \
-\ (F : A LeadsTo B)";
-by (simp_tac
- (simpset() addsimps [LeadsTo_def, reachable_extend_eq,
- extend_leadsTo, extend_set_Int_distrib RS sym]) 1);
-qed "extend_LeadsTo";
-
-
-(*** preserves ***)
-
-Goal "G : preserves (v o f) ==> project h C G : preserves v";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, project_stable_I,
- extend_set_eq_Collect]));
-qed "project_preserves_I";
-
-(*to preserve f is to preserve the whole original state*)
-Goal "G : preserves f ==> project h C G : preserves id";
-by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
-qed "project_preserves_id_I";
-
-Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, extend_stable RS sym,
- extend_set_eq_Collect]));
-qed "extend_preserves";
-
-Goal "inj h ==> (extend h G : preserves g)";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, extend_def, extend_act_def,
- stable_def, constrains_def, g_def]));
-qed "inj_extend_preserves";
-
-
-(*** Guarantees ***)
-
-Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
-by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_eq_UN, UN_Un]) 2);
-by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
-by Auto_tac;
-qed "project_extend_Join";
-
-Goal "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)";
-by (dres_inst_tac [("f", "project h UNIV")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
-qed "extend_Join_eq_extend_D";
-
-(** Strong precondition and postcondition; only useful when
- the old and new state sets are in bijection **)
-
-
-Goal "extend h F ok G ==> F ok project h UNIV G";
-by (auto_tac (claset(), simpset() addsimps [ok_def]));
-by (dtac subsetD 1);
-by (auto_tac (claset() addSIs [rev_image_eqI], simpset()));
-qed "ok_extend_imp_ok_project";
-
-Goal "(extend h F ok extend h G) = (F ok G)";
-by (asm_full_simp_tac (simpset() addsimps [ok_def]) 1);
-by Safe_tac;
-by (REPEAT (Force_tac 1));
-qed "ok_extend_iff";
-
-Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
-by Safe_tac;
-by (dres_inst_tac [("x","i")] bspec 1);
-by (dres_inst_tac [("x","j")] bspec 2);
-by (REPEAT (Force_tac 1));
-qed "OK_extend_iff";
-
-Goal "F : X guarantees Y ==> \
-\ extend h F : (extend h ` X) guarantees (extend h ` Y)";
-by (rtac guaranteesI 1);
-by (Clarify_tac 1);
-by (blast_tac (claset() addDs [ok_extend_imp_ok_project,
- extend_Join_eq_extend_D, guaranteesD]) 1);
-qed "guarantees_imp_extend_guarantees";
-
-Goal "extend h F : (extend h ` X) guarantees (extend h ` Y) \
-\ ==> F : X guarantees Y";
-by (auto_tac (claset(), simpset() addsimps [guar_def]));
-by (dres_inst_tac [("x", "extend h G")] spec 1);
-by (asm_full_simp_tac
- (simpset() delsimps [extend_Join]
- addsimps [extend_Join RS sym, ok_extend_iff,
- inj_extend RS inj_image_mem_iff]) 1);
-qed "extend_guarantees_imp_guarantees";
-
-Goal "(extend h F : (extend h ` X) guarantees (extend h ` Y)) = \
-\ (F : X guarantees Y)";
-by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
- extend_guarantees_imp_guarantees]) 1);
-qed "extend_guarantees_eq";
-
-
-Close_locale "Extend";
-
-(*Close_locale should do this!
-Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_Image];
-Delrules [make_elim h_inject1];
-*)
--- a/src/HOL/UNITY/Extend.thy Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/UNITY/Extend.thy Wed Jan 29 11:02:08 2003 +0100
@@ -8,7 +8,7 @@
function g (forgotten) maps the extended state to the "extending part"
*)
-Extend = Guar +
+theory Extend = Guar:
constdefs
@@ -46,17 +46,697 @@
project_act h ` Restrict C ` AllowedActs F})"
locale Extend =
- fixes
- f :: 'c => 'a
- g :: 'c => 'b
- h :: "'a*'b => 'c" (*isomorphism between 'a * 'b and 'c *)
- slice :: ['c set, 'b] => 'a set
+ 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. **)
+
+
+(*** 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)
+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 Int 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 Int Domain r"
+by blast
+
+lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A Int B)"
+by blast
+
+lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
+by (blast intro: sym [THEN image_eqI])
+
+(*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
+
+
+(*** 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
+
+
+
+(*** extend_set: basic properties ***)
+
+lemma project_set_iff [iff]:
+ "(x : project_set h C) = (EX y. h(x,y) : C)"
+by (simp add: project_set_def)
+
+lemma extend_set_mono: "A<=B ==> extend_set h A <= extend_set h B"
+by (unfold extend_set_def, blast)
+
+lemma (in Extend) 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 (in Extend) extend_set_strict_mono [iff]:
+ "(extend_set h A <= extend_set h B) = (A <= 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 <= 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
+
+(*** 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 : C ==> f z : project_set h C"
+by (auto simp add: split_extended_all)
+
+
+(*** More laws ***)
+
+(*Because A and B could differ on the "other" part of the state,
+ cannot generalize to
+ project_set h (A Int B) = project_set h A Int project_set h B
+*)
+lemma (in Extend) project_set_extend_set_Int:
+ "project_set h ((extend_set h A) Int B) = A Int (project_set h B)"
+by auto
+
+(*Unused, but interesting?*)
+lemma (in Extend) project_set_extend_set_Un:
+ "project_set h ((extend_set h A) Un B) = A Un (project_set h B)"
+by auto
+
+lemma project_set_Int_subset:
+ "project_set h (A Int B) <= (project_set h A) Int (project_set h B)"
+by auto
+
+lemma (in Extend) extend_set_Un_distrib:
+ "extend_set h (A Un B) = extend_set h A Un extend_set h B"
+by auto
+
+lemma (in Extend) extend_set_Int_distrib:
+ "extend_set h (A Int B) = extend_set h A Int extend_set h B"
+by auto
+
+lemma (in Extend) extend_set_INT_distrib:
+ "extend_set h (INTER A B) = (INT x: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) = (UN X:A. extend_set h X)"
+by blast
+
+lemma (in Extend) extend_set_subset_Compl_eq:
+ "(extend_set h A <= - extend_set h B) = (A <= - B)"
+by (unfold extend_set_def, auto)
+
+
+(*** 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 (in Extend) mem_extend_act_iff [iff]:
+ "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : 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') : extend_act h act ==> (f z, f z') : 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' <= extend_act h act ==> project_act h act' <= 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' <= 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') : act ==> (f z, f z') : 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
+
+
+
+(**** extend ****)
+
+(*** 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
+ : 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) = (UN X:A. project_set h X)"
+by blast
+
- assumes
- good_h "good_map h"
- defines
- f_def "f z == fst (inv h z)"
- g_def "g z == snd (inv h z)"
- slice_def "slice Z y == {x. h(x,y) : Z}"
+(*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) <=
+ 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
+ : 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 Join G) = extend h F Join 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) = (JN i: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 <= G ==> extend h F <= extend h G"
+by (force simp add: component_eq_subset)
+
+lemma (in Extend) project_mono: "F <= G ==> project h C F <= project h C G"
+by (simp add: component_eq_subset, blast)
+
+
+(*** Safety: co, stable ***)
+
+lemma (in Extend) extend_constrains:
+ "(extend h F : (extend_set h A) co (extend_set h B)) =
+ (F : A co B)"
+by (simp add: constrains_def)
+
+lemma (in Extend) extend_stable:
+ "(extend h F : stable (extend_set h A)) = (F : stable A)"
+by (simp add: stable_def extend_constrains)
+
+lemma (in Extend) extend_invariant:
+ "(extend h F : invariant (extend_set h A)) = (F : 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 : A co B ==> F : (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 : stable A ==> F : stable (project_set h A)"
+by (simp add: stable_def extend_constrains_project_set)
+
+
+(*** Weak safety primitives: Co, Stable ***)
+
+lemma (in Extend) reachable_extend_f:
+ "p : reachable (extend h F) ==> f p : 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) : reachable (extend h F) ==> s : 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 : (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 (in Extend) extend_Stable:
+ "(extend h F : Stable (extend_set h A)) = (F : Stable A)"
+by (simp add: Stable_def extend_Constrains)
+
+lemma (in Extend) extend_Always:
+ "(extend h F : Always (extend_set h A)) = (F : Always A)"
+by (simp (no_asm_simp) add: Always_def extend_Stable)
+
+
+(** Safety and "project" **)
+
+(** projection: monotonicity for safety **)
+
+lemma project_act_mono:
+ "D <= C ==>
+ project_act h (Restrict D act) <= project_act h (Restrict C act)"
+by (auto simp add: project_act_def)
+
+lemma (in Extend) project_constrains_mono:
+ "[| D <= C; project h C F : A co B |] ==> project h D F : A co B"
+apply (auto simp add: constrains_def)
+apply (drule project_act_mono, blast)
+done
+
+lemma (in Extend) project_stable_mono:
+ "[| D <= C; project h C F : stable A |] ==> project h D F : 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 : A co B) =
+ (F : (C Int 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 (in Extend) project_stable:
+ "(project h UNIV F : stable A) = (F : stable (extend_set h A))"
+apply (unfold stable_def)
+apply (simp (no_asm) add: project_constrains)
+done
+
+lemma (in Extend) 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 (in Extend) Int_extend_set_lemma:
+ "A Int extend_set h ((project_set h A) Int B) = A Int 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 : 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)"
+by (simp add: stable_def project_constrains_project_set)
+
+
+(*** Progress: transient, ensures ***)
+
+lemma (in Extend) 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 (in Extend) 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])
+
+lemma (in Extend) leadsTo_imp_extend_leadsTo:
+ "F : A leadsTo B
+ ==> extend h F : (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
+
+(*** Proving the converse takes some doing! ***)
+
+lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)"
+by (simp (no_asm) add: slice_def)
+
+lemma (in Extend) slice_Union: "slice (Union S) y = (UN x: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 = (UN y. slice A y)"
+by auto
+
+lemma (in Extend) extend_transient_slice:
+ "extend h F : transient A ==> F : transient (slice A y)"
+apply (unfold transient_def, auto)
+apply (rule bexI, auto)
+apply (force simp add: extend_act_def)
+done
+
+(*Converse?*)
+lemma (in Extend) extend_constrains_slice:
+ "extend h F : A co B ==> F : (slice A y) co (slice B y)"
+by (auto simp add: constrains_def)
+
+lemma (in Extend) 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
+
+lemma (in Extend) leadsTo_slice_project_set:
+ "ALL y. F : (slice B y) leadsTo CU ==> F : (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 (no_asm)]:
+ "extend h F : AU leadsTo BU
+ ==> ALL y. F : (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 : (extend_set h A) leadsTo (extend_set h B)) =
+ (F : 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 : (extend_set h A) LeadsTo (extend_set h B)) =
+ (F : A LeadsTo B)"
+by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
+ extend_set_Int_distrib [symmetric])
+
+
+(*** preserves ***)
+
+lemma (in Extend) 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 (in Extend) project_preserves_id_I:
+ "G : preserves f ==> project h C G : preserves id"
+by (simp add: project_preserves_I)
+
+lemma (in Extend) 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 (in Extend) 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)
+
+
+(*** Guarantees ***)
+
+lemma (in Extend) project_extend_Join:
+ "project h UNIV ((extend h F) Join G) = F Join (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) Join G = extend h H ==> H = F Join (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 : 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 (in Extend) extend_guarantees_imp_guarantees:
+ "extend h F : (extend h ` X) guarantees (extend h ` Y)
+ ==> F : 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 : (extend h ` X) guarantees (extend h ` Y)) =
+ (F : X guarantees Y)"
+by (blast intro: guarantees_imp_extend_guarantees
+ extend_guarantees_imp_guarantees)
end
--- a/src/HOL/UNITY/Lift_prog.thy Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Wed Jan 29 11:02:08 2003 +0100
@@ -348,13 +348,6 @@
apply (blast dest: insert_map_eq_diff)
done
-
-ML
-{*
-bind_thm ("export_mem_extend_act_iff", export mem_extend_act_iff)
-*}
-
-
lemma lift_transient_eq_disj:
"F : preserves snd
==> (lift i F : transient (lift_set j (A <*> UNIV))) =
@@ -362,8 +355,7 @@
apply (case_tac "i=j")
apply (auto simp add: lift_transient)
apply (auto simp add: lift_set_def lift_def transient_def rename_def extend_def Domain_extend_act)
-apply (drule subsetD, blast)
-apply auto
+apply (drule subsetD, blast, auto)
apply (rename_tac s f uu s' f' uu')
apply (subgoal_tac "f'=f & uu'=uu")
prefer 2 apply (force dest!: preserves_imp_eq, auto)
@@ -371,7 +363,8 @@
apply (drule subsetD)
apply (rule ImageI)
apply (erule bij_lift_map [THEN good_map_bij,
- THEN export_mem_extend_act_iff [THEN iffD2]], force)
+ THEN Extend.intro,
+ THEN Extend.mem_extend_act_iff [THEN iffD2]], force)
apply (erule lift_map_eq_diff [THEN exE], auto)
done
@@ -445,19 +438,12 @@
apply (auto simp add: preserves_def stable_def constrains_def)
done
-
-ML
-{*
-bind_thm ("export_Acts_extend", export Acts_extend);
-bind_thm ("export_AllowedActs_extend", export AllowedActs_extend)
-*}
-
lemma UNION_OK_lift_I:
"[| ALL i:I. F i : preserves snd;
ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]
==> OK I (%i. lift i (F i))"
-apply (auto simp add: OK_def lift_def rename_def export_Acts_extend)
-apply (simp (no_asm) add: export_AllowedActs_extend project_act_extend_act)
+apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
+apply (simp (no_asm) add: Extend.AllowedActs_extend project_act_extend_act)
apply (rename_tac "act")
apply (subgoal_tac
"{(x, x'). \<exists>s f u s' f' u'.
@@ -477,12 +463,11 @@
==> OK I (%i. lift i (F i))"
by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
-
lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
by (simp add: lift_def Allowed_rename)
-lemma lift_image_preserves: "lift i ` preserves v = preserves (v o drop_map i)"
-apply (simp (no_asm) add: rename_image_preserves lift_def inv_lift_map_eq)
-done
+lemma lift_image_preserves:
+ "lift i ` preserves v = preserves (v o drop_map i)"
+by (simp (no_asm) add: rename_image_preserves lift_def inv_lift_map_eq)
end
--- a/src/HOL/UNITY/Project.ML Tue Jan 28 22:53:39 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,718 +0,0 @@
-(* Title: HOL/UNITY/Project.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Projections of state sets (also of actions and programs)
-
-Inheritance of GUARANTEES properties under extension
-*)
-
-Open_locale "Extend";
-
-Goal "F : A co B ==> project h C (extend h F) : A co B";
-by (auto_tac (claset(),
- simpset() addsimps [extend_act_def, project_act_def, constrains_def]));
-qed "project_extend_constrains_I";
-
-
-(** Safety **)
-
-(*used below to prove Join_project_ensures*)
-Goal "[| G : stable C; project h C G : A unless B |] \
-\ ==> G : (C Int extend_set h A) unless (extend_set h B)";
-by (asm_full_simp_tac
- (simpset() addsimps [unless_def, project_constrains]) 1);
-by (blast_tac (claset() addDs [stable_constrains_Int]
- addIs [constrains_weaken]) 1);
-qed_spec_mp "project_unless";
-
-(*Generalizes project_constrains to the program F Join project h C G;
- useful with guarantees reasoning*)
-Goal "(F Join project h C G : A co B) = \
-\ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \
-\ F : A co B)";
-by (simp_tac (simpset() addsimps [project_constrains]) 1);
-by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
- addDs [constrains_imp_subset]) 1);
-qed "Join_project_constrains";
-
-(*The condition is required to prove the left-to-right direction;
- could weaken it to G : (C Int extend_set h A) co C*)
-Goalw [stable_def]
- "extend h F Join G : stable C \
-\ ==> (F Join project h C G : stable A) = \
-\ (extend h F Join G : stable (C Int extend_set h A) & \
-\ F : stable A)";
-by (simp_tac (HOL_ss addsimps [Join_project_constrains]) 1);
-by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
-qed "Join_project_stable";
-
-(*For using project_guarantees in particular cases*)
-Goal "extend h F Join G : extend_set h A co extend_set h B \
-\ ==> F Join project h C G : A co B";
-by (asm_full_simp_tac
- (simpset() addsimps [project_constrains, extend_constrains]) 1);
-by (blast_tac (claset() addIs [constrains_weaken]
- addDs [constrains_imp_subset]) 1);
-qed "project_constrains_I";
-
-Goalw [increasing_def, stable_def]
- "extend h F Join G : increasing (func o f) \
-\ ==> F Join project h C G : increasing func";
-by (asm_full_simp_tac (simpset_of SubstAx.thy
- addsimps [project_constrains_I, extend_set_eq_Collect]) 1);
-qed "project_increasing_I";
-
-Goal "(F Join project h UNIV G : increasing func) = \
-\ (extend h F Join G : increasing (func o f))";
-by (rtac iffI 1);
-by (etac project_increasing_I 2);
-by (asm_full_simp_tac (simpset_of SubstAx.thy
- addsimps [increasing_def, Join_project_stable]) 1);
-by (auto_tac (claset(),
- simpset() addsimps [extend_set_eq_Collect,
- extend_stable RS iffD1]));
-qed "Join_project_increasing";
-
-(*The UNIV argument is essential*)
-Goal "F Join project h UNIV G : A co B \
-\ ==> extend h F Join G : extend_set h A co extend_set h B";
-by (asm_full_simp_tac
- (simpset() addsimps [project_constrains, extend_constrains]) 1);
-qed "project_constrains_D";
-
-
-(*** "projecting" and union/intersection (no converses) ***)
-
-Goalw [projecting_def]
- "[| projecting C h F XA' XA; projecting C h F XB' XB |] \
-\ ==> projecting C h F (XA' Int XB') (XA Int XB)";
-by (Blast_tac 1);
-qed "projecting_Int";
-
-Goalw [projecting_def]
- "[| projecting C h F XA' XA; projecting C h F XB' XB |] \
-\ ==> projecting C h F (XA' Un XB') (XA Un XB)";
-by (Blast_tac 1);
-qed "projecting_Un";
-
-val [prem] = Goalw [projecting_def]
- "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
-\ ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)";
-by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
-qed "projecting_INT";
-
-val [prem] = Goalw [projecting_def]
- "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
-\ ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)";
-by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
-qed "projecting_UN";
-
-Goalw [projecting_def]
- "[| projecting C h F X' X; U'<=X'; X<=U |] ==> projecting C h F U' U";
-by Auto_tac;
-qed "projecting_weaken";
-
-Goalw [projecting_def]
- "[| projecting C h F X' X; U'<=X' |] ==> projecting C h F U' X";
-by Auto_tac;
-qed "projecting_weaken_L";
-
-Goalw [extending_def]
- "[| extending C h F YA' YA; extending C h F YB' YB |] \
-\ ==> extending C h F (YA' Int YB') (YA Int YB)";
-by (Blast_tac 1);
-qed "extending_Int";
-
-Goalw [extending_def]
- "[| extending C h F YA' YA; extending C h F YB' YB |] \
-\ ==> extending C h F (YA' Un YB') (YA Un YB)";
-by (Blast_tac 1);
-qed "extending_Un";
-
-val [prem] = Goalw [extending_def]
- "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
-\ ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)";
-by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
-qed "extending_INT";
-
-val [prem] = Goalw [extending_def]
- "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
-\ ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)";
-by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
-qed "extending_UN";
-
-Goalw [extending_def]
- "[| extending C h F Y' Y; Y'<=V'; V<=Y |] ==> extending C h F V' V";
-by Auto_tac;
-qed "extending_weaken";
-
-Goalw [extending_def]
- "[| extending C h F Y' Y; Y'<=V' |] ==> extending C h F V' Y";
-by Auto_tac;
-qed "extending_weaken_L";
-
-Goal "projecting C h F X' UNIV";
-by (simp_tac (simpset() addsimps [projecting_def]) 1);
-qed "projecting_UNIV";
-
-Goalw [projecting_def]
- "projecting C h F (extend_set h A co extend_set h B) (A co B)";
-by (blast_tac (claset() addIs [project_constrains_I]) 1);
-qed "projecting_constrains";
-
-Goalw [stable_def]
- "projecting C h F (stable (extend_set h A)) (stable A)";
-by (rtac projecting_constrains 1);
-qed "projecting_stable";
-
-Goalw [projecting_def]
- "projecting C h F (increasing (func o f)) (increasing func)";
-by (blast_tac (claset() addIs [project_increasing_I]) 1);
-qed "projecting_increasing";
-
-Goal "extending C h F UNIV Y";
-by (simp_tac (simpset() addsimps [extending_def]) 1);
-qed "extending_UNIV";
-
-Goalw [extending_def]
- "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
-by (blast_tac (claset() addIs [project_constrains_D]) 1);
-qed "extending_constrains";
-
-Goalw [stable_def]
- "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
-by (rtac extending_constrains 1);
-qed "extending_stable";
-
-Goalw [extending_def]
- "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)";
-by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
-qed "extending_increasing";
-
-
-(** Reachability and project **)
-
-(*In practice, C = reachable(...): the inclusion is equality*)
-Goal "[| reachable (extend h F Join G) <= C; \
-\ z : reachable (extend h F Join G) |] \
-\ ==> f z : reachable (F Join project h C G)";
-by (etac reachable.induct 1);
-by (force_tac (claset() addSIs [reachable.Init],
- simpset() addsimps [split_extended_all]) 1);
-by Auto_tac;
-by (force_tac (claset() delSWrapper "split_all_tac" addSbefore
- ("unsafe_split_all_tac", unsafe_split_all_tac)
- addIs [project_act_I RSN (3,reachable.Acts)], simpset()) 2);
-by (res_inst_tac [("act","x")] reachable.Acts 1);
-by Auto_tac;
-by (etac extend_act_D 1);
-qed "reachable_imp_reachable_project";
-
-Goalw [Constrains_def]
- "F Join project h (reachable (extend h F Join G)) G : A Co B \
-\ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
-by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains]) 1);
-by (Clarify_tac 1);
-by (etac constrains_weaken 1);
-by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
-qed "project_Constrains_D";
-
-Goalw [Stable_def]
- "F Join project h (reachable (extend h F Join G)) G : Stable A \
-\ ==> extend h F Join G : Stable (extend_set h A)";
-by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
-qed "project_Stable_D";
-
-Goalw [Always_def]
- "F Join project h (reachable (extend h F Join G)) G : Always A \
-\ ==> extend h F Join G : Always (extend_set h A)";
-by (force_tac (claset() addIs [reachable.Init],
- simpset() addsimps [project_Stable_D, split_extended_all]) 1);
-qed "project_Always_D";
-
-Goalw [Increasing_def]
- "F Join project h (reachable (extend h F Join G)) G : Increasing func \
-\ ==> extend h F Join G : Increasing (func o f)";
-by Auto_tac;
-by (stac (extend_set_eq_Collect RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1);
-qed "project_Increasing_D";
-
-
-(** Converse results for weak safety: benefits of the argument C *)
-
-(*In practice, C = reachable(...): the inclusion is equality*)
-Goal "[| C <= reachable(extend h F Join G); \
-\ x : reachable (F Join project h C G) |] \
-\ ==> EX y. h(x,y) : reachable (extend h F Join G)";
-by (etac reachable.induct 1);
-by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
-by (auto_tac (claset(), simpset()addsimps [project_act_def]));
-by (ALLGOALS (force_tac (claset() delrules [Id_in_Acts]
- addIs [reachable.Acts, extend_act_D], simpset())));
-qed "reachable_project_imp_reachable";
-
-Goal "project_set h (reachable (extend h F Join G)) = \
-\ reachable (F Join project h (reachable (extend h F Join G)) G)";
-by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
- subset_refl RS reachable_project_imp_reachable],
- simpset()));
-qed "project_set_reachable_extend_eq";
-
-(*UNUSED*)
-Goal "reachable (extend h F Join G) <= C \
-\ ==> reachable (extend h F Join G) <= \
-\ extend_set h (reachable (F Join project h C G))";
-by (auto_tac (claset() addDs [reachable_imp_reachable_project],
- simpset()));
-qed "reachable_extend_Join_subset";
-
-Goalw [Constrains_def]
- "extend h F Join G : (extend_set h A) Co (extend_set h B) \
-\ ==> F Join project h (reachable (extend h F Join G)) G : A Co B";
-by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains,
- extend_set_Int_distrib]) 1);
-by (rtac conjI 1);
-by (force_tac
- (claset() addEs [constrains_weaken_L]
- addSDs [extend_constrains_project_set,
- subset_refl RS reachable_project_imp_reachable],
- simpset()) 2);
-by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
-qed "project_Constrains_I";
-
-Goalw [Stable_def]
- "extend h F Join G : Stable (extend_set h A) \
-\ ==> F Join project h (reachable (extend h F Join G)) G : Stable A";
-by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
-qed "project_Stable_I";
-
-Goalw [Always_def]
- "extend h F Join G : Always (extend_set h A) \
-\ ==> F Join project h (reachable (extend h F Join G)) G : Always A";
-by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
-by (rewtac extend_set_def);
-by (Blast_tac 1);
-qed "project_Always_I";
-
-Goalw [Increasing_def]
- "extend h F Join G : Increasing (func o f) \
-\ ==> F Join project h (reachable (extend h F Join G)) G : Increasing func";
-by Auto_tac;
-by (asm_simp_tac (simpset() addsimps [extend_set_eq_Collect,
- project_Stable_I]) 1);
-qed "project_Increasing_I";
-
-Goal "(F Join project h (reachable (extend h F Join G)) G : A Co B) = \
-\ (extend h F Join G : (extend_set h A) Co (extend_set h B))";
-by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
-qed "project_Constrains";
-
-Goalw [Stable_def]
- "(F Join project h (reachable (extend h F Join G)) G : Stable A) = \
-\ (extend h F Join G : Stable (extend_set h A))";
-by (rtac project_Constrains 1);
-qed "project_Stable";
-
-Goal
- "(F Join project h (reachable (extend h F Join G)) G : Increasing func) = \
-\ (extend h F Join G : Increasing (func o f))";
-by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
- extend_set_eq_Collect]) 1);
-qed "project_Increasing";
-
-(** A lot of redundant theorems: all are proved to facilitate reasoning
- about guarantees. **)
-
-Goalw [projecting_def]
- "projecting (%G. reachable (extend h F Join G)) h F \
-\ (extend_set h A Co extend_set h B) (A Co B)";
-by (blast_tac (claset() addIs [project_Constrains_I]) 1);
-qed "projecting_Constrains";
-
-Goalw [Stable_def]
- "projecting (%G. reachable (extend h F Join G)) h F \
-\ (Stable (extend_set h A)) (Stable A)";
-by (rtac projecting_Constrains 1);
-qed "projecting_Stable";
-
-Goalw [projecting_def]
- "projecting (%G. reachable (extend h F Join G)) h F \
-\ (Always (extend_set h A)) (Always A)";
-by (blast_tac (claset() addIs [project_Always_I]) 1);
-qed "projecting_Always";
-
-Goalw [projecting_def]
- "projecting (%G. reachable (extend h F Join G)) h F \
-\ (Increasing (func o f)) (Increasing func)";
-by (blast_tac (claset() addIs [project_Increasing_I]) 1);
-qed "projecting_Increasing";
-
-Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F \
-\ (extend_set h A Co extend_set h B) (A Co B)";
-by (blast_tac (claset() addIs [project_Constrains_D]) 1);
-qed "extending_Constrains";
-
-Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F \
-\ (Stable (extend_set h A)) (Stable A)";
-by (blast_tac (claset() addIs [project_Stable_D]) 1);
-qed "extending_Stable";
-
-Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F \
-\ (Always (extend_set h A)) (Always A)";
-by (blast_tac (claset() addIs [project_Always_D]) 1);
-qed "extending_Always";
-
-Goalw [extending_def]
- "extending (%G. reachable (extend h F Join G)) h F \
-\ (Increasing (func o f)) (Increasing func)";
-by (blast_tac (claset() addIs [project_Increasing_D]) 1);
-qed "extending_Increasing";
-
-
-(*** leadsETo in the precondition (??) ***)
-
-(** transient **)
-
-Goalw [transient_def]
- "[| G : transient (C Int extend_set h A); G : stable C |] \
-\ ==> project h C G : transient (project_set h C Int A)";
-by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
-by (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A" 1);
-by (asm_full_simp_tac
- (simpset() addsimps [stable_def, constrains_def]) 2);
-by (Blast_tac 2);
-(*back to main goal*)
-by (thin_tac "?AA <= -C Un ?BB" 1);
-by (ball_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [extend_set_def, project_act_def]) 1);
-by (Blast_tac 1);
-qed "transient_extend_set_imp_project_transient";
-
-(*converse might hold too?*)
-Goalw [transient_def]
- "project h C (extend h F) : transient (project_set h C Int D) \
-\ ==> F : transient (project_set h C Int D)";
-by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
-by (rtac bexI 1);
-by (assume_tac 2);
-by Auto_tac;
-by (rewtac extend_act_def);
-by (Blast_tac 1);
-qed "project_extend_transient_D";
-
-
-(** ensures -- a primitive combining progress with safety **)
-
-(*Used to prove project_leadsETo_I*)
-Goal "[| extend h F : stable C; G : stable C; \
-\ extend h F Join G : A ensures B; A-B = C Int extend_set h D |] \
-\ ==> F Join project h C G \
-\ : (project_set h C Int project_set h A) ensures (project_set h B)";
-by (asm_full_simp_tac
- (simpset() addsimps [ensures_def, project_constrains,
- Join_transient, extend_transient]) 1);
-by (Clarify_tac 1);
-by (REPEAT_FIRST (rtac conjI));
-(*first subgoal*)
-by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS
- constrains_Int RS constrains_weaken]
- addSDs [extend_constrains_project_set]
- addSDs [equalityD1]) 1);
-(*2nd subgoal*)
-by (etac (stableD RS constrains_Int RS constrains_weaken) 1);
-by (assume_tac 1);
-by (Blast_tac 3);
-by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib,
- extend_set_Un_distrib]) 2);
-by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2);
-by (full_simp_tac (simpset() addsimps [extend_set_def]) 1);
-by (Blast_tac 1);
-(*The transient part*)
-by Auto_tac;
-by (force_tac (claset() addSDs [equalityD1]
- addIs [transient_extend_set_imp_project_transient RS
- transient_strengthen],
- simpset()) 2);
-by (full_simp_tac (simpset() addsimps [Int_Diff]) 1);
-by (force_tac (claset() addSDs [equalityD1]
- addIs [transient_extend_set_imp_project_transient RS
- project_extend_transient_D RS transient_strengthen],
- simpset()) 1);
-qed "ensures_extend_set_imp_project_ensures";
-
-(*Used to prove project_leadsETo_D*)
-Goal "[| project h C G ~: transient (A-B) | A<=B; \
-\ extend h F Join G : stable C; \
-\ F Join project h C G : A ensures B |] \
-\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
-by (etac disjE 1);
-by (blast_tac (claset() addIs [subset_imp_ensures]) 2);
-by (auto_tac (claset() addDs [extend_transient RS iffD2]
- addIs [transient_strengthen, project_set_I,
- project_unless RS unlessD, unlessI,
- project_extend_constrains_I],
- simpset() addsimps [ensures_def, Join_transient]));
-qed_spec_mp "Join_project_ensures";
-
-(** Lemma useful for both STRONG and WEAK progress, but the transient
- condition's very strong **)
-
-(*The strange induction formula allows induction over the leadsTo
- assumption's non-atomic precondition*)
-Goal "[| ALL D. project h C G : transient D --> D={}; \
-\ extend h F Join G : stable C; \
-\ F Join project h C G : (project_set h C Int A) leadsTo B |] \
-\ ==> extend h F Join G : \
-\ C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
-by (etac leadsTo_induct 1);
-by (asm_simp_tac (simpset() delsimps UN_simps
- addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
-by (blast_tac (claset() addIs [psp_stable2 RS leadsTo_weaken_L,
- leadsTo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
-val lemma = result();
-
-Goal "[| ALL D. project h C G : transient D --> D={}; \
-\ extend h F Join G : stable C; \
-\ F Join project h C G : (project_set h C Int A) leadsTo B |] \
-\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
-by (rtac (lemma RS leadsTo_weaken) 1);
-by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
-qed "project_leadsTo_D_lemma";
-
-Goal "[| C = (reachable (extend h F Join G)); \
-\ ALL D. project h C G : transient D --> D={}; \
-\ F Join project h C G : A LeadsTo B |] \
-\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
-by (asm_full_simp_tac
- (simpset_of SubstAx.thy addsimps [LeadsTo_def, project_leadsTo_D_lemma,
- project_set_reachable_extend_eq]) 1);
-qed "Join_project_LeadsTo";
-
-
-(*** Towards project_Ensures_D ***)
-
-
-Goalw [project_set_def, extend_set_def, project_act_def]
- "act `` (C Int extend_set h A) <= B \
-\ ==> project_act h (Restrict C act) `` (project_set h C Int A) \
-\ <= project_set h B";
-by (Blast_tac 1);
-qed "act_subset_imp_project_act_subset";
-
-(*This trivial proof is the complementation part of transferring a transient
- property upwards. The hard part would be to
- show that G's action has a big enough domain.*)
-Goal "[| act: Acts G; \
-\ (project_act h (Restrict C act))`` \
-\ (project_set h C Int A - B) <= -(project_set h C Int A - B) |] \
-\ ==> act``(C Int extend_set h A - extend_set h B) \
-\ <= -(C Int extend_set h A - extend_set h B)";
-by (auto_tac (claset(),
- simpset() addsimps [project_set_def, extend_set_def, project_act_def]));
-result();
-
-Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B)); \
-\ project h C G : transient (project_set h C Int A - B) |] \
-\ ==> (C Int extend_set h A) - extend_set h B = {}";
-by (auto_tac (claset(),
- simpset() addsimps [transient_def, subset_Compl_self_eq,
- Domain_project_act, split_extended_all]));
-by (Blast_tac 1);
-by (auto_tac (claset(),
- simpset() addsimps [stable_def, constrains_def]));
-by (ball_tac 1);
-by (auto_tac (claset(),
- simpset() addsimps [Int_Diff,
- extend_set_Diff_distrib RS sym]));
-by (dtac act_subset_imp_project_act_subset 1);
-by (subgoal_tac
- "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}" 1);
-by (REPEAT (thin_tac "?r``?A <= ?B" 1));
-by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]);
-by (Blast_tac 2);
-by (rtac ccontr 1);
-by (dtac subsetD 1);
-by (Blast_tac 1);
-by (force_tac (claset(), simpset() addsimps [split_extended_all]) 1);
-qed "stable_project_transient";
-
-Goal "[| G : stable C; project h C G : (project_set h C Int A) unless B |] \
-\ ==> G : (C Int extend_set h A) unless (extend_set h B)";
-by (auto_tac
- (claset() addDs [stable_constrains_Int]
- addIs [constrains_weaken],
- simpset() addsimps [unless_def, project_constrains, Diff_eq,
- Int_assoc, Int_extend_set_lemma]));
-qed_spec_mp "project_unless2";
-
-Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B)); \
-\ F Join project h C G : (project_set h C Int A) ensures B; \
-\ extend h F Join G : stable C |] \
-\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
-(*unless*)
-by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2]
- addIs [project_extend_constrains_I],
- simpset() addsimps [ensures_def]));
-(*transient*)
-(*A G-action cannot occur*)
-by (force_tac (claset() addDs [stable_project_transient],
- simpset() delsimps [Diff_eq_empty_iff]
- addsimps [Diff_eq_empty_iff RS sym]) 2);
-(*An F-action*)
-by (force_tac (claset() addSEs [extend_transient RS iffD2 RS
- transient_strengthen],
- simpset() addsimps [split_extended_all]) 1);
-qed "project_ensures_D_lemma";
-
-Goal "[| F Join project h UNIV G : A ensures B; \
-\ G : stable (extend_set h A - extend_set h B) |] \
-\ ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
-by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
-by (stac stable_UNIV 3);
-by Auto_tac;
-qed "project_ensures_D";
-
-Goalw [Ensures_def]
- "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B; \
-\ G : stable (reachable (extend h F Join G) Int extend_set h A - \
-\ extend_set h B) |] \
-\ ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)";
-by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
-by (auto_tac (claset(),
- simpset() addsimps [project_set_reachable_extend_eq RS sym]));
-qed "project_Ensures_D";
-
-
-(*** Guarantees ***)
-
-Goal "project_act h (Restrict C act) <= project_act h act";
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));
-qed "project_act_Restrict_subset_project_act";
-
-
-Goal "[| extend h F ok G; subset_closed (AllowedActs F) |] \
-\ ==> F ok project h C G";
-by (auto_tac (claset(), simpset() addsimps [ok_def]));
-by (dtac subsetD 1);
-by (Blast_tac 1);
-by (force_tac (claset() delSWrapper "split_all_tac" addSbefore
- ("unsafe_split_all_tac", unsafe_split_all_tac)
- addSIs [rev_image_eqI], simpset()) 1);
-by (cut_facts_tac [project_act_Restrict_subset_project_act] 1);
-by (auto_tac (claset(), simpset() addsimps [subset_closed_def]));
-qed "subset_closed_ok_extend_imp_ok_project";
-
-
-(*Weak precondition and postcondition
- Not clear that it has a converse [or that we want one!]*)
-
-(*The raw version; 3rd premise could be weakened by adding the
- precondition extend h F Join G : X' *)
-val [xguary,closed,project,extend] =
-Goal "[| F : X guarantees Y; subset_closed (AllowedActs F); \
-\ !!G. extend h F Join G : X' ==> F Join project h (C G) G : X; \
-\ !!G. [| F Join project h (C G) G : Y |] \
-\ ==> extend h F Join G : Y' |] \
-\ ==> extend h F : X' guarantees Y'";
-by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
-by (blast_tac (claset() addIs [closed,
- subset_closed_ok_extend_imp_ok_project]) 1);
-by (etac project 1);
-qed "project_guarantees_raw";
-
-Goal "[| F : X guarantees Y; subset_closed (AllowedActs F); \
-\ projecting C h F X' X; extending C h F Y' Y |] \
-\ ==> extend h F : X' guarantees Y'";
-by (rtac guaranteesI 1);
-by (auto_tac (claset(),
- simpset() addsimps [guaranteesD, projecting_def,
- extending_def, subset_closed_ok_extend_imp_ok_project]));
-qed "project_guarantees";
-
-
-(*It seems that neither "guarantees" law can be proved from the other.*)
-
-
-(*** guarantees corollaries ***)
-
-(** Some could be deleted: the required versions are easy to prove **)
-
-Goal "[| F : UNIV guarantees increasing func; \
-\ subset_closed (AllowedActs F) |] \
-\ ==> extend h F : X' guarantees increasing (func o f)";
-by (etac project_guarantees 1);
-by (rtac extending_increasing 3);
-by (rtac projecting_UNIV 2);
-by Auto_tac;
-qed "extend_guar_increasing";
-
-Goal "[| F : UNIV guarantees Increasing func; \
-\ subset_closed (AllowedActs F) |] \
-\ ==> extend h F : X' guarantees Increasing (func o f)";
-by (etac project_guarantees 1);
-by (rtac extending_Increasing 3);
-by (rtac projecting_UNIV 2);
-by Auto_tac;
-qed "extend_guar_Increasing";
-
-Goal "[| F : Always A guarantees Always B; \
-\ subset_closed (AllowedActs F) |] \
-\ ==> extend h F \
-\ : Always(extend_set h A) guarantees Always(extend_set h B)";
-by (etac project_guarantees 1);
-by (rtac extending_Always 3);
-by (rtac projecting_Always 2);
-by Auto_tac;
-qed "extend_guar_Always";
-
-Goal "[| G : preserves f; project h C G : transient D |] ==> D={}";
-by (rtac stable_transient_empty 1);
-by (assume_tac 2);
-by (blast_tac (claset() addIs [project_preserves_id_I,
- impOfSubs preserves_id_subset_stable]) 1);
-qed "preserves_project_transient_empty";
-
-
-(** Guarantees with a leadsTo postcondition
- THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
-
-Goal "[| F Join project h UNIV G : A leadsTo B; \
-\ G : preserves f |] \
-\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (res_inst_tac [("C1", "UNIV")]
- (project_leadsTo_D_lemma RS leadsTo_weaken) 1);
-by (auto_tac (claset() addDs [preserves_project_transient_empty],
- simpset()));
-qed "project_leadsTo_D";
-
-Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
-\ G : preserves f |] \
-\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
-by (rtac (refl RS Join_project_LeadsTo) 1);
-by (auto_tac (claset() addDs [preserves_project_transient_empty],
- simpset()));
-qed "project_LeadsTo_D";
-
-Goalw [extending_def]
- "(ALL G. extend h F ok G --> G : preserves f) \
-\ ==> extending (%G. UNIV) h F \
-\ (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
-by (blast_tac (claset() addIs [project_leadsTo_D]) 1);
-qed "extending_leadsTo";
-
-Goalw [extending_def]
- "(ALL G. extend h F ok G --> G : preserves f) \
-\ ==> extending (%G. reachable (extend h F Join G)) h F \
-\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
-by (blast_tac (claset() addIs [project_LeadsTo_D]) 1);
-qed "extending_LeadsTo";
-
-Close_locale "Extend";
--- a/src/HOL/UNITY/Project.thy Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/UNITY/Project.thy Wed Jan 29 11:02:08 2003 +0100
@@ -8,7 +8,7 @@
Inheritance of GUARANTEES properties under extension
*)
-Project = Extend +
+theory Project = Extend:
constdefs
projecting :: "['c program => 'c set, 'a*'b => 'c,
@@ -25,4 +25,713 @@
subset_closed :: "'a set set => bool"
"subset_closed U == ALL A: U. Pow A <= U"
+
+lemma (in Extend) project_extend_constrains_I:
+ "F : A co B ==> project h C (extend h F) : A co B"
+apply (auto simp add: extend_act_def project_act_def constrains_def)
+done
+
+
+(** Safety **)
+
+(*used below to prove Join_project_ensures*)
+lemma (in Extend) project_unless [rule_format (no_asm)]:
+ "[| G : stable C; project h C G : A unless B |]
+ ==> G : (C Int extend_set h A) unless (extend_set h B)"
+apply (simp add: unless_def project_constrains)
+apply (blast dest: stable_constrains_Int intro: constrains_weaken)
+done
+
+(*Generalizes project_constrains to the program F Join project h C G
+ useful with guarantees reasoning*)
+lemma (in Extend) Join_project_constrains:
+ "(F Join project h C G : A co B) =
+ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &
+ F : A co B)"
+apply (simp (no_asm) add: project_constrains)
+apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken]
+ dest: constrains_imp_subset)
+done
+
+(*The condition is required to prove the left-to-right direction
+ could weaken it to G : (C Int extend_set h A) co C*)
+lemma (in Extend) Join_project_stable:
+ "extend h F Join G : stable C
+ ==> (F Join project h C G : stable A) =
+ (extend h F Join G : stable (C Int extend_set h A) &
+ F : stable A)"
+apply (unfold stable_def)
+apply (simp only: Join_project_constrains)
+apply (blast intro: constrains_weaken dest: constrains_Int)
+done
+
+(*For using project_guarantees in particular cases*)
+lemma (in Extend) project_constrains_I:
+ "extend h F Join G : extend_set h A co extend_set h B
+ ==> F Join project h C G : A co B"
+apply (simp add: project_constrains extend_constrains)
+apply (blast intro: constrains_weaken dest: constrains_imp_subset)
+done
+
+lemma (in Extend) project_increasing_I:
+ "extend h F Join G : increasing (func o f)
+ ==> F Join project h C G : increasing func"
+apply (unfold increasing_def stable_def)
+apply (simp del: Join_constrains
+ add: project_constrains_I extend_set_eq_Collect)
+done
+
+lemma (in Extend) Join_project_increasing:
+ "(F Join project h UNIV G : increasing func) =
+ (extend h F Join G : increasing (func o f))"
+apply (rule iffI)
+apply (erule_tac [2] project_increasing_I)
+apply (simp del: Join_stable
+ add: increasing_def Join_project_stable)
+apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1])
+done
+
+(*The UNIV argument is essential*)
+lemma (in Extend) project_constrains_D:
+ "F Join project h UNIV G : A co B
+ ==> extend h F Join G : extend_set h A co extend_set h B"
+by (simp add: project_constrains extend_constrains)
+
+
+(*** "projecting" and union/intersection (no converses) ***)
+
+lemma projecting_Int:
+ "[| projecting C h F XA' XA; projecting C h F XB' XB |]
+ ==> projecting C h F (XA' Int XB') (XA Int XB)"
+by (unfold projecting_def, blast)
+
+lemma projecting_Un:
+ "[| projecting C h F XA' XA; projecting C h F XB' XB |]
+ ==> projecting C h F (XA' Un XB') (XA Un XB)"
+by (unfold projecting_def, blast)
+
+lemma projecting_INT:
+ "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]
+ ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"
+by (unfold projecting_def, blast)
+
+lemma projecting_UN:
+ "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]
+ ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"
+by (unfold projecting_def, blast)
+
+lemma projecting_weaken:
+ "[| projecting C h F X' X; U'<=X'; X<=U |] ==> projecting C h F U' U"
+by (unfold projecting_def, auto)
+
+lemma projecting_weaken_L:
+ "[| projecting C h F X' X; U'<=X' |] ==> projecting C h F U' X"
+by (unfold projecting_def, auto)
+
+lemma extending_Int:
+ "[| extending C h F YA' YA; extending C h F YB' YB |]
+ ==> extending C h F (YA' Int YB') (YA Int YB)"
+by (unfold extending_def, blast)
+
+lemma extending_Un:
+ "[| extending C h F YA' YA; extending C h F YB' YB |]
+ ==> extending C h F (YA' Un YB') (YA Un YB)"
+by (unfold extending_def, blast)
+
+lemma extending_INT:
+ "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]
+ ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)"
+by (unfold extending_def, blast)
+
+lemma extending_UN:
+ "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]
+ ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)"
+by (unfold extending_def, blast)
+
+lemma extending_weaken:
+ "[| extending C h F Y' Y; Y'<=V'; V<=Y |] ==> extending C h F V' V"
+by (unfold extending_def, auto)
+
+lemma extending_weaken_L:
+ "[| extending C h F Y' Y; Y'<=V' |] ==> extending C h F V' Y"
+by (unfold extending_def, auto)
+
+lemma projecting_UNIV: "projecting C h F X' UNIV"
+by (simp add: projecting_def)
+
+lemma (in Extend) projecting_constrains:
+ "projecting C h F (extend_set h A co extend_set h B) (A co B)"
+apply (unfold projecting_def)
+apply (blast intro: project_constrains_I)
+done
+
+lemma (in Extend) projecting_stable:
+ "projecting C h F (stable (extend_set h A)) (stable A)"
+apply (unfold stable_def)
+apply (rule projecting_constrains)
+done
+
+lemma (in Extend) projecting_increasing:
+ "projecting C h F (increasing (func o f)) (increasing func)"
+apply (unfold projecting_def)
+apply (blast intro: project_increasing_I)
+done
+
+lemma (in Extend) extending_UNIV: "extending C h F UNIV Y"
+apply (simp (no_asm) add: extending_def)
+done
+
+lemma (in Extend) extending_constrains:
+ "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)"
+apply (unfold extending_def)
+apply (blast intro: project_constrains_D)
+done
+
+lemma (in Extend) extending_stable:
+ "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)"
+apply (unfold stable_def)
+apply (rule extending_constrains)
+done
+
+lemma (in Extend) extending_increasing:
+ "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)"
+by (force simp only: extending_def Join_project_increasing)
+
+
+(** Reachability and project **)
+
+(*In practice, C = reachable(...): the inclusion is equality*)
+lemma (in Extend) reachable_imp_reachable_project:
+ "[| reachable (extend h F Join G) <= C;
+ z : reachable (extend h F Join G) |]
+ ==> f z : reachable (F Join project h C G)"
+apply (erule reachable.induct)
+apply (force intro!: reachable.Init simp add: split_extended_all, auto)
+ apply (rule_tac act = x in reachable.Acts)
+ apply auto
+ apply (erule extend_act_D)
+apply (rule_tac act1 = "Restrict C act"
+ in project_act_I [THEN [3] reachable.Acts], auto)
+done
+
+lemma (in Extend) project_Constrains_D:
+ "F Join project h (reachable (extend h F Join G)) G : A Co B
+ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"
+apply (unfold Constrains_def)
+apply (simp del: Join_constrains
+ add: Join_project_constrains, clarify)
+apply (erule constrains_weaken)
+apply (auto intro: reachable_imp_reachable_project)
+done
+
+lemma (in Extend) project_Stable_D:
+ "F Join project h (reachable (extend h F Join G)) G : Stable A
+ ==> extend h F Join G : Stable (extend_set h A)"
+apply (unfold Stable_def)
+apply (simp (no_asm_simp) add: project_Constrains_D)
+done
+
+lemma (in Extend) project_Always_D:
+ "F Join project h (reachable (extend h F Join G)) G : Always A
+ ==> extend h F Join G : Always (extend_set h A)"
+apply (unfold Always_def)
+apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
+done
+
+lemma (in Extend) project_Increasing_D:
+ "F Join project h (reachable (extend h F Join G)) G : Increasing func
+ ==> extend h F Join G : Increasing (func o f)"
+apply (unfold Increasing_def, auto)
+apply (subst extend_set_eq_Collect [symmetric])
+apply (simp (no_asm_simp) add: project_Stable_D)
+done
+
+
+(** Converse results for weak safety: benefits of the argument C *)
+
+(*In practice, C = reachable(...): the inclusion is equality*)
+lemma (in Extend) reachable_project_imp_reachable:
+ "[| C <= reachable(extend h F Join G);
+ x : reachable (F Join project h C G) |]
+ ==> EX y. h(x,y) : reachable (extend h F Join G)"
+apply (erule reachable.induct)
+apply (force intro: reachable.Init)
+apply (auto simp add: project_act_def)
+apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+
+done
+
+lemma (in Extend) project_set_reachable_extend_eq:
+ "project_set h (reachable (extend h F Join G)) =
+ reachable (F Join project h (reachable (extend h F Join G)) G)"
+by (auto dest: subset_refl [THEN reachable_imp_reachable_project]
+ subset_refl [THEN reachable_project_imp_reachable])
+
+(*UNUSED*)
+lemma (in Extend) reachable_extend_Join_subset:
+ "reachable (extend h F Join G) <= C
+ ==> reachable (extend h F Join G) <=
+ extend_set h (reachable (F Join project h C G))"
+apply (auto dest: reachable_imp_reachable_project)
+done
+
+lemma (in Extend) project_Constrains_I:
+ "extend h F Join G : (extend_set h A) Co (extend_set h B)
+ ==> F Join project h (reachable (extend h F Join G)) G : A Co B"
+apply (unfold Constrains_def)
+apply (simp del: Join_constrains
+ add: Join_project_constrains extend_set_Int_distrib)
+apply (rule conjI)
+ prefer 2
+ apply (force elim: constrains_weaken_L
+ dest!: extend_constrains_project_set
+ subset_refl [THEN reachable_project_imp_reachable])
+apply (blast intro: constrains_weaken_L)
+done
+
+lemma (in Extend) project_Stable_I:
+ "extend h F Join G : Stable (extend_set h A)
+ ==> F Join project h (reachable (extend h F Join G)) G : Stable A"
+apply (unfold Stable_def)
+apply (simp (no_asm_simp) add: project_Constrains_I)
+done
+
+lemma (in Extend) project_Always_I:
+ "extend h F Join G : Always (extend_set h A)
+ ==> F Join project h (reachable (extend h F Join G)) G : Always A"
+apply (unfold Always_def)
+apply (auto simp add: project_Stable_I)
+apply (unfold extend_set_def, blast)
+done
+
+lemma (in Extend) project_Increasing_I:
+ "extend h F Join G : Increasing (func o f)
+ ==> F Join project h (reachable (extend h F Join G)) G : Increasing func"
+apply (unfold Increasing_def, auto)
+apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
+done
+
+lemma (in Extend) project_Constrains:
+ "(F Join project h (reachable (extend h F Join G)) G : A Co B) =
+ (extend h F Join G : (extend_set h A) Co (extend_set h B))"
+apply (blast intro: project_Constrains_I project_Constrains_D)
+done
+
+lemma (in Extend) project_Stable:
+ "(F Join project h (reachable (extend h F Join G)) G : Stable A) =
+ (extend h F Join G : Stable (extend_set h A))"
+apply (unfold Stable_def)
+apply (rule project_Constrains)
+done
+
+lemma (in Extend) project_Increasing:
+ "(F Join project h (reachable (extend h F Join G)) G : Increasing func) =
+ (extend h F Join G : Increasing (func o f))"
+apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
+done
+
+(** A lot of redundant theorems: all are proved to facilitate reasoning
+ about guarantees. **)
+
+lemma (in Extend) projecting_Constrains:
+ "projecting (%G. reachable (extend h F Join G)) h F
+ (extend_set h A Co extend_set h B) (A Co B)"
+
+apply (unfold projecting_def)
+apply (blast intro: project_Constrains_I)
+done
+
+lemma (in Extend) projecting_Stable:
+ "projecting (%G. reachable (extend h F Join G)) h F
+ (Stable (extend_set h A)) (Stable A)"
+apply (unfold Stable_def)
+apply (rule projecting_Constrains)
+done
+
+lemma (in Extend) projecting_Always:
+ "projecting (%G. reachable (extend h F Join G)) h F
+ (Always (extend_set h A)) (Always A)"
+apply (unfold projecting_def)
+apply (blast intro: project_Always_I)
+done
+
+lemma (in Extend) projecting_Increasing:
+ "projecting (%G. reachable (extend h F Join G)) h F
+ (Increasing (func o f)) (Increasing func)"
+apply (unfold projecting_def)
+apply (blast intro: project_Increasing_I)
+done
+
+lemma (in Extend) extending_Constrains:
+ "extending (%G. reachable (extend h F Join G)) h F
+ (extend_set h A Co extend_set h B) (A Co B)"
+apply (unfold extending_def)
+apply (blast intro: project_Constrains_D)
+done
+
+lemma (in Extend) extending_Stable:
+ "extending (%G. reachable (extend h F Join G)) h F
+ (Stable (extend_set h A)) (Stable A)"
+apply (unfold extending_def)
+apply (blast intro: project_Stable_D)
+done
+
+lemma (in Extend) extending_Always:
+ "extending (%G. reachable (extend h F Join G)) h F
+ (Always (extend_set h A)) (Always A)"
+apply (unfold extending_def)
+apply (blast intro: project_Always_D)
+done
+
+lemma (in Extend) extending_Increasing:
+ "extending (%G. reachable (extend h F Join G)) h F
+ (Increasing (func o f)) (Increasing func)"
+apply (unfold extending_def)
+apply (blast intro: project_Increasing_D)
+done
+
+
+(*** leadsETo in the precondition (??) ***)
+
+(** transient **)
+
+lemma (in Extend) transient_extend_set_imp_project_transient:
+ "[| G : transient (C Int extend_set h A); G : stable C |]
+ ==> project h C G : transient (project_set h C Int A)"
+
+apply (unfold transient_def)
+apply (auto simp add: Domain_project_act)
+apply (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A")
+prefer 2
+ apply (simp add: stable_def constrains_def, blast)
+(*back to main goal*)
+apply (erule_tac V = "?AA <= -C Un ?BB" in thin_rl)
+apply (drule bspec, assumption)
+apply (simp add: extend_set_def project_act_def, blast)
+done
+
+(*converse might hold too?*)
+lemma (in Extend) project_extend_transient_D:
+ "project h C (extend h F) : transient (project_set h C Int D)
+ ==> F : transient (project_set h C Int D)"
+apply (unfold transient_def)
+apply (auto simp add: Domain_project_act)
+apply (rule bexI)
+prefer 2 apply assumption
+apply auto
+apply (unfold extend_act_def, blast)
+done
+
+
+(** ensures -- a primitive combining progress with safety **)
+
+(*Used to prove project_leadsETo_I*)
+lemma (in Extend) ensures_extend_set_imp_project_ensures:
+ "[| extend h F : stable C; G : stable C;
+ extend h F Join G : A ensures B; A-B = C Int extend_set h D |]
+ ==> F Join project h C G
+ : (project_set h C Int project_set h A) ensures (project_set h B)"
+apply (simp add: ensures_def project_constrains Join_transient extend_transient, clarify)
+apply (intro conjI)
+(*first subgoal*)
+apply (blast intro: extend_stable_project_set
+ [THEN stableD, THEN constrains_Int, THEN constrains_weaken]
+ dest!: extend_constrains_project_set equalityD1)
+(*2nd subgoal*)
+apply (erule stableD [THEN constrains_Int, THEN constrains_weaken])
+ apply assumption
+ apply (simp (no_asm_use) add: extend_set_def)
+ apply blast
+ apply (simp add: extend_set_Int_distrib extend_set_Un_distrib)
+ apply (blast intro!: extend_set_project_set [THEN subsetD], blast)
+(*The transient part*)
+apply auto
+ prefer 2
+ apply (force dest!: equalityD1
+ intro: transient_extend_set_imp_project_transient
+ [THEN transient_strengthen])
+apply (simp (no_asm_use) add: Int_Diff)
+apply (force dest!: equalityD1
+ intro: transient_extend_set_imp_project_transient
+ [THEN project_extend_transient_D, THEN transient_strengthen])
+done
+
+(*Used to prove project_leadsETo_D*)
+lemma (in Extend) Join_project_ensures [rule_format (no_asm)]:
+ "[| project h C G ~: transient (A-B) | A<=B;
+ extend h F Join G : stable C;
+ F Join project h C G : A ensures B |]
+ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
+apply (erule disjE)
+prefer 2 apply (blast intro: subset_imp_ensures)
+apply (auto dest: extend_transient [THEN iffD2]
+ intro: transient_strengthen project_set_I
+ project_unless [THEN unlessD] unlessI
+ project_extend_constrains_I
+ simp add: ensures_def Join_transient)
+done
+
+(** Lemma useful for both STRONG and WEAK progress, but the transient
+ condition's very strong **)
+
+(*The strange induction formula allows induction over the leadsTo
+ assumption's non-atomic precondition*)
+lemma (in Extend) PLD_lemma:
+ "[| ALL D. project h C G : transient D --> D={};
+ extend h F Join G : stable C;
+ F Join project h C G : (project_set h C Int A) leadsTo B |]
+ ==> extend h F Join G :
+ C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"
+apply (erule leadsTo_induct)
+ apply (blast intro: leadsTo_Basis Join_project_ensures)
+ apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
+apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union)
+done
+
+lemma (in Extend) project_leadsTo_D_lemma:
+ "[| ALL D. project h C G : transient D --> D={};
+ extend h F Join G : stable C;
+ F Join project h C G : (project_set h C Int A) leadsTo B |]
+ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"
+apply (rule PLD_lemma [THEN leadsTo_weaken])
+apply (auto simp add: split_extended_all)
+done
+
+lemma (in Extend) Join_project_LeadsTo:
+ "[| C = (reachable (extend h F Join G));
+ ALL D. project h C G : transient D --> D={};
+ F Join project h C G : A LeadsTo B |]
+ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
+by (simp del: Join_stable add: LeadsTo_def project_leadsTo_D_lemma
+ project_set_reachable_extend_eq)
+
+
+(*** Towards project_Ensures_D ***)
+
+
+lemma (in Extend) act_subset_imp_project_act_subset:
+ "act `` (C Int extend_set h A) <= B
+ ==> project_act h (Restrict C act) `` (project_set h C Int A)
+ <= project_set h B"
+apply (unfold project_set_def extend_set_def project_act_def, blast)
+done
+
+(*This trivial proof is the complementation part of transferring a transient
+ property upwards. The hard part would be to
+ show that G's action has a big enough domain.*)
+lemma (in Extend)
+ "[| act: Acts G;
+ (project_act h (Restrict C act))``
+ (project_set h C Int A - B) <= -(project_set h C Int A - B) |]
+ ==> act``(C Int extend_set h A - extend_set h B)
+ <= -(C Int extend_set h A - extend_set h B)"
+by (auto simp add: project_set_def extend_set_def project_act_def)
+
+lemma (in Extend) stable_project_transient:
+ "[| G : stable ((C Int extend_set h A) - (extend_set h B));
+ project h C G : transient (project_set h C Int A - B) |]
+ ==> (C Int extend_set h A) - extend_set h B = {}"
+apply (auto simp add: transient_def subset_Compl_self_eq Domain_project_act split_extended_all, blast)
+apply (auto simp add: stable_def constrains_def)
+apply (drule bspec, assumption)
+apply (auto simp add: Int_Diff extend_set_Diff_distrib [symmetric])
+apply (drule act_subset_imp_project_act_subset)
+apply (subgoal_tac "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}")
+apply (erule_tac V = "?r``?A <= ?B" in thin_rl)+
+apply (unfold project_set_def extend_set_def project_act_def)
+prefer 2 apply blast
+apply (rule ccontr)
+apply (drule subsetD, blast)
+apply (force simp add: split_extended_all)
+done
+
+lemma (in Extend) project_unless2 [rule_format (no_asm)]:
+ "[| G : stable C; project h C G : (project_set h C Int A) unless B |]
+ ==> G : (C Int extend_set h A) unless (extend_set h B)"
+by (auto dest: stable_constrains_Int intro: constrains_weaken
+ simp add: unless_def project_constrains Diff_eq Int_assoc
+ Int_extend_set_lemma)
+
+lemma (in Extend) project_ensures_D_lemma:
+ "[| G : stable ((C Int extend_set h A) - (extend_set h B));
+ F Join project h C G : (project_set h C Int A) ensures B;
+ extend h F Join G : stable C |]
+ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
+(*unless*)
+apply (auto intro!: project_unless2 [unfolded unless_def]
+ intro: project_extend_constrains_I
+ simp add: ensures_def)
+(*transient*)
+(*A G-action cannot occur*)
+ prefer 2
+ apply (force dest: stable_project_transient
+ simp del: Diff_eq_empty_iff
+ simp add: Diff_eq_empty_iff [symmetric])
+(*An F-action*)
+apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
+ simp add: split_extended_all)
+done
+
+lemma (in Extend) project_ensures_D:
+ "[| F Join project h UNIV G : A ensures B;
+ G : stable (extend_set h A - extend_set h B) |]
+ ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"
+apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
+done
+
+lemma (in Extend) project_Ensures_D:
+ "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B;
+ G : stable (reachable (extend h F Join G) Int extend_set h A -
+ extend_set h B) |]
+ ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)"
+apply (unfold Ensures_def)
+apply (rule project_ensures_D_lemma [THEN revcut_rl])
+apply (auto simp add: project_set_reachable_extend_eq [symmetric])
+done
+
+
+(*** Guarantees ***)
+
+lemma (in Extend) project_act_Restrict_subset_project_act:
+ "project_act h (Restrict C act) <= project_act h act"
+apply (auto simp add: project_act_def)
+done
+
+
+lemma (in Extend) subset_closed_ok_extend_imp_ok_project:
+ "[| extend h F ok G; subset_closed (AllowedActs F) |]
+ ==> F ok project h C G"
+apply (auto simp add: ok_def)
+apply (rename_tac act)
+apply (drule subsetD, blast)
+apply (rule_tac x = "Restrict C (extend_act h act)" in rev_image_eqI)
+apply simp +
+apply (cut_tac project_act_Restrict_subset_project_act)
+apply (auto simp add: subset_closed_def)
+done
+
+
+(*Weak precondition and postcondition
+ Not clear that it has a converse [or that we want one!]*)
+
+(*The raw version; 3rd premise could be weakened by adding the
+ precondition extend h F Join G : X' *)
+lemma (in Extend) project_guarantees_raw:
+ assumes xguary: "F : X guarantees Y"
+ and closed: "subset_closed (AllowedActs F)"
+ and project: "!!G. extend h F Join G : X'
+ ==> F Join project h (C G) G : X"
+ and extend: "!!G. [| F Join project h (C G) G : Y |]
+ ==> extend h F Join G : Y'"
+ shows "extend h F : X' guarantees Y'"
+apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
+apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
+apply (erule project)
+done
+
+lemma (in Extend) project_guarantees:
+ "[| F : X guarantees Y; subset_closed (AllowedActs F);
+ projecting C h F X' X; extending C h F Y' Y |]
+ ==> extend h F : X' guarantees Y'"
+apply (rule guaranteesI)
+apply (auto simp add: guaranteesD projecting_def extending_def
+ subset_closed_ok_extend_imp_ok_project)
+done
+
+
+(*It seems that neither "guarantees" law can be proved from the other.*)
+
+
+(*** guarantees corollaries ***)
+
+(** Some could be deleted: the required versions are easy to prove **)
+
+lemma (in Extend) extend_guar_increasing:
+ "[| F : UNIV guarantees increasing func;
+ subset_closed (AllowedActs F) |]
+ ==> extend h F : X' guarantees increasing (func o f)"
+apply (erule project_guarantees)
+apply (rule_tac [3] extending_increasing)
+apply (rule_tac [2] projecting_UNIV, auto)
+done
+
+lemma (in Extend) extend_guar_Increasing:
+ "[| F : UNIV guarantees Increasing func;
+ subset_closed (AllowedActs F) |]
+ ==> extend h F : X' guarantees Increasing (func o f)"
+apply (erule project_guarantees)
+apply (rule_tac [3] extending_Increasing)
+apply (rule_tac [2] projecting_UNIV, auto)
+done
+
+lemma (in Extend) extend_guar_Always:
+ "[| F : Always A guarantees Always B;
+ subset_closed (AllowedActs F) |]
+ ==> extend h F
+ : Always(extend_set h A) guarantees Always(extend_set h B)"
+apply (erule project_guarantees)
+apply (rule_tac [3] extending_Always)
+apply (rule_tac [2] projecting_Always, auto)
+done
+
+lemma (in Extend) preserves_project_transient_empty:
+ "[| G : preserves f; project h C G : transient D |] ==> D={}"
+apply (rule stable_transient_empty)
+ prefer 2 apply assumption
+apply (blast intro: project_preserves_id_I
+ preserves_id_subset_stable [THEN subsetD])
+done
+
+
+(** Guarantees with a leadsTo postcondition
+ THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
+
+lemma (in Extend) project_leadsTo_D:
+ "[| F Join project h UNIV G : A leadsTo B;
+ G : preserves f |]
+ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"
+apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken])
+apply (auto dest: preserves_project_transient_empty)
+done
+
+lemma (in Extend) project_LeadsTo_D:
+ "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B;
+ G : preserves f |]
+ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
+apply (rule refl [THEN Join_project_LeadsTo])
+apply (auto dest: preserves_project_transient_empty)
+done
+
+lemma (in Extend) extending_leadsTo:
+ "(ALL G. extend h F ok G --> G : preserves f)
+ ==> extending (%G. UNIV) h F
+ (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
+apply (unfold extending_def)
+apply (blast intro: project_leadsTo_D)
+done
+
+lemma (in Extend) extending_LeadsTo:
+ "(ALL G. extend h F ok G --> G : preserves f)
+ ==> extending (%G. reachable (extend h F Join G)) h F
+ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
+apply (unfold extending_def)
+apply (blast intro: project_LeadsTo_D)
+done
+
+ML
+{*
+val projecting_Int = thm "projecting_Int";
+val projecting_Un = thm "projecting_Un";
+val projecting_INT = thm "projecting_INT";
+val projecting_UN = thm "projecting_UN";
+val projecting_weaken = thm "projecting_weaken";
+val projecting_weaken_L = thm "projecting_weaken_L";
+val extending_Int = thm "extending_Int";
+val extending_Un = thm "extending_Un";
+val extending_INT = thm "extending_INT";
+val extending_UN = thm "extending_UN";
+val extending_weaken = thm "extending_weaken";
+val extending_weaken_L = thm "extending_weaken_L";
+val projecting_UNIV = thm "projecting_UNIV";
+*}
+
end
--- a/src/HOL/UNITY/ROOT.ML Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/UNITY/ROOT.ML Wed Jan 29 11:02:08 2003 +0100
@@ -24,7 +24,6 @@
time_use_thy"Simple/NSP_Bad";
(*Example of composition*)
-time_use_thy "Comp";
time_use_thy "Comp/Handshake";
(*Universal properties examples*)
@@ -32,10 +31,9 @@
time_use_thy "Comp/Counterc";
time_use_thy "Comp/Priority";
-(*Allocator example*)
-time_use_thy "PPROD";
time_use_thy "Comp/TimerArray";
+(*Allocator example*)
time_use_thy "Comp/Alloc";
time_use_thy "Comp/AllocImpl";
time_use_thy "Comp/Client";
--- a/src/HOL/UNITY/Rename.ML Tue Jan 28 22:53:39 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,383 +0,0 @@
-(* Title: HOL/UNITY/Rename.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
-
-*)
-
-Addsimps [image_inv_f_f, image_surj_f_inv_f];
-
-Goal "bij h ==> good_map (%(x,u). h x)";
-by (rtac good_mapI 1);
-by (rewrite_goals_tac [bij_def, inj_on_def, surj_def]);
-by Auto_tac;
-qed "good_map_bij";
-Addsimps [good_map_bij];
-AddIs [good_map_bij];
-
-fun bij_export th = good_map_bij RS export th |> simplify (simpset());
-
-Goalw [bij_def, split_def] "bij h ==> fst (inv (%(x,u). h x) s) = inv h s";
-by (Clarify_tac 1);
-by (subgoal_tac "surj (%p. h (fst p))" 1);
-by (asm_full_simp_tac (simpset() addsimps [surj_def]) 2);
-by (etac injD 1);
-by (asm_simp_tac (simpset() addsimps [surj_f_inv_f]) 1);
-by (etac surj_f_inv_f 1);
-qed "fst_o_inv_eq_inv";
-
-Goal "bij h ==> z : h`A = (inv h z : A)";
-by (auto_tac (claset() addSIs [image_eqI],
- simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
-qed "mem_rename_set_iff";
-
-Goal "extend_set (%(x,u). h x) A = h`A";
-by (auto_tac (claset() addSIs [image_eqI],
- simpset() addsimps [extend_set_def]));
-qed "extend_set_eq_image";
-Addsimps [extend_set_eq_image];
-
-Goalw [rename_def] "Init (rename h F) = h`(Init F)";
-by (Simp_tac 1);
-qed "Init_rename";
-
-Addsimps [Init_rename];
-
-
-(*** inverse properties ***)
-
-Goalw [bij_def]
- "bij h \
-\ ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)";
-by (rtac ext 1);
-by (auto_tac (claset() addSIs [image_eqI],
- simpset() addsimps [extend_set_def, project_set_def,
- surj_f_inv_f]));
-qed "extend_set_inv";
-
-(** for "rename" (programs) **)
-
-Goal "bij h \
-\ ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)";
-by (rtac ext 1);
-by (auto_tac (claset() addSIs [image_eqI],
- simpset() addsimps [extend_act_def, project_act_def, bij_def,
- surj_f_inv_f]));
-qed "bij_extend_act_eq_project_act";
-
-Goal "bij h ==> bij (extend_act (%(x,u::'c). h x))";
-by (rtac bijI 1);
-by (rtac (export inj_extend_act) 1);
-by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act]));
-by (rtac surjI 1);
-by (rtac (export extend_act_inverse) 1);
-by (blast_tac (claset() addIs [bij_imp_bij_inv, good_map_bij]) 1);
-qed "bij_extend_act";
-
-Goal "bij h ==> bij (project_act (%(x,u::'c). h x))";
-by (ftac (bij_imp_bij_inv RS bij_extend_act) 1);
-by (asm_full_simp_tac (simpset() addsimps [bij_extend_act_eq_project_act,
- bij_imp_bij_inv, inv_inv_eq]) 1);
-qed "bij_project_act";
-
-Goal "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = \
-\ project_act (%(x,u::'c). h x)";
-by (asm_simp_tac
- (simpset() addsimps [bij_extend_act_eq_project_act RS sym]) 1);
-by (rtac surj_imp_inv_eq 1);
-by (blast_tac (claset() addIs [bij_extend_act, bij_is_surj]) 1);
-by (asm_simp_tac (simpset() addsimps [export extend_act_inverse]) 1);
-qed "bij_inv_project_act_eq";
-
-Goal "bij h \
-\ ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV";
-by (ftac bij_imp_bij_inv 1);
-by (rtac ext 1);
-by (rtac program_equalityI 1);
-by (asm_simp_tac
- (simpset() addsimps [export project_act_Id, export Acts_extend,
- insert_Id_image_Acts, bij_extend_act_eq_project_act,
- inv_inv_eq]) 2);
-by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1);
-by (asm_simp_tac
- (simpset() addsimps [export AllowedActs_extend,
- export AllowedActs_project,
- bij_project_act, bij_vimage_eq_inv_image,
- bij_inv_project_act_eq]) 1);
-qed "extend_inv";
-
-Goal "bij h ==> rename (inv h) (rename h F) = F";
-by (asm_simp_tac (simpset() addsimps [rename_def, extend_inv,
- export extend_inverse]) 1);
-qed "rename_inv_rename";
-Addsimps [rename_inv_rename];
-
-Goal "bij h ==> rename h (rename (inv h) F) = F";
-by (ftac bij_imp_bij_inv 1);
-by (etac (inv_inv_eq RS subst) 1 THEN etac rename_inv_rename 1);
-qed "rename_rename_inv";
-Addsimps [rename_rename_inv];
-
-Goal "bij h ==> rename (inv h) = inv (rename h)";
-by (rtac (inv_equality RS sym) 1);
-by Auto_tac;
-qed "rename_inv_eq";
-
-(** (rename h) is bijective <=> h is bijective **)
-
-Goal "bij h ==> bij (extend (%(x,u::'c). h x))";
-by (rtac bijI 1);
-by (blast_tac (claset() addIs [export inj_extend]) 1);
-by (res_inst_tac [("f","extend (%(x,u). inv h x)")] surjI 1);
-by (stac ((inst "f" "h" inv_inv_eq) RS sym) 1
- THEN stac extend_inv 2 THEN stac (export extend_inverse) 3);
-by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, inv_inv_eq]));
-qed "bij_extend";
-
-Goal "bij h ==> bij (project (%(x,u::'c). h x) UNIV)";
-by (stac (extend_inv RS sym) 1);
-by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, bij_extend]));
-qed "bij_project";
-
-Goal "bij h \
-\ ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)";
-by (rtac inj_imp_inv_eq 1);
-by (etac (bij_project RS bij_is_inj) 1);
-by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1);
-qed "inv_project_eq";
-
-Goal "bij h ==> Allowed (rename h F) = rename h ` Allowed F";
-by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1);
-by (stac bij_vimage_eq_inv_image 1);
-by (rtac bij_project 1);
-by (Blast_tac 1);
-by (asm_simp_tac (simpset() addsimps [inv_project_eq]) 1);
-qed "Allowed_rename";
-Addsimps [Allowed_rename];
-
-Goal "bij h ==> bij (rename h)";
-by (asm_simp_tac (simpset() addsimps [rename_def, bij_extend]) 1);
-qed "bij_rename";
-bind_thm ("surj_rename", bij_rename RS bij_is_surj);
-
-Goalw [inj_on_def] "inj (rename h) ==> inj h";
-by Auto_tac;
-by (dres_inst_tac [("x", "mk_program ({x}, {}, {})")] spec 1);
-by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
-by (auto_tac (claset(),
- simpset() addsimps [program_equality_iff,
- rename_def, extend_def]));
-qed "inj_rename_imp_inj";
-
-Goalw [surj_def] "surj (rename h) ==> surj h";
-by Auto_tac;
-by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
-by (auto_tac (claset(),
- simpset() addsimps [program_equality_iff,
- rename_def, extend_def]));
-qed "surj_rename_imp_surj";
-
-Goalw [bij_def] "bij (rename h) ==> bij h";
-by (asm_simp_tac
- (simpset() addsimps [inj_rename_imp_inj, surj_rename_imp_surj]) 1);
-qed "bij_rename_imp_bij";
-
-Goal "bij (rename h) = bij h";
-by (blast_tac (claset() addIs [bij_rename, bij_rename_imp_bij]) 1);
-qed "bij_rename_iff";
-AddIffs [bij_rename_iff];
-
-
-(*** the lattice operations ***)
-
-Goalw [rename_def] "bij h ==> rename h SKIP = SKIP";
-by (Asm_simp_tac 1);
-qed "rename_SKIP";
-Addsimps [rename_SKIP];
-
-Goalw [rename_def]
- "bij h ==> rename h (F Join G) = rename h F Join rename h G";
-by (asm_simp_tac (simpset() addsimps [export extend_Join]) 1);
-qed "rename_Join";
-Addsimps [rename_Join];
-
-Goalw [rename_def] "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))";
-by (asm_simp_tac (simpset() addsimps [export extend_JN]) 1);
-qed "rename_JN";
-Addsimps [rename_JN];
-
-
-(*** Strong Safety: co, stable ***)
-
-Goalw [rename_def]
- "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)";
-by (REPEAT (stac (extend_set_eq_image RS sym) 1));
-by (etac (good_map_bij RS export extend_constrains) 1);
-qed "rename_constrains";
-
-Goalw [stable_def]
- "bij h ==> (rename h F : stable (h`A)) = (F : stable A)";
-by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
-qed "rename_stable";
-
-Goal "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)";
-by (asm_simp_tac (simpset() addsimps [invariant_def, rename_stable,
- bij_is_inj RS inj_image_subset_iff]) 1);
-qed "rename_invariant";
-
-Goal "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))";
-by (asm_simp_tac
- (simpset() addsimps [increasing_def, rename_stable RS sym,
- bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1);
-qed "rename_increasing";
-
-
-(*** Weak Safety: Co, Stable ***)
-
-Goalw [rename_def]
- "bij h ==> reachable (rename h F) = h ` (reachable F)";
-by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1);
-qed "reachable_rename_eq";
-
-Goal "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)";
-by (asm_simp_tac
- (simpset() addsimps [Constrains_def, reachable_rename_eq,
- rename_constrains, bij_is_inj, image_Int RS sym]) 1);
-qed "rename_Constrains";
-
-Goalw [Stable_def]
- "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)";
-by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
-qed "rename_Stable";
-
-Goal "bij h ==> (rename h F : Always (h`A)) = (F : Always A)";
-by (asm_simp_tac (simpset() addsimps [Always_def, rename_Stable,
- bij_is_inj RS inj_image_subset_iff]) 1);
-qed "rename_Always";
-
-Goal "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))";
-by (asm_simp_tac
- (simpset() addsimps [Increasing_def, rename_Stable RS sym,
- bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1);
-qed "rename_Increasing";
-
-
-(*** Progress: transient, ensures ***)
-
-Goalw [rename_def]
- "bij h ==> (rename h F : transient (h`A)) = (F : transient A)";
-by (stac (extend_set_eq_image RS sym) 1);
-by (etac (good_map_bij RS export extend_transient) 1);
-qed "rename_transient";
-
-Goalw [rename_def]
- "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)";
-by (REPEAT (stac (extend_set_eq_image RS sym) 1));
-by (etac (good_map_bij RS export extend_ensures) 1);
-qed "rename_ensures";
-
-Goalw [rename_def]
- "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)";
-by (REPEAT (stac (extend_set_eq_image RS sym) 1));
-by (etac (good_map_bij RS export extend_leadsTo) 1);
-qed "rename_leadsTo";
-
-Goalw [rename_def]
- "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)";
-by (REPEAT (stac (extend_set_eq_image RS sym) 1));
-by (etac (good_map_bij RS export extend_LeadsTo) 1);
-qed "rename_LeadsTo";
-
-Goalw [rename_def]
- "bij h ==> (rename h F : (rename h ` X) guarantees \
-\ (rename h ` Y)) = \
-\ (F : X guarantees Y)";
-by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1);
-qed "rename_rename_guarantees_eq";
-
-Goal "bij h ==> (rename h F : X guarantees Y) = \
-\ (F : (rename (inv h) ` X) guarantees \
-\ (rename (inv h) ` Y))";
-by (stac (rename_rename_guarantees_eq RS sym) 1);
-by (assume_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [image_eq_UN, o_def, bij_is_surj RS surj_f_inv_f]) 1);
-qed "rename_guarantees_eq_rename_inv";
-
-Goal "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))";
-by (stac (good_map_bij RS export extend_preserves RS sym) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [o_def, fst_o_inv_eq_inv, rename_def,
- bij_is_surj RS surj_f_inv_f]) 1);
-qed "rename_preserves";
-
-Goal "bij h ==> (rename h F ok rename h G) = (F ok G)";
-by (asm_simp_tac (simpset() addsimps [export ok_extend_iff, rename_def]) 1);
-qed "ok_rename_iff";
-Addsimps [ok_rename_iff];
-
-Goal "bij h ==> OK I (%i. rename h (F i)) = (OK I F)";
-by (asm_simp_tac (simpset() addsimps [export OK_extend_iff, rename_def]) 1);
-qed "OK_rename_iff";
-Addsimps [OK_rename_iff];
-
-
-(*** "image" versions of the rules, for lifting "guarantees" properties ***)
-
-
-(*Tactic used in all the proofs. Better would have been to prove one
- meta-theorem, but how can we handle the polymorphism? E.g. in
- rename_constrains the two appearances of "co" have different types!*)
-fun rename_image_tac ths =
- EVERY [Auto_tac,
- (rename_tac "F" 2),
- (subgoal_tac "EX G. F = rename h G" 2),
- (auto_tac (claset() addSIs [surj_rename RS surj_f_inv_f RS sym],
- simpset() addsimps ths))];
-
-Goal "bij h ==> rename h ` (A co B) = (h ` A) co (h`B)";
-by (rename_image_tac [rename_constrains]);
-qed "rename_image_constrains";
-
-Goal "bij h ==> rename h ` stable A = stable (h ` A)";
-by (rename_image_tac [rename_stable]);
-qed "rename_image_stable";
-
-Goal "bij h ==> rename h ` increasing func = increasing (func o inv h)";
-by (rename_image_tac [rename_increasing, o_def, bij_is_inj]);
-qed "rename_image_increasing";
-
-Goal "bij h ==> rename h ` invariant A = invariant (h ` A)";
-by (rename_image_tac [rename_invariant]);
-qed "rename_image_invariant";
-
-Goal "bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)";
-by (rename_image_tac [rename_Constrains]);
-qed "rename_image_Constrains";
-
-Goal "bij h ==> rename h ` preserves v = preserves (v o inv h)";
-by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable,
- preserves_def, bij_image_INT, bij_image_Collect_eq]) 1);
-qed "rename_image_preserves";
-
-Goal "bij h ==> rename h ` Stable A = Stable (h ` A)";
-by (rename_image_tac [rename_Stable]);
-qed "rename_image_Stable";
-
-Goal "bij h ==> rename h ` Increasing func = Increasing (func o inv h)";
-by (rename_image_tac [rename_Increasing, o_def, bij_is_inj]);
-qed "rename_image_Increasing";
-
-Goal "bij h ==> rename h ` Always A = Always (h ` A)";
-by (rename_image_tac [rename_Always]);
-qed "rename_image_Always";
-
-Goal "bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)";
-by (rename_image_tac [rename_leadsTo]);
-qed "rename_image_leadsTo";
-
-Goal "bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)";
-by (rename_image_tac [rename_LeadsTo]);
-qed "rename_image_LeadsTo";
--- a/src/HOL/UNITY/Rename.thy Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/UNITY/Rename.thy Wed Jan 29 11:02:08 2003 +0100
@@ -6,11 +6,388 @@
Renaming of state sets
*)
-Rename = Extend +
+theory Rename = Extend:
constdefs
rename :: "['a => 'b, 'a program] => 'b program"
"rename h == extend (%(x,u::unit). h x)"
+declare image_inv_f_f [simp] image_surj_f_inv_f [simp]
+
+declare Extend.intro [simp,intro]
+
+lemma good_map_bij [simp,intro]: "bij h ==> good_map (%(x,u). h x)"
+apply (rule good_mapI)
+apply (unfold bij_def inj_on_def surj_def, auto)
+done
+
+lemma fst_o_inv_eq_inv: "bij h ==> fst (inv (%(x,u). h x) s) = inv h s"
+apply (unfold bij_def split_def, clarify)
+apply (subgoal_tac "surj (%p. h (fst p))")
+ prefer 2 apply (simp add: surj_def)
+apply (erule injD)
+apply (simp (no_asm_simp) add: surj_f_inv_f)
+apply (erule surj_f_inv_f)
+done
+
+lemma mem_rename_set_iff: "bij h ==> z : h`A = (inv h z : A)"
+by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f])
+
+
+lemma extend_set_eq_image [simp]: "extend_set (%(x,u). h x) A = h`A"
+by (force simp add: extend_set_def)
+
+lemma Init_rename [simp]: "Init (rename h F) = h`(Init F)"
+by (simp add: rename_def)
+
+
+(*** inverse properties ***)
+
+lemma extend_set_inv:
+ "bij h
+ ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)"
+apply (unfold bij_def)
+apply (rule ext)
+apply (force simp add: extend_set_def project_set_def surj_f_inv_f)
+done
+
+(** for "rename" (programs) **)
+
+lemma bij_extend_act_eq_project_act: "bij h
+ ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)"
+apply (rule ext)
+apply (force simp add: extend_act_def project_act_def bij_def surj_f_inv_f)
+done
+
+lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
+apply (rule bijI)
+apply (rule Extend.inj_extend_act)
+apply (auto simp add: bij_extend_act_eq_project_act)
+apply (rule surjI)
+apply (rule Extend.extend_act_inverse)
+apply (blast intro: bij_imp_bij_inv good_map_bij)
+done
+
+lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"
+apply (frule bij_imp_bij_inv [THEN bij_extend_act])
+apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq)
+done
+
+lemma bij_inv_project_act_eq: "bij h ==> inv (project_act (%(x,u::'c). inv h x)) =
+ project_act (%(x,u::'c). h x)"
+apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
+apply (rule surj_imp_inv_eq)
+apply (blast intro: bij_extend_act bij_is_surj)
+apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
+done
+
+lemma extend_inv: "bij h
+ ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV"
+apply (frule bij_imp_bij_inv)
+apply (rule ext)
+apply (rule program_equalityI)
+ apply (simp (no_asm_simp) add: extend_set_inv)
+ apply (simp add: Extend.project_act_Id Extend.Acts_extend
+ insert_Id_image_Acts bij_extend_act_eq_project_act inv_inv_eq)
+apply (simp add: Extend.AllowedActs_extend Extend.AllowedActs_project
+ bij_project_act bij_vimage_eq_inv_image bij_inv_project_act_eq)
+done
+
+lemma rename_inv_rename [simp]: "bij h ==> rename (inv h) (rename h F) = F"
+by (simp add: rename_def extend_inv Extend.extend_inverse)
+
+lemma rename_rename_inv [simp]: "bij h ==> rename h (rename (inv h) F) = F"
+apply (frule bij_imp_bij_inv)
+apply (erule inv_inv_eq [THEN subst], erule rename_inv_rename)
+done
+
+lemma rename_inv_eq: "bij h ==> rename (inv h) = inv (rename h)"
+by (rule inv_equality [symmetric], auto)
+
+(** (rename h) is bijective <=> h is bijective **)
+
+lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))"
+apply (rule bijI)
+apply (blast intro: Extend.inj_extend)
+apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI)
+apply (subst inv_inv_eq [of h, symmetric], assumption)
+apply (subst extend_inv, simp add: bij_imp_bij_inv)
+apply (simp add: inv_inv_eq)
+apply (rule Extend.extend_inverse)
+apply (simp add: bij_imp_bij_inv)
+done
+
+lemma bij_project: "bij h ==> bij (project (%(x,u::'c). h x) UNIV)"
+apply (subst extend_inv [symmetric])
+apply (auto simp add: bij_imp_bij_inv bij_extend)
+done
+
+lemma inv_project_eq:
+ "bij h
+ ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)"
+apply (rule inj_imp_inv_eq)
+apply (erule bij_project [THEN bij_is_inj])
+apply (simp (no_asm_simp) add: Extend.extend_inverse)
+done
+
+lemma Allowed_rename [simp]:
+ "bij h ==> Allowed (rename h F) = rename h ` Allowed F"
+apply (simp (no_asm_simp) add: rename_def Extend.Allowed_extend)
+apply (subst bij_vimage_eq_inv_image)
+apply (rule bij_project, blast)
+apply (simp (no_asm_simp) add: inv_project_eq)
+done
+
+lemma bij_rename: "bij h ==> bij (rename h)"
+apply (simp (no_asm_simp) add: rename_def bij_extend)
+done
+lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]
+
+lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
+apply (unfold inj_on_def, auto)
+apply (drule_tac x = "mk_program ({x}, {}, {}) " in spec)
+apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
+apply (auto simp add: program_equality_iff rename_def extend_def)
+done
+
+lemma surj_rename_imp_surj: "surj (rename h) ==> surj h"
+apply (unfold surj_def, auto)
+apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
+apply (auto simp add: program_equality_iff rename_def extend_def)
+done
+
+lemma bij_rename_imp_bij: "bij (rename h) ==> bij h"
+apply (unfold bij_def)
+apply (simp (no_asm_simp) add: inj_rename_imp_inj surj_rename_imp_surj)
+done
+
+lemma bij_rename_iff [simp]: "bij (rename h) = bij h"
+by (blast intro: bij_rename bij_rename_imp_bij)
+
+
+(*** the lattice operations ***)
+
+lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
+by (simp add: rename_def Extend.extend_SKIP)
+
+lemma rename_Join [simp]:
+ "bij h ==> rename h (F Join G) = rename h F Join rename h G"
+by (simp add: rename_def Extend.extend_Join)
+
+lemma rename_JN [simp]:
+ "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))"
+by (simp add: rename_def Extend.extend_JN)
+
+
+(*** Strong Safety: co, stable ***)
+
+lemma rename_constrains:
+ "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"
+apply (unfold rename_def)
+apply (subst extend_set_eq_image [symmetric])+
+apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_constrains])
+done
+
+lemma rename_stable:
+ "bij h ==> (rename h F : stable (h`A)) = (F : stable A)"
+apply (simp add: stable_def rename_constrains)
+done
+
+lemma rename_invariant:
+ "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)"
+apply (simp add: invariant_def rename_stable bij_is_inj [THEN inj_image_subset_iff])
+done
+
+lemma rename_increasing:
+ "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))"
+apply (simp add: increasing_def rename_stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f])
+done
+
+
+(*** Weak Safety: Co, Stable ***)
+
+lemma reachable_rename_eq:
+ "bij h ==> reachable (rename h F) = h ` (reachable F)"
+apply (simp add: rename_def Extend.reachable_extend_eq)
+done
+
+lemma rename_Constrains:
+ "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)"
+by (simp add: Constrains_def reachable_rename_eq rename_constrains
+ bij_is_inj image_Int [symmetric])
+
+lemma rename_Stable:
+ "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)"
+by (simp add: Stable_def rename_Constrains)
+
+lemma rename_Always: "bij h ==> (rename h F : Always (h`A)) = (F : Always A)"
+by (simp add: Always_def rename_Stable bij_is_inj [THEN inj_image_subset_iff])
+
+lemma rename_Increasing:
+ "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))"
+by (simp add: Increasing_def rename_Stable [symmetric] bij_image_Collect_eq
+ bij_is_surj [THEN surj_f_inv_f])
+
+
+(*** Progress: transient, ensures ***)
+
+lemma rename_transient:
+ "bij h ==> (rename h F : transient (h`A)) = (F : transient A)"
+apply (unfold rename_def)
+apply (subst extend_set_eq_image [symmetric])
+apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_transient])
+done
+
+lemma rename_ensures:
+ "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)"
+apply (unfold rename_def)
+apply (subst extend_set_eq_image [symmetric])+
+apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_ensures])
+done
+
+lemma rename_leadsTo:
+ "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)"
+apply (unfold rename_def)
+apply (subst extend_set_eq_image [symmetric])+
+apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_leadsTo])
+done
+
+lemma rename_LeadsTo:
+ "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)"
+apply (unfold rename_def)
+apply (subst extend_set_eq_image [symmetric])+
+apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_LeadsTo])
+done
+
+lemma rename_rename_guarantees_eq:
+ "bij h ==> (rename h F : (rename h ` X) guarantees
+ (rename h ` Y)) =
+ (F : X guarantees Y)"
+apply (unfold rename_def)
+apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_guarantees_eq [symmetric]], assumption)
+apply (simp (no_asm_simp) add: fst_o_inv_eq_inv o_def)
+done
+
+lemma rename_guarantees_eq_rename_inv:
+ "bij h ==> (rename h F : X guarantees Y) =
+ (F : (rename (inv h) ` X) guarantees
+ (rename (inv h) ` Y))"
+apply (subst rename_rename_guarantees_eq [symmetric], assumption)
+apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f])
+done
+
+lemma rename_preserves:
+ "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))"
+apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_preserves [symmetric]], assumption)
+apply (simp add: o_def fst_o_inv_eq_inv rename_def bij_is_surj [THEN surj_f_inv_f])
+done
+
+lemma ok_rename_iff [simp]: "bij h ==> (rename h F ok rename h G) = (F ok G)"
+by (simp add: Extend.ok_extend_iff rename_def)
+
+lemma OK_rename_iff [simp]: "bij h ==> OK I (%i. rename h (F i)) = (OK I F)"
+by (simp add: Extend.OK_extend_iff rename_def)
+
+
+(*** "image" versions of the rules, for lifting "guarantees" properties ***)
+
+(*All the proofs are similar. Better would have been to prove one
+ meta-theorem, but how can we handle the polymorphism? E.g. in
+ rename_constrains the two appearances of "co" have different types!*)
+lemmas bij_eq_rename = surj_rename [THEN surj_f_inv_f, symmetric]
+
+lemma rename_image_constrains:
+ "bij h ==> rename h ` (A co B) = (h ` A) co (h`B)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_constrains)
+done
+
+lemma rename_image_stable: "bij h ==> rename h ` stable A = stable (h ` A)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_stable)
+done
+
+lemma rename_image_increasing:
+ "bij h ==> rename h ` increasing func = increasing (func o inv h)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_increasing o_def bij_is_inj)
+done
+
+lemma rename_image_invariant:
+ "bij h ==> rename h ` invariant A = invariant (h ` A)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_invariant)
+done
+
+lemma rename_image_Constrains:
+ "bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_Constrains)
+done
+
+lemma rename_image_preserves:
+ "bij h ==> rename h ` preserves v = preserves (v o inv h)"
+by (simp add: o_def rename_image_stable preserves_def bij_image_INT
+ bij_image_Collect_eq)
+
+lemma rename_image_Stable:
+ "bij h ==> rename h ` Stable A = Stable (h ` A)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_Stable)
+done
+
+lemma rename_image_Increasing:
+ "bij h ==> rename h ` Increasing func = Increasing (func o inv h)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_Increasing o_def bij_is_inj)
+done
+
+lemma rename_image_Always: "bij h ==> rename h ` Always A = Always (h ` A)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_Always)
+done
+
+lemma rename_image_leadsTo:
+ "bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_leadsTo)
+done
+
+lemma rename_image_LeadsTo:
+ "bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)"
+apply auto
+ defer 1
+ apply (rename_tac F)
+ apply (subgoal_tac "\<exists>G. F = rename h G")
+ apply (auto intro!: bij_eq_rename simp add: rename_LeadsTo)
+done
+
end
--- a/src/HOL/UNITY/UNITY_tactics.ML Tue Jan 28 22:53:39 2003 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 11:02:08 2003 +0100
@@ -6,6 +6,96 @@
Specialized UNITY tactics, and ML bindings of theorems
*)
+(*Extend*)
+val Restrict_iff = thm "Restrict_iff";
+val Restrict_UNIV = thm "Restrict_UNIV";
+val Restrict_empty = thm "Restrict_empty";
+val Restrict_Int = thm "Restrict_Int";
+val Restrict_triv = thm "Restrict_triv";
+val Restrict_subset = thm "Restrict_subset";
+val Restrict_eq_mono = thm "Restrict_eq_mono";
+val Restrict_imageI = thm "Restrict_imageI";
+val Domain_Restrict = thm "Domain_Restrict";
+val Image_Restrict = thm "Image_Restrict";
+val insert_Id_image_Acts = thm "insert_Id_image_Acts";
+val good_mapI = thm "good_mapI";
+val good_map_is_surj = thm "good_map_is_surj";
+val fst_inv_equalityI = thm "fst_inv_equalityI";
+val project_set_iff = thm "project_set_iff";
+val extend_set_mono = thm "extend_set_mono";
+val extend_set_empty = thm "extend_set_empty";
+val project_set_Int_subset = thm "project_set_Int_subset";
+val Init_extend = thm "Init_extend";
+val Init_project = thm "Init_project";
+val Acts_project = thm "Acts_project";
+val project_set_UNIV = thm "project_set_UNIV";
+val project_set_Union = thm "project_set_Union";
+val project_act_mono = thm "project_act_mono";
+val project_constrains_project_set = thm "project_constrains_project_set";
+val project_stable_project_set = thm "project_stable_project_set";
+
+
+(*Rename*)
+val good_map_bij = thm "good_map_bij";
+val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv";
+val mem_rename_set_iff = thm "mem_rename_set_iff";
+val extend_set_eq_image = thm "extend_set_eq_image";
+val Init_rename = thm "Init_rename";
+val extend_set_inv = thm "extend_set_inv";
+val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act";
+val bij_extend_act = thm "bij_extend_act";
+val bij_project_act = thm "bij_project_act";
+val bij_inv_project_act_eq = thm "bij_inv_project_act_eq";
+val Acts_project = thm "Acts_project";
+val extend_inv = thm "extend_inv";
+val rename_inv_rename = thm "rename_inv_rename";
+val rename_rename_inv = thm "rename_rename_inv";
+val rename_inv_eq = thm "rename_inv_eq";
+val bij_extend = thm "bij_extend";
+val bij_project = thm "bij_project";
+val inv_project_eq = thm "inv_project_eq";
+val Allowed_rename = thm "Allowed_rename";
+val bij_rename = thm "bij_rename";
+val surj_rename = thm "surj_rename";
+val inj_rename_imp_inj = thm "inj_rename_imp_inj";
+val surj_rename_imp_surj = thm "surj_rename_imp_surj";
+val bij_rename_imp_bij = thm "bij_rename_imp_bij";
+val bij_rename_iff = thm "bij_rename_iff";
+val rename_SKIP = thm "rename_SKIP";
+val rename_Join = thm "rename_Join";
+val rename_JN = thm "rename_JN";
+val rename_constrains = thm "rename_constrains";
+val rename_stable = thm "rename_stable";
+val rename_invariant = thm "rename_invariant";
+val rename_increasing = thm "rename_increasing";
+val reachable_rename_eq = thm "reachable_rename_eq";
+val rename_Constrains = thm "rename_Constrains";
+val rename_Stable = thm "rename_Stable";
+val rename_Always = thm "rename_Always";
+val rename_Increasing = thm "rename_Increasing";
+val rename_transient = thm "rename_transient";
+val rename_ensures = thm "rename_ensures";
+val rename_leadsTo = thm "rename_leadsTo";
+val rename_LeadsTo = thm "rename_LeadsTo";
+val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq";
+val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv";
+val rename_preserves = thm "rename_preserves";
+val ok_rename_iff = thm "ok_rename_iff";
+val OK_rename_iff = thm "OK_rename_iff";
+val bij_eq_rename = thm "bij_eq_rename";
+val rename_image_constrains = thm "rename_image_constrains";
+val rename_image_stable = thm "rename_image_stable";
+val rename_image_increasing = thm "rename_image_increasing";
+val rename_image_invariant = thm "rename_image_invariant";
+val rename_image_Constrains = thm "rename_image_Constrains";
+val rename_image_preserves = thm "rename_image_preserves";
+val rename_image_Stable = thm "rename_image_Stable";
+val rename_image_Increasing = thm "rename_image_Increasing";
+val rename_image_Always = thm "rename_image_Always";
+val rename_image_leadsTo = thm "rename_image_leadsTo";
+val rename_image_LeadsTo = thm "rename_image_LeadsTo";
+
+
(*Lift_prog*)
val sub_def = thm "sub_def";