specifications as sets of programs
authorpaulson
Thu Oct 15 11:35:07 1998 +0200 (1998-10-15)
changeset 5648fe887910e32e
parent 5647 4e8837255b87
child 5649 1bac26652f45
specifications as sets of programs
src/HOL/UNITY/Channel.ML
src/HOL/UNITY/Channel.thy
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Client.thy
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Common.thy
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/Deadlock.ML
src/HOL/UNITY/FP.ML
src/HOL/UNITY/FP.thy
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Handshake.thy
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/Mutex.ML
src/HOL/UNITY/NSP_Bad.ML
src/HOL/UNITY/Network.ML
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Reach.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/Traces.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.ML
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/UNITY/Channel.ML	Wed Oct 14 15:47:22 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Channel.ML	Thu Oct 15 11:35:07 1998 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
     1.5  *)
     1.6  
     1.7 -AddIffs [skip];
     1.8 -
     1.9  (*None represents "infinity" while Some represents proper integers*)
    1.10  Goalw [minSet_def] "minSet A = Some x --> x : A";
    1.11  by (Simp_tac 1);
    1.12 @@ -26,7 +24,7 @@
    1.13  by (Blast_tac 1);
    1.14  qed_spec_mp "minSet_nonempty";
    1.15  
    1.16 -Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
    1.17 +Goal "F : leadsTo (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
    1.18  by (rtac leadsTo_weaken 1);
    1.19  by (rtac ([UC2, UC1] MRS psp) 1);
    1.20  by (ALLGOALS Asm_simp_tac);
    1.21 @@ -38,7 +36,7 @@
    1.22  
    1.23  
    1.24  (*The induction*)
    1.25 -Goal "leadsTo acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
    1.26 +Goal "F : leadsTo (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
    1.27  by (rtac leadsTo_weaken_R 1);
    1.28  by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
    1.29       greaterThan_bounded_induct 1);
    1.30 @@ -54,7 +52,7 @@
    1.31  val lemma = result();
    1.32  
    1.33  
    1.34 -Goal "!!y::nat. leadsTo acts (UNIV-{{}}) {s. y ~: s}";
    1.35 +Goal "!!y::nat. F : leadsTo (UNIV-{{}}) {s. y ~: s}";
    1.36  by (rtac (lemma RS leadsTo_weaken_R) 1);
    1.37  by (Clarify_tac 1);
    1.38  by (forward_tac [minSet_nonempty] 1);
     2.1 --- a/src/HOL/UNITY/Channel.thy	Wed Oct 14 15:47:22 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Channel.thy	Thu Oct 15 11:35:07 1998 +0200
     2.3 @@ -12,18 +12,19 @@
     2.4  
     2.5  types state = nat set
     2.6  
     2.7 +consts
     2.8 +  F :: state program
     2.9 +
    2.10  constdefs
    2.11    minSet :: nat set => nat option
    2.12      "minSet A == if A={} then None else Some (LEAST x. x:A)"
    2.13  
    2.14  rules
    2.15  
    2.16 -  skip "Id: acts"
    2.17 -
    2.18 -  UC1  "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
    2.19 +  UC1  "F : constrains (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
    2.20  
    2.21 -  (*  UC1  "constrains acts {s. minSet s = x} {s. x <= minSet s}"  *)
    2.22 +  (*  UC1  "F : constrains {s. minSet s = x} {s. x <= minSet s}"  *)
    2.23  
    2.24 -  UC2  "leadsTo acts (minSet -`` {Some x}) {s. x ~: s}"
    2.25 +  UC2  "F : leadsTo (minSet -`` {Some x}) {s. x ~: s}"
    2.26  
    2.27  end
     3.1 --- a/src/HOL/UNITY/Client.ML	Wed Oct 14 15:47:22 1998 +0200
     3.2 +++ b/src/HOL/UNITY/Client.ML	Thu Oct 15 11:35:07 1998 +0200
     3.3 @@ -7,74 +7,9 @@
     3.4  *)
     3.5  
     3.6  
     3.7 - (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
     3.8 -
     3.9 -(*[| stable acts C; constrains acts (C Int A) A |] ==> stable acts (C Int A)*)
    3.10 -bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
    3.11 -
    3.12 -
    3.13 -(*"raw" notion of invariant.  Yields a SET of programs*)
    3.14 -Goal "[| Init F<=A;  stable (Acts F) A |] ==> F : invariant A";
    3.15 -by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
    3.16 -qed "invariantI";
    3.17 -
    3.18 -Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
    3.19 -     "F : invariant A ==> Invariant F A";
    3.20 -by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
    3.21 -qed "invariant_imp_Invariant";
    3.22 -
    3.23 -
    3.24 -(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
    3.25 -Goal "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)";
    3.26 -by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
    3.27 -qed "invariant_Int";
    3.28 -
    3.29 -Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
    3.30 -     "Invariant F A = (F : invariant (reachable F Int A))";
    3.31 -by (blast_tac (claset() addIs reachable.intrs) 1);
    3.32 -qed "Invariant_eq_invariant_reachable";
    3.33 -
    3.34 -
    3.35 -bind_thm ("invariant_includes_reachable",
    3.36 -	  invariant_imp_Invariant RS Invariant_includes_reachable);
    3.37 -
    3.38 -Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
    3.39 -by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
    3.40 -                               stable_reachable,
    3.41 -			       impOfSubs invariant_includes_reachable]) 1);
    3.42 -qed "always_eq_UN_invariant";
    3.43 -
    3.44 -Goal "F : always A = (EX I. F: invariant I & I <= A)";
    3.45 -by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
    3.46 -by (Blast_tac 1);
    3.47 -qed "always_iff_ex_invariant";
    3.48 -
    3.49 -
    3.50 -Goalw [increasing_def, stable_def, constrains_def]
    3.51 -     "increasing f <= increasing (length o f)";
    3.52 -by Auto_tac;
    3.53 -by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
    3.54 -qed "increasing_length";
    3.55 -
    3.56 -
    3.57 -Goalw [increasing_def]
    3.58 -     "increasing f <= {F. ALL z::nat. stable (Acts F) {s. z < f s}}";
    3.59 -by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
    3.60 -by (Blast_tac 1);
    3.61 -qed "increasing_less";
    3.62 -
    3.63 -
    3.64 -Goal "[| F Join G : f localTo F;  (s,s') : act;  \
    3.65 -\        act : Acts G; act ~: Acts F |] ==> f s' = f s";
    3.66 -by (asm_full_simp_tac 
    3.67 -    (simpset() addsimps [localTo_def, Acts_Join, stable_def, 
    3.68 -			 constrains_def]) 1);
    3.69 -by (Blast_tac 1);
    3.70 -qed "localTo_imp_equals";
    3.71 -
    3.72 -
    3.73 -Goal "[| Stable F A;  transient (Acts F) C;  \
    3.74 -\        reachable F <= (-A Un B Un C) |] ==> LeadsTo F A B";
    3.75 +(*Perhaps move to SubstAx.ML*)
    3.76 +Goal "[| F : Stable A;  F : transient C;  \
    3.77 +\        reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B";
    3.78  by (etac reachable_LeadsTo_weaken 1);
    3.79  by (rtac LeadsTo_Diff 1);
    3.80  by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
    3.81 @@ -82,28 +17,25 @@
    3.82  qed "Stable_transient_reachable_LeadsTo";
    3.83  
    3.84  
    3.85 -(**** things that definitely belong in Client.ML ****)
    3.86  
    3.87  (*split_all_tac causes a big blow-up*)
    3.88  claset_ref() := claset() delSWrapper "split_all_tac";
    3.89  
    3.90 -val Client_simp = Cli_prg_def RS def_prg_simps;
    3.91 +Addsimps [Cli_prg_def RS def_prg_Init];
    3.92 +program_defs_ref := [Cli_prg_def];
    3.93  
    3.94  Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
    3.95  
    3.96 -DelIffs [length_Suc_conv];
    3.97 -
    3.98  (*Simplification for records*)
    3.99  Addsimps (thms"state.update_defs");
   3.100  
   3.101 -
   3.102  (*CAN THIS be generalized?
   3.103    Importantly, the second case considers actions that are in G
   3.104    and NOT in Cli_prg (needed to use localTo_imp_equals) *)
   3.105  Goal "(act : Acts (Cli_prg Join G)) = \
   3.106  \      (act : {Id, rel_act, tok_act, ask_act} | \
   3.107  \       act : Acts G & act ~: Acts Cli_prg)";
   3.108 -by (asm_full_simp_tac (simpset() addsimps [Client_simp, Acts_Join]) 1);
   3.109 +by (asm_full_simp_tac (simpset() addsimps [Cli_prg_def, Acts_Join]) 1);
   3.110  (*don't unfold definitions of actions*)
   3.111  by (blast_tac HOL_cs 1);
   3.112  qed "Acts_Cli_Join_eq";
   3.113 @@ -111,19 +43,18 @@
   3.114  
   3.115  fun invariant_tac i = 
   3.116      rtac invariantI i  THEN
   3.117 -    auto_tac (claset(), simpset() addsimps [Client_simp])  THEN
   3.118 -    constrains_tac i;
   3.119 +    constrains_tac (i+1);
   3.120  
   3.121  (*Safety property 1(a): ask is nondecreasing*)
   3.122  Goalw [increasing_def] "Cli_prg: increasing ask";
   3.123 -by (auto_tac (claset(), simpset() addsimps [Client_simp]));
   3.124 +by (Clarify_tac 1);
   3.125  by (constrains_tac 1);
   3.126  by Auto_tac;
   3.127  qed "increasing_ask";
   3.128  
   3.129  (*Safety property 1(b): rel is nondecreasing*)
   3.130  Goalw [increasing_def] "Cli_prg: increasing rel";
   3.131 -by (auto_tac (claset(), simpset() addsimps [Client_simp]));
   3.132 +by (Clarify_tac 1);
   3.133  by (constrains_tac 1);
   3.134  by Auto_tac;
   3.135  qed "increasing_rel";
   3.136 @@ -148,16 +79,21 @@
   3.137  qed "ask_bounded";
   3.138  
   3.139  
   3.140 +(*Curiously, we no longer need to expand the program definition, and 
   3.141 +  expanding it is extremely expensive!*)
   3.142 +program_defs_ref := [];
   3.143 +
   3.144  (*Safety property 2: clients return the right number of tokens*)
   3.145  Goalw [increasing_def]
   3.146        "Cli_prg : (increasing giv Int (rel localTo Cli_prg))  \
   3.147  \                guarantees invariant {s. rel s <= giv s}";
   3.148  by (rtac guaranteesI 1);
   3.149 -by (Clarify_tac 1);
   3.150  by (invariant_tac 1);
   3.151 +by (Force_tac 1);
   3.152  by (subgoal_tac "rel s <= giv s'" 1);
   3.153  by (force_tac (claset(),
   3.154 -	       simpset() addsimps [stable_def, constrains_def]) 2);
   3.155 +	       simpset() delsimps [Acts_eq]
   3.156 +			 addsimps [stable_def, constrains_def]) 2);
   3.157  by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
   3.158  (*we note that "rel" is local to Client*)
   3.159  by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
   3.160 @@ -166,12 +102,12 @@
   3.161  
   3.162  (*** Towards proving the liveness property ***)
   3.163  
   3.164 -Goal "transient (Acts (Cli_prg Join G))   \
   3.165 -\               {s. length (giv s) = Suc k &  \
   3.166 -\                   length (rel s) = k & ask s ! k <= giv s ! k}";
   3.167 +Goal "Cli_prg Join G   \
   3.168 +\       : transient {s. length (giv s) = Suc k &  \
   3.169 +\                       length (rel s) = k & ask s ! k <= giv s ! k}";
   3.170  by (res_inst_tac [("act", "rel_act")] transient_mem 1);
   3.171  by (auto_tac (claset(),
   3.172 -	      simpset() addsimps [Domain_def, Acts_Join, Client_simp]));
   3.173 +	      simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def]));
   3.174  qed "transient_lemma";
   3.175  
   3.176  Goal "Cli_prg : \
   3.177 @@ -183,6 +119,7 @@
   3.178  by (Clarify_tac 1);
   3.179  by (dtac (impOfSubs increasing_length) 1);
   3.180  by (invariant_tac 1);
   3.181 +by (Force_tac 1);
   3.182  by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
   3.183  by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
   3.184  by (force_tac (claset(),
   3.185 @@ -194,8 +131,8 @@
   3.186  Goal "Cli_prg : \
   3.187  \      (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
   3.188  \                 Int invariant giv_meets_ask) \
   3.189 -\      guarantees {F. LeadsTo F {s. k < length (giv s)}    \
   3.190 -\                               {s. k < length (rel s)}}";
   3.191 +\      guarantees (LeadsTo {s. k < length (giv s)}    \
   3.192 +\                          {s. k < length (rel s)})";
   3.193  by (rtac guaranteesI 1);
   3.194  by (Clarify_tac 1);
   3.195  by (rtac Stable_transient_reachable_LeadsTo 1);
     4.1 --- a/src/HOL/UNITY/Client.thy	Wed Oct 14 15:47:22 1998 +0200
     4.2 +++ b/src/HOL/UNITY/Client.thy	Thu Oct 15 11:35:07 1998 +0200
     4.3 @@ -8,24 +8,6 @@
     4.4  
     4.5  Client = Comp + Prefix + 
     4.6  
     4.7 -constdefs  (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
     4.8 -  always :: "'a set => 'a program set"
     4.9 -    "always A == {F. reachable F <= A}"
    4.10 -
    4.11 -  (*The traditional word for inductive properties.  Anyway, INDUCTIVE is
    4.12 -    reserved!*)
    4.13 -  invariant :: "'a set => 'a program set"
    4.14 -    "invariant A == {F. Init F <= A & stable (Acts F) A}"
    4.15 -
    4.16 -  (*Polymorphic in both states and the meaning of <= *)
    4.17 -  increasing :: "['a => 'b::{ord}] => 'a program set"
    4.18 -    "increasing f == {F. ALL z. stable (Acts F) {s. z <= f s}}"
    4.19 -
    4.20 -  (*The set of systems that regard "f" as local to F*)
    4.21 -  localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
    4.22 -    "f localTo F == {G. ALL z. stable (Acts G - Acts F) {s. f s = z}}"
    4.23 -
    4.24 -
    4.25  consts
    4.26    Max :: nat       (*Maximum number of tokens*)
    4.27  
     5.1 --- a/src/HOL/UNITY/Common.ML	Wed Oct 14 15:47:22 1998 +0200
     5.2 +++ b/src/HOL/UNITY/Common.ML	Thu Oct 15 11:35:07 1998 +0200
     5.3 @@ -11,8 +11,8 @@
     5.4  *)
     5.5  
     5.6  (*Misra's property CMT4: t exceeds no common meeting time*)
     5.7 -Goal "[| ALL m. Constrains F {m} (maxfg m); n: common |] \
     5.8 -\     ==> Stable F (atMost n)";
     5.9 +Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \
    5.10 +\     ==> F : Stable (atMost n)";
    5.11  by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
    5.12  by (asm_full_simp_tac
    5.13      (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
    5.14 @@ -22,39 +22,40 @@
    5.15  qed "common_stable";
    5.16  
    5.17  Goal "[| Init F <= atMost n;  \
    5.18 -\        ALL m. Constrains F {m} (maxfg m); n: common |] \
    5.19 -\     ==> Invariant F (atMost n)";
    5.20 +\        ALL m. F : Constrains {m} (maxfg m); n: common |] \
    5.21 +\     ==> F : Invariant (atMost n)";
    5.22  by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
    5.23  qed "common_Invariant";
    5.24  
    5.25  
    5.26  (*** Some programs that implement the safety property above ***)
    5.27  
    5.28 -(*This one is just Skip*)
    5.29 -Goal "constrains {Id} {m} (maxfg m)";
    5.30 +Goal "SKIP : constrains {m} (maxfg m)";
    5.31  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    5.32 -				  fasc, gasc]) 1);
    5.33 +				  fasc]) 1);
    5.34  result();
    5.35  
    5.36 -(*This one is  t := ftime t || t := gtime t    really needs Skip too*)
    5.37 -Goal "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
    5.38 -\                    {m} (maxfg m)";
    5.39 +(*This one is  t := ftime t || t := gtime t*)
    5.40 +Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
    5.41 +\      : constrains {m} (maxfg m)";
    5.42  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    5.43 -				  le_max_iff_disj]) 1);
    5.44 +				  le_max_iff_disj, fasc]) 1);
    5.45  by (Blast_tac 1);
    5.46  result();
    5.47  
    5.48 -(*This one is  t := max (ftime t) (gtime t)    really needs Skip too*)
    5.49 -Goal "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
    5.50 -\                    {m} (maxfg m)";
    5.51 -by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
    5.52 +(*This one is  t := max (ftime t) (gtime t)*)
    5.53 +Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
    5.54 +\      : constrains {m} (maxfg m)";
    5.55 +by (simp_tac 
    5.56 +    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    5.57  by (Blast_tac 1);
    5.58  result();
    5.59  
    5.60  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    5.61 -Goalw [constrains_def, maxfg_def] 
    5.62 -    "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
    5.63 -\               {m} (maxfg m)";
    5.64 +Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
    5.65 +\      : constrains {m} (maxfg m)";
    5.66 +by (simp_tac 
    5.67 +    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    5.68  by (blast_tac (claset() addIs [Suc_leI]) 1);
    5.69  result();
    5.70  
    5.71 @@ -67,10 +68,10 @@
    5.72  
    5.73  Addsimps [atMost_Int_atLeast];
    5.74  
    5.75 -Goal "[| ALL m. Constrains F {m} (maxfg m); \
    5.76 -\               ALL m: lessThan n. LeadsTo F {m} (greaterThan m); \
    5.77 +Goal "[| ALL m. F : Constrains {m} (maxfg m); \
    5.78 +\               ALL m: lessThan n. F : LeadsTo {m} (greaterThan m); \
    5.79  \               n: common |]  \
    5.80 -\            ==> LeadsTo F (atMost n) common";
    5.81 +\     ==> F : LeadsTo (atMost n) common";
    5.82  by (rtac LeadsTo_weaken_R 1);
    5.83  by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
    5.84  by (ALLGOALS Asm_simp_tac);
    5.85 @@ -80,10 +81,10 @@
    5.86  val lemma = result();
    5.87  
    5.88  (*The "ALL m: -common" form echoes CMT6.*)
    5.89 -Goal "[| ALL m. Constrains F {m} (maxfg m); \
    5.90 -\               ALL m: -common. LeadsTo F {m} (greaterThan m); \
    5.91 +Goal "[| ALL m. F : Constrains {m} (maxfg m); \
    5.92 +\               ALL m: -common. F : LeadsTo {m} (greaterThan m); \
    5.93  \               n: common |]  \
    5.94 -\            ==> LeadsTo F (atMost (LEAST n. n: common)) common";
    5.95 +\            ==> F : LeadsTo (atMost (LEAST n. n: common)) common";
    5.96  by (rtac lemma 1);
    5.97  by (ALLGOALS Asm_simp_tac);
    5.98  by (etac LeastI 2);
     6.1 --- a/src/HOL/UNITY/Common.thy	Wed Oct 14 15:47:22 1998 +0200
     6.2 +++ b/src/HOL/UNITY/Common.thy	Thu Oct 15 11:35:07 1998 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
     6.5  *)
     6.6  
     6.7 -Common = SubstAx +
     6.8 +Common = SubstAx + Union + 
     6.9  
    6.10  consts
    6.11    ftime,gtime :: nat=>nat
     7.1 --- a/src/HOL/UNITY/Constrains.ML	Wed Oct 14 15:47:22 1998 +0200
     7.2 +++ b/src/HOL/UNITY/Constrains.ML	Thu Oct 15 11:35:07 1998 +0200
     7.3 @@ -9,68 +9,66 @@
     7.4  
     7.5  (*** Constrains ***)
     7.6  
     7.7 -(*Map its type, ('a * 'a)set set, 'a set, 'a set] => bool, to just 'a*)
     7.8 -Blast.overloaded ("Constrains.Constrains", 
     7.9 -		  HOLogic.dest_setT o domain_type o range_type);
    7.10 +overload_1st_set "Constrains.Constrains";
    7.11  
    7.12 -(*constrains (Acts F) B B'
    7.13 -  ==> constrains (Acts F) (reachable F Int B) (reachable F Int B')*)
    7.14 +(*F : constrains B B'
    7.15 +  ==> F : constrains (reachable F Int B) (reachable F Int B')*)
    7.16  bind_thm ("constrains_reachable_Int",
    7.17  	  subset_refl RS
    7.18  	  rewrite_rule [stable_def] stable_reachable RS 
    7.19  	  constrains_Int);
    7.20  
    7.21 -Goalw [Constrains_def] "constrains (Acts F) A A' ==> Constrains F A A'";
    7.22 -by (etac constrains_reachable_Int 1);
    7.23 +Goalw [Constrains_def] "F : constrains A A' ==> F : Constrains A A'";
    7.24 +by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
    7.25  qed "constrains_imp_Constrains";
    7.26  
    7.27 -Goalw [stable_def, Stable_def] "stable (Acts F) A ==> Stable F A";
    7.28 +Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A";
    7.29  by (etac constrains_imp_Constrains 1);
    7.30  qed "stable_imp_Stable";
    7.31  
    7.32  val prems = Goal
    7.33      "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
    7.34 -\    ==> Constrains F A A'";
    7.35 +\    ==> F : Constrains A A'";
    7.36  by (rtac constrains_imp_Constrains 1);
    7.37  by (blast_tac (claset() addIs (constrainsI::prems)) 1);
    7.38  qed "ConstrainsI";
    7.39  
    7.40 -Goalw [Constrains_def, constrains_def] "Constrains F {} B";
    7.41 +Goalw [Constrains_def, constrains_def] "F : Constrains {} B";
    7.42  by (Blast_tac 1);
    7.43  qed "Constrains_empty";
    7.44  
    7.45 -Goal "Constrains F A UNIV";
    7.46 +Goal "F : Constrains A UNIV";
    7.47  by (blast_tac (claset() addIs [ConstrainsI]) 1);
    7.48  qed "Constrains_UNIV";
    7.49  AddIffs [Constrains_empty, Constrains_UNIV];
    7.50  
    7.51  
    7.52  Goalw [Constrains_def]
    7.53 -    "[| Constrains F A A'; A'<=B' |] ==> Constrains F A B'";
    7.54 +    "[| F : Constrains A A'; A'<=B' |] ==> F : Constrains A B'";
    7.55  by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
    7.56  qed "Constrains_weaken_R";
    7.57  
    7.58  Goalw [Constrains_def]
    7.59 -    "[| Constrains F A A'; B<=A |] ==> Constrains F B A'";
    7.60 +    "[| F : Constrains A A'; B<=A |] ==> F : Constrains B A'";
    7.61  by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
    7.62  qed "Constrains_weaken_L";
    7.63  
    7.64  Goalw [Constrains_def]
    7.65 -   "[| Constrains F A A'; B<=A; A'<=B' |] ==> Constrains F B B'";
    7.66 +   "[| F : Constrains A A'; B<=A; A'<=B' |] ==> F : Constrains B B'";
    7.67  by (blast_tac (claset() addIs [constrains_weaken]) 1);
    7.68  qed "Constrains_weaken";
    7.69  
    7.70  (** Union **)
    7.71  
    7.72  Goalw [Constrains_def]
    7.73 -    "[| Constrains F A A'; Constrains F B B' |]   \
    7.74 -\    ==> Constrains F (A Un B) (A' Un B')";
    7.75 +    "[| F : Constrains A A'; F : Constrains B B' |]   \
    7.76 +\    ==> F : Constrains (A Un B) (A' Un B')";
    7.77  by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
    7.78  qed "Constrains_Un";
    7.79  
    7.80 -Goalw [Constrains_def]
    7.81 -    "ALL i:I. Constrains F (A i) (A' i) \
    7.82 -\    ==> Constrains F (UN i:I. A i) (UN i:I. A' i)";
    7.83 +Goal "ALL i:I. F : Constrains (A i) (A' i) \
    7.84 +\     ==> F : Constrains (UN i:I. A i) (UN i:I. A' i)";
    7.85 +by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
    7.86  by (dtac ball_constrains_UN 1);
    7.87  by (blast_tac (claset() addIs [constrains_weaken]) 1);
    7.88  qed "ball_Constrains_UN";
    7.89 @@ -78,75 +76,75 @@
    7.90  (** Intersection **)
    7.91  
    7.92  Goalw [Constrains_def]
    7.93 -    "[| Constrains F A A'; Constrains F B B' |]   \
    7.94 -\    ==> Constrains F (A Int B) (A' Int B')";
    7.95 +    "[| F : Constrains A A'; F : Constrains B B' |]   \
    7.96 +\    ==> F : Constrains (A Int B) (A' Int B')";
    7.97  by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
    7.98  qed "Constrains_Int";
    7.99  
   7.100 -Goalw [Constrains_def]
   7.101 -    "[| ALL i:I. Constrains F (A i) (A' i) |]   \
   7.102 -\    ==> Constrains F (INT i:I. A i) (INT i:I. A' i)";
   7.103 +Goal "[| ALL i:I. F : Constrains (A i) (A' i) |]   \
   7.104 +\     ==> F : Constrains (INT i:I. A i) (INT i:I. A' i)";
   7.105 +by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
   7.106  by (dtac ball_constrains_INT 1);
   7.107  by (dtac constrains_reachable_Int 1);
   7.108  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   7.109  qed "ball_Constrains_INT";
   7.110  
   7.111 -Goalw [Constrains_def]
   7.112 -     "Constrains F A A' ==> reachable F Int A <= A'";
   7.113 +Goal "F : Constrains A A' ==> reachable F Int A <= A'";
   7.114 +by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
   7.115  by (dtac constrains_imp_subset 1);
   7.116  by (ALLGOALS
   7.117      (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
   7.118  qed "Constrains_imp_subset";
   7.119  
   7.120  Goalw [Constrains_def]
   7.121 -    "[| Constrains F A B; Constrains F B C |]   \
   7.122 -\    ==> Constrains F A C";
   7.123 +    "[| F : Constrains A B; F : Constrains B C |]   \
   7.124 +\    ==> F : Constrains A C";
   7.125  by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
   7.126  qed "Constrains_trans";
   7.127  
   7.128  
   7.129  (*** Stable ***)
   7.130  
   7.131 -Goal "Stable F A = stable (Acts F) (reachable F Int A)";
   7.132 +Goal "(F : Stable A) = (F : stable (reachable F Int A))";
   7.133  by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
   7.134  qed "Stable_eq_stable";
   7.135  
   7.136 -Goalw [Stable_def] "Constrains F A A ==> Stable F A";
   7.137 +Goalw [Stable_def] "F : Constrains A A ==> F : Stable A";
   7.138  by (assume_tac 1);
   7.139  qed "StableI";
   7.140  
   7.141 -Goalw [Stable_def] "Stable F A ==> Constrains F A A";
   7.142 +Goalw [Stable_def] "F : Stable A ==> F : Constrains A A";
   7.143  by (assume_tac 1);
   7.144  qed "StableD";
   7.145  
   7.146  Goalw [Stable_def]
   7.147 -    "[| Stable F A; Stable F A' |] ==> Stable F (A Un A')";
   7.148 +    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')";
   7.149  by (blast_tac (claset() addIs [Constrains_Un]) 1);
   7.150  qed "Stable_Un";
   7.151  
   7.152  Goalw [Stable_def]
   7.153 -    "[| Stable F A; Stable F A' |] ==> Stable F (A Int A')";
   7.154 +    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')";
   7.155  by (blast_tac (claset() addIs [Constrains_Int]) 1);
   7.156  qed "Stable_Int";
   7.157  
   7.158  Goalw [Stable_def]
   7.159 -    "[| Stable F C; Constrains F A (C Un A') |]   \
   7.160 -\    ==> Constrains F (C Un A) (C Un A')";
   7.161 +    "[| F : Stable C; F : Constrains A (C Un A') |]   \
   7.162 +\    ==> F : Constrains (C Un A) (C Un A')";
   7.163  by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
   7.164  qed "Stable_Constrains_Un";
   7.165  
   7.166  Goalw [Stable_def]
   7.167 -    "[| Stable F C; Constrains F (C Int A) A' |]   \
   7.168 -\    ==> Constrains F (C Int A) (C Int A')";
   7.169 +    "[| F : Stable C; F : Constrains (C Int A) A' |]   \
   7.170 +\    ==> F : Constrains (C Int A) (C Int A')";
   7.171  by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
   7.172  qed "Stable_Constrains_Int";
   7.173  
   7.174  Goalw [Stable_def]
   7.175 -    "(ALL i:I. Stable F (A i)) ==> Stable F (INT i:I. A i)";
   7.176 +    "(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
   7.177  by (etac ball_Constrains_INT 1);
   7.178  qed "ball_Stable_INT";
   7.179  
   7.180 -Goal "Stable F (reachable F)";
   7.181 +Goal "F : Stable (reachable F)";
   7.182  by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
   7.183  qed "Stable_reachable";
   7.184  
   7.185 @@ -157,21 +155,21 @@
   7.186       in forward proof. ***)
   7.187  
   7.188  Goalw [Constrains_def, constrains_def]
   7.189 -    "[| ALL m. Constrains F {s. s x = m} (B m) |] \
   7.190 -\    ==> Constrains F {s. s x : M} (UN m:M. B m)";
   7.191 +    "[| ALL m. F : Constrains {s. s x = m} (B m) |] \
   7.192 +\    ==> F : Constrains {s. s x : M} (UN m:M. B m)";
   7.193  by (Blast_tac 1);
   7.194  qed "Elimination";
   7.195  
   7.196  (*As above, but for the trivial case of a one-variable state, in which the
   7.197    state is identified with its one variable.*)
   7.198  Goalw [Constrains_def, constrains_def]
   7.199 -    "(ALL m. Constrains F {m} (B m)) ==> Constrains F M (UN m:M. B m)";
   7.200 +    "(ALL m. F : Constrains {m} (B m)) ==> F : Constrains M (UN m:M. B m)";
   7.201  by (Blast_tac 1);
   7.202  qed "Elimination_sing";
   7.203  
   7.204  Goalw [Constrains_def, constrains_def]
   7.205 -   "[| Constrains F A (A' Un B); Constrains F B B' |] \
   7.206 -\   ==> Constrains F A (A' Un B')";
   7.207 +   "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
   7.208 +\   ==> F : Constrains A (A' Un B')";
   7.209  by (Blast_tac 1);
   7.210  qed "Constrains_cancel";
   7.211  
   7.212 @@ -180,11 +178,11 @@
   7.213  
   7.214  (** Natural deduction rules for "Invariant F A" **)
   7.215  
   7.216 -Goal "[| Init F<=A;  Stable F A |] ==> Invariant F A";
   7.217 +Goal "[| Init F<=A;  F : Stable A |] ==> F : Invariant A";
   7.218  by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
   7.219  qed "InvariantI";
   7.220  
   7.221 -Goal "Invariant F A ==> Init F<=A & Stable F A";
   7.222 +Goal "F : Invariant A ==> Init F<=A & F : Stable A";
   7.223  by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
   7.224  qed "InvariantD";
   7.225  
   7.226 @@ -192,13 +190,13 @@
   7.227  
   7.228  
   7.229  (*The set of all reachable states is an Invariant...*)
   7.230 -Goal "Invariant F (reachable F)";
   7.231 +Goal "F : Invariant (reachable F)";
   7.232  by (simp_tac (simpset() addsimps [Invariant_def]) 1);
   7.233  by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1);
   7.234  qed "Invariant_reachable";
   7.235  
   7.236  (*...in fact the strongest Invariant!*)
   7.237 -Goal "Invariant F A ==> reachable F <= A";
   7.238 +Goal "F : Invariant A ==> reachable F <= A";
   7.239  by (full_simp_tac 
   7.240      (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
   7.241  			 Invariant_def]) 1);
   7.242 @@ -207,25 +205,36 @@
   7.243  by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   7.244  qed "Invariant_includes_reachable";
   7.245  
   7.246 +Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
   7.247 +     "F : invariant A ==> F : Invariant A";
   7.248 +by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
   7.249 +qed "invariant_imp_Invariant";
   7.250  
   7.251 -Goal "Invariant F INV ==> reachable F Int INV = reachable F";
   7.252 +Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
   7.253 +     "(F : Invariant A) = (F : invariant (reachable F Int A))";
   7.254 +by (blast_tac (claset() addIs reachable.intrs) 1);
   7.255 +qed "Invariant_eq_invariant_reachable";
   7.256 +
   7.257 +
   7.258 +
   7.259 +Goal "F : Invariant INV ==> reachable F Int INV = reachable F";
   7.260  by (dtac Invariant_includes_reachable 1);
   7.261  by (Blast_tac 1);
   7.262  qed "reachable_Int_INV";
   7.263  
   7.264 -Goal "[| Invariant F INV;  Constrains F (INV Int A) A' |]   \
   7.265 -\     ==> Constrains F A A'";
   7.266 +Goal "[| F : Invariant INV;  F : Constrains (INV Int A) A' |]   \
   7.267 +\     ==> F : Constrains A A'";
   7.268  by (asm_full_simp_tac
   7.269      (simpset() addsimps [Constrains_def, reachable_Int_INV,
   7.270  			 Int_assoc RS sym]) 1);
   7.271  qed "Invariant_ConstrainsI";
   7.272  
   7.273 -(* [| Invariant F INV; Constrains F (INV Int A) A |]
   7.274 -   ==> Stable F A *)
   7.275 +(* [| F : Invariant INV; F : Constrains (INV Int A) A |]
   7.276 +   ==> F : Stable A *)
   7.277  bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
   7.278  
   7.279 -Goal "[| Invariant F INV;  Constrains F A A' |]   \
   7.280 -\     ==> Constrains F A (INV Int A')";
   7.281 +Goal "[| F : Invariant INV;  F : Constrains A A' |]   \
   7.282 +\     ==> F : Constrains A (INV Int A')";
   7.283  by (asm_full_simp_tac
   7.284      (simpset() addsimps [Constrains_def, reachable_Int_INV,
   7.285  			 Int_assoc RS sym]) 1);
   7.286 @@ -237,7 +246,7 @@
   7.287  
   7.288  (** Conjoining Invariants **)
   7.289  
   7.290 -Goal "[| Invariant F A;  Invariant F B |] ==> Invariant F (A Int B)";
   7.291 +Goal "[| F : Invariant A;  F : Invariant B |] ==> F : Invariant (A Int B)";
   7.292  by (auto_tac (claset(),
   7.293  	      simpset() addsimps [Invariant_def, Stable_Int]));
   7.294  qed "Invariant_Int";
   7.295 @@ -246,7 +255,7 @@
   7.296    used by Invariant_Int) *)
   7.297  val Invariant_thin =
   7.298      read_instantiate_sg (sign_of thy)
   7.299 -                [("V", "Invariant ?Prg ?A")] thin_rl;
   7.300 +                [("V", "?F : Invariant ?A")] thin_rl;
   7.301  
   7.302  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   7.303  val Invariant_Int_tac = dtac Invariant_Int THEN' 
   7.304 @@ -257,15 +266,19 @@
   7.305  val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
   7.306  
   7.307  
   7.308 +(*To allow expansion of the program's definition when appropriate*)
   7.309 +val program_defs_ref = ref ([] : thm list);
   7.310 +
   7.311  (*proves "constrains" properties when the program is specified*)
   7.312 -val constrains_tac = 
   7.313 +fun constrains_tac i = 
   7.314     SELECT_GOAL
   7.315 -      (EVERY [REPEAT (resolve_tac [StableI, stableI,
   7.316 +      (EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1,
   7.317 +	      REPEAT (resolve_tac [StableI, stableI,
   7.318  				   constrains_imp_Constrains] 1),
   7.319  	      rtac constrainsI 1,
   7.320  	      Full_simp_tac 1,
   7.321  	      REPEAT (FIRSTGOAL (etac disjE)),
   7.322  	      ALLGOALS Clarify_tac,
   7.323 -	      ALLGOALS Asm_full_simp_tac]);
   7.324 +	      ALLGOALS Asm_full_simp_tac]) i;
   7.325  
   7.326  
     8.1 --- a/src/HOL/UNITY/Constrains.thy	Wed Oct 14 15:47:22 1998 +0200
     8.2 +++ b/src/HOL/UNITY/Constrains.thy	Thu Oct 15 11:35:07 1998 +0200
     8.3 @@ -10,19 +10,17 @@
     8.4  
     8.5  constdefs
     8.6  
     8.7 -  Constrains :: "['a program, 'a set, 'a set] => bool"
     8.8 -    "Constrains F A B == 
     8.9 -		 constrains (Acts F)
    8.10 -                            (reachable F  Int  A)
    8.11 -  		            (reachable F  Int  B)"
    8.12 +  Constrains :: "['a set, 'a set] => 'a program set"
    8.13 +    "Constrains A B == {F. F : constrains (reachable F  Int  A)
    8.14 +  		                          (reachable F  Int  B)}"
    8.15  
    8.16 -  Stable     :: "'a program => 'a set => bool"
    8.17 -    "Stable F A == Constrains F A A"
    8.18 +  Stable     :: "'a set => 'a program set"
    8.19 +    "Stable A == Constrains A A"
    8.20  
    8.21 -  Unless :: "['a program, 'a set, 'a set] => bool"
    8.22 -    "Unless F A B == Constrains F (A-B) (A Un B)"
    8.23 +  Unless :: "['a set, 'a set] => 'a program set"
    8.24 +    "Unless A B == Constrains (A-B) (A Un B)"
    8.25  
    8.26 -  Invariant :: "['a program, 'a set] => bool"
    8.27 -  "Invariant F A == (Init F) <= A & Stable F A"
    8.28 +  Invariant :: "'a set => 'a program set"
    8.29 +    "Invariant A == {F. Init F <= A} Int Stable A"
    8.30  
    8.31  end
     9.1 --- a/src/HOL/UNITY/Deadlock.ML	Wed Oct 14 15:47:22 1998 +0200
     9.2 +++ b/src/HOL/UNITY/Deadlock.ML	Thu Oct 15 11:35:07 1998 +0200
     9.3 @@ -9,80 +9,70 @@
     9.4  
     9.5  (*Trivial, two-process case*)
     9.6  Goalw [constrains_def, stable_def]
     9.7 -    "[| constrains Acts (A Int B) A;  constrains Acts (B Int A) B |] \
     9.8 -\           ==> stable Acts (A Int B)";
     9.9 +    "[| F : constrains (A Int B) A;  F : constrains (B Int A) B |] \
    9.10 +\    ==> F : stable (A Int B)";
    9.11  by (Blast_tac 1);
    9.12  result();
    9.13  
    9.14  
    9.15 -Goal "{i. i < Suc n} = insert n {i. i < n}";
    9.16 -by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
    9.17 -qed "Collect_less_Suc_insert";
    9.18 -
    9.19 -
    9.20 -Goal "{i. i <= Suc n} = insert (Suc n) {i. i <= n}";
    9.21 -by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1);
    9.22 -qed "Collect_le_Suc_insert";
    9.23 -
    9.24 -
    9.25  (*a simplification step*)
    9.26 -Goal "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
    9.27 -\         (INT i:{i. i <= Suc n}. A i)";
    9.28 +Goal "(INT i: atMost n. A(Suc i) Int A i) = \
    9.29 +\     (INT i: atMost (Suc n). A i)";
    9.30  by (induct_tac "n" 1);
    9.31 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert])));
    9.32 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc])));
    9.33  by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
    9.34  qed "Collect_le_Int_equals";
    9.35  
    9.36  
    9.37  (*Dual of the required property.  Converse inclusion fails.*)
    9.38 -Goal "(UN i:{i. i < n}. A i) Int -(A n) <=  \
    9.39 -\         (UN i:{i. i < n}. (A i) Int -(A(Suc i)))";
    9.40 +Goal "(UN i: lessThan n. A i) Int -(A n) <=  \
    9.41 +\     (UN i: lessThan n. (A i) Int -(A(Suc i)))";
    9.42  by (induct_tac "n" 1);
    9.43  by (Asm_simp_tac 1);
    9.44 -by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
    9.45 +by (simp_tac (simpset() addsimps [lessThan_Suc]) 1);
    9.46  by (Blast_tac 1);
    9.47  qed "UN_Int_Compl_subset";
    9.48  
    9.49  
    9.50  (*Converse inclusion fails.*)
    9.51 -Goal "(INT i:{i. i < n}. -A i Un A (Suc i))  <= \
    9.52 -\         (INT i:{i. i < n}. -A i) Un A n";
    9.53 +Goal "(INT i: lessThan n. -A i Un A (Suc i))  <= \
    9.54 +\     (INT i: lessThan n. -A i) Un A n";
    9.55  by (induct_tac "n" 1);
    9.56  by (Asm_simp_tac 1);
    9.57 -by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
    9.58 +by (asm_simp_tac (simpset() addsimps [lessThan_Suc]) 1);
    9.59  by (Blast_tac 1);
    9.60  qed "INT_Un_Compl_subset";
    9.61  
    9.62  
    9.63  (*Specialized rewriting*)
    9.64 -Goal "A 0 Int (-(A n) Int (INT i:{i. i < n}. -A i Un A (Suc i))) = {}";
    9.65 +Goal "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}";
    9.66  by (blast_tac (claset() addIs [gr0I]
    9.67  		        addDs [impOfSubs INT_Un_Compl_subset]) 1);
    9.68  val lemma = result();
    9.69  
    9.70  (*Reverse direction makes it harder to invoke the ind hyp*)
    9.71 -Goal "(INT i:{i. i <= n}. A i) = \
    9.72 -\         A 0 Int (INT i:{i. i < n}. -A i Un A(Suc i))";
    9.73 +Goal "(INT i: atMost n. A i) = \
    9.74 +\         A 0 Int (INT i: lessThan n. -A i Un A(Suc i))";
    9.75  by (induct_tac "n" 1);
    9.76  by (Asm_simp_tac 1);
    9.77  by (asm_simp_tac
    9.78      (simpset() addsimps Int_ac @
    9.79  			[Int_Un_distrib, Int_Un_distrib2, lemma,
    9.80 -			 Collect_less_Suc_insert, Collect_le_Suc_insert]) 1);
    9.81 +			 lessThan_Suc, atMost_Suc]) 1);
    9.82  qed "INT_le_equals_Int";
    9.83  
    9.84 -Goal "(INT i:{i. i <= Suc n}. A i) = \
    9.85 -\         A 0 Int (INT i:{i. i <= n}. -A i Un A(Suc i))";
    9.86 -by (simp_tac (simpset() addsimps [less_Suc_eq_le, INT_le_equals_Int]) 1);
    9.87 +Goal "(INT i: atMost (Suc n). A i) = \
    9.88 +\         A 0 Int (INT i: atMost n. -A i Un A(Suc i))";
    9.89 +by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1);
    9.90  qed "INT_le_Suc_equals_Int";
    9.91  
    9.92  
    9.93  (*The final deadlock example*)
    9.94  val [zeroprem, allprem] = goalw thy [stable_def]
    9.95 -    "[| constrains Acts (A 0 Int A (Suc n)) (A 0);  \
    9.96 -\       ALL i:{i. i <= n}. constrains Acts (A(Suc i) Int A i) \
    9.97 +    "[| F : constrains (A 0 Int A (Suc n)) (A 0);  \
    9.98 +\       ALL i: atMost n. F : constrains (A(Suc i) Int A i) \
    9.99  \                                         (-A i Un A(Suc i)) |] \
   9.100 -\    ==> stable Acts (INT i:{i. i <= Suc n}. A i)";
   9.101 +\    ==> F : stable (INT i: atMost (Suc n). A i)";
   9.102  
   9.103  by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
   9.104      constrains_Int RS constrains_weaken) 1);
    10.1 --- a/src/HOL/UNITY/FP.ML	Wed Oct 14 15:47:22 1998 +0200
    10.2 +++ b/src/HOL/UNITY/FP.ML	Thu Oct 15 11:35:07 1998 +0200
    10.3 @@ -8,7 +8,7 @@
    10.4  From Misra, "A Logic for Concurrent Programming", 1994
    10.5  *)
    10.6  
    10.7 -Goalw [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
    10.8 +Goalw [FP_Orig_def, stable_def] "F : stable (FP_Orig F Int B)";
    10.9  by (stac Int_Union2 1);
   10.10  by (rtac ball_constrains_UN 1);
   10.11  by (Simp_tac 1);
   10.12 @@ -16,13 +16,13 @@
   10.13  
   10.14  
   10.15  val prems = goalw thy [FP_Orig_def, stable_def]
   10.16 -    "(!!B. stable Acts (A Int B)) ==> A <= FP_Orig Acts";
   10.17 +    "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F";
   10.18  by (blast_tac (claset() addIs prems) 1);
   10.19  qed "FP_Orig_weakest";
   10.20  
   10.21  
   10.22 -Goal "stable Acts (FP Acts Int B)";
   10.23 -by (subgoal_tac "FP Acts Int B = (UN x:B. FP Acts Int {x})" 1);
   10.24 +Goal "F : stable (FP F Int B)";
   10.25 +by (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x})" 1);
   10.26  by (Blast_tac 2);
   10.27  by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1);
   10.28  by (rewrite_goals_tac [FP_def, stable_def]);
   10.29 @@ -30,31 +30,31 @@
   10.30  by (Simp_tac 1);
   10.31  qed "stable_FP_Int";
   10.32  
   10.33 -Goal "FP Acts <= FP_Orig Acts";
   10.34 +Goal "FP F <= FP_Orig F";
   10.35  by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
   10.36  val lemma1 = result();
   10.37  
   10.38 -Goalw [FP_Orig_def, FP_def] "FP_Orig Acts <= FP Acts";
   10.39 +Goalw [FP_Orig_def, FP_def] "FP_Orig F <= FP F";
   10.40  by (Clarify_tac 1);
   10.41  by (dres_inst_tac [("x", "{x}")] spec 1);
   10.42  by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1);
   10.43  val lemma2 = result();
   10.44  
   10.45 -Goal "FP Acts = FP_Orig Acts";
   10.46 +Goal "FP F = FP_Orig F";
   10.47  by (rtac ([lemma1,lemma2] MRS equalityI) 1);
   10.48  qed "FP_equivalence";
   10.49  
   10.50  val [prem] = goal thy
   10.51 -    "(!!B. stable Acts (A Int B)) ==> A <= FP Acts";
   10.52 +    "(!!B. F : stable (A Int B)) ==> A <= FP F";
   10.53  by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
   10.54  qed "FP_weakest";
   10.55  
   10.56  Goalw [FP_def, stable_def, constrains_def]
   10.57 -    "-(FP Acts) = (UN act:Acts. -{s. act^^{s} <= {s}})";
   10.58 +    "-(FP F) = (UN act: Acts F. -{s. act^^{s} <= {s}})";
   10.59  by (Blast_tac 1);
   10.60  qed "Compl_FP";
   10.61  
   10.62 -Goal "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})";
   10.63 +Goal "A - (FP F) = (UN act: Acts F. A - {s. act^^{s} <= {s}})";
   10.64  by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
   10.65  qed "Diff_FP";
   10.66  
    11.1 --- a/src/HOL/UNITY/FP.thy	Wed Oct 14 15:47:22 1998 +0200
    11.2 +++ b/src/HOL/UNITY/FP.thy	Thu Oct 15 11:35:07 1998 +0200
    11.3 @@ -12,10 +12,10 @@
    11.4  
    11.5  constdefs
    11.6  
    11.7 -  FP_Orig :: "('a * 'a)set set => 'a set"
    11.8 -    "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}"
    11.9 +  FP_Orig :: "'a program => 'a set"
   11.10 +    "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
   11.11  
   11.12 -  FP :: "('a * 'a)set set => 'a set"
   11.13 -    "FP Acts == {s. stable Acts {s}}"
   11.14 +  FP :: "'a program => 'a set"
   11.15 +    "FP F == {s. F : stable {s}}"
   11.16  
   11.17  end
    12.1 --- a/src/HOL/UNITY/Handshake.ML	Wed Oct 14 15:47:22 1998 +0200
    12.2 +++ b/src/HOL/UNITY/Handshake.ML	Thu Oct 15 11:35:07 1998 +0200
    12.3 @@ -11,8 +11,9 @@
    12.4  (*split_all_tac causes a big blow-up*)
    12.5  claset_ref() := claset() delSWrapper "split_all_tac";
    12.6  
    12.7 -Addsimps [prgF_def RS def_prg_simps];
    12.8 -Addsimps [prgG_def RS def_prg_simps];
    12.9 +Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
   12.10 +program_defs_ref := [F_def, G_def];
   12.11 +
   12.12  Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
   12.13  
   12.14  (*Simplification for records*)
   12.15 @@ -20,7 +21,7 @@
   12.16  Addsimps [simp_of_set invFG_def];
   12.17  
   12.18  
   12.19 -Goal "Invariant (prgF Join prgG) invFG";
   12.20 +Goal "(F Join G) : Invariant invFG";
   12.21  by (rtac InvariantI 1);
   12.22  by (Force_tac 1);
   12.23  by (rtac (constrains_imp_Constrains RS StableI) 1);
   12.24 @@ -30,26 +31,26 @@
   12.25  by (constrains_tac 1);
   12.26  qed "invFG";
   12.27  
   12.28 -Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \
   12.29 +Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \
   12.30  \                              ({s. NF s = k} Int {s. BB s})";
   12.31  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
   12.32  by (ensures_tac "cmdG" 2);
   12.33  by (constrains_tac 1);
   12.34  qed "lemma2_1";
   12.35  
   12.36 -Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
   12.37 +Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
   12.38  by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
   12.39  by (constrains_tac 2);
   12.40  by (ensures_tac "cmdF" 1);
   12.41  qed "lemma2_2";
   12.42  
   12.43  
   12.44 -Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}";
   12.45 +Goal "(F Join G) : LeadsTo UNIV {s. m < NF s}";
   12.46  by (rtac LeadsTo_weaken_R 1);
   12.47  by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
   12.48      GreaterThan_bounded_induct 1);
   12.49  by (auto_tac (claset(), simpset() addsimps [vimage_def]));
   12.50 -(*The inductive step: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*)
   12.51 +(*The inductive step: (F Join G) : LeadsTo {x. NF x = ma} {x. ma < NF x}*)
   12.52  by (rtac LeadsTo_Diff 1);
   12.53  by (rtac lemma2_2 2);
   12.54  by (rtac LeadsTo_Trans 1);
    13.1 --- a/src/HOL/UNITY/Handshake.thy	Wed Oct 14 15:47:22 1998 +0200
    13.2 +++ b/src/HOL/UNITY/Handshake.thy	Thu Oct 15 11:35:07 1998 +0200
    13.3 @@ -20,15 +20,15 @@
    13.4    cmdF :: "(state*state) set"
    13.5      "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
    13.6  
    13.7 -  prgF :: "state program"
    13.8 -    "prgF == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
    13.9 +  F :: "state program"
   13.10 +    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
   13.11  
   13.12    (*G's program*)
   13.13    cmdG :: "(state*state) set"
   13.14      "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
   13.15  
   13.16 -  prgG :: "state program"
   13.17 -    "prgG == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
   13.18 +  G :: "state program"
   13.19 +    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
   13.20  
   13.21    (*the joint invariant*)
   13.22    invFG :: "state set"
    14.1 --- a/src/HOL/UNITY/LessThan.ML	Wed Oct 14 15:47:22 1998 +0200
    14.2 +++ b/src/HOL/UNITY/LessThan.ML	Thu Oct 15 11:35:07 1998 +0200
    14.3 @@ -7,6 +7,7 @@
    14.4  *)
    14.5  
    14.6  
    14.7 +(*Make Auto_tac and Force_tac try trans_tac!*)
    14.8  claset_ref() := claset() addaltern ("trans_tac",trans_tac);
    14.9  
   14.10  
   14.11 @@ -27,6 +28,10 @@
   14.12  by (Blast_tac 1);
   14.13  qed "lessThan_Suc";
   14.14  
   14.15 +Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
   14.16 +by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
   14.17 +qed "lessThan_Suc_atMost";
   14.18 +
   14.19  Goal "(UN m. lessThan m) = UNIV";
   14.20  by (Blast_tac 1);
   14.21  qed "UN_lessThan_UNIV";
    15.1 --- a/src/HOL/UNITY/Lift.ML	Wed Oct 14 15:47:22 1998 +0200
    15.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Oct 15 11:35:07 1998 +0200
    15.3 @@ -55,7 +55,8 @@
    15.4       zless_not_refl2, zless_not_refl3];
    15.5  
    15.6  
    15.7 -Addsimps [Lprg_def RS def_prg_simps];
    15.8 +Addsimps [Lprg_def RS def_prg_Init];
    15.9 +program_defs_ref := [Lprg_def];
   15.10  
   15.11  Addsimps (map simp_of_act
   15.12  	  [request_act_def, open_act_def, close_act_def,
   15.13 @@ -69,7 +70,7 @@
   15.14  
   15.15  
   15.16  val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
   15.17 -(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
   15.18 +(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *)
   15.19  
   15.20  
   15.21  (*Simplification for records*)
   15.22 @@ -87,41 +88,41 @@
   15.23  val nat_exhaust_pred_le = 
   15.24      read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
   15.25  
   15.26 -Goal "Invariant Lprg open_stop";
   15.27 +Goal "Lprg : Invariant open_stop";
   15.28  by (rtac InvariantI 1);
   15.29  by (Force_tac 1);
   15.30  by (constrains_tac 1);
   15.31  qed "open_stop";
   15.32  
   15.33 -Goal "Invariant Lprg stop_floor";
   15.34 +Goal "Lprg : Invariant stop_floor";
   15.35  by (rtac InvariantI 1);
   15.36  by (Force_tac 1);
   15.37  by (constrains_tac 1);
   15.38  qed "stop_floor";
   15.39  
   15.40  (*This one needs open_stop, which was proved above*)
   15.41 -Goal "Invariant Lprg open_move";
   15.42 +Goal "Lprg : Invariant open_move";
   15.43  by (rtac InvariantI 1);
   15.44  by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
   15.45  by (Force_tac 1);
   15.46  by (constrains_tac 1);
   15.47  qed "open_move";
   15.48  
   15.49 -Goal "Invariant Lprg moving_up";
   15.50 +Goal "Lprg : Invariant moving_up";
   15.51  by (rtac InvariantI 1);
   15.52  by (Force_tac 1);
   15.53  by (constrains_tac 1);
   15.54  by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
   15.55  qed "moving_up";
   15.56  
   15.57 -Goal "Invariant Lprg moving_down";
   15.58 +Goal "Lprg : Invariant moving_down";
   15.59  by (rtac InvariantI 1);
   15.60  by (Force_tac 1);
   15.61  by (constrains_tac 1);
   15.62  by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
   15.63  qed "moving_down";
   15.64  
   15.65 -Goal "Invariant Lprg bounded";
   15.66 +Goal "Lprg : Invariant bounded";
   15.67  by (rtac InvariantI 1);
   15.68  by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
   15.69  by (Force_tac 1);
   15.70 @@ -150,23 +151,23 @@
   15.71  
   15.72  (** Lift_1 **)
   15.73  
   15.74 -Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
   15.75 +Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)";
   15.76  by (cut_facts_tac [stop_floor] 1);
   15.77  by (ensures_tac "open_act" 1);
   15.78  qed "E_thm01";  (*lem_lift_1_5*)
   15.79  
   15.80 -Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
   15.81 +Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
   15.82  \                  (Req n Int opened - atFloor n)";
   15.83  by (cut_facts_tac [stop_floor] 1);
   15.84  by (ensures_tac "open_act" 1);
   15.85  qed "E_thm02";  (*lem_lift_1_1*)
   15.86  
   15.87 -Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
   15.88 +Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
   15.89  \                  (Req n Int closed - (atFloor n - queueing))";
   15.90  by (ensures_tac "close_act" 1);
   15.91  qed "E_thm03";  (*lem_lift_1_2*)
   15.92  
   15.93 -Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
   15.94 +Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
   15.95  \                  (opened Int atFloor n)";
   15.96  by (ensures_tac "open_act" 1);
   15.97  qed "E_thm04";  (*lem_lift_1_7*)
   15.98 @@ -190,7 +191,7 @@
   15.99  (*lem_lift_2_0 
  15.100    NOT an ensures property, but a mere inclusion;
  15.101    don't know why script lift_2.uni says ENSURES*)
  15.102 -Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
  15.103 +Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
  15.104  \                  ((closed Int goingup Int Req n)  Un \
  15.105  \                   (closed Int goingdown Int Req n))";
  15.106  by (rtac subset_imp_LeadsTo 1);
  15.107 @@ -198,7 +199,7 @@
  15.108  qed "E_thm05c";
  15.109  
  15.110  (*lift_2*)
  15.111 -Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
  15.112 +Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
  15.113  \                  (moving Int Req n)";
  15.114  by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
  15.115  by (ensures_tac "req_down" 2);
  15.116 @@ -212,7 +213,7 @@
  15.117  
  15.118  (*lem_lift_4_1 *)
  15.119  Goal "#0 < N ==> \
  15.120 -\     LeadsTo Lprg \
  15.121 +\     Lprg : LeadsTo \
  15.122  \       (moving Int Req n Int {s. metric n s = N} Int \
  15.123  \         {s. floor s ~: req s} Int {s. up s})   \
  15.124  \       (moving Int Req n Int {s. metric n s < N})";
  15.125 @@ -232,7 +233,7 @@
  15.126  
  15.127  (*lem_lift_4_3 *)
  15.128  Goal "#0 < N ==> \
  15.129 -\     LeadsTo Lprg \
  15.130 +\     Lprg : LeadsTo \
  15.131  \       (moving Int Req n Int {s. metric n s = N} Int \
  15.132  \        {s. floor s ~: req s} - {s. up s})   \
  15.133  \       (moving Int Req n Int {s. metric n s < N})";
  15.134 @@ -250,7 +251,7 @@
  15.135  qed "E_thm12b";
  15.136  
  15.137  (*lift_4*)
  15.138 -Goal "#0<N ==> LeadsTo Lprg (moving Int Req n Int {s. metric n s = N} Int \
  15.139 +Goal "#0<N ==> Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \
  15.140  \                           {s. floor s ~: req s})     \
  15.141  \                          (moving Int Req n Int {s. metric n s < N})";
  15.142  by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
  15.143 @@ -264,7 +265,7 @@
  15.144  
  15.145  (*lem_lift_5_3*)
  15.146  Goal "#0<N   \
  15.147 -\     ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
  15.148 +\     ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \
  15.149  \                      (moving Int Req n Int {s. metric n s < N})";
  15.150  by (cut_facts_tac [bounded] 1);
  15.151  by (ensures_tac "req_up" 1);
  15.152 @@ -280,7 +281,7 @@
  15.153  
  15.154  (*lem_lift_5_1 has ~goingup instead of goingdown*)
  15.155  Goal "#0<N ==>   \
  15.156 -\     LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
  15.157 +\     Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \
  15.158  \                  (moving Int Req n Int {s. metric n s < N})";
  15.159  by (cut_facts_tac [bounded] 1);
  15.160  by (ensures_tac "req_down" 1);
  15.161 @@ -309,7 +310,7 @@
  15.162  
  15.163  
  15.164  (*lift_5*)
  15.165 -Goal "#0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N})   \
  15.166 +Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N})   \
  15.167  \                          (moving Int Req n Int {s. metric n s < N})";
  15.168  by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
  15.169  by (etac E_thm16b 3);
  15.170 @@ -341,7 +342,7 @@
  15.171  
  15.172  
  15.173  (*lem_lift_3_1*)
  15.174 -Goal "LeadsTo Lprg (moving Int Req n Int {s. metric n s = #0})   \
  15.175 +Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0})   \
  15.176  \                  (stopped Int atFloor n)";
  15.177  by (cut_facts_tac [bounded] 1);
  15.178  by (ensures_tac "request_act" 1);
  15.179 @@ -349,7 +350,7 @@
  15.180  qed "E_thm11";
  15.181  
  15.182  (*lem_lift_3_5*)
  15.183 -Goal "LeadsTo Lprg \
  15.184 +Goal "Lprg : LeadsTo \
  15.185  \       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
  15.186  \       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
  15.187  by (ensures_tac "request_act" 1);
  15.188 @@ -358,7 +359,7 @@
  15.189  
  15.190  (*lem_lift_3_6*)
  15.191  Goal "#0 < N ==> \
  15.192 -\     LeadsTo Lprg \
  15.193 +\     Lprg : LeadsTo \
  15.194  \       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
  15.195  \       (opened Int Req n Int {s. metric n s = N})";
  15.196  by (ensures_tac "open_act" 1);
  15.197 @@ -367,7 +368,7 @@
  15.198  qed "E_thm14";
  15.199  
  15.200  (*lem_lift_3_7*)
  15.201 -Goal "LeadsTo Lprg \
  15.202 +Goal "Lprg : LeadsTo \
  15.203  \       (opened Int Req n Int {s. metric n s = N})  \
  15.204  \       (closed Int Req n Int {s. metric n s = N})";
  15.205  by (ensures_tac "close_act" 1);
  15.206 @@ -378,7 +379,7 @@
  15.207  (** the final steps **)
  15.208  
  15.209  Goal "#0 < N ==> \
  15.210 -\     LeadsTo Lprg \
  15.211 +\     Lprg : LeadsTo \
  15.212  \       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
  15.213  \       (moving Int Req n Int {s. metric n s < N})";
  15.214  by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
  15.215 @@ -399,7 +400,7 @@
  15.216  
  15.217  val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
  15.218  
  15.219 -Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
  15.220 +Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)";
  15.221  by (rtac (reach_nonneg RS integ_0_le_induct) 1);
  15.222  by (case_tac "#0 < z" 1);
  15.223  (*If z <= #0 then actually z = #0*)
  15.224 @@ -413,7 +414,7 @@
  15.225  qed "lift_3";
  15.226  
  15.227  
  15.228 -Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
  15.229 +Goal "Lprg : LeadsTo (Req n) (opened Int atFloor n)";
  15.230  by (rtac LeadsTo_Trans 1);
  15.231  by (rtac (E_thm04 RS LeadsTo_Un) 2);
  15.232  by (rtac LeadsTo_Un_post 2);
    16.1 --- a/src/HOL/UNITY/Mutex.ML	Wed Oct 14 15:47:22 1998 +0200
    16.2 +++ b/src/HOL/UNITY/Mutex.ML	Thu Oct 15 11:35:07 1998 +0200
    16.3 @@ -9,7 +9,8 @@
    16.4  (*split_all_tac causes a big blow-up*)
    16.5  claset_ref() := claset() delSWrapper "split_all_tac";
    16.6  
    16.7 -Addsimps [Mprg_def RS def_prg_simps];
    16.8 +Addsimps [Mprg_def RS def_prg_Init];
    16.9 +program_defs_ref := [Mprg_def];
   16.10  
   16.11  Addsimps (map simp_of_act
   16.12  	  [cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
   16.13 @@ -21,13 +22,13 @@
   16.14  (*Simplification for records*)
   16.15  Addsimps (thms"state.update_defs");
   16.16  
   16.17 -Goal "Invariant Mprg invariantU";
   16.18 +Goal "Mprg : Invariant invariantU";
   16.19  by (rtac InvariantI 1);
   16.20  by (constrains_tac 2);
   16.21  by Auto_tac;
   16.22  qed "invariantU";
   16.23  
   16.24 -Goal "Invariant Mprg invariantV";
   16.25 +Goal "Mprg : Invariant invariantV";
   16.26  by (rtac InvariantI 1);
   16.27  by (constrains_tac 2);
   16.28  by Auto_tac;
   16.29 @@ -44,7 +45,7 @@
   16.30  
   16.31  
   16.32  (*The bad invariant FAILS in cmd1V*)
   16.33 -Goal "Invariant Mprg bad_invariantU";
   16.34 +Goal "Mprg : Invariant bad_invariantU";
   16.35  by (rtac InvariantI 1);
   16.36  by (constrains_tac 2);
   16.37  by (Force_tac 1);
   16.38 @@ -77,44 +78,44 @@
   16.39  
   16.40  (*** Progress for U ***)
   16.41  
   16.42 -Goalw [Unless_def] "Unless Mprg {s. MM s=#2} {s. MM s=#3}";
   16.43 +Goalw [Unless_def] "Mprg : Unless {s. MM s=#2} {s. MM s=#3}";
   16.44  by (constrains_tac 1);
   16.45  qed "U_F0";
   16.46  
   16.47 -Goal "LeadsTo Mprg {s. MM s=#1} {s. PP s = VV s & MM s = #2}";
   16.48 +Goal "Mprg : LeadsTo {s. MM s=#1} {s. PP s = VV s & MM s = #2}";
   16.49  by (ensures_tac "cmd1U" 1);
   16.50  qed "U_F1";
   16.51  
   16.52 -Goal "LeadsTo Mprg {s. ~ PP s & MM s = #2} {s. MM s = #3}";
   16.53 +Goal "Mprg : LeadsTo {s. ~ PP s & MM s = #2} {s. MM s = #3}";
   16.54  by (cut_facts_tac [invariantU] 1);
   16.55  by (ensures_tac "cmd2U" 1);
   16.56  qed "U_F2";
   16.57  
   16.58 -Goal "LeadsTo Mprg {s. MM s = #3} {s. PP s}";
   16.59 +Goal "Mprg : LeadsTo {s. MM s = #3} {s. PP s}";
   16.60  by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1);
   16.61  by (ensures_tac "cmd4U" 2);
   16.62  by (ensures_tac "cmd3U" 1);
   16.63  qed "U_F3";
   16.64  
   16.65 -Goal "LeadsTo Mprg {s. MM s = #2} {s. PP s}";
   16.66 +Goal "Mprg : LeadsTo {s. MM s = #2} {s. PP s}";
   16.67  by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
   16.68  	  MRS LeadsTo_Diff) 1);
   16.69  by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   16.70  by (auto_tac (claset() addSEs [less_SucE], simpset()));
   16.71  val U_lemma2 = result();
   16.72  
   16.73 -Goal "LeadsTo Mprg {s. MM s = #1} {s. PP s}";
   16.74 +Goal "Mprg : LeadsTo {s. MM s = #1} {s. PP s}";
   16.75  by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
   16.76  by (Blast_tac 1);
   16.77  val U_lemma1 = result();
   16.78  
   16.79 -Goal "LeadsTo Mprg {s. #1 <= MM s & MM s <= #3} {s. PP s}";
   16.80 +Goal "Mprg : LeadsTo {s. #1 <= MM s & MM s <= #3} {s. PP s}";
   16.81  by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
   16.82  				  U_lemma1, U_lemma2, U_F3] ) 1);
   16.83  val U_lemma123 = result();
   16.84  
   16.85  (*Misra's F4*)
   16.86 -Goal "LeadsTo Mprg {s. UU s} {s. PP s}";
   16.87 +Goal "Mprg : LeadsTo {s. UU s} {s. PP s}";
   16.88  by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
   16.89  by Auto_tac;
   16.90  qed "u_Leadsto_p";
   16.91 @@ -123,45 +124,45 @@
   16.92  (*** Progress for V ***)
   16.93  
   16.94  
   16.95 -Goalw [Unless_def] "Unless Mprg {s. NN s=#2} {s. NN s=#3}";
   16.96 +Goalw [Unless_def] "Mprg : Unless {s. NN s=#2} {s. NN s=#3}";
   16.97  by (constrains_tac 1);
   16.98  qed "V_F0";
   16.99  
  16.100 -Goal "LeadsTo Mprg {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}";
  16.101 +Goal "Mprg : LeadsTo {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}";
  16.102  by (ensures_tac "cmd1V" 1);
  16.103  qed "V_F1";
  16.104  
  16.105 -Goal "LeadsTo Mprg {s. PP s & NN s = #2} {s. NN s = #3}";
  16.106 +Goal "Mprg : LeadsTo {s. PP s & NN s = #2} {s. NN s = #3}";
  16.107  by (cut_facts_tac [invariantV] 1);
  16.108  by (ensures_tac "cmd2V" 1);
  16.109  qed "V_F2";
  16.110  
  16.111 -Goal "LeadsTo Mprg {s. NN s = #3} {s. ~ PP s}";
  16.112 +Goal "Mprg : LeadsTo {s. NN s = #3} {s. ~ PP s}";
  16.113  by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1);
  16.114  by (ensures_tac "cmd4V" 2);
  16.115  by (ensures_tac "cmd3V" 1);
  16.116  qed "V_F3";
  16.117  
  16.118 -Goal "LeadsTo Mprg {s. NN s = #2} {s. ~ PP s}";
  16.119 +Goal "Mprg : LeadsTo {s. NN s = #2} {s. ~ PP s}";
  16.120  by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
  16.121  	  MRS LeadsTo_Diff) 1);
  16.122  by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
  16.123  by (auto_tac (claset() addSEs [less_SucE], simpset()));
  16.124  val V_lemma2 = result();
  16.125  
  16.126 -Goal "LeadsTo Mprg {s. NN s = #1} {s. ~ PP s}";
  16.127 +Goal "Mprg : LeadsTo {s. NN s = #1} {s. ~ PP s}";
  16.128  by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
  16.129  by (Blast_tac 1);
  16.130  val V_lemma1 = result();
  16.131  
  16.132 -Goal "LeadsTo Mprg {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}";
  16.133 +Goal "Mprg : LeadsTo {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}";
  16.134  by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
  16.135  				  V_lemma1, V_lemma2, V_F3] ) 1);
  16.136  val V_lemma123 = result();
  16.137  
  16.138  
  16.139  (*Misra's F4*)
  16.140 -Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
  16.141 +Goal "Mprg : LeadsTo {s. VV s} {s. ~ PP s}";
  16.142  by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
  16.143  by Auto_tac;
  16.144  qed "v_Leadsto_not_p";
  16.145 @@ -170,7 +171,7 @@
  16.146  (** Absence of starvation **)
  16.147  
  16.148  (*Misra's F6*)
  16.149 -Goal "LeadsTo Mprg {s. MM s = #1} {s. MM s = #3}";
  16.150 +Goal "Mprg : LeadsTo {s. MM s = #1} {s. MM s = #3}";
  16.151  by (rtac LeadsTo_Un_duplicate 1);
  16.152  by (rtac LeadsTo_cancel2 1);
  16.153  by (rtac U_F2 2);
  16.154 @@ -184,7 +185,7 @@
  16.155  
  16.156  
  16.157  (*The same for V*)
  16.158 -Goal "LeadsTo Mprg {s. NN s = #1} {s. NN s = #3}";
  16.159 +Goal "Mprg : LeadsTo {s. NN s = #1} {s. NN s = #3}";
  16.160  by (rtac LeadsTo_Un_duplicate 1);
  16.161  by (rtac LeadsTo_cancel2 1);
  16.162  by (rtac V_F2 2);
    17.1 --- a/src/HOL/UNITY/NSP_Bad.ML	Wed Oct 14 15:47:22 1998 +0200
    17.2 +++ b/src/HOL/UNITY/NSP_Bad.ML	Thu Oct 15 11:35:07 1998 +0200
    17.3 @@ -24,6 +24,7 @@
    17.4  
    17.5  Addsimps [Nprg_def RS def_prg_simps];
    17.6  
    17.7 +
    17.8  (*A "possibility property": there are traces that reach the end*)
    17.9  Goal "A ~= B ==> EX NB. EX s: reachable Nprg.                \
   17.10  \                  Says A B (Crypt (pubK B) (Nonce NB)) : set s";
   17.11 @@ -32,7 +33,7 @@
   17.12  by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
   17.13  by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
   17.14  by (rtac reachable.Init 5);
   17.15 -by (ALLGOALS Asm_simp_tac);
   17.16 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
   17.17  by (REPEAT_FIRST (rtac exI ));
   17.18  by possibility_tac;
   17.19  result();
   17.20 @@ -66,7 +67,7 @@
   17.21  
   17.22  (*Spy never sees another agent's private key! (unless it's bad at start)*)
   17.23  (*
   17.24 -    Goal "Invariant Nprg {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
   17.25 +    Goal "Nprg : Invariant {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
   17.26      by (rtac InvariantI 1);
   17.27      by (Force_tac 1);
   17.28      by (constrains_tac 1);
    18.1 --- a/src/HOL/UNITY/Network.ML	Wed Oct 14 15:47:22 1998 +0200
    18.2 +++ b/src/HOL/UNITY/Network.ML	Thu Oct 15 11:35:07 1998 +0200
    18.3 @@ -10,15 +10,15 @@
    18.4  
    18.5  val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = 
    18.6  Goalw [stable_def]
    18.7 -   "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
    18.8 -\      !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
    18.9 -\      !! m proc. stable Acts {s. m <= s(proc,Sent)};  \
   18.10 -\      !! n proc. stable Acts {s. n <= s(proc,Rcvd)};  \
   18.11 -\      !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
   18.12 +   "[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
   18.13 +\      !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
   18.14 +\      !! m proc. F : stable {s. m <= s(proc,Sent)};  \
   18.15 +\      !! n proc. F : stable {s. n <= s(proc,Rcvd)};  \
   18.16 +\      !! m proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
   18.17  \                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
   18.18 -\      !! n proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
   18.19 +\      !! n proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
   18.20  \                                 {s. s(proc,Sent) = n} \
   18.21 -\   |] ==> stable Acts {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
   18.22 +\   |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
   18.23  \                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
   18.24  \                         s(Bproc,Sent) = s(Aproc,Rcvd) & \
   18.25  \                         s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
    19.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Oct 14 15:47:22 1998 +0200
    19.2 +++ b/src/HOL/UNITY/ROOT.ML	Thu Oct 15 11:35:07 1998 +0200
    19.3 @@ -10,6 +10,10 @@
    19.4  
    19.5  writeln"Root file for HOL/UNITY";
    19.6  set proof_timing;
    19.7 +
    19.8 +loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
    19.9 +time_use_thy"UNITY";
   19.10 +
   19.11  time_use_thy "Deadlock";
   19.12  time_use_thy "WFair";
   19.13  time_use_thy "Common";
   19.14 @@ -22,9 +26,7 @@
   19.15  time_use_thy "Handshake";
   19.16  time_use_thy "Lift";
   19.17  time_use_thy "Comp";
   19.18 +time_use_thy "Client";
   19.19  
   19.20  loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
   19.21  use_thy"NSP_Bad";
   19.22 -
   19.23 -loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
   19.24 -use_thy"Client";
    20.1 --- a/src/HOL/UNITY/Reach.ML	Wed Oct 14 15:47:22 1998 +0200
    20.2 +++ b/src/HOL/UNITY/Reach.ML	Thu Oct 15 11:35:07 1998 +0200
    20.3 @@ -19,7 +19,8 @@
    20.4  AddSEs [ifE];
    20.5  
    20.6  
    20.7 -Addsimps [Rprg_def RS def_prg_simps];
    20.8 +Addsimps [Rprg_def RS def_prg_Init];
    20.9 +program_defs_ref := [Rprg_def];
   20.10  
   20.11  Addsimps [simp_of_act asgt_def];
   20.12  
   20.13 @@ -28,7 +29,7 @@
   20.14  
   20.15  Addsimps [simp_of_set reach_invariant_def];
   20.16  
   20.17 -Goal "Invariant Rprg reach_invariant";
   20.18 +Goal "Rprg : Invariant reach_invariant";
   20.19  by (rtac InvariantI 1);
   20.20  by Auto_tac;  (*for the initial state; proof of stability remains*)
   20.21  by (constrains_tac 1);
   20.22 @@ -48,20 +49,20 @@
   20.23  by Auto_tac;
   20.24  qed "fixedpoint_invariant_correct";
   20.25  
   20.26 -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
   20.27 -     "FP (Acts Rprg) <= fixedpoint";
   20.28 +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
   20.29 +     "FP Rprg <= fixedpoint";
   20.30  by Auto_tac;
   20.31  by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
   20.32  by (dtac fun_cong 1);
   20.33  by Auto_tac;
   20.34  val lemma1 = result();
   20.35  
   20.36 -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
   20.37 -     "fixedpoint <= FP (Acts Rprg)";
   20.38 +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
   20.39 +     "fixedpoint <= FP Rprg";
   20.40  by (auto_tac (claset() addSIs [ext], simpset()));
   20.41  val lemma2 = result();
   20.42  
   20.43 -Goal "FP (Acts Rprg) = fixedpoint";
   20.44 +Goal "FP Rprg = fixedpoint";
   20.45  by (rtac ([lemma1,lemma2] MRS equalityI) 1);
   20.46  qed "FP_fixedpoint";
   20.47  
   20.48 @@ -74,7 +75,7 @@
   20.49  
   20.50  Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
   20.51  by (simp_tac (simpset() addsimps
   20.52 -	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1);
   20.53 +	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def])) 1);
   20.54  by Auto_tac;
   20.55  by (rtac fun_upd_idem 1);
   20.56   by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff]));
   20.57 @@ -106,7 +107,7 @@
   20.58  	      simpset() addsimps [fun_upd_idem]));
   20.59  qed "metric_le";
   20.60  
   20.61 -Goal "LeadsTo Rprg ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
   20.62 +Goal "Rprg : LeadsTo ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
   20.63  by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
   20.64  by (rtac LeadsTo_UN 1);
   20.65  by Auto_tac;
   20.66 @@ -118,7 +119,7 @@
   20.67  	      simpset()));
   20.68  qed "LeadsTo_Diff_fixedpoint";
   20.69  
   20.70 -Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
   20.71 +Goal "Rprg : LeadsTo (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
   20.72  by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
   20.73  	   subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
   20.74  by Auto_tac;
   20.75 @@ -126,13 +127,13 @@
   20.76  
   20.77  
   20.78  (*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
   20.79 -Goal "LeadsTo Rprg UNIV fixedpoint";
   20.80 +Goal "Rprg : LeadsTo UNIV fixedpoint";
   20.81  by (rtac LessThan_induct 1);
   20.82  by Auto_tac;
   20.83  by (rtac LeadsTo_Un_fixedpoint 1);
   20.84  qed "LeadsTo_fixedpoint";
   20.85  
   20.86 -Goal "LeadsTo Rprg UNIV { %v. (init, v) : edges^* }";
   20.87 +Goal "Rprg : LeadsTo UNIV { %v. (init, v) : edges^* }";
   20.88  by (stac (fixedpoint_invariant_correct RS sym) 1);
   20.89  by (rtac ([reach_invariant, LeadsTo_fixedpoint] 
   20.90  	  MRS Invariant_LeadsTo_weaken) 1); 
    21.1 --- a/src/HOL/UNITY/SubstAx.ML	Wed Oct 14 15:47:22 1998 +0200
    21.2 +++ b/src/HOL/UNITY/SubstAx.ML	Thu Oct 15 11:35:07 1998 +0200
    21.3 @@ -6,23 +6,21 @@
    21.4  LeadsTo relation, restricted to the set of reachable states.
    21.5  *)
    21.6  
    21.7 -(*Map its type, ['a program, 'a set, 'a set] => bool, to just 'a*)
    21.8 -Blast.overloaded ("SubstAx.LeadsTo", 
    21.9 -		  HOLogic.dest_setT o domain_type o range_type);
   21.10 +overload_1st_set "SubstAx.LeadsTo";
   21.11  
   21.12  
   21.13  (*** Specialized laws for handling invariants ***)
   21.14  
   21.15  (** Conjoining a safety property **)
   21.16  
   21.17 -Goal "[| reachable F <= C;  LeadsTo F (C Int A) A' |]   \
   21.18 -\     ==> LeadsTo F A A'";
   21.19 +Goal "[| reachable F <= C;  F : LeadsTo (C Int A) A' |]   \
   21.20 +\     ==> F : LeadsTo A A'";
   21.21  by (asm_full_simp_tac
   21.22      (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
   21.23  qed "reachable_LeadsToI";
   21.24  
   21.25 -Goal "[| reachable F <= C;  LeadsTo F A A' |]   \
   21.26 -\     ==> LeadsTo F A (C Int A')";
   21.27 +Goal "[| reachable F <= C;  F : LeadsTo A A' |]   \
   21.28 +\     ==> F : LeadsTo A (C Int A')";
   21.29  by (asm_full_simp_tac
   21.30      (simpset() addsimps [LeadsTo_def, Int_absorb2,
   21.31  			 Int_assoc RS sym]) 1);
   21.32 @@ -31,11 +29,11 @@
   21.33  
   21.34  (** Conjoining an invariant **)
   21.35  
   21.36 -(* [| Invariant F C; LeadsTo F (C Int A) A' |] ==> LeadsTo F A A' *)
   21.37 +(* [| Invariant F C; F : LeadsTo (C Int A) A' |] ==> F : LeadsTo A A' *)
   21.38  bind_thm ("Invariant_LeadsToI", 
   21.39  	  Invariant_includes_reachable RS reachable_LeadsToI);
   21.40  
   21.41 -(* [| Invariant F C; LeadsTo F A A' |] ==> LeadsTo F A (C Int A') *)
   21.42 +(* [| Invariant F C; F : LeadsTo A A' |] ==> F : LeadsTo A (C Int A') *)
   21.43  bind_thm ("Invariant_LeadsToD", 
   21.44  	  Invariant_includes_reachable RS reachable_LeadsToD);
   21.45  
   21.46 @@ -44,55 +42,54 @@
   21.47  
   21.48  (*** Introduction rules: Basis, Trans, Union ***)
   21.49  
   21.50 -Goal "leadsTo (Acts F) A B ==> LeadsTo F A B";
   21.51 +Goal "F : leadsTo A B ==> F : LeadsTo A B";
   21.52  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   21.53  by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
   21.54  qed "leadsTo_imp_LeadsTo";
   21.55  
   21.56 -Goal "[| LeadsTo F A B;  LeadsTo F B C |] ==> LeadsTo F A C";
   21.57 +Goal "[| F : LeadsTo A B;  F : LeadsTo B C |] ==> F : LeadsTo A C";
   21.58  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   21.59  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
   21.60  qed "LeadsTo_Trans";
   21.61  
   21.62 -val [prem] = Goalw [LeadsTo_def]
   21.63 - "(!!A. A : S ==> LeadsTo F A B) ==> LeadsTo F (Union S) B";
   21.64 +val prems = Goalw [LeadsTo_def]
   21.65 +     "(!!A. A : S ==> F : LeadsTo A B) ==> F : LeadsTo (Union S) B";
   21.66  by (Simp_tac 1);
   21.67  by (stac Int_Union 1);
   21.68 -by (blast_tac (claset() addIs [leadsTo_UN,
   21.69 -			       simplify (simpset()) prem]) 1);
   21.70 +by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1);
   21.71  qed "LeadsTo_Union";
   21.72  
   21.73  
   21.74  (*** Derived rules ***)
   21.75  
   21.76 -Goal "LeadsTo F A UNIV";
   21.77 -by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
   21.78 -				      Int_lower1 RS subset_imp_leadsTo]) 1);
   21.79 +Goal "F : LeadsTo A UNIV";
   21.80 +by (asm_simp_tac 
   21.81 +    (simpset() addsimps [LeadsTo_def, Int_lower1 RS subset_imp_leadsTo]) 1);
   21.82  qed "LeadsTo_UNIV";
   21.83  Addsimps [LeadsTo_UNIV];
   21.84  
   21.85  (*Useful with cancellation, disjunction*)
   21.86 -Goal "LeadsTo F A (A' Un A') ==> LeadsTo F A A'";
   21.87 +Goal "F : LeadsTo A (A' Un A') ==> F : LeadsTo A A'";
   21.88  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   21.89  qed "LeadsTo_Un_duplicate";
   21.90  
   21.91 -Goal "LeadsTo F A (A' Un C Un C) ==> LeadsTo F A (A' Un C)";
   21.92 +Goal "F : LeadsTo A (A' Un C Un C) ==> F : LeadsTo A (A' Un C)";
   21.93  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   21.94  qed "LeadsTo_Un_duplicate2";
   21.95  
   21.96  val prems = 
   21.97 -Goal "(!!i. i : I ==> LeadsTo F (A i) B) ==> LeadsTo F (UN i:I. A i) B";
   21.98 +Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (UN i:I. A i) B";
   21.99  by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
  21.100  by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
  21.101  qed "LeadsTo_UN";
  21.102  
  21.103  (*Binary union introduction rule*)
  21.104 -Goal "[| LeadsTo F A C; LeadsTo F B C |] ==> LeadsTo F (A Un B) C";
  21.105 +Goal "[| F : LeadsTo A C; F : LeadsTo B C |] ==> F : LeadsTo (A Un B) C";
  21.106  by (stac Un_eq_Union 1);
  21.107  by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
  21.108  qed "LeadsTo_Un";
  21.109  
  21.110 -Goal "A <= B ==> LeadsTo F A B";
  21.111 +Goal "A <= B ==> F : LeadsTo A B";
  21.112  by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  21.113  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
  21.114  qed "subset_imp_LeadsTo";
  21.115 @@ -100,39 +97,39 @@
  21.116  bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
  21.117  Addsimps [empty_LeadsTo];
  21.118  
  21.119 -Goal "[| LeadsTo F A A';  A' <= B' |] ==> LeadsTo F A B'";
  21.120 +Goal "[| F : LeadsTo A A';  A' <= B' |] ==> F : LeadsTo A B'";
  21.121  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  21.122  by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
  21.123  qed_spec_mp "LeadsTo_weaken_R";
  21.124  
  21.125 -Goal "[| LeadsTo F A A';  B <= A |]  \
  21.126 -\     ==> LeadsTo F B A'";
  21.127 +Goal "[| F : LeadsTo A A';  B <= A |]  \
  21.128 +\     ==> F : LeadsTo B A'";
  21.129  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  21.130  by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
  21.131  qed_spec_mp "LeadsTo_weaken_L";
  21.132  
  21.133 -Goal "[| LeadsTo F A A';   \
  21.134 +Goal "[| F : LeadsTo A A';   \
  21.135  \        B  <= A;   A' <= B' |] \
  21.136 -\     ==> LeadsTo F B B'";
  21.137 +\     ==> F : LeadsTo B B'";
  21.138  by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
  21.139  			       LeadsTo_Trans]) 1);
  21.140  qed "LeadsTo_weaken";
  21.141  
  21.142 -Goal "[| reachable F <= C;  LeadsTo F A A';   \
  21.143 +Goal "[| reachable F <= C;  F : LeadsTo A A';   \
  21.144  \        C Int B <= A;   C Int A' <= B' |] \
  21.145 -\     ==> LeadsTo F B B'";
  21.146 +\     ==> F : LeadsTo B B'";
  21.147  by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
  21.148                          addIs [reachable_LeadsToD]) 1);
  21.149  qed "reachable_LeadsTo_weaken";
  21.150  
  21.151  (** Two theorems for "proof lattices" **)
  21.152  
  21.153 -Goal "[| LeadsTo F A B |] ==> LeadsTo F (A Un B) B";
  21.154 +Goal "[| F : LeadsTo A B |] ==> F : LeadsTo (A Un B) B";
  21.155  by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
  21.156  qed "LeadsTo_Un_post";
  21.157  
  21.158 -Goal "[| LeadsTo F A B;  LeadsTo F B C |] \
  21.159 -\     ==> LeadsTo F (A Un B) C";
  21.160 +Goal "[| F : LeadsTo A B;  F : LeadsTo B C |] \
  21.161 +\     ==> F : LeadsTo (A Un B) C";
  21.162  by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, 
  21.163  			       LeadsTo_weaken_L, LeadsTo_Trans]) 1);
  21.164  qed "LeadsTo_Trans_Un";
  21.165 @@ -140,33 +137,33 @@
  21.166  
  21.167  (** Distributive laws **)
  21.168  
  21.169 -Goal "LeadsTo F (A Un B) C  = (LeadsTo F A C & LeadsTo F B C)";
  21.170 +Goal "(F : LeadsTo (A Un B) C)  = (F : LeadsTo A C & F : LeadsTo B C)";
  21.171  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
  21.172  qed "LeadsTo_Un_distrib";
  21.173  
  21.174 -Goal "LeadsTo F (UN i:I. A i) B  =  (ALL i : I. LeadsTo F (A i) B)";
  21.175 +Goal "(F : LeadsTo (UN i:I. A i) B)  =  (ALL i : I. F : LeadsTo (A i) B)";
  21.176  by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
  21.177  qed "LeadsTo_UN_distrib";
  21.178  
  21.179 -Goal "LeadsTo F (Union S) B  =  (ALL A : S. LeadsTo F A B)";
  21.180 +Goal "(F : LeadsTo (Union S) B)  =  (ALL A : S. F : LeadsTo A B)";
  21.181  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
  21.182  qed "LeadsTo_Union_distrib";
  21.183  
  21.184  
  21.185  (** More rules using the premise "Invariant F" **)
  21.186  
  21.187 -Goalw [LeadsTo_def, Constrains_def]
  21.188 -     "[| Constrains F (A-A') (A Un A'); transient  (Acts F) (A-A') |]   \
  21.189 -\     ==> LeadsTo F A A'";
  21.190 +Goal "[| F : Constrains (A-A') (A Un A');  F : transient (A-A') |]   \
  21.191 +\     ==> F : LeadsTo A A'";
  21.192 +by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def]) 1);
  21.193  by (rtac (ensuresI RS leadsTo_Basis) 1);
  21.194  by (blast_tac (claset() addIs [transient_strengthen]) 2);
  21.195  by (blast_tac (claset() addIs [constrains_weaken]) 1);
  21.196  qed "LeadsTo_Basis";
  21.197  
  21.198 -Goal "[| Invariant F INV;      \
  21.199 -\        Constrains F (INV Int (A-A')) (A Un A'); \
  21.200 -\        transient  (Acts F) (INV Int (A-A')) |]   \
  21.201 -\ ==> LeadsTo F A A'";
  21.202 +Goal "[| F : Invariant INV;      \
  21.203 +\        F : Constrains (INV Int (A-A')) (A Un A'); \
  21.204 +\        F : transient (INV Int (A-A')) |]   \
  21.205 +\ ==> F : LeadsTo A A'";
  21.206  by (rtac Invariant_LeadsToI 1);
  21.207  by (assume_tac 1);
  21.208  by (rtac LeadsTo_Basis 1);
  21.209 @@ -174,10 +171,9 @@
  21.210  by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
  21.211  qed "Invariant_LeadsTo_Basis";
  21.212  
  21.213 -Goal "[| Invariant F INV;      \
  21.214 -\        LeadsTo F A A';   \
  21.215 -\        INV Int B  <= A;  INV Int A' <= B' |] \
  21.216 -\     ==> LeadsTo F B B'";
  21.217 +Goal "[| F : Invariant INV;      \
  21.218 +\        F : LeadsTo A A';  INV Int B  <= A;  INV Int A' <= B' |] \
  21.219 +\     ==> F : LeadsTo B B'";
  21.220  by (REPEAT (ares_tac [Invariant_includes_reachable, 
  21.221  		      reachable_LeadsTo_weaken] 1));
  21.222  qed "Invariant_LeadsTo_weaken";
  21.223 @@ -185,17 +181,15 @@
  21.224  
  21.225  (*Set difference: maybe combine with leadsTo_weaken_L??
  21.226    This is the most useful form of the "disjunction" rule*)
  21.227 -Goal "[| LeadsTo F (A-B) C; LeadsTo F (A Int B) C |] \
  21.228 -\     ==> LeadsTo F A C";
  21.229 +Goal "[| F : LeadsTo (A-B) C;  F : LeadsTo (A Int B) C |] \
  21.230 +\     ==> F : LeadsTo A C";
  21.231  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
  21.232  qed "LeadsTo_Diff";
  21.233  
  21.234  
  21.235 -
  21.236 -
  21.237  val prems = 
  21.238 -Goal "(!! i. i:I ==> LeadsTo F (A i) (A' i)) \
  21.239 -\     ==> LeadsTo F (UN i:I. A i) (UN i:I. A' i)";
  21.240 +Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \
  21.241 +\     ==> F : LeadsTo (UN i:I. A i) (UN i:I. A' i)";
  21.242  by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
  21.243  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
  21.244                          addIs prems) 1);
  21.245 @@ -204,22 +198,22 @@
  21.246  
  21.247  (*Version with no index set*)
  21.248  val prems = 
  21.249 -Goal "(!! i. LeadsTo F (A i) (A' i)) \
  21.250 -\     ==> LeadsTo F (UN i. A i) (UN i. A' i)";
  21.251 +Goal "(!! i. F : LeadsTo (A i) (A' i)) \
  21.252 +\     ==> F : LeadsTo (UN i. A i) (UN i. A' i)";
  21.253  by (blast_tac (claset() addIs [LeadsTo_UN_UN] 
  21.254                          addIs prems) 1);
  21.255  qed "LeadsTo_UN_UN_noindex";
  21.256  
  21.257  (*Version with no index set*)
  21.258 -Goal "ALL i. LeadsTo F (A i) (A' i) \
  21.259 -\     ==> LeadsTo F (UN i. A i) (UN i. A' i)";
  21.260 +Goal "ALL i. F : LeadsTo (A i) (A' i) \
  21.261 +\     ==> F : LeadsTo (UN i. A i) (UN i. A' i)";
  21.262  by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
  21.263  qed "all_LeadsTo_UN_UN";
  21.264  
  21.265  
  21.266  (*Binary union version*)
  21.267 -Goal "[| LeadsTo F A A'; LeadsTo F B B' |] \
  21.268 -\           ==> LeadsTo F (A Un B) (A' Un B')";
  21.269 +Goal "[| F : LeadsTo A A'; F : LeadsTo B B' |] \
  21.270 +\           ==> F : LeadsTo (A Un B) (A' Un B')";
  21.271  by (blast_tac (claset() addIs [LeadsTo_Un, 
  21.272  			       LeadsTo_weaken_R]) 1);
  21.273  qed "LeadsTo_Un_Un";
  21.274 @@ -227,38 +221,37 @@
  21.275  
  21.276  (** The cancellation law **)
  21.277  
  21.278 -Goal "[| LeadsTo F A (A' Un B); LeadsTo F B B' |]    \
  21.279 -\     ==> LeadsTo F A (A' Un B')";
  21.280 +Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo B B' |]    \
  21.281 +\     ==> F : LeadsTo A (A' Un B')";
  21.282  by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
  21.283  			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
  21.284  qed "LeadsTo_cancel2";
  21.285  
  21.286 -Goal "[| LeadsTo F A (A' Un B); LeadsTo F (B-A') B' |] \
  21.287 -\     ==> LeadsTo F A (A' Un B')";
  21.288 +Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo (B-A') B' |] \
  21.289 +\     ==> F : LeadsTo A (A' Un B')";
  21.290  by (rtac LeadsTo_cancel2 1);
  21.291  by (assume_tac 2);
  21.292  by (ALLGOALS Asm_simp_tac);
  21.293  qed "LeadsTo_cancel_Diff2";
  21.294  
  21.295 -Goal "[| LeadsTo F A (B Un A'); LeadsTo F B B' |] \
  21.296 -\     ==> LeadsTo F A (B' Un A')";
  21.297 +Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo B B' |] \
  21.298 +\     ==> F : LeadsTo A (B' Un A')";
  21.299  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
  21.300  by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
  21.301  qed "LeadsTo_cancel1";
  21.302  
  21.303 -Goal "[| LeadsTo F A (B Un A'); LeadsTo F (B-A') B' |] \
  21.304 -\     ==> LeadsTo F A (B' Un A')";
  21.305 +Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo (B-A') B' |] \
  21.306 +\     ==> F : LeadsTo A (B' Un A')";
  21.307  by (rtac LeadsTo_cancel1 1);
  21.308  by (assume_tac 2);
  21.309  by (ALLGOALS Asm_simp_tac);
  21.310  qed "LeadsTo_cancel_Diff1";
  21.311  
  21.312  
  21.313 -
  21.314  (** The impossibility law **)
  21.315  
  21.316  (*The set "A" may be non-empty, but it contains no reachable states*)
  21.317 -Goal "LeadsTo F A {} ==> reachable F Int A = {}";
  21.318 +Goal "F : LeadsTo A {} ==> reachable F Int A = {}";
  21.319  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  21.320  by (etac leadsTo_empty 1);
  21.321  qed "LeadsTo_empty";
  21.322 @@ -267,32 +260,33 @@
  21.323  (** PSP: Progress-Safety-Progress **)
  21.324  
  21.325  (*Special case of PSP: Misra's "stable conjunction"*)
  21.326 -Goal "[| LeadsTo F A A';  Stable F B |] ==> LeadsTo F (A Int B) (A' Int B)";
  21.327 +Goal "[| F : LeadsTo A A';  F : Stable B |] \
  21.328 +\     ==> F : LeadsTo (A Int B) (A' Int B)";
  21.329  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
  21.330  by (dtac psp_stable 1);
  21.331  by (assume_tac 1);
  21.332  by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
  21.333  qed "PSP_stable";
  21.334  
  21.335 -Goal "[| LeadsTo F A A'; Stable F B |] \
  21.336 -\     ==> LeadsTo F (B Int A) (B Int A')";
  21.337 +Goal "[| F : LeadsTo A A'; F : Stable B |] \
  21.338 +\     ==> F : LeadsTo (B Int A) (B Int A')";
  21.339  by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
  21.340  qed "PSP_stable2";
  21.341  
  21.342  Goalw [LeadsTo_def, Constrains_def]
  21.343 -     "[| LeadsTo F A A'; Constrains F B B' |] \
  21.344 -\     ==> LeadsTo F (A Int B) ((A' Int B) Un (B' - B))";
  21.345 +     "[| F : LeadsTo A A'; F : Constrains B B' |] \
  21.346 +\     ==> F : LeadsTo (A Int B) ((A' Int B) Un (B' - B))";
  21.347  by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
  21.348  qed "PSP";
  21.349  
  21.350 -Goal "[| LeadsTo F A A'; Constrains F B B' |] \
  21.351 -\     ==> LeadsTo F (B Int A) ((B Int A') Un (B' - B))";
  21.352 +Goal "[| F : LeadsTo A A'; F : Constrains B B' |] \
  21.353 +\     ==> F : LeadsTo (B Int A) ((B Int A') Un (B' - B))";
  21.354  by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
  21.355  qed "PSP2";
  21.356  
  21.357  Goalw [Unless_def]
  21.358 -     "[| LeadsTo F A A'; Unless F B B' |] \
  21.359 -\     ==> LeadsTo F (A Int B) ((A' Int B) Un B')";
  21.360 +     "[| F : LeadsTo A A'; F : Unless B B' |] \
  21.361 +\     ==> F : LeadsTo (A Int B) ((A' Int B) Un B')";
  21.362  by (dtac PSP 1);
  21.363  by (assume_tac 1);
  21.364  by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, 
  21.365 @@ -304,20 +298,19 @@
  21.366  
  21.367  (** Meta or object quantifier ????? **)
  21.368  Goal "[| wf r;     \
  21.369 -\        ALL m. LeadsTo F (A Int f-``{m})                     \
  21.370 +\        ALL m. F : LeadsTo (A Int f-``{m})                     \
  21.371  \                           ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  21.372 -\     ==> LeadsTo F A B";
  21.373 +\     ==> F : LeadsTo A B";
  21.374  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
  21.375  by (etac leadsTo_wf_induct 1);
  21.376 -by (Simp_tac 2);
  21.377  by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
  21.378  qed "LeadsTo_wf_induct";
  21.379  
  21.380  
  21.381  Goal "[| wf r;     \
  21.382 -\        ALL m:I. LeadsTo F (A Int f-``{m})                   \
  21.383 +\        ALL m:I. F : LeadsTo (A Int f-``{m})                   \
  21.384  \                             ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  21.385 -\     ==> LeadsTo F A ((A - (f-``I)) Un B)";
  21.386 +\     ==> F : LeadsTo A ((A - (f-``I)) Un B)";
  21.387  by (etac LeadsTo_wf_induct 1);
  21.388  by Safe_tac;
  21.389  by (case_tac "m:I" 1);
  21.390 @@ -326,9 +319,9 @@
  21.391  qed "Bounded_induct";
  21.392  
  21.393  
  21.394 -Goal "[| ALL m. LeadsTo F (A Int f-``{m})                     \
  21.395 +Goal "[| ALL m. F : LeadsTo (A Int f-``{m})                     \
  21.396  \                           ((A Int f-``(lessThan m)) Un B) |] \
  21.397 -\     ==> LeadsTo F A B";
  21.398 +\     ==> F : LeadsTo A B";
  21.399  by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
  21.400  by (Asm_simp_tac 1);
  21.401  qed "LessThan_induct";
  21.402 @@ -336,26 +329,26 @@
  21.403  (*Integer version.  Could generalize from #0 to any lower bound*)
  21.404  val [reach, prem] =
  21.405  Goal "[| reachable F <= {s. #0 <= f s};  \
  21.406 -\        !! z. LeadsTo F (A Int {s. f s = z})                     \
  21.407 +\        !! z. F : LeadsTo (A Int {s. f s = z})                     \
  21.408  \                           ((A Int {s. f s < z}) Un B) |] \
  21.409 -\     ==> LeadsTo F A B";
  21.410 +\     ==> F : LeadsTo A B";
  21.411  by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
  21.412  by (simp_tac (simpset() addsimps [vimage_def]) 1);
  21.413  by (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1);
  21.414  by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
  21.415  qed "integ_0_le_induct";
  21.416  
  21.417 -Goal "[| ALL m:(greaterThan l). LeadsTo F (A Int f-``{m})   \
  21.418 +Goal "[| ALL m:(greaterThan l). F : LeadsTo (A Int f-``{m})   \
  21.419  \                                        ((A Int f-``(lessThan m)) Un B) |] \
  21.420 -\           ==> LeadsTo F A ((A Int (f-``(atMost l))) Un B)";
  21.421 +\           ==> F : LeadsTo A ((A Int (f-``(atMost l))) Un B)";
  21.422  by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
  21.423  by (rtac (wf_less_than RS Bounded_induct) 1);
  21.424  by (Asm_simp_tac 1);
  21.425  qed "LessThan_bounded_induct";
  21.426  
  21.427 -Goal "[| ALL m:(lessThan l). LeadsTo F (A Int f-``{m})   \
  21.428 +Goal "[| ALL m:(lessThan l). F : LeadsTo (A Int f-``{m})   \
  21.429  \                              ((A Int f-``(greaterThan m)) Un B) |] \
  21.430 -\     ==> LeadsTo F A ((A Int (f-``(atLeast l))) Un B)";
  21.431 +\     ==> F : LeadsTo A ((A Int (f-``(atLeast l))) Un B)";
  21.432  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  21.433      (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
  21.434  by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
  21.435 @@ -368,27 +361,27 @@
  21.436  
  21.437  (*** Completion: Binary and General Finite versions ***)
  21.438  
  21.439 -Goal "[| LeadsTo F A A';  Stable F A';   \
  21.440 -\        LeadsTo F B B';  Stable F B' |] \
  21.441 -\     ==> LeadsTo F (A Int B) (A' Int B')";
  21.442 +Goal "[| F : LeadsTo A A';  F : Stable A';   \
  21.443 +\        F : LeadsTo B B';  F : Stable B' |] \
  21.444 +\     ==> F : LeadsTo (A Int B) (A' Int B')";
  21.445  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
  21.446  by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
  21.447  qed "Stable_completion";
  21.448  
  21.449  
  21.450  Goal "finite I      \
  21.451 -\     ==> (ALL i:I. LeadsTo F (A i) (A' i)) -->  \
  21.452 -\         (ALL i:I. Stable F (A' i)) -->         \
  21.453 -\         LeadsTo F (INT i:I. A i) (INT i:I. A' i)";
  21.454 +\     ==> (ALL i:I. F : LeadsTo (A i) (A' i)) -->  \
  21.455 +\         (ALL i:I. F : Stable (A' i)) -->         \
  21.456 +\         F : LeadsTo (INT i:I. A i) (INT i:I. A' i)";
  21.457  by (etac finite_induct 1);
  21.458  by (Asm_simp_tac 1);
  21.459  by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
  21.460  qed_spec_mp "Finite_stable_completion";
  21.461  
  21.462  
  21.463 -Goal "[| LeadsTo F A (A' Un C);  Constrains F A' (A' Un C); \
  21.464 -\        LeadsTo F B (B' Un C);  Constrains F B' (B' Un C) |] \
  21.465 -\     ==> LeadsTo F (A Int B) ((A' Int B') Un C)";
  21.466 +Goal "[| F : LeadsTo A (A' Un C);  F : Constrains A' (A' Un C); \
  21.467 +\        F : LeadsTo B (B' Un C);  F : Constrains B' (B' Un C) |] \
  21.468 +\     ==> F : LeadsTo (A Int B) ((A' Int B') Un C)";
  21.469  by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
  21.470  				       Int_Un_distrib]) 1);
  21.471  by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
  21.472 @@ -396,9 +389,9 @@
  21.473  
  21.474  
  21.475  Goal "[| finite I |] \
  21.476 -\     ==> (ALL i:I. LeadsTo F (A i) (A' i Un C)) -->  \
  21.477 -\         (ALL i:I. Constrains F (A' i) (A' i Un C)) --> \
  21.478 -\         LeadsTo F (INT i:I. A i) ((INT i:I. A' i) Un C)";
  21.479 +\     ==> (ALL i:I. F : LeadsTo (A i) (A' i Un C)) -->  \
  21.480 +\         (ALL i:I. F : Constrains (A' i) (A' i Un C)) --> \
  21.481 +\         F : LeadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)";
  21.482  by (etac finite_induct 1);
  21.483  by (ALLGOALS Asm_simp_tac);
  21.484  by (Clarify_tac 1);
  21.485 @@ -414,6 +407,8 @@
  21.486  	      etac Invariant_LeadsTo_Basis 1 
  21.487  	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
  21.488  		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
  21.489 +	      (*now there are two subgoals: constrains & transient*)
  21.490 +	      simp_tac (simpset() addsimps !program_defs_ref) 2,
  21.491  	      res_inst_tac [("act", sact)] transient_mem 2,
  21.492                   (*simplify the command's domain*)
  21.493  	      simp_tac (simpset() addsimps [Domain_def]) 3,
    22.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Oct 14 15:47:22 1998 +0200
    22.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Oct 15 11:35:07 1998 +0200
    22.3 @@ -10,9 +10,7 @@
    22.4  
    22.5  constdefs
    22.6  
    22.7 -   LeadsTo :: "['a program, 'a set, 'a set] => bool"
    22.8 -    "LeadsTo F A B ==
    22.9 -		 leadsTo (Acts F)
   22.10 -                         (reachable F  Int  A)
   22.11 -  		         (reachable F  Int  B)"
   22.12 +   LeadsTo :: "['a set, 'a set] => 'a program set"
   22.13 +    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
   22.14 +	   	                    (reachable F  Int  B)}"
   22.15  end
    23.1 --- a/src/HOL/UNITY/Token.ML	Wed Oct 14 15:47:22 1998 +0200
    23.2 +++ b/src/HOL/UNITY/Token.ML	Thu Oct 15 11:35:07 1998 +0200
    23.3 @@ -32,9 +32,9 @@
    23.4  val nodeOrder_def   = (thm "nodeOrder_def");
    23.5  val next_def   = (thm "next_def");
    23.6  
    23.7 -AddIffs [thm "N_positive", thm"skip"];
    23.8 +AddIffs [thm "N_positive"];
    23.9  
   23.10 -Goalw [stable_def] "stable acts (-(E i) Un (HasTok i))";
   23.11 +Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))";
   23.12  by (rtac constrains_weaken 1);
   23.13  by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
   23.14  by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
   23.15 @@ -70,7 +70,7 @@
   23.16  (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   23.17    Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
   23.18  Goal "[| i<N; j<N |] ==>   \
   23.19 -\     leadsTo acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
   23.20 +\     F : leadsTo (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
   23.21  by (case_tac "i=j" 1);
   23.22  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   23.23  by (rtac (TR7 RS leadsTo_weaken_R) 1);
   23.24 @@ -81,7 +81,7 @@
   23.25  
   23.26  (*Chapter 4 variant, the one actually used below.*)
   23.27  Goal "[| i<N; j<N; i~=j |]    \
   23.28 -\     ==> leadsTo acts (HasTok i) {s. (token s, i) : nodeOrder j}";
   23.29 +\     ==> F : leadsTo (HasTok i) {s. (token s, i) : nodeOrder j}";
   23.30  by (rtac (TR7 RS leadsTo_weaken_R) 1);
   23.31  by (Clarify_tac 1);
   23.32  by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
   23.33 @@ -94,7 +94,7 @@
   23.34  
   23.35  
   23.36  (*Misra's TR9: the token reaches an arbitrary node*)
   23.37 -Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)";
   23.38 +Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)";
   23.39  by (rtac leadsTo_weaken_R 1);
   23.40  by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
   23.41       (wf_nodeOrder RS bounded_induct) 1);
   23.42 @@ -108,7 +108,7 @@
   23.43  qed "leadsTo_j";
   23.44  
   23.45  (*Misra's TR8: a hungry process eventually eats*)
   23.46 -Goal "j<N ==> leadsTo acts ({s. token s < N} Int H j) (E j)";
   23.47 +Goal "j<N ==> F : leadsTo ({s. token s < N} Int H j) (E j)";
   23.48  by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
   23.49  by (rtac TR6 2);
   23.50  by (rtac leadsTo_weaken_R 1);
    24.1 --- a/src/HOL/UNITY/Token.thy	Wed Oct 14 15:47:22 1998 +0200
    24.2 +++ b/src/HOL/UNITY/Token.thy	Thu Oct 15 11:35:07 1998 +0200
    24.3 @@ -36,26 +36,24 @@
    24.4  locale Token =
    24.5    fixes
    24.6      N         :: nat	 (*number of nodes in the ring*)
    24.7 -    acts      :: "(state*state)set set"
    24.8 +    F         :: state program
    24.9      nodeOrder :: "nat => (nat*nat)set"
   24.10      next      :: nat => nat
   24.11  
   24.12    assumes
   24.13      N_positive "0<N"
   24.14  
   24.15 -    skip "Id: acts"
   24.16 +    TR2  "!!i. F : constrains (T i) (T i Un H i)"
   24.17  
   24.18 -    TR2  "!!i. constrains acts (T i) (T i Un H i)"
   24.19 +    TR3  "!!i. F : constrains (H i) (H i Un E i)"
   24.20  
   24.21 -    TR3  "!!i. constrains acts (H i) (H i Un E i)"
   24.22 +    TR4  "!!i. F : constrains (H i - HasTok i) (H i)"
   24.23  
   24.24 -    TR4  "!!i. constrains acts (H i - HasTok i) (H i)"
   24.25 -
   24.26 -    TR5  "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
   24.27 +    TR5  "!!i. F : constrains (HasTok i) (HasTok i Un Compl(E i))"
   24.28  
   24.29 -    TR6  "!!i. leadsTo acts (H i Int HasTok i) (E i)"
   24.30 +    TR6  "!!i. F : leadsTo (H i Int HasTok i) (E i)"
   24.31  
   24.32 -    TR7  "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
   24.33 +    TR7  "!!i. F : leadsTo (HasTok i) (HasTok (next i))"
   24.34  
   24.35    defines
   24.36      nodeOrder_def
    25.1 --- a/src/HOL/UNITY/Traces.ML	Wed Oct 14 15:47:22 1998 +0200
    25.2 +++ b/src/HOL/UNITY/Traces.ML	Thu Oct 15 11:35:07 1998 +0200
    25.3 @@ -43,8 +43,17 @@
    25.4  qed "program_equalityI";
    25.5  
    25.6  
    25.7 -(*** These three rules allow "lazy" definition expansion ***)
    25.8 +(*** These rules allow "lazy" definition expansion ***)
    25.9  
   25.10 +(*The program is not expanded, but its Init is*)
   25.11 +val [rew] = goal thy
   25.12 +    "[| F == mk_program (init,acts) |] \
   25.13 +\    ==> Init F = init";
   25.14 +by (rewtac rew);
   25.15 +by Auto_tac;
   25.16 +qed "def_prg_Init";
   25.17 +
   25.18 +(*The program is not expanded, but its Init and Acts are*)
   25.19  val [rew] = goal thy
   25.20      "[| F == mk_program (init,acts) |] \
   25.21  \    ==> Init F = init & Acts F = insert Id acts";
   25.22 @@ -52,6 +61,7 @@
   25.23  by Auto_tac;
   25.24  qed "def_prg_simps";
   25.25  
   25.26 +(*An action is expanded only if a pair of states is being tested against it*)
   25.27  val [rew] = goal thy
   25.28      "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
   25.29  by (rewtac rew);
   25.30 @@ -60,8 +70,9 @@
   25.31  
   25.32  fun simp_of_act def = def RS def_act_simp;
   25.33  
   25.34 +(*A set is expanded only if an element is being tested against it*)
   25.35  val [rew] = goal thy
   25.36 -    "[| A == B |] ==> (x : A) = (x : B)";
   25.37 +    "A == B ==> (x : A) = (x : B)";
   25.38  by (rewtac rew);
   25.39  by Auto_tac;
   25.40  qed "def_set_simp";
   25.41 @@ -77,11 +88,3 @@
   25.42  by (etac reachable.induct 1);
   25.43  by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
   25.44  qed "reachable_equiv_traces";
   25.45 -
   25.46 -Goal "Init F <= reachable F";
   25.47 -by (blast_tac (claset() addIs reachable.intrs) 1);
   25.48 -qed "Init_subset_reachable";
   25.49 -
   25.50 -Goal "acts <= Acts F ==> stable acts (reachable F)";
   25.51 -by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
   25.52 -qed "stable_reachable";
    26.1 --- a/src/HOL/UNITY/Traces.thy	Wed Oct 14 15:47:22 1998 +0200
    26.2 +++ b/src/HOL/UNITY/Traces.thy	Thu Oct 15 11:35:07 1998 +0200
    26.3 @@ -8,7 +8,7 @@
    26.4    * reachable: the set of reachable states
    26.5  *)
    26.6  
    26.7 -Traces = UNITY +
    26.8 +Traces = LessThan +
    26.9  
   26.10  consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
   26.11  
    27.1 --- a/src/HOL/UNITY/UNITY.ML	Wed Oct 14 15:47:22 1998 +0200
    27.2 +++ b/src/HOL/UNITY/UNITY.ML	Thu Oct 15 11:35:07 1998 +0200
    27.3 @@ -14,154 +14,216 @@
    27.4  
    27.5  (*** constrains ***)
    27.6  
    27.7 -(*Map the type (anything => ('a set => anything) to just 'a*)
    27.8 -fun overload_2nd_set s =
    27.9 -    Blast.overloaded (s, HOLogic.dest_setT o domain_type o range_type);
   27.10 -
   27.11 -overload_2nd_set "UNITY.constrains";
   27.12 -overload_2nd_set "UNITY.stable";
   27.13 -overload_2nd_set "UNITY.unless";
   27.14 +overload_1st_set "UNITY.constrains";
   27.15 +overload_1st_set "UNITY.stable";
   27.16 +overload_1st_set "UNITY.unless";
   27.17  
   27.18  val prems = Goalw [constrains_def]
   27.19 -    "(!!act s s'. [| act: acts;  (s,s') : act;  s: A |] ==> s': A') \
   27.20 -\    ==> constrains acts A A'";
   27.21 +    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
   27.22 +\    ==> F : constrains A A'";
   27.23  by (blast_tac (claset() addIs prems) 1);
   27.24  qed "constrainsI";
   27.25  
   27.26  Goalw [constrains_def]
   27.27 -    "[| constrains acts A A'; act: acts;  (s,s'): act;  s: A |] ==> s': A'";
   27.28 +    "[| F : constrains A A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'";
   27.29  by (Blast_tac 1);
   27.30  qed "constrainsD";
   27.31  
   27.32 -Goalw [constrains_def] "constrains acts {} B";
   27.33 +Goalw [constrains_def] "F : constrains {} B";
   27.34  by (Blast_tac 1);
   27.35  qed "constrains_empty";
   27.36  
   27.37 -Goalw [constrains_def] "constrains acts A UNIV";
   27.38 +Goalw [constrains_def] "F : constrains A UNIV";
   27.39  by (Blast_tac 1);
   27.40  qed "constrains_UNIV";
   27.41  AddIffs [constrains_empty, constrains_UNIV];
   27.42  
   27.43 +(*monotonic in 2nd argument*)
   27.44  Goalw [constrains_def]
   27.45 -    "[| constrains acts A A'; A'<=B' |] ==> constrains acts A B'";
   27.46 +    "[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'";
   27.47  by (Blast_tac 1);
   27.48  qed "constrains_weaken_R";
   27.49  
   27.50 +(*anti-monotonic in 1st argument*)
   27.51  Goalw [constrains_def]
   27.52 -    "[| constrains acts A A'; B<=A |] ==> constrains acts B A'";
   27.53 +    "[| F : constrains A A'; B<=A |] ==> F : constrains B A'";
   27.54  by (Blast_tac 1);
   27.55  qed "constrains_weaken_L";
   27.56  
   27.57  Goalw [constrains_def]
   27.58 -   "[| constrains acts A A'; B<=A; A'<=B' |] ==> constrains acts B B'";
   27.59 +   "[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'";
   27.60  by (Blast_tac 1);
   27.61  qed "constrains_weaken";
   27.62  
   27.63  (** Union **)
   27.64  
   27.65  Goalw [constrains_def]
   27.66 -    "[| constrains acts A A'; constrains acts B B' |]   \
   27.67 -\    ==> constrains acts (A Un B) (A' Un B')";
   27.68 +    "[| F : constrains A A'; F : constrains B B' |]   \
   27.69 +\    ==> F : constrains (A Un B) (A' Un B')";
   27.70  by (Blast_tac 1);
   27.71  qed "constrains_Un";
   27.72  
   27.73  Goalw [constrains_def]
   27.74 -    "ALL i:I. constrains acts (A i) (A' i) \
   27.75 -\    ==> constrains acts (UN i:I. A i) (UN i:I. A' i)";
   27.76 +    "ALL i:I. F : constrains (A i) (A' i) \
   27.77 +\    ==> F : constrains (UN i:I. A i) (UN i:I. A' i)";
   27.78  by (Blast_tac 1);
   27.79  qed "ball_constrains_UN";
   27.80  
   27.81  Goalw [constrains_def]
   27.82 -    "[| ALL i. constrains acts (A i) (A' i) |] \
   27.83 -\    ==> constrains acts (UN i. A i) (UN i. A' i)";
   27.84 +    "[| ALL i. F : constrains (A i) (A' i) |] \
   27.85 +\    ==> F : constrains (UN i. A i) (UN i. A' i)";
   27.86  by (Blast_tac 1);
   27.87  qed "all_constrains_UN";
   27.88  
   27.89  (** Intersection **)
   27.90  
   27.91  Goalw [constrains_def]
   27.92 -    "[| constrains acts A A'; constrains acts B B' |]   \
   27.93 -\    ==> constrains acts (A Int B) (A' Int B')";
   27.94 +    "[| F : constrains A A'; F : constrains B B' |]   \
   27.95 +\    ==> F : constrains (A Int B) (A' Int B')";
   27.96  by (Blast_tac 1);
   27.97  qed "constrains_Int";
   27.98  
   27.99  Goalw [constrains_def]
  27.100 -    "ALL i:I. constrains acts (A i) (A' i) \
  27.101 -\    ==> constrains acts (INT i:I. A i) (INT i:I. A' i)";
  27.102 +    "ALL i:I. F : constrains (A i) (A' i) \
  27.103 +\    ==> F : constrains (INT i:I. A i) (INT i:I. A' i)";
  27.104  by (Blast_tac 1);
  27.105  qed "ball_constrains_INT";
  27.106  
  27.107  Goalw [constrains_def]
  27.108 -    "[| ALL i. constrains acts (A i) (A' i) |] \
  27.109 -\    ==> constrains acts (INT i. A i) (INT i. A' i)";
  27.110 +    "[| ALL i. F : constrains (A i) (A' i) |] \
  27.111 +\    ==> F : constrains (INT i. A i) (INT i. A' i)";
  27.112  by (Blast_tac 1);
  27.113  qed "all_constrains_INT";
  27.114  
  27.115 -Goalw [constrains_def] "[| constrains acts A A'; Id: acts |] ==> A<=A'";
  27.116 +Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'";
  27.117  by (Blast_tac 1);
  27.118  qed "constrains_imp_subset";
  27.119  
  27.120  Goalw [constrains_def]
  27.121 -    "[| Id: acts; constrains acts A B; constrains acts B C |]   \
  27.122 -\    ==> constrains acts A C";
  27.123 +    "[| F : constrains A B; F : constrains B C |]   \
  27.124 +\    ==> F : constrains A C";
  27.125  by (Blast_tac 1);
  27.126  qed "constrains_trans";
  27.127  
  27.128  
  27.129  (*** stable ***)
  27.130  
  27.131 -Goalw [stable_def] "constrains acts A A ==> stable acts A";
  27.132 +Goalw [stable_def] "F : constrains A A ==> F : stable A";
  27.133  by (assume_tac 1);
  27.134  qed "stableI";
  27.135  
  27.136 -Goalw [stable_def] "stable acts A ==> constrains acts A A";
  27.137 +Goalw [stable_def] "F : stable A ==> F : constrains A A";
  27.138  by (assume_tac 1);
  27.139  qed "stableD";
  27.140  
  27.141  Goalw [stable_def]
  27.142 -    "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')";
  27.143 +    "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
  27.144  by (blast_tac (claset() addIs [constrains_Un]) 1);
  27.145  qed "stable_Un";
  27.146  
  27.147  Goalw [stable_def]
  27.148 -    "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')";
  27.149 +    "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
  27.150  by (blast_tac (claset() addIs [constrains_Int]) 1);
  27.151  qed "stable_Int";
  27.152  
  27.153  Goalw [stable_def, constrains_def]
  27.154 -    "[| stable acts C; constrains acts A (C Un A') |]   \
  27.155 -\    ==> constrains acts (C Un A) (C Un A')";
  27.156 +    "[| F : stable C; F : constrains A (C Un A') |]   \
  27.157 +\    ==> F : constrains (C Un A) (C Un A')";
  27.158  by (Blast_tac 1);
  27.159  qed "stable_constrains_Un";
  27.160  
  27.161  Goalw [stable_def, constrains_def]
  27.162 -    "[| stable acts C; constrains acts (C Int A) A' |]   \
  27.163 -\    ==> constrains acts (C Int A) (C Int A')";
  27.164 +    "[| F : stable C; F : constrains (C Int A) A' |]   \
  27.165 +\    ==> F : constrains (C Int A) (C Int A')";
  27.166  by (Blast_tac 1);
  27.167  qed "stable_constrains_Int";
  27.168  
  27.169 +Goal "Init F <= reachable F";
  27.170 +by (blast_tac (claset() addIs reachable.intrs) 1);
  27.171 +qed "Init_subset_reachable";
  27.172  
  27.173 -(*The Elimination Theorem.  The "free" m has become universally quantified!
  27.174 -  Should the premise be !!m instead of ALL m ?  Would make it harder to use
  27.175 -  in forward proof.*)
  27.176 +Goal "Acts G <= Acts F ==> G : stable (reachable F)";
  27.177 +by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
  27.178 +qed "stable_reachable";
  27.179 +
  27.180 +(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
  27.181 +bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
  27.182 +
  27.183 +
  27.184 +(*** invariant & always ***)
  27.185 +
  27.186 +Goal "[| Init F<=A;  F: stable A |] ==> F : invariant A";
  27.187 +by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
  27.188 +qed "invariantI";
  27.189 +
  27.190 +(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
  27.191 +Goal "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)";
  27.192 +by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
  27.193 +qed "invariant_Int";
  27.194 +
  27.195 +(*The set of all reachable states is an invariant...*)
  27.196 +Goal "F : invariant (reachable F)";
  27.197 +by (simp_tac (simpset() addsimps [invariant_def]) 1);
  27.198 +by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
  27.199 +qed "invariant_reachable";
  27.200 +
  27.201 +(*...in fact the strongest invariant!*)
  27.202 +Goal "F : invariant A ==> reachable F <= A";
  27.203 +by (full_simp_tac 
  27.204 +    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
  27.205 +by (rtac subsetI 1);
  27.206 +by (etac reachable.induct 1);
  27.207 +by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
  27.208 +qed "invariant_includes_reachable";
  27.209 +
  27.210 +Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
  27.211 +by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
  27.212 +                               stable_reachable,
  27.213 +			       impOfSubs invariant_includes_reachable]) 1);
  27.214 +qed "always_eq_UN_invariant";
  27.215 +
  27.216 +Goal "F : always A = (EX I. F: invariant I & I <= A)";
  27.217 +by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
  27.218 +by (Blast_tac 1);
  27.219 +qed "always_iff_ex_invariant";
  27.220 +
  27.221 +
  27.222 +(*** increasing ***)
  27.223 +
  27.224 +Goalw [increasing_def, stable_def, constrains_def]
  27.225 +     "increasing f <= increasing (length o f)";
  27.226 +by Auto_tac;
  27.227 +by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
  27.228 +qed "increasing_length";
  27.229 +
  27.230 +Goalw [increasing_def]
  27.231 +     "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
  27.232 +by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
  27.233 +by (Blast_tac 1);
  27.234 +qed "increasing_less";
  27.235 +
  27.236 +
  27.237 +(** The Elimination Theorem.  The "free" m has become universally quantified!
  27.238 +    Should the premise be !!m instead of ALL m ?  Would make it harder to use
  27.239 +    in forward proof. **)
  27.240 +
  27.241  Goalw [constrains_def]
  27.242 -    "[| ALL m. constrains acts {s. s x = m} (B m) |] \
  27.243 -\    ==> constrains acts {s. s x : M} (UN m:M. B m)";
  27.244 +    "[| ALL m. F : constrains {s. s x = m} (B m) |] \
  27.245 +\    ==> F : constrains {s. s x : M} (UN m:M. B m)";
  27.246  by (Blast_tac 1);
  27.247  qed "elimination";
  27.248  
  27.249 -
  27.250  (*As above, but for the trivial case of a one-variable state, in which the
  27.251    state is identified with its one variable.*)
  27.252  Goalw [constrains_def]
  27.253 -    "(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)";
  27.254 +    "(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)";
  27.255  by (Blast_tac 1);
  27.256  qed "elimination_sing";
  27.257  
  27.258  
  27.259  Goalw [constrains_def]
  27.260 -   "[| constrains acts A (A' Un B); constrains acts B B'; Id: acts |] \
  27.261 -\   ==> constrains acts A (A' Un B')";
  27.262 +   "[| F : constrains A (A' Un B); F : constrains B B' |] \
  27.263 +\   ==> F : constrains A (A' Un B')";
  27.264  by (Blast_tac 1);
  27.265  qed "constrains_cancel";
  27.266  
  27.267 @@ -170,11 +232,11 @@
  27.268  (*** Theoretical Results from Section 6 ***)
  27.269  
  27.270  Goalw [constrains_def, strongest_rhs_def]
  27.271 -    "constrains acts A (strongest_rhs acts A )";
  27.272 +    "F : constrains A (strongest_rhs F A )";
  27.273  by (Blast_tac 1);
  27.274  qed "constrains_strongest_rhs";
  27.275  
  27.276  Goalw [constrains_def, strongest_rhs_def]
  27.277 -    "constrains acts A B ==> strongest_rhs acts A <= B";
  27.278 +    "F : constrains A B ==> strongest_rhs F A <= B";
  27.279  by (Blast_tac 1);
  27.280  qed "strongest_rhs_is_strongest";
    28.1 --- a/src/HOL/UNITY/UNITY.thy	Wed Oct 14 15:47:22 1998 +0200
    28.2 +++ b/src/HOL/UNITY/UNITY.thy	Thu Oct 15 11:35:07 1998 +0200
    28.3 @@ -8,20 +8,33 @@
    28.4  From Misra, "A Logic for Concurrent Programming", 1994
    28.5  *)
    28.6  
    28.7 -UNITY = LessThan +
    28.8 +UNITY = Traces + Prefix +
    28.9  
   28.10  constdefs
   28.11  
   28.12 -  constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   28.13 -    "constrains acts A B == ALL act:acts. act^^A <= B"
   28.14 +  constrains :: "['a set, 'a set] => 'a program set"
   28.15 +    "constrains A B == {F. ALL act: Acts F. act^^A <= B}"
   28.16 +
   28.17 +  stable     :: "'a set => 'a program set"
   28.18 +    "stable A == constrains A A"
   28.19  
   28.20 -  stable     :: "('a * 'a)set set => 'a set => bool"
   28.21 -    "stable acts A == constrains acts A A"
   28.22 +  strongest_rhs :: "['a program, 'a set] => 'a set"
   28.23 +    "strongest_rhs F A == Inter {B. F : constrains A B}"
   28.24 +
   28.25 +  unless :: "['a set, 'a set] => 'a program set"
   28.26 +    "unless A B == constrains (A-B) (A Un B)"
   28.27  
   28.28 -  strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"
   28.29 -    "strongest_rhs acts A == Inter {B. constrains acts A B}"
   28.30 +  (*The traditional word for inductive properties.  Anyway, INDUCTIVE is
   28.31 +    reserved!*)
   28.32 +  invariant :: "'a set => 'a program set"
   28.33 +    "invariant A == {F. Init F <= A} Int stable A"
   28.34  
   28.35 -  unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   28.36 -    "unless acts A B == constrains acts (A-B) (A Un B)"
   28.37 +  (*Safety properties*)
   28.38 +  always :: "'a set => 'a program set"
   28.39 +    "always A == {F. reachable F <= A}"
   28.40 +
   28.41 +  (*Polymorphic in both states and the meaning of <= *)
   28.42 +  increasing :: "['a => 'b::{ord}] => 'a program set"
   28.43 +    "increasing f == INT z. stable {s. z <= f s}"
   28.44  
   28.45  end
    29.1 --- a/src/HOL/UNITY/Union.ML	Wed Oct 14 15:47:22 1998 +0200
    29.2 +++ b/src/HOL/UNITY/Union.ML	Thu Oct 15 11:35:07 1998 +0200
    29.3 @@ -9,10 +9,16 @@
    29.4  *)
    29.5  
    29.6  
    29.7 -Goal "Init (F Join G) = Init F Int Init G";
    29.8 -by (simp_tac (simpset() addsimps [Join_def]) 1);
    29.9 +Goal "Init SKIP = UNIV";
   29.10 +by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   29.11  qed "Init_SKIP";
   29.12  
   29.13 +Goal "Acts SKIP = {Id}";
   29.14 +by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   29.15 +qed "Acts_SKIP";
   29.16 +
   29.17 +Addsimps [Init_SKIP, Acts_SKIP];
   29.18 +
   29.19  Goal "Init (F Join G) = Init F Int Init G";
   29.20  by (simp_tac (simpset() addsimps [Join_def]) 1);
   29.21  qed "Init_Join";
   29.22 @@ -79,14 +85,13 @@
   29.23  
   29.24  Goalw [constrains_def, JOIN_def]
   29.25      "I ~= {} ==> \
   29.26 -\    constrains (Acts (JN i:I. F i)) A B = \
   29.27 -\    (ALL i:I. constrains (Acts (F i)) A B)";
   29.28 +\    (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
   29.29  by (Simp_tac 1);
   29.30  by (Blast_tac 1);
   29.31  qed "constrains_JN";
   29.32  
   29.33 -Goal "constrains (Acts (F Join G)) A B =  \
   29.34 -\     (constrains (Acts F) A B & constrains (Acts G) A B)";
   29.35 +Goal "F Join G : constrains A B =  \
   29.36 +\     (F : constrains A B & G : constrains A B)";
   29.37  by (auto_tac
   29.38      (claset(),
   29.39       simpset() addsimps [constrains_def, Join_def]));
   29.40 @@ -97,35 +102,35 @@
   29.41     reachable F and reachable G
   29.42  
   29.43  Goalw [Constrains_def]
   29.44 -    "Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)";
   29.45 +    "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)";
   29.46  by (simp_tac (simpset() addsimps [constrains_JN]) 1);
   29.47  by (Blast_tac 1);
   29.48  qed "Constrains_JN";
   29.49  
   29.50 -Goal "Constrains (F Join G) A B = (Constrains F A B & Constrains G A B)";
   29.51 +Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)";
   29.52  by (auto_tac
   29.53      (claset(),
   29.54       simpset() addsimps [Constrains_def, constrains_Join]));
   29.55  qed "Constrains_Join";
   29.56  **)
   29.57  
   29.58 -Goal "[| constrains (Acts F) A A';  constrains (Acts G) B B' |] \
   29.59 -\     ==> constrains (Acts (F Join G)) (A Int B) (A' Un B')";
   29.60 +Goal "[| F : constrains A A';  G : constrains B B' |] \
   29.61 +\     ==> F Join G : constrains (A Int B) (A' Un B')";
   29.62  by (simp_tac (simpset() addsimps [constrains_Join]) 1);
   29.63  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   29.64  qed "constrains_Join_weaken";
   29.65  
   29.66  Goal "I ~= {} ==> \
   29.67 -\     stable (Acts (JN i:I. F i)) A = (ALL i:I. stable (Acts (F i)) A)";
   29.68 +\     (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
   29.69  by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
   29.70  qed "stable_JN";
   29.71  
   29.72 -Goal "stable (Acts (F Join G)) A = \
   29.73 -\     (stable (Acts F) A & stable (Acts G) A)";
   29.74 +Goal "F Join G : stable A = \
   29.75 +\     (F : stable A & G : stable A)";
   29.76  by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
   29.77  qed "stable_Join";
   29.78  
   29.79 -Goal "I ~= {} ==> FP (Acts (JN i:I. F i)) = (INT i:I. FP (Acts (F i)))";
   29.80 +Goal "I ~= {} ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
   29.81  by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
   29.82  qed "FP_JN";
   29.83  
   29.84 @@ -133,54 +138,52 @@
   29.85  (*** Progress: transient, ensures ***)
   29.86  
   29.87  Goal "I ~= {} ==> \
   29.88 -\   transient (Acts (JN i:I. F i)) A = (EX i:I. transient (Acts (F i)) A)";
   29.89 +\   (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
   29.90  by (auto_tac (claset(),
   29.91  	      simpset() addsimps [transient_def, JOIN_def]));
   29.92  qed "transient_JN";
   29.93  
   29.94 -Goal "transient (Acts (F Join G)) A = \
   29.95 -\     (transient (Acts F) A | transient (Acts G) A)";
   29.96 +Goal "F Join G : transient A = \
   29.97 +\     (F : transient A | G : transient A)";
   29.98  by (auto_tac (claset(),
   29.99  	      simpset() addsimps [bex_Un, transient_def,
  29.100  				  Join_def]));
  29.101  qed "transient_Join";
  29.102  
  29.103  Goal "I ~= {} ==> \
  29.104 -\     ensures (Acts (JN i:I. F i)) A B = \
  29.105 -\     ((ALL i:I. constrains (Acts (F i)) (A-B) (A Un B)) & \
  29.106 -\      (EX i:I. ensures (Acts (F i)) A B))";
  29.107 +\     (JN i:I. F i) : ensures A B = \
  29.108 +\     ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
  29.109 +\      (EX i:I. F i : ensures A B))";
  29.110  by (auto_tac (claset(),
  29.111  	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
  29.112  qed "ensures_JN";
  29.113  
  29.114  Goalw [ensures_def]
  29.115 -     "ensures (Acts (F Join G)) A B =     \
  29.116 -\     (constrains (Acts F) (A-B) (A Un B) & \
  29.117 -\      constrains (Acts G) (A-B) (A Un B) & \
  29.118 -\      (ensures (Acts F) A B | ensures (Acts G) A B))";
  29.119 +     "F Join G : ensures A B =     \
  29.120 +\     (F : constrains (A-B) (A Un B) & \
  29.121 +\      G : constrains (A-B) (A Un B) & \
  29.122 +\      (F : ensures A B | G : ensures A B))";
  29.123  by (auto_tac (claset(),
  29.124  	      simpset() addsimps [constrains_Join, transient_Join]));
  29.125  qed "ensures_Join";
  29.126  
  29.127  Goalw [stable_def, constrains_def, Join_def]
  29.128 -    "[| stable (Acts F) A;  constrains (Acts G) A A' |] \
  29.129 -\    ==> constrains (Acts (F Join G)) A A'";
  29.130 -by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
  29.131 +    "[| F : stable A;  G : constrains A A' |] \
  29.132 +\    ==> F Join G : constrains A A'";
  29.133 +by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
  29.134  by (Blast_tac 1);
  29.135  qed "stable_constrains_Join";
  29.136  
  29.137 -(*Premises cannot use Invariant because  Stable F A  is weaker than
  29.138 -  stable (Acts G) A *)
  29.139 -Goal "[| stable (Acts F) A;  Init G <= A;  stable (Acts G) A |] \
  29.140 -\     ==> Invariant (F Join G) A";
  29.141 -by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
  29.142 -				  stable_Join]) 1);
  29.143 +(*Premise for G cannot use Invariant because  Stable F A  is weaker than
  29.144 +  G : stable A *)
  29.145 +Goal "[| F : stable A;  G : invariant A |] ==> F Join G : Invariant A";
  29.146 +by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, 
  29.147 +				       Stable_eq_stable, stable_Join]) 1);
  29.148  by (force_tac(claset() addIs [stable_reachable, stable_Int],
  29.149  	      simpset() addsimps [Acts_Join]) 1);
  29.150  qed "stable_Join_Invariant";
  29.151  
  29.152 -Goal "[| stable (Acts F) A;  ensures (Acts G) A B |]     \
  29.153 -\     ==> ensures (Acts (F Join G)) A B";
  29.154 +Goal "[| F : stable A;  G : ensures A B |] ==> F Join G : ensures A B";
  29.155  by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
  29.156  by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
  29.157  by (etac constrains_weaken 1);
  29.158 @@ -188,9 +191,18 @@
  29.159  qed "ensures_stable_Join1";
  29.160  
  29.161  (*As above, but exchanging the roles of F and G*)
  29.162 -Goal "[| ensures (Acts F) A B;  stable (Acts G) A |]     \
  29.163 -\     ==> ensures (Acts (F Join G)) A B";
  29.164 +Goal "[| F : ensures A B;  G : stable A |] ==> F Join G : ensures A B";
  29.165  by (stac Join_commute 1);
  29.166  by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
  29.167  qed "ensures_stable_Join2";
  29.168  
  29.169 +
  29.170 +(** localTo **)
  29.171 +
  29.172 +Goal "[| F Join G : f localTo F;  (s,s') : act;  \
  29.173 +\        act : Acts G; act ~: Acts F |] ==> f s' = f s";
  29.174 +by (asm_full_simp_tac 
  29.175 +    (simpset() addsimps [localTo_def, Diff_def, Acts_Join, stable_def, 
  29.176 +			 constrains_def]) 1);
  29.177 +by (Blast_tac 1);
  29.178 +qed "localTo_imp_equals";
    30.1 --- a/src/HOL/UNITY/Union.thy	Wed Oct 14 15:47:22 1998 +0200
    30.2 +++ b/src/HOL/UNITY/Union.thy	Thu Oct 15 11:35:07 1998 +0200
    30.3 @@ -11,15 +11,22 @@
    30.4  Union = SubstAx + FP +
    30.5  
    30.6  constdefs
    30.7 -   JOIN  :: ['a set, 'a => 'b program] => 'b program
    30.8 +  JOIN  :: ['a set, 'a => 'b program] => 'b program
    30.9      "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
   30.10  
   30.11 -   Join :: ['a program, 'a program] => 'a program      (infixl 65)
   30.12 +  Join :: ['a program, 'a program] => 'a program      (infixl 65)
   30.13      "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
   30.14  
   30.15 -   SKIP :: 'a program
   30.16 +  SKIP :: 'a program
   30.17      "SKIP == mk_program (UNIV, {})"
   30.18  
   30.19 +  Diff :: "['a program, ('a * 'a)set set] => 'a program"
   30.20 +    "Diff F acts == mk_program (Init F, Acts F - acts)"
   30.21 +
   30.22 +  (*The set of systems that regard "f" as local to F*)
   30.23 +  localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
   30.24 +    "f localTo F == {G. ALL z. Diff G (Acts F) : stable {s. f s = z}}"
   30.25 +
   30.26  syntax
   30.27    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
   30.28  
    31.1 --- a/src/HOL/UNITY/WFair.ML	Wed Oct 14 15:47:22 1998 +0200
    31.2 +++ b/src/HOL/UNITY/WFair.ML	Thu Oct 15 11:35:07 1998 +0200
    31.3 @@ -9,30 +9,26 @@
    31.4  *)
    31.5  
    31.6  
    31.7 -(*Map its type, [('a * 'a)set set] => ('a set * 'a set) set, to just 'a*)
    31.8 -Blast.overloaded ("WFair.leadsto", 
    31.9 -		  #1 o HOLogic.dest_prodT o 
   31.10 -		  HOLogic.dest_setT o HOLogic.dest_setT o domain_type);
   31.11 -
   31.12 -overload_2nd_set "WFair.transient";
   31.13 -overload_2nd_set "WFair.ensures";
   31.14 +overload_1st_set "WFair.transient";
   31.15 +overload_1st_set "WFair.ensures";
   31.16 +overload_1st_set "WFair.leadsTo";
   31.17  
   31.18  (*** transient ***)
   31.19  
   31.20  Goalw [stable_def, constrains_def, transient_def]
   31.21 -    "[| stable acts A; transient acts A |] ==> A = {}";
   31.22 +    "[| F : stable A; F : transient A |] ==> A = {}";
   31.23  by (Blast_tac 1);
   31.24  qed "stable_transient_empty";
   31.25  
   31.26  Goalw [transient_def]
   31.27 -    "[| transient acts A; B<=A |] ==> transient acts B";
   31.28 +    "[| F : transient A; B<=A |] ==> F : transient B";
   31.29  by (Clarify_tac 1);
   31.30  by (rtac bexI 1 THEN assume_tac 2);
   31.31  by (Blast_tac 1);
   31.32  qed "transient_strengthen";
   31.33  
   31.34  Goalw [transient_def]
   31.35 -    "[| act:acts;  A <= Domain act;  act^^A <= -A |] ==> transient acts A";
   31.36 +    "[| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> F : transient A";
   31.37  by (Blast_tac 1);
   31.38  qed "transient_mem";
   31.39  
   31.40 @@ -40,40 +36,38 @@
   31.41  (*** ensures ***)
   31.42  
   31.43  Goalw [ensures_def]
   31.44 -    "[| constrains acts (A-B) (A Un B); transient acts (A-B) |] \
   31.45 -\    ==> ensures acts A B";
   31.46 +    "[| F : constrains (A-B) (A Un B); F : transient (A-B) |] \
   31.47 +\    ==> F : ensures A B";
   31.48  by (Blast_tac 1);
   31.49  qed "ensuresI";
   31.50  
   31.51  Goalw [ensures_def]
   31.52 -    "ensures acts A B  \
   31.53 -\    ==> constrains acts (A-B) (A Un B) & transient acts (A-B)";
   31.54 +    "F : ensures A B ==> F : constrains (A-B) (A Un B) & F : transient (A-B)";
   31.55  by (Blast_tac 1);
   31.56  qed "ensuresD";
   31.57  
   31.58  (*The L-version (precondition strengthening) doesn't hold for ENSURES*)
   31.59  Goalw [ensures_def]
   31.60 -    "[| ensures acts A A'; A'<=B' |] ==> ensures acts A B'";
   31.61 +    "[| F : ensures A A'; A'<=B' |] ==> F : ensures A B'";
   31.62  by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   31.63  qed "ensures_weaken_R";
   31.64  
   31.65  Goalw [ensures_def, constrains_def, transient_def]
   31.66 -    "acts ~= {} ==> ensures acts A UNIV";
   31.67 +    "Acts F ~= {} ==> F : ensures A UNIV";
   31.68  by Auto_tac;
   31.69  qed "ensures_UNIV";
   31.70  
   31.71  Goalw [ensures_def]
   31.72 -    "[| stable acts C; \
   31.73 -\       constrains acts (C Int (A - A')) (A Un A'); \
   31.74 -\       transient  acts (C Int (A-A')) |]   \
   31.75 -\   ==> ensures acts (C Int A) (C Int A')";
   31.76 +    "[| F : stable C; \
   31.77 +\       F : constrains (C Int (A - A')) (A Un A'); \
   31.78 +\       F : transient (C Int (A-A')) |]   \
   31.79 +\   ==> F : ensures (C Int A) (C Int A')";
   31.80  by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
   31.81  				      Diff_Int_distrib RS sym,
   31.82  				      stable_constrains_Int]) 1);
   31.83  qed "stable_ensures_Int";
   31.84  
   31.85 -Goal "[| stable acts A;  transient acts C;  A <= B Un C |] \
   31.86 -\     ==> ensures acts A B";
   31.87 +Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : ensures A B";
   31.88  by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
   31.89  by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   31.90  qed "stable_transient_ensures";
   31.91 @@ -81,62 +75,67 @@
   31.92  
   31.93  (*** leadsTo ***)
   31.94  
   31.95 -(*Synonyms for the theorems produced by the inductive defn package*)
   31.96 -bind_thm ("leadsTo_Basis", leadsto.Basis);
   31.97 -bind_thm ("leadsTo_Trans", leadsto.Trans);
   31.98 +Goalw [leadsTo_def] "F : ensures A B ==> F : leadsTo A B";
   31.99 +by (blast_tac (claset() addIs [leadsto.Basis]) 1);
  31.100 +qed "leadsTo_Basis";
  31.101  
  31.102 -Goal "transient acts A ==> leadsTo acts A (-A)";
  31.103 +Goalw [leadsTo_def]
  31.104 +     "[| F : leadsTo A B;  F : leadsTo B C |] ==> F : leadsTo A C";
  31.105 +by (blast_tac (claset() addIs [leadsto.Trans]) 1);
  31.106 +qed "leadsTo_Trans";
  31.107 +
  31.108 +Goal "F : transient A ==> F : leadsTo A (-A)";
  31.109  by (asm_simp_tac 
  31.110      (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
  31.111  qed "transient_imp_leadsTo";
  31.112  
  31.113 -Goal "act: acts ==> leadsTo acts A UNIV";
  31.114 +Goal "F : leadsTo A UNIV";
  31.115  by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
  31.116  qed "leadsTo_UNIV";
  31.117  Addsimps [leadsTo_UNIV];
  31.118  
  31.119  (*Useful with cancellation, disjunction*)
  31.120 -Goal "leadsTo acts A (A' Un A') ==> leadsTo acts A A'";
  31.121 +Goal "F : leadsTo A (A' Un A') ==> F : leadsTo A A'";
  31.122  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
  31.123  qed "leadsTo_Un_duplicate";
  31.124  
  31.125 -Goal "leadsTo acts A (A' Un C Un C) ==> leadsTo acts A (A' Un C)";
  31.126 +Goal "F : leadsTo A (A' Un C Un C) ==> F : leadsTo A (A' Un C)";
  31.127  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
  31.128  qed "leadsTo_Un_duplicate2";
  31.129  
  31.130  (*The Union introduction rule as we should have liked to state it*)
  31.131 -val prems = goal thy
  31.132 -    "(!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B";
  31.133 -by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
  31.134 +val prems = Goalw [leadsTo_def]
  31.135 +    "(!!A. A : S ==> F : leadsTo A B) ==> F : leadsTo (Union S) B";
  31.136 +by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
  31.137  qed "leadsTo_Union";
  31.138  
  31.139 -val prems = goal thy
  31.140 -    "(!!i. i : I ==> leadsTo acts (A i) B) ==> leadsTo acts (UN i:I. A i) B";
  31.141 +val prems = Goal
  31.142 +    "(!!i. i : I ==> F : leadsTo (A i) B) ==> F : leadsTo (UN i:I. A i) B";
  31.143  by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
  31.144 -by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
  31.145 +by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
  31.146  qed "leadsTo_UN";
  31.147  
  31.148  (*Binary union introduction rule*)
  31.149 -Goal "[| leadsTo acts A C; leadsTo acts B C |] ==> leadsTo acts (A Un B) C";
  31.150 +Goal "[| F : leadsTo A C; F : leadsTo B C |] ==> F : leadsTo (A Un B) C";
  31.151  by (stac Un_eq_Union 1);
  31.152  by (blast_tac (claset() addIs [leadsTo_Union]) 1);
  31.153  qed "leadsTo_Un";
  31.154  
  31.155  
  31.156  (*The INDUCTION rule as we should have liked to state it*)
  31.157 -val major::prems = goal thy
  31.158 -  "[| leadsTo acts za zb;  \
  31.159 -\     !!A B. ensures acts A B ==> P A B; \
  31.160 -\     !!A B C. [| leadsTo acts A B; P A B; leadsTo acts B C; P B C |] \
  31.161 +val major::prems = Goalw [leadsTo_def]
  31.162 +  "[| F : leadsTo za zb;  \
  31.163 +\     !!A B. F : ensures A B ==> P A B; \
  31.164 +\     !!A B C. [| F : leadsTo A B; P A B; F : leadsTo B C; P B C |] \
  31.165  \              ==> P A C; \
  31.166 -\     !!B S. ALL A:S. leadsTo acts A B & P A B ==> P (Union S) B \
  31.167 +\     !!B S. ALL A:S. F : leadsTo A B & P A B ==> P (Union S) B \
  31.168  \  |] ==> P za zb";
  31.169 -by (rtac (major RS leadsto.induct) 1);
  31.170 +by (rtac (major RS CollectD RS leadsto.induct) 1);
  31.171  by (REPEAT (blast_tac (claset() addIs prems) 1));
  31.172  qed "leadsTo_induct";
  31.173  
  31.174  
  31.175 -Goal "[| A<=B;  Id: acts |] ==> leadsTo acts A B";
  31.176 +Goal "A<=B ==> F : leadsTo A B";
  31.177  by (rtac leadsTo_Basis 1);
  31.178  by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
  31.179  by (Blast_tac 1);
  31.180 @@ -146,50 +145,38 @@
  31.181  Addsimps [empty_leadsTo];
  31.182  
  31.183  
  31.184 -(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
  31.185 -  needs the extra premise Id:acts*)
  31.186 -Goal "leadsTo acts A A' ==> A'<=B' --> leadsTo acts A B'";
  31.187 -by (etac leadsTo_induct 1);
  31.188 -by (Clarify_tac 3);
  31.189 -by (blast_tac (claset() addIs [leadsTo_Union]) 3);
  31.190 -by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
  31.191 -by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1);
  31.192 -qed_spec_mp "leadsTo_weaken_R";
  31.193 +Goal "[| F : leadsTo A A'; A'<=B' |] ==> F : leadsTo A B'";
  31.194 +by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
  31.195 +qed "leadsTo_weaken_R";
  31.196  
  31.197  
  31.198 -Goal "[| leadsTo acts A A'; B<=A; Id: acts |] ==>  \
  31.199 -\         leadsTo acts B A'";
  31.200 +Goal "[| F : leadsTo A A'; B<=A |] ==> F : leadsTo B A'";
  31.201  by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
  31.202  			       subset_imp_leadsTo]) 1);
  31.203  qed_spec_mp "leadsTo_weaken_L";
  31.204  
  31.205  (*Distributes over binary unions*)
  31.206 -Goal "Id: acts ==> \
  31.207 -\       leadsTo acts (A Un B) C  =  (leadsTo acts A C & leadsTo acts B C)";
  31.208 +Goal "F : leadsTo (A Un B) C  =  (F : leadsTo A C & F : leadsTo B C)";
  31.209  by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
  31.210  qed "leadsTo_Un_distrib";
  31.211  
  31.212 -Goal "Id: acts ==> \
  31.213 -\       leadsTo acts (UN i:I. A i) B  =  (ALL i : I. leadsTo acts (A i) B)";
  31.214 +Goal "F : leadsTo (UN i:I. A i) B  =  (ALL i : I. F : leadsTo (A i) B)";
  31.215  by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
  31.216  qed "leadsTo_UN_distrib";
  31.217  
  31.218 -Goal "Id: acts ==> \
  31.219 -\       leadsTo acts (Union S) B  =  (ALL A : S. leadsTo acts A B)";
  31.220 +Goal "F : leadsTo (Union S) B  =  (ALL A : S. F : leadsTo A B)";
  31.221  by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
  31.222  qed "leadsTo_Union_distrib";
  31.223  
  31.224  
  31.225 -Goal "[| leadsTo acts A A'; Id: acts; B<=A; A'<=B' |] \
  31.226 -\   ==> leadsTo acts B B'";
  31.227 +Goal "[| F : leadsTo A A'; B<=A; A'<=B' |] ==> F : leadsTo B B'";
  31.228  by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
  31.229  			       leadsTo_Trans]) 1);
  31.230  qed "leadsTo_weaken";
  31.231  
  31.232  
  31.233  (*Set difference: maybe combine with leadsTo_weaken_L??*)
  31.234 -Goal "[| leadsTo acts (A-B) C; leadsTo acts B C; Id: acts |] \
  31.235 -\       ==> leadsTo acts A C";
  31.236 +Goal "[| F : leadsTo (A-B) C; F : leadsTo B C |]   ==> F : leadsTo A C";
  31.237  by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
  31.238  qed "leadsTo_Diff";
  31.239  
  31.240 @@ -198,8 +185,8 @@
  31.241      see ball_constrains_UN in UNITY.ML***)
  31.242  
  31.243  val prems = goal thy
  31.244 -   "(!! i. i:I ==> leadsTo acts (A i) (A' i)) \
  31.245 -\   ==> leadsTo acts (UN i:I. A i) (UN i:I. A' i)";
  31.246 +   "(!! i. i:I ==> F : leadsTo (A i) (A' i)) \
  31.247 +\   ==> F : leadsTo (UN i:I. A i) (UN i:I. A' i)";
  31.248  by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
  31.249  by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
  31.250                          addIs prems) 1);
  31.251 @@ -208,22 +195,21 @@
  31.252  
  31.253  (*Version with no index set*)
  31.254  val prems = goal thy
  31.255 -   "(!! i. leadsTo acts (A i) (A' i)) \
  31.256 -\   ==> leadsTo acts (UN i. A i) (UN i. A' i)";
  31.257 +   "(!! i. F : leadsTo (A i) (A' i)) \
  31.258 +\   ==> F : leadsTo (UN i. A i) (UN i. A' i)";
  31.259  by (blast_tac (claset() addIs [leadsTo_UN_UN] 
  31.260                          addIs prems) 1);
  31.261  qed "leadsTo_UN_UN_noindex";
  31.262  
  31.263  (*Version with no index set*)
  31.264 -Goal "ALL i. leadsTo acts (A i) (A' i) \
  31.265 -\   ==> leadsTo acts (UN i. A i) (UN i. A' i)";
  31.266 +Goal "ALL i. F : leadsTo (A i) (A' i) \
  31.267 +\   ==> F : leadsTo (UN i. A i) (UN i. A' i)";
  31.268  by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
  31.269  qed "all_leadsTo_UN_UN";
  31.270  
  31.271  
  31.272  (*Binary union version*)
  31.273 -Goal "[| leadsTo acts A A'; leadsTo acts B B' |] \
  31.274 -\         ==> leadsTo acts (A Un B) (A' Un B')";
  31.275 +Goal "[| F : leadsTo A A'; F : leadsTo B B' |]     ==> F : leadsTo (A Un B) (A' Un B')";
  31.276  by (blast_tac (claset() addIs [leadsTo_Un, 
  31.277  			       leadsTo_weaken_R]) 1);
  31.278  qed "leadsTo_Un_Un";
  31.279 @@ -231,27 +217,27 @@
  31.280  
  31.281  (** The cancellation law **)
  31.282  
  31.283 -Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; Id: acts |] \
  31.284 -\   ==> leadsTo acts A (A' Un B')";
  31.285 +Goal "[| F : leadsTo A (A' Un B); F : leadsTo B B' |] \
  31.286 +\   ==> F : leadsTo A (A' Un B')";
  31.287  by (blast_tac (claset() addIs [leadsTo_Un_Un, 
  31.288  			       subset_imp_leadsTo, leadsTo_Trans]) 1);
  31.289  qed "leadsTo_cancel2";
  31.290  
  31.291 -Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; Id: acts |] \
  31.292 -\   ==> leadsTo acts A (A' Un B')";
  31.293 +Goal "[| F : leadsTo A (A' Un B); F : leadsTo (B-A') B' |] \
  31.294 +\   ==> F : leadsTo A (A' Un B')";
  31.295  by (rtac leadsTo_cancel2 1);
  31.296  by (assume_tac 2);
  31.297  by (ALLGOALS Asm_simp_tac);
  31.298  qed "leadsTo_cancel_Diff2";
  31.299  
  31.300 -Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; Id: acts |] \
  31.301 -\   ==> leadsTo acts A (B' Un A')";
  31.302 +Goal "[| F : leadsTo A (B Un A'); F : leadsTo B B' |] \
  31.303 +\   ==> F : leadsTo A (B' Un A')";
  31.304  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
  31.305  by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
  31.306  qed "leadsTo_cancel1";
  31.307  
  31.308 -Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; Id: acts |] \
  31.309 -\   ==> leadsTo acts A (B' Un A')";
  31.310 +Goal "[| F : leadsTo A (B Un A'); F : leadsTo (B-A') B' |] \
  31.311 +\   ==> F : leadsTo A (B' Un A')";
  31.312  by (rtac leadsTo_cancel1 1);
  31.313  by (assume_tac 2);
  31.314  by (ALLGOALS Asm_simp_tac);
  31.315 @@ -261,14 +247,14 @@
  31.316  
  31.317  (** The impossibility law **)
  31.318  
  31.319 -Goal "leadsTo acts A B ==> B={} --> A={}";
  31.320 +Goal "F : leadsTo A B ==> B={} --> A={}";
  31.321  by (etac leadsTo_induct 1);
  31.322  by (ALLGOALS Asm_simp_tac);
  31.323  by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
  31.324  by (Blast_tac 1);
  31.325  val lemma = result() RS mp;
  31.326  
  31.327 -Goal "leadsTo acts A {} ==> A={}";
  31.328 +Goal "F : leadsTo A {} ==> A={}";
  31.329  by (blast_tac (claset() addSIs [lemma]) 1);
  31.330  qed "leadsTo_empty";
  31.331  
  31.332 @@ -277,8 +263,8 @@
  31.333  
  31.334  (*Special case of PSP: Misra's "stable conjunction"*)
  31.335  Goalw [stable_def]
  31.336 -   "[| leadsTo acts A A'; stable acts B |] \
  31.337 -\   ==> leadsTo acts (A Int B) (A' Int B)";
  31.338 +   "[| F : leadsTo A A'; F : stable B |] \
  31.339 +\   ==> F : leadsTo (A Int B) (A' Int B)";
  31.340  by (etac leadsTo_induct 1);
  31.341  by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
  31.342  by (blast_tac (claset() addIs [leadsTo_Union]) 3);
  31.343 @@ -290,47 +276,45 @@
  31.344  by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
  31.345  qed "psp_stable";
  31.346  
  31.347 -Goal "[| leadsTo acts A A'; stable acts B |] \
  31.348 -\   ==> leadsTo acts (B Int A) (B Int A')";
  31.349 +Goal "[| F : leadsTo A A'; F : stable B |] \
  31.350 +\   ==> F : leadsTo (B Int A) (B Int A')";
  31.351  by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
  31.352  qed "psp_stable2";
  31.353  
  31.354  Goalw [ensures_def, constrains_def]
  31.355 -   "[| ensures acts A A'; constrains acts B B' |] \
  31.356 -\   ==> ensures acts (A Int B) ((A' Int B) Un (B' - B))";
  31.357 +   "[| F : ensures A A'; F : constrains B B' |] \
  31.358 +\   ==> F : ensures (A Int B) ((A' Int B) Un (B' - B))";
  31.359  by (blast_tac (claset() addIs [transient_strengthen]) 1);
  31.360  qed "psp_ensures";
  31.361  
  31.362 -Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
  31.363 -\           ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))";
  31.364 +Goal "[| F : leadsTo A A'; F : constrains B B' |] \
  31.365 +\     ==> F : leadsTo (A Int B) ((A' Int B) Un (B' - B))";
  31.366  by (etac leadsTo_induct 1);
  31.367  by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
  31.368  by (blast_tac (claset() addIs [leadsTo_Union]) 3);
  31.369  (*Transitivity case has a delicate argument involving "cancellation"*)
  31.370  by (rtac leadsTo_Un_duplicate2 2);
  31.371  by (etac leadsTo_cancel_Diff1 2);
  31.372 -by (assume_tac 3);
  31.373  by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
  31.374  (*Basis case*)
  31.375  by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
  31.376  qed "psp";
  31.377  
  31.378 -Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
  31.379 -\   ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
  31.380 +Goal "[| F : leadsTo A A'; F : constrains B B' |] \
  31.381 +\   ==> F : leadsTo (B Int A) ((B Int A') Un (B' - B))";
  31.382  by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
  31.383  qed "psp2";
  31.384  
  31.385  
  31.386  Goalw [unless_def]
  31.387 -   "[| leadsTo acts A A'; unless acts B B'; Id: acts |] \
  31.388 -\   ==> leadsTo acts (A Int B) ((A' Int B) Un B')";
  31.389 +   "[| F : leadsTo A A';  F : unless B B' |] \
  31.390 +\   ==> F : leadsTo (A Int B) ((A' Int B) Un B')";
  31.391  by (dtac psp 1);
  31.392  by (assume_tac 1);
  31.393 -by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
  31.394 -by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
  31.395 -by (etac leadsTo_Diff 2);
  31.396 -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2);
  31.397 -by Auto_tac;
  31.398 +by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 1);
  31.399 +by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 1);
  31.400 +by (etac leadsTo_Diff 1);
  31.401 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
  31.402  qed "psp_unless";
  31.403  
  31.404  
  31.405 @@ -339,12 +323,11 @@
  31.406  (** The most general rule: r is any wf relation; f is any variant function **)
  31.407  
  31.408  Goal "[| wf r;     \
  31.409 -\        ALL m. leadsTo acts (A Int f-``{m})                     \
  31.410 -\                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  31.411 -\        Id: acts |] \
  31.412 -\     ==> leadsTo acts (A Int f-``{m}) B";
  31.413 +\        ALL m. F : leadsTo (A Int f-``{m})                     \
  31.414 +\                            ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  31.415 +\     ==> F : leadsTo (A Int f-``{m}) B";
  31.416  by (eres_inst_tac [("a","m")] wf_induct 1);
  31.417 -by (subgoal_tac "leadsTo acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
  31.418 +by (subgoal_tac "F : leadsTo (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
  31.419  by (stac vimage_eq_UN 2);
  31.420  by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
  31.421  by (blast_tac (claset() addIs [leadsTo_UN]) 2);
  31.422 @@ -354,10 +337,9 @@
  31.423  
  31.424  (** Meta or object quantifier ????? **)
  31.425  Goal "[| wf r;     \
  31.426 -\        ALL m. leadsTo acts (A Int f-``{m})                     \
  31.427 -\                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  31.428 -\        Id: acts |] \
  31.429 -\     ==> leadsTo acts A B";
  31.430 +\        ALL m. F : leadsTo (A Int f-``{m})                     \
  31.431 +\                            ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  31.432 +\     ==> F : leadsTo A B";
  31.433  by (res_inst_tac [("t", "A")] subst 1);
  31.434  by (rtac leadsTo_UN 2);
  31.435  by (etac lemma 2);
  31.436 @@ -367,10 +349,9 @@
  31.437  
  31.438  
  31.439  Goal "[| wf r;     \
  31.440 -\        ALL m:I. leadsTo acts (A Int f-``{m})                   \
  31.441 -\                              ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  31.442 -\        Id: acts |] \
  31.443 -\     ==> leadsTo acts A ((A - (f-``I)) Un B)";
  31.444 +\        ALL m:I. F : leadsTo (A Int f-``{m})                   \
  31.445 +\                              ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
  31.446 +\     ==> F : leadsTo A ((A - (f-``I)) Un B)";
  31.447  by (etac leadsTo_wf_induct 1);
  31.448  by Safe_tac;
  31.449  by (case_tac "m:I" 1);
  31.450 @@ -379,33 +360,28 @@
  31.451  qed "bounded_induct";
  31.452  
  31.453  
  31.454 -(*Alternative proof is via the lemma leadsTo acts (A Int f-``(lessThan m)) B*)
  31.455 -Goal "[| ALL m. leadsTo acts (A Int f-``{m})                     \
  31.456 -\                            ((A Int f-``(lessThan m)) Un B);   \
  31.457 -\        Id: acts |] \
  31.458 -\     ==> leadsTo acts A B";
  31.459 +(*Alternative proof is via the lemma F : leadsTo (A Int f-``(lessThan m)) B*)
  31.460 +Goal "[| ALL m. F : leadsTo (A Int f-``{m})                     \
  31.461 +\                            ((A Int f-``(lessThan m)) Un B) |] \
  31.462 +\     ==> F : leadsTo A B";
  31.463  by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
  31.464 -by (assume_tac 2);
  31.465  by (Asm_simp_tac 1);
  31.466  qed "lessThan_induct";
  31.467  
  31.468 -Goal "[| ALL m:(greaterThan l). leadsTo acts (A Int f-``{m})   \
  31.469 -\                                  ((A Int f-``(lessThan m)) Un B);   \
  31.470 -\        Id: acts |] \
  31.471 -\     ==> leadsTo acts A ((A Int (f-``(atMost l))) Un B)";
  31.472 -by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
  31.473 +Goal "[| ALL m:(greaterThan l). F : leadsTo (A Int f-``{m})   \
  31.474 +\                                  ((A Int f-``(lessThan m)) Un B) |] \
  31.475 +\     ==> F : leadsTo A ((A Int (f-``(atMost l))) Un B)";
  31.476 +by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
  31.477 +			       Compl_greaterThan RS sym]) 1);
  31.478  by (rtac (wf_less_than RS bounded_induct) 1);
  31.479 -by (assume_tac 2);
  31.480  by (Asm_simp_tac 1);
  31.481  qed "lessThan_bounded_induct";
  31.482  
  31.483 -Goal "[| ALL m:(lessThan l). leadsTo acts (A Int f-``{m})   \
  31.484 -\                              ((A Int f-``(greaterThan m)) Un B);   \
  31.485 -\        Id: acts |] \
  31.486 -\     ==> leadsTo acts A ((A Int (f-``(atLeast l))) Un B)";
  31.487 +Goal "[| ALL m:(lessThan l). F : leadsTo (A Int f-``{m})   \
  31.488 +\                              ((A Int f-``(greaterThan m)) Un B) |] \
  31.489 +\     ==> F : leadsTo A ((A Int (f-``(atLeast l))) Un B)";
  31.490  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  31.491      (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
  31.492 -by (assume_tac 2);
  31.493  by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
  31.494  by (Clarify_tac 1);
  31.495  by (case_tac "m<l" 1);
  31.496 @@ -418,22 +394,22 @@
  31.497  (*** wlt ****)
  31.498  
  31.499  (*Misra's property W3*)
  31.500 -Goalw [wlt_def] "leadsTo acts (wlt acts B) B";
  31.501 +Goalw [wlt_def] "F : leadsTo (wlt F B) B";
  31.502  by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
  31.503  qed "wlt_leadsTo";
  31.504  
  31.505 -Goalw [wlt_def] "leadsTo acts A B ==> A <= wlt acts B";
  31.506 +Goalw [wlt_def] "F : leadsTo A B ==> A <= wlt F B";
  31.507  by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
  31.508  qed "leadsTo_subset";
  31.509  
  31.510  (*Misra's property W2*)
  31.511 -Goal "Id: acts ==> leadsTo acts A B = (A <= wlt acts B)";
  31.512 +Goal "F : leadsTo A B = (A <= wlt F B)";
  31.513  by (blast_tac (claset() addSIs [leadsTo_subset, 
  31.514  				wlt_leadsTo RS leadsTo_weaken_L]) 1);
  31.515  qed "leadsTo_eq_subset_wlt";
  31.516  
  31.517  (*Misra's property W4*)
  31.518 -Goal "Id: acts ==> B <= wlt acts B";
  31.519 +Goal "B <= wlt F B";
  31.520  by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
  31.521  				      subset_imp_leadsTo]) 1);
  31.522  qed "wlt_increasing";
  31.523 @@ -442,16 +418,16 @@
  31.524  (*Used in the Trans case below*)
  31.525  Goalw [constrains_def]
  31.526     "[| B <= A2;  \
  31.527 -\      constrains acts (A1 - B) (A1 Un B); \
  31.528 -\      constrains acts (A2 - C) (A2 Un C) |] \
  31.529 -\   ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)";
  31.530 +\      F : constrains (A1 - B) (A1 Un B); \
  31.531 +\      F : constrains (A2 - C) (A2 Un C) |] \
  31.532 +\   ==> F : constrains (A1 Un A2 - C) (A1 Un A2 Un C)";
  31.533  by (Blast_tac 1);
  31.534  val lemma1 = result();
  31.535  
  31.536  
  31.537  (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
  31.538 -Goal "[| leadsTo acts A A';  Id: acts |] ==> \
  31.539 -\      EX B. A<=B & leadsTo acts B A' & constrains acts (B-A') (B Un A')";
  31.540 +Goal "F : leadsTo A A' ==> \
  31.541 +\     EX B. A<=B & F : leadsTo B A' & F : constrains (B-A') (B Un A')";
  31.542  by (etac leadsTo_induct 1);
  31.543  (*Basis*)
  31.544  by (blast_tac (claset() addIs [leadsTo_Basis]
  31.545 @@ -470,11 +446,11 @@
  31.546  
  31.547  
  31.548  (*Misra's property W5*)
  31.549 -Goal "Id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)";
  31.550 -by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
  31.551 +Goal "F : constrains (wlt F B - B) (wlt F B)";
  31.552 +by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
  31.553  by (Clarify_tac 1);
  31.554 -by (subgoal_tac "Ba = wlt acts B" 1);
  31.555 -by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2);
  31.556 +by (subgoal_tac "Ba = wlt F B" 1);
  31.557 +by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2);
  31.558  by (Clarify_tac 1);
  31.559  by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
  31.560  qed "wlt_constrains_wlt";
  31.561 @@ -482,30 +458,29 @@
  31.562  
  31.563  (*** Completion: Binary and General Finite versions ***)
  31.564  
  31.565 -Goal "[| leadsTo acts A A';  stable acts A';   \
  31.566 -\        leadsTo acts B B';  stable acts B';  Id: acts |] \
  31.567 -\   ==> leadsTo acts (A Int B) (A' Int B')";
  31.568 -by (subgoal_tac "stable acts (wlt acts B')" 1);
  31.569 +Goal "[| F : leadsTo A A';  F : stable A';   \
  31.570 +\        F : leadsTo B B';  F : stable B' |] \
  31.571 +\   ==> F : leadsTo (A Int B) (A' Int B')";
  31.572 +by (subgoal_tac "F : stable (wlt F B')" 1);
  31.573  by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
  31.574  by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
  31.575 -	   etac wlt_constrains_wlt 2,
  31.576 +	   rtac wlt_constrains_wlt 2,
  31.577  	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
  31.578  	   Blast_tac 2]);
  31.579 -by (subgoal_tac "leadsTo acts (A Int wlt acts B') (A' Int wlt acts B')" 1);
  31.580 +by (subgoal_tac "F : leadsTo (A Int wlt F B') (A' Int wlt F B')" 1);
  31.581  by (blast_tac (claset() addIs [psp_stable]) 2);
  31.582 -by (subgoal_tac "leadsTo acts (A' Int wlt acts B') (A' Int B')" 1);
  31.583 +by (subgoal_tac "F : leadsTo (A' Int wlt F B') (A' Int B')" 1);
  31.584  by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
  31.585 -by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
  31.586 +by (subgoal_tac "F : leadsTo (A Int B) (A Int wlt F B')" 1);
  31.587  by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
  31.588  			       subset_imp_leadsTo]) 2);
  31.589  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
  31.590  qed "stable_completion";
  31.591  
  31.592  
  31.593 -Goal "[| finite I;  Id: acts |]                     \
  31.594 -\   ==> (ALL i:I. leadsTo acts (A i) (A' i)) -->  \
  31.595 -\       (ALL i:I. stable acts (A' i)) -->         \
  31.596 -\       leadsTo acts (INT i:I. A i) (INT i:I. A' i)";
  31.597 +Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i)) -->  \
  31.598 +\                  (ALL i:I. F : stable (A' i)) -->         \
  31.599 +\                  F : leadsTo (INT i:I. A i) (INT i:I. A' i)";
  31.600  by (etac finite_induct 1);
  31.601  by (Asm_simp_tac 1);
  31.602  by (asm_simp_tac 
  31.603 @@ -514,28 +489,26 @@
  31.604  qed_spec_mp "finite_stable_completion";
  31.605  
  31.606  
  31.607 -Goal "[| W = wlt acts (B' Un C);     \
  31.608 -\      leadsTo acts A (A' Un C);  constrains acts A' (A' Un C);   \
  31.609 -\      leadsTo acts B (B' Un C);  constrains acts B' (B' Un C);   \
  31.610 -\      Id: acts |] \
  31.611 -\   ==> leadsTo acts (A Int B) ((A' Int B') Un C)";
  31.612 -by (subgoal_tac "constrains acts (W-C) (W Un B' Un C)" 1);
  31.613 +Goal "[| W = wlt F (B' Un C);     \
  31.614 +\      F : leadsTo A (A' Un C);  F : constrains A' (A' Un C);   \
  31.615 +\      F : leadsTo B (B' Un C);  F : constrains B' (B' Un C) |] \
  31.616 +\   ==> F : leadsTo (A Int B) ((A' Int B') Un C)";
  31.617 +by (subgoal_tac "F : constrains (W-C) (W Un B' Un C)" 1);
  31.618  by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
  31.619  			       MRS constrains_Un RS constrains_weaken]) 2);
  31.620 -by (subgoal_tac "constrains acts (W-C) W" 1);
  31.621 +by (subgoal_tac "F : constrains (W-C) W" 1);
  31.622  by (asm_full_simp_tac 
  31.623      (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
  31.624 -by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1);
  31.625 +by (subgoal_tac "F : leadsTo (A Int W - C) (A' Int W Un C)" 1);
  31.626  by (simp_tac (simpset() addsimps [Int_Diff]) 2);
  31.627  by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2);
  31.628  (** LEVEL 7 **)
  31.629 -by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1);
  31.630 +by (subgoal_tac "F : leadsTo (A' Int W Un C) (A' Int B' Un C)" 1);
  31.631  by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
  31.632                                 psp2 RS leadsTo_weaken_R, 
  31.633  			       subset_refl RS subset_imp_leadsTo, 
  31.634  			       leadsTo_Un_duplicate2]) 2);
  31.635  by (dtac leadsTo_Diff 1);
  31.636 -by (assume_tac 2);
  31.637  by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
  31.638  by (subgoal_tac "A Int B <= A Int W" 1);
  31.639  by (blast_tac (claset() addSDs [leadsTo_subset]
  31.640 @@ -544,10 +517,9 @@
  31.641  bind_thm("completion", refl RS result());
  31.642  
  31.643  
  31.644 -Goal "[| finite I;  Id: acts |] \
  31.645 -\   ==> (ALL i:I. leadsTo acts (A i) (A' i Un C)) -->  \
  31.646 -\       (ALL i:I. constrains acts (A' i) (A' i Un C)) --> \
  31.647 -\       leadsTo acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
  31.648 +Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i Un C)) -->  \
  31.649 +\                  (ALL i:I. F : constrains (A' i) (A' i Un C)) --> \
  31.650 +\                  F : leadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)";
  31.651  by (etac finite_induct 1);
  31.652  by (ALLGOALS Asm_simp_tac);
  31.653  by (Clarify_tac 1);
    32.1 --- a/src/HOL/UNITY/WFair.thy	Wed Oct 14 15:47:22 1998 +0200
    32.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Oct 15 11:35:07 1998 +0200
    32.3 @@ -14,39 +14,38 @@
    32.4  
    32.5    (*This definition specifies weak fairness.  The rest of the theory
    32.6      is generic to all forms of fairness.*)
    32.7 -  transient :: "[('a * 'a)set set, 'a set] => bool"
    32.8 -    "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A"
    32.9 -
   32.10 -  ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   32.11 -    "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
   32.12 -			(*(unless acts A B) would be equivalent*)
   32.13 +  transient :: "'a set => 'a program set"
   32.14 +    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"
   32.15  
   32.16 -syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   32.17 -consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
   32.18 +  ensures :: "['a set, 'a set] => 'a program set"
   32.19 +    "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
   32.20 +
   32.21 +
   32.22 +consts leadsto :: "'a program => ('a set * 'a set) set"
   32.23    
   32.24 -translations
   32.25 -  "leadsTo acts A B" == "(A,B) : leadsto acts"
   32.26 -  "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts"
   32.27 -
   32.28 -inductive "leadsto acts"
   32.29 +inductive "leadsto F"
   32.30    intrs 
   32.31  
   32.32 -    Basis  "ensures acts A B ==> leadsTo acts A B"
   32.33 +    Basis  "F : ensures A B ==> (A,B) : leadsto F"
   32.34  
   32.35 -    Trans  "[| leadsTo acts A B;  leadsTo acts B C |]
   32.36 -	   ==> leadsTo acts A C"
   32.37 +    Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
   32.38 +	   ==> (A,C) : leadsto F"
   32.39  
   32.40      (*Encoding using powerset of the desired axiom
   32.41 -       (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B
   32.42 +       (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
   32.43      *)
   32.44 -    Union  "(UN A:S. {(A,B)}) : Pow (leadsto acts)
   32.45 -	   ==> leadsTo acts (Union S) B"
   32.46 +    Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
   32.47  
   32.48    monos "[Pow_mono]"
   32.49  
   32.50  
   32.51 -(*wlt acts B is the largest set that leads to B*)
   32.52 -constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
   32.53 -  "wlt acts B == Union {A. leadsTo acts A B}"
   32.54 +  
   32.55 +constdefs (*visible version of the relation*)
   32.56 +  leadsTo :: "['a set, 'a set] => 'a program set"
   32.57 +    "leadsTo A B == {F. (A,B) : leadsto F}"
   32.58 +  
   32.59 +  (*wlt F B is the largest set that leads to B*)
   32.60 +  wlt :: "['a program, 'a set] => 'a set"
   32.61 +    "wlt F B == Union {A. F: leadsTo A B}"
   32.62  
   32.63  end