Uncurried functions LeadsTo and reach
Deleted leading parameters thanks to new Goal command
--- 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";
--- 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";
--- 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();
--- 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);
--- 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
--- 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);
--- 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);
--- 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
--- 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<n; Suc m ~= n |] ==> Suc(m) < n";
+Goal "[| m<n; Suc m ~= n |] ==> 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<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
+ "[| i<N; j<N |] ==> ((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<N; j<N |] ==> \
+ "[| i<N; j<N |] ==> \
\ 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<N; j<N; i~=j |] ==> \
+ "[| i<N; j<N; i~=j |] ==> \
\ 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<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
+ "j<N ==> 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<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
+Goal "j<N ==> 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);
--- 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";
--- 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
--- 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";
--- 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)";