# HG changeset patch # User paulson # Date 1043834528 -3600 # Node ID 8d7e9fce8c505c825891c685ee649ef4cb7499f0 # Parent d37f66755f477e490fa86c8652e2289fc3a2069b converting UNITY to new-style theories diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/IsaMakefile --- 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 diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/ELT.ML --- 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"; - - diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/ELT.thy --- 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 diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/Extend.ML --- 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]; -*) diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/Extend.thy --- 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: "\z. PROP P z" + fix u y + show "PROP P (h (u, y))" by (rule allP) + next + assume allPh: "\u y. PROP P (h(u,y))" + fix z + have Phfgz: "PROP P (h (f z, g z))" by (rule allPh) + show "PROP P z" by (rule Phfgz [unfolded h_f_g_equiv]) +qed + + + +(*** 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 diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/Lift_prog.thy --- 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'). \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 diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/Project.ML --- 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"; diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/Project.thy --- 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 diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/ROOT.ML --- 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"; diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/Rename.ML --- 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"; diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/Rename.thy --- 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 "\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 "\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 "\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 "\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 "\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 "\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 "\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 "\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 "\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 "\G. F = rename h G") + apply (auto intro!: bij_eq_rename simp add: rename_LeadsTo) +done + end diff -r d37f66755f47 -r 8d7e9fce8c50 src/HOL/UNITY/UNITY_tactics.ML --- 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";