# HG changeset patch # User paulson # Date 1043946489 -3600 # Node ID baefae13ad379e78b6bcae1a1bf88f3ccc2ae3bd # Parent 19f50fa807ae16653d9c3a5e74765e9e13f38e04 conversion of UNITY theories to new-style diff -r 19f50fa807ae -r baefae13ad37 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/IsaMakefile Thu Jan 30 18:08:09 2003 +0100 @@ -382,13 +382,12 @@ $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \ - UNITY/Comp.thy UNITY/Detects.thy UNITY/ELT.thy \ + UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ UNITY/Extend.thy UNITY/FP.thy \ UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \ UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \ UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ - UNITY/SubstAx.thy UNITY/UNITY.ML \ - UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \ + UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy 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 \ diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/Comp/Client.ML --- a/src/HOL/UNITY/Comp/Client.ML Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/Comp/Client.ML Thu Jan 30 18:08:09 2003 +0100 @@ -8,8 +8,6 @@ Addsimps [Client_def RS def_prg_Init, Client_def RS def_prg_AllowedActs]; -program_defs_ref := [Client_def]; - Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]); Goal "(Client ok G) = \ @@ -26,7 +24,7 @@ by (auto_tac (claset() addSIs [increasing_imp_Increasing], simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing])); -by (auto_tac (claset(), simpset() addsimps [increasing_def])); +by (auto_tac (claset(), simpset() addsimps [Client_def, increasing_def])); by (ALLGOALS constrains_tac); by Auto_tac; qed "increasing_ask_rel"; @@ -46,6 +44,7 @@ by (rtac (invariantI RS stable_Join_Always2) 1); by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable] addSIs [stable_Int]) 3); +by (asm_full_simp_tac (simpset() addsimps [Client_def]) 2); by (constrains_tac 2); by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2); by Auto_tac; @@ -63,6 +62,7 @@ (*** Towards proving the liveness property ***) Goal "Client: stable {s. rel s <= giv s}"; +by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1); by (constrains_tac 1); by Auto_tac; qed "stable_rel_le_giv"; @@ -150,8 +150,8 @@ (*This shows that the Client won't alter other variables in any state that it is combined with*) Goal "Client : preserves dummy"; -by (rewtac preserves_def); -by Auto_tac; +by (asm_full_simp_tac (simpset() addsimps [Client_def, preserves_def]) 1); +by (Clarify_tac 1); by (constrains_tac 1); by Auto_tac; qed "client_preserves_dummy"; @@ -160,6 +160,7 @@ (** Obsolete lemmas from first version of the Client **) Goal "Client: stable {s. size (rel s) <= size (giv s)}"; +by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1); by (constrains_tac 1); by Auto_tac; qed "stable_size_rel_le_giv"; diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/Comp/Counter.ML --- a/src/HOL/UNITY/Comp/Counter.ML Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counter.ML Thu Jan 30 18:08:09 2003 +0100 @@ -12,7 +12,6 @@ *) Addsimps [Component_def RS def_prg_Init]; -program_defs_ref := [Component_def]; Addsimps (map simp_of_act [a_def]); (* Theorems about sum and sumj *) @@ -67,11 +66,12 @@ (* Correctness proofs for Components *) (* p2 and p3 proofs *) Goal "Component i : stable {s. s C = s (c i) + k}"; +by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); by (constrains_tac 1); qed "p2"; -Goal -"Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}"; +Goal "Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}"; +by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); by (constrains_tac 1); qed "p3"; diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/Comp/Counterc.ML --- a/src/HOL/UNITY/Comp/Counterc.ML Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counterc.ML Thu Jan 30 18:08:09 2003 +0100 @@ -13,7 +13,6 @@ Addsimps [Component_def RS def_prg_Init, Component_def RS def_prg_AllowedActs]; -program_defs_ref := [Component_def]; Addsimps (map simp_of_act [a_def]); (* Theorems about sum and sumj *) @@ -57,6 +56,7 @@ Goal "Component i: stable {s. C s = (c s) i + k}"; +by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); by (constrains_tac 1); qed "p2"; diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/Constrains.ML --- a/src/HOL/UNITY/Constrains.ML Thu Jan 30 10:35:56 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,407 +0,0 @@ -(* Title: HOL/UNITY/Constrains - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Safety relations: restricted to the set of reachable states. -*) - - -(*** traces and reachable ***) - -Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"; -by Safe_tac; -by (etac traces.induct 2); -by (etac reachable.induct 1); -by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs))); -qed "reachable_equiv_traces"; - -Goal "Init F <= reachable F"; -by (blast_tac (claset() addIs reachable.intrs) 1); -qed "Init_subset_reachable"; - -Goal "Acts G <= Acts F ==> G : stable (reachable F)"; -by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1); -qed "stable_reachable"; - -AddSIs [stable_reachable]; -Addsimps [stable_reachable]; - -(*The set of all reachable states is an invariant...*) -Goal "F : invariant (reachable F)"; -by (simp_tac (simpset() addsimps [invariant_def]) 1); -by (blast_tac (claset() addIs reachable.intrs) 1); -qed "invariant_reachable"; - -(*...in fact the strongest invariant!*) -Goal "F : invariant A ==> reachable F <= A"; -by (full_simp_tac - (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1); -by (rtac subsetI 1); -by (etac reachable.induct 1); -by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); -qed "invariant_includes_reachable"; - - -(*** Co ***) - -(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) -bind_thm ("constrains_reachable_Int", - subset_refl RS - rewrite_rule [stable_def] stable_reachable RS - constrains_Int); - -(*Resembles the previous definition of Constrains*) -Goalw [Constrains_def] - "A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}"; -by (blast_tac (claset() addDs [constrains_reachable_Int] - addIs [constrains_weaken]) 1); -qed "Constrains_eq_constrains"; - -Goalw [Constrains_def] "F : A co A' ==> F : A Co A'"; -by (blast_tac (claset() addIs [constrains_weaken_L]) 1); -qed "constrains_imp_Constrains"; - -Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A"; -by (etac constrains_imp_Constrains 1); -qed "stable_imp_Stable"; - -val prems = Goal - "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ -\ ==> F : A Co A'"; -by (rtac constrains_imp_Constrains 1); -by (blast_tac (claset() addIs (constrainsI::prems)) 1); -qed "ConstrainsI"; - -Goalw [Constrains_def, constrains_def] "F : {} Co B"; -by (Blast_tac 1); -qed "Constrains_empty"; - -Goal "F : A Co UNIV"; -by (blast_tac (claset() addIs [ConstrainsI]) 1); -qed "Constrains_UNIV"; -AddIffs [Constrains_empty, Constrains_UNIV]; - -Goalw [Constrains_def] - "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"; -by (blast_tac (claset() addIs [constrains_weaken_R]) 1); -qed "Constrains_weaken_R"; - -Goalw [Constrains_def] - "[| F : A Co A'; B<=A |] ==> F : B Co A'"; -by (blast_tac (claset() addIs [constrains_weaken_L]) 1); -qed "Constrains_weaken_L"; - -Goalw [Constrains_def] - "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"; -by (blast_tac (claset() addIs [constrains_weaken]) 1); -qed "Constrains_weaken"; - -(** Union **) - -Goalw [Constrains_def] - "[| F : A Co A'; F : B Co B' |] \ -\ ==> F : (A Un B) Co (A' Un B')"; -by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1); -qed "Constrains_Un"; - -val [prem] = Goalw [Constrains_def] - "(!!i. i:I ==> F : (A i) Co (A' i)) \ -\ ==> F : (UN i:I. A i) Co (UN i:I. A' i)"; -by (rtac CollectI 1); -by (rtac (prem RS CollectD RS constrains_UN RS constrains_weaken) 1); -by Auto_tac; -qed "Constrains_UN"; - -(** Intersection **) - -Goalw [Constrains_def] - "[| F : A Co A'; F : B Co B' |] \ -\ ==> F : (A Int B) Co (A' Int B')"; -by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1); -qed "Constrains_Int"; - -val [prem] = Goalw [Constrains_def] - "(!!i. i:I ==> F : (A i) Co (A' i)) \ -\ ==> F : (INT i:I. A i) Co (INT i:I. A' i)"; -by (rtac CollectI 1); -by (rtac (prem RS CollectD RS constrains_INT RS constrains_weaken) 1); -by Auto_tac; -qed "Constrains_INT"; - -Goal "F : A Co A' ==> reachable F Int A <= A'"; -by (asm_full_simp_tac (simpset() addsimps [constrains_imp_subset, - Constrains_def]) 1); -qed "Constrains_imp_subset"; - -Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C"; -by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); -by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); -qed "Constrains_trans"; - -Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"; -by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains, - constrains_def]) 1); -by (Blast_tac 1); -qed "Constrains_cancel"; - - -(*** Stable ***) - -(*Useful because there's no Stable_weaken. [Tanja Vos]*) -Goal "[| F: Stable A; A = B |] ==> F : Stable B"; -by (Blast_tac 1); -qed "Stable_eq"; - -Goal "(F : Stable A) = (F : stable (reachable F Int A))"; -by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains, - stable_def]) 1); -qed "Stable_eq_stable"; - -Goalw [Stable_def] "F : A Co A ==> F : Stable A"; -by (assume_tac 1); -qed "StableI"; - -Goalw [Stable_def] "F : Stable A ==> F : A Co A"; -by (assume_tac 1); -qed "StableD"; - -Goalw [Stable_def] - "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"; -by (blast_tac (claset() addIs [Constrains_Un]) 1); -qed "Stable_Un"; - -Goalw [Stable_def] - "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"; -by (blast_tac (claset() addIs [Constrains_Int]) 1); -qed "Stable_Int"; - -Goalw [Stable_def] - "[| F : Stable C; F : A Co (C Un A') |] \ -\ ==> F : (C Un A) Co (C Un A')"; -by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1); -qed "Stable_Constrains_Un"; - -Goalw [Stable_def] - "[| F : Stable C; F : (C Int A) Co A' |] \ -\ ==> F : (C Int A) Co (C Int A')"; -by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1); -qed "Stable_Constrains_Int"; - -val [prem] = Goalw [Stable_def] - "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)"; -by (rtac (prem RS Constrains_UN) 1); -by (assume_tac 1); -qed "Stable_UN"; - -val [prem] = Goalw [Stable_def] - "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)"; -by (rtac (prem RS Constrains_INT) 1); -by (assume_tac 1); -qed "Stable_INT"; - -Goal "F : Stable (reachable F)"; -by (simp_tac (simpset() addsimps [Stable_eq_stable]) 1); -qed "Stable_reachable"; - - - -(*** Increasing ***) - -Goalw [Increasing_def] - "F : Increasing f ==> F : Stable {s. x <= f s}"; -by (Blast_tac 1); -qed "IncreasingD"; - -Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def] - "mono g ==> Increasing f <= Increasing (g o f)"; -by Auto_tac; -by (blast_tac (claset() addIs [monoD, order_trans]) 1); -qed "mono_Increasing_o"; - -Goalw [Increasing_def] - "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"; -by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); -by (Blast_tac 1); -qed "strict_IncreasingD"; - -Goalw [increasing_def, Increasing_def] - "F : increasing f ==> F : Increasing f"; -by (blast_tac (claset() addIs [stable_imp_Stable]) 1); -qed "increasing_imp_Increasing"; - -bind_thm ("Increasing_constant", - increasing_constant RS increasing_imp_Increasing); -AddIffs [Increasing_constant]; - - -(*** The Elimination Theorem. The "free" m has become universally quantified! - Should the premise be !!m instead of ALL m ? Would make it harder to use - in forward proof. ***) - -Goalw [Constrains_def, constrains_def] - "[| ALL m. F : {s. s x = m} Co (B m) |] \ -\ ==> F : {s. s x : M} Co (UN m:M. B m)"; -by (Blast_tac 1); -qed "Elimination"; - -(*As above, but for the trivial case of a one-variable state, in which the - state is identified with its one variable.*) -Goalw [Constrains_def, constrains_def] - "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"; -by (Blast_tac 1); -qed "Elimination_sing"; - - -(*** Specialized laws for handling Always ***) - -(** Natural deduction rules for "Always A" **) - -Goal "[| Init F<=A; F : Stable A |] ==> F : Always A"; -by (asm_simp_tac (simpset() addsimps [Always_def]) 1); -qed "AlwaysI"; - -Goal "F : Always A ==> Init F<=A & F : Stable A"; -by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1); -qed "AlwaysD"; - -bind_thm ("AlwaysE", AlwaysD RS conjE); -bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2); - - -(*The set of all reachable states is Always*) -Goal "F : Always A ==> reachable F <= A"; -by (full_simp_tac - (simpset() addsimps [Stable_def, Constrains_def, constrains_def, - Always_def]) 1); -by (rtac subsetI 1); -by (etac reachable.induct 1); -by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); -qed "Always_includes_reachable"; - -Goalw [Always_def, invariant_def, Stable_def, stable_def] - "F : invariant A ==> F : Always A"; -by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1); -qed "invariant_imp_Always"; - -bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always); - -Goal "Always A = {F. F : invariant (reachable F Int A)}"; -by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, - Constrains_eq_constrains, stable_def]) 1); -by (blast_tac (claset() addIs reachable.intrs) 1); -qed "Always_eq_invariant_reachable"; - -(*the RHS is the traditional definition of the "always" operator*) -Goal "Always A = {F. reachable F <= A}"; -by (auto_tac (claset() addDs [invariant_includes_reachable], - simpset() addsimps [Int_absorb2, invariant_reachable, - Always_eq_invariant_reachable])); -qed "Always_eq_includes_reachable"; - -Goal "Always UNIV = UNIV"; -by (auto_tac (claset(), - simpset() addsimps [Always_eq_includes_reachable])); -qed "Always_UNIV_eq"; -Addsimps [Always_UNIV_eq]; - -Goal "UNIV <= A ==> F : Always A"; -by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); -qed "UNIV_AlwaysI"; - -Goal "Always A = (UN I: Pow A. invariant I)"; -by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); -by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, - impOfSubs invariant_includes_reachable]) 1); -qed "Always_eq_UN_invariant"; - -Goal "[| F : Always A; A <= B |] ==> F : Always B"; -by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); -qed "Always_weaken"; - - -(*** "Co" rules involving Always ***) - -Goal "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"; -by (asm_simp_tac - (simpset() addsimps [Always_includes_reachable RS Int_absorb2, - Constrains_def, Int_assoc RS sym]) 1); -qed "Always_Constrains_pre"; - -Goal "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"; -by (asm_simp_tac - (simpset() addsimps [Always_includes_reachable RS Int_absorb2, - Constrains_eq_constrains, Int_assoc RS sym]) 1); -qed "Always_Constrains_post"; - -(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *) -bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1); - -(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *) -bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2); - -(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) -Goal "[| F : Always C; F : A Co A'; \ -\ C Int B <= A; C Int A' <= B' |] \ -\ ==> F : B Co B'"; -by (rtac Always_ConstrainsI 1); -by (assume_tac 1); -by (dtac Always_ConstrainsD 1); -by (assume_tac 1); -by (blast_tac (claset() addIs [Constrains_weaken]) 1); -qed "Always_Constrains_weaken"; - - -(** Conjoining Always properties **) - -Goal "Always (A Int B) = Always A Int Always B"; -by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); -qed "Always_Int_distrib"; - -Goal "Always (INTER I A) = (INT i:I. Always (A i))"; -by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); -qed "Always_INT_distrib"; - -Goal "[| F : Always A; F : Always B |] ==> F : Always (A Int B)"; -by (asm_simp_tac (simpset() addsimps [Always_Int_distrib]) 1); -qed "Always_Int_I"; - -(*Allows a kind of "implication introduction"*) -Goal "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)"; -by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); -qed "Always_Compl_Un_eq"; - -(*Delete the nearest invariance assumption (which will be the second one - used by Always_Int_I) *) -val Always_thin = - read_instantiate_sg (sign_of thy) - [("V", "?F : Always ?A")] thin_rl; - -(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) -val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin; - -(*Combines a list of invariance THEOREMS into one.*) -val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I); - - -(*To allow expansion of the program's definition when appropriate*) -val program_defs_ref = ref ([] : thm list); - -(*proves "co" properties when the program is specified*) -fun constrains_tac i = - SELECT_GOAL - (EVERY [REPEAT (Always_Int_tac 1), - REPEAT (etac Always_ConstrainsI 1 - ORELSE - resolve_tac [StableI, stableI, - constrains_imp_Constrains] 1), - rtac constrainsI 1, - full_simp_tac (simpset() addsimps !program_defs_ref) 1, - REPEAT (FIRSTGOAL (etac disjE)), - ALLGOALS Clarify_tac, - ALLGOALS Asm_lr_simp_tac]) i; - - -(*For proving invariants*) -fun always_tac i = - rtac AlwaysI i THEN Force_tac i THEN constrains_tac i; diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/Constrains.thy --- a/src/HOL/UNITY/Constrains.thy Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/Constrains.thy Thu Jan 30 18:08:09 2003 +0100 @@ -3,10 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Safety relations: restricted to the set of reachable states. +Weak safety relations: restricted to the set of reachable states. *) -Constrains = UNITY + +theory Constrains = UNITY: consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" @@ -14,36 +14,30 @@ Arguments MUST be curried in an inductive definition*) inductive "traces init acts" - intrs + intros (*Initial trace is empty*) - Init "s: init ==> (s,[]) : traces init acts" + Init: "s: init ==> (s,[]) : traces init acts" - Acts "[| act: acts; (s,evs) : traces init acts; (s,s'): act |] - ==> (s', s#evs) : traces init acts" + Acts: "[| act: acts; (s,evs) : traces init acts; (s,s'): act |] + ==> (s', s#evs) : traces init acts" consts reachable :: "'a program => 'a set" inductive "reachable F" - intrs - Init "s: Init F ==> s : reachable F" - - Acts "[| act: Acts F; s : reachable F; (s,s'): act |] - ==> s' : reachable F" + intros + Init: "s: Init F ==> s : reachable F" -consts - Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) - op_Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) + Acts: "[| act: Acts F; s : reachable F; (s,s'): act |] + ==> s' : reachable F" -defs - Constrains_def +constdefs + Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) "A Co B == {F. F : (reachable F Int A) co B}" - Unless_def + Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) "A Unless B == (A-B) Co (A Un B)" -constdefs - Stable :: "'a set => 'a program set" "Stable A == A Co A" @@ -55,4 +49,345 @@ Increasing :: "['a => 'b::{order}] => 'a program set" "Increasing f == INT z. Stable {s. z <= f s}" + +(*** traces and reachable ***) + +lemma reachable_equiv_traces: + "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}" +apply safe +apply (erule_tac [2] traces.induct) +apply (erule reachable.induct) +apply (blast intro: reachable.intros traces.intros)+ +done + +lemma Init_subset_reachable: "Init F <= reachable F" +by (blast intro: reachable.intros) + +lemma stable_reachable [intro!,simp]: + "Acts G <= Acts F ==> G : stable (reachable F)" +by (blast intro: stableI constrainsI reachable.intros) + +(*The set of all reachable states is an invariant...*) +lemma invariant_reachable: "F : invariant (reachable F)" +apply (simp add: invariant_def) +apply (blast intro: reachable.intros) +done + +(*...in fact the strongest invariant!*) +lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A" +apply (simp add: stable_def constrains_def invariant_def) +apply (rule subsetI) +apply (erule reachable.induct) +apply (blast intro: reachable.intros)+ +done + + +(*** Co ***) + +(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) +lemmas constrains_reachable_Int = + subset_refl [THEN stable_reachable [unfolded stable_def], + THEN constrains_Int, standard] + +(*Resembles the previous definition of Constrains*) +lemma Constrains_eq_constrains: + "A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}" +apply (unfold Constrains_def) +apply (blast dest: constrains_reachable_Int intro: constrains_weaken) +done + +lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'" +apply (unfold Constrains_def) +apply (blast intro: constrains_weaken_L) +done + +lemma stable_imp_Stable: "F : stable A ==> F : Stable A" +apply (unfold stable_def Stable_def) +apply (erule constrains_imp_Constrains) +done + +lemma ConstrainsI: + "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') + ==> F : A Co A'" +apply (rule constrains_imp_Constrains) +apply (blast intro: constrainsI) +done + +lemma Constrains_empty [iff]: "F : {} Co B" +by (unfold Constrains_def constrains_def, blast) + +lemma Constrains_UNIV [iff]: "F : A Co UNIV" +by (blast intro: ConstrainsI) + +lemma Constrains_weaken_R: + "[| F : A Co A'; A'<=B' |] ==> F : A Co B'" +apply (unfold Constrains_def) +apply (blast intro: constrains_weaken_R) +done + +lemma Constrains_weaken_L: + "[| F : A Co A'; B<=A |] ==> F : B Co A'" +apply (unfold Constrains_def) +apply (blast intro: constrains_weaken_L) +done + +lemma Constrains_weaken: + "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'" +apply (unfold Constrains_def) +apply (blast intro: constrains_weaken) +done + +(** Union **) + +lemma Constrains_Un: + "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')" +apply (unfold Constrains_def) +apply (blast intro: constrains_Un [THEN constrains_weaken]) +done + +lemma Constrains_UN: + assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)" + shows "F : (UN i:I. A i) Co (UN i:I. A' i)" +apply (unfold Constrains_def) +apply (rule CollectI) +apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, + THEN constrains_weaken], auto) +done + +(** Intersection **) + +lemma Constrains_Int: + "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')" +apply (unfold Constrains_def) +apply (blast intro: constrains_Int [THEN constrains_weaken]) +done + +lemma Constrains_INT: + assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)" + shows "F : (INT i:I. A i) Co (INT i:I. A' i)" +apply (unfold Constrains_def) +apply (rule CollectI) +apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, + THEN constrains_weaken], auto) +done + +lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'" +by (simp add: constrains_imp_subset Constrains_def) + +lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C" +apply (simp add: Constrains_eq_constrains) +apply (blast intro: constrains_trans constrains_weaken) +done + +lemma Constrains_cancel: + "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')" +by (simp add: Constrains_eq_constrains constrains_def, blast) + + +(*** Stable ***) + +(*Useful because there's no Stable_weaken. [Tanja Vos]*) +lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B" +by blast + +lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))" +by (simp add: Stable_def Constrains_eq_constrains stable_def) + +lemma StableI: "F : A Co A ==> F : Stable A" +by (unfold Stable_def, assumption) + +lemma StableD: "F : Stable A ==> F : A Co A" +by (unfold Stable_def, assumption) + +lemma Stable_Un: + "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')" +apply (unfold Stable_def) +apply (blast intro: Constrains_Un) +done + +lemma Stable_Int: + "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')" +apply (unfold Stable_def) +apply (blast intro: Constrains_Int) +done + +lemma Stable_Constrains_Un: + "[| F : Stable C; F : A Co (C Un A') |] + ==> F : (C Un A) Co (C Un A')" +apply (unfold Stable_def) +apply (blast intro: Constrains_Un [THEN Constrains_weaken]) +done + +lemma Stable_Constrains_Int: + "[| F : Stable C; F : (C Int A) Co A' |] + ==> F : (C Int A) Co (C Int A')" +apply (unfold Stable_def) +apply (blast intro: Constrains_Int [THEN Constrains_weaken]) +done + +lemma Stable_UN: + "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)" +by (simp add: Stable_def Constrains_UN) + +lemma Stable_INT: + "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)" +by (simp add: Stable_def Constrains_INT) + +lemma Stable_reachable: "F : Stable (reachable F)" +by (simp add: Stable_eq_stable) + + + +(*** Increasing ***) + +lemma IncreasingD: + "F : Increasing f ==> F : Stable {s. x <= f s}" +by (unfold Increasing_def, blast) + +lemma mono_Increasing_o: + "mono g ==> Increasing f <= Increasing (g o f)" +apply (simp add: Increasing_def Stable_def Constrains_def stable_def + constrains_def) +apply (blast intro: monoD order_trans) +done + +lemma strict_IncreasingD: + "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}" +by (simp add: Increasing_def Suc_le_eq [symmetric]) + +lemma increasing_imp_Increasing: + "F : increasing f ==> F : Increasing f" +apply (unfold increasing_def Increasing_def) +apply (blast intro: stable_imp_Stable) +done + +lemmas Increasing_constant = + increasing_constant [THEN increasing_imp_Increasing, standard, iff] + + +(*** The Elimination Theorem. The "free" m has become universally quantified! + Should the premise be !!m instead of ALL m ? Would make it harder to use + in forward proof. ***) + +lemma Elimination: + "[| ALL m. F : {s. s x = m} Co (B m) |] + ==> F : {s. s x : M} Co (UN m:M. B m)" + +by (unfold Constrains_def constrains_def, blast) + +(*As above, but for the trivial case of a one-variable state, in which the + state is identified with its one variable.*) +lemma Elimination_sing: + "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)" +by (unfold Constrains_def constrains_def, blast) + + +(*** Specialized laws for handling Always ***) + +(** Natural deduction rules for "Always A" **) + +lemma AlwaysI: "[| Init F<=A; F : Stable A |] ==> F : Always A" +by (simp add: Always_def) + +lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A" +by (simp add: Always_def) + +lemmas AlwaysE = AlwaysD [THEN conjE, standard] +lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard] + + +(*The set of all reachable states is Always*) +lemma Always_includes_reachable: "F : Always A ==> reachable F <= A" +apply (simp add: Stable_def Constrains_def constrains_def Always_def) +apply (rule subsetI) +apply (erule reachable.induct) +apply (blast intro: reachable.intros)+ +done + +lemma invariant_imp_Always: + "F : invariant A ==> F : Always A" +apply (unfold Always_def invariant_def Stable_def stable_def) +apply (blast intro: constrains_imp_Constrains) +done + +lemmas Always_reachable = + invariant_reachable [THEN invariant_imp_Always, standard] + +lemma Always_eq_invariant_reachable: + "Always A = {F. F : invariant (reachable F Int A)}" +apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains + stable_def) +apply (blast intro: reachable.intros) +done + +(*the RHS is the traditional definition of the "always" operator*) +lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}" +by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable) + +lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV" +by (auto simp add: Always_eq_includes_reachable) + +lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A" +by (auto simp add: Always_eq_includes_reachable) + +lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)" +apply (simp add: Always_eq_includes_reachable) +apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] + invariant_includes_reachable [THEN subsetD]) +done + +lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B" +by (auto simp add: Always_eq_includes_reachable) + + +(*** "Co" rules involving Always ***) + +lemma Always_Constrains_pre: + "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')" +by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def + Int_assoc [symmetric]) + +lemma Always_Constrains_post: + "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')" +by (simp add: Always_includes_reachable [THEN Int_absorb2] + Constrains_eq_constrains Int_assoc [symmetric]) + +(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *) +lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard] + +(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *) +lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard] + +(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) +lemma Always_Constrains_weaken: + "[| F : Always C; F : A Co A'; + C Int B <= A; C Int A' <= B' |] + ==> F : B Co B'" +apply (rule Always_ConstrainsI, assumption) +apply (drule Always_ConstrainsD, assumption) +apply (blast intro: Constrains_weaken) +done + + +(** Conjoining Always properties **) + +lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B" +by (auto simp add: Always_eq_includes_reachable) + +lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))" +by (auto simp add: Always_eq_includes_reachable) + +lemma Always_Int_I: + "[| F : Always A; F : Always B |] ==> F : Always (A Int B)" +by (simp add: Always_Int_distrib) + +(*Allows a kind of "implication introduction"*) +lemma Always_Compl_Un_eq: + "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)" +by (auto simp add: Always_eq_includes_reachable) + +(*Delete the nearest invariance assumption (which will be the second one + used by Always_Int_I) *) +lemmas Always_thin = thin_rl [of "F : Always A", standard] + end diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/Simple/NSP_Bad.ML --- a/src/HOL/UNITY/Simple/NSP_Bad.ML Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.ML Thu Jan 30 18:08:09 2003 +0100 @@ -31,10 +31,10 @@ Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \ \ Says A B (Crypt (pubK B) (Nonce NB)) : set s"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (res_inst_tac [("act", "NS3")] reachable.Acts 2); -by (res_inst_tac [("act", "NS2")] reachable.Acts 3); -by (res_inst_tac [("act", "NS1")] reachable.Acts 4); -by (rtac reachable.Init 5); +by (res_inst_tac [("act", "NS3")] reachable_Acts 2); +by (res_inst_tac [("act", "NS2")] reachable_Acts 3); +by (res_inst_tac [("act", "NS1")] reachable_Acts 4); +by (rtac reachable_Init 5); by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def]))); by (REPEAT_FIRST (rtac exI )); by possibility_tac; diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jan 30 18:08:09 2003 +0100 @@ -10,7 +10,7 @@ Original file is ../Auth/NS_Public_Bad *) -NSP_Bad = Public + Constrains + +NSP_Bad = Public + UNITY_Main + types state = event list diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Thu Jan 30 10:35:56 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,394 +0,0 @@ -(* Title: HOL/UNITY/UNITY - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -The basic UNITY theory (revised version, based upon the "co" operator) - -From Misra, "A Logic for Concurrent Programming", 1994 -*) - -(*Perhaps equalities.ML shouldn't add this in the first place!*) -Delsimps [image_Collect]; - -(*** The abstract type of programs ***) - -val rep_ss = simpset() addsimps - [Init_def, Acts_def, AllowedActs_def, - mk_program_def, Program_def, Rep_Program, - Rep_Program_inverse, Abs_Program_inverse]; - - -Goal "Id : Acts F"; -by (cut_inst_tac [("x", "F")] Rep_Program 1); -by (auto_tac (claset(), rep_ss)); -qed "Id_in_Acts"; -AddIffs [Id_in_Acts]; - -Goal "insert Id (Acts F) = Acts F"; -by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1); -qed "insert_Id_Acts"; -AddIffs [insert_Id_Acts]; - -Goal "Id : AllowedActs F"; -by (cut_inst_tac [("x", "F")] Rep_Program 1); -by (auto_tac (claset(), rep_ss)); -qed "Id_in_AllowedActs"; -AddIffs [Id_in_AllowedActs]; - -Goal "insert Id (AllowedActs F) = AllowedActs F"; -by (simp_tac (simpset() addsimps [insert_absorb, Id_in_AllowedActs]) 1); -qed "insert_Id_AllowedActs"; -AddIffs [insert_Id_AllowedActs]; - -(** Inspectors for type "program" **) - -Goal "Init (mk_program (init,acts,allowed)) = init"; -by (auto_tac (claset(), rep_ss)); -qed "Init_eq"; - -Goal "Acts (mk_program (init,acts,allowed)) = insert Id acts"; -by (auto_tac (claset(), rep_ss)); -qed "Acts_eq"; - -Goal "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"; -by (auto_tac (claset(), rep_ss)); -qed "AllowedActs_eq"; - -Addsimps [Init_eq, Acts_eq, AllowedActs_eq]; - -(** Equality for UNITY programs **) - -Goal "mk_program (Init F, Acts F, AllowedActs F) = F"; -by (cut_inst_tac [("x", "F")] Rep_Program 1); -by (auto_tac (claset(), rep_ss)); -by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1)); -by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1); -qed "surjective_mk_program"; - -Goal "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] \ -\ ==> F = G"; -by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1); -by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1); -by (Asm_simp_tac 1); -qed "program_equalityI"; - -val [major,minor] = -Goal "[| F = G; \ -\ [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]\ -\ ==> P |] ==> P"; -by (rtac minor 1); -by (auto_tac (claset(), simpset() addsimps [major])); -qed "program_equalityE"; - -Goal "(F=G) = \ -\ (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"; -by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1); -qed "program_equality_iff"; - -Addsimps [surjective_mk_program]; - - -(*** These rules allow "lazy" definition expansion - They avoid expanding the full program, which is a large expression -***) - -Goal "F == mk_program (init,acts,allowed) ==> Init F = init"; -by Auto_tac; -qed "def_prg_Init"; - -Goal "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"; -by Auto_tac; -qed "def_prg_Acts"; - -Goal "F == mk_program (init,acts,allowed) \ -\ ==> AllowedActs F = insert Id allowed"; -by Auto_tac; -qed "def_prg_AllowedActs"; - -(*The program is not expanded, but its Init and Acts are*) -val [rew] = goal thy - "[| F == mk_program (init,acts,allowed) |] \ -\ ==> Init F = init & Acts F = insert Id acts"; -by (rewtac rew); -by Auto_tac; -qed "def_prg_simps"; - -(*An action is expanded only if a pair of states is being tested against it*) -Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; -by Auto_tac; -qed "def_act_simp"; - -fun simp_of_act def = def RS def_act_simp; - -(*A set is expanded only if an element is being tested against it*) -Goal "A == B ==> (x : A) = (x : B)"; -by Auto_tac; -qed "def_set_simp"; - -fun simp_of_set def = def RS def_set_simp; - - -(*** co ***) - -val prems = Goalw [constrains_def] - "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ -\ ==> F : A co A'"; -by (blast_tac (claset() addIs prems) 1); -qed "constrainsI"; - -Goalw [constrains_def] - "[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'"; -by (Blast_tac 1); -qed "constrainsD"; - -Goalw [constrains_def] "F : {} co B"; -by (Blast_tac 1); -qed "constrains_empty"; - -Goalw [constrains_def] "(F : A co {}) = (A={})"; -by (Blast_tac 1); -qed "constrains_empty2"; - -Goalw [constrains_def] "(F : UNIV co B) = (B = UNIV)"; -by (Blast_tac 1); -qed "constrains_UNIV"; - -Goalw [constrains_def] "F : A co UNIV"; -by (Blast_tac 1); -qed "constrains_UNIV2"; - -AddIffs [constrains_empty, constrains_empty2, - constrains_UNIV, constrains_UNIV2]; - -(*monotonic in 2nd argument*) -Goalw [constrains_def] - "[| F : A co A'; A'<=B' |] ==> F : A co B'"; -by (Blast_tac 1); -qed "constrains_weaken_R"; - -(*anti-monotonic in 1st argument*) -Goalw [constrains_def] - "[| F : A co A'; B<=A |] ==> F : B co A'"; -by (Blast_tac 1); -qed "constrains_weaken_L"; - -Goalw [constrains_def] - "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"; -by (Blast_tac 1); -qed "constrains_weaken"; - -(** Union **) - -Goalw [constrains_def] - "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"; -by (Blast_tac 1); -qed "constrains_Un"; - -Goalw [constrains_def] - "ALL i:I. F : (A i) co (A' i) ==> F : (UN i:I. A i) co (UN i:I. A' i)"; -by (Blast_tac 1); -bind_thm ("constrains_UN", ballI RS result()); - -Goalw [constrains_def] "(A Un B) co C = (A co C) Int (B co C)"; -by (Blast_tac 1); -qed "constrains_Un_distrib"; - -Goalw [constrains_def] "(UN i:I. A i) co B = (INT i:I. A i co B)"; -by (Blast_tac 1); -qed "constrains_UN_distrib"; - -Goalw [constrains_def] "C co (A Int B) = (C co A) Int (C co B)"; -by (Blast_tac 1); -qed "constrains_Int_distrib"; - -Goalw [constrains_def] "A co (INT i:I. B i) = (INT i:I. A co B i)"; -by (Blast_tac 1); -qed "constrains_INT_distrib"; - -(** Intersection **) - -Goalw [constrains_def] - "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"; -by (Blast_tac 1); -qed "constrains_Int"; - -Goalw [constrains_def] - "ALL i:I. F : (A i) co (A' i) ==> F : (INT i:I. A i) co (INT i:I. A' i)"; -by (Blast_tac 1); -bind_thm ("constrains_INT", ballI RS result()); - -Goalw [constrains_def] "F : A co A' ==> A <= A'"; -by Auto_tac; -qed "constrains_imp_subset"; - -(*The reasoning is by subsets since "co" refers to single actions - only. So this rule isn't that useful.*) -Goalw [constrains_def] - "[| F : A co B; F : B co C |] ==> F : A co C"; -by (Blast_tac 1); -qed "constrains_trans"; - -Goalw [constrains_def] - "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"; -by (Clarify_tac 1); -by (Blast_tac 1); -qed "constrains_cancel"; - - -(*** unless ***) - -Goalw [unless_def] "F : (A-B) co (A Un B) ==> F : A unless B"; -by (assume_tac 1); -qed "unlessI"; - -Goalw [unless_def] "F : A unless B ==> F : (A-B) co (A Un B)"; -by (assume_tac 1); -qed "unlessD"; - - -(*** stable ***) - -Goalw [stable_def] "F : A co A ==> F : stable A"; -by (assume_tac 1); -qed "stableI"; - -Goalw [stable_def] "F : stable A ==> F : A co A"; -by (assume_tac 1); -qed "stableD"; - -Goalw [stable_def, constrains_def] "stable UNIV = UNIV"; -by Auto_tac; -qed "stable_UNIV"; -Addsimps [stable_UNIV]; - -(** Union **) - -Goalw [stable_def] - "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"; -by (blast_tac (claset() addIs [constrains_Un]) 1); -qed "stable_Un"; - -Goalw [stable_def] - "ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)"; -by (blast_tac (claset() addIs [constrains_UN]) 1); -bind_thm ("stable_UN", ballI RS result()); - -(** Intersection **) - -Goalw [stable_def] - "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')"; -by (blast_tac (claset() addIs [constrains_Int]) 1); -qed "stable_Int"; - -Goalw [stable_def] - "ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)"; -by (blast_tac (claset() addIs [constrains_INT]) 1); -bind_thm ("stable_INT", ballI RS result()); - -Goalw [stable_def, constrains_def] - "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"; -by (Blast_tac 1); -qed "stable_constrains_Un"; - -Goalw [stable_def, constrains_def] - "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"; -by (Blast_tac 1); -qed "stable_constrains_Int"; - -(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *) -bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); - - -(*** invariant ***) - -Goal "[| Init F<=A; F: stable A |] ==> F : invariant A"; -by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); -qed "invariantI"; - -(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) -Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)"; -by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int])); -qed "invariant_Int"; - - -(*** increasing ***) - -Goalw [increasing_def] - "F : increasing f ==> F : stable {s. z <= f s}"; -by (Blast_tac 1); -qed "increasingD"; - -Goalw [increasing_def, stable_def] "F : increasing (%s. c)"; -by Auto_tac; -qed "increasing_constant"; -AddIffs [increasing_constant]; - -Goalw [increasing_def, stable_def, constrains_def] - "mono g ==> increasing f <= increasing (g o f)"; -by Auto_tac; -by (blast_tac (claset() addIs [monoD, order_trans]) 1); -qed "mono_increasing_o"; - -(*Holds by the theorem (Suc m <= n) = (m < n) *) -Goalw [increasing_def] - "!!z::nat. F : increasing f ==> F: stable {s. z < f s}"; -by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); -by (Blast_tac 1); -qed "strict_increasingD"; - - -(** The Elimination Theorem. The "free" m has become universally quantified! - Should the premise be !!m instead of ALL m ? Would make it harder to use - in forward proof. **) - -Goalw [constrains_def] - "[| ALL m:M. F : {s. s x = m} co (B m) |] \ -\ ==> F : {s. s x : M} co (UN m:M. B m)"; -by (Blast_tac 1); -qed "elimination"; - -(*As above, but for the trivial case of a one-variable state, in which the - state is identified with its one variable.*) -Goalw [constrains_def] - "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"; -by (Blast_tac 1); -qed "elimination_sing"; - - - -(*** Theoretical Results from Section 6 ***) - -Goalw [constrains_def, strongest_rhs_def] - "F : A co (strongest_rhs F A )"; -by (Blast_tac 1); -qed "constrains_strongest_rhs"; - -Goalw [constrains_def, strongest_rhs_def] - "F : A co B ==> strongest_rhs F A <= B"; -by (Blast_tac 1); -qed "strongest_rhs_is_strongest"; - - -(** Ad-hoc set-theory rules **) - -Goal "A Un B - (A - B) = B"; -by (Blast_tac 1); -qed "Un_Diff_Diff"; -Addsimps [Un_Diff_Diff]; - -Goal "Union(B) Int A = Union((%C. C Int A)`B)"; -by (Blast_tac 1); -qed "Int_Union_Union"; - -(** Needed for WF reasoning in WFair.ML **) - -Goal "less_than `` {k} = greaterThan k"; -by (Blast_tac 1); -qed "Image_less_than"; - -Goal "less_than^-1 `` {k} = lessThan k"; -by (Blast_tac 1); -qed "Image_inverse_less_than"; - -Addsimps [Image_less_than, Image_inverse_less_than]; diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/UNITY.thy Thu Jan 30 18:08:09 2003 +0100 @@ -8,18 +8,21 @@ From Misra, "A Logic for Concurrent Programming", 1994 *) -UNITY = Main + +theory UNITY = Main: typedef (Program) 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set, - allowed :: ('a * 'a)set set). Id:acts & Id: allowed}" - -consts - constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60) - op_unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60) + allowed :: ('a * 'a)set set). Id:acts & Id: allowed}" + by blast constdefs - mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set) + constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60) + "A co B == {F. ALL act: Acts F. act``A <= B}" + + unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60) + "A unless B == (A-B) co (A Un B)" + + mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set) => 'a program" "mk_program == %(init, acts, allowed). Abs_Program (init, insert Id acts, insert Id allowed)" @@ -50,9 +53,325 @@ "increasing f == INT z. stable {s. z <= f s}" -defs - constrains_def "A co B == {F. ALL act: Acts F. act``A <= B}" +(*Perhaps equalities.ML shouldn't add this in the first place!*) +declare image_Collect [simp del] + +(*** The abstract type of programs ***) + +lemmas program_typedef = + Rep_Program Rep_Program_inverse Abs_Program_inverse + Program_def Init_def Acts_def AllowedActs_def mk_program_def + +lemma Id_in_Acts [iff]: "Id : Acts F" +apply (cut_tac x = F in Rep_Program) +apply (auto simp add: program_typedef) +done + +lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F" +by (simp add: insert_absorb Id_in_Acts) + +lemma Id_in_AllowedActs [iff]: "Id : AllowedActs F" +apply (cut_tac x = F in Rep_Program) +apply (auto simp add: program_typedef) +done + +lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F" +by (simp add: insert_absorb Id_in_AllowedActs) + +(** Inspectors for type "program" **) + +lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init" +by (auto simp add: program_typedef) + +lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts" +by (auto simp add: program_typedef) + +lemma AllowedActs_eq [simp]: + "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed" +by (auto simp add: program_typedef) + +(** Equality for UNITY programs **) + +lemma surjective_mk_program [simp]: + "mk_program (Init F, Acts F, AllowedActs F) = F" +apply (cut_tac x = F in Rep_Program) +apply (auto simp add: program_typedef) +apply (drule_tac f = Abs_Program in arg_cong)+ +apply (simp add: program_typedef insert_absorb) +done + +lemma program_equalityI: + "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] + ==> F = G" +apply (rule_tac t = F in surjective_mk_program [THEN subst]) +apply (rule_tac t = G in surjective_mk_program [THEN subst], simp) +done + +lemma program_equalityE: + "[| F = G; + [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] + ==> P |] ==> P" +by simp + +lemma program_equality_iff: + "(F=G) = + (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)" +by (blast intro: program_equalityI program_equalityE) + + +(*** These rules allow "lazy" definition expansion + They avoid expanding the full program, which is a large expression +***) + +lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init" +by auto + +lemma def_prg_Acts: + "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts" +by auto + +lemma def_prg_AllowedActs: + "F == mk_program (init,acts,allowed) + ==> AllowedActs F = insert Id allowed" +by auto + +(*The program is not expanded, but its Init and Acts are*) +lemma def_prg_simps: + "[| F == mk_program (init,acts,allowed) |] + ==> Init F = init & Acts F = insert Id acts" +by simp + +(*An action is expanded only if a pair of states is being tested against it*) +lemma def_act_simp: + "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'" +by auto + +(*A set is expanded only if an element is being tested against it*) +lemma def_set_simp: "A == B ==> (x : A) = (x : B)" +by auto + + +(*** co ***) + +lemma constrainsI: + "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') + ==> F : A co A'" +by (simp add: constrains_def, blast) + +lemma constrainsD: + "[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'" +by (unfold constrains_def, blast) + +lemma constrains_empty [iff]: "F : {} co B" +by (unfold constrains_def, blast) + +lemma constrains_empty2 [iff]: "(F : A co {}) = (A={})" +by (unfold constrains_def, blast) + +lemma constrains_UNIV [iff]: "(F : UNIV co B) = (B = UNIV)" +by (unfold constrains_def, blast) + +lemma constrains_UNIV2 [iff]: "F : A co UNIV" +by (unfold constrains_def, blast) + +(*monotonic in 2nd argument*) +lemma constrains_weaken_R: + "[| F : A co A'; A'<=B' |] ==> F : A co B'" +by (unfold constrains_def, blast) + +(*anti-monotonic in 1st argument*) +lemma constrains_weaken_L: + "[| F : A co A'; B<=A |] ==> F : B co A'" +by (unfold constrains_def, blast) + +lemma constrains_weaken: + "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'" +by (unfold constrains_def, blast) + +(** Union **) + +lemma constrains_Un: + "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')" +by (unfold constrains_def, blast) + +lemma constrains_UN: + "(!!i. i:I ==> F : (A i) co (A' i)) + ==> F : (UN i:I. A i) co (UN i:I. A' i)" +by (unfold constrains_def, blast) + +lemma constrains_Un_distrib: "(A Un B) co C = (A co C) Int (B co C)" +by (unfold constrains_def, blast) + +lemma constrains_UN_distrib: "(UN i:I. A i) co B = (INT i:I. A i co B)" +by (unfold constrains_def, blast) + +lemma constrains_Int_distrib: "C co (A Int B) = (C co A) Int (C co B)" +by (unfold constrains_def, blast) + +lemma constrains_INT_distrib: "A co (INT i:I. B i) = (INT i:I. A co B i)" +by (unfold constrains_def, blast) + +(** Intersection **) - unless_def "A unless B == (A-B) co (A Un B)" +lemma constrains_Int: + "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')" +by (unfold constrains_def, blast) + +lemma constrains_INT: + "(!!i. i:I ==> F : (A i) co (A' i)) + ==> F : (INT i:I. A i) co (INT i:I. A' i)" +by (unfold constrains_def, blast) + +lemma constrains_imp_subset: "F : A co A' ==> A <= A'" +by (unfold constrains_def, auto) + +(*The reasoning is by subsets since "co" refers to single actions + only. So this rule isn't that useful.*) +lemma constrains_trans: + "[| F : A co B; F : B co C |] ==> F : A co C" +by (unfold constrains_def, blast) + +lemma constrains_cancel: + "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')" +by (unfold constrains_def, clarify, blast) + + +(*** unless ***) + +lemma unlessI: "F : (A-B) co (A Un B) ==> F : A unless B" +by (unfold unless_def, assumption) + +lemma unlessD: "F : A unless B ==> F : (A-B) co (A Un B)" +by (unfold unless_def, assumption) + + +(*** stable ***) + +lemma stableI: "F : A co A ==> F : stable A" +by (unfold stable_def, assumption) + +lemma stableD: "F : stable A ==> F : A co A" +by (unfold stable_def, assumption) + +lemma stable_UNIV [simp]: "stable UNIV = UNIV" +by (unfold stable_def constrains_def, auto) + +(** Union **) + +lemma stable_Un: + "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')" + +apply (unfold stable_def) +apply (blast intro: constrains_Un) +done + +lemma stable_UN: + "(!!i. i:I ==> F : stable (A i)) ==> F : stable (UN i:I. A i)" +apply (unfold stable_def) +apply (blast intro: constrains_UN) +done + +(** Intersection **) + +lemma stable_Int: + "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')" +apply (unfold stable_def) +apply (blast intro: constrains_Int) +done + +lemma stable_INT: + "(!!i. i:I ==> F : stable (A i)) ==> F : stable (INT i:I. A i)" +apply (unfold stable_def) +apply (blast intro: constrains_INT) +done + +lemma stable_constrains_Un: + "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')" +by (unfold stable_def constrains_def, blast) + +lemma stable_constrains_Int: + "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')" +by (unfold stable_def constrains_def, blast) + +(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *) +lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard] + + +(*** invariant ***) + +lemma invariantI: "[| Init F<=A; F: stable A |] ==> F : invariant A" +by (simp add: invariant_def) + +(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) +lemma invariant_Int: + "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)" +by (auto simp add: invariant_def stable_Int) + + +(*** increasing ***) + +lemma increasingD: + "F : increasing f ==> F : stable {s. z <= f s}" + +by (unfold increasing_def, blast) + +lemma increasing_constant [iff]: "F : increasing (%s. c)" +by (unfold increasing_def stable_def, auto) + +lemma mono_increasing_o: + "mono g ==> increasing f <= increasing (g o f)" +apply (unfold increasing_def stable_def constrains_def, auto) +apply (blast intro: monoD order_trans) +done + +(*Holds by the theorem (Suc m <= n) = (m < n) *) +lemma strict_increasingD: + "!!z::nat. F : increasing f ==> F: stable {s. z < f s}" +by (simp add: increasing_def Suc_le_eq [symmetric]) + + +(** The Elimination Theorem. The "free" m has become universally quantified! + Should the premise be !!m instead of ALL m ? Would make it harder to use + in forward proof. **) + +lemma elimination: + "[| ALL m:M. F : {s. s x = m} co (B m) |] + ==> F : {s. s x : M} co (UN m:M. B m)" +by (unfold constrains_def, blast) + +(*As above, but for the trivial case of a one-variable state, in which the + state is identified with its one variable.*) +lemma elimination_sing: + "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)" +by (unfold constrains_def, blast) + + + +(*** Theoretical Results from Section 6 ***) + +lemma constrains_strongest_rhs: + "F : A co (strongest_rhs F A )" +by (unfold constrains_def strongest_rhs_def, blast) + +lemma strongest_rhs_is_strongest: + "F : A co B ==> strongest_rhs F A <= B" +by (unfold constrains_def strongest_rhs_def, blast) + + +(** Ad-hoc set-theory rules **) + +lemma Un_Diff_Diff [simp]: "A Un B - (A - B) = B" +by blast + +lemma Int_Union_Union: "Union(B) Int A = Union((%C. C Int A)`B)" +by blast + +(** Needed for WF reasoning in WFair.ML **) + +lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k" +by blast + +lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k" +by blast end diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Thu Jan 30 18:08:09 2003 +0100 @@ -6,6 +6,215 @@ Specialized UNITY tactics, and ML bindings of theorems *) +(*UNITY*) +val constrains_def = thm "constrains_def"; +val stable_def = thm "stable_def"; +val invariant_def = thm "invariant_def"; +val increasing_def = thm "increasing_def"; +val Allowed_def = thm "Allowed_def"; +val Id_in_Acts = thm "Id_in_Acts"; +val insert_Id_Acts = thm "insert_Id_Acts"; +val Id_in_AllowedActs = thm "Id_in_AllowedActs"; +val insert_Id_AllowedActs = thm "insert_Id_AllowedActs"; +val Init_eq = thm "Init_eq"; +val Acts_eq = thm "Acts_eq"; +val AllowedActs_eq = thm "AllowedActs_eq"; +val surjective_mk_program = thm "surjective_mk_program"; +val program_equalityI = thm "program_equalityI"; +val program_equalityE = thm "program_equalityE"; +val program_equality_iff = thm "program_equality_iff"; +val def_prg_Init = thm "def_prg_Init"; +val def_prg_Acts = thm "def_prg_Acts"; +val def_prg_AllowedActs = thm "def_prg_AllowedActs"; +val def_prg_simps = thm "def_prg_simps"; +val def_act_simp = thm "def_act_simp"; +val def_set_simp = thm "def_set_simp"; +val constrainsI = thm "constrainsI"; +val constrainsD = thm "constrainsD"; +val constrains_empty = thm "constrains_empty"; +val constrains_empty2 = thm "constrains_empty2"; +val constrains_UNIV = thm "constrains_UNIV"; +val constrains_UNIV2 = thm "constrains_UNIV2"; +val constrains_weaken_R = thm "constrains_weaken_R"; +val constrains_weaken_L = thm "constrains_weaken_L"; +val constrains_weaken = thm "constrains_weaken"; +val constrains_Un = thm "constrains_Un"; +val constrains_UN = thm "constrains_UN"; +val constrains_Un_distrib = thm "constrains_Un_distrib"; +val constrains_UN_distrib = thm "constrains_UN_distrib"; +val constrains_Int_distrib = thm "constrains_Int_distrib"; +val constrains_INT_distrib = thm "constrains_INT_distrib"; +val constrains_Int = thm "constrains_Int"; +val constrains_INT = thm "constrains_INT"; +val constrains_imp_subset = thm "constrains_imp_subset"; +val constrains_trans = thm "constrains_trans"; +val constrains_cancel = thm "constrains_cancel"; +val unlessI = thm "unlessI"; +val unlessD = thm "unlessD"; +val stableI = thm "stableI"; +val stableD = thm "stableD"; +val stable_UNIV = thm "stable_UNIV"; +val stable_Un = thm "stable_Un"; +val stable_UN = thm "stable_UN"; +val stable_Int = thm "stable_Int"; +val stable_INT = thm "stable_INT"; +val stable_constrains_Un = thm "stable_constrains_Un"; +val stable_constrains_Int = thm "stable_constrains_Int"; +val stable_constrains_stable = thm "stable_constrains_stable"; +val invariantI = thm "invariantI"; +val invariant_Int = thm "invariant_Int"; +val increasingD = thm "increasingD"; +val increasing_constant = thm "increasing_constant"; +val mono_increasing_o = thm "mono_increasing_o"; +val strict_increasingD = thm "strict_increasingD"; +val elimination = thm "elimination"; +val elimination_sing = thm "elimination_sing"; +val constrains_strongest_rhs = thm "constrains_strongest_rhs"; +val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest"; +val Un_Diff_Diff = thm "Un_Diff_Diff"; +val Int_Union_Union = thm "Int_Union_Union"; +val Image_less_than = thm "Image_less_than"; +val Image_inverse_less_than = thm "Image_inverse_less_than"; + +(*WFair*) +val stable_transient_empty = thm "stable_transient_empty"; +val transient_strengthen = thm "transient_strengthen"; +val transientI = thm "transientI"; +val transientE = thm "transientE"; +val transient_UNIV = thm "transient_UNIV"; +val transient_empty = thm "transient_empty"; +val ensuresI = thm "ensuresI"; +val ensuresD = thm "ensuresD"; +val ensures_weaken_R = thm "ensures_weaken_R"; +val stable_ensures_Int = thm "stable_ensures_Int"; +val stable_transient_ensures = thm "stable_transient_ensures"; +val ensures_eq = thm "ensures_eq"; +val leadsTo_Basis = thm "leadsTo_Basis"; +val leadsTo_Trans = thm "leadsTo_Trans"; +val transient_imp_leadsTo = thm "transient_imp_leadsTo"; +val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate"; +val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2"; +val leadsTo_Union = thm "leadsTo_Union"; +val leadsTo_Union_Int = thm "leadsTo_Union_Int"; +val leadsTo_UN = thm "leadsTo_UN"; +val leadsTo_Un = thm "leadsTo_Un"; +val single_leadsTo_I = thm "single_leadsTo_I"; +val leadsTo_induct = thm "leadsTo_induct"; +val subset_imp_ensures = thm "subset_imp_ensures"; +val subset_imp_leadsTo = thm "subset_imp_leadsTo"; +val leadsTo_refl = thm "leadsTo_refl"; +val empty_leadsTo = thm "empty_leadsTo"; +val leadsTo_UNIV = thm "leadsTo_UNIV"; +val leadsTo_induct_pre_lemma = thm "leadsTo_induct_pre_lemma"; +val leadsTo_induct_pre = thm "leadsTo_induct_pre"; +val leadsTo_weaken_R = thm "leadsTo_weaken_R"; +val leadsTo_weaken_L = thm "leadsTo_weaken_L"; +val leadsTo_Un_distrib = thm "leadsTo_Un_distrib"; +val leadsTo_UN_distrib = thm "leadsTo_UN_distrib"; +val leadsTo_Union_distrib = thm "leadsTo_Union_distrib"; +val leadsTo_weaken = thm "leadsTo_weaken"; +val leadsTo_Diff = thm "leadsTo_Diff"; +val leadsTo_UN_UN = thm "leadsTo_UN_UN"; +val leadsTo_Un_Un = thm "leadsTo_Un_Un"; +val leadsTo_cancel2 = thm "leadsTo_cancel2"; +val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2"; +val leadsTo_cancel1 = thm "leadsTo_cancel1"; +val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1"; +val leadsTo_empty = thm "leadsTo_empty"; +val psp_stable = thm "psp_stable"; +val psp_stable2 = thm "psp_stable2"; +val psp_ensures = thm "psp_ensures"; +val psp = thm "psp"; +val psp2 = thm "psp2"; +val psp_unless = thm "psp_unless"; +val leadsTo_wf_induct_lemma = thm "leadsTo_wf_induct_lemma"; +val leadsTo_wf_induct = thm "leadsTo_wf_induct"; +val bounded_induct = thm "bounded_induct"; +val lessThan_induct = thm "lessThan_induct"; +val lessThan_bounded_induct = thm "lessThan_bounded_induct"; +val greaterThan_bounded_induct = thm "greaterThan_bounded_induct"; +val wlt_leadsTo = thm "wlt_leadsTo"; +val leadsTo_subset = thm "leadsTo_subset"; +val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt"; +val wlt_increasing = thm "wlt_increasing"; +val lemma1 = thm "lemma1"; +val leadsTo_123 = thm "leadsTo_123"; +val wlt_constrains_wlt = thm "wlt_constrains_wlt"; +val completion_lemma = thm "completion_lemma"; +val completion = thm "completion"; +val finite_completion_lemma = thm "finite_completion_lemma"; +val finite_completion = thm "finite_completion"; +val stable_completion = thm "stable_completion"; +val finite_stable_completion = thm "finite_stable_completion"; + +(*Constrains*) +val Increasing_def = thm "Increasing_def"; +val reachable_Init = thm "reachable.Init"; +val reachable_Acts = thm "reachable.Acts"; +val reachable_equiv_traces = thm "reachable_equiv_traces"; +val Init_subset_reachable = thm "Init_subset_reachable"; +val stable_reachable = thm "stable_reachable"; +val invariant_reachable = thm "invariant_reachable"; +val invariant_includes_reachable = thm "invariant_includes_reachable"; +val constrains_reachable_Int = thm "constrains_reachable_Int"; +val Constrains_eq_constrains = thm "Constrains_eq_constrains"; +val constrains_imp_Constrains = thm "constrains_imp_Constrains"; +val stable_imp_Stable = thm "stable_imp_Stable"; +val ConstrainsI = thm "ConstrainsI"; +val Constrains_empty = thm "Constrains_empty"; +val Constrains_UNIV = thm "Constrains_UNIV"; +val Constrains_weaken_R = thm "Constrains_weaken_R"; +val Constrains_weaken_L = thm "Constrains_weaken_L"; +val Constrains_weaken = thm "Constrains_weaken"; +val Constrains_Un = thm "Constrains_Un"; +val Constrains_UN = thm "Constrains_UN"; +val Constrains_Int = thm "Constrains_Int"; +val Constrains_INT = thm "Constrains_INT"; +val Constrains_imp_subset = thm "Constrains_imp_subset"; +val Constrains_trans = thm "Constrains_trans"; +val Constrains_cancel = thm "Constrains_cancel"; +val Stable_eq = thm "Stable_eq"; +val Stable_eq_stable = thm "Stable_eq_stable"; +val StableI = thm "StableI"; +val StableD = thm "StableD"; +val Stable_Un = thm "Stable_Un"; +val Stable_Int = thm "Stable_Int"; +val Stable_Constrains_Un = thm "Stable_Constrains_Un"; +val Stable_Constrains_Int = thm "Stable_Constrains_Int"; +val Stable_UN = thm "Stable_UN"; +val Stable_INT = thm "Stable_INT"; +val Stable_reachable = thm "Stable_reachable"; +val IncreasingD = thm "IncreasingD"; +val mono_Increasing_o = thm "mono_Increasing_o"; +val strict_IncreasingD = thm "strict_IncreasingD"; +val increasing_imp_Increasing = thm "increasing_imp_Increasing"; +val Increasing_constant = thm "Increasing_constant"; +val Elimination = thm "Elimination"; +val Elimination_sing = thm "Elimination_sing"; +val AlwaysI = thm "AlwaysI"; +val AlwaysD = thm "AlwaysD"; +val AlwaysE = thm "AlwaysE"; +val Always_imp_Stable = thm "Always_imp_Stable"; +val Always_includes_reachable = thm "Always_includes_reachable"; +val invariant_imp_Always = thm "invariant_imp_Always"; +val Always_reachable = thm "Always_reachable"; +val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable"; +val Always_eq_includes_reachable = thm "Always_eq_includes_reachable"; +val Always_UNIV_eq = thm "Always_UNIV_eq"; +val UNIV_AlwaysI = thm "UNIV_AlwaysI"; +val Always_eq_UN_invariant = thm "Always_eq_UN_invariant"; +val Always_weaken = thm "Always_weaken"; +val Always_Constrains_pre = thm "Always_Constrains_pre"; +val Always_Constrains_post = thm "Always_Constrains_post"; +val Always_ConstrainsI = thm "Always_ConstrainsI"; +val Always_ConstrainsD = thm "Always_ConstrainsD"; +val Always_Constrains_weaken = thm "Always_Constrains_weaken"; +val Always_Int_distrib = thm "Always_Int_distrib"; +val Always_INT_distrib = thm "Always_INT_distrib"; +val Always_Int_I = thm "Always_Int_I"; +val Always_Compl_Un_eq = thm "Always_Compl_Un_eq"; +val Always_thin = thm "Always_thin"; + (*FP*) val stable_FP_Orig_Int = thm "stable_FP_Orig_Int"; val FP_Orig_weakest = thm "FP_Orig_weakest"; @@ -473,6 +682,18 @@ val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe"; +(*Lazy unfolding of actions or of sets*) +fun simp_of_act def = def RS def_act_simp; + +fun simp_of_set def = def RS def_set_simp; + + +(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) +val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin + +(*Combines a list of invariance THEOREMS into one.*) +val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I) + (*proves "co" properties when the program is specified*) fun gen_constrains_tac(cs,ss) i = SELECT_GOAL @@ -504,6 +725,8 @@ ALLGOALS (clarify_tac cs), ALLGOALS (asm_lr_simp_tac ss)]); +fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st; + fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact; diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/WFair.ML --- a/src/HOL/UNITY/WFair.ML Thu Jan 30 10:35:56 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,560 +0,0 @@ -(* Title: HOL/UNITY/WFair - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Weak Fairness versions of transient, ensures, leadsTo. - -From Misra, "A Logic for Concurrent Programming", 1994 -*) - - -(*** transient ***) - -Goalw [stable_def, constrains_def, transient_def] - "[| F : stable A; F : transient A |] ==> A = {}"; -by (Blast_tac 1); -qed "stable_transient_empty"; - -Goalw [transient_def] - "[| F : transient A; B<=A |] ==> F : transient B"; -by (Clarify_tac 1); -by (blast_tac (claset() addSIs [rev_bexI]) 1); -qed "transient_strengthen"; - -Goalw [transient_def] - "[| act: Acts F; A <= Domain act; act``A <= -A |] ==> F : transient A"; -by (Blast_tac 1); -qed "transientI"; - -val major::prems = -Goalw [transient_def] - "[| F : transient A; \ -\ !!act. [| act: Acts F; A <= Domain act; act``A <= -A |] ==> P |] \ -\ ==> P"; -by (rtac (major RS CollectD RS bexE) 1); -by (blast_tac (claset() addIs prems) 1); -qed "transientE"; - -Goalw [transient_def] "transient UNIV = {}"; -by (Blast_tac 1); -qed "transient_UNIV"; - -Goalw [transient_def] "transient {} = UNIV"; -by Auto_tac; -qed "transient_empty"; -Addsimps [transient_UNIV, transient_empty]; - - -(*** ensures ***) - -Goalw [ensures_def] - "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"; -by (Blast_tac 1); -qed "ensuresI"; - -Goalw [ensures_def] - "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"; -by (Blast_tac 1); -qed "ensuresD"; - -Goalw [ensures_def] - "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"; -by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); -qed "ensures_weaken_R"; - -(*The L-version (precondition strengthening) fails, but we have this*) -Goalw [ensures_def] - "[| F : stable C; F : A ensures B |] \ -\ ==> F : (C Int A) ensures (C Int B)"; -by (auto_tac (claset(), - simpset() addsimps [ensures_def, - Int_Un_distrib RS sym, - Diff_Int_distrib RS sym])); -by (blast_tac (claset() addIs [transient_strengthen]) 2); -by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1); -qed "stable_ensures_Int"; - -Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B"; -by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); -by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); -qed "stable_transient_ensures"; - -Goal "(A ensures B) = (A unless B) Int transient (A-B)"; -by (simp_tac (simpset() addsimps [ensures_def, unless_def]) 1); -qed "ensures_eq"; - - -(*** leadsTo ***) - -Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B"; -by (blast_tac (claset() addIs [leads.Basis]) 1); -qed "leadsTo_Basis"; - -AddIs [leadsTo_Basis]; - -Goalw [leadsTo_def] - "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C"; -by (blast_tac (claset() addIs [leads.Trans]) 1); -qed "leadsTo_Trans"; - -Goal "F : transient A ==> F : A leadsTo (-A)"; -by (asm_simp_tac - (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); -qed "transient_imp_leadsTo"; - -(*Useful with cancellation, disjunction*) -Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; -by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); -qed "leadsTo_Un_duplicate"; - -Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"; -by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); -qed "leadsTo_Un_duplicate2"; - -(*The Union introduction rule as we should have liked to state it*) -val prems = Goalw [leadsTo_def] - "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"; -by (blast_tac (claset() addIs [leads.Union] addDs prems) 1); -qed "leadsTo_Union"; - -val prems = Goalw [leadsTo_def] - "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"; -by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1); -by (blast_tac (claset() addIs [leads.Union] addDs prems) 1); -qed "leadsTo_Union_Int"; - -val prems = Goal - "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"; -by (stac (Union_image_eq RS sym) 1); -by (blast_tac (claset() addIs leadsTo_Union::prems) 1); -qed "leadsTo_UN"; - -(*Binary union introduction rule*) -Goal "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"; -by (stac Un_eq_Union 1); -by (blast_tac (claset() addIs [leadsTo_Union]) 1); -qed "leadsTo_Un"; - -val prems = -Goal "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"; -by (stac (UN_singleton RS sym) 1 THEN rtac leadsTo_UN 1); -by (blast_tac (claset() addIs prems) 1); -qed "single_leadsTo_I"; - - -(*The INDUCTION rule as we should have liked to state it*) -val major::prems = Goalw [leadsTo_def] - "[| F : za leadsTo zb; \ -\ !!A B. F : A ensures B ==> P A B; \ -\ !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] \ -\ ==> P A C; \ -\ !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \ -\ |] ==> P za zb"; -by (rtac (major RS CollectD RS leads.induct) 1); -by (REPEAT (blast_tac (claset() addIs prems) 1)); -qed "leadsTo_induct"; - - -Goal "A<=B ==> F : A ensures B"; -by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); -by (Blast_tac 1); -qed "subset_imp_ensures"; - -bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); - -bind_thm ("leadsTo_refl", subset_refl RS subset_imp_leadsTo); - -bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); -Addsimps [empty_leadsTo]; - -bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo); -Addsimps [leadsTo_UNIV]; - - - -(** Variant induction rule: on the preconditions for B **) - -(*Lemma is the weak version: can't see how to do it in one step*) -val major::prems = Goal - "[| F : za leadsTo zb; \ -\ P zb; \ -\ !!A B. [| F : A ensures B; P B |] ==> P A; \ -\ !!S. ALL A:S. P A ==> P (Union S) \ -\ |] ==> P za"; -(*by induction on this formula*) -by (subgoal_tac "P zb --> P za" 1); -(*now solve first subgoal: this formula is sufficient*) -by (blast_tac (claset() addIs leadsTo_refl::prems) 1); -by (rtac (major RS leadsTo_induct) 1); -by (REPEAT (blast_tac (claset() addIs prems) 1)); -val lemma = result(); - -val major::prems = Goal - "[| F : za leadsTo zb; \ -\ P zb; \ -\ !!A B. [| F : A ensures B; F : B leadsTo zb; P B |] ==> P A; \ -\ !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S) \ -\ |] ==> P za"; -by (subgoal_tac "F : za leadsTo zb & P za" 1); -by (etac conjunct2 1); -by (rtac (major RS lemma) 1); -by (blast_tac (claset() addIs [leadsTo_Union]@prems) 3); -by (blast_tac (claset() addIs [leadsTo_Trans]@prems) 2); -by (blast_tac (claset() addIs [leadsTo_refl]@prems) 1); -qed "leadsTo_induct_pre"; - - -Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"; -by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1); -qed "leadsTo_weaken_R"; - -Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"; -by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); -qed_spec_mp "leadsTo_weaken_L"; - -(*Distributes over binary unions*) -Goal "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)"; -by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); -qed "leadsTo_Un_distrib"; - -Goal "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)"; -by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); -qed "leadsTo_UN_distrib"; - -Goal "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)"; -by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); -qed "leadsTo_Union_distrib"; - - -Goal "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"; -by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, - leadsTo_Trans]) 1); -qed "leadsTo_weaken"; - - -(*Set difference: maybe combine with leadsTo_weaken_L?*) -Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C"; -by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1); -qed "leadsTo_Diff"; - -val prems = goal thy - "(!! i. i:I ==> F : (A i) leadsTo (A' i)) \ -\ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"; -by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); -by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] - addIs prems) 1); -qed "leadsTo_UN_UN"; - -(*Binary union version*) -Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \ -\ ==> F : (A Un B) leadsTo (A' Un B')"; -by (blast_tac (claset() addIs [leadsTo_Un, - leadsTo_weaken_R]) 1); -qed "leadsTo_Un_Un"; - - -(** The cancellation law **) - -Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \ -\ ==> F : A leadsTo (A' Un B')"; -by (blast_tac (claset() addIs [leadsTo_Un_Un, - subset_imp_leadsTo, leadsTo_Trans]) 1); -qed "leadsTo_cancel2"; - -Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \ -\ ==> F : A leadsTo (A' Un B')"; -by (rtac leadsTo_cancel2 1); -by (assume_tac 2); -by (ALLGOALS Asm_simp_tac); -qed "leadsTo_cancel_Diff2"; - -Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \ -\ ==> F : A leadsTo (B' Un A')"; -by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); -by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); -qed "leadsTo_cancel1"; - -Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \ -\ ==> F : A leadsTo (B' Un A')"; -by (rtac leadsTo_cancel1 1); -by (assume_tac 2); -by (ALLGOALS Asm_simp_tac); -qed "leadsTo_cancel_Diff1"; - - - -(** The impossibility law **) - -Goal "F : A leadsTo {} ==> A={}"; -by (etac leadsTo_induct_pre 1); -by (ALLGOALS - (asm_full_simp_tac - (simpset() addsimps [ensures_def, constrains_def, transient_def]))); -by (Blast_tac 1); -qed "leadsTo_empty"; - - -(** PSP: Progress-Safety-Progress **) - -(*Special case of PSP: Misra's "stable conjunction"*) -Goalw [stable_def] - "[| F : A leadsTo A'; F : stable B |] \ -\ ==> F : (A Int B) leadsTo (A' Int B)"; -by (etac leadsTo_induct 1); -by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); -by (blast_tac (claset() addIs [leadsTo_Trans]) 2); -by (rtac leadsTo_Basis 1); -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 "psp_stable"; - -Goal - "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"; -by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); -qed "psp_stable2"; - -Goalw [ensures_def, constrains_def] - "[| F : A ensures A'; F : B co B' |] \ -\ ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"; -by (Clarify_tac 1); (*speeds up the proof*) -by (blast_tac (claset() addIs [transient_strengthen]) 1); -qed "psp_ensures"; - -Goal "[| F : A leadsTo A'; F : B co B' |] \ -\ ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"; -by (etac leadsTo_induct 1); -by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); -(*Transitivity case has a delicate argument involving "cancellation"*) -by (rtac leadsTo_Un_duplicate2 2); -by (etac leadsTo_cancel_Diff1 2); -by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); -by (blast_tac (claset() addIs [leadsTo_weaken_L] - addDs [constrains_imp_subset]) 2); -(*Basis case*) -by (blast_tac (claset() addIs [psp_ensures]) 1); -qed "psp"; - -Goal "[| F : A leadsTo A'; F : B co B' |] \ -\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"; -by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); -qed "psp2"; - - -Goalw [unless_def] - "[| F : A leadsTo A'; F : B unless B' |] \ -\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')"; -by (dtac psp 1); -by (assume_tac 1); -by (blast_tac (claset() addIs [leadsTo_weaken]) 1); -qed "psp_unless"; - - -(*** Proving the induction rules ***) - -(** The most general rule: r is any wf relation; f is any variant function **) - -Goal "[| wf r; \ -\ ALL m. F : (A Int f-`{m}) leadsTo \ -\ ((A Int f-`(r^-1 `` {m})) Un B) |] \ -\ ==> F : (A Int f-`{m}) leadsTo B"; -by (eres_inst_tac [("a","m")] wf_induct 1); -by (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B" 1); -by (stac vimage_eq_UN 2); -by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2); -by (blast_tac (claset() addIs [leadsTo_UN]) 2); -by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); -val lemma = result(); - - -(** Meta or object quantifier ? **) -Goal "[| wf r; \ -\ ALL m. F : (A Int f-`{m}) leadsTo \ -\ ((A Int f-`(r^-1 `` {m})) Un B) |] \ -\ ==> F : A leadsTo B"; -by (res_inst_tac [("t", "A")] subst 1); -by (rtac leadsTo_UN 2); -by (etac lemma 2); -by (REPEAT (assume_tac 2)); -by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*) -qed "leadsTo_wf_induct"; - - -Goal "[| wf r; \ -\ ALL m:I. F : (A Int f-`{m}) leadsTo \ -\ ((A Int f-`(r^-1 `` {m})) Un B) |] \ -\ ==> F : A leadsTo ((A - (f-`I)) Un B)"; -by (etac leadsTo_wf_induct 1); -by Safe_tac; -by (case_tac "m:I" 1); -by (blast_tac (claset() addIs [leadsTo_weaken]) 1); -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); -qed "bounded_induct"; - - -(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*) -val prems = -Goal "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |] \ -\ ==> F : A leadsTo B"; -by (rtac (wf_less_than RS leadsTo_wf_induct) 1); -by (Asm_simp_tac 1); -by (blast_tac (claset() addIs prems) 1); -qed "lessThan_induct"; - -Goal "!!l::nat. [| ALL m:(greaterThan l). \ -\ F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |] \ -\ ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)"; -by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, - Compl_greaterThan RS sym]) 1); -by (rtac (wf_less_than RS bounded_induct) 1); -by (Asm_simp_tac 1); -qed "lessThan_bounded_induct"; - -Goal "!!l::nat. [| ALL m:(lessThan l). \ -\ F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |] \ -\ ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)"; -by (res_inst_tac [("f","f"),("f1", "%k. l - k")] - (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1); -by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); -by (Clarify_tac 1); -by (case_tac "m A <= wlt F B"; -by (blast_tac (claset() addSIs [leadsTo_Union]) 1); -qed "leadsTo_subset"; - -(*Misra's property W2*) -Goal "F : A leadsTo B = (A <= wlt F B)"; -by (blast_tac (claset() addSIs [leadsTo_subset, - wlt_leadsTo RS leadsTo_weaken_L]) 1); -qed "leadsTo_eq_subset_wlt"; - -(*Misra's property W4*) -Goal "B <= wlt F B"; -by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym, - subset_imp_leadsTo]) 1); -qed "wlt_increasing"; - - -(*Used in the Trans case below*) -Goalw [constrains_def] - "[| B <= A2; \ -\ F : (A1 - B) co (A1 Un B); \ -\ F : (A2 - C) co (A2 Un C) |] \ -\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"; -by (Clarify_tac 1); -by (Blast_tac 1); -val lemma1 = result(); - - -(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) -Goal "F : A leadsTo A' \ -\ ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"; -by (etac leadsTo_induct 1); -(*Basis*) -by (blast_tac (claset() addDs [ensuresD]) 1); -(*Trans*) -by (Clarify_tac 1); -by (res_inst_tac [("x", "Ba Un Bb")] exI 1); -by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1, - leadsTo_Un_duplicate]) 1); -(*Union*) -by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, bchoice]) 1);; -by (res_inst_tac [("x", "UN A:S. f A")] exI 1); -by (auto_tac (claset() addIs [leadsTo_UN], simpset())); -(*Blast_tac says PROOF FAILED*) -by (deepen_tac (claset() addIs [constrains_UN RS constrains_weaken]) 0 1); -qed "leadsTo_123"; - - -(*Misra's property W5*) -Goal "F : (wlt F B - B) co (wlt F B)"; -by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); -by (Clarify_tac 1); -by (subgoal_tac "Ba = wlt F B" 1); -by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1); -qed "wlt_constrains_wlt"; - - -(*** Completion: Binary and General Finite versions ***) - -Goal "[| W = wlt F (B' Un C); \ -\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \ -\ F : B leadsTo (B' Un C); F : B' co (B' Un C) |] \ -\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"; -by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1); -by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] - MRS constrains_Un RS constrains_weaken]) 2); -by (subgoal_tac "F : (W-C) co W" 1); -by (asm_full_simp_tac - (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); -by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1); -by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2); -(** LEVEL 6 **) -by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); -by (rtac leadsTo_Un_duplicate2 2); -by (blast_tac (claset() addIs [leadsTo_Un_Un, - wlt_leadsTo RS psp2 RS leadsTo_weaken, - leadsTo_refl]) 2); -by (dtac leadsTo_Diff 1); -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); -by (subgoal_tac "A Int B <= A Int W" 1); -by (blast_tac (claset() addSDs [leadsTo_subset] - addSIs [subset_refl RS Int_mono]) 2); -by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); -bind_thm("completion", refl RS result()); - - -Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) --> \ -\ (ALL i:I. F : (A' i) co (A' i Un C)) --> \ -\ F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"; -by (etac finite_induct 1); -by Auto_tac; -by (rtac completion 1); -by (simp_tac (HOL_ss addsimps (INT_simps RL [sym])) 4); -by (rtac constrains_INT 4); -by Auto_tac; -val lemma = result(); - -val prems = Goal - "[| finite I; \ -\ !!i. i:I ==> F : (A i) leadsTo (A' i Un C); \ -\ !!i. i:I ==> F : (A' i) co (A' i Un C) |] \ -\ ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"; -by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1); -qed "finite_completion"; - -Goalw [stable_def] - "[| F : A leadsTo A'; F : stable A'; \ -\ F : B leadsTo B'; F : stable B' |] \ -\ ==> F : (A Int B) leadsTo (A' Int B')"; -by (res_inst_tac [("C1", "{}")] (completion RS leadsTo_weaken_R) 1); -by (REPEAT (Force_tac 1)); -qed "stable_completion"; - -val prems = Goalw [stable_def] - "[| finite I; \ -\ !!i. i:I ==> F : (A i) leadsTo (A' i); \ -\ !!i. i:I ==> F : stable (A' i) |] \ -\ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"; -by (res_inst_tac [("C1", "{}")] (finite_completion RS leadsTo_weaken_R) 1); -by (ALLGOALS Asm_simp_tac); -by (ALLGOALS (blast_tac (claset() addIs prems))); -qed "finite_stable_completion"; - - diff -r 19f50fa807ae -r baefae13ad37 src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Thu Jan 30 10:35:56 2003 +0100 +++ b/src/HOL/UNITY/WFair.thy Thu Jan 30 18:08:09 2003 +0100 @@ -8,7 +8,7 @@ From Misra, "A Logic for Concurrent Programming", 1994 *) -WFair = UNITY + +theory WFair = UNITY: constdefs @@ -17,7 +17,7 @@ transient :: "'a set => 'a program set" "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}" - ensures :: "['a set, 'a set] => 'a program set" (infixl 60) + ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60) "A ensures B == (A-B co A Un B) Int transient (A-B)" @@ -28,19 +28,19 @@ inductive "leads F" - intrs + intros - Basis "F : A ensures B ==> (A,B) : leads F" + Basis: "F : A ensures B ==> (A,B) : leads F" - Trans "[| (A,B) : leads F; (B,C) : leads F |] ==> (A,C) : leads F" + Trans: "[| (A,B) : leads F; (B,C) : leads F |] ==> (A,C) : leads F" - Union "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F" + Union: "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F" constdefs (*visible version of the LEADS-TO relation*) - leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) + leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) "A leadsTo B == {F. (A,B) : leads F}" (*wlt F B is the largest set that leads to B*) @@ -48,6 +48,537 @@ "wlt F B == Union {A. F: A leadsTo B}" syntax (xsymbols) - "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\" 60) + "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\" 60) + + +(*** transient ***) + +lemma stable_transient_empty: + "[| F : stable A; F : transient A |] ==> A = {}" + +by (unfold stable_def constrains_def transient_def, blast) + +lemma transient_strengthen: + "[| F : transient A; B<=A |] ==> F : transient B" +apply (unfold transient_def, clarify) +apply (blast intro!: rev_bexI) +done + +lemma transientI: + "[| act: Acts F; A <= Domain act; act``A <= -A |] ==> F : transient A" +by (unfold transient_def, blast) + +lemma transientE: + "[| F : transient A; + !!act. [| act: Acts F; A <= Domain act; act``A <= -A |] ==> P |] + ==> P" +by (unfold transient_def, blast) + +lemma transient_UNIV [simp]: "transient UNIV = {}" +by (unfold transient_def, blast) + +lemma transient_empty [simp]: "transient {} = UNIV" +by (unfold transient_def, auto) + + +(*** ensures ***) + +lemma ensuresI: + "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B" +by (unfold ensures_def, blast) + +lemma ensuresD: + "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)" +by (unfold ensures_def, blast) + +lemma ensures_weaken_R: + "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'" +apply (unfold ensures_def) +apply (blast intro: constrains_weaken transient_strengthen) +done + +(*The L-version (precondition strengthening) fails, but we have this*) +lemma stable_ensures_Int: + "[| F : stable C; F : A ensures B |] + ==> F : (C Int A) ensures (C Int B)" +apply (unfold ensures_def) +apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric]) +prefer 2 apply (blast intro: transient_strengthen) +apply (blast intro: stable_constrains_Int constrains_weaken) +done + +lemma stable_transient_ensures: + "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B" +apply (simp add: ensures_def stable_def) +apply (blast intro: constrains_weaken transient_strengthen) +done + +lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)" +by (simp (no_asm) add: ensures_def unless_def) + + +(*** leadsTo ***) + +lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B" +apply (unfold leadsTo_def) +apply (blast intro: leads.Basis) +done + +lemma leadsTo_Trans: + "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C" +apply (unfold leadsTo_def) +apply (blast intro: leads.Trans) +done + +lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)" +by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition) + +(*Useful with cancellation, disjunction*) +lemma leadsTo_Un_duplicate: "F : A leadsTo (A' Un A') ==> F : A leadsTo A'" +by (simp add: Un_ac) + +lemma leadsTo_Un_duplicate2: + "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)" +by (simp add: Un_ac) + +(*The Union introduction rule as we should have liked to state it*) +lemma leadsTo_Union: + "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B" +apply (unfold leadsTo_def) +apply (blast intro: leads.Union) +done + +lemma leadsTo_Union_Int: + "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B" +apply (unfold leadsTo_def) +apply (simp only: Int_Union_Union) +apply (blast intro: leads.Union) +done + +lemma leadsTo_UN: + "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B" +apply (subst Union_image_eq [symmetric]) +apply (blast intro: leadsTo_Union) +done + +(*Binary union introduction rule*) +lemma leadsTo_Un: + "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C" +apply (subst Un_eq_Union) +apply (blast intro: leadsTo_Union) +done + +lemma single_leadsTo_I: + "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B" +by (subst UN_singleton [symmetric], rule leadsTo_UN, blast) + + +(*The INDUCTION rule as we should have liked to state it*) +lemma leadsTo_induct: + "[| F : za leadsTo zb; + !!A B. F : A ensures B ==> P A B; + !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] + ==> P A C; + !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B + |] ==> P za zb" +apply (unfold leadsTo_def) +apply (drule CollectD, erule leads.induct) +apply (blast+) +done + + +lemma subset_imp_ensures: "A<=B ==> F : A ensures B" +by (unfold ensures_def constrains_def transient_def, blast) + +lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard] + +lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard] + +lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp] + +lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp] + + + +(** Variant induction rule: on the preconditions for B **) + +(*Lemma is the weak version: can't see how to do it in one step*) +lemma leadsTo_induct_pre_lemma: + "[| F : za leadsTo zb; + P zb; + !!A B. [| F : A ensures B; P B |] ==> P A; + !!S. ALL A:S. P A ==> P (Union S) + |] ==> P za" +(*by induction on this formula*) +apply (subgoal_tac "P zb --> P za") +(*now solve first subgoal: this formula is sufficient*) +apply (blast intro: leadsTo_refl) +apply (erule leadsTo_induct) +apply (blast+) +done + +lemma leadsTo_induct_pre: + "[| F : za leadsTo zb; + P zb; + !!A B. [| F : A ensures B; F : B leadsTo zb; P B |] ==> P A; + !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S) + |] ==> P za" +apply (subgoal_tac "F : za leadsTo zb & P za") +apply (erule conjunct2) +apply (erule leadsTo_induct_pre_lemma) +prefer 3 apply (blast intro: leadsTo_Union) +prefer 2 apply (blast intro: leadsTo_Trans) +apply (blast intro: leadsTo_refl) +done + + +lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'" +by (blast intro: subset_imp_leadsTo leadsTo_Trans) + +lemma leadsTo_weaken_L [rule_format (no_asm)]: + "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'" +by (blast intro: leadsTo_Trans subset_imp_leadsTo) + +(*Distributes over binary unions*) +lemma leadsTo_Un_distrib: + "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)" +by (blast intro: leadsTo_Un leadsTo_weaken_L) + +lemma leadsTo_UN_distrib: + "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)" +by (blast intro: leadsTo_UN leadsTo_weaken_L) + +lemma leadsTo_Union_distrib: + "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)" +by (blast intro: leadsTo_Union leadsTo_weaken_L) + + +lemma leadsTo_weaken: + "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'" +by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans) + + +(*Set difference: maybe combine with leadsTo_weaken_L?*) +lemma leadsTo_Diff: + "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C" +by (blast intro: leadsTo_Un leadsTo_weaken) + +lemma leadsTo_UN_UN: + "(!! i. i:I ==> F : (A i) leadsTo (A' i)) + ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)" +apply (simp only: Union_image_eq [symmetric]) +apply (blast intro: leadsTo_Union leadsTo_weaken_R) +done + +(*Binary union version*) +lemma leadsTo_Un_Un: + "[| F : A leadsTo A'; F : B leadsTo B' |] + ==> F : (A Un B) leadsTo (A' Un B')" +by (blast intro: leadsTo_Un leadsTo_weaken_R) + + +(** The cancellation law **) + +lemma leadsTo_cancel2: + "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] + ==> F : A leadsTo (A' Un B')" +by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans) + +lemma leadsTo_cancel_Diff2: + "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] + ==> F : A leadsTo (A' Un B')" +apply (rule leadsTo_cancel2) +prefer 2 apply assumption +apply (simp_all (no_asm_simp)) +done + +lemma leadsTo_cancel1: + "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] + ==> F : A leadsTo (B' Un A')" +apply (simp add: Un_commute) +apply (blast intro!: leadsTo_cancel2) +done + +lemma leadsTo_cancel_Diff1: + "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] + ==> F : A leadsTo (B' Un A')" +apply (rule leadsTo_cancel1) +prefer 2 apply assumption +apply (simp_all (no_asm_simp)) +done + + + +(** The impossibility law **) + +lemma leadsTo_empty: "F : A leadsTo {} ==> A={}" +apply (erule leadsTo_induct_pre) +apply (simp_all add: ensures_def constrains_def transient_def, blast) +done + + +(** PSP: Progress-Safety-Progress **) + +(*Special case of PSP: Misra's "stable conjunction"*) +lemma psp_stable: + "[| F : A leadsTo A'; F : stable B |] + ==> F : (A Int B) leadsTo (A' Int B)" +apply (unfold stable_def) +apply (erule leadsTo_induct) +prefer 3 apply (blast intro: leadsTo_Union_Int) +prefer 2 apply (blast intro: leadsTo_Trans) +apply (rule leadsTo_Basis) +apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric]) +apply (blast intro: transient_strengthen constrains_Int) +done + +lemma psp_stable2: + "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')" +by (simp add: psp_stable Int_ac) + +lemma psp_ensures: + "[| F : A ensures A'; F : B co B' |] + ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))" +apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*) +apply (blast intro: transient_strengthen) +done + +lemma psp: + "[| F : A leadsTo A'; F : B co B' |] + ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))" +apply (erule leadsTo_induct) + prefer 3 apply (blast intro: leadsTo_Union_Int) + txt{*Basis case*} + apply (blast intro: psp_ensures) +txt{*Transitivity case has a delicate argument involving "cancellation"*} +apply (rule leadsTo_Un_duplicate2) +apply (erule leadsTo_cancel_Diff1) +apply (simp add: Int_Diff Diff_triv) +apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset) +done + +lemma psp2: + "[| F : A leadsTo A'; F : B co B' |] + ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))" +by (simp (no_asm_simp) add: psp Int_ac) + +lemma psp_unless: + "[| F : A leadsTo A'; F : B unless B' |] + ==> F : (A Int B) leadsTo ((A' Int B) Un B')" + +apply (unfold unless_def) +apply (drule psp, assumption) +apply (blast intro: leadsTo_weaken) +done + + +(*** Proving the induction rules ***) + +(** The most general rule: r is any wf relation; f is any variant function **) + +lemma leadsTo_wf_induct_lemma: + "[| wf r; + ALL m. F : (A Int f-`{m}) leadsTo + ((A Int f-`(r^-1 `` {m})) Un B) |] + ==> F : (A Int f-`{m}) leadsTo B" +apply (erule_tac a = m in wf_induct) +apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B") + apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate) +apply (subst vimage_eq_UN) +apply (simp only: UN_simps [symmetric]) +apply (blast intro: leadsTo_UN) +done + + +(** Meta or object quantifier ? **) +lemma leadsTo_wf_induct: + "[| wf r; + ALL m. F : (A Int f-`{m}) leadsTo + ((A Int f-`(r^-1 `` {m})) Un B) |] + ==> F : A leadsTo B" +apply (rule_tac t = A in subst) + defer 1 + apply (rule leadsTo_UN) + apply (erule leadsTo_wf_induct_lemma) + apply assumption +apply fast (*Blast_tac: Function unknown's argument not a parameter*) +done + + +lemma bounded_induct: + "[| wf r; + ALL m:I. F : (A Int f-`{m}) leadsTo + ((A Int f-`(r^-1 `` {m})) Un B) |] + ==> F : A leadsTo ((A - (f-`I)) Un B)" +apply (erule leadsTo_wf_induct, safe) +apply (case_tac "m:I") +apply (blast intro: leadsTo_weaken) +apply (blast intro: subset_imp_leadsTo) +done + + +(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*) +lemma lessThan_induct: + "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |] + ==> F : A leadsTo B" +apply (rule wf_less_than [THEN leadsTo_wf_induct]) +apply (simp (no_asm_simp)) +apply blast +done + +lemma lessThan_bounded_induct: + "!!l::nat. [| ALL m:(greaterThan l). + F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |] + ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)" +apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric]) +apply (rule wf_less_than [THEN bounded_induct]) +apply (simp (no_asm_simp)) +done + +lemma greaterThan_bounded_induct: + "!!l::nat. [| ALL m:(lessThan l). + F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |] + ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)" +apply (rule_tac f = f and f1 = "%k. l - k" + in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct]) +apply (simp (no_asm) add: inv_image_def Image_singleton) +apply clarify +apply (case_tac "m A <= wlt F B" +apply (unfold wlt_def) +apply (blast intro!: leadsTo_Union) +done + +(*Misra's property W2*) +lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)" +by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L]) + +(*Misra's property W4*) +lemma wlt_increasing: "B <= wlt F B" +apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo) +done + + +(*Used in the Trans case below*) +lemma lemma1: + "[| B <= A2; + F : (A1 - B) co (A1 Un B); + F : (A2 - C) co (A2 Un C) |] + ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)" +by (unfold constrains_def, clarify, blast) + +(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) +lemma leadsTo_123: + "F : A leadsTo A' + ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')" +apply (erule leadsTo_induct) +(*Basis*) +apply (blast dest: ensuresD) +(*Trans*) +apply clarify +apply (rule_tac x = "Ba Un Bb" in exI) +apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate) +(*Union*) +apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice) +apply (rule_tac x = "UN A:S. f A" in exI) +apply (auto intro: leadsTo_UN) +(*Blast_tac says PROOF FAILED*) +apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B" + in constrains_UN [THEN constrains_weaken]) +apply (auto ); +done + + +(*Misra's property W5*) +lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)" +apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], clarify) +apply (subgoal_tac "Ba = wlt F B") +prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify) +apply (simp add: wlt_increasing Un_absorb2) +done + + +(*** Completion: Binary and General Finite versions ***) + +lemma completion_lemma : + "[| W = wlt F (B' Un C); + F : A leadsTo (A' Un C); F : A' co (A' Un C); + F : B leadsTo (B' Un C); F : B' co (B' Un C) |] + ==> F : (A Int B) leadsTo ((A' Int B') Un C)" +apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ") + prefer 2 + apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, + THEN constrains_weaken]) +apply (subgoal_tac "F : (W-C) co W") + prefer 2 + apply (simp add: wlt_increasing Un_assoc Un_absorb2) +apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ") + prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken]) +(** LEVEL 6 **) +apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ") + prefer 2 + apply (rule leadsTo_Un_duplicate2) + apply (blast intro: leadsTo_Un_Un wlt_leadsTo + [THEN psp2, THEN leadsTo_weaken] leadsTo_refl) +apply (drule leadsTo_Diff) +apply (blast intro: subset_imp_leadsTo) +apply (subgoal_tac "A Int B <= A Int W") + prefer 2 + apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono]) +apply (blast intro: leadsTo_Trans subset_imp_leadsTo) +done + +lemmas completion = completion_lemma [OF refl] + +lemma finite_completion_lemma: + "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) --> + (ALL i:I. F : (A' i) co (A' i Un C)) --> + F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)" +apply (erule finite_induct, auto) +apply (rule completion) + prefer 4 + apply (simp only: INT_simps [symmetric]) + apply (rule constrains_INT, auto) +done + +lemma finite_completion: + "[| finite I; + !!i. i:I ==> F : (A i) leadsTo (A' i Un C); + !!i. i:I ==> F : (A' i) co (A' i Un C) |] + ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)" +by (blast intro: finite_completion_lemma [THEN mp, THEN mp]) + +lemma stable_completion: + "[| F : A leadsTo A'; F : stable A'; + F : B leadsTo B'; F : stable B' |] + ==> F : (A Int B) leadsTo (A' Int B')" +apply (unfold stable_def) +apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R]) +apply (force+) +done + +lemma finite_stable_completion: + "[| finite I; + !!i. i:I ==> F : (A i) leadsTo (A' i); + !!i. i:I ==> F : stable (A' i) |] + ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)" +apply (unfold stable_def) +apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R]) +apply (simp_all (no_asm_simp)) +apply blast+ +done end