A higher-level treatment of LeadsTo, minimizing use of "reachable"
authorpaulson
Thu Aug 06 15:47:26 1998 +0200 (1998-08-06)
changeset 5277e4297d03e5d2
parent 5276 dd99b958b306
child 5278 a903b66822e2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
src/HOL/UNITY/Channel.ML
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Common.thy
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/Lift.thy
src/HOL/UNITY/Mutex.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Token.ML
src/HOL/UNITY/Token.thy
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/WFair.ML
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/UNITY/Channel.ML	Thu Aug 06 14:04:49 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Channel.ML	Thu Aug 06 15:47:26 1998 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
     1.6  by (rtac leadsTo_weaken 1);
     1.7 -by (rtac ([UC2, UC1] MRS PSP) 1);
     1.8 +by (rtac ([UC2, UC1] MRS psp) 1);
     1.9  by (ALLGOALS Asm_simp_tac);
    1.10  by (Blast_tac 1);
    1.11  by Safe_tac;
     2.1 --- a/src/HOL/UNITY/Common.ML	Thu Aug 06 14:04:49 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Common.ML	Thu Aug 06 15:47:26 1998 +0200
     2.3 @@ -71,8 +71,7 @@
     2.4  
     2.5  Addsimps [atMost_Int_atLeast];
     2.6  
     2.7 -Goal
     2.8 -    "[| ALL m. constrains acts {m} (maxfg m); \
     2.9 +Goal "[| ALL m. constrains acts {m} (maxfg m); \
    2.10  \               ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \
    2.11  \               n: common;  id: acts |]  \
    2.12  \            ==> leadsTo acts (atMost n) common";
    2.13 @@ -80,13 +79,12 @@
    2.14  by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
    2.15  by (ALLGOALS Asm_simp_tac);
    2.16  by (rtac subset_refl 2);
    2.17 -by (blast_tac (claset() addDs [PSP_stable2] 
    2.18 +by (blast_tac (claset() addDs [psp_stable2] 
    2.19                          addIs [common_stable, leadsTo_weaken_R]) 1);
    2.20  val lemma = result();
    2.21  
    2.22  (*The "ALL m: Compl common" form echoes CMT6.*)
    2.23 -Goal
    2.24 -    "[| ALL m. constrains acts {m} (maxfg m); \
    2.25 +Goal "[| ALL m. constrains acts {m} (maxfg m); \
    2.26  \               ALL m: Compl common. leadsTo acts {m} (greaterThan m); \
    2.27  \               n: common;  id: acts |]  \
    2.28  \            ==> leadsTo acts (atMost (LEAST n. n: common)) common";
     3.1 --- a/src/HOL/UNITY/Common.thy	Thu Aug 06 14:04:49 1998 +0200
     3.2 +++ b/src/HOL/UNITY/Common.thy	Thu Aug 06 15:47:26 1998 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
     3.5  *)
     3.6  
     3.7 -Common = WFair +
     3.8 +Common = WFair + Traces +
     3.9  
    3.10  consts
    3.11    ftime,gtime :: nat=>nat
     4.1 --- a/src/HOL/UNITY/Handshake.ML	Thu Aug 06 14:04:49 1998 +0200
     4.2 +++ b/src/HOL/UNITY/Handshake.ML	Thu Aug 06 15:47:26 1998 +0200
     4.3 @@ -48,7 +48,7 @@
     4.4  Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
     4.5  br LeadsTo_weaken_R 1;
     4.6  by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
     4.7 -    R_greaterThan_bounded_induct 1);
     4.8 +    GreaterThan_bounded_induct 1);
     4.9  by (auto_tac (claset(), simpset() addsimps [vimage_def]));
    4.10  by (trans_tac 2);
    4.11  (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Aug 06 15:47:26 1998 +0200
     5.3 @@ -0,0 +1,142 @@
     5.4 +(*  Title:      HOL/UNITY/Lift
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1998  University of Cambridge
     5.8 +
     5.9 +The Lift-Control Example
    5.10 +*)
    5.11 +
    5.12 +val always_defs = [above_def, below_def, queueing_def, 
    5.13 +		   goingup_def, goingdown_def, ready_def];
    5.14 +
    5.15 +val cmd_defs = [Lprg_def, 
    5.16 +		request_act_def, open_act_def, close_act_def,
    5.17 +		req_up_act_def, req_down_act_def, move_up_def, move_down_def];
    5.18 +
    5.19 +AddIffs [min_le_max];
    5.20 +
    5.21 +Goalw [Lprg_def] "id : Acts Lprg";
    5.22 +by (Simp_tac 1);
    5.23 +qed "id_in_Acts";
    5.24 +AddIffs [id_in_Acts];
    5.25 +
    5.26 +
    5.27 +(*split_all_tac causes a big blow-up*)
    5.28 +claset_ref() := claset() delSWrapper "split_all_tac";
    5.29 +
    5.30 +(*Simplification for records*)
    5.31 +Addsimps (thms"state.update_defs");
    5.32 +
    5.33 +Addsimps [Suc_le_eq];
    5.34 +
    5.35 +Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
    5.36 +	  moving_up_def, moving_down_def];
    5.37 +
    5.38 +
    5.39 +Goal "0 < n ==> (m <= n-1) = (m<n)";
    5.40 +by (exhaust_tac "n" 1);
    5.41 +by Auto_tac;
    5.42 +by (REPEAT_FIRST trans_tac);
    5.43 +qed "le_pred_eq";
    5.44 +
    5.45 +Goal "m < n ==> m <= n-1";
    5.46 +by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
    5.47 +qed "less_imp_le_pred";
    5.48 +
    5.49 +
    5.50 +Goalw [Lprg_def] "invariant Lprg open_stop";
    5.51 +by (rtac invariantI 1);
    5.52 +by (Force_tac 1);
    5.53 +by (constrains_tac (cmd_defs@always_defs) 1);
    5.54 +qed "open_stop";
    5.55 +
    5.56 +Goalw [Lprg_def] "invariant Lprg stop_floor";
    5.57 +by (rtac invariantI 1);
    5.58 +by (Force_tac 1);
    5.59 +by (constrains_tac (cmd_defs@always_defs) 1);
    5.60 +qed "stop_floor";
    5.61 +
    5.62 +(*Should not have to prove open_stop concurrently!!*)
    5.63 +Goalw [Lprg_def] "invariant Lprg (open_stop Int open_move)";
    5.64 +by (rtac invariantI 1);
    5.65 +by (Force_tac 1);
    5.66 +by (constrains_tac (cmd_defs@always_defs) 1);
    5.67 +qed "open_move";
    5.68 +
    5.69 +Goalw [Lprg_def] "invariant Lprg moving_up";
    5.70 +by (rtac invariantI 1);
    5.71 +by (Force_tac 1);
    5.72 +by (constrains_tac (cmd_defs@always_defs) 1);
    5.73 +by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
    5.74 +qed "moving_up";
    5.75 +
    5.76 +Goalw [Lprg_def] "invariant Lprg moving_down";
    5.77 +by (rtac invariantI 1);
    5.78 +by (Force_tac 1);
    5.79 +by (constrains_tac (cmd_defs@always_defs) 1);
    5.80 +by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
    5.81 +by (auto_tac (claset(),
    5.82 +	      simpset() addsimps [gr_implies_gr0 RS le_pred_eq]));
    5.83 +qed "moving_down";
    5.84 +
    5.85 +
    5.86 +xxxxxxxxxxxxxxxx;
    5.87 +
    5.88 +Goalw [Lprg_def] "invariant Lprg bounded";
    5.89 +by (rtac invariantI 1);
    5.90 +by (Force_tac 1);
    5.91 +by (constrains_tac (cmd_defs@always_defs) 1);
    5.92 +by (ALLGOALS
    5.93 +    (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq])));
    5.94 +by (REPEAT_FIRST trans_tac);
    5.95 +by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
    5.96 +by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
    5.97 +by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
    5.98 +qed "bounded";
    5.99 +
   5.100 +Goalw [Lprg_def] "invariant Lprg invariantV";
   5.101 +by (rtac invariantI 1);
   5.102 +by (constrains_tac cmd_defs 2);
   5.103 +by Auto_tac;
   5.104 +qed "invariantV";
   5.105 +
   5.106 +val invariantUV = invariant_Int_rule [invariantU, invariantV];
   5.107 +
   5.108 +
   5.109 +(*The safety property: mutual exclusion*)
   5.110 +Goal "(reachable Lprg) Int {s. MM s = 3 & NN s = 3} = {}";
   5.111 +by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
   5.112 +by Auto_tac;
   5.113 +qed "mutual_exclusion";
   5.114 +
   5.115 +
   5.116 +(*** Progress for U ***)
   5.117 +
   5.118 +Goalw [unless_def] "unless (Acts Lprg) {s. MM s=2} {s. MM s=3}";
   5.119 +by (constrains_tac cmd_defs 1);
   5.120 +qed "U_F0";
   5.121 +
   5.122 +Goal "LeadsTo Lprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
   5.123 +by (ensures_tac cmd_defs "cmd1U" 1);
   5.124 +qed "U_F1";
   5.125 +
   5.126 +Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
   5.127 +by (cut_facts_tac [invariantUV] 1);
   5.128 +bw Lprg_def;
   5.129 +by (ensures_tac cmd_defs "cmd2U" 1);
   5.130 +qed "U_F2";
   5.131 +
   5.132 +Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}";
   5.133 +by (rtac leadsTo_imp_LeadsTo 1); 
   5.134 +by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
   5.135 +by (ensures_tac cmd_defs "cmd4U" 2);
   5.136 +by (ensures_tac cmd_defs "cmd3U" 1);
   5.137 +qed "U_F3";
   5.138 +
   5.139 +Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
   5.140 +by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   5.141 +	  MRS LeadsTo_Diff) 1);
   5.142 +by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   5.143 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
   5.144 +val U_lemma2 = result();
   5.145 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/UNITY/Lift.thy	Thu Aug 06 15:47:26 1998 +0200
     6.3 @@ -0,0 +1,127 @@
     6.4 +(*  Title:      HOL/UNITY/Lift.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1998  University of Cambridge
     6.8 +
     6.9 +The Lift-Control Example
    6.10 +*)
    6.11 +
    6.12 +Lift = SubstAx +
    6.13 +
    6.14 +record state =
    6.15 +  floor :: nat		(*current position of the lift*)
    6.16 +  open  :: bool		(*whether the door is open at floor*)
    6.17 +  stop  :: bool		(*whether the lift is stopped at floor*)
    6.18 +  req   :: nat set	(*for each floor, whether the lift is requested*)
    6.19 +  up    :: bool		(*current direction of movement*)
    6.20 +  move  :: bool		(*whether moving takes precedence over opening*)
    6.21 +
    6.22 +consts
    6.23 +  min, max :: nat	(*least and greatest floors*)
    6.24 +
    6.25 +rules
    6.26 +  min_le_max  "min <= max"
    6.27 +  
    6.28 +
    6.29 +constdefs
    6.30 +  
    6.31 +  (** Abbreviations: the "always" part **)
    6.32 +  
    6.33 +  above :: "state set"
    6.34 +    "above == {s. EX i. floor s < i & i <= max & i : req s}"
    6.35 +
    6.36 +  below :: "state set"
    6.37 +    "below == {s. EX i. min <= i & i < floor s & i : req s}"
    6.38 +
    6.39 +  queueing :: "state set"
    6.40 +    "queueing == above Un below"
    6.41 +
    6.42 +  goingup :: "state set"
    6.43 +    "goingup == above Int ({s. up s} Un Compl below)"
    6.44 +
    6.45 +  goingdown :: "state set"
    6.46 +    "goingdown == below Int ({s. ~ up s} Un Compl above)"
    6.47 +
    6.48 +  ready :: "state set"
    6.49 +    "ready == {s. stop s & ~ open s & move s}"
    6.50 +
    6.51 +
    6.52 +  (** The program **)
    6.53 +  
    6.54 +  request_act :: "(state*state) set"
    6.55 +    "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
    6.56 +		                  & ~ stop s & floor s : req s}"
    6.57 +
    6.58 +  open_act :: "(state*state) set"
    6.59 +    "open_act ==
    6.60 +         {(s,s'). s' = s (|open :=True,
    6.61 +			   req  := req s - {floor s},
    6.62 +			   move := True|)
    6.63 +		       & stop s & ~ open s & floor s : req s
    6.64 +	               & ~(move s & s: queueing)}"
    6.65 +
    6.66 +  close_act :: "(state*state) set"
    6.67 +    "close_act == {(s,s'). s' = s (|open := False|) & open s}"
    6.68 +
    6.69 +  req_up_act :: "(state*state) set"
    6.70 +    "req_up_act ==
    6.71 +         {(s,s'). s' = s (|stop  :=False,
    6.72 +			   floor := Suc (floor s),
    6.73 +			   up    := True|)
    6.74 +		       & s : (ready Int goingup)}"
    6.75 +
    6.76 +  req_down_act :: "(state*state) set"
    6.77 +    "req_down_act ==
    6.78 +         {(s,s'). s' = s (|stop  :=False,
    6.79 +			   floor := floor s - 1,
    6.80 +			   up    := False|)
    6.81 +		       & s : (ready Int goingdown)}"
    6.82 +
    6.83 +  move_up :: "(state*state) set"
    6.84 +    "move_up ==
    6.85 +         {(s,s'). s' = s (|floor := Suc (floor s)|)
    6.86 +		       & ~ stop s & up s & floor s ~: req s}"
    6.87 +
    6.88 +  move_down :: "(state*state) set"
    6.89 +    "move_down ==
    6.90 +         {(s,s'). s' = s (|floor := floor s - 1|)
    6.91 +		       & ~ stop s & ~ up s & floor s ~: req s}"
    6.92 +
    6.93 +  Lprg :: state program
    6.94 +    "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
    6.95 +		          ~ open s & req s = {}},
    6.96 +	       Acts = {id, request_act, open_act, close_act,
    6.97 +		       req_up_act, req_down_act, move_up, move_down}|)"
    6.98 +
    6.99 +
   6.100 +  (** Invariants **)
   6.101 +
   6.102 +  bounded :: state set
   6.103 +    "bounded == {s. min <= floor s & floor s <= max}"
   6.104 +
   6.105 +  (** ???
   6.106 +		    (~ stop s & up s --> floor s < max) &
   6.107 +		    (~ stop s & ~ up s --> min < floor s)}"
   6.108 +  **)
   6.109 +
   6.110 +  open_stop :: state set
   6.111 +    "open_stop == {s. open s --> stop s}"
   6.112 +  
   6.113 +  open_move :: state set
   6.114 +    "open_move == {s. open s --> move s}"
   6.115 +  
   6.116 +  stop_floor :: state set
   6.117 +    "stop_floor == {s. open s & ~ move s --> floor s : req s}"
   6.118 +  
   6.119 +  moving_up :: state set
   6.120 +    "moving_up == {s. ~ stop s & up s -->
   6.121 +                   (EX f. floor s <= f & f <= max & f : req s)}"
   6.122 +  
   6.123 +  moving_down :: state set
   6.124 +    "moving_down == {s. ~ stop s & ~ up s -->
   6.125 +                     (EX f. min <= f & f <= floor s & f : req s)}"
   6.126 +  
   6.127 +  valid :: "state set"
   6.128 +    "valid == bounded Int open_stop Int open_move"
   6.129 +
   6.130 +end
     7.1 --- a/src/HOL/UNITY/Mutex.ML	Thu Aug 06 14:04:49 1998 +0200
     7.2 +++ b/src/HOL/UNITY/Mutex.ML	Thu Aug 06 15:47:26 1998 +0200
     7.3 @@ -174,7 +174,7 @@
     7.4  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
     7.5  by (stac Un_commute 1);
     7.6  by (rtac LeadsTo_Un_duplicate 1);
     7.7 -by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
     7.8 +by (rtac ([v_leadsto_not_p, U_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
     7.9  by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
    7.10  by (auto_tac (claset() addSEs [less_SucE], simpset()));
    7.11  qed "m1_leadsto_3";
    7.12 @@ -188,7 +188,7 @@
    7.13  by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
    7.14  by (stac Un_commute 1);
    7.15  by (rtac LeadsTo_Un_duplicate 1);
    7.16 -by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
    7.17 +by (rtac ([u_leadsto_p, V_F0] MRS PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
    7.18  by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
    7.19  by (auto_tac (claset() addSEs [less_SucE], simpset()));
    7.20  qed "n1_leadsto_3";
     8.1 --- a/src/HOL/UNITY/SubstAx.ML	Thu Aug 06 14:04:49 1998 +0200
     8.2 +++ b/src/HOL/UNITY/SubstAx.ML	Thu Aug 06 15:47:26 1998 +0200
     8.3 @@ -3,39 +3,54 @@
     8.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1998  University of Cambridge
     8.6  
     8.7 -Weak Fairness versions of transient, ensures, LeadsTo.
     8.8 -
     8.9 -From Misra, "A Logic for Concurrent Programming", 1994
    8.10 +LeadsTo relation, restricted to the set of reachable states.
    8.11  *)
    8.12  
    8.13 -(*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B)
    8.14 -                                           (reachable(Init,Acts) Int B') *)
    8.15 +
    8.16 +(*constrains (Acts prg) B B'
    8.17 +  ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
    8.18  bind_thm ("constrains_reachable",
    8.19  	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
    8.20  
    8.21  
    8.22 +(*** Specialized laws for handling invariants ***)
    8.23 +
    8.24 +Goal "invariant prg INV ==> reachable prg Int INV = reachable prg";
    8.25 +bd invariant_includes_reachable 1;
    8.26 +by (Blast_tac 1);
    8.27 +qed "reachable_Int_INV";
    8.28 +
    8.29 +Goal "[| invariant prg INV;  LeadsTo prg (INV Int A) A' |]   \
    8.30 +\     ==> LeadsTo prg A A'";
    8.31 +by (asm_full_simp_tac
    8.32 +    (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
    8.33 +			 Int_assoc RS sym]) 1);
    8.34 +qed "invariant_LeadsToI";
    8.35 +
    8.36 +Goal "[| invariant prg INV;  LeadsTo prg A A' |]   \
    8.37 +\     ==> LeadsTo prg A (INV Int A')";
    8.38 +by (asm_full_simp_tac
    8.39 +    (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
    8.40 +			 Int_assoc RS sym]) 1);
    8.41 +qed "invariant_LeadsToD";
    8.42 +
    8.43 +
    8.44  (*** Introduction rules: Basis, Trans, Union ***)
    8.45  
    8.46  Goal "leadsTo (Acts prg) A B ==> LeadsTo prg A B";
    8.47  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
    8.48 -by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
    8.49 +by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
    8.50  qed "leadsTo_imp_LeadsTo";
    8.51  
    8.52 -Goal "ensures (Acts prg) (reachable prg Int A) (reachable prg Int A') \
    8.53 -\     ==> LeadsTo prg A A'";
    8.54 -by (full_simp_tac (simpset() addsimps [ensures_def, LeadsTo_def]) 1);
    8.55 -by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
    8.56 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib])));
    8.57 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
    8.58 -qed "LeadsTo_Basis";
    8.59 +(* ensures (Acts prg) A B ==> LeadsTo prg A B *)
    8.60 +bind_thm ("LeadsTo_Basis", leadsTo_Basis RS leadsTo_imp_LeadsTo);
    8.61  
    8.62 -Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] \
    8.63 -\      ==> LeadsTo prg A C";
    8.64 +Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] ==> LeadsTo prg A C";
    8.65  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
    8.66  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
    8.67  qed "LeadsTo_Trans";
    8.68  
    8.69 -val [prem] = goalw thy [LeadsTo_def]
    8.70 +val [prem] = Goalw [LeadsTo_def]
    8.71   "(!!A. A : S ==> LeadsTo prg A B) ==> LeadsTo prg (Union S) B";
    8.72  by (Simp_tac 1);
    8.73  by (stac Int_Union 1);
    8.74 @@ -46,7 +61,7 @@
    8.75  
    8.76  (*** Derived rules ***)
    8.77  
    8.78 -Goal "id: (Acts prg) ==> LeadsTo prg A UNIV";
    8.79 +Goal "id: Acts prg ==> LeadsTo prg A UNIV";
    8.80  by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
    8.81  				      Int_lower1 RS subset_imp_leadsTo]) 1);
    8.82  qed "LeadsTo_UNIV";
    8.83 @@ -61,9 +76,8 @@
    8.84  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
    8.85  qed "LeadsTo_Un_duplicate2";
    8.86  
    8.87 -val prems = goal thy
    8.88 -   "(!!i. i : I ==> LeadsTo prg (A i) B) \
    8.89 -\   ==> LeadsTo prg (UN i:I. A i) B";
    8.90 +val prems = 
    8.91 +Goal "(!!i. i : I ==> LeadsTo prg (A i) B) ==> LeadsTo prg (UN i:I. A i) B";
    8.92  by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
    8.93  by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
    8.94  qed "LeadsTo_UN";
    8.95 @@ -74,14 +88,7 @@
    8.96  by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
    8.97  qed "LeadsTo_Un";
    8.98  
    8.99 -
   8.100 -Goal "[| reachable prg Int A <= B;  id: (Acts prg) |] \
   8.101 -\     ==> LeadsTo prg A B";
   8.102 -by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.103 -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   8.104 -qed "Int_subset_imp_LeadsTo";
   8.105 -
   8.106 -Goal "[| A <= B;  id: (Acts prg) |] ==> LeadsTo prg A B";
   8.107 +Goal "[| A <= B;  id: Acts prg |] ==> LeadsTo prg A B";
   8.108  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.109  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   8.110  qed "subset_imp_LeadsTo";
   8.111 @@ -89,22 +96,13 @@
   8.112  bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
   8.113  Addsimps [empty_LeadsTo];
   8.114  
   8.115 -Goal "[| reachable prg Int A = {};  id: (Acts prg) |] \
   8.116 -\     ==> LeadsTo prg A B";
   8.117 -by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
   8.118 -qed "Int_empty_LeadsTo";
   8.119 -
   8.120 -
   8.121 -Goal "[| LeadsTo prg A A';   \
   8.122 -\        reachable prg Int A' <= B' |] \
   8.123 -\     ==> LeadsTo prg A B'";
   8.124 +Goal "[| LeadsTo prg A A';  A' <= B' |] ==> LeadsTo prg A B'";
   8.125  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.126  by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
   8.127  qed_spec_mp "LeadsTo_weaken_R";
   8.128  
   8.129  
   8.130 -Goal "[| LeadsTo prg A A'; \
   8.131 -\        reachable prg Int B <= A; id: (Acts prg) |]  \
   8.132 +Goal "[| LeadsTo prg A A';  B <= A; id: Acts prg |]  \
   8.133  \     ==> LeadsTo prg B A'";
   8.134  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.135  by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
   8.136 @@ -112,49 +110,74 @@
   8.137  
   8.138  
   8.139  (*Distributes over binary unions*)
   8.140 -Goal "id: (Acts prg) ==> \
   8.141 +Goal "id: Acts prg ==> \
   8.142  \       LeadsTo prg (A Un B) C  =  \
   8.143  \       (LeadsTo prg A C & LeadsTo prg B C)";
   8.144  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
   8.145  qed "LeadsTo_Un_distrib";
   8.146  
   8.147 -Goal "id: (Acts prg) ==> \
   8.148 +Goal "id: Acts prg ==> \
   8.149  \       LeadsTo prg (UN i:I. A i) B  =  \
   8.150  \       (ALL i : I. LeadsTo prg (A i) B)";
   8.151  by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
   8.152  qed "LeadsTo_UN_distrib";
   8.153  
   8.154 -Goal "id: (Acts prg) ==> \
   8.155 +Goal "id: Acts prg ==> \
   8.156  \       LeadsTo prg (Union S) B  =  \
   8.157  \       (ALL A : S. LeadsTo prg A B)";
   8.158  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
   8.159  qed "LeadsTo_Union_distrib";
   8.160  
   8.161  
   8.162 -Goal "[| LeadsTo prg A A'; id: (Acts prg);   \
   8.163 -\        reachable prg Int B  <= A;     \
   8.164 -\        reachable prg Int A' <= B' |] \
   8.165 +Goal "[| LeadsTo prg A A'; id: Acts prg;   \
   8.166 +\        B  <= A;   A' <= B' |] \
   8.167  \     ==> LeadsTo prg B B'";
   8.168 -(*PROOF FAILED: why?*)
   8.169 +(*PROOF FAILED*)
   8.170  by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
   8.171  			       LeadsTo_weaken_L]) 1);
   8.172  qed "LeadsTo_weaken";
   8.173  
   8.174  
   8.175 +(** More rules using the premise "invariant prg" **)
   8.176 +
   8.177 +Goal "[| invariant prg INV;      \
   8.178 +\        constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
   8.179 +\        transient  (Acts prg) (INV Int (A-A')) |]   \
   8.180 +\ ==> LeadsTo prg A A'";
   8.181 +br invariant_LeadsToI 1;
   8.182 +ba 1;
   8.183 +by (rtac (ensuresI RS LeadsTo_Basis) 1);
   8.184 +by (ALLGOALS 
   8.185 +    (full_simp_tac (simpset() addsimps [Int_Diff, Int_Un_distrib RS sym, 
   8.186 +					Diff_Int_distrib RS sym])));
   8.187 +be invariantE 1;
   8.188 +by (blast_tac (claset() addSDs [stable_constrains_Int]
   8.189 +			addIs [constrains_weaken]) 1);
   8.190 +qed "invariant_LeadsTo_Basis";
   8.191 +
   8.192 +Goal "[| invariant prg INV;      \
   8.193 +\        LeadsTo prg A A'; id: Acts prg;   \
   8.194 +\        INV Int B  <= A;  INV Int A' <= B' |] \
   8.195 +\     ==> LeadsTo prg B B'";
   8.196 +br invariant_LeadsToI 1;
   8.197 +ba 1;
   8.198 +bd invariant_LeadsToD 1;
   8.199 +ba 1;
   8.200 +by (blast_tac (claset()addIs [LeadsTo_weaken]) 1);
   8.201 +qed "invariant_LeadsTo_weaken";
   8.202 +
   8.203 +
   8.204  (*Set difference: maybe combine with leadsTo_weaken_L??
   8.205    This is the most useful form of the "disjunction" rule*)
   8.206 -Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: (Acts prg) |] \
   8.207 +Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: Acts prg |] \
   8.208  \     ==> LeadsTo prg A C";
   8.209  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
   8.210  qed "LeadsTo_Diff";
   8.211  
   8.212  
   8.213 -(** Meta or object quantifier ???????????????????
   8.214 -    see ball_constrains_UN in UNITY.ML***)
   8.215 -
   8.216 -val prems = goal thy
   8.217 -   "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
   8.218 -\   ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
   8.219 +val prems = 
   8.220 +Goal "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
   8.221 +\     ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
   8.222  by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
   8.223  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
   8.224                          addIs prems) 1);
   8.225 @@ -187,26 +210,26 @@
   8.226  (** The cancellation law **)
   8.227  
   8.228  Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B'; \
   8.229 -\        id: (Acts prg) |]    \
   8.230 +\        id: Acts prg |]    \
   8.231  \     ==> LeadsTo prg A (A' Un B')";
   8.232  by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
   8.233  			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
   8.234  qed "LeadsTo_cancel2";
   8.235  
   8.236 -Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: (Acts prg) |] \
   8.237 +Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: Acts prg |] \
   8.238  \     ==> LeadsTo prg A (A' Un B')";
   8.239  by (rtac LeadsTo_cancel2 1);
   8.240  by (assume_tac 2);
   8.241  by (ALLGOALS Asm_simp_tac);
   8.242  qed "LeadsTo_cancel_Diff2";
   8.243  
   8.244 -Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: (Acts prg) |] \
   8.245 +Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: Acts prg |] \
   8.246  \     ==> LeadsTo prg A (B' Un A')";
   8.247  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
   8.248  by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
   8.249  qed "LeadsTo_cancel1";
   8.250  
   8.251 -Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: (Acts prg) |] \
   8.252 +Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: Acts prg |] \
   8.253  \     ==> LeadsTo prg A (B' Un A')";
   8.254  by (rtac LeadsTo_cancel1 1);
   8.255  by (assume_tac 2);
   8.256 @@ -217,7 +240,8 @@
   8.257  
   8.258  (** The impossibility law **)
   8.259  
   8.260 -Goal "LeadsTo prg A {} ==> reachable prg Int A  = {}";
   8.261 +(*The set "A" may be non-empty, but it contains no reachable states*)
   8.262 +Goal "LeadsTo prg A {} ==> reachable prg Int A = {}";
   8.263  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.264  by (etac leadsTo_empty 1);
   8.265  qed "LeadsTo_empty";
   8.266 @@ -229,40 +253,40 @@
   8.267  Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
   8.268  \     ==> LeadsTo prg (A Int B) (A' Int B)";
   8.269  by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, 
   8.270 -					   PSP_stable]) 1);
   8.271 -qed "R_PSP_stable";
   8.272 +					   psp_stable]) 1);
   8.273 +qed "PSP_stable";
   8.274  
   8.275  Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
   8.276 -\       ==> LeadsTo prg (B Int A) (B Int A')";
   8.277 -by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
   8.278 -qed "R_PSP_stable2";
   8.279 +\     ==> LeadsTo prg (B Int A) (B Int A')";
   8.280 +by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
   8.281 +qed "PSP_stable2";
   8.282  
   8.283  
   8.284 -Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: (Acts prg) |] \
   8.285 +Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
   8.286  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
   8.287  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.288 -by (dtac PSP 1);
   8.289 +by (dtac psp 1);
   8.290  by (etac constrains_reachable 1);
   8.291  by (etac leadsTo_weaken 2);
   8.292  by (ALLGOALS Blast_tac);
   8.293 -qed "R_PSP";
   8.294 +qed "PSP";
   8.295  
   8.296 -Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: (Acts prg) |] \
   8.297 +Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
   8.298  \     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
   8.299 -by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
   8.300 -qed "R_PSP2";
   8.301 +by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
   8.302 +qed "PSP2";
   8.303  
   8.304  Goalw [unless_def]
   8.305 -   "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: (Acts prg) |] \
   8.306 +   "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: Acts prg |] \
   8.307  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
   8.308 -by (dtac R_PSP 1);
   8.309 +by (dtac PSP 1);
   8.310  by (assume_tac 1);
   8.311  by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
   8.312  by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
   8.313  by (etac LeadsTo_Diff 2);
   8.314  by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
   8.315  by Auto_tac;
   8.316 -qed "R_PSP_unless";
   8.317 +qed "PSP_unless";
   8.318  
   8.319  
   8.320  (*** Induction rules ***)
   8.321 @@ -271,7 +295,7 @@
   8.322  Goal "[| wf r;     \
   8.323  \        ALL m. LeadsTo prg (A Int f-``{m})                     \
   8.324  \                                 ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   8.325 -\        id: (Acts prg) |] \
   8.326 +\        id: Acts prg |] \
   8.327  \     ==> LeadsTo prg A B";
   8.328  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.329  by (etac leadsTo_wf_induct 1);
   8.330 @@ -283,38 +307,38 @@
   8.331  Goal "[| wf r;     \
   8.332  \        ALL m:I. LeadsTo prg (A Int f-``{m})                   \
   8.333  \                             ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   8.334 -\        id: (Acts prg) |] \
   8.335 +\        id: Acts prg |] \
   8.336  \     ==> LeadsTo prg A ((A - (f-``I)) Un B)";
   8.337  by (etac LeadsTo_wf_induct 1);
   8.338  by Safe_tac;
   8.339  by (case_tac "m:I" 1);
   8.340  by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
   8.341  by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
   8.342 -qed "R_bounded_induct";
   8.343 +qed "Bounded_induct";
   8.344  
   8.345  
   8.346  Goal "[| ALL m. LeadsTo prg (A Int f-``{m})                     \
   8.347  \                           ((A Int f-``(lessThan m)) Un B);   \
   8.348 -\        id: (Acts prg) |] \
   8.349 +\        id: Acts prg |] \
   8.350  \     ==> LeadsTo prg A B";
   8.351  by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
   8.352  by (assume_tac 2);
   8.353  by (Asm_simp_tac 1);
   8.354 -qed "R_lessThan_induct";
   8.355 +qed "LessThan_induct";
   8.356  
   8.357  Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m})   \
   8.358  \                                        ((A Int f-``(lessThan m)) Un B);   \
   8.359 -\              id: (Acts prg) |] \
   8.360 +\              id: Acts prg |] \
   8.361  \           ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)";
   8.362  by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
   8.363 -by (rtac (wf_less_than RS R_bounded_induct) 1);
   8.364 +by (rtac (wf_less_than RS Bounded_induct) 1);
   8.365  by (assume_tac 2);
   8.366  by (Asm_simp_tac 1);
   8.367 -qed "R_lessThan_bounded_induct";
   8.368 +qed "LessThan_bounded_induct";
   8.369  
   8.370  Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m})   \
   8.371  \                              ((A Int f-``(greaterThan m)) Un B);   \
   8.372 -\        id: (Acts prg) |] \
   8.373 +\        id: Acts prg |] \
   8.374  \     ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)";
   8.375  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
   8.376      (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
   8.377 @@ -324,36 +348,35 @@
   8.378  by (case_tac "m<l" 1);
   8.379  by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2);
   8.380  by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1);
   8.381 -qed "R_greaterThan_bounded_induct";
   8.382 -
   8.383 +qed "GreaterThan_bounded_induct";
   8.384  
   8.385  
   8.386  (*** Completion: Binary and General Finite versions ***)
   8.387  
   8.388  Goal "[| LeadsTo prg A A';  stable (Acts prg) A';   \
   8.389 -\        LeadsTo prg B B';  stable (Acts prg) B';  id: (Acts prg) |] \
   8.390 +\        LeadsTo prg B B';  stable (Acts prg) B';  id: Acts prg |] \
   8.391  \     ==> LeadsTo prg (A Int B) (A' Int B')";
   8.392  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   8.393  by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
   8.394                          addSIs [stable_Int, stable_reachable]) 1);
   8.395 -qed "R_stable_completion";
   8.396 +qed "Stable_completion";
   8.397  
   8.398  
   8.399 -Goal "[| finite I;  id: (Acts prg) |]                     \
   8.400 +Goal "[| finite I;  id: Acts prg |]                     \
   8.401  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i)) -->  \
   8.402  \         (ALL i:I. stable (Acts prg) (A' i)) -->         \
   8.403  \         LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
   8.404  by (etac finite_induct 1);
   8.405  by (Asm_simp_tac 1);
   8.406  by (asm_simp_tac 
   8.407 -    (simpset() addsimps [R_stable_completion, stable_def, 
   8.408 +    (simpset() addsimps [Stable_completion, stable_def, 
   8.409  			 ball_constrains_INT]) 1);
   8.410 -qed_spec_mp "R_finite_stable_completion";
   8.411 +qed_spec_mp "Finite_stable_completion";
   8.412  
   8.413  
   8.414  Goal "[| LeadsTo prg A (A' Un C);  constrains (Acts prg) A' (A' Un C); \
   8.415  \        LeadsTo prg B (B' Un C);  constrains (Acts prg) B' (B' Un C); \
   8.416 -\        id: (Acts prg) |] \
   8.417 +\        id: Acts prg |] \
   8.418  \     ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
   8.419  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
   8.420  by (dtac completion 1);
   8.421 @@ -362,10 +385,10 @@
   8.422      (asm_simp_tac 
   8.423       (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
   8.424  by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   8.425 -qed "R_completion";
   8.426 +qed "Completion";
   8.427  
   8.428  
   8.429 -Goal "[| finite I;  id: (Acts prg) |] \
   8.430 +Goal "[| finite I;  id: Acts prg |] \
   8.431  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) -->  \
   8.432  \         (ALL i:I. constrains (Acts prg) (A' i) (A' i Un C)) --> \
   8.433  \         LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
   8.434 @@ -373,48 +396,8 @@
   8.435  by (ALLGOALS Asm_simp_tac);
   8.436  by (Clarify_tac 1);
   8.437  by (dtac ball_constrains_INT 1);
   8.438 -by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); 
   8.439 -qed "R_finite_completion";
   8.440 -
   8.441 -
   8.442 -
   8.443 -(*** Specialized laws for handling invariants ***)
   8.444 -
   8.445 -Goalw [transient_def]
   8.446 -    "[| reachable prg <= INV;  transient (Acts prg) (INV Int A) |]  \
   8.447 -\    ==> transient (Acts prg) (reachable prg Int A)";
   8.448 -by (Clarify_tac 1);
   8.449 -by (rtac bexI 1); 
   8.450 -by (assume_tac 2);
   8.451 -by (Blast_tac 1);
   8.452 -qed "reachable_transient";
   8.453 -
   8.454 -(*Uses the premise "invariant prg".  Raw theorem-proving on this
   8.455 -  inclusion is slow: the term contains a copy of the program.*)
   8.456 -Goal "[| invariant prg INV;      \
   8.457 -\        constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
   8.458 -\        transient  (Acts prg) (INV Int (A-A')) |]   \
   8.459 -\ ==> ensures (Acts prg) (reachable prg Int A) (reachable prg Int A')";
   8.460 -bd invariant_includes_reachable 1;
   8.461 -by (rtac ensuresI 1);
   8.462 -by (ALLGOALS 
   8.463 -    (full_simp_tac (simpset() addsimps [Int_Un_distrib RS sym, 
   8.464 -					Diff_Int_distrib RS sym])));
   8.465 -by (blast_tac (claset() addSIs [reachable_transient]) 2);
   8.466 -br (stable_reachable RS stable_constrains_Int) 1;
   8.467 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
   8.468 -qed "invariant_ensuresI";
   8.469 -
   8.470 -bind_thm ("invariant_LeadsTo_Basis", invariant_ensuresI RS LeadsTo_Basis);
   8.471 -
   8.472 -
   8.473 -Goal "[| invariant prg INV;      \
   8.474 -\        LeadsTo prg A A'; id: (Acts prg);   \
   8.475 -\        INV Int B  <= A;  INV Int A' <= B' |] \
   8.476 -\     ==> LeadsTo prg B B'";
   8.477 -by (blast_tac (claset() addDs [invariant_includes_reachable]
   8.478 -			addIs [LeadsTo_weaken]) 1);
   8.479 -qed "invariant_LeadsTo_weaken";
   8.480 +by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); 
   8.481 +qed "Finite_completion";
   8.482  
   8.483  
   8.484  (** Constrains/Ensures tactics 
     9.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 06 14:04:49 1998 +0200
     9.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 06 15:47:26 1998 +0200
     9.3 @@ -3,10 +3,10 @@
     9.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.5      Copyright   1998  University of Cambridge
     9.6  
     9.7 -My treatment of the Substitution Axiom -- not as an axiom!
     9.8 +LeadsTo relation: restricted to the set of reachable states.
     9.9  *)
    9.10  
    9.11 -SubstAx = WFair +
    9.12 +SubstAx = WFair + Traces + 
    9.13  
    9.14  constdefs
    9.15  
    10.1 --- a/src/HOL/UNITY/Token.ML	Thu Aug 06 14:04:49 1998 +0200
    10.2 +++ b/src/HOL/UNITY/Token.ML	Thu Aug 06 15:47:26 1998 +0200
    10.3 @@ -119,6 +119,6 @@
    10.4  by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
    10.5  by (rtac TR6 2);
    10.6  by (rtac leadsTo_weaken_R 1);
    10.7 -by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
    10.8 +by (rtac ([leadsTo_j, TR3] MRS psp) 1);
    10.9  by (ALLGOALS Blast_tac);
   10.10  qed "token_progress";
    11.1 --- a/src/HOL/UNITY/Token.thy	Thu Aug 06 14:04:49 1998 +0200
    11.2 +++ b/src/HOL/UNITY/Token.thy	Thu Aug 06 15:47:26 1998 +0200
    11.3 @@ -9,7 +9,7 @@
    11.4  *)
    11.5  
    11.6  
    11.7 -Token = WFair +
    11.8 +Token = WFair + 
    11.9  
   11.10  (*process states*)
   11.11  datatype pstate = Hungry | Eating | Thinking
    12.1 --- a/src/HOL/UNITY/Traces.ML	Thu Aug 06 14:04:49 1998 +0200
    12.2 +++ b/src/HOL/UNITY/Traces.ML	Thu Aug 06 15:47:26 1998 +0200
    12.3 @@ -35,12 +35,19 @@
    12.4  by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
    12.5  qed "invariant_includes_reachable";
    12.6  
    12.7 -(*If "A" includes the initial states and is stable then "A" is invariant.
    12.8 -  Result is trivial from the definition, but it is handy.*)
    12.9 +
   12.10 +(** Natural deduction rules for "invariant prg A" **)
   12.11 +
   12.12  Goal "[| (Init prg)<=A;  stable (Acts prg) A |] ==> invariant prg A";
   12.13  by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
   12.14  qed "invariantI";
   12.15  
   12.16 +Goal "invariant prg A ==> (Init prg)<=A & stable (Acts prg) A";
   12.17 +by (asm_full_simp_tac (simpset() addsimps [invariant_def]) 1);
   12.18 +qed "invariantD";
   12.19 +
   12.20 +bind_thm ("invariantE", invariantD RS conjE);
   12.21 +
   12.22  
   12.23  (** Conjoining invariants **)
   12.24  
    13.1 --- a/src/HOL/UNITY/UNITY.ML	Thu Aug 06 14:04:49 1998 +0200
    13.2 +++ b/src/HOL/UNITY/UNITY.ML	Thu Aug 06 15:47:26 1998 +0200
    13.3 @@ -14,7 +14,7 @@
    13.4  
    13.5  (*** constrains ***)
    13.6  
    13.7 -val prems = goalw thy [constrains_def]
    13.8 +val prems = Goalw [constrains_def]
    13.9      "(!!act s s'. [| act: acts;  (s,s') : act;  s: A |] ==> s': A') \
   13.10  \    ==> constrains acts A A'";
   13.11  by (blast_tac (claset() addIs prems) 1);
   13.12 @@ -50,18 +50,11 @@
   13.13  by (Blast_tac 1);
   13.14  qed "constrains_weaken";
   13.15  
   13.16 -(*Set difference: UNUSED*)
   13.17 -Goalw [constrains_def]
   13.18 -  "[| constrains acts (A-B) C; constrains acts B C |] \
   13.19 -\       ==> constrains acts A C";
   13.20 -by (Blast_tac 1);
   13.21 -qed "constrains_Diff";
   13.22 -
   13.23  (** Union **)
   13.24  
   13.25  Goalw [constrains_def]
   13.26      "[| constrains acts A A'; constrains acts B B' |]   \
   13.27 -\           ==> constrains acts (A Un B) (A' Un B')";
   13.28 +\    ==> constrains acts (A Un B) (A' Un B')";
   13.29  by (Blast_tac 1);
   13.30  qed "constrains_Un";
   13.31  
   13.32 @@ -73,7 +66,7 @@
   13.33  
   13.34  Goalw [constrains_def]
   13.35      "[| ALL i. constrains acts (A i) (A' i) |] \
   13.36 -\           ==> constrains acts (UN i. A i) (UN i. A' i)";
   13.37 +\    ==> constrains acts (UN i. A i) (UN i. A' i)";
   13.38  by (Blast_tac 1);
   13.39  qed "all_constrains_UN";
   13.40  
   13.41 @@ -81,7 +74,7 @@
   13.42  
   13.43  Goalw [constrains_def]
   13.44      "[| constrains acts A A'; constrains acts B B' |]   \
   13.45 -\           ==> constrains acts (A Int B) (A' Int B')";
   13.46 +\    ==> constrains acts (A Int B) (A' Int B')";
   13.47  by (Blast_tac 1);
   13.48  qed "constrains_Int";
   13.49  
   13.50 @@ -93,21 +86,20 @@
   13.51  
   13.52  Goalw [constrains_def]
   13.53      "[| ALL i. constrains acts (A i) (A' i) |] \
   13.54 -\           ==> constrains acts (INT i. A i) (INT i. A' i)";
   13.55 +\    ==> constrains acts (INT i. A i) (INT i. A' i)";
   13.56  by (Blast_tac 1);
   13.57  qed "all_constrains_INT";
   13.58  
   13.59 -Goalw [stable_def, constrains_def]
   13.60 -    "[| stable acts C; constrains acts A (C Un A') |]   \
   13.61 -\           ==> constrains acts (C Un A) (C Un A')";
   13.62 +Goalw [constrains_def]
   13.63 +    "[| constrains acts A A'; id: acts |] ==> A<=A'";
   13.64  by (Blast_tac 1);
   13.65 -qed "stable_constrains_Un";
   13.66 +qed "constrains_imp_subset";
   13.67  
   13.68 -Goalw [stable_def, constrains_def]
   13.69 -    "[| stable acts C; constrains acts (C Int A) A' |]   \
   13.70 -\           ==> constrains acts (C Int A) (C Int A')";
   13.71 +Goalw [constrains_def]
   13.72 +    "[| id: acts; constrains acts A B; constrains acts B C |]   \
   13.73 +\    ==> constrains acts A C";
   13.74  by (Blast_tac 1);
   13.75 -qed "stable_constrains_Int";
   13.76 +qed "constrains_trans";
   13.77  
   13.78  
   13.79  (*** stable ***)
   13.80 @@ -124,27 +116,27 @@
   13.81  
   13.82  Goalw [stable_def]
   13.83      "[| stable acts A; stable acts A' |]   \
   13.84 -\           ==> stable acts (A Un A')";
   13.85 +\    ==> stable acts (A Un A')";
   13.86  by (blast_tac (claset() addIs [constrains_Un]) 1);
   13.87  qed "stable_Un";
   13.88  
   13.89  Goalw [stable_def]
   13.90      "[| stable acts A; stable acts A' |]   \
   13.91 -\           ==> stable acts (A Int A')";
   13.92 +\    ==> stable acts (A Int A')";
   13.93  by (blast_tac (claset() addIs [constrains_Int]) 1);
   13.94  qed "stable_Int";
   13.95  
   13.96 -Goalw [constrains_def]
   13.97 -    "[| constrains acts A A'; id: acts |] ==> A<=A'";
   13.98 +Goalw [stable_def, constrains_def]
   13.99 +    "[| stable acts C; constrains acts A (C Un A') |]   \
  13.100 +\    ==> constrains acts (C Un A) (C Un A')";
  13.101  by (Blast_tac 1);
  13.102 -qed "constrains_imp_subset";
  13.103 -
  13.104 +qed "stable_constrains_Un";
  13.105  
  13.106 -Goalw [constrains_def]
  13.107 -    "[| id: acts; constrains acts A B; constrains acts B C |]   \
  13.108 -\           ==> constrains acts A C";
  13.109 +Goalw [stable_def, constrains_def]
  13.110 +    "[| stable acts C; constrains acts (C Int A) A' |]   \
  13.111 +\    ==> constrains acts (C Int A) (C Int A')";
  13.112  by (Blast_tac 1);
  13.113 -qed "constrains_trans";
  13.114 +qed "stable_constrains_Int";
  13.115  
  13.116  
  13.117  (*The Elimination Theorem.  The "free" m has become universally quantified!
  13.118 @@ -152,7 +144,7 @@
  13.119    in forward proof.*)
  13.120  Goalw [constrains_def]
  13.121      "[| ALL m. constrains acts {s. s x = m} (B m) |] \
  13.122 -\           ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
  13.123 +\    ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
  13.124  by (Blast_tac 1);
  13.125  qed "elimination";
  13.126  
  13.127 @@ -160,14 +152,14 @@
  13.128    state is identified with its one variable.*)
  13.129  Goalw [constrains_def]
  13.130      "[| ALL m. constrains acts {m} (B m) |] \
  13.131 -\           ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)";
  13.132 +\    ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)";
  13.133  by (Blast_tac 1);
  13.134  qed "elimination_sing";
  13.135  
  13.136  
  13.137  Goalw [constrains_def]
  13.138     "[| constrains acts A (A' Un B); constrains acts B B'; id: acts |] \
  13.139 -\           ==> constrains acts A (A' Un B')";
  13.140 +\   ==> constrains acts A (A' Un B')";
  13.141  by (Blast_tac 1);
  13.142  qed "constrains_cancel";
  13.143  
    14.1 --- a/src/HOL/UNITY/WFair.ML	Thu Aug 06 14:04:49 1998 +0200
    14.2 +++ b/src/HOL/UNITY/WFair.ML	Thu Aug 06 15:47:26 1998 +0200
    14.3 @@ -272,23 +272,18 @@
    14.4      (simpset() addsimps [ensures_def, 
    14.5  			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
    14.6  by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
    14.7 -qed "PSP_stable";
    14.8 +qed "psp_stable";
    14.9  
   14.10  Goal "[| leadsTo acts A A'; stable acts B |] \
   14.11  \   ==> leadsTo acts (B Int A) (B Int A')";
   14.12 -by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
   14.13 -qed "PSP_stable2";
   14.14 +by (asm_simp_tac (simpset() addsimps (psp_stable::Int_ac)) 1);
   14.15 +qed "psp_stable2";
   14.16  
   14.17 -
   14.18 -Goalw [ensures_def]
   14.19 +Goalw [ensures_def, constrains_def]
   14.20     "[| ensures acts A A'; constrains acts B B' |] \
   14.21  \   ==> ensures acts (A Int B) ((A' Int B) Un (B' - B))";
   14.22 -by Safe_tac;
   14.23 -by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);
   14.24 -by (etac transient_strengthen 1);
   14.25 -by (Blast_tac 1);
   14.26 -qed "PSP_ensures";
   14.27 -
   14.28 +by (blast_tac (claset() addIs [transient_strengthen]) 1);
   14.29 +qed "psp_ensures";
   14.30  
   14.31  Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
   14.32  \           ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))";
   14.33 @@ -301,26 +296,26 @@
   14.34  by (assume_tac 3);
   14.35  by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
   14.36  (*Basis case*)
   14.37 -by (blast_tac (claset() addIs [leadsTo_Basis, PSP_ensures]) 1);
   14.38 -qed "PSP";
   14.39 +by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
   14.40 +qed "psp";
   14.41  
   14.42  Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
   14.43  \   ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
   14.44 -by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
   14.45 -qed "PSP2";
   14.46 +by (asm_simp_tac (simpset() addsimps (psp::Int_ac)) 1);
   14.47 +qed "psp2";
   14.48  
   14.49  
   14.50  Goalw [unless_def]
   14.51     "[| leadsTo acts A A'; unless acts B B'; id: acts |] \
   14.52  \   ==> leadsTo acts (A Int B) ((A' Int B) Un B')";
   14.53 -by (dtac PSP 1);
   14.54 +by (dtac psp 1);
   14.55  by (assume_tac 1);
   14.56  by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
   14.57  by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
   14.58  by (etac leadsTo_Diff 2);
   14.59  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2);
   14.60  by Auto_tac;
   14.61 -qed "PSP_unless";
   14.62 +qed "psp_unless";
   14.63  
   14.64  
   14.65  (*** Proving the induction rules ***)
   14.66 @@ -482,9 +477,9 @@
   14.67  	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
   14.68  	   Blast_tac 2]);
   14.69  by (subgoal_tac "leadsTo acts (A Int wlt acts B') (A' Int wlt acts B')" 1);
   14.70 -by (blast_tac (claset() addIs [PSP_stable]) 2);
   14.71 +by (blast_tac (claset() addIs [psp_stable]) 2);
   14.72  by (subgoal_tac "leadsTo acts (A' Int wlt acts B') (A' Int B')" 1);
   14.73 -by (blast_tac (claset() addIs [wlt_leadsTo, PSP_stable2]) 2);
   14.74 +by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
   14.75  by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
   14.76  by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
   14.77  			       subset_imp_leadsTo]) 2);
   14.78 @@ -518,10 +513,10 @@
   14.79      (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
   14.80  by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1);
   14.81  by (simp_tac (simpset() addsimps [Int_Diff]) 2);
   14.82 -by (blast_tac (claset() addIs [wlt_leadsTo, PSP RS leadsTo_weaken_R]) 2);
   14.83 +by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2);
   14.84  by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1);
   14.85  by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
   14.86 -                               PSP2 RS leadsTo_weaken_R, 
   14.87 +                               psp2 RS leadsTo_weaken_R, 
   14.88  			       subset_refl RS subset_imp_leadsTo, 
   14.89  			       leadsTo_Un_duplicate2]) 2);
   14.90  by (dtac leadsTo_Diff 1);
    15.1 --- a/src/HOL/UNITY/WFair.thy	Thu Aug 06 14:04:49 1998 +0200
    15.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Aug 06 15:47:26 1998 +0200
    15.3 @@ -8,7 +8,7 @@
    15.4  From Misra, "A Logic for Concurrent Programming", 1994
    15.5  *)
    15.6  
    15.7 -WFair = Traces + Vimage +
    15.8 +WFair = UNITY +
    15.9  
   15.10  constdefs
   15.11