# HG changeset patch # User paulson # Date 899391235 -7200 # Node ID 8f4b72f0c15d9fc58333d355dbdf4fef6147219b # Parent 2497807020fa0b84837c0e143a5e18d25bfc9989 Uncurried functions LeadsTo and reach Deleted leading parameters thanks to new Goal command diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Channel.ML --- a/src/HOL/UNITY/Channel.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Channel.ML Thu Jul 02 16:53:55 1998 +0200 @@ -14,7 +14,7 @@ (*None represents "infinity" while Some represents proper integers*) -Goalw [minSet_def] "!!A. minSet A = Some x --> x : A"; +Goalw [minSet_def] "minSet A = Some x --> x : A"; by (Simp_tac 1); by (fast_tac (claset() addIs [LeastI]) 1); qed_spec_mp "minSet_eq_SomeD"; @@ -24,7 +24,7 @@ qed_spec_mp "minSet_empty"; Addsimps [minSet_empty]; -Goalw [minSet_def] "!!A. x:A ==> minSet A = Some (LEAST x. x: A)"; +Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)"; by (ALLGOALS Asm_simp_tac); by (Blast_tac 1); qed_spec_mp "minSet_nonempty"; diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Common.ML --- a/src/HOL/UNITY/Common.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Common.ML Thu Jul 02 16:53:55 1998 +0200 @@ -14,9 +14,8 @@ open Common; (*Misra's property CMT4: t exceeds no common meeting time*) -Goal - "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \ -\ ==> stable Acts (atMost n)"; +Goal "[| ALL m. constrains Acts {m} (maxfg m); n: common |] \ +\ ==> stable Acts (atMost n)"; by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1); by (asm_full_simp_tac (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def, @@ -28,9 +27,8 @@ addIs [order_eq_refl, fmono, gmono, le_trans]) 1); qed "common_stable"; -Goal - "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \ -\ ==> reachable {0} Acts <= atMost n"; +Goal "[| ALL m. constrains Acts {m} (maxfg m); n: common |] \ +\ ==> reachable ({0},Acts) <= atMost n"; by (rtac strongest_invariant 1); by (asm_simp_tac (simpset() addsimps [common_stable]) 2); by (simp_tac (simpset() addsimps [atMost_def]) 1); @@ -77,7 +75,7 @@ Addsimps [atMost_Int_atLeast]; Goal - "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \ + "[| ALL m. constrains Acts {m} (maxfg m); \ \ ALL m: lessThan n. leadsTo Acts {m} (greaterThan m); \ \ n: common; id: Acts |] \ \ ==> leadsTo Acts (atMost n) common"; @@ -91,7 +89,7 @@ (*The "ALL m: Compl common" form echoes CMT6.*) Goal - "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \ + "[| ALL m. constrains Acts {m} (maxfg m); \ \ ALL m: Compl common. leadsTo Acts {m} (greaterThan m); \ \ n: common; id: Acts |] \ \ ==> leadsTo Acts (atMost (LEAST n. n: common)) common"; diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Deadlock.ML --- a/src/HOL/UNITY/Deadlock.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Deadlock.ML Thu Jul 02 16:53:55 1998 +0200 @@ -1,10 +1,15 @@ - +(* Title: HOL/UNITY/Traces + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge -(*** Deadlock examples from section 5.6 ***) +Deadlock examples from section 5.6 of + Misra, "A Logic for Concurrent Programming", 1994 +*) (*Trivial, two-process case*) Goalw [constrains_def, stable_def] - "!!Acts. [| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \ + "[| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \ \ ==> stable Acts (A Int B)"; by (Blast_tac 1); result(); diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Mutex.ML --- a/src/HOL/UNITY/Mutex.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Mutex.ML Thu Jul 02 16:53:55 1998 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/UNITY/Mutex.thy +(* Title: HOL/UNITY/Mutex ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge @@ -47,7 +47,7 @@ by (auto_tac (claset() addSEs [less_SucE], simpset())); qed "stable_boolVars"; -Goal "reachable MInit mutex <= boolVars"; +Goal "reachable (MInit,mutex) <= boolVars"; by (rtac strongest_invariant 1); by (rtac stable_boolVars 2); by (rewrite_goals_tac [MInit_def, boolVars_def]); @@ -76,7 +76,7 @@ qed "MInit_invar_1vn"; (*The intersection is an invariant of the system*) -Goal "reachable MInit mutex <= invariant 0 UU MM Int invariant 1 VV NN"; +Goal "reachable (MInit,mutex) <= invariant 0 UU MM Int invariant 1 VV NN"; by (simp_tac (simpset() addsimps [strongest_invariant, Int_greatest, stable_Int, stable_invar_0um, stable_invar_1vn, @@ -94,7 +94,7 @@ by Auto_tac; val lemma = result(); -Goal "{s. s MM = 3 & s NN = 3} <= Compl (reachable MInit mutex)"; +Goal "{s. s MM = 3 & s NN = 3} <= Compl (reachable (MInit,mutex))"; by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1); qed "mutual_exclusion"; @@ -119,24 +119,24 @@ by (constrains_tac 1); qed "U_F0"; -Goal "LeadsTo MInit mutex {s. s MM=1} {s. s PP = s VV & s MM = 2}"; +Goal "LeadsTo(MInit,mutex) {s. s MM=1} {s. s PP = s VV & s MM = 2}"; by (rtac leadsTo_imp_LeadsTo 1); (*makes the proof much faster*) by (ensures_tac "cmd1u" 1); qed "U_F1"; -Goal "LeadsTo MInit mutex {s. s PP = 0 & s MM = 2} {s. s MM = 3}"; +Goal "LeadsTo(MInit,mutex) {s. s PP = 0 & s MM = 2} {s. s MM = 3}"; by (cut_facts_tac [reachable_subset_invariant'] 1); by (ensures_tac "cmd2 0 MM" 1); qed "U_F2"; -Goalw [mutex_def] "LeadsTo MInit mutex {s. s MM = 3} {s. s PP = 1}"; +Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s MM = 3} {s. s PP = 1}"; by (rtac leadsTo_imp_LeadsTo 1); by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1); by (ensures_tac "cmd4 1 MM" 2); by (ensures_tac "cmd3 UU MM" 1); qed "U_F3"; -Goal "LeadsTo MInit mutex {s. s MM = 2} {s. s PP = 1}"; +Goal "LeadsTo(MInit,mutex) {s. s MM = 2} {s. s PP = 1}"; by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); @@ -144,13 +144,13 @@ by (auto_tac (claset() addSEs [less_SucE], simpset())); val lemma2 = result(); -Goal "LeadsTo MInit mutex {s. s MM = 1} {s. s PP = 1}"; +Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s PP = 1}"; by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val lemma1 = result(); -Goal "LeadsTo MInit mutex {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}"; +Goal "LeadsTo(MInit,mutex) {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}"; by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] addcongs [rev_conj_cong]) 1); by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib, @@ -159,7 +159,7 @@ (*Misra's F4*) -Goal "LeadsTo MInit mutex {s. s UU = 1} {s. s PP = 1}"; +Goal "LeadsTo(MInit,mutex) {s. s UU = 1} {s. s PP = 1}"; by (rtac LeadsTo_weaken_L 1); by (rtac lemma123 1); by (cut_facts_tac [reachable_subset_invariant'] 1); @@ -174,24 +174,24 @@ by (constrains_tac 1); qed "V_F0"; -Goal "LeadsTo MInit mutex {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}"; +Goal "LeadsTo(MInit,mutex) {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}"; by (rtac leadsTo_imp_LeadsTo 1); (*makes the proof much faster*) by (ensures_tac "cmd1v" 1); qed "V_F1"; -Goal "LeadsTo MInit mutex {s. s PP = 1 & s NN = 2} {s. s NN = 3}"; +Goal "LeadsTo(MInit,mutex) {s. s PP = 1 & s NN = 2} {s. s NN = 3}"; by (cut_facts_tac [reachable_subset_invariant'] 1); by (ensures_tac "cmd2 1 NN" 1); qed "V_F2"; -Goalw [mutex_def] "LeadsTo MInit mutex {s. s NN = 3} {s. s PP = 0}"; +Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s NN = 3} {s. s PP = 0}"; by (rtac leadsTo_imp_LeadsTo 1); by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1); by (ensures_tac "cmd4 0 NN" 2); by (ensures_tac "cmd3 VV NN" 1); qed "V_F3"; -Goal "LeadsTo MInit mutex {s. s NN = 2} {s. s PP = 0}"; +Goal "LeadsTo(MInit,mutex) {s. s NN = 2} {s. s PP = 0}"; by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); @@ -199,13 +199,13 @@ by (auto_tac (claset() addSEs [less_SucE], simpset())); val lemma2 = result(); -Goal "LeadsTo MInit mutex {s. s NN = 1} {s. s PP = 0}"; +Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s PP = 0}"; by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val lemma1 = result(); -Goal "LeadsTo MInit mutex {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}"; +Goal "LeadsTo(MInit,mutex) {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}"; by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] addcongs [rev_conj_cong]) 1); by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib, @@ -214,7 +214,7 @@ (*Misra's F4*) -Goal "LeadsTo MInit mutex {s. s VV = 1} {s. s PP = 0}"; +Goal "LeadsTo(MInit,mutex) {s. s VV = 1} {s. s PP = 0}"; by (rtac LeadsTo_weaken_L 1); by (rtac lemma123 1); by (cut_facts_tac [reachable_subset_invariant'] 1); @@ -225,14 +225,14 @@ (** Absence of starvation **) (*Misra's F6*) -Goal "LeadsTo MInit mutex {s. s MM = 1} {s. s MM = 3}"; +Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s MM = 3}"; by (rtac LeadsTo_Un_duplicate 1); by (rtac LeadsTo_cancel2 1); by (rtac U_F2 2); by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); by (stac Un_commute 1); by (rtac LeadsTo_Un_duplicate 1); -by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1); +by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1); by (rtac (U_F1 RS LeadsTo_weaken_R) 1); by (cut_facts_tac [reachable_subset_boolVars'] 1); by (auto_tac (claset() addSEs [less_SucE], simpset())); @@ -240,7 +240,7 @@ (*The same for V*) -Goal "LeadsTo MInit mutex {s. s NN = 1} {s. s NN = 3}"; +Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s NN = 3}"; by (rtac LeadsTo_Un_duplicate 1); by (rtac LeadsTo_cancel2 1); by (rtac V_F2 2); diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Network.thy --- a/src/HOL/UNITY/Network.thy Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Network.thy Thu Jul 02 16:53:55 1998 +0200 @@ -1,5 +1,17 @@ +(* Title: HOL/UNITY/Network + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +The Communication Network + +From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 +*) + Network = UNITY + +(*The state assigns a number to each process variable*) + datatype pvar = Sent | Rcvd | Idle datatype pname = Aproc | Bproc diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Reach.ML --- a/src/HOL/UNITY/Reach.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Reach.ML Thu Jul 02 16:53:55 1998 +0200 @@ -65,7 +65,7 @@ by Auto_tac; qed "rinit_invariant"; -Goal "reachable rinit racts <= invariant"; +Goal "reachable (rinit,racts) <= invariant"; by (simp_tac (simpset() addsimps [strongest_invariant, stable_invariant, rinit_invariant]) 1); qed "reachable_subset_invariant"; @@ -134,13 +134,13 @@ (*** Progress ***) -Goalw [metric_def] "!!s. ~ s x ==> Suc (metric (s(x:=True))) = metric s"; +Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s"; by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1); by Auto_tac; by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1); qed "Suc_metric"; -Goal "!!s. ~ s x ==> metric (s(x:=True)) < metric s"; +Goal "~ s x ==> metric (s(x:=True)) < metric s"; by (etac (Suc_metric RS subst) 1); by (Blast_tac 1); qed "metric_less"; @@ -152,7 +152,7 @@ simpset() addsimps [update_idem])); qed "metric_le"; -Goal "!!m. (u,v): edges ==> \ +Goal "(u,v): edges ==> \ \ ensures racts ((metric-``{m}) Int {s. s u & ~ s v}) \ \ (metric-``(lessThan m))"; by (ensures_tac "asgt u v" 1); @@ -180,7 +180,7 @@ by (rtac leadsTo_Un_fixedpoint 1); qed "leadsTo_fixedpoint"; -Goal "LeadsTo rinit racts UNIV { %v. (init, v) : edges^* }"; +Goal "LeadsTo(rinit,racts) UNIV { %v. (init, v) : edges^* }"; by (stac (fixedpoint_invariant_correct RS sym) 1); by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1); by (cut_facts_tac [reachable_subset_invariant] 1); diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/SubstAx.ML --- a/src/HOL/UNITY/SubstAx.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/SubstAx.ML Thu Jul 02 16:53:55 1998 +0200 @@ -10,24 +10,24 @@ open SubstAx; -(*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B) - (reachable Init Acts Int B') *) +(*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B) + (reachable(Init,Acts) Int B') *) bind_thm ("constrains_reachable", rewrite_rule [stable_def] stable_reachable RS constrains_Int); (*** Introduction rules: Basis, Trans, Union ***) -Goalw [LeadsTo_def] - "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B"; +Goal "leadsTo Acts A B ==> LeadsTo(Init,Acts) A B"; +by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1); qed "leadsTo_imp_LeadsTo"; -Goalw [LeadsTo_def] - "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A')) \ +Goal "[| constrains Acts (reachable(Init,Acts) Int (A - A')) \ \ (A Un A'); \ -\ transient Acts (reachable Init Acts Int (A-A')) |] \ -\ ==> LeadsTo Init Acts A A'"; +\ transient Acts (reachable(Init,Acts) Int (A-A')) |] \ +\ ==> LeadsTo(Init,Acts) A A'"; +by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1); by (assume_tac 2); by (asm_simp_tac @@ -35,117 +35,117 @@ stable_constrains_Int]) 1); qed "LeadsTo_Basis"; -Goalw [LeadsTo_def] - "!!Acts. [| LeadsTo Init Acts A B; LeadsTo Init Acts B C |] \ -\ ==> LeadsTo Init Acts A C"; +Goal "[| LeadsTo(Init,Acts) A B; LeadsTo(Init,Acts) B C |] \ +\ ==> LeadsTo(Init,Acts) A C"; +by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [leadsTo_Trans]) 1); qed "LeadsTo_Trans"; -val prems = goalw thy [LeadsTo_def] - "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B"; +val [prem] = goalw thy [LeadsTo_def] + "(!!A. A : S ==> LeadsTo(Init,Acts) A B) ==> LeadsTo(Init,Acts) (Union S) B"; +by (Simp_tac 1); by (stac Int_Union 1); -by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1); +by (blast_tac (claset() addIs [leadsTo_UN, + simplify (simpset()) prem]) 1); qed "LeadsTo_Union"; (*** Derived rules ***) -Goal "!!Acts. id: Acts ==> LeadsTo Init Acts A UNIV"; +Goal "id: Acts ==> LeadsTo(Init,Acts) 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 "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'"; +Goal "LeadsTo(Init,Acts) A (A' Un A') ==> LeadsTo(Init,Acts) A A'"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "LeadsTo_Un_duplicate"; -Goal "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)"; +Goal "LeadsTo(Init,Acts) A (A' Un C Un C) ==> LeadsTo(Init,Acts) A (A' Un C)"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "LeadsTo_Un_duplicate2"; val prems = goal thy - "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \ -\ ==> LeadsTo Init Acts (UN i:I. A i) B"; + "(!!i. i : I ==> LeadsTo(Init,Acts) (A i) B) \ +\ ==> LeadsTo(Init,Acts) (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 - "!!C. [| LeadsTo Init Acts A C; LeadsTo Init Acts B C |] ==> LeadsTo Init Acts (A Un B) C"; + "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C"; by (stac Un_eq_Union 1); by (blast_tac (claset() addIs [LeadsTo_Union]) 1); qed "LeadsTo_Un"; -Goalw [LeadsTo_def] - "!!A B. [| reachable Init Acts Int A <= B; id: Acts |] \ -\ ==> LeadsTo Init Acts A B"; +Goal "[| reachable(Init,Acts) Int A <= B; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) A B"; +by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); qed "Int_subset_imp_LeadsTo"; -Goalw [LeadsTo_def] - "!!A B. [| A <= B; id: Acts |] \ -\ ==> LeadsTo Init Acts A B"; +Goal "[| A <= B; id: Acts |] ==> LeadsTo(Init,Acts) A B"; +by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); qed "subset_imp_LeadsTo"; bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); Addsimps [empty_LeadsTo]; -Goal - "!!A B. [| reachable Init Acts Int A = {}; id: Acts |] \ -\ ==> LeadsTo Init Acts A B"; +Goal "[| reachable(Init,Acts) Int A = {}; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) A B"; by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1); qed "Int_empty_LeadsTo"; -Goalw [LeadsTo_def] - "!!Acts. [| LeadsTo Init Acts A A'; \ -\ reachable Init Acts Int A' <= B' |] \ -\ ==> LeadsTo Init Acts A B'"; +Goal "[| LeadsTo(Init,Acts) A A'; \ +\ reachable(Init,Acts) Int A' <= B' |] \ +\ ==> LeadsTo(Init,Acts) 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"; -Goalw [LeadsTo_def] - "!!Acts. [| LeadsTo Init Acts A A'; \ - \ reachable Init Acts Int B <= A; id: Acts |] \ -\ ==> LeadsTo Init Acts B A'"; +Goal "[| LeadsTo(Init,Acts) A A'; \ +\ reachable(Init,Acts) Int B <= A; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) 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"; (*Distributes over binary unions*) Goal - "!!C. id: Acts ==> \ -\ LeadsTo Init Acts (A Un B) C = \ -\ (LeadsTo Init Acts A C & LeadsTo Init Acts B C)"; + "id: Acts ==> \ +\ LeadsTo(Init,Acts) (A Un B) C = \ +\ (LeadsTo(Init,Acts) A C & LeadsTo(Init,Acts) B C)"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); qed "LeadsTo_Un_distrib"; Goal - "!!C. id: Acts ==> \ -\ LeadsTo Init Acts (UN i:I. A i) B = \ -\ (ALL i : I. LeadsTo Init Acts (A i) B)"; + "id: Acts ==> \ +\ LeadsTo(Init,Acts) (UN i:I. A i) B = \ +\ (ALL i : I. LeadsTo(Init,Acts) (A i) B)"; by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); qed "LeadsTo_UN_distrib"; Goal - "!!C. id: Acts ==> \ -\ LeadsTo Init Acts (Union S) B = \ -\ (ALL A : S. LeadsTo Init Acts A B)"; + "id: Acts ==> \ +\ LeadsTo(Init,Acts) (Union S) B = \ +\ (ALL A : S. LeadsTo(Init,Acts) A B)"; by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); qed "LeadsTo_Union_distrib"; Goal - "!!Acts. [| LeadsTo Init Acts A A'; id: Acts; \ -\ reachable Init Acts Int B <= A; \ -\ reachable Init Acts Int A' <= B' |] \ -\ ==> LeadsTo Init Acts B B'"; + "[| LeadsTo(Init,Acts) A A'; id: Acts; \ +\ reachable(Init,Acts) Int B <= A; \ +\ reachable(Init,Acts) Int A' <= B' |] \ +\ ==> LeadsTo(Init,Acts) B B'"; (*PROOF FAILED: why?*) by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R, LeadsTo_weaken_L]) 1); @@ -154,8 +154,8 @@ (*Set difference: maybe combine with leadsTo_weaken_L??*) Goal - "!!C. [| LeadsTo Init Acts (A-B) C; LeadsTo Init Acts B C; id: Acts |] \ -\ ==> LeadsTo Init Acts A C"; + "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) A C"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); qed "LeadsTo_Diff"; @@ -164,8 +164,8 @@ see ball_constrains_UN in UNITY.ML***) val prems = goal thy - "(!! i. i:I ==> LeadsTo Init Acts (A i) (A' i)) \ -\ ==> LeadsTo Init Acts (UN i:I. A i) (UN i:I. A' i)"; + "(!! i. i:I ==> LeadsTo(Init,Acts) (A i) (A' i)) \ +\ ==> LeadsTo(Init,Acts) (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); @@ -174,23 +174,23 @@ (*Version with no index set*) val prems = goal thy - "(!! i. LeadsTo Init Acts (A i) (A' i)) \ -\ ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)"; + "(!! i. LeadsTo(Init,Acts) (A i) (A' i)) \ +\ ==> LeadsTo(Init,Acts) (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 - "!!Acts. ALL i. LeadsTo Init Acts (A i) (A' i) \ -\ ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)"; + "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \ +\ ==> LeadsTo(Init,Acts) (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 "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \ -\ ==> LeadsTo Init Acts (A Un B) (A' Un B')"; +Goal "[| LeadsTo(Init,Acts) A A'; LeadsTo(Init,Acts) B B' |] \ +\ ==> LeadsTo(Init,Acts) (A Un B) (A' Un B')"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_R]) 1); qed "LeadsTo_Un_Un"; @@ -199,31 +199,31 @@ (** The cancellation law **) Goal - "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts B B'; \ + "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \ \ id: Acts |] \ -\ ==> LeadsTo Init Acts A (A' Un B')"; +\ ==> LeadsTo(Init,Acts) A (A' Un B')"; by (blast_tac (claset() addIs [LeadsTo_Un_Un, subset_imp_LeadsTo, LeadsTo_Trans]) 1); qed "LeadsTo_cancel2"; Goal - "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts (B-A') B'; id: Acts |] \ -\ ==> LeadsTo Init Acts A (A' Un B')"; + "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) A (A' Un B')"; by (rtac LeadsTo_cancel2 1); by (assume_tac 2); by (ALLGOALS Asm_simp_tac); qed "LeadsTo_cancel_Diff2"; Goal - "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts B B'; id: Acts |] \ -\ ==> LeadsTo Init Acts A (B' Un A')"; + "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) 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 - "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts (B-A') B'; id: Acts |] \ -\ ==> LeadsTo Init Acts A (B' Un A')"; + "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) A (B' Un A')"; by (rtac LeadsTo_cancel1 1); by (assume_tac 2); by (ALLGOALS Asm_simp_tac); @@ -233,9 +233,8 @@ (** The impossibility law **) -Goalw [LeadsTo_def] - "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A = {}"; -by (Full_simp_tac 1); +Goal "LeadsTo(Init,Acts) A {} ==> reachable(Init,Acts) Int A = {}"; +by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (etac leadsTo_empty 1); qed "LeadsTo_empty"; @@ -243,22 +242,21 @@ (** PSP: Progress-Safety-Progress **) (*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *) -Goalw [LeadsTo_def] - "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \ -\ ==> LeadsTo Init Acts (A Int B) (A' Int B)"; -by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1); +Goal "[| LeadsTo(Init,Acts) A A'; stable Acts B |] \ +\ ==> LeadsTo(Init,Acts) (A Int B) (A' Int B)"; +by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, + PSP_stable]) 1); qed "R_PSP_stable"; -Goal - "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \ -\ ==> LeadsTo Init Acts (B Int A) (B Int A')"; +Goal "[| LeadsTo(Init,Acts) A A'; stable Acts B |] \ +\ ==> LeadsTo(Init,Acts) (B Int A) (B Int A')"; by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1); qed "R_PSP_stable2"; -Goalw [LeadsTo_def] - "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \ -\ ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))"; +Goal "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B) Un (B' - B))"; +by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (dtac PSP 1); by (etac constrains_reachable 1); by (etac leadsTo_weaken 2); @@ -266,14 +264,14 @@ qed "R_PSP"; Goal - "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \ -\ ==> LeadsTo Init Acts (B Int A) ((B Int A') Un (B' - B))"; + "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) (B Int A) ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1); qed "R_PSP2"; Goalw [unless_def] - "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \ -\ ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')"; + "[| LeadsTo(Init,Acts) A A'; unless Acts B B'; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B) Un B')"; by (dtac R_PSP 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2); @@ -287,12 +285,13 @@ (*** Induction rules ***) (** Meta or object quantifier ????? **) -Goalw [LeadsTo_def] - "!!Acts. [| wf r; \ -\ ALL m. LeadsTo Init Acts (A Int f-``{m}) \ +Goal + "[| wf r; \ +\ ALL m. LeadsTo(Init,Acts) (A Int f-``{m}) \ \ ((A Int f-``(r^-1 ^^ {m})) Un B); \ \ id: Acts |] \ -\ ==> LeadsTo Init Acts A B"; +\ ==> LeadsTo(Init,Acts) A B"; +by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (etac leadsTo_wf_induct 1); by (assume_tac 2); by (blast_tac (claset() addIs [leadsTo_weaken]) 1); @@ -300,11 +299,11 @@ Goal - "!!Acts. [| wf r; \ -\ ALL m:I. LeadsTo Init Acts (A Int f-``{m}) \ + "[| wf r; \ +\ ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m}) \ \ ((A Int f-``(r^-1 ^^ {m})) Un B); \ \ id: Acts |] \ -\ ==> LeadsTo Init Acts A ((A - (f-``I)) Un B)"; +\ ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)"; by (etac LeadsTo_wf_induct 1); by Safe_tac; by (case_tac "m:I" 1); @@ -314,20 +313,20 @@ Goal - "!!Acts. [| ALL m. LeadsTo Init Acts (A Int f-``{m}) \ + "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m}) \ \ ((A Int f-``(lessThan m)) Un B); \ \ id: Acts |] \ -\ ==> LeadsTo Init Acts A B"; +\ ==> LeadsTo(Init,Acts) A B"; by (rtac (wf_less_than RS LeadsTo_wf_induct) 1); by (assume_tac 2); by (Asm_simp_tac 1); qed "R_lessThan_induct"; Goal - "!!Acts. [| ALL m:(greaterThan l). LeadsTo Init Acts (A Int f-``{m}) \ + "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m}) \ \ ((A Int f-``(lessThan m)) Un B); \ \ id: Acts |] \ -\ ==> LeadsTo Init Acts A ((A Int (f-``(atMost l))) Un B)"; +\ ==> LeadsTo(Init,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); by (rtac (wf_less_than RS R_bounded_induct) 1); by (assume_tac 2); @@ -335,10 +334,10 @@ qed "R_lessThan_bounded_induct"; Goal - "!!Acts. [| ALL m:(lessThan l). LeadsTo Init Acts (A Int f-``{m}) \ + "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m}) \ \ ((A Int f-``(greaterThan m)) Un B); \ \ id: Acts |] \ -\ ==> LeadsTo Init Acts A ((A Int (f-``(atLeast l))) Un B)"; +\ ==> LeadsTo(Init,Acts) 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); @@ -353,20 +352,20 @@ (*** Completion: Binary and General Finite versions ***) -Goalw [LeadsTo_def] - "!!Acts. [| LeadsTo Init Acts A A'; stable Acts A'; \ -\ LeadsTo Init Acts B B'; stable Acts B'; id: Acts |] \ -\ ==> LeadsTo Init Acts (A Int B) (A' Int B')"; +Goal + "[| LeadsTo(Init,Acts) A A'; stable Acts A'; \ +\ LeadsTo(Init,Acts) B B'; stable Acts B'; id: Acts |] \ +\ ==> LeadsTo(Init,Acts) (A Int B) (A' Int B')"; +by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] addSIs [stable_Int, stable_reachable]) 1); qed "R_stable_completion"; -Goal - "!!Acts. [| finite I; id: Acts |] \ -\ ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i)) --> \ +Goal "[| finite I; id: Acts |] \ +\ ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) --> \ \ (ALL i:I. stable Acts (A' i)) --> \ -\ LeadsTo Init Acts (INT i:I. A i) (INT i:I. A' i)"; +\ LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)"; by (etac finite_induct 1); by (Asm_simp_tac 1); by (asm_simp_tac @@ -375,13 +374,13 @@ qed_spec_mp "R_finite_stable_completion"; -Goalw [LeadsTo_def] - "!!Acts. [| LeadsTo Init Acts A (A' Un C); constrains Acts A' (A' Un C); \ -\ LeadsTo Init Acts B (B' Un C); constrains Acts B' (B' Un C); \ +Goal + "[| LeadsTo(Init,Acts) A (A' Un C); constrains Acts A' (A' Un C); \ +\ LeadsTo(Init,Acts) B (B' Un C); constrains Acts B' (B' Un C); \ \ id: Acts |] \ -\ ==> LeadsTo Init Acts (A Int B) ((A' Int B') Un C)"; +\ ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)"; -by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1); +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1); by (dtac completion 1); by (assume_tac 2); by (ALLGOALS @@ -392,10 +391,10 @@ Goal - "!!Acts. [| finite I; id: Acts |] \ -\ ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i Un C)) --> \ + "[| finite I; id: Acts |] \ +\ ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) --> \ \ (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \ -\ LeadsTo Init Acts (INT i:I. A i) ((INT i:I. A' i) Un C)"; +\ LeadsTo(Init,Acts) (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 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/SubstAx.thy Thu Jul 02 16:53:55 1998 +0200 @@ -10,10 +10,10 @@ constdefs - LeadsTo :: "['a set, ('a * 'a)set set, 'a set, 'a set] => bool" - "LeadsTo Init Acts A B == - leadsTo Acts (reachable Init Acts Int A) - (reachable Init Acts Int B)" + LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool" + "LeadsTo == %(Init,Acts) A B. + leadsTo Acts (reachable (Init,Acts) Int A) + (reachable (Init,Acts) Int B)" end diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Token.ML --- a/src/HOL/UNITY/Token.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Token.ML Thu Jul 02 16:53:55 1998 +0200 @@ -16,11 +16,11 @@ AddIffs [N_positive, skip]; -Goalw [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j"; +Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j"; by Auto_tac; qed "HasToK_partition"; -Goalw Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)"; +Goalw Token_defs "s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)"; by (Simp_tac 1); by (exhaust_tac "s (Suc i)" 1); by Auto_tac; @@ -61,13 +61,13 @@ by (Blast_tac 1); qed"wf_nodeOrder"; -Goal "!!m. [| m Suc(m) < n"; +Goal "[| m Suc(m) < n"; by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); by (blast_tac (claset() addEs [less_asym, less_SucE]) 1); qed "Suc_lessI"; Goalw [nodeOrder_def, next_def, inv_image_def] - "!!x. [| i ((next i, i) : nodeOrder j) = (i ~= j)"; + "[| i ((next i, i) : nodeOrder j) = (i ~= j)"; by (auto_tac (claset(), simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq])); by (dtac sym 1); @@ -100,7 +100,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. [| i \ + "[| i \ \ leadsTo Acts (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); @@ -112,7 +112,7 @@ (*Chapter 4 variant, the one actually used below.*) Goal - "!!i. [| i \ + "[| i \ \ leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}"; by (rtac (TR7 RS leadsTo_weaken_R) 1); by (Clarify_tac 1); @@ -127,7 +127,7 @@ (*Misra's TR9: the token reaches an arbitrary node*) Goal - "!!i. j leadsTo Acts {s. Token s < N} (HasTok j)"; + "j leadsTo Acts {s. Token s < N} (HasTok j)"; by (rtac leadsTo_weaken_R 1); by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")] (wf_nodeOrder RS bounded_induct) 1); @@ -141,7 +141,7 @@ qed "leadsTo_j"; (*Misra's TR8: a hungry process eventually eats*) -Goal "!!i. j leadsTo Acts ({s. Token s < N} Int H j) (E j)"; +Goal "j leadsTo Acts ({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 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Traces.ML --- a/src/HOL/UNITY/Traces.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Traces.ML Thu Jul 02 16:53:55 1998 +0200 @@ -1,39 +1,81 @@ +(* Title: HOL/UNITY/Traces + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +Definitions of + * traces: the possible execution traces + * reachable: the set of reachable states + +*) + open Traces; -Goal "reachable Init Acts <= {s. EX evs. s#evs: traces Init Acts}"; -by (rtac subsetI 1); -be reachable.induct 1; -by (REPEAT (blast_tac (claset() addIs traces.intrs) 1)); -val lemma1 = result(); + +(**** +Now simulate the inductive definition (illegal due to paired arguments) + +inductive "reachable(Init,Acts)" + intrs + Init "s: Init ==> s : reachable(Init,Acts)" + + Acts "[| act: Acts; s : reachable(Init,Acts); (s,s'): act |] + ==> s' : reachable(Init,Acts)" -Goal "!!evs. evs : traces Init Acts \ -\ ==> ALL s evs'. evs = s#evs' --> s: reachable Init Acts"; -be traces.induct 1; -by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); -val lemma2 = normalize_thm [RSmp, RSspec] (result()); +This amounts to an equivalence proof for the definition actually used, +****) + -Goal "{s. EX evs. s#evs: traces Init Acts} <= reachable Init Acts"; -by (blast_tac (claset() addIs [lemma2]) 1); -val lemma3 = result(); +(** reachable: Deriving the Introduction rules **) -Goal "reachable Init Acts = {s. EX evs. s#evs: traces Init Acts}"; -by (rtac ([lemma1,lemma3] MRS equalityI) 1); -qed "reachable_eq_traces"; +Goal "s: Init ==> s : reachable(Init,Acts)"; +by (simp_tac (simpset() addsimps [reachable_def]) 1); +by (blast_tac (claset() addIs traces.intrs) 1); +qed "reachable_Init"; -(*Could/should this be proved?*) -Goal "reachable Init Acts = (UN evs: traces Init Acts. set evs)"; +Goal "[| act: Acts; s : reachable(Init,Acts) |] \ +\ ==> (s,s'): act --> s' : reachable(Init,Acts)"; +by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); +by (etac exE 1); +be traces.induct 1; +by (ALLGOALS Asm_simp_tac); +by (ALLGOALS (blast_tac (claset() addIs traces.intrs))); +qed_spec_mp "reachable_Acts"; + + +val major::prems = +Goalw [reachable_def] + "[| za : reachable(Init,Acts); \ +\ !!s. s : Init ==> P s; \ +\ !!act s s'. \ +\ [| act : Acts; s : reachable(Init,Acts); P s; (s, s') : act |] \ +\ ==> P s' |] \ +\ ==> P za"; +by (cut_facts_tac [major] 1); +auto(); +be traces.induct 1; +by (ALLGOALS (blast_tac (claset() addIs prems))); +qed "reachable_induct"; + +structure reachable = + struct + val Init = reachable_Init + val Acts = reachable_Acts + val intrs = [reachable_Init, reachable_Acts] + val induct = reachable_induct + end; (*The strongest invariant is the set of all reachable states!*) Goalw [stable_def, constrains_def] - "!!A. [| Init<=A; stable Acts A |] ==> reachable Init Acts <= A"; + "[| Init<=A; stable Acts A |] ==> reachable(Init,Acts) <= A"; by (rtac subsetI 1); be reachable.induct 1; by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); qed "strongest_invariant"; -Goal "stable Acts (reachable Init Acts)"; +Goal "stable Acts (reachable(Init,Acts))"; by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI] addIs reachable.intrs) 1)); qed "stable_reachable"; diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Traces.thy --- a/src/HOL/UNITY/Traces.thy Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/Traces.thy Thu Jul 02 16:53:55 1998 +0200 @@ -1,23 +1,30 @@ +(* Title: HOL/UNITY/Traces + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +Inductive definitions of + * traces: the possible execution traces + * reachable: the set of reachable states +*) + Traces = UNITY + -consts traces :: "['a set, ('a * 'a)set set] => 'a list set" +consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" -inductive "traces Init Acts" + (*Initial states and program => (final state, reversed trace to it)... + Arguments MUST be curried in an inductive definition*) + +inductive "traces Init Acts" intrs (*Initial trace is empty*) - Init "s: Init ==> [s] : traces Init Acts" + Init "s: Init ==> (s,[]) : traces Init Acts" - Acts "[| act: Acts; s#evs : traces Init Acts; (s,s'): act |] - ==> s'#s#evs : traces Init Acts" + Acts "[| act: Acts; (s,evs) : traces Init Acts; (s,s'): act |] + ==> (s', s#evs) : traces Init Acts" -consts reachable :: "['a set, ('a * 'a)set set] => 'a set" - -inductive "reachable Init Acts" - intrs - Init "s: Init ==> s : reachable Init Acts" - - Acts "[| act: Acts; s : reachable Init Acts; (s,s'): act |] - ==> s' : reachable Init Acts" +constdefs reachable :: "'a set * ('a * 'a)set set => 'a set" + "reachable == %(Init,Acts). {s. EX evs. (s,evs): traces Init Acts}" end diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/UNITY.ML Thu Jul 02 16:53:55 1998 +0200 @@ -18,11 +18,11 @@ be any set including A Int C and contained in A Un C, such as B=A or B=C. **) -Goal "!!x. [| A Int C <= B; B <= A Un C |] \ +Goal "[| A Int C <= B; B <= A Un C |] \ \ ==> (A Int B) Un (Compl A Int C) = B Un C"; by (Blast_tac 1); -Goal "!!x. [| A Int C <= B; B <= A Un C |] \ +Goal "[| A Int C <= B; B <= A Un C |] \ \ ==> (A Un B) Int (Compl A Un C) = B Int C"; by (Blast_tac 1); @@ -64,7 +64,7 @@ qed "constrainsI"; Goalw [constrains_def] - "!!Acts. [| constrains Acts A A'; act: Acts; (s,s'): act; s: A |] \ + "[| constrains Acts A A'; act: Acts; (s,s'): act; s: A |] \ \ ==> s': A'"; by (Blast_tac 1); qed "constrainsD"; @@ -79,23 +79,23 @@ AddIffs [constrains_empty, constrains_UNIV]; Goalw [constrains_def] - "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'"; + "[| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'"; by (Blast_tac 1); qed "constrains_weaken_R"; Goalw [constrains_def] - "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'"; + "[| constrains Acts A A'; B<=A |] ==> constrains Acts B A'"; by (Blast_tac 1); qed "constrains_weaken_L"; Goalw [constrains_def] - "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'"; + "[| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'"; by (Blast_tac 1); qed "constrains_weaken"; (*Set difference: UNUSED*) Goalw [constrains_def] - "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \ + "[| constrains Acts (A-B) C; constrains Acts B C |] \ \ ==> constrains Acts A C"; by (Blast_tac 1); qed "constrains_Diff"; @@ -103,19 +103,19 @@ (** Union **) Goalw [constrains_def] - "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \ + "[| constrains Acts A A'; constrains Acts B B' |] \ \ ==> constrains Acts (A Un B) (A' Un B')"; by (Blast_tac 1); qed "constrains_Un"; Goalw [constrains_def] - "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \ + "ALL i:I. constrains Acts (A i) (A' i) \ \ ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)"; by (Blast_tac 1); qed "ball_constrains_UN"; Goalw [constrains_def] - "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \ + "[| ALL i. constrains Acts (A i) (A' i) |] \ \ ==> constrains Acts (UN i. A i) (UN i. A' i)"; by (Blast_tac 1); qed "all_constrains_UN"; @@ -123,31 +123,31 @@ (** Intersection **) Goalw [constrains_def] - "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \ + "[| constrains Acts A A'; constrains Acts B B' |] \ \ ==> constrains Acts (A Int B) (A' Int B')"; by (Blast_tac 1); qed "constrains_Int"; Goalw [constrains_def] - "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \ + "ALL i:I. constrains Acts (A i) (A' i) \ \ ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)"; by (Blast_tac 1); qed "ball_constrains_INT"; Goalw [constrains_def] - "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \ + "[| ALL i. constrains Acts (A i) (A' i) |] \ \ ==> constrains Acts (INT i. A i) (INT i. A' i)"; by (Blast_tac 1); qed "all_constrains_INT"; Goalw [stable_def, constrains_def] - "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |] \ + "[| stable Acts C; constrains Acts A (C Un A') |] \ \ ==> constrains Acts (C Un A) (C Un A')"; by (Blast_tac 1); qed "stable_constrains_Un"; Goalw [stable_def, constrains_def] - "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |] \ + "[| stable Acts C; constrains Acts (C Int A) A' |] \ \ ==> constrains Acts (C Int A) (C Int A')"; by (Blast_tac 1); qed "stable_constrains_Int"; @@ -156,35 +156,35 @@ (*** stable ***) Goalw [stable_def] - "!!Acts. constrains Acts A A ==> stable Acts A"; + "constrains Acts A A ==> stable Acts A"; by (assume_tac 1); qed "stableI"; Goalw [stable_def] - "!!Acts. stable Acts A ==> constrains Acts A A"; + "stable Acts A ==> constrains Acts A A"; by (assume_tac 1); qed "stableD"; Goalw [stable_def] - "!!Acts. [| stable Acts A; stable Acts A' |] \ + "[| stable Acts A; stable Acts A' |] \ \ ==> stable Acts (A Un A')"; by (blast_tac (claset() addIs [constrains_Un]) 1); qed "stable_Un"; Goalw [stable_def] - "!!Acts. [| stable Acts A; stable Acts A' |] \ + "[| stable Acts A; stable Acts A' |] \ \ ==> stable Acts (A Int A')"; by (blast_tac (claset() addIs [constrains_Int]) 1); qed "stable_Int"; Goalw [constrains_def] - "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'"; + "[| constrains Acts A A'; id: Acts |] ==> A<=A'"; by (Blast_tac 1); qed "constrains_imp_subset"; Goalw [constrains_def] - "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |] \ + "[| id: Acts; constrains Acts A B; constrains Acts B C |] \ \ ==> constrains Acts A C"; by (Blast_tac 1); qed "constrains_trans"; @@ -194,7 +194,7 @@ Should the premise be !!m instead of ALL m ? Would make it harder to use in forward proof.*) Goalw [constrains_def] - "!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \ + "[| ALL m. constrains Acts {s. s x = m} (B m) |] \ \ ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int B m)"; by (Blast_tac 1); qed "elimination"; @@ -202,14 +202,14 @@ (*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] - "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \ + "[| ALL m. constrains Acts {m} (B m) |] \ \ ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)"; by (Blast_tac 1); qed "elimination_sing"; Goalw [constrains_def] - "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \ + "[| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \ \ ==> constrains Acts A (A' Un B')"; by (Blast_tac 1); qed "constrains_cancel"; @@ -224,6 +224,6 @@ qed "constrains_strongest_rhs"; Goalw [constrains_def, strongest_rhs_def] - "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B"; + "constrains Acts A B ==> strongest_rhs Acts A <= B"; by (Blast_tac 1); qed "strongest_rhs_is_strongest"; diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/WFair.ML --- a/src/HOL/UNITY/WFair.ML Thu Jul 02 16:44:39 1998 +0200 +++ b/src/HOL/UNITY/WFair.ML Thu Jul 02 16:53:55 1998 +0200 @@ -18,19 +18,19 @@ (*** transient ***) Goalw [stable_def, constrains_def, transient_def] - "!!A. [| stable Acts A; transient Acts A |] ==> A = {}"; + "[| stable Acts A; transient Acts A |] ==> A = {}"; by (Blast_tac 1); qed "stable_transient_empty"; Goalw [transient_def] - "!!A. [| transient Acts A; B<=A |] ==> transient Acts B"; + "[| transient Acts A; B<=A |] ==> transient Acts B"; by (Clarify_tac 1); by (rtac bexI 1 THEN assume_tac 2); by (Blast_tac 1); qed "transient_strengthen"; Goalw [transient_def] - "!!A. [| act:Acts; A <= Domain act; act^^A <= Compl A |] \ + "[| act:Acts; A <= Domain act; act^^A <= Compl A |] \ \ ==> transient Acts A"; by (Blast_tac 1); qed "transient_mem"; @@ -39,31 +39,31 @@ (*** ensures ***) Goalw [ensures_def] - "!!Acts. [| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \ + "[| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \ \ ==> ensures Acts A B"; by (Blast_tac 1); qed "ensuresI"; Goalw [ensures_def] - "!!Acts. ensures Acts A B \ + "ensures Acts A B \ \ ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)"; by (Blast_tac 1); qed "ensuresD"; (*The L-version (precondition strengthening) doesn't hold for ENSURES*) Goalw [ensures_def] - "!!Acts. [| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'"; + "[| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'"; by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); qed "ensures_weaken_R"; Goalw [ensures_def, constrains_def, transient_def] - "!!Acts. Acts ~= {} ==> ensures Acts A UNIV"; + "Acts ~= {} ==> ensures Acts A UNIV"; by (Asm_simp_tac 1); (*omitting this causes PROOF FAILED, even with Safe_tac*) by (Blast_tac 1); qed "ensures_UNIV"; Goalw [ensures_def] - "!!Acts. [| stable Acts C; \ + "[| 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')"; @@ -79,17 +79,17 @@ bind_thm ("leadsTo_Basis", leadsto.Basis); bind_thm ("leadsTo_Trans", leadsto.Trans); -Goal "!!Acts. act: Acts ==> leadsTo Acts A UNIV"; +Goal "act: Acts ==> leadsTo Acts A UNIV"; by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1); qed "leadsTo_UNIV"; Addsimps [leadsTo_UNIV]; (*Useful with cancellation, disjunction*) -Goal "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'"; +Goal "leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "leadsTo_Un_duplicate"; -Goal "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)"; +Goal "leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "leadsTo_Un_duplicate2"; @@ -107,7 +107,7 @@ (*Binary union introduction rule*) Goal - "!!C. [| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C"; + "[| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C"; by (stac Un_eq_Union 1); by (blast_tac (claset() addIs [leadsTo_Union]) 1); qed "leadsTo_Un"; @@ -126,7 +126,7 @@ qed "leadsTo_induct"; -Goal "!!A B. [| A<=B; id: Acts |] ==> leadsTo Acts A B"; +Goal "[| A<=B; id: Acts |] ==> leadsTo Acts A B"; by (rtac leadsTo_Basis 1); by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); by (Blast_tac 1); @@ -138,7 +138,7 @@ (*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it needs the extra premise id:Acts*) -Goal "!!Acts. leadsTo Acts A A' ==> A'<=B' --> leadsTo Acts A B'"; +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); @@ -147,7 +147,7 @@ qed_spec_mp "leadsTo_weaken_R"; -Goal "!!Acts. [| leadsTo Acts A A'; B<=A; id: Acts |] ==> \ +Goal "[| leadsTo Acts A A'; B<=A; id: Acts |] ==> \ \ leadsTo Acts B A'"; by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, subset_imp_leadsTo]) 1); @@ -155,26 +155,26 @@ (*Distributes over binary unions*) Goal - "!!C. id: Acts ==> \ + "id: Acts ==> \ \ leadsTo Acts (A Un B) C = (leadsTo Acts A C & leadsTo Acts B C)"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); qed "leadsTo_Un_distrib"; Goal - "!!C. id: Acts ==> \ + "id: Acts ==> \ \ leadsTo Acts (UN i:I. A i) B = (ALL i : I. leadsTo Acts (A i) B)"; by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); qed "leadsTo_UN_distrib"; Goal - "!!C. id: Acts ==> \ + "id: Acts ==> \ \ leadsTo Acts (Union S) B = (ALL A : S. leadsTo Acts A B)"; by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); qed "leadsTo_Union_distrib"; Goal - "!!Acts. [| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \ + "[| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \ \ ==> leadsTo Acts B B'"; (*PROOF FAILED: why?*) by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R, @@ -184,7 +184,7 @@ (*Set difference: maybe combine with leadsTo_weaken_L??*) Goal - "!!C. [| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \ + "[| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \ \ ==> leadsTo Acts A C"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1); qed "leadsTo_Diff"; @@ -212,14 +212,14 @@ (*Version with no index set*) Goal - "!!Acts. ALL i. leadsTo Acts (A i) (A' i) \ + "ALL i. leadsTo Acts (A i) (A' i) \ \ ==> leadsTo Acts (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 "!!Acts. [| leadsTo Acts A A'; leadsTo Acts B B' |] \ +Goal "[| leadsTo Acts A A'; leadsTo Acts B B' |] \ \ ==> leadsTo Acts (A Un B) (A' Un B')"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]) 1); @@ -229,14 +229,14 @@ (** The cancellation law **) Goal - "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \ + "[| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \ \ ==> leadsTo Acts A (A' Un B')"; by (blast_tac (claset() addIs [leadsTo_Un_Un, subset_imp_leadsTo, leadsTo_Trans]) 1); qed "leadsTo_cancel2"; Goal - "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \ + "[| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \ \ ==> leadsTo Acts A (A' Un B')"; by (rtac leadsTo_cancel2 1); by (assume_tac 2); @@ -244,14 +244,14 @@ qed "leadsTo_cancel_Diff2"; Goal - "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \ + "[| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \ \ ==> leadsTo Acts 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 - "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \ + "[| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \ \ ==> leadsTo Acts A (B' Un A')"; by (rtac leadsTo_cancel1 1); by (assume_tac 2); @@ -262,14 +262,14 @@ (** The impossibility law **) -Goal "!!Acts. leadsTo Acts A B ==> B={} --> A={}"; +Goal "leadsTo Acts 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 "!!Acts. leadsTo Acts A {} ==> A={}"; +Goal "leadsTo Acts A {} ==> A={}"; by (blast_tac (claset() addSIs [lemma]) 1); qed "leadsTo_empty"; @@ -278,7 +278,7 @@ (*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *) Goalw [stable_def] - "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \ + "[| leadsTo Acts A A'; stable Acts B |] \ \ ==> leadsTo Acts (A Int B) (A' Int B)"; by (etac leadsTo_induct 1); by (simp_tac (simpset() addsimps [Int_Union_Union]) 3); @@ -292,14 +292,14 @@ qed "PSP_stable"; Goal - "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \ + "[| leadsTo Acts A A'; stable Acts B |] \ \ ==> leadsTo Acts (B Int A) (B Int A')"; by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1); qed "PSP_stable2"; Goalw [ensures_def] - "!!Acts. [| ensures Acts A A'; constrains Acts B B' |] \ + "[| ensures Acts A A'; constrains Acts B B' |] \ \ ==> ensures Acts (A Int B) ((A' Int B) Un (B' - B))"; by Safe_tac; by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1); @@ -309,7 +309,7 @@ Goal - "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \ + "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \ \ ==> leadsTo Acts (A Int B) ((A' Int B) Un (B' - B))"; by (etac leadsTo_induct 1); by (simp_tac (simpset() addsimps [Int_Union_Union]) 3); @@ -324,14 +324,14 @@ qed "PSP"; Goal - "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \ + "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \ \ ==> leadsTo Acts (B Int A) ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1); qed "PSP2"; Goalw [unless_def] - "!!Acts. [| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \ + "[| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \ \ ==> leadsTo Acts (A Int B) ((A' Int B) Un B')"; by (dtac PSP 1); by (assume_tac 1); @@ -346,7 +346,7 @@ (*** Proving the induction rules ***) Goal - "!!Acts. [| wf r; \ + "[| wf r; \ \ ALL m. leadsTo Acts (A Int f-``{m}) \ \ ((A Int f-``(r^-1 ^^ {m})) Un B); \ \ id: Acts |] \ @@ -362,7 +362,7 @@ (** Meta or object quantifier ????? **) Goal - "!!Acts. [| wf r; \ + "[| wf r; \ \ ALL m. leadsTo Acts (A Int f-``{m}) \ \ ((A Int f-``(r^-1 ^^ {m})) Un B); \ \ id: Acts |] \ @@ -376,7 +376,7 @@ Goal - "!!Acts. [| wf r; \ + "[| wf r; \ \ ALL m:I. leadsTo Acts (A Int f-``{m}) \ \ ((A Int f-``(r^-1 ^^ {m})) Un B); \ \ id: Acts |] \ @@ -391,7 +391,7 @@ (*Alternative proof is via the lemma leadsTo Acts (A Int f-``(lessThan m)) B*) Goal - "!!Acts. [| ALL m. leadsTo Acts (A Int f-``{m}) \ + "[| ALL m. leadsTo Acts (A Int f-``{m}) \ \ ((A Int f-``(lessThan m)) Un B); \ \ id: Acts |] \ \ ==> leadsTo Acts A B"; @@ -401,7 +401,7 @@ qed "lessThan_induct"; Goal - "!!Acts. [| ALL m:(greaterThan l). leadsTo Acts (A Int f-``{m}) \ + "[| 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)"; @@ -412,7 +412,7 @@ qed "lessThan_bounded_induct"; Goal - "!!Acts. [| ALL m:(lessThan l). leadsTo Acts (A Int f-``{m}) \ + "[| 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)"; @@ -435,18 +435,18 @@ by (blast_tac (claset() addSIs [leadsTo_Union]) 1); qed "wlt_leadsTo"; -Goalw [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B"; +Goalw [wlt_def] "leadsTo Acts A B ==> A <= wlt Acts B"; by (blast_tac (claset() addSIs [leadsTo_Union]) 1); qed "leadsTo_subset"; (*Misra's property W2*) -Goal "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)"; +Goal "id: Acts ==> leadsTo Acts A B = (A <= wlt Acts 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 "!!Acts. id: Acts ==> B <= wlt Acts B"; +Goal "id: Acts ==> B <= wlt Acts B"; by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym, subset_imp_leadsTo]) 1); qed "wlt_increasing"; @@ -454,7 +454,7 @@ (*Used in the Trans case below*) Goalw [constrains_def] - "!!Acts. [| B <= A2; \ + "[| 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)"; @@ -465,7 +465,7 @@ (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) Goal - "!!Acts. [| leadsTo Acts A A'; id: Acts |] ==> \ + "[| leadsTo Acts A A'; id: Acts |] ==> \ \ EX B. A<=B & leadsTo Acts B A' & constrains Acts (B-A') (B Un A')"; by (etac leadsTo_induct 1); (*Basis*) @@ -485,7 +485,7 @@ (*Misra's property W5*) -Goal "!!Acts. id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)"; +Goal "id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)"; by (forward_tac [wlt_leadsTo RS leadsTo_123] 1); by (Clarify_tac 1); by (subgoal_tac "Ba = wlt Acts B" 1); @@ -498,7 +498,7 @@ (*** Completion: Binary and General Finite versions ***) Goal - "!!Acts. [| leadsTo Acts A A'; stable Acts A'; \ + "[| 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); @@ -520,7 +520,7 @@ Goal - "!!Acts. [| finite I; id: Acts |] \ + "[| 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)"; @@ -533,7 +533,7 @@ Goal - "!!Acts. [| W = wlt Acts (B' Un C); \ + "[| 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 |] \ @@ -563,7 +563,7 @@ Goal - "!!Acts. [| finite I; id: Acts |] \ + "[| 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)";