# HG changeset patch # User paulson # Date 908444107 -7200 # Node ID fe887910e32ebd122ac53e71c2b0695e9adf2b8f # Parent 4e8837255b87ce3d7a6ab52e5d53e99009ef7e84 specifications as sets of programs diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Channel.ML --- a/src/HOL/UNITY/Channel.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Channel.ML Thu Oct 15 11:35:07 1998 +0200 @@ -8,8 +8,6 @@ From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 *) -AddIffs [skip]; - (*None represents "infinity" while Some represents proper integers*) Goalw [minSet_def] "minSet A = Some x --> x : A"; by (Simp_tac 1); @@ -26,7 +24,7 @@ by (Blast_tac 1); qed_spec_mp "minSet_nonempty"; -Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))"; +Goal "F : leadsTo (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))"; by (rtac leadsTo_weaken 1); by (rtac ([UC2, UC1] MRS psp) 1); by (ALLGOALS Asm_simp_tac); @@ -38,7 +36,7 @@ (*The induction*) -Goal "leadsTo acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))"; +Goal "F : leadsTo (UNIV-{{}}) (minSet -`` (Some``atLeast y))"; by (rtac leadsTo_weaken_R 1); by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")] greaterThan_bounded_induct 1); @@ -54,7 +52,7 @@ val lemma = result(); -Goal "!!y::nat. leadsTo acts (UNIV-{{}}) {s. y ~: s}"; +Goal "!!y::nat. F : leadsTo (UNIV-{{}}) {s. y ~: s}"; by (rtac (lemma RS leadsTo_weaken_R) 1); by (Clarify_tac 1); by (forward_tac [minSet_nonempty] 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Channel.thy --- a/src/HOL/UNITY/Channel.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Channel.thy Thu Oct 15 11:35:07 1998 +0200 @@ -12,18 +12,19 @@ types state = nat set +consts + F :: state program + constdefs minSet :: nat set => nat option "minSet A == if A={} then None else Some (LEAST x. x:A)" rules - skip "Id: acts" - - UC1 "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))" + UC1 "F : constrains (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))" - (* UC1 "constrains acts {s. minSet s = x} {s. x <= minSet s}" *) + (* UC1 "F : constrains {s. minSet s = x} {s. x <= minSet s}" *) - UC2 "leadsTo acts (minSet -`` {Some x}) {s. x ~: s}" + UC2 "F : leadsTo (minSet -`` {Some x}) {s. x ~: s}" end diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Client.ML --- a/src/HOL/UNITY/Client.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Client.ML Thu Oct 15 11:35:07 1998 +0200 @@ -7,74 +7,9 @@ *) - (*MOVE higher-up: UNITY.thy or Traces.thy ???*) - -(*[| stable acts C; constrains acts (C Int A) A |] ==> stable acts (C Int A)*) -bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); - - -(*"raw" notion of invariant. Yields a SET of programs*) -Goal "[| Init F<=A; stable (Acts F) A |] ==> F : invariant A"; -by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); -qed "invariantI"; - -Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def] - "F : invariant A ==> Invariant F A"; -by (blast_tac (claset() addIs [constrains_reachable_Int]) 1); -qed "invariant_imp_Invariant"; - - -(*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"; - -Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def] - "Invariant F A = (F : invariant (reachable F Int A))"; -by (blast_tac (claset() addIs reachable.intrs) 1); -qed "Invariant_eq_invariant_reachable"; - - -bind_thm ("invariant_includes_reachable", - invariant_imp_Invariant RS Invariant_includes_reachable); - -Goalw [always_def] "always A = (UN I: Pow A. invariant I)"; -by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, - stable_reachable, - impOfSubs invariant_includes_reachable]) 1); -qed "always_eq_UN_invariant"; - -Goal "F : always A = (EX I. F: invariant I & I <= A)"; -by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1); -by (Blast_tac 1); -qed "always_iff_ex_invariant"; - - -Goalw [increasing_def, stable_def, constrains_def] - "increasing f <= increasing (length o f)"; -by Auto_tac; -by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1); -qed "increasing_length"; - - -Goalw [increasing_def] - "increasing f <= {F. ALL z::nat. stable (Acts F) {s. z < f s}}"; -by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); -by (Blast_tac 1); -qed "increasing_less"; - - -Goal "[| F Join G : f localTo F; (s,s') : act; \ -\ act : Acts G; act ~: Acts F |] ==> f s' = f s"; -by (asm_full_simp_tac - (simpset() addsimps [localTo_def, Acts_Join, stable_def, - constrains_def]) 1); -by (Blast_tac 1); -qed "localTo_imp_equals"; - - -Goal "[| Stable F A; transient (Acts F) C; \ -\ reachable F <= (-A Un B Un C) |] ==> LeadsTo F A B"; +(*Perhaps move to SubstAx.ML*) +Goal "[| F : Stable A; F : transient C; \ +\ reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B"; by (etac reachable_LeadsTo_weaken 1); by (rtac LeadsTo_Diff 1); by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2); @@ -82,28 +17,25 @@ qed "Stable_transient_reachable_LeadsTo"; -(**** things that definitely belong in Client.ML ****) (*split_all_tac causes a big blow-up*) claset_ref() := claset() delSWrapper "split_all_tac"; -val Client_simp = Cli_prg_def RS def_prg_simps; +Addsimps [Cli_prg_def RS def_prg_Init]; +program_defs_ref := [Cli_prg_def]; Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]); -DelIffs [length_Suc_conv]; - (*Simplification for records*) Addsimps (thms"state.update_defs"); - (*CAN THIS be generalized? Importantly, the second case considers actions that are in G and NOT in Cli_prg (needed to use localTo_imp_equals) *) Goal "(act : Acts (Cli_prg Join G)) = \ \ (act : {Id, rel_act, tok_act, ask_act} | \ \ act : Acts G & act ~: Acts Cli_prg)"; -by (asm_full_simp_tac (simpset() addsimps [Client_simp, Acts_Join]) 1); +by (asm_full_simp_tac (simpset() addsimps [Cli_prg_def, Acts_Join]) 1); (*don't unfold definitions of actions*) by (blast_tac HOL_cs 1); qed "Acts_Cli_Join_eq"; @@ -111,19 +43,18 @@ fun invariant_tac i = rtac invariantI i THEN - auto_tac (claset(), simpset() addsimps [Client_simp]) THEN - constrains_tac i; + constrains_tac (i+1); (*Safety property 1(a): ask is nondecreasing*) Goalw [increasing_def] "Cli_prg: increasing ask"; -by (auto_tac (claset(), simpset() addsimps [Client_simp])); +by (Clarify_tac 1); by (constrains_tac 1); by Auto_tac; qed "increasing_ask"; (*Safety property 1(b): rel is nondecreasing*) Goalw [increasing_def] "Cli_prg: increasing rel"; -by (auto_tac (claset(), simpset() addsimps [Client_simp])); +by (Clarify_tac 1); by (constrains_tac 1); by Auto_tac; qed "increasing_rel"; @@ -148,16 +79,21 @@ qed "ask_bounded"; +(*Curiously, we no longer need to expand the program definition, and + expanding it is extremely expensive!*) +program_defs_ref := []; + (*Safety property 2: clients return the right number of tokens*) Goalw [increasing_def] "Cli_prg : (increasing giv Int (rel localTo Cli_prg)) \ \ guarantees invariant {s. rel s <= giv s}"; by (rtac guaranteesI 1); -by (Clarify_tac 1); by (invariant_tac 1); +by (Force_tac 1); by (subgoal_tac "rel s <= giv s'" 1); by (force_tac (claset(), - simpset() addsimps [stable_def, constrains_def]) 2); + simpset() delsimps [Acts_eq] + addsimps [stable_def, constrains_def]) 2); by (dtac (Acts_Cli_Join_eq RS iffD1) 1); (*we note that "rel" is local to Client*) by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset())); @@ -166,12 +102,12 @@ (*** Towards proving the liveness property ***) -Goal "transient (Acts (Cli_prg Join G)) \ -\ {s. length (giv s) = Suc k & \ -\ length (rel s) = k & ask s ! k <= giv s ! k}"; +Goal "Cli_prg Join G \ +\ : transient {s. length (giv s) = Suc k & \ +\ length (rel s) = k & ask s ! k <= giv s ! k}"; by (res_inst_tac [("act", "rel_act")] transient_mem 1); by (auto_tac (claset(), - simpset() addsimps [Domain_def, Acts_Join, Client_simp])); + simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def])); qed "transient_lemma"; Goal "Cli_prg : \ @@ -183,6 +119,7 @@ by (Clarify_tac 1); by (dtac (impOfSubs increasing_length) 1); by (invariant_tac 1); +by (Force_tac 1); by (dtac (Acts_Cli_Join_eq RS iffD1) 1); by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset())); by (force_tac (claset(), @@ -194,8 +131,8 @@ Goal "Cli_prg : \ \ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \ \ Int invariant giv_meets_ask) \ -\ guarantees {F. LeadsTo F {s. k < length (giv s)} \ -\ {s. k < length (rel s)}}"; +\ guarantees (LeadsTo {s. k < length (giv s)} \ +\ {s. k < length (rel s)})"; by (rtac guaranteesI 1); by (Clarify_tac 1); by (rtac Stable_transient_reachable_LeadsTo 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Client.thy --- a/src/HOL/UNITY/Client.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Client.thy Thu Oct 15 11:35:07 1998 +0200 @@ -8,24 +8,6 @@ Client = Comp + Prefix + -constdefs (*MOVE higher-up: UNITY.thy or Traces.thy ???*) - always :: "'a set => 'a program set" - "always A == {F. reachable F <= A}" - - (*The traditional word for inductive properties. Anyway, INDUCTIVE is - reserved!*) - invariant :: "'a set => 'a program set" - "invariant A == {F. Init F <= A & stable (Acts F) A}" - - (*Polymorphic in both states and the meaning of <= *) - increasing :: "['a => 'b::{ord}] => 'a program set" - "increasing f == {F. ALL z. stable (Acts F) {s. z <= f s}}" - - (*The set of systems that regard "f" as local to F*) - localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80) - "f localTo F == {G. ALL z. stable (Acts G - Acts F) {s. f s = z}}" - - consts Max :: nat (*Maximum number of tokens*) diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Common.ML --- a/src/HOL/UNITY/Common.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Common.ML Thu Oct 15 11:35:07 1998 +0200 @@ -11,8 +11,8 @@ *) (*Misra's property CMT4: t exceeds no common meeting time*) -Goal "[| ALL m. Constrains F {m} (maxfg m); n: common |] \ -\ ==> Stable F (atMost n)"; +Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \ +\ ==> F : Stable (atMost n)"; by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1); by (asm_full_simp_tac (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def, @@ -22,39 +22,40 @@ qed "common_stable"; Goal "[| Init F <= atMost n; \ -\ ALL m. Constrains F {m} (maxfg m); n: common |] \ -\ ==> Invariant F (atMost n)"; +\ ALL m. F : Constrains {m} (maxfg m); n: common |] \ +\ ==> F : Invariant (atMost n)"; by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1); qed "common_Invariant"; (*** Some programs that implement the safety property above ***) -(*This one is just Skip*) -Goal "constrains {Id} {m} (maxfg m)"; +Goal "SKIP : constrains {m} (maxfg m)"; by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, - fasc, gasc]) 1); + fasc]) 1); result(); -(*This one is t := ftime t || t := gtime t really needs Skip too*) -Goal "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \ -\ {m} (maxfg m)"; +(*This one is t := ftime t || t := gtime t*) +Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \ +\ : constrains {m} (maxfg m)"; by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, - le_max_iff_disj]) 1); + le_max_iff_disj, fasc]) 1); by (Blast_tac 1); result(); -(*This one is t := max (ftime t) (gtime t) really needs Skip too*) -Goal "constrains {range(%t.(t, max (ftime t) (gtime t)))} \ -\ {m} (maxfg m)"; -by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1); +(*This one is t := max (ftime t) (gtime t)*) +Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \ +\ : constrains {m} (maxfg m)"; +by (simp_tac + (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); by (Blast_tac 1); result(); (*This one is t := t+1 if t LeadsTo F (atMost n) common"; +\ ==> F : LeadsTo (atMost n) common"; by (rtac LeadsTo_weaken_R 1); by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1); by (ALLGOALS Asm_simp_tac); @@ -80,10 +81,10 @@ val lemma = result(); (*The "ALL m: -common" form echoes CMT6.*) -Goal "[| ALL m. Constrains F {m} (maxfg m); \ -\ ALL m: -common. LeadsTo F {m} (greaterThan m); \ +Goal "[| ALL m. F : Constrains {m} (maxfg m); \ +\ ALL m: -common. F : LeadsTo {m} (greaterThan m); \ \ n: common |] \ -\ ==> LeadsTo F (atMost (LEAST n. n: common)) common"; +\ ==> F : LeadsTo (atMost (LEAST n. n: common)) common"; by (rtac lemma 1); by (ALLGOALS Asm_simp_tac); by (etac LeastI 2); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Common.thy --- a/src/HOL/UNITY/Common.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Common.thy Thu Oct 15 11:35:07 1998 +0200 @@ -10,7 +10,7 @@ From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. *) -Common = SubstAx + +Common = SubstAx + Union + consts ftime,gtime :: nat=>nat diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Constrains.ML --- a/src/HOL/UNITY/Constrains.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Constrains.ML Thu Oct 15 11:35:07 1998 +0200 @@ -9,68 +9,66 @@ (*** Constrains ***) -(*Map its type, ('a * 'a)set set, 'a set, 'a set] => bool, to just 'a*) -Blast.overloaded ("Constrains.Constrains", - HOLogic.dest_setT o domain_type o range_type); +overload_1st_set "Constrains.Constrains"; -(*constrains (Acts F) B B' - ==> constrains (Acts F) (reachable F Int B) (reachable F Int B')*) +(*F : constrains B B' + ==> F : constrains (reachable F Int B) (reachable F Int B')*) bind_thm ("constrains_reachable_Int", subset_refl RS rewrite_rule [stable_def] stable_reachable RS constrains_Int); -Goalw [Constrains_def] "constrains (Acts F) A A' ==> Constrains F A A'"; -by (etac constrains_reachable_Int 1); +Goalw [Constrains_def] "F : constrains A A' ==> F : Constrains A A'"; +by (blast_tac (claset() addIs [constrains_reachable_Int]) 1); qed "constrains_imp_Constrains"; -Goalw [stable_def, Stable_def] "stable (Acts F) A ==> Stable F A"; +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') \ -\ ==> Constrains F A A'"; +\ ==> F : Constrains A A'"; by (rtac constrains_imp_Constrains 1); by (blast_tac (claset() addIs (constrainsI::prems)) 1); qed "ConstrainsI"; -Goalw [Constrains_def, constrains_def] "Constrains F {} B"; +Goalw [Constrains_def, constrains_def] "F : Constrains {} B"; by (Blast_tac 1); qed "Constrains_empty"; -Goal "Constrains F A UNIV"; +Goal "F : Constrains A UNIV"; by (blast_tac (claset() addIs [ConstrainsI]) 1); qed "Constrains_UNIV"; AddIffs [Constrains_empty, Constrains_UNIV]; Goalw [Constrains_def] - "[| Constrains F A A'; A'<=B' |] ==> Constrains F A B'"; + "[| F : Constrains A A'; A'<=B' |] ==> F : Constrains A B'"; by (blast_tac (claset() addIs [constrains_weaken_R]) 1); qed "Constrains_weaken_R"; Goalw [Constrains_def] - "[| Constrains F A A'; B<=A |] ==> Constrains F B A'"; + "[| F : Constrains A A'; B<=A |] ==> F : Constrains B A'"; by (blast_tac (claset() addIs [constrains_weaken_L]) 1); qed "Constrains_weaken_L"; Goalw [Constrains_def] - "[| Constrains F A A'; B<=A; A'<=B' |] ==> Constrains F B B'"; + "[| F : Constrains A A'; B<=A; A'<=B' |] ==> F : Constrains B B'"; by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "Constrains_weaken"; (** Union **) Goalw [Constrains_def] - "[| Constrains F A A'; Constrains F B B' |] \ -\ ==> Constrains F (A Un B) (A' Un B')"; + "[| F : Constrains A A'; F : Constrains B B' |] \ +\ ==> F : Constrains (A Un B) (A' Un B')"; by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1); qed "Constrains_Un"; -Goalw [Constrains_def] - "ALL i:I. Constrains F (A i) (A' i) \ -\ ==> Constrains F (UN i:I. A i) (UN i:I. A' i)"; +Goal "ALL i:I. F : Constrains (A i) (A' i) \ +\ ==> F : Constrains (UN i:I. A i) (UN i:I. A' i)"; +by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); by (dtac ball_constrains_UN 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "ball_Constrains_UN"; @@ -78,75 +76,75 @@ (** Intersection **) Goalw [Constrains_def] - "[| Constrains F A A'; Constrains F B B' |] \ -\ ==> Constrains F (A Int B) (A' Int B')"; + "[| F : Constrains A A'; F : Constrains B B' |] \ +\ ==> F : Constrains (A Int B) (A' Int B')"; by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1); qed "Constrains_Int"; -Goalw [Constrains_def] - "[| ALL i:I. Constrains F (A i) (A' i) |] \ -\ ==> Constrains F (INT i:I. A i) (INT i:I. A' i)"; +Goal "[| ALL i:I. F : Constrains (A i) (A' i) |] \ +\ ==> F : Constrains (INT i:I. A i) (INT i:I. A' i)"; +by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); by (dtac ball_constrains_INT 1); by (dtac constrains_reachable_Int 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "ball_Constrains_INT"; -Goalw [Constrains_def] - "Constrains F A A' ==> reachable F Int A <= A'"; +Goal "F : Constrains A A' ==> reachable F Int A <= A'"; +by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); by (dtac constrains_imp_subset 1); by (ALLGOALS (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]))); qed "Constrains_imp_subset"; Goalw [Constrains_def] - "[| Constrains F A B; Constrains F B C |] \ -\ ==> Constrains F A C"; + "[| F : Constrains A B; F : Constrains B C |] \ +\ ==> F : Constrains A C"; by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); qed "Constrains_trans"; (*** Stable ***) -Goal "Stable F A = stable (Acts F) (reachable F Int A)"; +Goal "(F : Stable A) = (F : stable (reachable F Int A))"; by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1); qed "Stable_eq_stable"; -Goalw [Stable_def] "Constrains F A A ==> Stable F A"; +Goalw [Stable_def] "F : Constrains A A ==> F : Stable A"; by (assume_tac 1); qed "StableI"; -Goalw [Stable_def] "Stable F A ==> Constrains F A A"; +Goalw [Stable_def] "F : Stable A ==> F : Constrains A A"; by (assume_tac 1); qed "StableD"; Goalw [Stable_def] - "[| Stable F A; Stable F A' |] ==> Stable F (A Un A')"; + "[| 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] - "[| Stable F A; Stable F A' |] ==> Stable F (A Int A')"; + "[| 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] - "[| Stable F C; Constrains F A (C Un A') |] \ -\ ==> Constrains F (C Un A) (C Un A')"; + "[| F : Stable C; F : Constrains A (C Un A') |] \ +\ ==> F : Constrains (C Un A) (C Un A')"; by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1); qed "Stable_Constrains_Un"; Goalw [Stable_def] - "[| Stable F C; Constrains F (C Int A) A' |] \ -\ ==> Constrains F (C Int A) (C Int A')"; + "[| F : Stable C; F : Constrains (C Int A) A' |] \ +\ ==> F : Constrains (C Int A) (C Int A')"; by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1); qed "Stable_Constrains_Int"; Goalw [Stable_def] - "(ALL i:I. Stable F (A i)) ==> Stable F (INT i:I. A i)"; + "(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)"; by (etac ball_Constrains_INT 1); qed "ball_Stable_INT"; -Goal "Stable F (reachable F)"; +Goal "F : Stable (reachable F)"; by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1); qed "Stable_reachable"; @@ -157,21 +155,21 @@ in forward proof. ***) Goalw [Constrains_def, constrains_def] - "[| ALL m. Constrains F {s. s x = m} (B m) |] \ -\ ==> Constrains F {s. s x : M} (UN m:M. B m)"; + "[| ALL m. F : Constrains {s. s x = m} (B m) |] \ +\ ==> F : Constrains {s. s x : M} (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. Constrains F {m} (B m)) ==> Constrains F M (UN m:M. B m)"; + "(ALL m. F : Constrains {m} (B m)) ==> F : Constrains M (UN m:M. B m)"; by (Blast_tac 1); qed "Elimination_sing"; Goalw [Constrains_def, constrains_def] - "[| Constrains F A (A' Un B); Constrains F B B' |] \ -\ ==> Constrains F A (A' Un B')"; + "[| F : Constrains A (A' Un B); F : Constrains B B' |] \ +\ ==> F : Constrains A (A' Un B')"; by (Blast_tac 1); qed "Constrains_cancel"; @@ -180,11 +178,11 @@ (** Natural deduction rules for "Invariant F A" **) -Goal "[| Init F<=A; Stable F A |] ==> Invariant F A"; +Goal "[| Init F<=A; F : Stable A |] ==> F : Invariant A"; by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1); qed "InvariantI"; -Goal "Invariant F A ==> Init F<=A & Stable F A"; +Goal "F : Invariant A ==> Init F<=A & F : Stable A"; by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1); qed "InvariantD"; @@ -192,13 +190,13 @@ (*The set of all reachable states is an Invariant...*) -Goal "Invariant F (reachable F)"; +Goal "F : Invariant (reachable F)"; by (simp_tac (simpset() addsimps [Invariant_def]) 1); by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1); qed "Invariant_reachable"; (*...in fact the strongest Invariant!*) -Goal "Invariant F A ==> reachable F <= A"; +Goal "F : Invariant A ==> reachable F <= A"; by (full_simp_tac (simpset() addsimps [Stable_def, Constrains_def, constrains_def, Invariant_def]) 1); @@ -207,25 +205,36 @@ by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); qed "Invariant_includes_reachable"; +Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def] + "F : invariant A ==> F : Invariant A"; +by (blast_tac (claset() addIs [constrains_reachable_Int]) 1); +qed "invariant_imp_Invariant"; -Goal "Invariant F INV ==> reachable F Int INV = reachable F"; +Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def] + "(F : Invariant A) = (F : invariant (reachable F Int A))"; +by (blast_tac (claset() addIs reachable.intrs) 1); +qed "Invariant_eq_invariant_reachable"; + + + +Goal "F : Invariant INV ==> reachable F Int INV = reachable F"; by (dtac Invariant_includes_reachable 1); by (Blast_tac 1); qed "reachable_Int_INV"; -Goal "[| Invariant F INV; Constrains F (INV Int A) A' |] \ -\ ==> Constrains F A A'"; +Goal "[| F : Invariant INV; F : Constrains (INV Int A) A' |] \ +\ ==> F : Constrains A A'"; by (asm_full_simp_tac (simpset() addsimps [Constrains_def, reachable_Int_INV, Int_assoc RS sym]) 1); qed "Invariant_ConstrainsI"; -(* [| Invariant F INV; Constrains F (INV Int A) A |] - ==> Stable F A *) +(* [| F : Invariant INV; F : Constrains (INV Int A) A |] + ==> F : Stable A *) bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI); -Goal "[| Invariant F INV; Constrains F A A' |] \ -\ ==> Constrains F A (INV Int A')"; +Goal "[| F : Invariant INV; F : Constrains A A' |] \ +\ ==> F : Constrains A (INV Int A')"; by (asm_full_simp_tac (simpset() addsimps [Constrains_def, reachable_Int_INV, Int_assoc RS sym]) 1); @@ -237,7 +246,7 @@ (** Conjoining Invariants **) -Goal "[| Invariant F A; Invariant F B |] ==> Invariant F (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"; @@ -246,7 +255,7 @@ used by Invariant_Int) *) val Invariant_thin = read_instantiate_sg (sign_of thy) - [("V", "Invariant ?Prg ?A")] thin_rl; + [("V", "?F : Invariant ?A")] thin_rl; (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) val Invariant_Int_tac = dtac Invariant_Int THEN' @@ -257,15 +266,19 @@ val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int); +(*To allow expansion of the program's definition when appropriate*) +val program_defs_ref = ref ([] : thm list); + (*proves "constrains" properties when the program is specified*) -val constrains_tac = +fun constrains_tac i = SELECT_GOAL - (EVERY [REPEAT (resolve_tac [StableI, stableI, + (EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1, + REPEAT (resolve_tac [StableI, stableI, constrains_imp_Constrains] 1), rtac constrainsI 1, Full_simp_tac 1, REPEAT (FIRSTGOAL (etac disjE)), ALLGOALS Clarify_tac, - ALLGOALS Asm_full_simp_tac]); + ALLGOALS Asm_full_simp_tac]) i; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Constrains.thy --- a/src/HOL/UNITY/Constrains.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Constrains.thy Thu Oct 15 11:35:07 1998 +0200 @@ -10,19 +10,17 @@ constdefs - Constrains :: "['a program, 'a set, 'a set] => bool" - "Constrains F A B == - constrains (Acts F) - (reachable F Int A) - (reachable F Int B)" + Constrains :: "['a set, 'a set] => 'a program set" + "Constrains A B == {F. F : constrains (reachable F Int A) + (reachable F Int B)}" - Stable :: "'a program => 'a set => bool" - "Stable F A == Constrains F A A" + Stable :: "'a set => 'a program set" + "Stable A == Constrains A A" - Unless :: "['a program, 'a set, 'a set] => bool" - "Unless F A B == Constrains F (A-B) (A Un B)" + Unless :: "['a set, 'a set] => 'a program set" + "Unless A B == Constrains (A-B) (A Un B)" - Invariant :: "['a program, 'a set] => bool" - "Invariant F A == (Init F) <= A & Stable F A" + Invariant :: "'a set => 'a program set" + "Invariant A == {F. Init F <= A} Int Stable A" end diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Deadlock.ML --- a/src/HOL/UNITY/Deadlock.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Deadlock.ML Thu Oct 15 11:35:07 1998 +0200 @@ -9,80 +9,70 @@ (*Trivial, two-process case*) Goalw [constrains_def, stable_def] - "[| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \ -\ ==> stable Acts (A Int B)"; + "[| F : constrains (A Int B) A; F : constrains (B Int A) B |] \ +\ ==> F : stable (A Int B)"; by (Blast_tac 1); result(); -Goal "{i. i < Suc n} = insert n {i. i < n}"; -by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1); -qed "Collect_less_Suc_insert"; - - -Goal "{i. i <= Suc n} = insert (Suc n) {i. i <= n}"; -by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1); -qed "Collect_le_Suc_insert"; - - (*a simplification step*) -Goal "(INT i:{i. i <= n}. A(Suc i) Int A i) = \ -\ (INT i:{i. i <= Suc n}. A i)"; +Goal "(INT i: atMost n. A(Suc i) Int A i) = \ +\ (INT i: atMost (Suc n). A i)"; by (induct_tac "n" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc]))); by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1); qed "Collect_le_Int_equals"; (*Dual of the required property. Converse inclusion fails.*) -Goal "(UN i:{i. i < n}. A i) Int -(A n) <= \ -\ (UN i:{i. i < n}. (A i) Int -(A(Suc i)))"; +Goal "(UN i: lessThan n. A i) Int -(A n) <= \ +\ (UN i: lessThan n. (A i) Int -(A(Suc i)))"; by (induct_tac "n" 1); by (Asm_simp_tac 1); -by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1); +by (simp_tac (simpset() addsimps [lessThan_Suc]) 1); by (Blast_tac 1); qed "UN_Int_Compl_subset"; (*Converse inclusion fails.*) -Goal "(INT i:{i. i < n}. -A i Un A (Suc i)) <= \ -\ (INT i:{i. i < n}. -A i) Un A n"; +Goal "(INT i: lessThan n. -A i Un A (Suc i)) <= \ +\ (INT i: lessThan n. -A i) Un A n"; by (induct_tac "n" 1); by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1); +by (asm_simp_tac (simpset() addsimps [lessThan_Suc]) 1); by (Blast_tac 1); qed "INT_Un_Compl_subset"; (*Specialized rewriting*) -Goal "A 0 Int (-(A n) Int (INT i:{i. i < n}. -A i Un A (Suc i))) = {}"; +Goal "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}"; by (blast_tac (claset() addIs [gr0I] addDs [impOfSubs INT_Un_Compl_subset]) 1); val lemma = result(); (*Reverse direction makes it harder to invoke the ind hyp*) -Goal "(INT i:{i. i <= n}. A i) = \ -\ A 0 Int (INT i:{i. i < n}. -A i Un A(Suc i))"; +Goal "(INT i: atMost n. A i) = \ +\ A 0 Int (INT i: lessThan n. -A i Un A(Suc i))"; by (induct_tac "n" 1); by (Asm_simp_tac 1); by (asm_simp_tac (simpset() addsimps Int_ac @ [Int_Un_distrib, Int_Un_distrib2, lemma, - Collect_less_Suc_insert, Collect_le_Suc_insert]) 1); + lessThan_Suc, atMost_Suc]) 1); qed "INT_le_equals_Int"; -Goal "(INT i:{i. i <= Suc n}. A i) = \ -\ A 0 Int (INT i:{i. i <= n}. -A i Un A(Suc i))"; -by (simp_tac (simpset() addsimps [less_Suc_eq_le, INT_le_equals_Int]) 1); +Goal "(INT i: atMost (Suc n). A i) = \ +\ A 0 Int (INT i: atMost n. -A i Un A(Suc i))"; +by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1); qed "INT_le_Suc_equals_Int"; (*The final deadlock example*) val [zeroprem, allprem] = goalw thy [stable_def] - "[| constrains Acts (A 0 Int A (Suc n)) (A 0); \ -\ ALL i:{i. i <= n}. constrains Acts (A(Suc i) Int A i) \ + "[| F : constrains (A 0 Int A (Suc n)) (A 0); \ +\ ALL i: atMost n. F : constrains (A(Suc i) Int A i) \ \ (-A i Un A(Suc i)) |] \ -\ ==> stable Acts (INT i:{i. i <= Suc n}. A i)"; +\ ==> F : stable (INT i: atMost (Suc n). A i)"; by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS constrains_Int RS constrains_weaken) 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/FP.ML --- a/src/HOL/UNITY/FP.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/FP.ML Thu Oct 15 11:35:07 1998 +0200 @@ -8,7 +8,7 @@ From Misra, "A Logic for Concurrent Programming", 1994 *) -Goalw [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)"; +Goalw [FP_Orig_def, stable_def] "F : stable (FP_Orig F Int B)"; by (stac Int_Union2 1); by (rtac ball_constrains_UN 1); by (Simp_tac 1); @@ -16,13 +16,13 @@ val prems = goalw thy [FP_Orig_def, stable_def] - "(!!B. stable Acts (A Int B)) ==> A <= FP_Orig Acts"; + "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"; by (blast_tac (claset() addIs prems) 1); qed "FP_Orig_weakest"; -Goal "stable Acts (FP Acts Int B)"; -by (subgoal_tac "FP Acts Int B = (UN x:B. FP Acts Int {x})" 1); +Goal "F : stable (FP F Int B)"; +by (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x})" 1); by (Blast_tac 2); by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1); by (rewrite_goals_tac [FP_def, stable_def]); @@ -30,31 +30,31 @@ by (Simp_tac 1); qed "stable_FP_Int"; -Goal "FP Acts <= FP_Orig Acts"; +Goal "FP F <= FP_Orig F"; by (rtac (stable_FP_Int RS FP_Orig_weakest) 1); val lemma1 = result(); -Goalw [FP_Orig_def, FP_def] "FP_Orig Acts <= FP Acts"; +Goalw [FP_Orig_def, FP_def] "FP_Orig F <= FP F"; by (Clarify_tac 1); by (dres_inst_tac [("x", "{x}")] spec 1); by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1); val lemma2 = result(); -Goal "FP Acts = FP_Orig Acts"; +Goal "FP F = FP_Orig F"; by (rtac ([lemma1,lemma2] MRS equalityI) 1); qed "FP_equivalence"; val [prem] = goal thy - "(!!B. stable Acts (A Int B)) ==> A <= FP Acts"; + "(!!B. F : stable (A Int B)) ==> A <= FP F"; by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1); qed "FP_weakest"; Goalw [FP_def, stable_def, constrains_def] - "-(FP Acts) = (UN act:Acts. -{s. act^^{s} <= {s}})"; + "-(FP F) = (UN act: Acts F. -{s. act^^{s} <= {s}})"; by (Blast_tac 1); qed "Compl_FP"; -Goal "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})"; +Goal "A - (FP F) = (UN act: Acts F. A - {s. act^^{s} <= {s}})"; by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1); qed "Diff_FP"; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/FP.thy --- a/src/HOL/UNITY/FP.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/FP.thy Thu Oct 15 11:35:07 1998 +0200 @@ -12,10 +12,10 @@ constdefs - FP_Orig :: "('a * 'a)set set => 'a set" - "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}" + FP_Orig :: "'a program => 'a set" + "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}" - FP :: "('a * 'a)set set => 'a set" - "FP Acts == {s. stable Acts {s}}" + FP :: "'a program => 'a set" + "FP F == {s. F : stable {s}}" end diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Handshake.ML --- a/src/HOL/UNITY/Handshake.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Handshake.ML Thu Oct 15 11:35:07 1998 +0200 @@ -11,8 +11,9 @@ (*split_all_tac causes a big blow-up*) claset_ref() := claset() delSWrapper "split_all_tac"; -Addsimps [prgF_def RS def_prg_simps]; -Addsimps [prgG_def RS def_prg_simps]; +Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init]; +program_defs_ref := [F_def, G_def]; + Addsimps (map simp_of_act [cmdF_def, cmdG_def]); (*Simplification for records*) @@ -20,7 +21,7 @@ Addsimps [simp_of_set invFG_def]; -Goal "Invariant (prgF Join prgG) invFG"; +Goal "(F Join G) : Invariant invFG"; by (rtac InvariantI 1); by (Force_tac 1); by (rtac (constrains_imp_Constrains RS StableI) 1); @@ -30,26 +31,26 @@ by (constrains_tac 1); qed "invFG"; -Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \ +Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \ \ ({s. NF s = k} Int {s. BB s})"; by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); by (ensures_tac "cmdG" 2); by (constrains_tac 1); qed "lemma2_1"; -Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}"; +Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}"; by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); by (constrains_tac 2); by (ensures_tac "cmdF" 1); qed "lemma2_2"; -Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}"; +Goal "(F Join G) : LeadsTo UNIV {s. m < NF s}"; by (rtac LeadsTo_weaken_R 1); by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] GreaterThan_bounded_induct 1); by (auto_tac (claset(), simpset() addsimps [vimage_def])); -(*The inductive step: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*) +(*The inductive step: (F Join G) : LeadsTo {x. NF x = ma} {x. ma < NF x}*) by (rtac LeadsTo_Diff 1); by (rtac lemma2_2 2); by (rtac LeadsTo_Trans 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Handshake.thy --- a/src/HOL/UNITY/Handshake.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Handshake.thy Thu Oct 15 11:35:07 1998 +0200 @@ -20,15 +20,15 @@ cmdF :: "(state*state) set" "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" - prgF :: "state program" - "prgF == mk_program ({s. NF s = 0 & BB s}, {cmdF})" + F :: "state program" + "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})" (*G's program*) cmdG :: "(state*state) set" "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" - prgG :: "state program" - "prgG == mk_program ({s. NG s = 0 & BB s}, {cmdG})" + G :: "state program" + "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})" (*the joint invariant*) invFG :: "state set" diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/LessThan.ML --- a/src/HOL/UNITY/LessThan.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/LessThan.ML Thu Oct 15 11:35:07 1998 +0200 @@ -7,6 +7,7 @@ *) +(*Make Auto_tac and Force_tac try trans_tac!*) claset_ref() := claset() addaltern ("trans_tac",trans_tac); @@ -27,6 +28,10 @@ by (Blast_tac 1); qed "lessThan_Suc"; +Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k"; +by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1); +qed "lessThan_Suc_atMost"; + Goal "(UN m. lessThan m) = UNIV"; by (Blast_tac 1); qed "UN_lessThan_UNIV"; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Lift.ML --- a/src/HOL/UNITY/Lift.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Lift.ML Thu Oct 15 11:35:07 1998 +0200 @@ -55,7 +55,8 @@ zless_not_refl2, zless_not_refl3]; -Addsimps [Lprg_def RS def_prg_simps]; +Addsimps [Lprg_def RS def_prg_Init]; +program_defs_ref := [Lprg_def]; Addsimps (map simp_of_act [request_act_def, open_act_def, close_act_def, @@ -69,7 +70,7 @@ val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; -(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *) +(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *) (*Simplification for records*) @@ -87,41 +88,41 @@ val nat_exhaust_pred_le = read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust; -Goal "Invariant Lprg open_stop"; +Goal "Lprg : Invariant open_stop"; by (rtac InvariantI 1); by (Force_tac 1); by (constrains_tac 1); qed "open_stop"; -Goal "Invariant Lprg stop_floor"; +Goal "Lprg : Invariant stop_floor"; by (rtac InvariantI 1); by (Force_tac 1); by (constrains_tac 1); qed "stop_floor"; (*This one needs open_stop, which was proved above*) -Goal "Invariant Lprg open_move"; +Goal "Lprg : Invariant open_move"; by (rtac InvariantI 1); by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2); by (Force_tac 1); by (constrains_tac 1); qed "open_move"; -Goal "Invariant Lprg moving_up"; +Goal "Lprg : Invariant moving_up"; by (rtac InvariantI 1); by (Force_tac 1); by (constrains_tac 1); by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); qed "moving_up"; -Goal "Invariant Lprg moving_down"; +Goal "Lprg : Invariant moving_down"; by (rtac InvariantI 1); by (Force_tac 1); by (constrains_tac 1); by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); qed "moving_down"; -Goal "Invariant Lprg bounded"; +Goal "Lprg : Invariant bounded"; by (rtac InvariantI 1); by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2); by (Force_tac 1); @@ -150,23 +151,23 @@ (** Lift_1 **) -Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)"; +Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)"; by (cut_facts_tac [stop_floor] 1); by (ensures_tac "open_act" 1); qed "E_thm01"; (*lem_lift_1_5*) -Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \ +Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \ \ (Req n Int opened - atFloor n)"; by (cut_facts_tac [stop_floor] 1); by (ensures_tac "open_act" 1); qed "E_thm02"; (*lem_lift_1_1*) -Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \ +Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \ \ (Req n Int closed - (atFloor n - queueing))"; by (ensures_tac "close_act" 1); qed "E_thm03"; (*lem_lift_1_2*) -Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \ +Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \ \ (opened Int atFloor n)"; by (ensures_tac "open_act" 1); qed "E_thm04"; (*lem_lift_1_7*) @@ -190,7 +191,7 @@ (*lem_lift_2_0 NOT an ensures property, but a mere inclusion; don't know why script lift_2.uni says ENSURES*) -Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \ +Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \ \ ((closed Int goingup Int Req n) Un \ \ (closed Int goingdown Int Req n))"; by (rtac subset_imp_LeadsTo 1); @@ -198,7 +199,7 @@ qed "E_thm05c"; (*lift_2*) -Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \ +Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \ \ (moving Int Req n)"; by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1); by (ensures_tac "req_down" 2); @@ -212,7 +213,7 @@ (*lem_lift_4_1 *) Goal "#0 < N ==> \ -\ LeadsTo Lprg \ +\ Lprg : LeadsTo \ \ (moving Int Req n Int {s. metric n s = N} Int \ \ {s. floor s ~: req s} Int {s. up s}) \ \ (moving Int Req n Int {s. metric n s < N})"; @@ -232,7 +233,7 @@ (*lem_lift_4_3 *) Goal "#0 < N ==> \ -\ LeadsTo Lprg \ +\ Lprg : LeadsTo \ \ (moving Int Req n Int {s. metric n s = N} Int \ \ {s. floor s ~: req s} - {s. up s}) \ \ (moving Int Req n Int {s. metric n s < N})"; @@ -250,7 +251,7 @@ qed "E_thm12b"; (*lift_4*) -Goal "#0 LeadsTo Lprg (moving Int Req n Int {s. metric n s = N} Int \ +Goal "#0 Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \ \ {s. floor s ~: req s}) \ \ (moving Int Req n Int {s. metric n s < N})"; by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); @@ -264,7 +265,7 @@ (*lem_lift_5_3*) Goal "#0 LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \ +\ ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \ \ (moving Int Req n Int {s. metric n s < N})"; by (cut_facts_tac [bounded] 1); by (ensures_tac "req_up" 1); @@ -280,7 +281,7 @@ (*lem_lift_5_1 has ~goingup instead of goingdown*) Goal "#0 \ -\ LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \ +\ Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \ \ (moving Int Req n Int {s. metric n s < N})"; by (cut_facts_tac [bounded] 1); by (ensures_tac "req_down" 1); @@ -309,7 +310,7 @@ (*lift_5*) -Goal "#0 LeadsTo Lprg (closed Int Req n Int {s. metric n s = N}) \ +Goal "#0 Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N}) \ \ (moving Int Req n Int {s. metric n s < N})"; by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); by (etac E_thm16b 3); @@ -341,7 +342,7 @@ (*lem_lift_3_1*) -Goal "LeadsTo Lprg (moving Int Req n Int {s. metric n s = #0}) \ +Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0}) \ \ (stopped Int atFloor n)"; by (cut_facts_tac [bounded] 1); by (ensures_tac "request_act" 1); @@ -349,7 +350,7 @@ qed "E_thm11"; (*lem_lift_3_5*) -Goal "LeadsTo Lprg \ +Goal "Lprg : LeadsTo \ \ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ \ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"; by (ensures_tac "request_act" 1); @@ -358,7 +359,7 @@ (*lem_lift_3_6*) Goal "#0 < N ==> \ -\ LeadsTo Lprg \ +\ Lprg : LeadsTo \ \ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ \ (opened Int Req n Int {s. metric n s = N})"; by (ensures_tac "open_act" 1); @@ -367,7 +368,7 @@ qed "E_thm14"; (*lem_lift_3_7*) -Goal "LeadsTo Lprg \ +Goal "Lprg : LeadsTo \ \ (opened Int Req n Int {s. metric n s = N}) \ \ (closed Int Req n Int {s. metric n s = N})"; by (ensures_tac "close_act" 1); @@ -378,7 +379,7 @@ (** the final steps **) Goal "#0 < N ==> \ -\ LeadsTo Lprg \ +\ Lprg : LeadsTo \ \ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ \ (moving Int Req n Int {s. metric n s < N})"; by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5] @@ -399,7 +400,7 @@ val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken; -Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)"; +Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)"; by (rtac (reach_nonneg RS integ_0_le_induct) 1); by (case_tac "#0 < z" 1); (*If z <= #0 then actually z = #0*) @@ -413,7 +414,7 @@ qed "lift_3"; -Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)"; +Goal "Lprg : LeadsTo (Req n) (opened Int atFloor n)"; by (rtac LeadsTo_Trans 1); by (rtac (E_thm04 RS LeadsTo_Un) 2); by (rtac LeadsTo_Un_post 2); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Mutex.ML --- a/src/HOL/UNITY/Mutex.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Mutex.ML Thu Oct 15 11:35:07 1998 +0200 @@ -9,7 +9,8 @@ (*split_all_tac causes a big blow-up*) claset_ref() := claset() delSWrapper "split_all_tac"; -Addsimps [Mprg_def RS def_prg_simps]; +Addsimps [Mprg_def RS def_prg_Init]; +program_defs_ref := [Mprg_def]; Addsimps (map simp_of_act [cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, @@ -21,13 +22,13 @@ (*Simplification for records*) Addsimps (thms"state.update_defs"); -Goal "Invariant Mprg invariantU"; +Goal "Mprg : Invariant invariantU"; by (rtac InvariantI 1); by (constrains_tac 2); by Auto_tac; qed "invariantU"; -Goal "Invariant Mprg invariantV"; +Goal "Mprg : Invariant invariantV"; by (rtac InvariantI 1); by (constrains_tac 2); by Auto_tac; @@ -44,7 +45,7 @@ (*The bad invariant FAILS in cmd1V*) -Goal "Invariant Mprg bad_invariantU"; +Goal "Mprg : Invariant bad_invariantU"; by (rtac InvariantI 1); by (constrains_tac 2); by (Force_tac 1); @@ -77,44 +78,44 @@ (*** Progress for U ***) -Goalw [Unless_def] "Unless Mprg {s. MM s=#2} {s. MM s=#3}"; +Goalw [Unless_def] "Mprg : Unless {s. MM s=#2} {s. MM s=#3}"; by (constrains_tac 1); qed "U_F0"; -Goal "LeadsTo Mprg {s. MM s=#1} {s. PP s = VV s & MM s = #2}"; +Goal "Mprg : LeadsTo {s. MM s=#1} {s. PP s = VV s & MM s = #2}"; by (ensures_tac "cmd1U" 1); qed "U_F1"; -Goal "LeadsTo Mprg {s. ~ PP s & MM s = #2} {s. MM s = #3}"; +Goal "Mprg : LeadsTo {s. ~ PP s & MM s = #2} {s. MM s = #3}"; by (cut_facts_tac [invariantU] 1); by (ensures_tac "cmd2U" 1); qed "U_F2"; -Goal "LeadsTo Mprg {s. MM s = #3} {s. PP s}"; +Goal "Mprg : LeadsTo {s. MM s = #3} {s. PP s}"; by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1); by (ensures_tac "cmd4U" 2); by (ensures_tac "cmd3U" 1); qed "U_F3"; -Goal "LeadsTo Mprg {s. MM s = #2} {s. PP s}"; +Goal "Mprg : LeadsTo {s. MM s = #2} {s. PP s}"; by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); by (auto_tac (claset() addSEs [less_SucE], simpset())); val U_lemma2 = result(); -Goal "LeadsTo Mprg {s. MM s = #1} {s. PP s}"; +Goal "Mprg : LeadsTo {s. MM s = #1} {s. PP s}"; by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val U_lemma1 = result(); -Goal "LeadsTo Mprg {s. #1 <= MM s & MM s <= #3} {s. PP s}"; +Goal "Mprg : LeadsTo {s. #1 <= MM s & MM s <= #3} {s. PP s}"; by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, U_lemma1, U_lemma2, U_F3] ) 1); val U_lemma123 = result(); (*Misra's F4*) -Goal "LeadsTo Mprg {s. UU s} {s. PP s}"; +Goal "Mprg : LeadsTo {s. UU s} {s. PP s}"; by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1); by Auto_tac; qed "u_Leadsto_p"; @@ -123,45 +124,45 @@ (*** Progress for V ***) -Goalw [Unless_def] "Unless Mprg {s. NN s=#2} {s. NN s=#3}"; +Goalw [Unless_def] "Mprg : Unless {s. NN s=#2} {s. NN s=#3}"; by (constrains_tac 1); qed "V_F0"; -Goal "LeadsTo Mprg {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}"; +Goal "Mprg : LeadsTo {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}"; by (ensures_tac "cmd1V" 1); qed "V_F1"; -Goal "LeadsTo Mprg {s. PP s & NN s = #2} {s. NN s = #3}"; +Goal "Mprg : LeadsTo {s. PP s & NN s = #2} {s. NN s = #3}"; by (cut_facts_tac [invariantV] 1); by (ensures_tac "cmd2V" 1); qed "V_F2"; -Goal "LeadsTo Mprg {s. NN s = #3} {s. ~ PP s}"; +Goal "Mprg : LeadsTo {s. NN s = #3} {s. ~ PP s}"; by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1); by (ensures_tac "cmd4V" 2); by (ensures_tac "cmd3V" 1); qed "V_F3"; -Goal "LeadsTo Mprg {s. NN s = #2} {s. ~ PP s}"; +Goal "Mprg : LeadsTo {s. NN s = #2} {s. ~ PP s}"; by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); by (auto_tac (claset() addSEs [less_SucE], simpset())); val V_lemma2 = result(); -Goal "LeadsTo Mprg {s. NN s = #1} {s. ~ PP s}"; +Goal "Mprg : LeadsTo {s. NN s = #1} {s. ~ PP s}"; by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val V_lemma1 = result(); -Goal "LeadsTo Mprg {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}"; +Goal "Mprg : LeadsTo {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}"; by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, V_lemma1, V_lemma2, V_F3] ) 1); val V_lemma123 = result(); (*Misra's F4*) -Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}"; +Goal "Mprg : LeadsTo {s. VV s} {s. ~ PP s}"; by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1); by Auto_tac; qed "v_Leadsto_not_p"; @@ -170,7 +171,7 @@ (** Absence of starvation **) (*Misra's F6*) -Goal "LeadsTo Mprg {s. MM s = #1} {s. MM s = #3}"; +Goal "Mprg : LeadsTo {s. MM s = #1} {s. MM s = #3}"; by (rtac LeadsTo_Un_duplicate 1); by (rtac LeadsTo_cancel2 1); by (rtac U_F2 2); @@ -184,7 +185,7 @@ (*The same for V*) -Goal "LeadsTo Mprg {s. NN s = #1} {s. NN s = #3}"; +Goal "Mprg : LeadsTo {s. NN s = #1} {s. NN s = #3}"; by (rtac LeadsTo_Un_duplicate 1); by (rtac LeadsTo_cancel2 1); by (rtac V_F2 2); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/NSP_Bad.ML --- a/src/HOL/UNITY/NSP_Bad.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/NSP_Bad.ML Thu Oct 15 11:35:07 1998 +0200 @@ -24,6 +24,7 @@ Addsimps [Nprg_def RS def_prg_simps]; + (*A "possibility property": there are traces that reach the end*) Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \ \ Says A B (Crypt (pubK B) (Nonce NB)) : set s"; @@ -32,7 +33,7 @@ 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); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def]))); by (REPEAT_FIRST (rtac exI )); by possibility_tac; result(); @@ -66,7 +67,7 @@ (*Spy never sees another agent's private key! (unless it's bad at start)*) (* - Goal "Invariant Nprg {s. (Key (priK A) : parts (spies s)) = (A : bad)}"; + Goal "Nprg : Invariant {s. (Key (priK A) : parts (spies s)) = (A : bad)}"; by (rtac InvariantI 1); by (Force_tac 1); by (constrains_tac 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Network.ML --- a/src/HOL/UNITY/Network.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Network.ML Thu Oct 15 11:35:07 1998 +0200 @@ -10,15 +10,15 @@ val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = Goalw [stable_def] - "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \ -\ !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \ -\ !! m proc. stable Acts {s. m <= s(proc,Sent)}; \ -\ !! n proc. stable Acts {s. n <= s(proc,Rcvd)}; \ -\ !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \ + "[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \ +\ !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \ +\ !! m proc. F : stable {s. m <= s(proc,Sent)}; \ +\ !! n proc. F : stable {s. n <= s(proc,Rcvd)}; \ +\ !! m proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \ \ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \ -\ !! n proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \ +\ !! n proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \ \ {s. s(proc,Sent) = n} \ -\ |] ==> stable Acts {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \ +\ |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \ \ s(Aproc,Sent) = s(Bproc,Rcvd) & \ \ s(Bproc,Sent) = s(Aproc,Rcvd) & \ \ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}"; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/ROOT.ML Thu Oct 15 11:35:07 1998 +0200 @@ -10,6 +10,10 @@ writeln"Root file for HOL/UNITY"; set proof_timing; + +loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*) +time_use_thy"UNITY"; + time_use_thy "Deadlock"; time_use_thy "WFair"; time_use_thy "Common"; @@ -22,9 +26,7 @@ time_use_thy "Handshake"; time_use_thy "Lift"; time_use_thy "Comp"; +time_use_thy "Client"; loadpath := "../Auth" :: !loadpath; (*to find Public.thy*) use_thy"NSP_Bad"; - -loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*) -use_thy"Client"; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Reach.ML --- a/src/HOL/UNITY/Reach.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Reach.ML Thu Oct 15 11:35:07 1998 +0200 @@ -19,7 +19,8 @@ AddSEs [ifE]; -Addsimps [Rprg_def RS def_prg_simps]; +Addsimps [Rprg_def RS def_prg_Init]; +program_defs_ref := [Rprg_def]; Addsimps [simp_of_act asgt_def]; @@ -28,7 +29,7 @@ Addsimps [simp_of_set reach_invariant_def]; -Goal "Invariant Rprg reach_invariant"; +Goal "Rprg : Invariant reach_invariant"; by (rtac InvariantI 1); by Auto_tac; (*for the initial state; proof of stability remains*) by (constrains_tac 1); @@ -48,20 +49,20 @@ by Auto_tac; qed "fixedpoint_invariant_correct"; -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def] - "FP (Acts Rprg) <= fixedpoint"; +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def] + "FP Rprg <= fixedpoint"; by Auto_tac; by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1); by (dtac fun_cong 1); by Auto_tac; val lemma1 = result(); -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def] - "fixedpoint <= FP (Acts Rprg)"; +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def] + "fixedpoint <= FP Rprg"; by (auto_tac (claset() addSIs [ext], simpset())); val lemma2 = result(); -Goal "FP (Acts Rprg) = fixedpoint"; +Goal "FP Rprg = fixedpoint"; by (rtac ([lemma1,lemma2] MRS equalityI) 1); qed "FP_fixedpoint"; @@ -74,7 +75,7 @@ Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})"; by (simp_tac (simpset() addsimps - ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1); + ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def])) 1); by Auto_tac; by (rtac fun_upd_idem 1); by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff])); @@ -106,7 +107,7 @@ simpset() addsimps [fun_upd_idem])); qed "metric_le"; -Goal "LeadsTo Rprg ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))"; +Goal "Rprg : LeadsTo ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))"; by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1); by (rtac LeadsTo_UN 1); by Auto_tac; @@ -118,7 +119,7 @@ simpset())); qed "LeadsTo_Diff_fixedpoint"; -Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)"; +Goal "Rprg : LeadsTo (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)"; by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R, subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by Auto_tac; @@ -126,13 +127,13 @@ (*Execution in any state leads to a fixedpoint (i.e. can terminate)*) -Goal "LeadsTo Rprg UNIV fixedpoint"; +Goal "Rprg : LeadsTo UNIV fixedpoint"; by (rtac LessThan_induct 1); by Auto_tac; by (rtac LeadsTo_Un_fixedpoint 1); qed "LeadsTo_fixedpoint"; -Goal "LeadsTo Rprg UNIV { %v. (init, v) : edges^* }"; +Goal "Rprg : LeadsTo UNIV { %v. (init, v) : edges^* }"; by (stac (fixedpoint_invariant_correct RS sym) 1); by (rtac ([reach_invariant, LeadsTo_fixedpoint] MRS Invariant_LeadsTo_weaken) 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/SubstAx.ML --- a/src/HOL/UNITY/SubstAx.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/SubstAx.ML Thu Oct 15 11:35:07 1998 +0200 @@ -6,23 +6,21 @@ LeadsTo relation, restricted to the set of reachable states. *) -(*Map its type, ['a program, 'a set, 'a set] => bool, to just 'a*) -Blast.overloaded ("SubstAx.LeadsTo", - HOLogic.dest_setT o domain_type o range_type); +overload_1st_set "SubstAx.LeadsTo"; (*** Specialized laws for handling invariants ***) (** Conjoining a safety property **) -Goal "[| reachable F <= C; LeadsTo F (C Int A) A' |] \ -\ ==> LeadsTo F A A'"; +Goal "[| reachable F <= C; F : LeadsTo (C Int A) A' |] \ +\ ==> F : LeadsTo A A'"; by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1); qed "reachable_LeadsToI"; -Goal "[| reachable F <= C; LeadsTo F A A' |] \ -\ ==> LeadsTo F A (C Int A')"; +Goal "[| reachable F <= C; F : LeadsTo A A' |] \ +\ ==> F : LeadsTo A (C Int A')"; by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1); @@ -31,11 +29,11 @@ (** Conjoining an invariant **) -(* [| Invariant F C; LeadsTo F (C Int A) A' |] ==> LeadsTo F A A' *) +(* [| Invariant F C; F : LeadsTo (C Int A) A' |] ==> F : LeadsTo A A' *) bind_thm ("Invariant_LeadsToI", Invariant_includes_reachable RS reachable_LeadsToI); -(* [| Invariant F C; LeadsTo F A A' |] ==> LeadsTo F A (C Int A') *) +(* [| Invariant F C; F : LeadsTo A A' |] ==> F : LeadsTo A (C Int A') *) bind_thm ("Invariant_LeadsToD", Invariant_includes_reachable RS reachable_LeadsToD); @@ -44,55 +42,54 @@ (*** Introduction rules: Basis, Trans, Union ***) -Goal "leadsTo (Acts F) A B ==> LeadsTo F A B"; +Goal "F : leadsTo A B ==> F : LeadsTo A B"; by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1); qed "leadsTo_imp_LeadsTo"; -Goal "[| LeadsTo F A B; LeadsTo F B C |] ==> LeadsTo F A C"; +Goal "[| F : LeadsTo A B; F : LeadsTo B C |] ==> F : LeadsTo A C"; by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [leadsTo_Trans]) 1); qed "LeadsTo_Trans"; -val [prem] = Goalw [LeadsTo_def] - "(!!A. A : S ==> LeadsTo F A B) ==> LeadsTo F (Union S) B"; +val prems = Goalw [LeadsTo_def] + "(!!A. A : S ==> F : LeadsTo A B) ==> F : LeadsTo (Union S) B"; by (Simp_tac 1); by (stac Int_Union 1); -by (blast_tac (claset() addIs [leadsTo_UN, - simplify (simpset()) prem]) 1); +by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1); qed "LeadsTo_Union"; (*** Derived rules ***) -Goal "LeadsTo F A UNIV"; -by (asm_simp_tac (simpset() addsimps [LeadsTo_def, - Int_lower1 RS subset_imp_leadsTo]) 1); +Goal "F : LeadsTo A UNIV"; +by (asm_simp_tac + (simpset() addsimps [LeadsTo_def, Int_lower1 RS subset_imp_leadsTo]) 1); qed "LeadsTo_UNIV"; Addsimps [LeadsTo_UNIV]; (*Useful with cancellation, disjunction*) -Goal "LeadsTo F A (A' Un A') ==> LeadsTo F A A'"; +Goal "F : LeadsTo A (A' Un A') ==> F : LeadsTo A A'"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "LeadsTo_Un_duplicate"; -Goal "LeadsTo F A (A' Un C Un C) ==> LeadsTo F A (A' Un C)"; +Goal "F : LeadsTo A (A' Un C Un C) ==> F : LeadsTo A (A' Un C)"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "LeadsTo_Un_duplicate2"; val prems = -Goal "(!!i. i : I ==> LeadsTo F (A i) B) ==> LeadsTo F (UN i:I. A i) B"; +Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (UN i:I. A i) B"; by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1); qed "LeadsTo_UN"; (*Binary union introduction rule*) -Goal "[| LeadsTo F A C; LeadsTo F B C |] ==> LeadsTo F (A Un B) C"; +Goal "[| F : LeadsTo A C; F : LeadsTo B C |] ==> F : LeadsTo (A Un B) C"; by (stac Un_eq_Union 1); by (blast_tac (claset() addIs [LeadsTo_Union]) 1); qed "LeadsTo_Un"; -Goal "A <= B ==> LeadsTo F A B"; +Goal "A <= B ==> F : LeadsTo A B"; by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); qed "subset_imp_LeadsTo"; @@ -100,39 +97,39 @@ bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); Addsimps [empty_LeadsTo]; -Goal "[| LeadsTo F A A'; A' <= B' |] ==> LeadsTo F A B'"; +Goal "[| F : LeadsTo A A'; A' <= B' |] ==> F : LeadsTo A B'"; by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); qed_spec_mp "LeadsTo_weaken_R"; -Goal "[| LeadsTo F A A'; B <= A |] \ -\ ==> LeadsTo F B A'"; +Goal "[| F : LeadsTo A A'; B <= A |] \ +\ ==> F : LeadsTo B A'"; by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); qed_spec_mp "LeadsTo_weaken_L"; -Goal "[| LeadsTo F A A'; \ +Goal "[| F : LeadsTo A A'; \ \ B <= A; A' <= B' |] \ -\ ==> LeadsTo F B B'"; +\ ==> F : LeadsTo B B'"; by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L, LeadsTo_Trans]) 1); qed "LeadsTo_weaken"; -Goal "[| reachable F <= C; LeadsTo F A A'; \ +Goal "[| reachable F <= C; F : LeadsTo A A'; \ \ C Int B <= A; C Int A' <= B' |] \ -\ ==> LeadsTo F B B'"; +\ ==> F : LeadsTo B B'"; by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken] addIs [reachable_LeadsToD]) 1); qed "reachable_LeadsTo_weaken"; (** Two theorems for "proof lattices" **) -Goal "[| LeadsTo F A B |] ==> LeadsTo F (A Un B) B"; +Goal "[| F : LeadsTo A B |] ==> F : LeadsTo (A Un B) B"; by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1); qed "LeadsTo_Un_post"; -Goal "[| LeadsTo F A B; LeadsTo F B C |] \ -\ ==> LeadsTo F (A Un B) C"; +Goal "[| F : LeadsTo A B; F : LeadsTo B C |] \ +\ ==> F : LeadsTo (A Un B) C"; by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, LeadsTo_weaken_L, LeadsTo_Trans]) 1); qed "LeadsTo_Trans_Un"; @@ -140,33 +137,33 @@ (** Distributive laws **) -Goal "LeadsTo F (A Un B) C = (LeadsTo F A C & LeadsTo F B C)"; +Goal "(F : LeadsTo (A Un B) C) = (F : LeadsTo A C & F : LeadsTo B C)"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); qed "LeadsTo_Un_distrib"; -Goal "LeadsTo F (UN i:I. A i) B = (ALL i : I. LeadsTo F (A i) B)"; +Goal "(F : LeadsTo (UN i:I. A i) B) = (ALL i : I. F : LeadsTo (A i) B)"; by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); qed "LeadsTo_UN_distrib"; -Goal "LeadsTo F (Union S) B = (ALL A : S. LeadsTo F A B)"; +Goal "(F : LeadsTo (Union S) B) = (ALL A : S. F : LeadsTo A B)"; by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); qed "LeadsTo_Union_distrib"; (** More rules using the premise "Invariant F" **) -Goalw [LeadsTo_def, Constrains_def] - "[| Constrains F (A-A') (A Un A'); transient (Acts F) (A-A') |] \ -\ ==> LeadsTo F A A'"; +Goal "[| F : Constrains (A-A') (A Un A'); F : transient (A-A') |] \ +\ ==> F : LeadsTo A A'"; +by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def]) 1); by (rtac (ensuresI RS leadsTo_Basis) 1); by (blast_tac (claset() addIs [transient_strengthen]) 2); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "LeadsTo_Basis"; -Goal "[| Invariant F INV; \ -\ Constrains F (INV Int (A-A')) (A Un A'); \ -\ transient (Acts F) (INV Int (A-A')) |] \ -\ ==> LeadsTo F A A'"; +Goal "[| F : Invariant INV; \ +\ F : Constrains (INV Int (A-A')) (A Un A'); \ +\ F : transient (INV Int (A-A')) |] \ +\ ==> F : LeadsTo A A'"; by (rtac Invariant_LeadsToI 1); by (assume_tac 1); by (rtac LeadsTo_Basis 1); @@ -174,10 +171,9 @@ by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1); qed "Invariant_LeadsTo_Basis"; -Goal "[| Invariant F INV; \ -\ LeadsTo F A A'; \ -\ INV Int B <= A; INV Int A' <= B' |] \ -\ ==> LeadsTo F B B'"; +Goal "[| F : Invariant INV; \ +\ F : LeadsTo A A'; INV Int B <= A; INV Int A' <= B' |] \ +\ ==> F : LeadsTo B B'"; by (REPEAT (ares_tac [Invariant_includes_reachable, reachable_LeadsTo_weaken] 1)); qed "Invariant_LeadsTo_weaken"; @@ -185,17 +181,15 @@ (*Set difference: maybe combine with leadsTo_weaken_L?? This is the most useful form of the "disjunction" rule*) -Goal "[| LeadsTo F (A-B) C; LeadsTo F (A Int B) C |] \ -\ ==> LeadsTo F A C"; +Goal "[| F : LeadsTo (A-B) C; F : LeadsTo (A Int B) C |] \ +\ ==> F : LeadsTo A C"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); qed "LeadsTo_Diff"; - - val prems = -Goal "(!! i. i:I ==> LeadsTo F (A i) (A' i)) \ -\ ==> LeadsTo F (UN i:I. A i) (UN i:I. A' i)"; +Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \ +\ ==> F : LeadsTo (UN i:I. A i) (UN i:I. A' i)"; by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] addIs prems) 1); @@ -204,22 +198,22 @@ (*Version with no index set*) val prems = -Goal "(!! i. LeadsTo F (A i) (A' i)) \ -\ ==> LeadsTo F (UN i. A i) (UN i. A' i)"; +Goal "(!! i. F : LeadsTo (A i) (A' i)) \ +\ ==> F : LeadsTo (UN i. A i) (UN i. A' i)"; by (blast_tac (claset() addIs [LeadsTo_UN_UN] addIs prems) 1); qed "LeadsTo_UN_UN_noindex"; (*Version with no index set*) -Goal "ALL i. LeadsTo F (A i) (A' i) \ -\ ==> LeadsTo F (UN i. A i) (UN i. A' i)"; +Goal "ALL i. F : LeadsTo (A i) (A' i) \ +\ ==> F : LeadsTo (UN i. A i) (UN i. A' i)"; by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); qed "all_LeadsTo_UN_UN"; (*Binary union version*) -Goal "[| LeadsTo F A A'; LeadsTo F B B' |] \ -\ ==> LeadsTo F (A Un B) (A' Un B')"; +Goal "[| F : LeadsTo A A'; F : LeadsTo B B' |] \ +\ ==> F : LeadsTo (A Un B) (A' Un B')"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_R]) 1); qed "LeadsTo_Un_Un"; @@ -227,38 +221,37 @@ (** The cancellation law **) -Goal "[| LeadsTo F A (A' Un B); LeadsTo F B B' |] \ -\ ==> LeadsTo F A (A' Un B')"; +Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo B B' |] \ +\ ==> F : LeadsTo A (A' Un B')"; by (blast_tac (claset() addIs [LeadsTo_Un_Un, subset_imp_LeadsTo, LeadsTo_Trans]) 1); qed "LeadsTo_cancel2"; -Goal "[| LeadsTo F A (A' Un B); LeadsTo F (B-A') B' |] \ -\ ==> LeadsTo F A (A' Un B')"; +Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo (B-A') B' |] \ +\ ==> F : LeadsTo A (A' Un B')"; by (rtac LeadsTo_cancel2 1); by (assume_tac 2); by (ALLGOALS Asm_simp_tac); qed "LeadsTo_cancel_Diff2"; -Goal "[| LeadsTo F A (B Un A'); LeadsTo F B B' |] \ -\ ==> LeadsTo F A (B' Un A')"; +Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo B B' |] \ +\ ==> F : LeadsTo A (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 "[| LeadsTo F A (B Un A'); LeadsTo F (B-A') B' |] \ -\ ==> LeadsTo F A (B' Un A')"; +Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo (B-A') B' |] \ +\ ==> F : LeadsTo A (B' Un A')"; by (rtac LeadsTo_cancel1 1); by (assume_tac 2); by (ALLGOALS Asm_simp_tac); qed "LeadsTo_cancel_Diff1"; - (** The impossibility law **) (*The set "A" may be non-empty, but it contains no reachable states*) -Goal "LeadsTo F A {} ==> reachable F Int A = {}"; +Goal "F : LeadsTo A {} ==> reachable F Int A = {}"; by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (etac leadsTo_empty 1); qed "LeadsTo_empty"; @@ -267,32 +260,33 @@ (** PSP: Progress-Safety-Progress **) (*Special case of PSP: Misra's "stable conjunction"*) -Goal "[| LeadsTo F A A'; Stable F B |] ==> LeadsTo F (A Int B) (A' Int B)"; +Goal "[| F : LeadsTo A A'; F : Stable B |] \ +\ ==> F : LeadsTo (A Int B) (A' Int B)"; by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1); by (dtac psp_stable 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps Int_ac) 1); qed "PSP_stable"; -Goal "[| LeadsTo F A A'; Stable F B |] \ -\ ==> LeadsTo F (B Int A) (B Int A')"; +Goal "[| F : LeadsTo A A'; F : Stable B |] \ +\ ==> F : LeadsTo (B Int A) (B Int A')"; by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1); qed "PSP_stable2"; Goalw [LeadsTo_def, Constrains_def] - "[| LeadsTo F A A'; Constrains F B B' |] \ -\ ==> LeadsTo F (A Int B) ((A' Int B) Un (B' - B))"; + "[| F : LeadsTo A A'; F : Constrains B B' |] \ +\ ==> F : LeadsTo (A Int B) ((A' Int B) Un (B' - B))"; by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1); qed "PSP"; -Goal "[| LeadsTo F A A'; Constrains F B B' |] \ -\ ==> LeadsTo F (B Int A) ((B Int A') Un (B' - B))"; +Goal "[| F : LeadsTo A A'; F : Constrains B B' |] \ +\ ==> F : LeadsTo (B Int A) ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1); qed "PSP2"; Goalw [Unless_def] - "[| LeadsTo F A A'; Unless F B B' |] \ -\ ==> LeadsTo F (A Int B) ((A' Int B) Un B')"; + "[| F : LeadsTo A A'; F : Unless B B' |] \ +\ ==> F : LeadsTo (A Int B) ((A' Int B) Un B')"; by (dtac PSP 1); by (assume_tac 1); by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, @@ -304,20 +298,19 @@ (** Meta or object quantifier ????? **) Goal "[| wf r; \ -\ ALL m. LeadsTo F (A Int f-``{m}) \ +\ ALL m. F : LeadsTo (A Int f-``{m}) \ \ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ -\ ==> LeadsTo F A B"; +\ ==> F : LeadsTo A B"; by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (etac leadsTo_wf_induct 1); -by (Simp_tac 2); by (blast_tac (claset() addIs [leadsTo_weaken]) 1); qed "LeadsTo_wf_induct"; Goal "[| wf r; \ -\ ALL m:I. LeadsTo F (A Int f-``{m}) \ +\ ALL m:I. F : LeadsTo (A Int f-``{m}) \ \ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ -\ ==> LeadsTo F A ((A - (f-``I)) Un B)"; +\ ==> F : LeadsTo A ((A - (f-``I)) Un B)"; by (etac LeadsTo_wf_induct 1); by Safe_tac; by (case_tac "m:I" 1); @@ -326,9 +319,9 @@ qed "Bounded_induct"; -Goal "[| ALL m. LeadsTo F (A Int f-``{m}) \ +Goal "[| ALL m. F : LeadsTo (A Int f-``{m}) \ \ ((A Int f-``(lessThan m)) Un B) |] \ -\ ==> LeadsTo F A B"; +\ ==> F : LeadsTo A B"; by (rtac (wf_less_than RS LeadsTo_wf_induct) 1); by (Asm_simp_tac 1); qed "LessThan_induct"; @@ -336,26 +329,26 @@ (*Integer version. Could generalize from #0 to any lower bound*) val [reach, prem] = Goal "[| reachable F <= {s. #0 <= f s}; \ -\ !! z. LeadsTo F (A Int {s. f s = z}) \ +\ !! z. F : LeadsTo (A Int {s. f s = z}) \ \ ((A Int {s. f s < z}) Un B) |] \ -\ ==> LeadsTo F A B"; +\ ==> F : LeadsTo A B"; by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1); by (simp_tac (simpset() addsimps [vimage_def]) 1); by (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1); by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff])); qed "integ_0_le_induct"; -Goal "[| ALL m:(greaterThan l). LeadsTo F (A Int f-``{m}) \ +Goal "[| ALL m:(greaterThan l). F : LeadsTo (A Int f-``{m}) \ \ ((A Int f-``(lessThan m)) Un B) |] \ -\ ==> LeadsTo F A ((A Int (f-``(atMost l))) Un B)"; +\ ==> F : LeadsTo A ((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 "[| ALL m:(lessThan l). LeadsTo F (A Int f-``{m}) \ +Goal "[| ALL m:(lessThan l). F : LeadsTo (A Int f-``{m}) \ \ ((A Int f-``(greaterThan m)) Un B) |] \ -\ ==> LeadsTo F A ((A Int (f-``(atLeast l))) Un B)"; +\ ==> F : LeadsTo A ((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); @@ -368,27 +361,27 @@ (*** Completion: Binary and General Finite versions ***) -Goal "[| LeadsTo F A A'; Stable F A'; \ -\ LeadsTo F B B'; Stable F B' |] \ -\ ==> LeadsTo F (A Int B) (A' Int B')"; +Goal "[| F : LeadsTo A A'; F : Stable A'; \ +\ F : LeadsTo B B'; F : Stable B' |] \ +\ ==> F : LeadsTo (A Int B) (A' Int B')"; by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1); by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1); qed "Stable_completion"; Goal "finite I \ -\ ==> (ALL i:I. LeadsTo F (A i) (A' i)) --> \ -\ (ALL i:I. Stable F (A' i)) --> \ -\ LeadsTo F (INT i:I. A i) (INT i:I. A' i)"; +\ ==> (ALL i:I. F : LeadsTo (A i) (A' i)) --> \ +\ (ALL i:I. F : Stable (A' i)) --> \ +\ F : LeadsTo (INT i:I. A i) (INT i:I. A' i)"; by (etac finite_induct 1); by (Asm_simp_tac 1); by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1); qed_spec_mp "Finite_stable_completion"; -Goal "[| LeadsTo F A (A' Un C); Constrains F A' (A' Un C); \ -\ LeadsTo F B (B' Un C); Constrains F B' (B' Un C) |] \ -\ ==> LeadsTo F (A Int B) ((A' Int B') Un C)"; +Goal "[| F : LeadsTo A (A' Un C); F : Constrains A' (A' Un C); \ +\ F : LeadsTo B (B' Un C); F : Constrains B' (B' Un C) |] \ +\ ==> F : LeadsTo (A Int B) ((A' Int B') Un C)"; by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def, Int_Un_distrib]) 1); by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1); @@ -396,9 +389,9 @@ Goal "[| finite I |] \ -\ ==> (ALL i:I. LeadsTo F (A i) (A' i Un C)) --> \ -\ (ALL i:I. Constrains F (A' i) (A' i Un C)) --> \ -\ LeadsTo F (INT i:I. A i) ((INT i:I. A' i) Un C)"; +\ ==> (ALL i:I. F : LeadsTo (A i) (A' i Un C)) --> \ +\ (ALL i:I. F : Constrains (A' i) (A' i Un C)) --> \ +\ F : LeadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)"; by (etac finite_induct 1); by (ALLGOALS Asm_simp_tac); by (Clarify_tac 1); @@ -414,6 +407,8 @@ etac Invariant_LeadsTo_Basis 1 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1), + (*now there are two subgoals: constrains & transient*) + simp_tac (simpset() addsimps !program_defs_ref) 2, res_inst_tac [("act", sact)] transient_mem 2, (*simplify the command's domain*) simp_tac (simpset() addsimps [Domain_def]) 3, diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/SubstAx.thy Thu Oct 15 11:35:07 1998 +0200 @@ -10,9 +10,7 @@ constdefs - LeadsTo :: "['a program, 'a set, 'a set] => bool" - "LeadsTo F A B == - leadsTo (Acts F) - (reachable F Int A) - (reachable F Int B)" + LeadsTo :: "['a set, 'a set] => 'a program set" + "LeadsTo A B == {F. F : leadsTo (reachable F Int A) + (reachable F Int B)}" end diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Token.ML --- a/src/HOL/UNITY/Token.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Token.ML Thu Oct 15 11:35:07 1998 +0200 @@ -32,9 +32,9 @@ val nodeOrder_def = (thm "nodeOrder_def"); val next_def = (thm "next_def"); -AddIffs [thm "N_positive", thm"skip"]; +AddIffs [thm "N_positive"]; -Goalw [stable_def] "stable acts (-(E i) Un (HasTok i))"; +Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))"; by (rtac constrains_weaken 1); by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1); by (auto_tac (claset(), simpset() addsimps [not_E_eq])); @@ -70,7 +70,7 @@ (*From "A Logic for Concurrent Programming", but not used in Chapter 4. Note the use of case_tac. Reasoning about leadsTo takes practice!*) Goal "[| i \ -\ leadsTo acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)"; +\ F : leadsTo (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)"; by (case_tac "i=j" 1); by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); by (rtac (TR7 RS leadsTo_weaken_R) 1); @@ -81,7 +81,7 @@ (*Chapter 4 variant, the one actually used below.*) Goal "[| i leadsTo acts (HasTok i) {s. (token s, i) : nodeOrder j}"; +\ ==> F : leadsTo (HasTok i) {s. (token s, i) : nodeOrder j}"; by (rtac (TR7 RS leadsTo_weaken_R) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); @@ -94,7 +94,7 @@ (*Misra's TR9: the token reaches an arbitrary node*) -Goal "j leadsTo acts {s. token s < N} (HasTok j)"; +Goal "j F : leadsTo {s. token s < N} (HasTok j)"; by (rtac leadsTo_weaken_R 1); by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] (wf_nodeOrder RS bounded_induct) 1); @@ -108,7 +108,7 @@ qed "leadsTo_j"; (*Misra's TR8: a hungry process eventually eats*) -Goal "j leadsTo acts ({s. token s < N} Int H j) (E j)"; +Goal "j F : leadsTo ({s. token s < N} Int H j) (E j)"; by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); by (rtac TR6 2); by (rtac leadsTo_weaken_R 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Token.thy --- a/src/HOL/UNITY/Token.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Token.thy Thu Oct 15 11:35:07 1998 +0200 @@ -36,26 +36,24 @@ locale Token = fixes N :: nat (*number of nodes in the ring*) - acts :: "(state*state)set set" + F :: state program nodeOrder :: "nat => (nat*nat)set" next :: nat => nat assumes N_positive "0 Init F = init"; +by (rewtac rew); +by Auto_tac; +qed "def_prg_Init"; + +(*The program is not expanded, but its Init and Acts are*) val [rew] = goal thy "[| F == mk_program (init,acts) |] \ \ ==> Init F = init & Acts F = insert Id acts"; @@ -52,6 +61,7 @@ by Auto_tac; qed "def_prg_simps"; +(*An action is expanded only if a pair of states is being tested against it*) val [rew] = goal thy "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; by (rewtac rew); @@ -60,8 +70,9 @@ fun simp_of_act def = def RS def_act_simp; +(*A set is expanded only if an element is being tested against it*) val [rew] = goal thy - "[| A == B |] ==> (x : A) = (x : B)"; + "A == B ==> (x : A) = (x : B)"; by (rewtac rew); by Auto_tac; qed "def_set_simp"; @@ -77,11 +88,3 @@ 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 <= Acts F ==> stable acts (reachable F)"; -by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1); -qed "stable_reachable"; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Traces.thy --- a/src/HOL/UNITY/Traces.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Traces.thy Thu Oct 15 11:35:07 1998 +0200 @@ -8,7 +8,7 @@ * reachable: the set of reachable states *) -Traces = UNITY + +Traces = LessThan + consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/UNITY.ML Thu Oct 15 11:35:07 1998 +0200 @@ -14,154 +14,216 @@ (*** constrains ***) -(*Map the type (anything => ('a set => anything) to just 'a*) -fun overload_2nd_set s = - Blast.overloaded (s, HOLogic.dest_setT o domain_type o range_type); - -overload_2nd_set "UNITY.constrains"; -overload_2nd_set "UNITY.stable"; -overload_2nd_set "UNITY.unless"; +overload_1st_set "UNITY.constrains"; +overload_1st_set "UNITY.stable"; +overload_1st_set "UNITY.unless"; val prems = Goalw [constrains_def] - "(!!act s s'. [| act: acts; (s,s') : act; s: A |] ==> s': A') \ -\ ==> constrains acts A A'"; + "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ +\ ==> F : constrains A A'"; by (blast_tac (claset() addIs prems) 1); qed "constrainsI"; Goalw [constrains_def] - "[| constrains acts A A'; act: acts; (s,s'): act; s: A |] ==> s': A'"; + "[| F : constrains A A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'"; by (Blast_tac 1); qed "constrainsD"; -Goalw [constrains_def] "constrains acts {} B"; +Goalw [constrains_def] "F : constrains {} B"; by (Blast_tac 1); qed "constrains_empty"; -Goalw [constrains_def] "constrains acts A UNIV"; +Goalw [constrains_def] "F : constrains A UNIV"; by (Blast_tac 1); qed "constrains_UNIV"; AddIffs [constrains_empty, constrains_UNIV]; +(*monotonic in 2nd argument*) Goalw [constrains_def] - "[| constrains acts A A'; A'<=B' |] ==> constrains acts A B'"; + "[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'"; by (Blast_tac 1); qed "constrains_weaken_R"; +(*anti-monotonic in 1st argument*) Goalw [constrains_def] - "[| constrains acts A A'; B<=A |] ==> constrains acts B A'"; + "[| F : constrains A A'; B<=A |] ==> F : constrains B A'"; by (Blast_tac 1); qed "constrains_weaken_L"; Goalw [constrains_def] - "[| constrains acts A A'; B<=A; A'<=B' |] ==> constrains acts B B'"; + "[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'"; by (Blast_tac 1); qed "constrains_weaken"; (** Union **) Goalw [constrains_def] - "[| constrains acts A A'; constrains acts B B' |] \ -\ ==> constrains acts (A Un B) (A' Un B')"; + "[| F : constrains A A'; F : constrains B B' |] \ +\ ==> F : constrains (A Un B) (A' Un B')"; by (Blast_tac 1); qed "constrains_Un"; Goalw [constrains_def] - "ALL i:I. constrains acts (A i) (A' i) \ -\ ==> constrains acts (UN i:I. A i) (UN i:I. A' i)"; + "ALL i:I. F : constrains (A i) (A' i) \ +\ ==> F : constrains (UN i:I. A i) (UN i:I. A' i)"; by (Blast_tac 1); qed "ball_constrains_UN"; Goalw [constrains_def] - "[| ALL i. constrains acts (A i) (A' i) |] \ -\ ==> constrains acts (UN i. A i) (UN i. A' i)"; + "[| ALL i. F : constrains (A i) (A' i) |] \ +\ ==> F : constrains (UN i. A i) (UN i. A' i)"; by (Blast_tac 1); qed "all_constrains_UN"; (** Intersection **) Goalw [constrains_def] - "[| constrains acts A A'; constrains acts B B' |] \ -\ ==> constrains acts (A Int B) (A' Int B')"; + "[| F : constrains A A'; F : constrains B B' |] \ +\ ==> F : constrains (A Int B) (A' Int B')"; by (Blast_tac 1); qed "constrains_Int"; Goalw [constrains_def] - "ALL i:I. constrains acts (A i) (A' i) \ -\ ==> constrains acts (INT i:I. A i) (INT i:I. A' i)"; + "ALL i:I. F : constrains (A i) (A' i) \ +\ ==> F : constrains (INT i:I. A i) (INT i:I. A' i)"; by (Blast_tac 1); qed "ball_constrains_INT"; Goalw [constrains_def] - "[| ALL i. constrains acts (A i) (A' i) |] \ -\ ==> constrains acts (INT i. A i) (INT i. A' i)"; + "[| ALL i. F : constrains (A i) (A' i) |] \ +\ ==> F : constrains (INT i. A i) (INT i. A' i)"; by (Blast_tac 1); qed "all_constrains_INT"; -Goalw [constrains_def] "[| constrains acts A A'; Id: acts |] ==> A<=A'"; +Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'"; by (Blast_tac 1); qed "constrains_imp_subset"; Goalw [constrains_def] - "[| Id: acts; constrains acts A B; constrains acts B C |] \ -\ ==> constrains acts A C"; + "[| F : constrains A B; F : constrains B C |] \ +\ ==> F : constrains A C"; by (Blast_tac 1); qed "constrains_trans"; (*** stable ***) -Goalw [stable_def] "constrains acts A A ==> stable acts A"; +Goalw [stable_def] "F : constrains A A ==> F : stable A"; by (assume_tac 1); qed "stableI"; -Goalw [stable_def] "stable acts A ==> constrains acts A A"; +Goalw [stable_def] "F : stable A ==> F : constrains A A"; by (assume_tac 1); qed "stableD"; Goalw [stable_def] - "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')"; + "[| 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] - "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')"; + "[| 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, constrains_def] - "[| stable acts C; constrains acts A (C Un A') |] \ -\ ==> constrains acts (C Un A) (C Un A')"; + "[| F : stable C; F : constrains A (C Un A') |] \ +\ ==> F : constrains (C Un A) (C Un A')"; by (Blast_tac 1); qed "stable_constrains_Un"; Goalw [stable_def, constrains_def] - "[| stable acts C; constrains acts (C Int A) A' |] \ -\ ==> constrains acts (C Int A) (C Int A')"; + "[| F : stable C; F : constrains (C Int A) A' |] \ +\ ==> F : constrains (C Int A) (C Int A')"; by (Blast_tac 1); qed "stable_constrains_Int"; +Goal "Init F <= reachable F"; +by (blast_tac (claset() addIs reachable.intrs) 1); +qed "Init_subset_reachable"; -(*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.*) +Goal "Acts G <= Acts F ==> G : stable (reachable F)"; +by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1); +qed "stable_reachable"; + +(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*) +bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); + + +(*** invariant & always ***) + +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"; + +(*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 (stable_reachable::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"; + +Goalw [always_def] "always A = (UN I: Pow A. invariant I)"; +by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, + stable_reachable, + impOfSubs invariant_includes_reachable]) 1); +qed "always_eq_UN_invariant"; + +Goal "F : always A = (EX I. F: invariant I & I <= A)"; +by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1); +by (Blast_tac 1); +qed "always_iff_ex_invariant"; + + +(*** increasing ***) + +Goalw [increasing_def, stable_def, constrains_def] + "increasing f <= increasing (length o f)"; +by Auto_tac; +by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1); +qed "increasing_length"; + +Goalw [increasing_def] + "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}"; +by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); +by (Blast_tac 1); +qed "increasing_less"; + + +(** 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. constrains acts {s. s x = m} (B m) |] \ -\ ==> constrains acts {s. s x : M} (UN m:M. B m)"; + "[| ALL m. F : constrains {s. s x = m} (B m) |] \ +\ ==> F : constrains {s. s x : M} (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. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)"; + "(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)"; by (Blast_tac 1); qed "elimination_sing"; Goalw [constrains_def] - "[| constrains acts A (A' Un B); constrains acts B B'; Id: acts |] \ -\ ==> constrains acts A (A' Un B')"; + "[| F : constrains A (A' Un B); F : constrains B B' |] \ +\ ==> F : constrains A (A' Un B')"; by (Blast_tac 1); qed "constrains_cancel"; @@ -170,11 +232,11 @@ (*** Theoretical Results from Section 6 ***) Goalw [constrains_def, strongest_rhs_def] - "constrains acts A (strongest_rhs acts A )"; + "F : constrains A (strongest_rhs F A )"; by (Blast_tac 1); qed "constrains_strongest_rhs"; Goalw [constrains_def, strongest_rhs_def] - "constrains acts A B ==> strongest_rhs acts A <= B"; + "F : constrains A B ==> strongest_rhs F A <= B"; by (Blast_tac 1); qed "strongest_rhs_is_strongest"; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/UNITY.thy Thu Oct 15 11:35:07 1998 +0200 @@ -8,20 +8,33 @@ From Misra, "A Logic for Concurrent Programming", 1994 *) -UNITY = LessThan + +UNITY = Traces + Prefix + constdefs - constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool" - "constrains acts A B == ALL act:acts. act^^A <= B" + constrains :: "['a set, 'a set] => 'a program set" + "constrains A B == {F. ALL act: Acts F. act^^A <= B}" + + stable :: "'a set => 'a program set" + "stable A == constrains A A" - stable :: "('a * 'a)set set => 'a set => bool" - "stable acts A == constrains acts A A" + strongest_rhs :: "['a program, 'a set] => 'a set" + "strongest_rhs F A == Inter {B. F : constrains A B}" + + unless :: "['a set, 'a set] => 'a program set" + "unless A B == constrains (A-B) (A Un B)" - strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set" - "strongest_rhs acts A == Inter {B. constrains acts A B}" + (*The traditional word for inductive properties. Anyway, INDUCTIVE is + reserved!*) + invariant :: "'a set => 'a program set" + "invariant A == {F. Init F <= A} Int stable A" - unless :: "[('a * 'a)set set, 'a set, 'a set] => bool" - "unless acts A B == constrains acts (A-B) (A Un B)" + (*Safety properties*) + always :: "'a set => 'a program set" + "always A == {F. reachable F <= A}" + + (*Polymorphic in both states and the meaning of <= *) + increasing :: "['a => 'b::{ord}] => 'a program set" + "increasing f == INT z. stable {s. z <= f s}" end diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Union.ML --- a/src/HOL/UNITY/Union.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Union.ML Thu Oct 15 11:35:07 1998 +0200 @@ -9,10 +9,16 @@ *) -Goal "Init (F Join G) = Init F Int Init G"; -by (simp_tac (simpset() addsimps [Join_def]) 1); +Goal "Init SKIP = UNIV"; +by (simp_tac (simpset() addsimps [SKIP_def]) 1); qed "Init_SKIP"; +Goal "Acts SKIP = {Id}"; +by (simp_tac (simpset() addsimps [SKIP_def]) 1); +qed "Acts_SKIP"; + +Addsimps [Init_SKIP, Acts_SKIP]; + Goal "Init (F Join G) = Init F Int Init G"; by (simp_tac (simpset() addsimps [Join_def]) 1); qed "Init_Join"; @@ -79,14 +85,13 @@ Goalw [constrains_def, JOIN_def] "I ~= {} ==> \ -\ constrains (Acts (JN i:I. F i)) A B = \ -\ (ALL i:I. constrains (Acts (F i)) A B)"; +\ (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)"; by (Simp_tac 1); by (Blast_tac 1); qed "constrains_JN"; -Goal "constrains (Acts (F Join G)) A B = \ -\ (constrains (Acts F) A B & constrains (Acts G) A B)"; +Goal "F Join G : constrains A B = \ +\ (F : constrains A B & G : constrains A B)"; by (auto_tac (claset(), simpset() addsimps [constrains_def, Join_def])); @@ -97,35 +102,35 @@ reachable F and reachable G Goalw [Constrains_def] - "Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)"; + "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)"; by (simp_tac (simpset() addsimps [constrains_JN]) 1); by (Blast_tac 1); qed "Constrains_JN"; -Goal "Constrains (F Join G) A B = (Constrains F A B & Constrains G A B)"; +Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)"; by (auto_tac (claset(), simpset() addsimps [Constrains_def, constrains_Join])); qed "Constrains_Join"; **) -Goal "[| constrains (Acts F) A A'; constrains (Acts G) B B' |] \ -\ ==> constrains (Acts (F Join G)) (A Int B) (A' Un B')"; +Goal "[| F : constrains A A'; G : constrains B B' |] \ +\ ==> F Join G : constrains (A Int B) (A' Un B')"; by (simp_tac (simpset() addsimps [constrains_Join]) 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "constrains_Join_weaken"; Goal "I ~= {} ==> \ -\ stable (Acts (JN i:I. F i)) A = (ALL i:I. stable (Acts (F i)) A)"; +\ (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"; by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1); qed "stable_JN"; -Goal "stable (Acts (F Join G)) A = \ -\ (stable (Acts F) A & stable (Acts G) A)"; +Goal "F Join G : stable A = \ +\ (F : stable A & G : stable A)"; by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1); qed "stable_Join"; -Goal "I ~= {} ==> FP (Acts (JN i:I. F i)) = (INT i:I. FP (Acts (F i)))"; +Goal "I ~= {} ==> FP (JN i:I. F i) = (INT i:I. FP (F i))"; by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1); qed "FP_JN"; @@ -133,54 +138,52 @@ (*** Progress: transient, ensures ***) Goal "I ~= {} ==> \ -\ transient (Acts (JN i:I. F i)) A = (EX i:I. transient (Acts (F i)) A)"; +\ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"; by (auto_tac (claset(), simpset() addsimps [transient_def, JOIN_def])); qed "transient_JN"; -Goal "transient (Acts (F Join G)) A = \ -\ (transient (Acts F) A | transient (Acts G) A)"; +Goal "F Join G : transient A = \ +\ (F : transient A | G : transient A)"; by (auto_tac (claset(), simpset() addsimps [bex_Un, transient_def, Join_def])); qed "transient_Join"; Goal "I ~= {} ==> \ -\ ensures (Acts (JN i:I. F i)) A B = \ -\ ((ALL i:I. constrains (Acts (F i)) (A-B) (A Un B)) & \ -\ (EX i:I. ensures (Acts (F i)) A B))"; +\ (JN i:I. F i) : ensures A B = \ +\ ((ALL i:I. F i : constrains (A-B) (A Un B)) & \ +\ (EX i:I. F i : ensures A B))"; by (auto_tac (claset(), simpset() addsimps [ensures_def, constrains_JN, transient_JN])); qed "ensures_JN"; Goalw [ensures_def] - "ensures (Acts (F Join G)) A B = \ -\ (constrains (Acts F) (A-B) (A Un B) & \ -\ constrains (Acts G) (A-B) (A Un B) & \ -\ (ensures (Acts F) A B | ensures (Acts G) A B))"; + "F Join G : ensures A B = \ +\ (F : constrains (A-B) (A Un B) & \ +\ G : constrains (A-B) (A Un B) & \ +\ (F : ensures A B | G : ensures A B))"; by (auto_tac (claset(), simpset() addsimps [constrains_Join, transient_Join])); qed "ensures_Join"; Goalw [stable_def, constrains_def, Join_def] - "[| stable (Acts F) A; constrains (Acts G) A A' |] \ -\ ==> constrains (Acts (F Join G)) A A'"; -by (asm_simp_tac (simpset() addsimps [ball_Un]) 1); + "[| F : stable A; G : constrains A A' |] \ +\ ==> F Join G : constrains A A'"; +by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1); by (Blast_tac 1); qed "stable_constrains_Join"; -(*Premises cannot use Invariant because Stable F A is weaker than - stable (Acts G) A *) -Goal "[| stable (Acts F) A; Init G <= A; stable (Acts G) A |] \ -\ ==> Invariant (F Join G) A"; -by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable, - stable_Join]) 1); +(*Premise for G cannot use Invariant because Stable F A is weaker than + G : stable A *) +Goal "[| F : stable A; G : invariant A |] ==> F Join G : Invariant A"; +by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, + Stable_eq_stable, stable_Join]) 1); by (force_tac(claset() addIs [stable_reachable, stable_Int], simpset() addsimps [Acts_Join]) 1); qed "stable_Join_Invariant"; -Goal "[| stable (Acts F) A; ensures (Acts G) A B |] \ -\ ==> ensures (Acts (F Join G)) A B"; +Goal "[| F : stable A; G : ensures A B |] ==> F Join G : ensures A B"; by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1); by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); by (etac constrains_weaken 1); @@ -188,9 +191,18 @@ qed "ensures_stable_Join1"; (*As above, but exchanging the roles of F and G*) -Goal "[| ensures (Acts F) A B; stable (Acts G) A |] \ -\ ==> ensures (Acts (F Join G)) A B"; +Goal "[| F : ensures A B; G : stable A |] ==> F Join G : ensures A B"; by (stac Join_commute 1); by (blast_tac (claset() addIs [ensures_stable_Join1]) 1); qed "ensures_stable_Join2"; + +(** localTo **) + +Goal "[| F Join G : f localTo F; (s,s') : act; \ +\ act : Acts G; act ~: Acts F |] ==> f s' = f s"; +by (asm_full_simp_tac + (simpset() addsimps [localTo_def, Diff_def, Acts_Join, stable_def, + constrains_def]) 1); +by (Blast_tac 1); +qed "localTo_imp_equals"; diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/Union.thy Thu Oct 15 11:35:07 1998 +0200 @@ -11,15 +11,22 @@ Union = SubstAx + FP + constdefs - JOIN :: ['a set, 'a => 'b program] => 'b program + JOIN :: ['a set, 'a => 'b program] => 'b program "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))" - Join :: ['a program, 'a program] => 'a program (infixl 65) + Join :: ['a program, 'a program] => 'a program (infixl 65) "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)" - SKIP :: 'a program + SKIP :: 'a program "SKIP == mk_program (UNIV, {})" + Diff :: "['a program, ('a * 'a)set set] => 'a program" + "Diff F acts == mk_program (Init F, Acts F - acts)" + + (*The set of systems that regard "f" as local to F*) + localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80) + "f localTo F == {G. ALL z. Diff G (Acts F) : stable {s. f s = z}}" + syntax "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10) diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/WFair.ML --- a/src/HOL/UNITY/WFair.ML Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/WFair.ML Thu Oct 15 11:35:07 1998 +0200 @@ -9,30 +9,26 @@ *) -(*Map its type, [('a * 'a)set set] => ('a set * 'a set) set, to just 'a*) -Blast.overloaded ("WFair.leadsto", - #1 o HOLogic.dest_prodT o - HOLogic.dest_setT o HOLogic.dest_setT o domain_type); - -overload_2nd_set "WFair.transient"; -overload_2nd_set "WFair.ensures"; +overload_1st_set "WFair.transient"; +overload_1st_set "WFair.ensures"; +overload_1st_set "WFair.leadsTo"; (*** transient ***) Goalw [stable_def, constrains_def, transient_def] - "[| stable acts A; transient acts A |] ==> A = {}"; + "[| F : stable A; F : transient A |] ==> A = {}"; by (Blast_tac 1); qed "stable_transient_empty"; Goalw [transient_def] - "[| transient acts A; B<=A |] ==> transient acts B"; + "[| F : transient A; B<=A |] ==> F : transient B"; by (Clarify_tac 1); by (rtac bexI 1 THEN assume_tac 2); by (Blast_tac 1); qed "transient_strengthen"; Goalw [transient_def] - "[| act:acts; A <= Domain act; act^^A <= -A |] ==> transient acts A"; + "[| act: Acts F; A <= Domain act; act^^A <= -A |] ==> F : transient A"; by (Blast_tac 1); qed "transient_mem"; @@ -40,40 +36,38 @@ (*** ensures ***) Goalw [ensures_def] - "[| constrains acts (A-B) (A Un B); transient acts (A-B) |] \ -\ ==> ensures acts A B"; + "[| F : constrains (A-B) (A Un B); F : transient (A-B) |] \ +\ ==> F : ensures A B"; by (Blast_tac 1); qed "ensuresI"; Goalw [ensures_def] - "ensures acts A B \ -\ ==> constrains acts (A-B) (A Un B) & transient acts (A-B)"; + "F : ensures A B ==> F : constrains (A-B) (A Un B) & F : transient (A-B)"; by (Blast_tac 1); qed "ensuresD"; (*The L-version (precondition strengthening) doesn't hold for ENSURES*) Goalw [ensures_def] - "[| ensures acts A A'; A'<=B' |] ==> ensures acts A B'"; + "[| F : ensures A A'; A'<=B' |] ==> F : ensures A B'"; by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); qed "ensures_weaken_R"; Goalw [ensures_def, constrains_def, transient_def] - "acts ~= {} ==> ensures acts A UNIV"; + "Acts F ~= {} ==> F : ensures A UNIV"; by Auto_tac; qed "ensures_UNIV"; Goalw [ensures_def] - "[| stable acts C; \ -\ constrains acts (C Int (A - A')) (A Un A'); \ -\ transient acts (C Int (A-A')) |] \ -\ ==> ensures acts (C Int A) (C Int A')"; + "[| F : stable C; \ +\ F : constrains (C Int (A - A')) (A Un A'); \ +\ F : transient (C Int (A-A')) |] \ +\ ==> F : ensures (C Int A) (C Int A')"; by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym, stable_constrains_Int]) 1); qed "stable_ensures_Int"; -Goal "[| stable acts A; transient acts C; A <= B Un C |] \ -\ ==> ensures acts A B"; +Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : ensures A 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"; @@ -81,62 +75,67 @@ (*** leadsTo ***) -(*Synonyms for the theorems produced by the inductive defn package*) -bind_thm ("leadsTo_Basis", leadsto.Basis); -bind_thm ("leadsTo_Trans", leadsto.Trans); +Goalw [leadsTo_def] "F : ensures A B ==> F : leadsTo A B"; +by (blast_tac (claset() addIs [leadsto.Basis]) 1); +qed "leadsTo_Basis"; -Goal "transient acts A ==> leadsTo acts A (-A)"; +Goalw [leadsTo_def] + "[| F : leadsTo A B; F : leadsTo B C |] ==> F : leadsTo A C"; +by (blast_tac (claset() addIs [leadsto.Trans]) 1); +qed "leadsTo_Trans"; + +Goal "F : transient A ==> F : leadsTo A (-A)"; by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); qed "transient_imp_leadsTo"; -Goal "act: acts ==> leadsTo acts A UNIV"; +Goal "F : leadsTo A UNIV"; by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1); qed "leadsTo_UNIV"; Addsimps [leadsTo_UNIV]; (*Useful with cancellation, disjunction*) -Goal "leadsTo acts A (A' Un A') ==> leadsTo acts A A'"; +Goal "F : leadsTo A (A' Un A') ==> F : leadsTo A A'"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "leadsTo_Un_duplicate"; -Goal "leadsTo acts A (A' Un C Un C) ==> leadsTo acts A (A' Un C)"; +Goal "F : leadsTo A (A' Un C Un C) ==> F : leadsTo A (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 = goal thy - "(!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B"; -by (blast_tac (claset() addIs (leadsto.Union::prems)) 1); +val prems = Goalw [leadsTo_def] + "(!!A. A : S ==> F : leadsTo A B) ==> F : leadsTo (Union S) B"; +by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1); qed "leadsTo_Union"; -val prems = goal thy - "(!!i. i : I ==> leadsTo acts (A i) B) ==> leadsTo acts (UN i:I. A i) B"; +val prems = Goal + "(!!i. i : I ==> F : leadsTo (A i) B) ==> F : leadsTo (UN i:I. A i) B"; by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); -by (blast_tac (claset() addIs (leadsto.Union::prems)) 1); +by (blast_tac (claset() addIs leadsTo_Union::prems) 1); qed "leadsTo_UN"; (*Binary union introduction rule*) -Goal "[| leadsTo acts A C; leadsTo acts B C |] ==> leadsTo acts (A Un B) C"; +Goal "[| F : leadsTo A C; F : leadsTo B C |] ==> F : leadsTo (A Un B) C"; by (stac Un_eq_Union 1); by (blast_tac (claset() addIs [leadsTo_Union]) 1); qed "leadsTo_Un"; (*The INDUCTION rule as we should have liked to state it*) -val major::prems = goal thy - "[| leadsTo acts za zb; \ -\ !!A B. ensures acts A B ==> P A B; \ -\ !!A B C. [| leadsTo acts A B; P A B; leadsTo acts B C; P B C |] \ +val major::prems = Goalw [leadsTo_def] + "[| F : leadsTo za zb; \ +\ !!A B. F : ensures A B ==> P A B; \ +\ !!A B C. [| F : leadsTo A B; P A B; F : leadsTo B C; P B C |] \ \ ==> P A C; \ -\ !!B S. ALL A:S. leadsTo acts A B & P A B ==> P (Union S) B \ +\ !!B S. ALL A:S. F : leadsTo A B & P A B ==> P (Union S) B \ \ |] ==> P za zb"; -by (rtac (major RS leadsto.induct) 1); +by (rtac (major RS CollectD RS leadsto.induct) 1); by (REPEAT (blast_tac (claset() addIs prems) 1)); qed "leadsTo_induct"; -Goal "[| A<=B; Id: acts |] ==> leadsTo acts A B"; +Goal "A<=B ==> F : leadsTo A B"; by (rtac leadsTo_Basis 1); by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); by (Blast_tac 1); @@ -146,50 +145,38 @@ Addsimps [empty_leadsTo]; -(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it - needs the extra premise Id:acts*) -Goal "leadsTo acts A A' ==> A'<=B' --> leadsTo acts A B'"; -by (etac leadsTo_induct 1); -by (Clarify_tac 3); -by (blast_tac (claset() addIs [leadsTo_Union]) 3); -by (blast_tac (claset() addIs [leadsTo_Trans]) 2); -by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1); -qed_spec_mp "leadsTo_weaken_R"; +Goal "[| F : leadsTo A A'; A'<=B' |] ==> F : leadsTo A B'"; +by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1); +qed "leadsTo_weaken_R"; -Goal "[| leadsTo acts A A'; B<=A; Id: acts |] ==> \ -\ leadsTo acts B A'"; +Goal "[| F : leadsTo A A'; B<=A |] ==> F : leadsTo B A'"; by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, subset_imp_leadsTo]) 1); qed_spec_mp "leadsTo_weaken_L"; (*Distributes over binary unions*) -Goal "Id: acts ==> \ -\ leadsTo acts (A Un B) C = (leadsTo acts A C & leadsTo acts B C)"; +Goal "F : leadsTo (A Un B) C = (F : leadsTo A C & F : leadsTo B C)"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); qed "leadsTo_Un_distrib"; -Goal "Id: acts ==> \ -\ leadsTo acts (UN i:I. A i) B = (ALL i : I. leadsTo acts (A i) B)"; +Goal "F : leadsTo (UN i:I. A i) B = (ALL i : I. F : leadsTo (A i) B)"; by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); qed "leadsTo_UN_distrib"; -Goal "Id: acts ==> \ -\ leadsTo acts (Union S) B = (ALL A : S. leadsTo acts A B)"; +Goal "F : leadsTo (Union S) B = (ALL A : S. F : leadsTo A B)"; by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); qed "leadsTo_Union_distrib"; -Goal "[| leadsTo acts A A'; Id: acts; B<=A; A'<=B' |] \ -\ ==> leadsTo acts B B'"; +Goal "[| F : leadsTo A A'; B<=A; A'<=B' |] ==> F : leadsTo B 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 "[| leadsTo acts (A-B) C; leadsTo acts B C; Id: acts |] \ -\ ==> leadsTo acts A C"; +Goal "[| F : leadsTo (A-B) C; F : leadsTo B C |] ==> F : leadsTo A C"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1); qed "leadsTo_Diff"; @@ -198,8 +185,8 @@ see ball_constrains_UN in UNITY.ML***) val prems = goal thy - "(!! i. i:I ==> leadsTo acts (A i) (A' i)) \ -\ ==> leadsTo acts (UN i:I. A i) (UN i:I. A' i)"; + "(!! i. i:I ==> F : leadsTo (A i) (A' i)) \ +\ ==> F : leadsTo (UN i:I. A i) (UN i:I. A' i)"; by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] addIs prems) 1); @@ -208,22 +195,21 @@ (*Version with no index set*) val prems = goal thy - "(!! i. leadsTo acts (A i) (A' i)) \ -\ ==> leadsTo acts (UN i. A i) (UN i. A' i)"; + "(!! i. F : leadsTo (A i) (A' i)) \ +\ ==> F : leadsTo (UN i. A i) (UN i. A' i)"; by (blast_tac (claset() addIs [leadsTo_UN_UN] addIs prems) 1); qed "leadsTo_UN_UN_noindex"; (*Version with no index set*) -Goal "ALL i. leadsTo acts (A i) (A' i) \ -\ ==> leadsTo acts (UN i. A i) (UN i. A' i)"; +Goal "ALL i. F : leadsTo (A i) (A' i) \ +\ ==> F : leadsTo (UN i. A i) (UN i. A' i)"; by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1); qed "all_leadsTo_UN_UN"; (*Binary union version*) -Goal "[| leadsTo acts A A'; leadsTo acts B B' |] \ -\ ==> leadsTo acts (A Un B) (A' Un B')"; +Goal "[| F : leadsTo A A'; F : leadsTo B B' |] ==> F : leadsTo (A Un B) (A' Un B')"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]) 1); qed "leadsTo_Un_Un"; @@ -231,27 +217,27 @@ (** The cancellation law **) -Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; Id: acts |] \ -\ ==> leadsTo acts A (A' Un B')"; +Goal "[| F : leadsTo A (A' Un B); F : leadsTo B B' |] \ +\ ==> F : leadsTo A (A' Un B')"; by (blast_tac (claset() addIs [leadsTo_Un_Un, subset_imp_leadsTo, leadsTo_Trans]) 1); qed "leadsTo_cancel2"; -Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; Id: acts |] \ -\ ==> leadsTo acts A (A' Un B')"; +Goal "[| F : leadsTo A (A' Un B); F : leadsTo (B-A') B' |] \ +\ ==> F : leadsTo A (A' Un B')"; by (rtac leadsTo_cancel2 1); by (assume_tac 2); by (ALLGOALS Asm_simp_tac); qed "leadsTo_cancel_Diff2"; -Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; Id: acts |] \ -\ ==> leadsTo acts A (B' Un A')"; +Goal "[| F : leadsTo A (B Un A'); F : leadsTo B B' |] \ +\ ==> F : leadsTo A (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 "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; Id: acts |] \ -\ ==> leadsTo acts A (B' Un A')"; +Goal "[| F : leadsTo A (B Un A'); F : leadsTo (B-A') B' |] \ +\ ==> F : leadsTo A (B' Un A')"; by (rtac leadsTo_cancel1 1); by (assume_tac 2); by (ALLGOALS Asm_simp_tac); @@ -261,14 +247,14 @@ (** The impossibility law **) -Goal "leadsTo acts A B ==> B={} --> A={}"; +Goal "F : leadsTo A B ==> B={} --> A={}"; by (etac leadsTo_induct 1); by (ALLGOALS Asm_simp_tac); by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); by (Blast_tac 1); val lemma = result() RS mp; -Goal "leadsTo acts A {} ==> A={}"; +Goal "F : leadsTo A {} ==> A={}"; by (blast_tac (claset() addSIs [lemma]) 1); qed "leadsTo_empty"; @@ -277,8 +263,8 @@ (*Special case of PSP: Misra's "stable conjunction"*) Goalw [stable_def] - "[| leadsTo acts A A'; stable acts B |] \ -\ ==> leadsTo acts (A Int B) (A' Int B)"; + "[| F : leadsTo A A'; F : stable B |] \ +\ ==> F : leadsTo (A Int B) (A' Int B)"; by (etac leadsTo_induct 1); by (simp_tac (simpset() addsimps [Int_Union_Union]) 3); by (blast_tac (claset() addIs [leadsTo_Union]) 3); @@ -290,47 +276,45 @@ by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1); qed "psp_stable"; -Goal "[| leadsTo acts A A'; stable acts B |] \ -\ ==> leadsTo acts (B Int A) (B Int A')"; +Goal "[| F : leadsTo A A'; F : stable B |] \ +\ ==> F : leadsTo (B Int A) (B Int A')"; by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); qed "psp_stable2"; Goalw [ensures_def, constrains_def] - "[| ensures acts A A'; constrains acts B B' |] \ -\ ==> ensures acts (A Int B) ((A' Int B) Un (B' - B))"; + "[| F : ensures A A'; F : constrains B B' |] \ +\ ==> F : ensures (A Int B) ((A' Int B) Un (B' - B))"; by (blast_tac (claset() addIs [transient_strengthen]) 1); qed "psp_ensures"; -Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \ -\ ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))"; +Goal "[| F : leadsTo A A'; F : constrains B B' |] \ +\ ==> F : leadsTo (A Int B) ((A' Int B) Un (B' - B))"; by (etac leadsTo_induct 1); by (simp_tac (simpset() addsimps [Int_Union_Union]) 3); by (blast_tac (claset() addIs [leadsTo_Union]) 3); (*Transitivity case has a delicate argument involving "cancellation"*) by (rtac leadsTo_Un_duplicate2 2); by (etac leadsTo_cancel_Diff1 2); -by (assume_tac 3); by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); (*Basis case*) by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1); qed "psp"; -Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \ -\ ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))"; +Goal "[| F : leadsTo A A'; F : constrains B B' |] \ +\ ==> F : leadsTo (B Int A) ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); qed "psp2"; Goalw [unless_def] - "[| leadsTo acts A A'; unless acts B B'; Id: acts |] \ -\ ==> leadsTo acts (A Int B) ((A' Int B) Un B')"; + "[| F : leadsTo A A'; F : unless B B' |] \ +\ ==> F : leadsTo (A Int B) ((A' Int B) Un B')"; by (dtac psp 1); by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2); -by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2); -by (etac leadsTo_Diff 2); -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2); -by Auto_tac; +by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 1); +by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 1); +by (etac leadsTo_Diff 1); +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); qed "psp_unless"; @@ -339,12 +323,11 @@ (** The most general rule: r is any wf relation; f is any variant function **) Goal "[| wf r; \ -\ ALL m. leadsTo acts (A Int f-``{m}) \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ -\ Id: acts |] \ -\ ==> leadsTo acts (A Int f-``{m}) B"; +\ ALL m. F : leadsTo (A Int f-``{m}) \ +\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ==> F : leadsTo (A Int f-``{m}) B"; by (eres_inst_tac [("a","m")] wf_induct 1); -by (subgoal_tac "leadsTo acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1); +by (subgoal_tac "F : leadsTo (A Int (f -`` (r^-1 ^^ {x}))) 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); @@ -354,10 +337,9 @@ (** Meta or object quantifier ????? **) Goal "[| wf r; \ -\ ALL m. leadsTo acts (A Int f-``{m}) \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ -\ Id: acts |] \ -\ ==> leadsTo acts A B"; +\ ALL m. F : leadsTo (A Int f-``{m}) \ +\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ==> F : leadsTo A B"; by (res_inst_tac [("t", "A")] subst 1); by (rtac leadsTo_UN 2); by (etac lemma 2); @@ -367,10 +349,9 @@ Goal "[| wf r; \ -\ ALL m:I. leadsTo acts (A Int f-``{m}) \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B); \ -\ Id: acts |] \ -\ ==> leadsTo acts A ((A - (f-``I)) Un B)"; +\ ALL m:I. F : leadsTo (A Int f-``{m}) \ +\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ==> F : leadsTo A ((A - (f-``I)) Un B)"; by (etac leadsTo_wf_induct 1); by Safe_tac; by (case_tac "m:I" 1); @@ -379,33 +360,28 @@ qed "bounded_induct"; -(*Alternative proof is via the lemma leadsTo acts (A Int f-``(lessThan m)) B*) -Goal "[| ALL m. leadsTo acts (A Int f-``{m}) \ -\ ((A Int f-``(lessThan m)) Un B); \ -\ Id: acts |] \ -\ ==> leadsTo acts A B"; +(*Alternative proof is via the lemma F : leadsTo (A Int f-``(lessThan m)) B*) +Goal "[| ALL m. F : leadsTo (A Int f-``{m}) \ +\ ((A Int f-``(lessThan m)) Un B) |] \ +\ ==> F : leadsTo A B"; by (rtac (wf_less_than RS leadsTo_wf_induct) 1); -by (assume_tac 2); by (Asm_simp_tac 1); qed "lessThan_induct"; -Goal "[| ALL m:(greaterThan l). leadsTo acts (A Int f-``{m}) \ -\ ((A Int f-``(lessThan m)) Un B); \ -\ Id: acts |] \ -\ ==> leadsTo acts A ((A Int (f-``(atMost l))) Un B)"; -by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1); +Goal "[| ALL m:(greaterThan l). F : leadsTo (A Int f-``{m}) \ +\ ((A Int f-``(lessThan m)) Un B) |] \ +\ ==> F : leadsTo A ((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 (assume_tac 2); by (Asm_simp_tac 1); qed "lessThan_bounded_induct"; -Goal "[| ALL m:(lessThan l). leadsTo acts (A Int f-``{m}) \ -\ ((A Int f-``(greaterThan m)) Un B); \ -\ Id: acts |] \ -\ ==> leadsTo acts A ((A Int (f-``(atLeast l))) Un B)"; +Goal "[| ALL m:(lessThan l). F : leadsTo (A Int f-``{m}) \ +\ ((A Int f-``(greaterThan m)) Un B) |] \ +\ ==> F : leadsTo A ((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 (assume_tac 2); by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); by (Clarify_tac 1); by (case_tac "m A <= wlt acts B"; +Goalw [wlt_def] "F : leadsTo A B ==> A <= wlt F B"; by (blast_tac (claset() addSIs [leadsTo_Union]) 1); qed "leadsTo_subset"; (*Misra's property W2*) -Goal "Id: acts ==> leadsTo acts A B = (A <= wlt acts B)"; +Goal "F : leadsTo A 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 "Id: acts ==> B <= wlt acts B"; +Goal "B <= wlt F B"; by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym, subset_imp_leadsTo]) 1); qed "wlt_increasing"; @@ -442,16 +418,16 @@ (*Used in the Trans case below*) Goalw [constrains_def] "[| B <= A2; \ -\ constrains acts (A1 - B) (A1 Un B); \ -\ constrains acts (A2 - C) (A2 Un C) |] \ -\ ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)"; +\ F : constrains (A1 - B) (A1 Un B); \ +\ F : constrains (A2 - C) (A2 Un C) |] \ +\ ==> F : constrains (A1 Un A2 - C) (A1 Un A2 Un C)"; by (Blast_tac 1); val lemma1 = result(); (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) -Goal "[| leadsTo acts A A'; Id: acts |] ==> \ -\ EX B. A<=B & leadsTo acts B A' & constrains acts (B-A') (B Un A')"; +Goal "F : leadsTo A A' ==> \ +\ EX B. A<=B & F : leadsTo B A' & F : constrains (B-A') (B Un A')"; by (etac leadsTo_induct 1); (*Basis*) by (blast_tac (claset() addIs [leadsTo_Basis] @@ -470,11 +446,11 @@ (*Misra's property W5*) -Goal "Id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)"; -by (forward_tac [wlt_leadsTo RS leadsTo_123] 1); +Goal "F : constrains (wlt F B - B) (wlt F B)"; +by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); by (Clarify_tac 1); -by (subgoal_tac "Ba = wlt acts B" 1); -by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2); +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"; @@ -482,30 +458,29 @@ (*** Completion: Binary and General Finite versions ***) -Goal "[| leadsTo acts A A'; stable acts A'; \ -\ leadsTo acts B B'; stable acts B'; Id: acts |] \ -\ ==> leadsTo acts (A Int B) (A' Int B')"; -by (subgoal_tac "stable acts (wlt acts B')" 1); +Goal "[| F : leadsTo A A'; F : stable A'; \ +\ F : leadsTo B B'; F : stable B' |] \ +\ ==> F : leadsTo (A Int B) (A' Int B')"; +by (subgoal_tac "F : stable (wlt F B')" 1); by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2); by (EVERY [etac (constrains_Un RS constrains_weaken) 2, - etac wlt_constrains_wlt 2, + rtac wlt_constrains_wlt 2, fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3, Blast_tac 2]); -by (subgoal_tac "leadsTo acts (A Int wlt acts B') (A' Int wlt acts B')" 1); +by (subgoal_tac "F : leadsTo (A Int wlt F B') (A' Int wlt F B')" 1); by (blast_tac (claset() addIs [psp_stable]) 2); -by (subgoal_tac "leadsTo acts (A' Int wlt acts B') (A' Int B')" 1); +by (subgoal_tac "F : leadsTo (A' Int wlt F B') (A' Int B')" 1); by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2); -by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1); +by (subgoal_tac "F : leadsTo (A Int B) (A Int wlt F B')" 1); by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, subset_imp_leadsTo]) 2); by (blast_tac (claset() addIs [leadsTo_Trans]) 1); qed "stable_completion"; -Goal "[| finite I; Id: acts |] \ -\ ==> (ALL i:I. leadsTo acts (A i) (A' i)) --> \ -\ (ALL i:I. stable acts (A' i)) --> \ -\ leadsTo acts (INT i:I. A i) (INT i:I. A' i)"; +Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i)) --> \ +\ (ALL i:I. F : stable (A' i)) --> \ +\ F : leadsTo (INT i:I. A i) (INT i:I. A' i)"; by (etac finite_induct 1); by (Asm_simp_tac 1); by (asm_simp_tac @@ -514,28 +489,26 @@ qed_spec_mp "finite_stable_completion"; -Goal "[| W = wlt acts (B' Un C); \ -\ leadsTo acts A (A' Un C); constrains acts A' (A' Un C); \ -\ leadsTo acts B (B' Un C); constrains acts B' (B' Un C); \ -\ Id: acts |] \ -\ ==> leadsTo acts (A Int B) ((A' Int B') Un C)"; -by (subgoal_tac "constrains acts (W-C) (W Un B' Un C)" 1); +Goal "[| W = wlt F (B' Un C); \ +\ F : leadsTo A (A' Un C); F : constrains A' (A' Un C); \ +\ F : leadsTo B (B' Un C); F : constrains B' (B' Un C) |] \ +\ ==> F : leadsTo (A Int B) ((A' Int B') Un C)"; +by (subgoal_tac "F : constrains (W-C) (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 "constrains acts (W-C) W" 1); +by (subgoal_tac "F : constrains (W-C) W" 1); by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); -by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1); +by (subgoal_tac "F : leadsTo (A Int W - C) (A' Int W Un C)" 1); by (simp_tac (simpset() addsimps [Int_Diff]) 2); by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2); (** LEVEL 7 **) -by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1); +by (subgoal_tac "F : leadsTo (A' Int W Un C) (A' Int B' Un C)" 1); by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, psp2 RS leadsTo_weaken_R, subset_refl RS subset_imp_leadsTo, leadsTo_Un_duplicate2]) 2); by (dtac leadsTo_Diff 1); -by (assume_tac 2); 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] @@ -544,10 +517,9 @@ bind_thm("completion", refl RS result()); -Goal "[| finite I; Id: acts |] \ -\ ==> (ALL i:I. leadsTo acts (A i) (A' i Un C)) --> \ -\ (ALL i:I. constrains acts (A' i) (A' i Un C)) --> \ -\ leadsTo acts (INT i:I. A i) ((INT i:I. A' i) Un C)"; +Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i Un C)) --> \ +\ (ALL i:I. F : constrains (A' i) (A' i Un C)) --> \ +\ F : leadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)"; by (etac finite_induct 1); by (ALLGOALS Asm_simp_tac); by (Clarify_tac 1); diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/WFair.thy Thu Oct 15 11:35:07 1998 +0200 @@ -14,39 +14,38 @@ (*This definition specifies weak fairness. The rest of the theory is generic to all forms of fairness.*) - transient :: "[('a * 'a)set set, 'a set] => bool" - "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A" - - ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool" - "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)" - (*(unless acts A B) would be equivalent*) + transient :: "'a set => 'a program set" + "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}" -syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool" -consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set" + ensures :: "['a set, 'a set] => 'a program set" + "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)" + + +consts leadsto :: "'a program => ('a set * 'a set) set" -translations - "leadsTo acts A B" == "(A,B) : leadsto acts" - "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts" - -inductive "leadsto acts" +inductive "leadsto F" intrs - Basis "ensures acts A B ==> leadsTo acts A B" + Basis "F : ensures A B ==> (A,B) : leadsto F" - Trans "[| leadsTo acts A B; leadsTo acts B C |] - ==> leadsTo acts A C" + Trans "[| (A,B) : leadsto F; (B,C) : leadsto F |] + ==> (A,C) : leadsto F" (*Encoding using powerset of the desired axiom - (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B + (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F *) - Union "(UN A:S. {(A,B)}) : Pow (leadsto acts) - ==> leadsTo acts (Union S) B" + Union "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F" monos "[Pow_mono]" -(*wlt acts B is the largest set that leads to B*) -constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set" - "wlt acts B == Union {A. leadsTo acts A B}" + +constdefs (*visible version of the relation*) + leadsTo :: "['a set, 'a set] => 'a program set" + "leadsTo A B == {F. (A,B) : leadsto F}" + + (*wlt F B is the largest set that leads to B*) + wlt :: "['a program, 'a set] => 'a set" + "wlt F B == Union {A. F: leadsTo A B}" end