removed the infernal States, eqStates, compatible, etc.
authorpaulson
Mon Mar 01 18:38:43 1999 +0100 (1999-03-01)
changeset 6295351b3c2b0d83
parent 6294 bc084e1b4d8d
child 6296 9da8f9262c4c
removed the infernal States, eqStates, compatible, etc.
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Client.thy
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Handshake.thy
src/HOL/UNITY/Lift.thy
src/HOL/UNITY/Mutex.thy
src/HOL/UNITY/NSP_Bad.thy
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Reach.thy
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/Traces.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Client.ML	Mon Mar 01 18:37:52 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Client.ML	Mon Mar 01 18:38:43 1999 +0100
     1.3 @@ -90,8 +90,7 @@
     1.4  
     1.5  (*** Towards proving the liveness property ***)
     1.6  
     1.7 -Goal "States Cli_prg = States G \
     1.8 -\     ==> Cli_prg Join G   \
     1.9 +Goal "Cli_prg Join G   \
    1.10  \       : transient {s. size (giv s) = Suc k &  \
    1.11  \                       size (rel s) = k & ask s ! k <= giv s ! k}";
    1.12  by (res_inst_tac [("act", "rel_act")] transient_mem 1);
    1.13 @@ -131,13 +130,11 @@
    1.14  by (Clarify_tac 1);
    1.15  by (rtac Stable_transient_reachable_LeadsTo 1);
    1.16  by (res_inst_tac [("k", "k")] transient_lemma 2);
    1.17 -by (etac Disjoint_States_eq 2);
    1.18  by (force_tac (claset() addDs [impOfSubs Increasing_size,
    1.19  			       impOfSubs Increasing_Stable_less],
    1.20  	       simpset()) 1);
    1.21  by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
    1.22   by (Blast_tac 1);
    1.23 -by (etac Disjoint_States_eq 1);
    1.24  by (auto_tac (claset(),
    1.25  	      simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
    1.26  by (ALLGOALS Force_tac);
     2.1 --- a/src/HOL/UNITY/Client.thy	Mon Mar 01 18:37:52 1999 +0100
     2.2 +++ b/src/HOL/UNITY/Client.thy	Mon Mar 01 18:38:43 1999 +0100
     2.3 @@ -48,8 +48,7 @@
     2.4  		          size (ask s) = size (rel s))}"
     2.5  
     2.6    Cli_prg :: state program
     2.7 -    "Cli_prg == mk_program (UNIV,
     2.8 -			    {s. tok s : atMost Max &
     2.9 +    "Cli_prg == mk_program ({s. tok s : atMost Max &
    2.10  			        giv s = [] &
    2.11  			        ask s = [] &
    2.12  			        rel s = []},
     3.1 --- a/src/HOL/UNITY/Common.ML	Mon Mar 01 18:37:52 1999 +0100
     3.2 +++ b/src/HOL/UNITY/Common.ML	Mon Mar 01 18:38:43 1999 +0100
     3.3 @@ -30,13 +30,13 @@
     3.4  
     3.5  (*** Some programs that implement the safety property above ***)
     3.6  
     3.7 -Goal "SKIP UNIV : constrains {m} (maxfg m)";
     3.8 +Goal "SKIP : constrains {m} (maxfg m)";
     3.9  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    3.10  				  fasc]) 1);
    3.11  result();
    3.12  
    3.13  (*This one is  t := ftime t || t := gtime t*)
    3.14 -Goal "mk_program (UNIV, UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
    3.15 +Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
    3.16  \      : constrains {m} (maxfg m)";
    3.17  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    3.18  				  le_max_iff_disj, fasc]) 1);
    3.19 @@ -44,7 +44,7 @@
    3.20  result();
    3.21  
    3.22  (*This one is  t := max (ftime t) (gtime t)*)
    3.23 -Goal "mk_program (UNIV, UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
    3.24 +Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
    3.25  \      : constrains {m} (maxfg m)";
    3.26  by (simp_tac 
    3.27      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    3.28 @@ -52,8 +52,7 @@
    3.29  result();
    3.30  
    3.31  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    3.32 -Goal "mk_program (UNIV, UNIV, \
    3.33 -\                 { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
    3.34 +Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
    3.35  \      : constrains {m} (maxfg m)";
    3.36  by (simp_tac 
    3.37      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
     4.1 --- a/src/HOL/UNITY/Comp.ML	Mon Mar 01 18:37:52 1999 +0100
     4.2 +++ b/src/HOL/UNITY/Comp.ML	Mon Mar 01 18:38:43 1999 +0100
     4.3 @@ -16,33 +16,31 @@
     4.4  
     4.5  (*** component ***)
     4.6  
     4.7 -Goalw [component_def] "component (SKIP (States F)) F";
     4.8 +Goalw [component_def] "component SKIP F";
     4.9  by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
    4.10  qed "component_SKIP";
    4.11  
    4.12  Goalw [component_def] "component F F";
    4.13 -by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1);
    4.14 +by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
    4.15  qed "component_refl";
    4.16  
    4.17  AddIffs [component_SKIP, component_refl];
    4.18  
    4.19 -Goalw [component_def] "States F = States G ==> component F (F Join G)";
    4.20 +Goalw [component_def] "component F (F Join G)";
    4.21  by (Blast_tac 1);
    4.22  qed "component_Join1";
    4.23  
    4.24 -Goalw [component_def] "States F = States G ==> component G (F Join G)";
    4.25 +Goalw [component_def] "component G (F Join G)";
    4.26  by (simp_tac (simpset() addsimps [Join_commute]) 1);
    4.27 -by (dtac sym 1);
    4.28  by (Blast_tac 1);
    4.29  qed "component_Join2";
    4.30  
    4.31 -Goalw [component_def, eqStates_def] 
    4.32 -    "[| i : I;  eqStates I F |] ==> component (F i) (JN i:I. (F i))";
    4.33 -by (force_tac (claset() addIs [JN_absorb], simpset()) 1);
    4.34 +Goalw [component_def] "i : I ==> component (F i) (JN i:I. (F i))";
    4.35 +by (blast_tac (claset() addIs [JN_absorb]) 1);
    4.36  qed "component_JN";
    4.37  
    4.38  Goalw [component_def] "[| component F G; component G H |] ==> component F H";
    4.39 -by (force_tac (claset() addIs [Join_assoc RS sym], simpset()) 1);
    4.40 +by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    4.41  qed "component_trans";
    4.42  
    4.43  Goalw [component_def] "component F G ==> Acts F <= Acts G";
    4.44 @@ -53,46 +51,34 @@
    4.45  by Auto_tac;
    4.46  qed "component_Init";
    4.47  
    4.48 -Goalw [component_def] "component F G ==> States F = States G";
    4.49 -by Auto_tac;
    4.50 -qed "component_States";
    4.51 -
    4.52  Goal "[| component F G; component G F |] ==> F=G";
    4.53 -by (blast_tac (claset() addSIs [program_equalityI, component_States, 
    4.54 +by (blast_tac (claset() addSIs [program_equalityI, 
    4.55  				component_Init, component_Acts]) 1);
    4.56  qed "component_anti_sym";
    4.57  
    4.58  Goalw [component_def]
    4.59        "component F H = (EX G. F Join G = H & Disjoint F G)";
    4.60 -by (blast_tac (claset() addSIs [Disjoint_States_eq, 
    4.61 -				Diff_Disjoint, Join_Diff2]) 1);
    4.62 +by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
    4.63  qed "component_eq";
    4.64  
    4.65 +
    4.66  (*** existential properties ***)
    4.67  
    4.68  Goalw [ex_prop_def]
    4.69 -     "[| ex_prop X;  finite GG |] \
    4.70 -\     ==> eqStates GG (%x. x) --> GG Int X ~= {} --> (JN G:GG. G) : X";
    4.71 +     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
    4.72  by (etac finite_induct 1);
    4.73 -by (Simp_tac 1);
    4.74 -by (rename_tac "GG J" 1);
    4.75 -by (full_simp_tac (simpset() addsimps [Int_insert_left]) 1);
    4.76 -by (dres_inst_tac [("x","J")] spec 1);
    4.77 -by (Force_tac 1);
    4.78 +by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    4.79  qed_spec_mp "ex1";
    4.80  
    4.81  Goalw [ex_prop_def]
    4.82 -     "ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \
    4.83 -\       --> (JN G:GG. G) : X ==> ex_prop X";
    4.84 +     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
    4.85  by (Clarify_tac 1);
    4.86  by (dres_inst_tac [("x", "{F,G}")] spec 1);
    4.87  by Auto_tac;
    4.88  qed "ex2";
    4.89  
    4.90  (*Chandy & Sanders take this as a definition*)
    4.91 -Goal "ex_prop X = \
    4.92 -\       (ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \
    4.93 -\          --> (JN G:GG. G) : X)";
    4.94 +Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
    4.95  by (blast_tac (claset() addIs [ex1,ex2]) 1);
    4.96  qed "ex_prop_finite";
    4.97  
    4.98 @@ -103,7 +89,6 @@
    4.99  by (Blast_tac 1);
   4.100  by Safe_tac;
   4.101  by (stac Join_commute 2);
   4.102 -by (dtac sym 2);
   4.103  by (ALLGOALS Blast_tac);
   4.104  qed "ex_prop_equiv";
   4.105  
   4.106 @@ -111,15 +96,13 @@
   4.107  (*** universal properties ***)
   4.108  
   4.109  Goalw [uv_prop_def]
   4.110 -     "[| uv_prop X; finite GG |] \
   4.111 -\     ==> eqStates GG (%x. x) --> GG <= X --> (JN G:GG. G) : X";
   4.112 +     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
   4.113  by (etac finite_induct 1);
   4.114  by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
   4.115  qed_spec_mp "uv1";
   4.116  
   4.117  Goalw [uv_prop_def]
   4.118 -     "ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \
   4.119 -\       --> (JN G:GG. G) : X  ==> uv_prop X";
   4.120 +     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
   4.121  by (rtac conjI 1);
   4.122  by (Clarify_tac 2);
   4.123  by (dres_inst_tac [("x", "{F,G}")] spec 2);
   4.124 @@ -128,8 +111,7 @@
   4.125  qed "uv2";
   4.126  
   4.127  (*Chandy & Sanders take this as a definition*)
   4.128 -Goal "uv_prop X = (ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \
   4.129 -\       --> (JN G:GG. G) : X)";
   4.130 +Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
   4.131  by (blast_tac (claset() addIs [uv1,uv2]) 1);
   4.132  qed "uv_prop_finite";
   4.133  
   4.134 @@ -199,7 +181,7 @@
   4.135  qed "guaranteesI";
   4.136  
   4.137  Goalw [guarantees_def, component_def]
   4.138 -     "[| F : X guarantees Y;  F Join G : X;  States F = States G |] \
   4.139 +     "[| F : X guarantees Y;  F Join G : X;  compatible{F,G} |] \
   4.140  \     ==> F Join G : Y";
   4.141  by (Blast_tac 1);
   4.142  qed "guaranteesD";
   4.143 @@ -227,42 +209,34 @@
   4.144  qed "refines_trans";
   4.145  
   4.146  Goalw [strict_ex_prop_def]
   4.147 -     "[| strict_ex_prop X;  States F = States G |] \
   4.148 -\     ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = \
   4.149 -\         (F:X --> G:X)";
   4.150 -by Safe_tac;
   4.151 +     "strict_ex_prop X \
   4.152 +\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   4.153  by (Blast_tac 1);
   4.154 -by Auto_tac;
   4.155  qed "strict_ex_refine_lemma";
   4.156  
   4.157  Goalw [strict_ex_prop_def]
   4.158 -     "[| strict_ex_prop X;  States F = States G |] \
   4.159 -\     ==> (ALL H. States F = States H & F Join H : welldef & F Join H : X \
   4.160 -\           --> G Join H : X) = \
   4.161 +     "strict_ex_prop X \
   4.162 +\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   4.163  \         (F: welldef Int X --> G:X)";
   4.164  by Safe_tac;
   4.165 -by (eres_inst_tac [("x","SKIP ?A"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   4.166 +by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   4.167  by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
   4.168  qed "strict_ex_refine_lemma_v";
   4.169  
   4.170 -Goal "[| strict_ex_prop X;  States F = States G;  \
   4.171 -\        ALL H. States F = States H & F Join H : welldef Int X \
   4.172 -\          --> G Join H : welldef |] \
   4.173 +Goal "[| strict_ex_prop X;  \
   4.174 +\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   4.175  \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   4.176 -by (dtac sym 1);
   4.177 -by (res_inst_tac [("x","SKIP (States G)")] allE 1
   4.178 +by (res_inst_tac [("x","SKIP")] allE 1
   4.179      THEN assume_tac 1);
   4.180 -by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   4.181 -					   strict_ex_refine_lemma_v]) 1);
   4.182 +by (asm_full_simp_tac
   4.183 +    (simpset() addsimps [refines_def, iso_refines_def,
   4.184 +			 strict_ex_refine_lemma_v]) 1);
   4.185  qed "ex_refinement_thm";
   4.186  
   4.187  
   4.188 -(***
   4.189 -
   4.190 -
   4.191  Goalw [strict_uv_prop_def]
   4.192       "strict_uv_prop X \
   4.193 -\     ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
   4.194 +\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   4.195  by (Blast_tac 1);
   4.196  qed "strict_uv_refine_lemma";
   4.197  
   4.198 @@ -284,4 +258,3 @@
   4.199  by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   4.200  					   strict_uv_refine_lemma_v]) 1);
   4.201  qed "uv_refinement_thm";
   4.202 -***)
     5.1 --- a/src/HOL/UNITY/Comp.thy	Mon Mar 01 18:37:52 1999 +0100
     5.2 +++ b/src/HOL/UNITY/Comp.thy	Mon Mar 01 18:38:43 1999 +0100
     5.3 @@ -6,11 +6,6 @@
     5.4  Composition
     5.5  
     5.6  From Chandy and Sanders, "Reasoning About Program Composition"
     5.7 -
     5.8 -QUESTIONS:
     5.9 -  refines_def: needs the States F = States G?
    5.10 -
    5.11 -  uv_prop, component: should be States F = States (F Join G)
    5.12  *)
    5.13  
    5.14  Comp = Union +
    5.15 @@ -21,29 +16,23 @@
    5.16      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    5.17  
    5.18    ex_prop  :: 'a program set => bool
    5.19 -   "ex_prop X ==
    5.20 -      ALL F G. (F:X | G: X) & States F = States G --> (F Join G) : X"
    5.21 +   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
    5.22  
    5.23    strict_ex_prop  :: 'a program set => bool
    5.24 -   "strict_ex_prop X ==
    5.25 -      ALL F G. States F = States G --> (F:X | G: X) = (F Join G : X)"
    5.26 +   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
    5.27  
    5.28    uv_prop  :: 'a program set => bool
    5.29 -   "uv_prop X ==
    5.30 -      SKIP UNIV : X &
    5.31 -      (ALL F G. F:X & G: X & States F = States G --> (F Join G) : X)"
    5.32 +   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
    5.33  
    5.34    strict_uv_prop  :: 'a program set => bool
    5.35 -   "strict_uv_prop X ==
    5.36 -      SKIP UNIV : X &
    5.37 -      (ALL F G. States F = States G --> (F:X & G: X) = (F Join G : X))"
    5.38 +   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
    5.39  
    5.40    (*Ill-defined programs can arise through "Join"*)
    5.41    welldef :: 'a program set  
    5.42     "welldef == {F. Init F ~= {}}"
    5.43  
    5.44    component :: ['a program, 'a program] => bool
    5.45 -   "component F H == EX G. F Join G = H & States F = States G"
    5.46 +   "component F H == EX G. F Join G = H"
    5.47  
    5.48    guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
    5.49     "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
    5.50 @@ -51,9 +40,7 @@
    5.51    refines :: ['a program, 'a program, 'a program set] => bool
    5.52  			("(3_ refines _ wrt _)" [10,10,10] 10)
    5.53     "G refines F wrt X ==
    5.54 -      States F = States G &
    5.55 -      (ALL H. States F = States H & (F Join H) : welldef Int X
    5.56 -        --> G Join H : welldef Int X)"
    5.57 +      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
    5.58  
    5.59    iso_refines :: ['a program, 'a program, 'a program set] => bool
    5.60  			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
     6.1 --- a/src/HOL/UNITY/Constrains.ML	Mon Mar 01 18:37:52 1999 +0100
     6.2 +++ b/src/HOL/UNITY/Constrains.ML	Mon Mar 01 18:38:43 1999 +0100
     6.3 @@ -89,25 +89,24 @@
     6.4  by (blast_tac (claset() addIs [constrains_weaken]) 1);
     6.5  qed "ball_Constrains_INT";
     6.6  
     6.7 -Goal "[| F : Constrains A A'; A <= reachable F |] ==> A <= A'";
     6.8 +Goal "F : Constrains A A' ==> reachable F Int A <= A'";
     6.9  by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
    6.10  by (dtac constrains_imp_subset 1);
    6.11 -by (auto_tac (claset() addIs [impOfSubs reachable_subset_States],
    6.12 -	      simpset() addsimps [Int_subset_iff, Int_lower1]));
    6.13 +by (ALLGOALS
    6.14 +    (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
    6.15  qed "Constrains_imp_subset";
    6.16  
    6.17  Goalw [Constrains_def]
    6.18      "[| F : Constrains A B; F : Constrains B C |]   \
    6.19  \    ==> F : Constrains A C";
    6.20 -by (blast_tac (claset() addIs [impOfSubs reachable_subset_States,
    6.21 -			       constrains_trans, constrains_weaken]) 1);
    6.22 +by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
    6.23  qed "Constrains_trans";
    6.24  
    6.25 -Goal "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
    6.26 -\     ==> F : Constrains A (A' Un B')";
    6.27 -by (asm_full_simp_tac (simpset() addsimps [Constrains_def, Int_Un_distrib]) 1);
    6.28 -by (blast_tac (claset() addIs [impOfSubs reachable_subset_States,
    6.29 -			       constrains_cancel]) 1);
    6.30 +Goalw [Constrains_def, constrains_def]
    6.31 +   "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
    6.32 +\   ==> F : Constrains A (A' Un B')";
    6.33 +by (Clarify_tac 1);
    6.34 +by (Blast_tac 1);
    6.35  qed "Constrains_cancel";
    6.36  
    6.37  
     7.1 --- a/src/HOL/UNITY/Handshake.ML	Mon Mar 01 18:37:52 1999 +0100
     7.2 +++ b/src/HOL/UNITY/Handshake.ML	Mon Mar 01 18:38:43 1999 +0100
     7.3 @@ -11,7 +11,6 @@
     7.4  (*split_all_tac causes a big blow-up*)
     7.5  claset_ref() := claset() delSWrapper record_split_name;
     7.6  
     7.7 -Addsimps [F_def RS def_prg_States, G_def RS def_prg_States];
     7.8  Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
     7.9  program_defs_ref := [F_def, G_def];
    7.10  
    7.11 @@ -21,6 +20,7 @@
    7.12  Addsimps (thms"state.update_defs");
    7.13  Addsimps [simp_of_set invFG_def];
    7.14  
    7.15 +
    7.16  Goal "(F Join G) : Invariant invFG";
    7.17  by (rtac InvariantI 1);
    7.18  by (Force_tac 1);
    7.19 @@ -32,7 +32,7 @@
    7.20  qed "invFG";
    7.21  
    7.22  Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \
    7.23 -\                              ({s. NF s = k} Int {s. BB s})";
    7.24 +\                          ({s. NF s = k} Int {s. BB s})";
    7.25  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    7.26  by (ensures_tac "cmdG" 2);
    7.27  by (constrains_tac 1);
     8.1 --- a/src/HOL/UNITY/Handshake.thy	Mon Mar 01 18:37:52 1999 +0100
     8.2 +++ b/src/HOL/UNITY/Handshake.thy	Mon Mar 01 18:38:43 1999 +0100
     8.3 @@ -21,14 +21,14 @@
     8.4      "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
     8.5  
     8.6    F :: "state program"
     8.7 -    "F == mk_program (UNIV, {s. NF s = 0 & BB s}, {cmdF})"
     8.8 +    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
     8.9  
    8.10    (*G's program*)
    8.11    cmdG :: "(state*state) set"
    8.12      "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
    8.13  
    8.14    G :: "state program"
    8.15 -    "G == mk_program (UNIV, {s. NG s = 0 & BB s}, {cmdG})"
    8.16 +    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
    8.17  
    8.18    (*the joint invariant*)
    8.19    invFG :: "state set"
     9.1 --- a/src/HOL/UNITY/Lift.thy	Mon Mar 01 18:37:52 1999 +0100
     9.2 +++ b/src/HOL/UNITY/Lift.thy	Mon Mar 01 18:38:43 1999 +0100
     9.3 @@ -116,8 +116,7 @@
     9.4  
     9.5    Lprg :: state program
     9.6      (*for the moment, we OMIT button_press*)
     9.7 -    "Lprg == mk_program (UNIV,
     9.8 -			 {s. floor s = Min & ~ up s & move s & stop s &
     9.9 +    "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
    9.10  		          ~ open s & req s = {}},
    9.11  			 {request_act, open_act, close_act,
    9.12  			  req_up, req_down, move_up, move_down})"
    9.13 @@ -160,5 +159,6 @@
    9.14    assumes
    9.15      Min_le_n    "Min <= n"
    9.16      n_le_Max    "n <= Max"
    9.17 +  defines
    9.18  
    9.19  end
    10.1 --- a/src/HOL/UNITY/Mutex.thy	Mon Mar 01 18:37:52 1999 +0100
    10.2 +++ b/src/HOL/UNITY/Mutex.thy	Mon Mar 01 18:38:43 1999 +0100
    10.3 @@ -52,8 +52,7 @@
    10.4      "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}"
    10.5  
    10.6    Mprg :: state program
    10.7 -    "Mprg == mk_program (UNIV,
    10.8 -			 {s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0},
    10.9 +    "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0},
   10.10  			 {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
   10.11  			  cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})"
   10.12  
    11.1 --- a/src/HOL/UNITY/NSP_Bad.thy	Mon Mar 01 18:37:52 1999 +0100
    11.2 +++ b/src/HOL/UNITY/NSP_Bad.thy	Mon Mar 01 18:38:43 1999 +0100
    11.3 @@ -54,6 +54,6 @@
    11.4  constdefs
    11.5    Nprg :: state program
    11.6      (*Initial trace is empty*)
    11.7 -    "Nprg == mk_program(UNIV, {[]}, {Fake, NS1, NS2, NS3})"
    11.8 +    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})"
    11.9  
   11.10  end
    12.1 --- a/src/HOL/UNITY/PPROD.ML	Mon Mar 01 18:37:52 1999 +0100
    12.2 +++ b/src/HOL/UNITY/PPROD.ML	Mon Mar 01 18:38:43 1999 +0100
    12.3 @@ -7,241 +7,6 @@
    12.4  
    12.5  val rinst = read_instantiate_sg (sign_of thy);
    12.6  
    12.7 -    (*** General lemmas ***)
    12.8 -
    12.9 -Goalw [sharing_def] "((x,y): sharing Rsh A) = (x: A & y : range (Rsh x))";
   12.10 -by Auto_tac;
   12.11 -qed "sharing_iff";
   12.12 -AddIffs [sharing_iff]; 
   12.13 -
   12.14 -Goalw [sharing_def] "(sharing Rsh A <= sharing Rsh B) = (A <= B)";
   12.15 -by Auto_tac;
   12.16 -qed "sharing_subset_iff";
   12.17 -AddIffs [sharing_subset_iff]; 
   12.18 -
   12.19 -Goalw [sharing_def] "sharing Rsh (A Un B) = sharing Rsh A Un sharing Rsh B";
   12.20 -by Auto_tac;
   12.21 -qed "sharing_Un_distrib";
   12.22 -
   12.23 -Goalw [sharing_def] "sharing Rsh (A Int B) = sharing Rsh A Int sharing Rsh B";
   12.24 -by Auto_tac;
   12.25 -qed "sharing_Int_distrib";
   12.26 -
   12.27 -Goalw [sharing_def] "sharing Rsh (A - B) = sharing Rsh A - sharing Rsh B";
   12.28 -by Auto_tac;
   12.29 -qed "sharing_Diff_distrib";
   12.30 -
   12.31 -Goalw [sharing_def] "sharing Rsh (Union A) = (UN X:A. sharing Rsh X)";
   12.32 -by (Blast_tac 1);
   12.33 -qed "sharing_Union";
   12.34 -
   12.35 -Goal "(sharing Rsh A <= - sharing Rsh B) = (A <= - B)";
   12.36 -by (force_tac (claset(),simpset() addsimps [sharing_def, Image_iff]) 1);
   12.37 -qed "Lcopy_subset_Compl_eq";
   12.38 -
   12.39 -Goal "(((a,b), (a',b')) : Lcopy_act Rsh act) = \
   12.40 -\     ((a,a'):act & Rsh a b = b & Rsh a' b = b')";
   12.41 -by (simp_tac (simpset() addsimps [Lcopy_act_def]) 1);
   12.42 -qed "mem_Lcopy_act_iff";
   12.43 -AddIffs [mem_Lcopy_act_iff]; 
   12.44 -
   12.45 -(*NEEDED????????????????*)
   12.46 -Goal "[| (a,a'):act; Rsh a b = b |] ==> (((a,b), (a', Rsh a' b)) : Lcopy_act Rsh act)";
   12.47 -by Auto_tac;
   12.48 -qed "mem_Lcopy_actI";
   12.49 -
   12.50 -
   12.51 -Goal "act : Acts F \
   12.52 -\     ==> Lcopy_act Rsh act <= \
   12.53 -\         sharing Rsh (States F) Times sharing Rsh (States F)";
   12.54 -by (auto_tac (claset() addIs [range_eqI, sym]
   12.55 -                       addDs [impOfSubs Acts_subset_Pow_States], 
   12.56 -              simpset()));
   12.57 -qed "Lcopy_act_subset_Times";
   12.58 -
   12.59 -
   12.60 -
   12.61 -Open_locale "Share";
   12.62 -
   12.63 -val overwrite = thm "overwrite";
   12.64 -Addsimps [overwrite];
   12.65 -
   12.66 -Goal "Lcopy_act Rsh act ^^ sharing Rsh A = sharing Rsh (act ^^ A)";
   12.67 -by (force_tac (claset(),simpset() addsimps [sharing_def, Image_iff]) 1);
   12.68 -qed "Lcopy_act_Image";
   12.69 -Addsimps [Lcopy_act_Image];
   12.70 -
   12.71 -
   12.72 -
   12.73 -Goal "(Lcopy_act Rsh act ^^ sharing Rsh A <= sharing Rsh B) = (act ^^ A <= B)";
   12.74 -by (force_tac (claset(),simpset() addsimps [sharing_def, Image_iff]) 1);
   12.75 -qed "Lcopy_act_Image_subset_eq";
   12.76 -
   12.77 -Goal "Domain (Lcopy_act Rsh act) = sharing Rsh (Domain act)";
   12.78 -by (auto_tac (claset() addIs [sym], simpset() addsimps [Domain_iff]));
   12.79 -qed "Domain_Lcopy_act"; 
   12.80 -
   12.81 -(*?? needed??
   12.82 -Goal "(Lcopy_act Rsh act) ^^ (SIGMA x:A. B Int range(Rsh x)) = (SIGMA x: act^^A. Rsh x `` B)";
   12.83 -by (auto_tac (claset(), simpset() addsimps [Image_iff]));
   12.84 -qed "Image_Lcopy_act"; 
   12.85 -**)
   12.86 -
   12.87 -Goal "Lcopy_act Rsh (diag A) = diag (sharing Rsh A)";
   12.88 -by (auto_tac (claset() addIs [sym], simpset()));
   12.89 -qed "Lcopy_diag";
   12.90 -
   12.91 -Addsimps [Lcopy_diag];
   12.92 -
   12.93 -
   12.94 -(**** Lcopy ****)
   12.95 -
   12.96 -(*** Basic properties ***)
   12.97 -
   12.98 -Goalw [Lcopy_def] "States (Lcopy Rsh F) = sharing Rsh (States F)";
   12.99 -by Auto_tac;
  12.100 -qed "States_Lcopy";
  12.101 -
  12.102 -Goalw [Lcopy_def] "Init (Lcopy Rsh F) = sharing Rsh (Init F)";
  12.103 -by (auto_tac (claset() addIs [impOfSubs Init_subset_States], simpset()));
  12.104 -qed "Init_Lcopy";
  12.105 -
  12.106 -Goal "diag (sharing Rsh (States F)) : Lcopy_act Rsh `` Acts F";
  12.107 -by (rtac image_eqI 1);
  12.108 -by (rtac diag_in_Acts 2);
  12.109 -by Auto_tac;
  12.110 -val lemma = result();
  12.111 -
  12.112 -Goal "Acts (Lcopy Rsh F) = (Lcopy_act Rsh `` Acts F)";
  12.113 -by (auto_tac (claset() addSIs [lemma] 
  12.114 -                       addDs [impOfSubs Acts_subset_Pow_States], 
  12.115 -	      simpset() addsimps [Lcopy_def, Lcopy_act_subset_Times, 
  12.116 -				  image_subset_iff]));
  12.117 -qed "Acts_Lcopy";
  12.118 -
  12.119 -Addsimps [States_Lcopy, Init_Lcopy, Acts_Lcopy];
  12.120 -
  12.121 -Goalw [SKIP_def] "Lcopy Rsh (SKIP A) = SKIP(sharing Rsh A)";
  12.122 -by (rtac program_equalityI 1);
  12.123 -by Auto_tac;
  12.124 -qed "Lcopy_SKIP";
  12.125 -
  12.126 -
  12.127 -(*** Safety: constrains, stable ***)
  12.128 -
  12.129 -Goal "(Lcopy Rsh F : constrains (sharing Rsh A) (sharing Rsh B)) = \
  12.130 -\     (F : constrains A B)";
  12.131 -by (simp_tac (simpset() addsimps [constrains_def, 
  12.132 -				  Lcopy_act_Image_subset_eq]) 1);
  12.133 -qed "Lcopy_constrains";
  12.134 -
  12.135 -Goal "[| Lcopy Rsh F : constrains A B;  A <= States (Lcopy Rsh F) |]  \
  12.136 -\     ==> F : constrains (Domain A) (Domain B)";
  12.137 -by (force_tac (claset() addIs [rev_bexI], 
  12.138 -	       simpset() addsimps [constrains_def, sharing_def, Image_iff]) 1);
  12.139 -qed "Lcopy_constrains_Domain";
  12.140 -
  12.141 -Goal "(Lcopy Rsh F : stable (sharing Rsh A)) = (F : stable A)";
  12.142 -by (asm_simp_tac (simpset() addsimps [stable_def, Lcopy_constrains]) 1);
  12.143 -qed "Lcopy_stable";
  12.144 -
  12.145 -Goal "(Lcopy Rsh F : invariant (sharing Rsh A)) = (F : invariant A)";
  12.146 -by (asm_simp_tac (simpset() addsimps [invariant_def, Lcopy_stable]) 1);
  12.147 -qed "Lcopy_invariant";
  12.148 -
  12.149 -(** Substitution Axiom versions: Constrains, Stable **)
  12.150 -
  12.151 -Goal "p : reachable (Lcopy Rsh F) \
  12.152 -\     ==> (%(a,b). a : reachable F & b : range (Rsh a)) p";
  12.153 -by (etac reachable.induct 1);
  12.154 -by (auto_tac
  12.155 -    (claset() addIs reachable.intrs,
  12.156 -     simpset() addsimps [Acts_Lcopy]));
  12.157 -qed "reachable_Lcopy_fst";
  12.158 -
  12.159 -Goal "(a,b) : reachable (Lcopy Rsh F) \
  12.160 -\     ==> a : reachable F & b : range (Rsh a)";
  12.161 -by (force_tac (claset() addSDs [reachable_Lcopy_fst], simpset()) 1);
  12.162 -qed "reachable_LcopyD";
  12.163 -
  12.164 -Goal "reachable (Lcopy Rsh F) = sharing Rsh (reachable F)";
  12.165 -by (rtac equalityI 1);
  12.166 -by (force_tac (claset() addSDs [reachable_LcopyD], simpset()) 1);
  12.167 -by (Clarify_tac 1);
  12.168 -by (etac reachable.induct 1);
  12.169 -by (ALLGOALS (force_tac (claset() addIs reachable.intrs, 
  12.170 -			 simpset())));
  12.171 -qed "reachable_Lcopy_eq";
  12.172 -
  12.173 -Goal "(Lcopy Rsh F : Constrains (sharing Rsh A) (sharing Rsh B)) =  \
  12.174 -\     (F : Constrains A B)";
  12.175 -by (simp_tac
  12.176 -    (simpset() addsimps [Constrains_def, reachable_Lcopy_eq, 
  12.177 -			 Lcopy_constrains, sharing_Int_distrib RS sym]) 1);
  12.178 -qed "Lcopy_Constrains";
  12.179 -
  12.180 -Goal "(Lcopy Rsh F : Stable (sharing Rsh A)) = (F : Stable A)";
  12.181 -by (simp_tac (simpset() addsimps [Stable_def, Lcopy_Constrains]) 1);
  12.182 -qed "Lcopy_Stable";
  12.183 -
  12.184 -
  12.185 -(*** Progress: transient, ensures ***)
  12.186 -
  12.187 -Goal "(Lcopy Rsh F : transient (sharing Rsh A)) = (F : transient A)";
  12.188 -by (auto_tac (claset(),
  12.189 -	      simpset() addsimps [transient_def, Lcopy_subset_Compl_eq,
  12.190 -				  Domain_Lcopy_act]));
  12.191 -qed "Lcopy_transient";
  12.192 -
  12.193 -Goal "(Lcopy Rsh F : ensures (sharing Rsh A) (sharing Rsh B)) = \
  12.194 -\     (F : ensures A B)";
  12.195 -by (simp_tac
  12.196 -    (simpset() addsimps [ensures_def, Lcopy_constrains, Lcopy_transient, 
  12.197 -			 sharing_Un_distrib RS sym, 
  12.198 -			 sharing_Diff_distrib RS sym]) 1);
  12.199 -qed "Lcopy_ensures";
  12.200 -
  12.201 -Goal "F : leadsTo A B \
  12.202 -\     ==> Lcopy Rsh F : leadsTo (sharing Rsh A) (sharing Rsh B)";
  12.203 -by (etac leadsTo_induct 1);
  12.204 -by (asm_simp_tac (simpset() addsimps [leadsTo_UN, sharing_Union]) 3);
  12.205 -by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
  12.206 -by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, Lcopy_ensures]) 1);
  12.207 -qed "leadsTo_imp_Lcopy_leadsTo";
  12.208 -
  12.209 -(**
  12.210 -    Goal "Lcopy Rsh F : ensures A B ==> F : ensures (Domain A) (Domain B)";
  12.211 -    by (full_simp_tac
  12.212 -	(simpset() addsimps [ensures_def, Lcopy_constrains, Lcopy_transient, 
  12.213 -			     Domain_Un_eq RS sym,
  12.214 -			     sharing_Un_distrib RS sym, 
  12.215 -			     sharing_Diff_distrib RS sym]) 1);
  12.216 -    by (safe_tac (claset() addSDs [Lcopy_constrains_Domain]));
  12.217 -    by (etac constrains_weaken_L 1);
  12.218 -    by (Blast_tac 1);
  12.219 -    (*NOT able to prove this:
  12.220 -    Lcopy Rsh F : ensures A B ==> F : ensures (Domain A) (Domain B)
  12.221 -     1. [| Lcopy Rsh F : transient (A - B);
  12.222 -	   F : constrains (Domain (A - B)) (Domain (A Un B)) |]
  12.223 -	==> F : transient (Domain A - Domain B)
  12.224 -    **)
  12.225 -
  12.226 -
  12.227 -    Goal "Lcopy Rsh F : leadsTo AU BU ==> F : leadsTo (Domain AU) (Domain BU)";
  12.228 -    by (etac leadsTo_induct 1);
  12.229 -    by (full_simp_tac (simpset() addsimps [Domain_Union]) 3);
  12.230 -    by (blast_tac (claset() addIs [leadsTo_UN]) 3);
  12.231 -    by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
  12.232 -    by (rtac leadsTo_Basis 1);
  12.233 -    (*...and so CANNOT PROVE THIS*)
  12.234 -
  12.235 -
  12.236 -    (*This also seems impossible to prove??*)
  12.237 -    Goal "(Lcopy Rsh F : leadsTo (sharing Rsh A) (sharing Rsh B)) = \
  12.238 -    \     (F : leadsTo A B)";
  12.239 -**)
  12.240 -
  12.241 -
  12.242  (**** PPROD ****)
  12.243  
  12.244  (*** Basic properties ***)
  12.245 @@ -251,40 +16,20 @@
  12.246  qed "lift_set_iff";
  12.247  AddIffs [lift_set_iff];
  12.248  
  12.249 -Goalw [lift_act_def] "lift_act i (diag A) = (diag (lift_set i A))";
  12.250 +Goalw [lift_act_def] "lift_act i Id = Id";
  12.251  by Auto_tac;
  12.252 -qed "lift_act_diag";
  12.253 -Addsimps [lift_act_diag];
  12.254 +qed "lift_act_Id";
  12.255 +Addsimps [lift_act_Id];
  12.256  
  12.257 -Goalw [lift_prog_def] "States (lift_prog i F) = (lift_set i (States F))";
  12.258 +Goalw [lift_prog_def] "Init (lift_prog i F) = {f. f i : Init F}";
  12.259  by Auto_tac;
  12.260 -qed "States_lift_prog";
  12.261 -Addsimps [States_lift_prog];
  12.262 -
  12.263 -Goalw [lift_prog_def] "Init (lift_prog i F) = (lift_set i (Init F))";
  12.264 -by (auto_tac (claset() addIs [impOfSubs Init_subset_States], simpset()));
  12.265  qed "Init_lift_prog";
  12.266  Addsimps [Init_lift_prog];
  12.267  
  12.268 -Goalw [lift_act_def]
  12.269 -     "act : Acts F \
  12.270 -\     ==> lift_act i act <= lift_set i (States F) Times lift_set i (States F)";
  12.271 -by (force_tac (claset()  addIs [range_eqI, sym]
  12.272 -                    addDs [impOfSubs Acts_subset_Pow_States], 
  12.273 -              simpset()) 1);
  12.274 -qed "lift_act_subset_Times";
  12.275 -
  12.276  Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
  12.277 -by (auto_tac (claset() addIs [diag_in_Acts RSN (2,image_eqI)], 
  12.278 -	      simpset() addsimps [lift_act_subset_Times, 
  12.279 -				  image_subset_iff]));
  12.280 +by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
  12.281  qed "Acts_lift_prog";
  12.282  
  12.283 -Goalw [PPROD_def] "States (PPROD I F) = (INT i:I. lift_set i (States (F i)))";
  12.284 -by Auto_tac;
  12.285 -qed "States_PPROD";
  12.286 -Addsimps [States_PPROD];
  12.287 -
  12.288  Goalw [PPROD_def] "Init (PPROD I F) = (INT i:I. lift_set i (Init (F i)))";
  12.289  by Auto_tac;
  12.290  qed "Init_PPROD";
  12.291 @@ -296,12 +41,7 @@
  12.292  qed "lift_act_eq";
  12.293  AddIffs [lift_act_eq];
  12.294  
  12.295 -Goalw [eqStates_def] "eqStates I (%i. lift_prog i F)";
  12.296 -
  12.297 -Goalw [eqStates_def] "eqStates I (%i. lift_prog i (F i))";
  12.298 -
  12.299 -Goal "[| eqStates I (%i. lift_prog i (F i));  i: I |] \
  12.300 -\     ==> Acts (PPROD I F) = (UN i:I. lift_act i `` Acts (F i))";
  12.301 +Goal "i: I ==> Acts (PPROD I F) = (UN i:I. lift_act i `` Acts (F i))";
  12.302  by (auto_tac (claset(),
  12.303  	      simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN]));
  12.304  qed "Acts_PPROD";
  12.305 @@ -577,37 +317,6 @@
  12.306  
  12.307  (*** guarantees properties ***)
  12.308  
  12.309 -(*We only need act2=Id but the condition used is very weak*)
  12.310 -Goal "(x,y): act2 ==> fst_act (act1 Lcopy_act act2) = act1";
  12.311 -by (auto_tac (claset(), simpset() addsimps [fst_act_def, Lcopy_act_def]));
  12.312 -qed "fst_act_Lcopy_act";
  12.313 -Addsimps [fst_act_Lcopy_act];
  12.314 -
  12.315 -
  12.316 -Goal "(Lcopy Rsh F) Join G = Lcopy H ==> EX J. H = F Join J";
  12.317 -by (etac program_equalityE 1);
  12.318 -by (auto_tac (claset(), simpset() addsimps [Acts_Join]));
  12.319 -by (res_inst_tac 
  12.320 -     [("x", "mk_program(Domain (Init G), fst_act `` Acts G)")] exI 1);
  12.321 -by (rtac program_equalityI 1);
  12.322 -(*Init*)
  12.323 -by (simp_tac (simpset() addsimps [Acts_Join]) 1);
  12.324 -by (blast_tac (claset() addEs [equalityE]) 1);
  12.325 -(*Now for the Actions*)
  12.326 -by (dres_inst_tac [("f", "op `` fst_act")] arg_cong 1);
  12.327 -by (asm_full_simp_tac 
  12.328 -    (simpset() addsimps [insert_absorb, Acts_Lcopy, Acts_Join,
  12.329 -			 image_Un, image_compose RS sym, o_def]) 1);
  12.330 -qed "Lcopy_Join_eq_Lcopy_D";
  12.331 -
  12.332 -
  12.333 -Goal "F : X guarantees Y \
  12.334 -\     ==> Lcopy Rsh F : (Lcopy `` X) guarantees (Lcopy `` Y)";
  12.335 -by (rtac guaranteesI 1);
  12.336 -by Auto_tac;
  12.337 -by (blast_tac (claset() addDs [Lcopy_Join_eq_Lcopy_D, guaranteesD]) 1);
  12.338 -qed "Lcopy_guarantees";
  12.339 -
  12.340  
  12.341  Goal "drop_act i (lift_act i act) = act";
  12.342  by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI],
    13.1 --- a/src/HOL/UNITY/PPROD.thy	Mon Mar 01 18:37:52 1999 +0100
    13.2 +++ b/src/HOL/UNITY/PPROD.thy	Mon Mar 01 18:38:43 1999 +0100
    13.3 @@ -4,35 +4,14 @@
    13.4      Copyright   1998  University of Cambridge
    13.5  
    13.6  General products of programs (Pi operation), for replicating components.
    13.7 -Also merging of state sets.
    13.8 -
    13.9 -The idea of Rsh is to represent sharing in the Right part.
   13.10 -If x and y are states then (Rsh x y) updates y to agree with variables shared
   13.11 -with x.  Therefore Rsh x (Rsh x y) = Rsh x y.  The pair (x,y)
   13.12 -is a valid state of the composite program if and only if y = Rsh x y.
   13.13 -
   13.14 -Needs Rcopy; try to do by swapping (symmetry argument)
   13.15 -  instead of repeating all Lcopy proofs.
   13.16  *)
   13.17  
   13.18  PPROD = Union + Comp +
   13.19  
   13.20  constdefs
   13.21  
   13.22 -  sharing :: "[['a,'b]=>'b, 'a set] => ('a*'b) set"
   13.23 -    "sharing Rsh A == SIGMA x: A. range (Rsh x)"
   13.24 -
   13.25 -  Lcopy_act :: "[['a,'b]=>'b, ('a*'a) set] => (('a*'b) * ('a*'b)) set"
   13.26 -    "Lcopy_act Rsh act == {((x,y),(x',y')). (x,x'): act & Rsh x y = y &
   13.27 -			                    Rsh x' y = y'}"
   13.28 -
   13.29 -  fst_act :: "(('a*'b) * ('a*'b)) set => ('a*'a) set"
   13.30 -    "fst_act act == (%((x,y),(x',y')). (x,x')) `` act"
   13.31 -
   13.32 -  Lcopy :: "[['a,'b]=>'b, 'a program] => ('a*'b) program"
   13.33 -    "Lcopy Rsh F == mk_program (sharing Rsh (States F),
   13.34 -			        sharing Rsh (Init F),
   13.35 -			        Lcopy_act Rsh `` Acts F)"
   13.36 +  (**possible to force all acts to be included in common initial state
   13.37 +      (by intersection) ??*)
   13.38  
   13.39    lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
   13.40      "lift_act i act == {(f,f'). EX s'. f' = f(i:=s') & (f i, s') : act}"
   13.41 @@ -45,8 +24,7 @@
   13.42  
   13.43    lift_prog :: "['a, 'b program] => ('a => 'b) program"
   13.44      "lift_prog i F ==
   13.45 -       mk_program (lift_set i (States F),
   13.46 -		   lift_set i (Init F),
   13.47 +       mk_program (lift_set i (Init F),
   13.48  		   lift_act i `` Acts F)"
   13.49  
   13.50    (*products of programs*)
   13.51 @@ -59,12 +37,4 @@
   13.52  translations
   13.53    "PPI x:A. B"   == "PPROD A (%x. B)"
   13.54  
   13.55 -
   13.56 -locale Share =
   13.57 -  fixes 
   13.58 -    Rsh	:: ['a,'b]=>'b
   13.59 -  assumes
   13.60 -    (*the last update (from the other side) takes precedence*)
   13.61 -    overwrite "Rsh x (Rsh x' y) = Rsh x y"
   13.62 -
   13.63  end
    14.1 --- a/src/HOL/UNITY/ROOT.ML	Mon Mar 01 18:37:52 1999 +0100
    14.2 +++ b/src/HOL/UNITY/ROOT.ML	Mon Mar 01 18:38:43 1999 +0100
    14.3 @@ -29,7 +29,8 @@
    14.4  time_use_thy "Comp";
    14.5  time_use_thy "Client";
    14.6  (**
    14.7 -time_use_thy "PPX";
    14.8 +time_use_thy "Extend";
    14.9 +time_use_thy "PPROD";
   14.10  **)
   14.11  
   14.12  add_path "../Auth";	(*to find Public.thy*)
    15.1 --- a/src/HOL/UNITY/Reach.thy	Mon Mar 01 18:37:52 1999 +0100
    15.2 +++ b/src/HOL/UNITY/Reach.thy	Mon Mar 01 18:38:43 1999 +0100
    15.3 @@ -24,7 +24,7 @@
    15.4      "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
    15.5  
    15.6    Rprg :: state program
    15.7 -    "Rprg == mk_program (UNIV, {%v. v=init}, UN (u,v): edges. {asgt u v})"
    15.8 +    "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})"
    15.9  
   15.10    reach_invariant :: state set
   15.11      "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
    16.1 --- a/src/HOL/UNITY/SubstAx.ML	Mon Mar 01 18:37:52 1999 +0100
    16.2 +++ b/src/HOL/UNITY/SubstAx.ML	Mon Mar 01 18:38:43 1999 +0100
    16.3 @@ -79,7 +79,7 @@
    16.4  
    16.5  val prems = 
    16.6  Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (UN i:I. A i) B";
    16.7 -by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
    16.8 +by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
    16.9  by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
   16.10  qed "LeadsTo_UN";
   16.11  
   16.12 @@ -190,7 +190,7 @@
   16.13  val prems = 
   16.14  Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \
   16.15  \     ==> F : LeadsTo (UN i:I. A i) (UN i:I. A' i)";
   16.16 -by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
   16.17 +by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
   16.18  by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
   16.19                          addIs prems) 1);
   16.20  qed "LeadsTo_UN_UN";
    17.1 --- a/src/HOL/UNITY/Traces.ML	Mon Mar 01 18:37:52 1999 +0100
    17.2 +++ b/src/HOL/UNITY/Traces.ML	Mon Mar 01 18:38:43 1999 +0100
    17.3 @@ -10,110 +10,41 @@
    17.4  *)
    17.5  
    17.6  
    17.7 +
    17.8  (*** The abstract type of programs ***)
    17.9  
   17.10 -Goalw [restrict_rel_def] "restrict_rel A Id = diag A";
   17.11 -by (Blast_tac 1);
   17.12 -qed "restrict_rel_Id";
   17.13 -Addsimps [restrict_rel_Id];
   17.14 -
   17.15 -Goalw [restrict_rel_def] "restrict_rel A (diag B) = diag (A Int B)";
   17.16 -by (Blast_tac 1);
   17.17 -qed "restrict_rel_diag";
   17.18 -Addsimps [restrict_rel_diag];
   17.19 -
   17.20 -Goalw [restrict_rel_def]
   17.21 -    "restrict_rel A (restrict_rel B r) = restrict_rel (A Int B) r";
   17.22 -by (Blast_tac 1);
   17.23 -qed "restrict_rel_restrict_rel";
   17.24 -Addsimps [restrict_rel_restrict_rel];
   17.25 -
   17.26 -Goalw [restrict_rel_def] "restrict_rel A r <= A Times A";
   17.27 -by (Blast_tac 1);
   17.28 -qed "restrict_rel_subset";
   17.29 -Addsimps [restrict_rel_subset];
   17.30 -
   17.31 -Goalw [restrict_rel_def]
   17.32 -    "((x,y) : restrict_rel A r) = ((x,y): r & x: A & y: A)";
   17.33 -by (Blast_tac 1);
   17.34 -qed "restrict_rel_iff";
   17.35 -Addsimps [restrict_rel_iff];
   17.36 -
   17.37 -Goalw [restrict_rel_def] "r <= A Times A ==> restrict_rel A r = r";
   17.38 -by (Blast_tac 1);
   17.39 -qed "restrict_rel_eq";
   17.40 -Addsimps [restrict_rel_eq];
   17.41 -
   17.42 -Goal "acts <= Pow (A Times A) ==> restrict_rel A `` acts = acts";
   17.43 -by Auto_tac;
   17.44 -by (rtac image_eqI 1);
   17.45 -by (assume_tac 2);
   17.46 -by (set_mp_tac 1);
   17.47 -by (Force_tac 1);
   17.48 -qed "restrict_rel_image";
   17.49 -
   17.50 -Goalw [restrict_rel_def] "Domain (restrict_rel A r) <= A Int Domain r";
   17.51 -by (Blast_tac 1);
   17.52 -qed "Domain_restrict_rel";
   17.53 -
   17.54 -Goalw [restrict_rel_def] "restrict_rel A r ^^ B <= A Int (r ^^ B)";
   17.55 -by (Blast_tac 1);
   17.56 -qed "Image_restrict_rel";
   17.57 -
   17.58 -Addsimps [diag_iff];
   17.59 -
   17.60  val rep_ss = simpset() addsimps 
   17.61 -                [Int_lower1, image_subset_iff, diag_subset_Times,
   17.62 -		 States_def, Init_def, Acts_def, 
   17.63 -		 mk_program_def, Program_def, Rep_Program, 
   17.64 +                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
   17.65  		 Rep_Program_inverse, Abs_Program_inverse];
   17.66  
   17.67  
   17.68 -(** Basic laws guaranteed by the abstract type "program" **)
   17.69 -
   17.70 -Goal "Init F <= States F";
   17.71 +Goal "Id : Acts F";
   17.72  by (cut_inst_tac [("x", "F")] Rep_Program 1);
   17.73  by (auto_tac (claset(), rep_ss));
   17.74 -qed "Init_subset_States";
   17.75 -
   17.76 -Goal "Acts F <= Pow(States F Times States F)";
   17.77 -by (cut_inst_tac [("x", "F")] Rep_Program 1);
   17.78 -by (force_tac (claset(),rep_ss) 1);
   17.79 -qed "Acts_subset_Pow_States";
   17.80 +qed "Id_in_Acts";
   17.81 +AddIffs [Id_in_Acts];
   17.82  
   17.83 -Goal "diag (States F) : Acts F";
   17.84 -by (cut_inst_tac [("x", "F")] Rep_Program 1);
   17.85 -by (auto_tac (claset(), rep_ss));
   17.86 -qed "diag_in_Acts";
   17.87 -AddIffs [diag_in_Acts];
   17.88 -
   17.89 +Goal "insert Id (Acts F) = Acts F";
   17.90 +by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
   17.91 +qed "insert_Id_Acts";
   17.92 +AddIffs [insert_Id_Acts];
   17.93  
   17.94  (** Inspectors for type "program" **)
   17.95  
   17.96 -Goal "States (mk_program (states,init,acts)) = states";
   17.97 -by (auto_tac (claset(), rep_ss));
   17.98 -qed "States_eq";
   17.99 -
  17.100 -Goal "Init (mk_program (states,init,acts)) = states Int init";
  17.101 +Goal "Init (mk_program (init,acts)) = init";
  17.102  by (auto_tac (claset(), rep_ss));
  17.103  qed "Init_eq";
  17.104  
  17.105 -Goal "Acts (mk_program (states,init,acts)) = \
  17.106 -\     insert (diag states) (restrict_rel states `` acts)";
  17.107 +Goal "Acts (mk_program (init,acts)) = insert Id acts";
  17.108  by (auto_tac (claset(), rep_ss));
  17.109 -qed "Acts_eq_raw";
  17.110 -
  17.111 -Goal "acts <= Pow(states Times states) \
  17.112 -\     ==> Acts (mk_program (states,init,acts)) = insert (diag states) acts";
  17.113 -by (asm_simp_tac (simpset() addsimps [Acts_eq_raw, restrict_rel_image]) 1);
  17.114  qed "Acts_eq";
  17.115  
  17.116 -Addsimps [States_eq, Acts_eq, Init_eq];
  17.117 +Addsimps [Acts_eq, Init_eq];
  17.118  
  17.119  
  17.120  (** The notation of equality for type "program" **)
  17.121  
  17.122 -Goal "[| States F = States G; Init F = Init G; Acts F = Acts G |] ==> F = G";
  17.123 +Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
  17.124  by (subgoals_tac ["EX x. Rep_Program F = x",
  17.125  		  "EX x. Rep_Program G = x"] 1);
  17.126  by (REPEAT (Blast_tac 2));
  17.127 @@ -124,38 +55,26 @@
  17.128  qed "program_equalityI";
  17.129  
  17.130  val [major,minor] =
  17.131 -Goal "[| F = G; \
  17.132 -\        [| States F = States G; Init F = Init G; Acts F = Acts G |] ==> P \
  17.133 -\     |] ==> P";
  17.134 +Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
  17.135  by (rtac minor 1);
  17.136  by (auto_tac (claset(), simpset() addsimps [major]));
  17.137  qed "program_equalityE";
  17.138  
  17.139 +
  17.140  (*** These rules allow "lazy" definition expansion 
  17.141       They avoid expanding the full program, which is a large expression
  17.142  ***)
  17.143  
  17.144 -Goal "[| F == mk_program (states,init,acts) |] \
  17.145 -\     ==> States F = states";
  17.146 -by Auto_tac;
  17.147 -qed "def_prg_States";
  17.148 -
  17.149 -Goal "[| F == mk_program (states,init,acts); init <= states |] \
  17.150 -\     ==> Init F = init";
  17.151 +Goal "F == mk_program (init,acts) ==> Init F = init";
  17.152  by Auto_tac;
  17.153  qed "def_prg_Init";
  17.154  
  17.155 -Goal "[| F == mk_program (states,init,acts); \
  17.156 -\        acts <= Pow(states Times states) |] \
  17.157 -\     ==> Acts F = insert (diag states) acts";
  17.158 -by (asm_simp_tac (simpset() addsimps [restrict_rel_image]) 1);
  17.159 -qed "def_prg_Acts";
  17.160 -
  17.161  (*The program is not expanded, but its Init and Acts are*)
  17.162 -Goal "[| F == mk_program (states,init,acts); \
  17.163 -\        init <= states;  acts <= Pow(states Times states) |] \
  17.164 -\     ==> Init F = init & Acts F = insert (diag states) acts";
  17.165 -by (asm_simp_tac (HOL_ss addsimps [def_prg_Init, def_prg_Acts]) 1);
  17.166 +val [rew] = goal thy
  17.167 +    "[| F == mk_program (init,acts) |] \
  17.168 +\    ==> Init F = init & Acts F = insert Id acts";
  17.169 +by (rewtac rew);
  17.170 +by Auto_tac;
  17.171  qed "def_prg_simps";
  17.172  
  17.173  (*An action is expanded only if a pair of states is being tested against it*)
  17.174 @@ -175,13 +94,6 @@
  17.175  
  17.176  (*** traces and reachable ***)
  17.177  
  17.178 -Goal "reachable F <= States F";
  17.179 -by Safe_tac;
  17.180 -by (etac reachable.induct 1);
  17.181 -by (blast_tac (claset() addDs [impOfSubs Acts_subset_Pow_States]) 2);
  17.182 -by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1);
  17.183 -qed "reachable_subset_States";
  17.184 -
  17.185  Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
  17.186  by Safe_tac;
  17.187  by (etac traces.induct 2);
    18.1 --- a/src/HOL/UNITY/Traces.thy	Mon Mar 01 18:37:52 1999 +0100
    18.2 +++ b/src/HOL/UNITY/Traces.thy	Mon Mar 01 18:38:43 1999 +0100
    18.3 @@ -25,32 +25,17 @@
    18.4  
    18.5  
    18.6  typedef (Program)
    18.7 -  'a program = "{(states :: 'a set,
    18.8 -		  init   :: 'a set,
    18.9 -		  acts   :: ('a * 'a)set set).
   18.10 -		 init <= states &
   18.11 -		 acts <= Pow(states Times states) &
   18.12 -		 diag states : acts}"
   18.13 +  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
   18.14  
   18.15  constdefs
   18.16 -  restrict_rel :: "['a set, ('a * 'a) set] => ('a * 'a) set"
   18.17 -    "restrict_rel A r == (A Times A) Int r"
   18.18 -
   18.19 -  mk_program :: "('a set * 'a set * ('a * 'a)set set) => 'a program"
   18.20 -    "mk_program ==
   18.21 -       %(states, init, acts).
   18.22 -	Abs_Program (states,
   18.23 -		     states Int init,
   18.24 -		     restrict_rel states `` (insert Id acts))"
   18.25 -
   18.26 -  States :: "'a program => 'a set"
   18.27 -    "States F == (%(states, init, acts). states) (Rep_Program F)"
   18.28 +    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
   18.29 +    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
   18.30  
   18.31    Init :: "'a program => 'a set"
   18.32 -    "Init F == (%(states, init, acts). init) (Rep_Program F)"
   18.33 +    "Init F == (%(init, acts). init) (Rep_Program F)"
   18.34  
   18.35    Acts :: "'a program => ('a * 'a)set set"
   18.36 -    "Acts F == (%(states, init, acts). acts) (Rep_Program F)"
   18.37 +    "Acts F == (%(init, acts). acts) (Rep_Program F)"
   18.38  
   18.39  
   18.40  consts reachable :: "'a program => 'a set"
    19.1 --- a/src/HOL/UNITY/UNITY.ML	Mon Mar 01 18:37:52 1999 +0100
    19.2 +++ b/src/HOL/UNITY/UNITY.ML	Mon Mar 01 18:38:43 1999 +0100
    19.3 @@ -14,11 +14,6 @@
    19.4  
    19.5  (*** General lemmas ***)
    19.6  
    19.7 -    Goal "Pow UNIV = UNIV";
    19.8 -    by (Blast_tac 1);
    19.9 -    qed "Pow_UNIV";
   19.10 -    Addsimps [Pow_UNIV];
   19.11 -
   19.12  Goal "UNIV Times UNIV = UNIV";
   19.13  by Auto_tac;
   19.14  qed "UNIV_Times_UNIV"; 
   19.15 @@ -106,23 +101,23 @@
   19.16  by (Blast_tac 1);
   19.17  qed "ball_constrains_INT";
   19.18  
   19.19 -Goalw [constrains_def] "[| F : constrains A A'; A <= States F |] ==> A <= A'";
   19.20 -by (Force_tac 1);
   19.21 +Goalw [constrains_def] "F : constrains A A' ==> A <= A'";
   19.22 +by Auto_tac;
   19.23  qed "constrains_imp_subset";
   19.24  
   19.25  (*The reasoning is by subsets since "constrains" refers to single actions
   19.26    only.  So this rule isn't that useful.*)
   19.27 -Goal "[| F : constrains A B; F : constrains B C; B <= States F |]   \
   19.28 +Goalw [constrains_def]
   19.29 +    "[| F : constrains A B; F : constrains B C |]   \
   19.30  \    ==> F : constrains A C";
   19.31 -by (etac constrains_weaken_R 1);
   19.32 -by (etac constrains_imp_subset 1);
   19.33 -by (assume_tac 1);
   19.34 +by (Blast_tac 1);
   19.35  qed "constrains_trans";
   19.36  
   19.37 -Goal "[| F : constrains A (A' Un B); F : constrains B B'; B <= States F|] \
   19.38 -\     ==> F : constrains A (A' Un B')";
   19.39 -by (etac constrains_weaken_R 1);
   19.40 -by (blast_tac (claset() addDs [impOfSubs constrains_imp_subset]) 1);
   19.41 +Goalw [constrains_def]
   19.42 +   "[| F : constrains A (A' Un B); F : constrains B B' |] \
   19.43 +\   ==> F : constrains A (A' Un B')";
   19.44 +by (Clarify_tac 1);
   19.45 +by (Blast_tac 1);
   19.46  qed "constrains_cancel";
   19.47  
   19.48  
    20.1 --- a/src/HOL/UNITY/Union.ML	Mon Mar 01 18:37:52 1999 +0100
    20.2 +++ b/src/HOL/UNITY/Union.ML	Mon Mar 01 18:38:43 1999 +0100
    20.3 @@ -8,6 +8,7 @@
    20.4  From Misra's Chapter 5: Asynchronous Compositions of Programs
    20.5  *)
    20.6  
    20.7 +
    20.8  Goal "k:I ==> (INT i:I. A i) Int A k = (INT i:I. A i)";
    20.9  by (Blast_tac 1);
   20.10  qed "INT_absorb2";
   20.11 @@ -17,23 +18,20 @@
   20.12  
   20.13  Addcongs [UN_cong, INT_cong];
   20.14  
   20.15 +
   20.16  (** SKIP **)
   20.17  
   20.18 -Goal "States (SKIP A) = A";
   20.19 -by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   20.20 -qed "States_SKIP";
   20.21 -
   20.22 -Goal "Init (SKIP A) = A";
   20.23 +Goal "Init SKIP = UNIV";
   20.24  by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   20.25  qed "Init_SKIP";
   20.26  
   20.27 -Goal "Acts (SKIP A) = {diag A}";
   20.28 +Goal "Acts SKIP = {Id}";
   20.29  by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   20.30  qed "Acts_SKIP";
   20.31  
   20.32 -Addsimps [States_SKIP, Init_SKIP, Acts_SKIP];
   20.33 +Addsimps [Init_SKIP, Acts_SKIP];
   20.34  
   20.35 -Goal "reachable (SKIP A) = A";
   20.36 +Goal "reachable SKIP = UNIV";
   20.37  by (force_tac (claset() addEs [reachable.induct]
   20.38  			addIs reachable.intrs, simpset()) 1);
   20.39  qed "reachable_SKIP";
   20.40 @@ -43,90 +41,47 @@
   20.41  
   20.42  (** Join **)
   20.43  
   20.44 -Goal "States (F Join G) = States F Int States G";
   20.45 +Goal "Init (F Join G) = Init F Int Init G";
   20.46  by (simp_tac (simpset() addsimps [Join_def]) 1);
   20.47 -qed "States_Join";
   20.48 -
   20.49 -Goal "Init (F Join G) = Init F Int Init G";
   20.50 -by (auto_tac (claset() addIs [impOfSubs Init_subset_States],
   20.51 -	      simpset() addsimps [Join_def]));
   20.52  qed "Init_Join";
   20.53  
   20.54 -Goal "States F = States G ==> Acts (F Join G) = Acts F Un Acts G";
   20.55 -by (subgoal_tac "Acts F Un Acts G <= Pow (States G Times States G)" 1);
   20.56 -by (blast_tac (claset() addEs [equalityE] 
   20.57 -                        addDs [impOfSubs Acts_subset_Pow_States]) 2);
   20.58 +Goal "Acts (F Join G) = Acts F Un Acts G";
   20.59  by (auto_tac (claset(), simpset() addsimps [Join_def]));
   20.60  qed "Acts_Join";
   20.61  
   20.62 +Addsimps [Init_Join];
   20.63 +
   20.64  
   20.65  (** JN **)
   20.66  
   20.67 -Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP UNIV";
   20.68 +Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP";
   20.69  by Auto_tac;
   20.70  qed "JN_empty";
   20.71  Addsimps [JN_empty];
   20.72  
   20.73 -Goal "States (JN i:I. F i) = (INT i:I. States (F i))";
   20.74 -by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   20.75 -qed "States_JN";
   20.76 +Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
   20.77 +by (rtac program_equalityI 1);
   20.78 +by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
   20.79 +qed "JN_insert";
   20.80 +Addsimps[JN_empty, JN_insert];
   20.81  
   20.82  Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))";
   20.83 -by (auto_tac (claset() addIs [impOfSubs Init_subset_States],
   20.84 -	      simpset() addsimps [JOIN_def]));
   20.85 +by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   20.86  qed "Init_JN";
   20.87  
   20.88 -(*If I={} then the LHS is (SKIP UNIV) while the RHS is {}.*)
   20.89 -Goalw [eqStates_def]
   20.90 -     "[| eqStates I F; i: I |] ==> Acts (JN i:I. F i) = (UN i:I. Acts (F i))";
   20.91 -by (Clarify_tac 1);
   20.92 -by (subgoal_tac "(UN i:I. Acts (F i)) <= Pow (St Times St)" 1);
   20.93 -by (blast_tac (claset() addEs [equalityE] 
   20.94 -                        addDs [impOfSubs Acts_subset_Pow_States]) 2);
   20.95 +Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))";
   20.96  by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
   20.97  qed "Acts_JN";
   20.98  
   20.99 -Goal "eqStates I F \
  20.100 -\     ==> Acts (JN i:I. F i) = \
  20.101 -\         (if I={} then {diag UNIV} else (UN i:I. Acts (F i)))";
  20.102 -by (force_tac (claset(), simpset() addsimps [Acts_JN]) 1);
  20.103 -qed "Acts_JN_if";
  20.104 -
  20.105 -Addsimps [States_Join, Init_Join, States_JN, Init_JN];
  20.106 -
  20.107 -
  20.108 -Goal "(JN x:insert j I. F x) = (F j) Join (JN x:I. F x)";
  20.109 -by (rtac program_equalityI 1);
  20.110 -by (ALLGOALS Asm_simp_tac);
  20.111 -by (asm_simp_tac 
  20.112 -    (simpset() addsimps [JOIN_def, Join_def, Acts_eq_raw,
  20.113 -			 image_UNION, image_Un, image_image, Int_assoc]) 1);
  20.114 -qed "JN_insert";
  20.115 -Addsimps[JN_insert];
  20.116 +Addsimps [Init_JN];
  20.117  
  20.118 -Goal "k:I ==> A k Join (JN i:I. A i) = (JN i:I. A i)";
  20.119 -by (stac (JN_insert RS sym) 1);
  20.120 -by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
  20.121 -qed "JN_absorb";
  20.122 -
  20.123 -
  20.124 -Goalw [eqStates_def] "eqStates {} F";
  20.125 -by (Simp_tac 1);
  20.126 -qed "eqStates_empty";
  20.127 +val prems = Goalw [JOIN_def]
  20.128 +    "[| A=B;  !!x. x:B ==> F(x) = G(x) |] ==> \
  20.129 +\    (JN x:A. F(x)) = (JN x:B. G(x))";
  20.130 +by (asm_simp_tac (simpset() addsimps prems) 1);
  20.131 +qed "JN_cong";
  20.132  
  20.133 -Goalw [eqStates_def]
  20.134 -    "[| eqStates I F; States (F i) = (INT i: I. States (F i)) |] \
  20.135 -\    ==> eqStates (insert i I) F";
  20.136 -by Auto_tac;
  20.137 -qed "eqStates_insertI";
  20.138 -
  20.139 -Goalw [eqStates_def]
  20.140 -    "eqStates (insert i I) F = \
  20.141 -\    (eqStates I F & (I={} | States (F i) = (INT i: I. States (F i))))";
  20.142 -by Auto_tac;
  20.143 -qed "eqStates_insert_eq";
  20.144 -
  20.145 -Addsimps [eqStates_empty, eqStates_insert_eq];
  20.146 +Addcongs [JN_cong];
  20.147  
  20.148  
  20.149  (** Algebraic laws **)
  20.150 @@ -136,97 +91,86 @@
  20.151  qed "Join_commute";
  20.152  
  20.153  Goal "(F Join G) Join H = F Join (G Join H)";
  20.154 -by (rtac program_equalityI 1);
  20.155 -by (ALLGOALS (asm_simp_tac (simpset() addsimps Un_ac@[Int_assoc])));
  20.156 -by (asm_simp_tac 
  20.157 -    (simpset() addsimps Un_ac@Int_ac@[Join_def, Acts_eq_raw,
  20.158 -				      image_Un, image_image]) 1);
  20.159 -by (Blast_tac 1);
  20.160 +by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
  20.161  qed "Join_assoc";
  20.162   
  20.163 -Goalw [Join_def, SKIP_def] "States F <= A ==> (SKIP A) Join F = F";
  20.164 +Goalw [Join_def, SKIP_def] "SKIP Join F = F";
  20.165  by (rtac program_equalityI 1);
  20.166 -by (ALLGOALS
  20.167 -    (asm_simp_tac (simpset() addsimps 
  20.168 -		   Int_ac@[Acts_subset_Pow_States RS restrict_rel_image, 
  20.169 -			   Acts_eq_raw, insert_absorb, Int_absorb1])));
  20.170 -by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1);
  20.171 +by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
  20.172  qed "Join_SKIP_left";
  20.173  
  20.174 -Goal "States F <= A ==> F Join (SKIP A) = F";
  20.175 -by (stac Join_commute 1);
  20.176 -by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1);
  20.177 +Goalw [Join_def, SKIP_def] "F Join SKIP = F";
  20.178 +by (rtac program_equalityI 1);
  20.179 +by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
  20.180  qed "Join_SKIP_right";
  20.181  
  20.182  Addsimps [Join_SKIP_left, Join_SKIP_right];
  20.183  
  20.184  Goalw [Join_def] "F Join F = F";
  20.185  by (rtac program_equalityI 1);
  20.186 -by (ALLGOALS
  20.187 -    (asm_simp_tac (simpset() addsimps 
  20.188 -		   [insert_absorb, Acts_subset_Pow_States RS Acts_eq])));
  20.189 -by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1);
  20.190 +by Auto_tac;
  20.191  qed "Join_absorb";
  20.192  
  20.193  Addsimps [Join_absorb];
  20.194  
  20.195 +
  20.196 +
  20.197 +(*** JN laws ***)
  20.198 +
  20.199 +
  20.200 +
  20.201 +Goal "i : I ==> (JN i:I. A i Join B) = ((JN i:I. A i) Join B)";
  20.202 +by (auto_tac (claset() addSIs [program_equalityI],
  20.203 +	      simpset() addsimps [Acts_JN, Acts_Join]));
  20.204 +qed "JN_Join_miniscope";
  20.205 +
  20.206 +Goal "k:I ==> A k Join (JN i:I. A i) = (JN i:I. A i)";
  20.207 +by (auto_tac (claset() addSIs [program_equalityI],
  20.208 +	      simpset() addsimps [Acts_JN, Acts_Join]));
  20.209 +qed "JN_absorb";
  20.210 +
  20.211  Goal "(JN i: I Un J. A i) = ((JN i: I. A i) Join (JN i:J. A i))";
  20.212 -by (rtac program_equalityI 1);
  20.213 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [INT_Un])));
  20.214 -by (asm_simp_tac 
  20.215 -    (simpset() addsimps Int_ac@
  20.216 -                        [JOIN_def, Join_def, Acts_eq_raw, UN_Un, INT_Un, 
  20.217 -			 image_UNION, image_Un, image_image]) 1);
  20.218 +by (auto_tac (claset() addSIs [program_equalityI],
  20.219 +	      simpset() addsimps [Acts_JN, Acts_Join]));
  20.220  qed "JN_Join";
  20.221  
  20.222  Goal "i: I ==> (JN i:I. c) = c";
  20.223  by (auto_tac (claset() addSIs [program_equalityI],
  20.224 -	      simpset() addsimps [Acts_JN, eqStates_def]));
  20.225 +	      simpset() addsimps [Acts_JN]));
  20.226  qed "JN_constant";
  20.227  
  20.228  Goal "(JN i:I. A i Join B i) = (JN i:I. A i)  Join  (JN i:I. B i)";
  20.229 -by (rtac program_equalityI 1);
  20.230 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [INT_Int_distrib])));
  20.231 -by (asm_simp_tac 
  20.232 -    (simpset() addsimps [JOIN_def, Join_def, Acts_eq_raw, image_UNION, 
  20.233 -			 rinst [("A","%x. States (A x) Int States (B x)")] 
  20.234 -			     INT_absorb2, 
  20.235 -			 image_Un, image_image]) 1);
  20.236 -by (asm_simp_tac (simpset() addsimps [INT_Int_distrib RS sym] @ Int_ac) 1);
  20.237 -by (Blast_tac 1);
  20.238 +by (auto_tac (claset() addSIs [program_equalityI],
  20.239 +	      simpset() addsimps [Acts_JN, Acts_Join]));
  20.240  qed "JN_Join_distrib";
  20.241  
  20.242 -Goal "i : I ==> (JN i:I. A i Join B) = ((JN i:I. A i) Join B)";
  20.243 -by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1);
  20.244 -qed "JN_Join_miniscope";
  20.245 -
  20.246  
  20.247  (*** Safety: constrains, stable, FP ***)
  20.248  
  20.249 -Goal "[| F : constrains A B;  G : constrains A B |] \
  20.250 -\     ==> F Join G : constrains A B";
  20.251 -by (auto_tac (claset(),
  20.252 -	      simpset() addsimps [constrains_def, Join_def, Acts_eq_raw, 
  20.253 -				  image_Un]));
  20.254 -by (REPEAT (force_tac (claset() addSEs [ballE], simpset()) 1));
  20.255 -qed "constrains_imp_Join_constrains";
  20.256 +Goalw [constrains_def, JOIN_def]
  20.257 +    "i : I ==> \
  20.258 +\    (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
  20.259 +by (Simp_tac 1);
  20.260 +by (Blast_tac 1);
  20.261 +qed "constrains_JN";
  20.262  
  20.263 -Goal "States F = States G ==> \
  20.264 -\     F Join G : constrains A B = (F : constrains A B & G : constrains A B)";
  20.265 -by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
  20.266 +Goal "F Join G : constrains A B =  \
  20.267 +\     (F : constrains A B & G : constrains A B)";
  20.268 +by (auto_tac
  20.269 +    (claset(),
  20.270 +     simpset() addsimps [constrains_def, Join_def]));
  20.271  qed "constrains_Join";
  20.272  
  20.273  Goal "[| i : I;  ALL i:I. F i : constrains A B |] \
  20.274  \     ==> (JN i:I. F i) : constrains A B";
  20.275 -by (full_simp_tac (simpset() addsimps [constrains_def, JOIN_def, Acts_eq_raw, 
  20.276 -				  image_Un]) 1);
  20.277 -by Safe_tac;
  20.278 -by (REPEAT (force_tac (claset() addSEs [ballE], simpset()) 1));
  20.279 +by (full_simp_tac (simpset() addsimps [constrains_def, Acts_JN]) 1);
  20.280 +by (Blast_tac 1);
  20.281  qed "constrains_imp_JN_constrains";
  20.282  
  20.283 -Goal "[| i : I;  eqStates I F |] \
  20.284 +Goal "[| i : I;  compatible (F``I) |] \
  20.285  \     ==> (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
  20.286 -by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_JN]));
  20.287 +by (asm_simp_tac (simpset() addsimps [constrains_def, Acts_JN]) 1);
  20.288 +by (Blast_tac 1);
  20.289  qed "constrains_JN";
  20.290  
  20.291      (**FAILS, I think; see 5.4.1, Substitution Axiom.
  20.292 @@ -246,114 +190,89 @@
  20.293      qed "Constrains_Join";
  20.294      **)
  20.295  
  20.296 -Goal "[| F : constrains A A';  G : constrains B B';  States F = States G |] \
  20.297 +
  20.298 +Goal "[| F : constrains A A';  G : constrains B B' |] \
  20.299  \     ==> F Join G : constrains (A Int B) (A' Un B')";
  20.300 -by (asm_simp_tac (simpset() addsimps [constrains_Join]) 1);
  20.301 +by (simp_tac (simpset() addsimps [constrains_Join]) 1);
  20.302  by (blast_tac (claset() addIs [constrains_weaken]) 1);
  20.303  qed "constrains_Join_weaken";
  20.304  
  20.305 -Goal "[| i : I;  eqStates I F |]  \
  20.306 -\     ==> (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
  20.307 +Goal "i : I ==> \
  20.308 +\     (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
  20.309  by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
  20.310  qed "stable_JN";
  20.311  
  20.312 -Goal "[| ALL i:I. F i : invariant A;  i : I;  eqStates I F |]  \
  20.313 +Goal "[| ALL i:I. F i : invariant A;  i : I |]  \
  20.314  \      ==> (JN i:I. F i) : invariant A";
  20.315  by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_JN]) 1);
  20.316  by (Blast_tac 1);
  20.317  bind_thm ("invariant_JN_I", ballI RS result());
  20.318  
  20.319 -Goal "States F = States G \
  20.320 -\     ==> F Join G : stable A = (F : stable A & G : stable A)";
  20.321 -by (asm_simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
  20.322 +Goal "F Join G : stable A = \
  20.323 +\     (F : stable A & G : stable A)";
  20.324 +by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
  20.325  qed "stable_Join";
  20.326  
  20.327 -Goal "[| F : invariant A; G : invariant A; States F = States G |]  \
  20.328 +Goal "[| F : invariant A; G : invariant A |]  \
  20.329  \     ==> F Join G : invariant A";
  20.330 -by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1);
  20.331 +by (full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1);
  20.332  by (Blast_tac 1);
  20.333  qed "invariant_JoinI";
  20.334  
  20.335 -Goal "[| i : I;  eqStates I F |]  \
  20.336 -\      ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
  20.337 +Goal "i : I ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
  20.338  by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
  20.339  qed "FP_JN";
  20.340  
  20.341  
  20.342  (*** Progress: transient, ensures ***)
  20.343  
  20.344 -
  20.345 -Goal "[| (JN i:I. F i) : transient A;  i: I |] ==> EX i:I. F i : transient A";
  20.346 -by (full_simp_tac (simpset() addsimps [transient_def, JOIN_def, Acts_eq_raw, 
  20.347 -				  Int_absorb1, restrict_rel_def]) 1);
  20.348 -by Safe_tac;
  20.349 -by (REPEAT (blast_tac (claset() addSIs [rev_bexI]) 1));
  20.350 -qed "transient_JN_imp_transient";
  20.351 -
  20.352 -Goal "[| i : I;  eqStates I F |]  \
  20.353 -\     ==> (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
  20.354 -by (auto_tac (claset() addSIs [transient_JN_imp_transient], simpset()));
  20.355 -by (auto_tac (claset(), simpset() addsimps [transient_def, Acts_JN]));
  20.356 +Goal "i : I ==> \
  20.357 +\   (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
  20.358 +by (auto_tac (claset(),
  20.359 +	      simpset() addsimps [transient_def, JOIN_def]));
  20.360  qed "transient_JN";
  20.361  
  20.362 -Goal "F Join G : transient A ==> \
  20.363 -\     F : transient A | G : transient A";
  20.364 -by (full_simp_tac (simpset() addsimps [transient_def, Join_def, Acts_eq_raw, 
  20.365 -				       restrict_rel_def]) 1);
  20.366 -by Safe_tac;
  20.367 -(*delete act:Acts F possibility*)
  20.368 -by (rtac FalseE 3);  
  20.369 -(*delete act:Acts G possibility*)
  20.370 -by (thin_tac "~ (EX act:Acts G. ?P act)" 2);
  20.371 -by (REPEAT (blast_tac (claset() addSIs [rev_bexI]) 1));
  20.372 -qed "transient_Join_imp_transient";
  20.373 -
  20.374 -Goal "States F = States G  \
  20.375 -\     ==> (F Join G : transient A) = (F : transient A | G : transient A)";
  20.376 -by (auto_tac (claset() addSIs [transient_Join_imp_transient], simpset()));
  20.377 -by (auto_tac (claset(), simpset() addsimps [transient_def, Acts_Join]));
  20.378 +Goal "F Join G : transient A = \
  20.379 +\     (F : transient A | G : transient A)";
  20.380 +by (auto_tac (claset(),
  20.381 +	      simpset() addsimps [bex_Un, transient_def,
  20.382 +				  Join_def]));
  20.383  qed "transient_Join";
  20.384  
  20.385 -Goal "[| i : I;  eqStates I F |]  \
  20.386 -\     ==> (JN i:I. F i) : ensures A B = \
  20.387 -\         ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
  20.388 -\          (EX i:I. F i : ensures A B))";
  20.389 +Goal "i : I ==> \
  20.390 +\     (JN i:I. F i) : ensures A B = \
  20.391 +\     ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
  20.392 +\      (EX i:I. F i : ensures A B))";
  20.393  by (auto_tac (claset(),
  20.394  	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
  20.395  qed "ensures_JN";
  20.396  
  20.397  Goalw [ensures_def]
  20.398 -     "States F = States G  \
  20.399 -\     ==> F Join G : ensures A B =     \
  20.400 -\         (F : constrains (A-B) (A Un B) & \
  20.401 -\          G : constrains (A-B) (A Un B) & \
  20.402 -\          (F : ensures A B | G : ensures A B))";
  20.403 +     "F Join G : ensures A B =     \
  20.404 +\     (F : constrains (A-B) (A Un B) & \
  20.405 +\      G : constrains (A-B) (A Un B) & \
  20.406 +\      (F : ensures A B | G : ensures A B))";
  20.407  by (auto_tac (claset(),
  20.408  	      simpset() addsimps [constrains_Join, transient_Join]));
  20.409  qed "ensures_Join";
  20.410  
  20.411 -Goal "[| F : stable A;  G : constrains A A';  \
  20.412 -\        States F = States G; A <= States G |] \
  20.413 +Goalw [stable_def, constrains_def, Join_def]
  20.414 +    "[| F : stable A;  G : constrains A A' |] \
  20.415  \    ==> F Join G : constrains A A'";
  20.416 -by (forward_tac [constrains_imp_subset] 1);
  20.417 -by (assume_tac 1);
  20.418 -by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def,
  20.419 -					   ball_Un, Acts_Join]) 1);
  20.420 +by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
  20.421  by (Blast_tac 1);
  20.422  qed "stable_constrains_Join";
  20.423  
  20.424  (*Premise for G cannot use Invariant because  Stable F A  is weaker than
  20.425    G : stable A *)
  20.426 -Goal "[| F : stable A;  G : invariant A;  \
  20.427 -\        States F = States G |] ==> F Join G : Invariant A";
  20.428 -by (asm_full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, 
  20.429 -					   Stable_eq_stable, stable_Join]) 1);
  20.430 +Goal "[| F : stable A;  G : invariant A |] ==> F Join G : Invariant A";
  20.431 +by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, 
  20.432 +				       Stable_eq_stable, stable_Join]) 1);
  20.433  by (force_tac(claset() addIs [stable_reachable, stable_Int],
  20.434  	      simpset() addsimps [Acts_Join]) 1);
  20.435  qed "stable_Join_Invariant";
  20.436  
  20.437 -Goal "[| F : stable A;  G : ensures A B;  \
  20.438 -\        States F = States G |] ==> F Join G : ensures A B";
  20.439 +Goal "[| F : stable A;  G : ensures A B |] ==> F Join G : ensures A B";
  20.440  by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
  20.441  by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
  20.442  by (etac constrains_weaken 1);
  20.443 @@ -361,61 +280,35 @@
  20.444  qed "ensures_stable_Join1";
  20.445  
  20.446  (*As above, but exchanging the roles of F and G*)
  20.447 -Goal "[| F : ensures A B;  G : stable A;  \
  20.448 -\        States F = States G |] ==> F Join G : ensures A B";
  20.449 +Goal "[| F : ensures A B;  G : stable A |] ==> F Join G : ensures A B";
  20.450  by (stac Join_commute 1);
  20.451 -by (dtac sym 1);
  20.452  by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
  20.453  qed "ensures_stable_Join2";
  20.454  
  20.455  
  20.456  (** Diff and localTo **)
  20.457  
  20.458 -
  20.459 -Goal "States (Diff F acts) = States F";
  20.460 -by (simp_tac (simpset() addsimps [Diff_def]) 1);
  20.461 -qed "States_Diff";
  20.462 -
  20.463 -Goal "Init (Diff F acts) = Init F";
  20.464 -by (auto_tac (claset() addIs [impOfSubs Init_subset_States],
  20.465 -	      simpset() addsimps [Diff_def]));
  20.466 -qed "Init_Diff";
  20.467 -
  20.468 -Goal "Acts (Diff F acts) = insert (diag (States F)) (Acts F - acts)";
  20.469 -by (subgoal_tac "Acts F - acts <= Pow (States F Times States F)" 1);
  20.470 -by (blast_tac (claset() addEs [equalityE] 
  20.471 -                        addDs [impOfSubs Acts_subset_Pow_States]) 2);
  20.472 -by (auto_tac (claset(), simpset() addsimps [Diff_def]));
  20.473 -qed "Acts_Diff";
  20.474 -
  20.475 -Addsimps [States_Diff, Init_Diff, Acts_Diff];
  20.476 -
  20.477 -
  20.478 -Goalw [Join_def] "States F = States G ==> F Join (Diff G (Acts F)) = F Join G";
  20.479 +Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G";
  20.480  by (rtac program_equalityI 1);
  20.481 -by (auto_tac (claset(), simpset() addsimps [insert_absorb]));
  20.482 +by Auto_tac;
  20.483  qed "Join_Diff2";
  20.484  
  20.485 -Goalw [Disjoint_def] "States F = States G ==> Disjoint F (Diff G (Acts F))";
  20.486 +Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
  20.487  by Auto_tac;
  20.488  qed "Diff_Disjoint";
  20.489  
  20.490 -Goalw [Disjoint_def] "Disjoint F G ==> States F = States G";
  20.491 -by Auto_tac;
  20.492 -qed "Disjoint_States_eq";
  20.493 -
  20.494  Goal "[| F Join G : v localTo F;  Disjoint F G |] \
  20.495  \     ==> G : (INT z. stable {s. v s = z})";
  20.496  by (asm_full_simp_tac 
  20.497 -    (simpset() addsimps [localTo_def, Disjoint_def,
  20.498 +    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
  20.499  			 Acts_Join, stable_def, constrains_def]) 1);
  20.500  by (Blast_tac 1);
  20.501  qed "localTo_imp_stable";
  20.502  
  20.503  Goal "[| F Join G : v localTo F;  (s,s') : act;  \
  20.504 -\        act : Acts G;  Disjoint F G  |] ==> v s' = v s";
  20.505 +\        act : Acts G;  Disjoint F G |] ==> v s' = v s";
  20.506  by (asm_full_simp_tac 
  20.507 -    (simpset() addsimps [localTo_def, Disjoint_def,
  20.508 +    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
  20.509  			 Acts_Join, stable_def, constrains_def]) 1);
  20.510  by (Blast_tac 1);
  20.511  qed "localTo_imp_equals";
  20.512 @@ -434,15 +327,9 @@
  20.513  \        F Join G : w localTo F;       \
  20.514  \        Disjoint F G |]               \
  20.515  \     ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
  20.516 -by (auto_tac (claset(), 
  20.517 -	      simpset() addsimps [constrains_def, 
  20.518 -				  Disjoint_States_eq RS Acts_Join]));
  20.519 +by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
  20.520  by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
  20.521 -by (subgoal_tac "xa : States F" 1);
  20.522 -by (force_tac
  20.523 -    (claset() addSDs [Disjoint_States_eq,impOfSubs Acts_subset_Pow_States], 
  20.524 -     simpset()) 2);
  20.525 -by (Force_tac 1);
  20.526 +by Auto_tac;
  20.527  qed "constrains_localTo_constrains2";
  20.528  
  20.529  Goalw [stable_def]
  20.530 @@ -472,8 +359,7 @@
  20.531  by (rtac ballI 1);
  20.532  by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
  20.533  \                                      ({s. v s = k} Un {s. v s <= w s})" 1);
  20.534 -by (asm_simp_tac
  20.535 -    (simpset() addsimps [Disjoint_States_eq RS constrains_Join]) 2);
  20.536 +by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
  20.537  by (blast_tac (claset() addIs [constrains_weaken]) 2);
  20.538  by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
  20.539  by (etac Constrains_weaken 2);
    21.1 --- a/src/HOL/UNITY/Union.thy	Mon Mar 01 18:37:52 1999 +0100
    21.2 +++ b/src/HOL/UNITY/Union.thy	Mon Mar 01 18:38:43 1999 +0100
    21.3 @@ -11,24 +11,17 @@
    21.4  Union = SubstAx + FP +
    21.5  
    21.6  constdefs
    21.7 -  eqStates :: ['a set, 'a => 'b program] => bool
    21.8 -    "eqStates I F == EX St. ALL i:I. States (F i) = St"
    21.9 -
   21.10    JOIN  :: ['a set, 'a => 'b program] => 'b program
   21.11 -    "JOIN I F == mk_program (INT i:I. States (F i),
   21.12 -			     INT i:I. Init (F i),
   21.13 -			     UN i:I. Acts (F i))"
   21.14 +    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
   21.15  
   21.16    Join :: ['a program, 'a program] => 'a program      (infixl 65)
   21.17 -    "F Join G == mk_program (States F Int States G,
   21.18 -			     Init F Int Init G,
   21.19 -			     Acts F Un Acts G)"
   21.20 +    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
   21.21  
   21.22 -  SKIP :: 'a set => 'a program
   21.23 -    "SKIP states == mk_program (states, states, {})"
   21.24 +  SKIP :: 'a program
   21.25 +    "SKIP == mk_program (UNIV, {})"
   21.26  
   21.27    Diff :: "['a program, ('a * 'a)set set] => 'a program"
   21.28 -    "Diff F acts == mk_program (States F, Init F, Acts F - acts)"
   21.29 +    "Diff F acts == mk_program (Init F, Acts F - acts)"
   21.30  
   21.31    (*The set of systems that regard "v" as local to F*)
   21.32    localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
   21.33 @@ -36,8 +29,7 @@
   21.34  
   21.35    (*Two programs with disjoint actions, except for identity actions *)
   21.36    Disjoint :: ['a program, 'a program] => bool
   21.37 -    "Disjoint F G == States F = States G &
   21.38 -                     Acts F Int Acts G <= {diag (States G)}"
   21.39 +    "Disjoint F G == Acts F Int Acts G <= {Id}"
   21.40  
   21.41  syntax
   21.42    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
    22.1 --- a/src/HOL/UNITY/WFair.ML	Mon Mar 01 18:37:52 1999 +0100
    22.2 +++ b/src/HOL/UNITY/WFair.ML	Mon Mar 01 18:38:43 1999 +0100
    22.3 @@ -8,10 +8,6 @@
    22.4  From Misra, "A Logic for Concurrent Programming", 1994
    22.5  *)
    22.6  
    22.7 -    Goal "[| x:A;  P(x) |] ==> ? x:A. P(x)";
    22.8 -    by (Blast_tac 1);
    22.9 -    qed "rev_bexI";
   22.10 -
   22.11  
   22.12  overload_1st_set "WFair.transient";
   22.13  overload_1st_set "WFair.ensures";
   22.14 @@ -112,9 +108,16 @@
   22.15  by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
   22.16  qed "leadsTo_Union";
   22.17  
   22.18 +val prems = Goalw [leadsTo_def]
   22.19 +    "(!!A. A : S ==> F : leadsTo (A Int C) B) \
   22.20 +\    ==> F : leadsTo (Union S Int C) B";
   22.21 +by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
   22.22 +by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
   22.23 +qed "leadsTo_Union_Int";
   22.24 +
   22.25  val prems = Goal
   22.26      "(!!i. i : I ==> F : leadsTo (A i) B) ==> F : leadsTo (UN i:I. A i) B";
   22.27 -by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
   22.28 +by (stac (Union_image_eq RS sym) 1);
   22.29  by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
   22.30  qed "leadsTo_UN";
   22.31  
   22.32 @@ -152,10 +155,8 @@
   22.33  by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
   22.34  qed "leadsTo_weaken_R";
   22.35  
   22.36 -
   22.37  Goal "[| F : leadsTo A A'; B<=A |] ==> F : leadsTo B A'";
   22.38 -by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
   22.39 -			       subset_imp_leadsTo]) 1);
   22.40 +by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
   22.41  qed_spec_mp "leadsTo_weaken_L";
   22.42  
   22.43  (*Distributes over binary unions*)
   22.44 @@ -190,7 +191,7 @@
   22.45  val prems = goal thy
   22.46     "(!! i. i:I ==> F : leadsTo (A i) (A' i)) \
   22.47  \   ==> F : leadsTo (UN i:I. A i) (UN i:I. A' i)";
   22.48 -by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
   22.49 +by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
   22.50  by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
   22.51                          addIs prems) 1);
   22.52  qed "leadsTo_UN_UN";
   22.53 @@ -269,8 +270,7 @@
   22.54     "[| F : leadsTo A A'; F : stable B |] \
   22.55  \   ==> F : leadsTo (A Int B) (A' Int B)";
   22.56  by (etac leadsTo_induct 1);
   22.57 -by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
   22.58 -by (blast_tac (claset() addIs [leadsTo_Union]) 3);
   22.59 +by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
   22.60  by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
   22.61  by (rtac leadsTo_Basis 1);
   22.62  by (asm_full_simp_tac
   22.63 @@ -293,8 +293,7 @@
   22.64  Goal "[| F : leadsTo A A'; F : constrains B B' |] \
   22.65  \     ==> F : leadsTo (A Int B) ((A' Int B) Un (B' - B))";
   22.66  by (etac leadsTo_induct 1);
   22.67 -by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
   22.68 -by (blast_tac (claset() addIs [leadsTo_Union]) 3);
   22.69 +by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
   22.70  (*Transitivity case has a delicate argument involving "cancellation"*)
   22.71  by (rtac leadsTo_Un_duplicate2 2);
   22.72  by (etac leadsTo_cancel_Diff1 2);