Addition of the States component; parts of Comp not working
authorpaulson
Thu Dec 03 10:45:06 1998 +0100 (1998-12-03)
changeset 60121894bfc4aee9
parent 6011 c48050d6928d
child 6013 6da9ae6d40f5
Addition of the States component; parts of Comp not working
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/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	Wed Dec 02 16:14:09 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Client.ML	Thu Dec 03 10:45:06 1998 +0100
     1.3 @@ -90,7 +90,8 @@
     1.4  
     1.5  (*** Towards proving the liveness property ***)
     1.6  
     1.7 -Goal "Cli_prg Join G   \
     1.8 +Goal "States Cli_prg = States G \
     1.9 +\     ==> 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 @@ -130,11 +131,13 @@
    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 +be 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 +be 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	Wed Dec 02 16:14:09 1998 +0100
     2.2 +++ b/src/HOL/UNITY/Client.thy	Thu Dec 03 10:45:06 1998 +0100
     2.3 @@ -48,7 +48,8 @@
     2.4  		          size (ask s) = size (rel s))}"
     2.5  
     2.6    Cli_prg :: state program
     2.7 -    "Cli_prg == mk_program ({s. tok s : atMost Max &
     2.8 +    "Cli_prg == mk_program (UNIV,
     2.9 +			    {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	Wed Dec 02 16:14:09 1998 +0100
     3.2 +++ b/src/HOL/UNITY/Common.ML	Thu Dec 03 10:45:06 1998 +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 : constrains {m} (maxfg m)";
     3.8 +Goal "SKIP UNIV : 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, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
    3.15 +Goal "mk_program (UNIV, 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, {range(%t.(t, max (ftime t) (gtime t)))}) \
    3.24 +Goal "mk_program (UNIV, 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,7 +52,8 @@
    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, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
    3.33 +Goal "mk_program (UNIV, UNIV, \
    3.34 +\                 { {(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	Wed Dec 02 16:14:09 1998 +0100
     4.2 +++ b/src/HOL/UNITY/Comp.ML	Thu Dec 03 10:45:06 1998 +0100
     4.3 @@ -16,68 +16,83 @@
     4.4  
     4.5  (*** component ***)
     4.6  
     4.7 -Goalw [component_def] "component SKIP F";
     4.8 -by (blast_tac (claset() addIs [Join_SKIP_left]) 1);
     4.9 +Goalw [component_def] "component (SKIP (States F)) F";
    4.10 +by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
    4.11  qed "component_SKIP";
    4.12  
    4.13  Goalw [component_def] "component F F";
    4.14 -by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
    4.15 +by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1);
    4.16  qed "component_refl";
    4.17  
    4.18  AddIffs [component_SKIP, component_refl];
    4.19  
    4.20 -Goalw [component_def] "component F (F Join G)";
    4.21 +Goalw [component_def] "States F = States G ==> component F (F Join G)";
    4.22  by (Blast_tac 1);
    4.23  qed "component_Join1";
    4.24  
    4.25 -Goalw [component_def] "component G (F Join G)";
    4.26 +Goalw [component_def] "States F = States G ==> component G (F Join G)";
    4.27  by (simp_tac (simpset() addsimps [Join_commute]) 1);
    4.28 +by (dtac sym 1);
    4.29  by (Blast_tac 1);
    4.30  qed "component_Join2";
    4.31  
    4.32 -Goalw [component_def] "i : I ==> component (F i) (JN i:I. (F i))";
    4.33 -by (blast_tac (claset() addIs [JN_absorb]) 1);
    4.34 +Goalw [component_def, eqStates_def] 
    4.35 +    "[| i : I;  eqStates I F |] ==> component (F i) (JN i:I. (F i))";
    4.36 +by (force_tac (claset() addIs [JN_absorb], simpset()) 1);
    4.37  qed "component_JN";
    4.38  
    4.39  Goalw [component_def] "[| component F G; component G H |] ==> component F H";
    4.40 -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    4.41 +by (force_tac (claset() addIs [Join_assoc RS sym], simpset()) 1);
    4.42  qed "component_trans";
    4.43  
    4.44 -Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";
    4.45 -by Auto_tac;
    4.46 +Goalw [component_def] "component F G ==> Acts F <= Acts G";
    4.47 +by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
    4.48  qed "component_Acts";
    4.49  
    4.50  Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
    4.51  by Auto_tac;
    4.52  qed "component_Init";
    4.53  
    4.54 +Goalw [component_def] "component F G ==> States F = States G";
    4.55 +by Auto_tac;
    4.56 +qed "component_States";
    4.57 +
    4.58  Goal "[| component F G; component G F |] ==> F=G";
    4.59 -by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, 
    4.60 -				      component_Acts, component_Init]) 1);
    4.61 +by (blast_tac (claset() addSIs [program_equalityI, component_States, 
    4.62 +				component_Init, component_Acts]) 1);
    4.63  qed "component_anti_sym";
    4.64  
    4.65  Goalw [component_def]
    4.66        "component F H = (EX G. F Join G = H & Disjoint F G)";
    4.67 -by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
    4.68 +by (blast_tac (claset() addSIs [Disjoint_States_eq, 
    4.69 +				Diff_Disjoint, Join_Diff2]) 1);
    4.70  qed "component_eq";
    4.71  
    4.72  (*** existential properties ***)
    4.73  
    4.74  Goalw [ex_prop_def]
    4.75 -     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
    4.76 +     "[| ex_prop X;  finite GG |] \
    4.77 +\     ==> eqStates GG (%x. x) --> GG Int X ~= {} --> (JN G:GG. G) : X";
    4.78  by (etac finite_induct 1);
    4.79 -by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    4.80 +by (Simp_tac 1);
    4.81 +by (rename_tac "GG J" 1);
    4.82 +by (full_simp_tac (simpset() addsimps [Int_insert_left]) 1);
    4.83 +by (dres_inst_tac [("x","J")] spec 1);
    4.84 +by (Force_tac 1);
    4.85  qed_spec_mp "ex1";
    4.86  
    4.87  Goalw [ex_prop_def]
    4.88 -     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
    4.89 +     "ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \
    4.90 +\       --> (JN G:GG. G) : X ==> ex_prop X";
    4.91  by (Clarify_tac 1);
    4.92  by (dres_inst_tac [("x", "{F,G}")] spec 1);
    4.93  by Auto_tac;
    4.94  qed "ex2";
    4.95  
    4.96  (*Chandy & Sanders take this as a definition*)
    4.97 -Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
    4.98 +Goal "ex_prop X = \
    4.99 +\       (ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \
   4.100 +\          --> (JN G:GG. G) : X)";
   4.101  by (blast_tac (claset() addIs [ex1,ex2]) 1);
   4.102  qed "ex_prop_finite";
   4.103  
   4.104 @@ -88,6 +103,7 @@
   4.105  by (Blast_tac 1);
   4.106  by Safe_tac;
   4.107  by (stac Join_commute 2);
   4.108 +by (dtac sym 2);
   4.109  by (ALLGOALS Blast_tac);
   4.110  qed "ex_prop_equiv";
   4.111  
   4.112 @@ -95,13 +111,15 @@
   4.113  (*** universal properties ***)
   4.114  
   4.115  Goalw [uv_prop_def]
   4.116 -     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
   4.117 +     "[| uv_prop X; finite GG |] \
   4.118 +\     ==> eqStates GG (%x. x) --> GG <= X --> (JN G:GG. G) : X";
   4.119  by (etac finite_induct 1);
   4.120  by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
   4.121  qed_spec_mp "uv1";
   4.122  
   4.123  Goalw [uv_prop_def]
   4.124 -     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
   4.125 +     "ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \
   4.126 +\       --> (JN G:GG. G) : X  ==> uv_prop X";
   4.127  by (rtac conjI 1);
   4.128  by (Clarify_tac 2);
   4.129  by (dres_inst_tac [("x", "{F,G}")] spec 2);
   4.130 @@ -110,7 +128,8 @@
   4.131  qed "uv2";
   4.132  
   4.133  (*Chandy & Sanders take this as a definition*)
   4.134 -Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
   4.135 +Goal "uv_prop X = (ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \
   4.136 +\       --> (JN G:GG. G) : X)";
   4.137  by (blast_tac (claset() addIs [uv1,uv2]) 1);
   4.138  qed "uv_prop_finite";
   4.139  
   4.140 @@ -180,7 +199,8 @@
   4.141  qed "guaranteesI";
   4.142  
   4.143  Goalw [guarantees_def, component_def]
   4.144 -     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
   4.145 +     "[| F : X guarantees Y;  F Join G : X;  States F = States G |] \
   4.146 +\     ==> F Join G : Y";
   4.147  by (Blast_tac 1);
   4.148  qed "guaranteesD";
   4.149  
   4.150 @@ -203,36 +223,46 @@
   4.151  
   4.152  Goalw [refines_def]
   4.153       "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X";
   4.154 -by (Blast_tac 1);
   4.155 +by Auto_tac;
   4.156  qed "refines_trans";
   4.157  
   4.158  Goalw [strict_ex_prop_def]
   4.159 -     "strict_ex_prop X \
   4.160 -\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   4.161 +     "[| strict_ex_prop X;  States F = States G |] \
   4.162 +\     ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = \
   4.163 +\         (F:X --> G:X)";
   4.164 +by Safe_tac;
   4.165  by (Blast_tac 1);
   4.166 +auto();
   4.167  qed "strict_ex_refine_lemma";
   4.168  
   4.169  Goalw [strict_ex_prop_def]
   4.170 -     "strict_ex_prop X \
   4.171 -\     ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
   4.172 +     "[| strict_ex_prop X;  States F = States G |] \
   4.173 +\     ==> (ALL H. States F = States H & F Join H : welldef & F Join H : X \
   4.174 +\           --> G Join H : X) = \
   4.175  \         (F: welldef Int X --> G:X)";
   4.176  by Safe_tac;
   4.177 -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   4.178 +by (eres_inst_tac [("x","SKIP ?A"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   4.179  by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
   4.180  qed "strict_ex_refine_lemma_v";
   4.181  
   4.182 -Goal "[| strict_ex_prop X;  \
   4.183 -\        ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
   4.184 +Goal "[| strict_ex_prop X;  States F = States G;  \
   4.185 +\        ALL H. States F = States H & F Join H : welldef Int X \
   4.186 +\          --> G Join H : welldef |] \
   4.187  \     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   4.188 -by (res_inst_tac [("x","SKIP")] allE 1
   4.189 +bd sym 1;
   4.190 +by (res_inst_tac [("x","SKIP (States G)")] allE 1
   4.191      THEN assume_tac 1);
   4.192  by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   4.193  					   strict_ex_refine_lemma_v]) 1);
   4.194  qed "ex_refinement_thm";
   4.195  
   4.196 +
   4.197 +(***
   4.198 +
   4.199 +
   4.200  Goalw [strict_uv_prop_def]
   4.201       "strict_uv_prop X \
   4.202 -\     ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
   4.203 +\     ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
   4.204  by (Blast_tac 1);
   4.205  qed "strict_uv_refine_lemma";
   4.206  
   4.207 @@ -254,3 +284,4 @@
   4.208  by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   4.209  					   strict_uv_refine_lemma_v]) 1);
   4.210  qed "uv_refinement_thm";
   4.211 +***)
     5.1 --- a/src/HOL/UNITY/Comp.thy	Wed Dec 02 16:14:09 1998 +0100
     5.2 +++ b/src/HOL/UNITY/Comp.thy	Thu Dec 03 10:45:06 1998 +0100
     5.3 @@ -16,23 +16,29 @@
     5.4      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
     5.5  
     5.6    ex_prop  :: 'a program set => bool
     5.7 -   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
     5.8 +   "ex_prop X ==
     5.9 +      ALL F G. (F:X | G: X) & States F = States G --> (F Join G) : X"
    5.10  
    5.11    strict_ex_prop  :: 'a program set => bool
    5.12 -   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
    5.13 +   "strict_ex_prop X ==
    5.14 +      ALL F G. States F = States G --> (F:X | G: X) = (F Join G : X)"
    5.15  
    5.16    uv_prop  :: 'a program set => bool
    5.17 -   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (F Join G) : X)"
    5.18 +   "uv_prop X ==
    5.19 +      SKIP UNIV : X &
    5.20 +      (ALL F G. F:X & G: X & States F = States G --> (F Join G) : X)"
    5.21  
    5.22    strict_uv_prop  :: 'a program set => bool
    5.23 -   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (F Join G : X))"
    5.24 +   "strict_uv_prop X ==
    5.25 +      SKIP UNIV : X &
    5.26 +      (ALL F G. States F = States G --> (F:X & G: X) = (F Join G : X))"
    5.27  
    5.28    (*Ill-defined programs can arise through "Join"*)
    5.29    welldef :: 'a program set  
    5.30     "welldef == {F. Init F ~= {}}"
    5.31  
    5.32    component :: ['a program, 'a program] => bool
    5.33 -   "component F H == EX G. F Join G = H"
    5.34 +   "component F H == EX G. F Join G = H & States F = States G"
    5.35  
    5.36    guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
    5.37     "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
    5.38 @@ -40,7 +46,9 @@
    5.39    refines :: ['a program, 'a program, 'a program set] => bool
    5.40  			("(3_ refines _ wrt _)" [10,10,10] 10)
    5.41     "G refines F wrt X ==
    5.42 -      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
    5.43 +      States F = States G &
    5.44 +      (ALL H. States F = States H & (F Join H) : welldef Int X
    5.45 +        --> G Join H : welldef Int X)"
    5.46  
    5.47    iso_refines :: ['a program, 'a program, 'a program set] => bool
    5.48  			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
     6.1 --- a/src/HOL/UNITY/Constrains.ML	Wed Dec 02 16:14:09 1998 +0100
     6.2 +++ b/src/HOL/UNITY/Constrains.ML	Thu Dec 03 10:45:06 1998 +0100
     6.3 @@ -89,19 +89,27 @@
     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' ==> reachable F Int A <= A'";
     6.8 +Goal "[| F : Constrains A A'; A <= reachable F |] ==> 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 (ALLGOALS
    6.12 -    (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
    6.13 +by (auto_tac (claset() addIs [impOfSubs reachable_subset_States],
    6.14 +	      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 [constrains_trans, constrains_weaken]) 1);
    6.21 +by (blast_tac (claset() addIs [impOfSubs reachable_subset_States,
    6.22 +			       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 +qed "Constrains_cancel";
    6.31 +
    6.32  
    6.33  (*** Stable ***)
    6.34  
    6.35 @@ -193,13 +201,6 @@
    6.36  by (Blast_tac 1);
    6.37  qed "Elimination_sing";
    6.38  
    6.39 -Goalw [Constrains_def, constrains_def]
    6.40 -   "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
    6.41 -\   ==> F : Constrains A (A' Un B')";
    6.42 -by (Clarify_tac 1);
    6.43 -by (Blast_tac 1);
    6.44 -qed "Constrains_cancel";
    6.45 -
    6.46  
    6.47  (*** Specialized laws for handling Invariants ***)
    6.48  
     7.1 --- a/src/HOL/UNITY/Handshake.ML	Wed Dec 02 16:14:09 1998 +0100
     7.2 +++ b/src/HOL/UNITY/Handshake.ML	Thu Dec 03 10:45:06 1998 +0100
     7.3 @@ -11,6 +11,7 @@
     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 @@ -20,7 +21,6 @@
    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 @@ -36,12 +36,14 @@
    7.20  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    7.21  by (ensures_tac "cmdG" 2);
    7.22  by (constrains_tac 1);
    7.23 +by Auto_tac;
    7.24  qed "lemma2_1";
    7.25  
    7.26  Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
    7.27  by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    7.28  by (constrains_tac 2);
    7.29  by (ensures_tac "cmdF" 1);
    7.30 +by Auto_tac;
    7.31  qed "lemma2_2";
    7.32  
    7.33  
     8.1 --- a/src/HOL/UNITY/Handshake.thy	Wed Dec 02 16:14:09 1998 +0100
     8.2 +++ b/src/HOL/UNITY/Handshake.thy	Thu Dec 03 10:45:06 1998 +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 ({s. NF s = 0 & BB s}, {cmdF})"
     8.8 +    "F == mk_program (UNIV, {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 ({s. NG s = 0 & BB s}, {cmdG})"
    8.16 +    "G == mk_program (UNIV, {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	Wed Dec 02 16:14:09 1998 +0100
     9.2 +++ b/src/HOL/UNITY/Lift.thy	Thu Dec 03 10:45:06 1998 +0100
     9.3 @@ -116,7 +116,8 @@
     9.4  
     9.5    Lprg :: state program
     9.6      (*for the moment, we OMIT button_press*)
     9.7 -    "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
     9.8 +    "Lprg == mk_program (UNIV,
     9.9 +			 {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})"
    10.1 --- a/src/HOL/UNITY/Mutex.thy	Wed Dec 02 16:14:09 1998 +0100
    10.2 +++ b/src/HOL/UNITY/Mutex.thy	Thu Dec 03 10:45:06 1998 +0100
    10.3 @@ -52,7 +52,8 @@
    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 ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0},
    10.8 +    "Mprg == mk_program (UNIV,
    10.9 +			 {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	Wed Dec 02 16:14:09 1998 +0100
    11.2 +++ b/src/HOL/UNITY/NSP_Bad.thy	Thu Dec 03 10:45:06 1998 +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({[]}, {Fake, NS1, NS2, NS3})"
    11.8 +    "Nprg == mk_program(UNIV, {[]}, {Fake, NS1, NS2, NS3})"
    11.9  
   11.10  end
    12.1 --- a/src/HOL/UNITY/PPROD.ML	Wed Dec 02 16:14:09 1998 +0100
    12.2 +++ b/src/HOL/UNITY/PPROD.ML	Thu Dec 03 10:45:06 1998 +0100
    12.3 @@ -4,11 +4,6 @@
    12.4      Copyright   1998  University of Cambridge
    12.5  *)
    12.6  
    12.7 -	Addsimps [image_id];
    12.8 -
    12.9 -
   12.10 -val rinst = read_instantiate_sg (sign_of thy);
   12.11 -
   12.12  (*** General lemmas ***)
   12.13  
   12.14  Goal "x:C ==> (A Times C <= B Times C) = (A <= B)";
   12.15 @@ -23,9 +18,9 @@
   12.16  by (Blast_tac 1);
   12.17  qed "Times_Union2";
   12.18  
   12.19 -Goal "Domain (Union S) = (UN A:S. Domain A)";
   12.20 -by (Blast_tac 1);
   12.21 -qed "Domain_Union";
   12.22 +    Goal "Domain (Union S) = (UN A:S. Domain A)";
   12.23 +    by (Blast_tac 1);
   12.24 +    qed "Domain_Union";
   12.25  
   12.26  (** RTimes: the product of two relations **)
   12.27  
   12.28 @@ -65,17 +60,6 @@
   12.29  qed "Image_RTimes"; 
   12.30  
   12.31  
   12.32 -Goal "- (UNIV Times A) = UNIV Times (-A)";
   12.33 -by Auto_tac;
   12.34 -qed "Compl_Times_UNIV1"; 
   12.35 -
   12.36 -Goal "- (A Times UNIV) = (-A) Times UNIV";
   12.37 -by Auto_tac;
   12.38 -qed "Compl_Times_UNIV2"; 
   12.39 -
   12.40 -Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
   12.41 -
   12.42 -
   12.43  (**** Lcopy ****)
   12.44  
   12.45  (*** Basic properties ***)
   12.46 @@ -84,9 +68,9 @@
   12.47  by (simp_tac (simpset() addsimps [Lcopy_def]) 1);
   12.48  qed "Init_Lcopy";
   12.49  
   12.50 -Goal "Id : (%act. act RTimes Id) `` Acts F";
   12.51 +Goal "diag (States F Times UNIV) : (%act. act RTimes diag UNIV) `` Acts F";
   12.52  by (rtac image_eqI 1);
   12.53 -by (rtac Id_in_Acts 2);
   12.54 +by (rtac diag_in_Acts 2);
   12.55  by Auto_tac;
   12.56  val lemma = result();
   12.57  
   12.58 @@ -234,7 +218,7 @@
   12.59  Addsimps [Init_lift_prog];
   12.60  
   12.61  Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
   12.62 -by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
   12.63 +by (auto_tac (claset() addIs [diag_in_Acts RSN (2,image_eqI)], simpset()));
   12.64  qed "Acts_lift_prog";
   12.65  
   12.66  Goalw [PPROD_def] "Init (PPROD I F) = {f. ALL i:I. f i : Init (F i)}";
    13.1 --- a/src/HOL/UNITY/PPROD.thy	Wed Dec 02 16:14:09 1998 +0100
    13.2 +++ b/src/HOL/UNITY/PPROD.thy	Thu Dec 03 10:45:06 1998 +0100
    13.3 @@ -3,7 +3,7 @@
    13.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.5      Copyright   1998  University of Cambridge
    13.6  
    13.7 -General products of programs (Pi operation).
    13.8 +General products of programs (Pi operation), for replicating components.
    13.9  Also merging of state sets.
   13.10  *)
   13.11  
   13.12 @@ -11,7 +11,7 @@
   13.13  
   13.14  constdefs
   13.15    (*Cartesian product of two relations*)
   13.16 -  RTimes :: "[('a*'a) set, ('b*'b) set] => (('a*'b) * ('a*'b)) set"
   13.17 +  RTimes :: "[('a*'b) set, ('c*'d) set] => (('a*'c) * ('b*'d)) set"
   13.18  	("_ RTimes _" [81, 80] 80)
   13.19  
   13.20      "R RTimes S == {((x,y),(x',y')). (x,x'):R & (y,y'):S}"
   13.21 @@ -26,8 +26,9 @@
   13.22      "fst_act act == (%((x,y),(x',y')). (x,x')) `` act"
   13.23  
   13.24    Lcopy :: "'a program => ('a*'b) program"
   13.25 -    "Lcopy F == mk_program (Init F Times UNIV,
   13.26 -			    (%act. act RTimes Id) `` Acts F)"
   13.27 +    "Lcopy F == mk_program (UNIV,
   13.28 +			    Init F Times UNIV,
   13.29 +			    (%act. act RTimes (diag UNIV)) `` Acts F)"
   13.30  
   13.31    lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
   13.32      "lift_act i act == {(f,f'). EX s'. f' = f(i:=s') & (f i, s') : act}"
   13.33 @@ -36,7 +37,8 @@
   13.34      "drop_act i act == (%(f,f'). (f i, f' i)) `` act"
   13.35  
   13.36    lift_prog :: "['a, 'b program] => ('a => 'b) program"
   13.37 -    "lift_prog i F == mk_program ({f. f i : Init F}, lift_act i `` Acts F)"
   13.38 +    "lift_prog i F ==
   13.39 +       mk_program (UNIV, {f. f i : Init F}, lift_act i `` Acts F)"
   13.40  
   13.41    (*products of programs*)
   13.42    PPROD  :: ['a set, 'a => 'b program] => ('a => 'b) program
    14.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Dec 02 16:14:09 1998 +0100
    14.2 +++ b/src/HOL/UNITY/ROOT.ML	Thu Dec 03 10:45:06 1998 +0100
    14.3 @@ -11,6 +11,8 @@
    14.4  writeln"Root file for HOL/UNITY";
    14.5  set proof_timing;
    14.6  
    14.7 +
    14.8 +
    14.9  loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
   14.10  time_use_thy"UNITY";
   14.11  
   14.12 @@ -27,7 +29,9 @@
   14.13  time_use_thy "Lift";
   14.14  time_use_thy "Comp";
   14.15  time_use_thy "Client";
   14.16 -time_use_thy "PPROD";
   14.17 +(**
   14.18 +time_use_thy "PPX";
   14.19 +**)
   14.20  
   14.21  loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
   14.22  use_thy"NSP_Bad";
    15.1 --- a/src/HOL/UNITY/Reach.thy	Wed Dec 02 16:14:09 1998 +0100
    15.2 +++ b/src/HOL/UNITY/Reach.thy	Thu Dec 03 10:45:06 1998 +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 ({%v. v=init}, UN (u,v): edges. {asgt u v})"
    15.8 +    "Rprg == mk_program (UNIV, {%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/Traces.ML	Wed Dec 02 16:14:09 1998 +0100
    16.2 +++ b/src/HOL/UNITY/Traces.ML	Thu Dec 03 10:45:06 1998 +0100
    16.3 @@ -12,73 +12,161 @@
    16.4  
    16.5  (*** The abstract type of programs ***)
    16.6  
    16.7 +Goalw [restrict_rel_def] "restrict_rel A Id = diag A";
    16.8 +by (Blast_tac 1);
    16.9 +qed "restrict_rel_Id";
   16.10 +Addsimps [restrict_rel_Id];
   16.11 +
   16.12 +Goalw [restrict_rel_def] "restrict_rel A (diag B) = diag (A Int B)";
   16.13 +by (Blast_tac 1);
   16.14 +qed "restrict_rel_diag";
   16.15 +Addsimps [restrict_rel_diag];
   16.16 +
   16.17 +Goalw [restrict_rel_def]
   16.18 +    "restrict_rel A (restrict_rel B r) = restrict_rel (A Int B) r";
   16.19 +by (Blast_tac 1);
   16.20 +qed "restrict_rel_restrict_rel";
   16.21 +Addsimps [restrict_rel_restrict_rel];
   16.22 +
   16.23 +Goalw [restrict_rel_def] "restrict_rel A r <= A Times A";
   16.24 +by (Blast_tac 1);
   16.25 +qed "restrict_rel_subset";
   16.26 +Addsimps [restrict_rel_subset];
   16.27 +
   16.28 +Goalw [restrict_rel_def]
   16.29 +    "((x,y) : restrict_rel A r) = ((x,y): r & x: A & y: A)";
   16.30 +by (Blast_tac 1);
   16.31 +qed "restrict_rel_iff";
   16.32 +Addsimps [restrict_rel_iff];
   16.33 +
   16.34 +Goalw [restrict_rel_def] "r <= A Times A ==> restrict_rel A r = r";
   16.35 +by (Blast_tac 1);
   16.36 +qed "restrict_rel_eq";
   16.37 +Addsimps [restrict_rel_eq];
   16.38 +
   16.39 +Goal "acts <= Pow (A Times A) ==> restrict_rel A `` acts = acts";
   16.40 +by Auto_tac;
   16.41 +by (rtac image_eqI 1);
   16.42 +by (assume_tac 2);
   16.43 +by (set_mp_tac 1);
   16.44 +by (Force_tac 1);
   16.45 +qed "restrict_rel_image";
   16.46 +
   16.47 +Goalw [restrict_rel_def] "Domain (restrict_rel A r) <= A Int Domain r";
   16.48 +by (Blast_tac 1);
   16.49 +qed "Domain_restrict_rel";
   16.50 +
   16.51 +Goalw [restrict_rel_def] "restrict_rel A r ^^ B <= A Int (r ^^ B)";
   16.52 +by (Blast_tac 1);
   16.53 +qed "Image_restrict_rel";
   16.54 +
   16.55 +Addsimps [diag_iff];
   16.56 +
   16.57  val rep_ss = simpset() addsimps 
   16.58 -                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
   16.59 +                [Int_lower1, image_subset_iff, diag_subset_Times,
   16.60 +		 States_def, Init_def, Acts_def, 
   16.61 +		 mk_program_def, Program_def, Rep_Program, 
   16.62  		 Rep_Program_inverse, Abs_Program_inverse];
   16.63  
   16.64  
   16.65 -Goal "Id: Acts F";
   16.66 +(** Basic laws guaranteed by the abstract type "program" **)
   16.67 +
   16.68 +Goal "Init F <= States F";
   16.69  by (cut_inst_tac [("x", "F")] Rep_Program 1);
   16.70  by (auto_tac (claset(), rep_ss));
   16.71 -qed "Id_in_Acts";
   16.72 -AddIffs [Id_in_Acts];
   16.73 +qed "Init_subset_States";
   16.74 +
   16.75 +Goal "Acts F <= Pow(States F Times States F)";
   16.76 +by (cut_inst_tac [("x", "F")] Rep_Program 1);
   16.77 +by (force_tac (claset(),rep_ss) 1);
   16.78 +qed "Acts_subset_Pow_States";
   16.79 +
   16.80 +Goal "diag (States F) : Acts F";
   16.81 +by (cut_inst_tac [("x", "F")] Rep_Program 1);
   16.82 +by (auto_tac (claset(), rep_ss));
   16.83 +qed "diag_in_Acts";
   16.84 +AddIffs [diag_in_Acts];
   16.85  
   16.86  
   16.87 -Goal "Init (mk_program (init,acts)) = init";
   16.88 +(** Inspectors for type "program" **)
   16.89 +
   16.90 +Goal "States (mk_program (states,init,acts)) = states";
   16.91 +by (auto_tac (claset(), rep_ss));
   16.92 +qed "States_eq";
   16.93 +
   16.94 +Goal "Init (mk_program (states,init,acts)) = states Int init";
   16.95  by (auto_tac (claset(), rep_ss));
   16.96  qed "Init_eq";
   16.97  
   16.98 -Goal "Acts (mk_program (init,acts)) = insert Id acts";
   16.99 +Goal "Acts (mk_program (states,init,acts)) = \
  16.100 +\     insert (diag states) (restrict_rel states `` acts)";
  16.101  by (auto_tac (claset(), rep_ss));
  16.102 +qed "Acts_eq_raw";
  16.103 +
  16.104 +Goal "acts <= Pow(states Times states) \
  16.105 +\     ==> Acts (mk_program (states,init,acts)) = insert (diag states) acts";
  16.106 +by (asm_simp_tac (simpset() addsimps [Acts_eq_raw, restrict_rel_image]) 1);
  16.107  qed "Acts_eq";
  16.108  
  16.109 -Addsimps [Acts_eq, Init_eq];
  16.110 +Addsimps [States_eq, Acts_eq, Init_eq];
  16.111  
  16.112  
  16.113 -Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
  16.114 -by (cut_inst_tac [("p", "Rep_Program F")] surjective_pairing 1);
  16.115 +(** The notation of equality for type "program" **)
  16.116 +
  16.117 +Goal "[| States F = States G; Init F = Init G; Acts F = Acts G |] ==> F = G";
  16.118 +by (subgoals_tac ["EX x. Rep_Program F = x",
  16.119 +		  "EX x. Rep_Program G = x"] 1);
  16.120 +by (REPEAT (Blast_tac 2));
  16.121 +by (Clarify_tac 1);
  16.122  by (auto_tac (claset(), rep_ss));
  16.123 -by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1);
  16.124 -by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1);
  16.125 +by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
  16.126 +by (asm_full_simp_tac rep_ss 1);
  16.127  qed "program_equalityI";
  16.128  
  16.129  val [major,minor] =
  16.130 -Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
  16.131 +Goal "[| F = G; \
  16.132 +\        [| States F = States G; Init F = Init G; Acts F = Acts G |] ==> P \
  16.133 +\     |] ==> P";
  16.134  by (rtac minor 1);
  16.135  by (auto_tac (claset(), simpset() addsimps [major]));
  16.136  qed "program_equalityE";
  16.137  
  16.138 -(*** These rules allow "lazy" definition expansion ***)
  16.139 +(*** These rules allow "lazy" definition expansion 
  16.140 +     They avoid expanding the full program, which is a large expression
  16.141 +***)
  16.142  
  16.143 -(*The program is not expanded, but its Init is*)
  16.144 -val [rew] = goal thy
  16.145 -    "[| F == mk_program (init,acts) |] \
  16.146 -\    ==> Init F = init";
  16.147 -by (rewtac rew);
  16.148 +Goal "[| F == mk_program (states,init,acts) |] \
  16.149 +\     ==> States F = states";
  16.150 +by Auto_tac;
  16.151 +qed "def_prg_States";
  16.152 +
  16.153 +Goal "[| F == mk_program (states,init,acts); init <= states |] \
  16.154 +\     ==> Init F = init";
  16.155  by Auto_tac;
  16.156  qed "def_prg_Init";
  16.157  
  16.158 +Goal "[| F == mk_program (states,init,acts); \
  16.159 +\        acts <= Pow(states Times states) |] \
  16.160 +\     ==> Acts F = insert (diag states) acts";
  16.161 +by (asm_simp_tac (simpset() addsimps [restrict_rel_image]) 1);
  16.162 +qed "def_prg_Acts";
  16.163 +
  16.164  (*The program is not expanded, but its Init and Acts are*)
  16.165 -val [rew] = goal thy
  16.166 -    "[| F == mk_program (init,acts) |] \
  16.167 -\    ==> Init F = init & Acts F = insert Id acts";
  16.168 -by (rewtac rew);
  16.169 -by Auto_tac;
  16.170 +Goal "[| F == mk_program (states,init,acts); \
  16.171 +\        init <= states;  acts <= Pow(states Times states) |] \
  16.172 +\     ==> Init F = init & Acts F = insert (diag states) acts";
  16.173 +by (asm_simp_tac (HOL_ss addsimps [def_prg_Init, def_prg_Acts]) 1);
  16.174  qed "def_prg_simps";
  16.175  
  16.176  (*An action is expanded only if a pair of states is being tested against it*)
  16.177 -val [rew] = goal thy
  16.178 -    "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
  16.179 -by (rewtac rew);
  16.180 +Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
  16.181  by Auto_tac;
  16.182  qed "def_act_simp";
  16.183  
  16.184  fun simp_of_act def = def RS def_act_simp;
  16.185  
  16.186  (*A set is expanded only if an element is being tested against it*)
  16.187 -val [rew] = goal thy
  16.188 -    "A == B ==> (x : A) = (x : B)";
  16.189 -by (rewtac rew);
  16.190 +Goal "A == B ==> (x : A) = (x : B)";
  16.191  by Auto_tac;
  16.192  qed "def_set_simp";
  16.193  
  16.194 @@ -87,6 +175,13 @@
  16.195  
  16.196  (*** traces and reachable ***)
  16.197  
  16.198 +Goal "reachable F <= States F";
  16.199 +by Safe_tac;
  16.200 +by (etac reachable.induct 1);
  16.201 +by (blast_tac (claset() addDs [impOfSubs Acts_subset_Pow_States]) 2);
  16.202 +by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1);
  16.203 +qed "reachable_subset_States";
  16.204 +
  16.205  Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
  16.206  by Safe_tac;
  16.207  by (etac traces.induct 2);
    17.1 --- a/src/HOL/UNITY/Traces.thy	Wed Dec 02 16:14:09 1998 +0100
    17.2 +++ b/src/HOL/UNITY/Traces.thy	Thu Dec 03 10:45:06 1998 +0100
    17.3 @@ -25,17 +25,32 @@
    17.4  
    17.5  
    17.6  typedef (Program)
    17.7 -  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
    17.8 +  'a program = "{(states :: 'a set,
    17.9 +		  init   :: 'a set,
   17.10 +		  acts   :: ('a * 'a)set set).
   17.11 +		 init <= states &
   17.12 +		 acts <= Pow(states Times states) &
   17.13 +		 diag states : acts}"
   17.14  
   17.15  constdefs
   17.16 -    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
   17.17 -    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
   17.18 +  restrict_rel :: "['a set, ('a * 'a) set] => ('a * 'a) set"
   17.19 +    "restrict_rel A r == (A Times A) Int r"
   17.20  
   17.21 -    Init :: "'a program => 'a set"
   17.22 -    "Init F == fst (Rep_Program F)"
   17.23 +  mk_program :: "('a set * 'a set * ('a * 'a)set set) => 'a program"
   17.24 +    "mk_program ==
   17.25 +       %(states, init, acts).
   17.26 +	Abs_Program (states,
   17.27 +		     states Int init,
   17.28 +		     restrict_rel states `` (insert Id acts))"
   17.29  
   17.30 -    Acts :: "'a program => ('a * 'a)set set"
   17.31 -    "Acts F == snd (Rep_Program F)"
   17.32 +  States :: "'a program => 'a set"
   17.33 +    "States F == (%(states, init, acts). states) (Rep_Program F)"
   17.34 +
   17.35 +  Init :: "'a program => 'a set"
   17.36 +    "Init F == (%(states, init, acts). init) (Rep_Program F)"
   17.37 +
   17.38 +  Acts :: "'a program => ('a * 'a)set set"
   17.39 +    "Acts F == (%(states, init, acts). acts) (Rep_Program F)"
   17.40  
   17.41  
   17.42  consts reachable :: "'a program => 'a set"
    18.1 --- a/src/HOL/UNITY/UNITY.ML	Wed Dec 02 16:14:09 1998 +0100
    18.2 +++ b/src/HOL/UNITY/UNITY.ML	Thu Dec 03 10:45:06 1998 +0100
    18.3 @@ -12,6 +12,29 @@
    18.4  HOL_quantifiers := false;
    18.5  
    18.6  
    18.7 +(*** General lemmas ***)
    18.8 +
    18.9 +    Goal "Pow UNIV = UNIV";
   18.10 +    by (Blast_tac 1);
   18.11 +    qed "Pow_UNIV";
   18.12 +    Addsimps [Pow_UNIV];
   18.13 +
   18.14 +Goal "UNIV Times UNIV = UNIV";
   18.15 +by Auto_tac;
   18.16 +qed "UNIV_Times_UNIV"; 
   18.17 +Addsimps [UNIV_Times_UNIV];
   18.18 +
   18.19 +Goal "- (UNIV Times A) = UNIV Times (-A)";
   18.20 +by Auto_tac;
   18.21 +qed "Compl_Times_UNIV1"; 
   18.22 +
   18.23 +Goal "- (A Times UNIV) = (-A) Times UNIV";
   18.24 +by Auto_tac;
   18.25 +qed "Compl_Times_UNIV2"; 
   18.26 +
   18.27 +Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
   18.28 +
   18.29 +
   18.30  (*** constrains ***)
   18.31  
   18.32  overload_1st_set "UNITY.constrains";
   18.33 @@ -83,16 +106,25 @@
   18.34  by (Blast_tac 1);
   18.35  qed "ball_constrains_INT";
   18.36  
   18.37 -Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'";
   18.38 -by (Blast_tac 1);
   18.39 +Goalw [constrains_def] "[| F : constrains A A'; A <= States F |] ==> A <= A'";
   18.40 +by (Force_tac 1);
   18.41  qed "constrains_imp_subset";
   18.42  
   18.43 -Goalw [constrains_def]
   18.44 -    "[| F : constrains A B; F : constrains B C |]   \
   18.45 +(*The reasoning is by subsets since "constrains" refers to single actions
   18.46 +  only.  So this rule isn't that useful.*)
   18.47 +Goal "[| F : constrains A B; F : constrains B C; B <= States F |]   \
   18.48  \    ==> F : constrains A C";
   18.49 -by (Blast_tac 1);
   18.50 +by (etac constrains_weaken_R 1);
   18.51 +by (etac constrains_imp_subset 1);
   18.52 +by (assume_tac 1);
   18.53  qed "constrains_trans";
   18.54  
   18.55 +Goal "[| F : constrains A (A' Un B); F : constrains B B'; B <= States F|] \
   18.56 +\     ==> F : constrains A (A' Un B')";
   18.57 +by (etac constrains_weaken_R 1);
   18.58 +by (blast_tac (claset() addDs [impOfSubs constrains_imp_subset]) 1);
   18.59 +qed "constrains_cancel";
   18.60 +
   18.61  
   18.62  (*** stable ***)
   18.63  
   18.64 @@ -212,14 +244,6 @@
   18.65  qed "elimination_sing";
   18.66  
   18.67  
   18.68 -Goalw [constrains_def]
   18.69 -   "[| F : constrains A (A' Un B); F : constrains B B' |] \
   18.70 -\   ==> F : constrains A (A' Un B')";
   18.71 -by (Clarify_tac 1);
   18.72 -by (Blast_tac 1);
   18.73 -qed "constrains_cancel";
   18.74 -
   18.75 -
   18.76  
   18.77  (*** Theoretical Results from Section 6 ***)
   18.78  
    19.1 --- a/src/HOL/UNITY/Union.ML	Wed Dec 02 16:14:09 1998 +0100
    19.2 +++ b/src/HOL/UNITY/Union.ML	Thu Dec 03 10:45:06 1998 +0100
    19.3 @@ -8,55 +8,124 @@
    19.4  From Misra's Chapter 5: Asynchronous Compositions of Programs
    19.5  *)
    19.6  
    19.7 +Goal "k:I ==> (INT i:I. A i) Int A k = (INT i:I. A i)";
    19.8 +by (Blast_tac 1);
    19.9 +qed "INT_absorb2";
   19.10 +
   19.11 +
   19.12 +val rinst = read_instantiate_sg (sign_of thy);
   19.13 +
   19.14 +Addcongs [UN_cong, INT_cong];
   19.15  
   19.16  (** SKIP **)
   19.17  
   19.18 -Goal "Init SKIP = UNIV";
   19.19 +Goal "States (SKIP A) = A";
   19.20 +by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   19.21 +qed "States_SKIP";
   19.22 +
   19.23 +Goal "Init (SKIP A) = A";
   19.24  by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   19.25  qed "Init_SKIP";
   19.26  
   19.27 -Goal "Acts SKIP = {Id}";
   19.28 +Goal "Acts (SKIP A) = {diag A}";
   19.29  by (simp_tac (simpset() addsimps [SKIP_def]) 1);
   19.30  qed "Acts_SKIP";
   19.31  
   19.32 -Addsimps [Init_SKIP, Acts_SKIP];
   19.33 +Addsimps [States_SKIP, Init_SKIP, Acts_SKIP];
   19.34  
   19.35 -Goal "reachable SKIP = UNIV";
   19.36 -by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
   19.37 +Goal "reachable (SKIP A) = A";
   19.38 +by (force_tac (claset() addEs [reachable.induct]
   19.39 +			addIs reachable.intrs, simpset()) 1);
   19.40  qed "reachable_SKIP";
   19.41  
   19.42  Addsimps [reachable_SKIP];
   19.43  
   19.44  
   19.45 -(** Join and JN **)
   19.46 +(** Join **)
   19.47 +
   19.48 +Goal "States (F Join G) = States F Int States G";
   19.49 +by (simp_tac (simpset() addsimps [Join_def]) 1);
   19.50 +qed "States_Join";
   19.51  
   19.52  Goal "Init (F Join G) = Init F Int Init G";
   19.53 -by (simp_tac (simpset() addsimps [Join_def]) 1);
   19.54 +by (auto_tac (claset() addIs [impOfSubs Init_subset_States],
   19.55 +	      simpset() addsimps [Join_def]));
   19.56  qed "Init_Join";
   19.57  
   19.58 -Goal "Acts (F Join G) = Acts F Un Acts G";
   19.59 +Goal "States F = States G ==> Acts (F Join G) = Acts F Un Acts G";
   19.60 +by (subgoal_tac "Acts F Un Acts G <= Pow (States G Times States G)" 1);
   19.61 +by (blast_tac (claset() addEs [equalityE] 
   19.62 +                        addDs [impOfSubs Acts_subset_Pow_States]) 2);
   19.63  by (auto_tac (claset(), simpset() addsimps [Join_def]));
   19.64  qed "Acts_Join";
   19.65  
   19.66 +
   19.67 +(** JN **)
   19.68 +
   19.69 +Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = (SKIP UNIV)";
   19.70 +by Auto_tac;
   19.71 +qed "JN_empty";
   19.72 +Addsimps [JN_empty];
   19.73 +
   19.74 +Goal "States (JN i:I. F i) = (INT i:I. States (F i))";
   19.75 +by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   19.76 +qed "States_JN";
   19.77 +
   19.78  Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))";
   19.79 -by (simp_tac (simpset() addsimps [JOIN_def]) 1);
   19.80 +by (auto_tac (claset() addIs [impOfSubs Init_subset_States],
   19.81 +	      simpset() addsimps [JOIN_def]));
   19.82  qed "Init_JN";
   19.83  
   19.84 -Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))";
   19.85 +Goalw [eqStates_def]
   19.86 +     "[| i: I;  eqStates I F |] ==> Acts (JN i:I. F i) = (UN i:I. Acts (F i))";
   19.87 +by (Clarify_tac 1);
   19.88 +by (subgoal_tac "(UN i:I. Acts (F i)) <= Pow (St Times St)" 1);
   19.89 +by (blast_tac (claset() addEs [equalityE] 
   19.90 +                        addDs [impOfSubs Acts_subset_Pow_States]) 2);
   19.91  by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
   19.92  qed "Acts_JN";
   19.93  
   19.94 -Addsimps [Init_Join, Init_JN];
   19.95 +Goal "eqStates I F \
   19.96 +\     ==> Acts (JN i:I. F i) = \
   19.97 +\         (if I={} then {diag UNIV} else (UN i:I. Acts (F i)))";
   19.98 +by (force_tac (claset(), simpset() addsimps [Acts_JN]) 1);
   19.99 +qed "Acts_JN_if";
  19.100 +
  19.101 +Addsimps [States_Join, Init_Join, States_JN, Init_JN];
  19.102 +
  19.103  
  19.104 -Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP";
  19.105 -by Auto_tac;
  19.106 -qed "JN_empty";
  19.107 +Goal "(JN x:insert j I. F x) = (F j) Join (JN x:I. F x)";
  19.108 +by (rtac program_equalityI 1);
  19.109 +by (ALLGOALS Asm_simp_tac);
  19.110 +by (asm_simp_tac 
  19.111 +    (simpset() addsimps [JOIN_def, Join_def, Acts_eq_raw,
  19.112 +			 image_UNION, image_Un, image_image, Int_assoc]) 1);
  19.113 +qed "JN_insert";
  19.114 +Addsimps[JN_insert];
  19.115  
  19.116 -Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
  19.117 -by (rtac program_equalityI 1);
  19.118 -by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
  19.119 -qed "JN_insert";
  19.120 -Addsimps[JN_empty, JN_insert];
  19.121 +Goal "k:I ==> A k Join (JN i:I. A i) = (JN i:I. A i)";
  19.122 +by (stac (JN_insert RS sym) 1);
  19.123 +by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
  19.124 +qed "JN_absorb";
  19.125 +
  19.126 +
  19.127 +Goalw [eqStates_def] "eqStates {} F";
  19.128 +by (Simp_tac 1);
  19.129 +qed "eqStates_empty";
  19.130 +
  19.131 +Goalw [eqStates_def]
  19.132 +    "[| eqStates I F; States (F i) = (INT i: I. States (F i)) |] \
  19.133 +\    ==> eqStates (insert i I) F";
  19.134 +by Auto_tac;
  19.135 +qed "eqStates_insertI";
  19.136 +
  19.137 +Goalw [eqStates_def]
  19.138 +    "eqStates (insert i I) F = \
  19.139 +\    (eqStates I F & (I={} | States (F i) = (INT i: I. States (F i))))";
  19.140 +by Auto_tac;
  19.141 +qed "eqStates_insert_eq";
  19.142 +
  19.143 +Addsimps [eqStates_empty, eqStates_insert_eq];
  19.144  
  19.145  
  19.146  (** Algebraic laws **)
  19.147 @@ -66,170 +135,224 @@
  19.148  qed "Join_commute";
  19.149  
  19.150  Goal "(F Join G) Join H = F Join (G Join H)";
  19.151 -by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
  19.152 +by (rtac program_equalityI 1);
  19.153 +by (ALLGOALS (asm_simp_tac (simpset() addsimps Un_ac@[Int_assoc])));
  19.154 +by (asm_simp_tac 
  19.155 +    (simpset() addsimps Un_ac@Int_ac@[Join_def, Acts_eq_raw,
  19.156 +				      image_Un, image_image]) 1);
  19.157 +by (Blast_tac 1);
  19.158  qed "Join_assoc";
  19.159   
  19.160 -Goalw [Join_def, SKIP_def] "SKIP Join F = F";
  19.161 +Goalw [Join_def, SKIP_def] "States F <= A ==> (SKIP A) Join F = F";
  19.162  by (rtac program_equalityI 1);
  19.163 -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
  19.164 +by (ALLGOALS
  19.165 +    (asm_simp_tac (simpset() addsimps 
  19.166 +		   Int_ac@[Acts_subset_Pow_States RS restrict_rel_image, 
  19.167 +			   Acts_eq_raw, insert_absorb, Int_absorb1])));
  19.168 +by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1);
  19.169  qed "Join_SKIP_left";
  19.170  
  19.171 -Goalw [Join_def, SKIP_def] "F Join SKIP = F";
  19.172 -by (rtac program_equalityI 1);
  19.173 -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
  19.174 +Goal "States F <= A ==> F Join (SKIP A) = F";
  19.175 +by (stac Join_commute 1);
  19.176 +by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1);
  19.177  qed "Join_SKIP_right";
  19.178  
  19.179  Addsimps [Join_SKIP_left, Join_SKIP_right];
  19.180  
  19.181  Goalw [Join_def] "F Join F = F";
  19.182  by (rtac program_equalityI 1);
  19.183 -by Auto_tac;
  19.184 +by (ALLGOALS
  19.185 +    (asm_simp_tac (simpset() addsimps 
  19.186 +		   [insert_absorb, Acts_subset_Pow_States RS Acts_eq])));
  19.187 +by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1);
  19.188  qed "Join_absorb";
  19.189  
  19.190  Addsimps [Join_absorb];
  19.191  
  19.192 -
  19.193 -Goal "i : I ==> (JN i:I. A i Join B) = ((JN i:I. A i) Join B)";
  19.194 -by (auto_tac (claset() addSIs [program_equalityI],
  19.195 -	      simpset() addsimps [Acts_JN, Acts_Join]));
  19.196 -qed "JN_Join_miniscope";
  19.197 -
  19.198 -Goal "k:I ==> A k Join (JN i:I. A i) = (JN i:I. A i)";
  19.199 -by (auto_tac (claset() addSIs [program_equalityI],
  19.200 -	      simpset() addsimps [Acts_JN, Acts_Join]));
  19.201 -qed "JN_absorb";
  19.202 -
  19.203  Goal "(JN i: I Un J. A i) = ((JN i: I. A i) Join (JN i:J. A i))";
  19.204 -by (auto_tac (claset() addSIs [program_equalityI],
  19.205 -	      simpset() addsimps [Acts_JN, Acts_Join]));
  19.206 +by (rtac program_equalityI 1);
  19.207 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [INT_Un])));
  19.208 +by (asm_simp_tac 
  19.209 +    (simpset() addsimps Int_ac@
  19.210 +                        [JOIN_def, Join_def, Acts_eq_raw, UN_Un, INT_Un, 
  19.211 +			 image_UNION, image_Un, image_image]) 1);
  19.212  qed "JN_Join";
  19.213  
  19.214  Goal "i: I ==> (JN i:I. c) = c";
  19.215  by (auto_tac (claset() addSIs [program_equalityI],
  19.216 -	      simpset() addsimps [Acts_JN]));
  19.217 +	      simpset() addsimps [Acts_JN, eqStates_def]));
  19.218  qed "JN_constant";
  19.219  
  19.220  Goal "(JN i:I. A i Join B i) = (JN i:I. A i)  Join  (JN i:I. B i)";
  19.221 -by (auto_tac (claset() addSIs [program_equalityI],
  19.222 -	      simpset() addsimps [Acts_JN, Acts_Join]));
  19.223 +by (rtac program_equalityI 1);
  19.224 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [INT_Int_distrib])));
  19.225 +by (asm_simp_tac 
  19.226 +    (simpset() addsimps [JOIN_def, Join_def, Acts_eq_raw, image_UNION, 
  19.227 +			 rinst [("A","%x. States (A x) Int States (B x)")] 
  19.228 +			     INT_absorb2, 
  19.229 +			 image_Un, image_image]) 1);
  19.230 +by (asm_simp_tac (simpset() addsimps [INT_Int_distrib RS sym] @ Int_ac) 1);
  19.231 +by (Blast_tac 1);
  19.232  qed "JN_Join_distrib";
  19.233  
  19.234 +Goal "i : I ==> (JN i:I. A i Join B) = ((JN i:I. A i) Join B)";
  19.235 +by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1);
  19.236 +qed "JN_Join_miniscope";
  19.237 +
  19.238  
  19.239  (*** Safety: constrains, stable, FP ***)
  19.240  
  19.241 -Goalw [constrains_def, JOIN_def]
  19.242 -    "i : I ==> \
  19.243 -\    (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
  19.244 -by (Simp_tac 1);
  19.245 -by (Blast_tac 1);
  19.246 -qed "constrains_JN";
  19.247 +Goal "[| F : constrains A B;  G : constrains A B |] \
  19.248 +\     ==> F Join G : constrains A B";
  19.249 +by (auto_tac (claset(),
  19.250 +	      simpset() addsimps [constrains_def, Join_def, Acts_eq_raw, 
  19.251 +				  image_Un]));
  19.252 +by (REPEAT (force_tac (claset() addSEs [ballE], simpset()) 1));
  19.253 +qed "constrains_imp_Join_constrains";
  19.254  
  19.255 -Goal "F Join G : constrains A B =  \
  19.256 -\     (F : constrains A B & G : constrains A B)";
  19.257 -by (auto_tac
  19.258 -    (claset(),
  19.259 -     simpset() addsimps [constrains_def, Join_def]));
  19.260 +Goal "States F = States G ==> \
  19.261 +\     F Join G : constrains A B = (F : constrains A B & G : constrains A B)";
  19.262 +by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
  19.263  qed "constrains_Join";
  19.264  
  19.265 -(**FAILS, I think; see 5.4.1, Substitution Axiom.
  19.266 -   The problem is to relate reachable (F Join G) with 
  19.267 -   reachable F and reachable G
  19.268 +Goal "[| i : I;  ALL i:I. F i : constrains A B |] \
  19.269 +\     ==> (JN i:I. F i) : constrains A B";
  19.270 +by (full_simp_tac (simpset() addsimps [constrains_def, JOIN_def, Acts_eq_raw, 
  19.271 +				  image_Un]) 1);
  19.272 +by Safe_tac;
  19.273 +by (REPEAT (force_tac (claset() addSEs [ballE], simpset()) 1));
  19.274 +qed "constrains_imp_JN_constrains";
  19.275  
  19.276 -Goalw [Constrains_def]
  19.277 -    "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)";
  19.278 -by (simp_tac (simpset() addsimps [constrains_JN]) 1);
  19.279 -by (Blast_tac 1);
  19.280 -qed "Constrains_JN";
  19.281 +Goal "[| i : I;  eqStates I F |] \
  19.282 +\     ==> (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
  19.283 +by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_JN]));
  19.284 +qed "constrains_JN";
  19.285 +
  19.286 +    (**FAILS, I think; see 5.4.1, Substitution Axiom.
  19.287 +       The problem is to relate reachable (F Join G) with 
  19.288 +       reachable F and reachable G
  19.289  
  19.290 -Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)";
  19.291 -by (auto_tac
  19.292 -    (claset(),
  19.293 -     simpset() addsimps [Constrains_def, constrains_Join]));
  19.294 -qed "Constrains_Join";
  19.295 -**)
  19.296 +    Goalw [Constrains_def]
  19.297 +	"(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)";
  19.298 +    by (simp_tac (simpset() addsimps [constrains_JN]) 1);
  19.299 +    by (Blast_tac 1);
  19.300 +    qed "Constrains_JN";
  19.301  
  19.302 -Goal "[| F : constrains A A';  G : constrains B B' |] \
  19.303 +    Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)";
  19.304 +    by (auto_tac
  19.305 +	(claset(),
  19.306 +	 simpset() addsimps [Constrains_def, constrains_Join]));
  19.307 +    qed "Constrains_Join";
  19.308 +    **)
  19.309 +
  19.310 +Goal "[| F : constrains A A';  G : constrains B B';  States F = States G |] \
  19.311  \     ==> F Join G : constrains (A Int B) (A' Un B')";
  19.312 -by (simp_tac (simpset() addsimps [constrains_Join]) 1);
  19.313 +by (asm_simp_tac (simpset() addsimps [constrains_Join]) 1);
  19.314  by (blast_tac (claset() addIs [constrains_weaken]) 1);
  19.315  qed "constrains_Join_weaken";
  19.316  
  19.317 -Goal "i : I ==> \
  19.318 -\     (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
  19.319 +Goal "[| i : I;  eqStates I F |]  \
  19.320 +\     ==> (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
  19.321  by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
  19.322  qed "stable_JN";
  19.323  
  19.324 -Goal "[| ALL i:I. F i : invariant A;  i : I |]  \
  19.325 +Goal "[| ALL i:I. F i : invariant A;  i : I;  eqStates I F |]  \
  19.326  \      ==> (JN i:I. F i) : invariant A";
  19.327  by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_JN]) 1);
  19.328  by (Blast_tac 1);
  19.329  bind_thm ("invariant_JN_I", ballI RS result());
  19.330  
  19.331 -Goal "F Join G : stable A = \
  19.332 -\     (F : stable A & G : stable A)";
  19.333 -by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
  19.334 +Goal "States F = States G \
  19.335 +\     ==> F Join G : stable A = (F : stable A & G : stable A)";
  19.336 +by (asm_simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
  19.337  qed "stable_Join";
  19.338  
  19.339 -Goal "[| F : invariant A; G : invariant A |]  \
  19.340 +Goal "[| F : invariant A; G : invariant A; States F = States G |]  \
  19.341  \     ==> F Join G : invariant A";
  19.342 -by (full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1);
  19.343 +by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1);
  19.344  by (Blast_tac 1);
  19.345  qed "invariant_JoinI";
  19.346  
  19.347 -Goal "i : I ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
  19.348 +Goal "[| i : I;  eqStates I F |]  \
  19.349 +\      ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
  19.350  by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
  19.351  qed "FP_JN";
  19.352  
  19.353  
  19.354  (*** Progress: transient, ensures ***)
  19.355  
  19.356 -Goal "i : I ==> \
  19.357 -\   (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
  19.358 -by (auto_tac (claset(),
  19.359 -	      simpset() addsimps [transient_def, JOIN_def]));
  19.360 +
  19.361 +Goal "[| (JN i:I. F i) : transient A;  i: I |] ==> EX i:I. F i : transient A";
  19.362 +by (full_simp_tac (simpset() addsimps [transient_def, JOIN_def, Acts_eq_raw, 
  19.363 +				  Int_absorb1, restrict_rel_def]) 1);
  19.364 +by Safe_tac;
  19.365 +by (REPEAT (blast_tac (claset() addSIs [rev_bexI]) 1));
  19.366 +qed "transient_JN_imp_transient";
  19.367 +
  19.368 +Goal "[| i : I;  eqStates I F |]  \
  19.369 +\     ==> (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
  19.370 +by (auto_tac (claset() addSIs [transient_JN_imp_transient], simpset()));
  19.371 +by (auto_tac (claset(), simpset() addsimps [transient_def, Acts_JN]));
  19.372  qed "transient_JN";
  19.373  
  19.374 -Goal "F Join G : transient A = \
  19.375 -\     (F : transient A | G : transient A)";
  19.376 -by (auto_tac (claset(),
  19.377 -	      simpset() addsimps [bex_Un, transient_def,
  19.378 -				  Join_def]));
  19.379 +Goal "F Join G : transient A ==> \
  19.380 +\     F : transient A | G : transient A";
  19.381 +by (full_simp_tac (simpset() addsimps [transient_def, Join_def, Acts_eq_raw, 
  19.382 +				       restrict_rel_def]) 1);
  19.383 +by Safe_tac;
  19.384 +(*delete act:Acts F possibility*)
  19.385 +by (rtac FalseE 3);  
  19.386 +(*delete act:Acts G possibility*)
  19.387 +by (thin_tac "~ (EX act:Acts G. ?P act)" 2);
  19.388 +by (REPEAT (blast_tac (claset() addSIs [rev_bexI]) 1));
  19.389 +qed "transient_Join_imp_transient";
  19.390 +
  19.391 +Goal "States F = States G  \
  19.392 +\     ==> (F Join G : transient A) = (F : transient A | G : transient A)";
  19.393 +by (auto_tac (claset() addSIs [transient_Join_imp_transient], simpset()));
  19.394 +by (auto_tac (claset(), simpset() addsimps [transient_def, Acts_Join]));
  19.395  qed "transient_Join";
  19.396  
  19.397 -Goal "i : I ==> \
  19.398 -\     (JN i:I. F i) : ensures A B = \
  19.399 -\     ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
  19.400 -\      (EX i:I. F i : ensures A B))";
  19.401 +Goal "[| i : I;  eqStates I F |]  \
  19.402 +\     ==> (JN i:I. F i) : ensures A B = \
  19.403 +\         ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
  19.404 +\          (EX i:I. F i : ensures A B))";
  19.405  by (auto_tac (claset(),
  19.406  	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
  19.407  qed "ensures_JN";
  19.408  
  19.409  Goalw [ensures_def]
  19.410 -     "F Join G : ensures A B =     \
  19.411 -\     (F : constrains (A-B) (A Un B) & \
  19.412 -\      G : constrains (A-B) (A Un B) & \
  19.413 -\      (F : ensures A B | G : ensures A B))";
  19.414 +     "States F = States G  \
  19.415 +\     ==> F Join G : ensures A B =     \
  19.416 +\         (F : constrains (A-B) (A Un B) & \
  19.417 +\          G : constrains (A-B) (A Un B) & \
  19.418 +\          (F : ensures A B | G : ensures A B))";
  19.419  by (auto_tac (claset(),
  19.420  	      simpset() addsimps [constrains_Join, transient_Join]));
  19.421  qed "ensures_Join";
  19.422  
  19.423 -Goalw [stable_def, constrains_def, Join_def]
  19.424 -    "[| F : stable A;  G : constrains A A' |] \
  19.425 +Goal "[| F : stable A;  G : constrains A A';  \
  19.426 +\        States F = States G; A <= States G |] \
  19.427  \    ==> F Join G : constrains A A'";
  19.428 -by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
  19.429 +by (forward_tac [constrains_imp_subset] 1);
  19.430 +by (assume_tac 1);
  19.431 +by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def,
  19.432 +					   ball_Un, Acts_Join]) 1);
  19.433  by (Blast_tac 1);
  19.434  qed "stable_constrains_Join";
  19.435  
  19.436  (*Premise for G cannot use Invariant because  Stable F A  is weaker than
  19.437    G : stable A *)
  19.438 -Goal "[| F : stable A;  G : invariant A |] ==> F Join G : Invariant A";
  19.439 -by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, 
  19.440 -				       Stable_eq_stable, stable_Join]) 1);
  19.441 +Goal "[| F : stable A;  G : invariant A;  \
  19.442 +\        States F = States G |] ==> F Join G : Invariant A";
  19.443 +by (asm_full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, 
  19.444 +					   Stable_eq_stable, stable_Join]) 1);
  19.445  by (force_tac(claset() addIs [stable_reachable, stable_Int],
  19.446  	      simpset() addsimps [Acts_Join]) 1);
  19.447  qed "stable_Join_Invariant";
  19.448  
  19.449 -Goal "[| F : stable A;  G : ensures A B |] ==> F Join G : ensures A B";
  19.450 +Goal "[| F : stable A;  G : ensures A B;  \
  19.451 +\        States F = States G |] ==> F Join G : ensures A B";
  19.452  by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
  19.453  by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
  19.454  by (etac constrains_weaken 1);
  19.455 @@ -237,35 +360,61 @@
  19.456  qed "ensures_stable_Join1";
  19.457  
  19.458  (*As above, but exchanging the roles of F and G*)
  19.459 -Goal "[| F : ensures A B;  G : stable A |] ==> F Join G : ensures A B";
  19.460 +Goal "[| F : ensures A B;  G : stable A;  \
  19.461 +\        States F = States G |] ==> F Join G : ensures A B";
  19.462  by (stac Join_commute 1);
  19.463 +by (dtac sym 1);
  19.464  by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
  19.465  qed "ensures_stable_Join2";
  19.466  
  19.467  
  19.468  (** Diff and localTo **)
  19.469  
  19.470 -Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G";
  19.471 +
  19.472 +Goal "States (Diff F acts) = States F";
  19.473 +by (simp_tac (simpset() addsimps [Diff_def]) 1);
  19.474 +qed "States_Diff";
  19.475 +
  19.476 +Goal "Init (Diff F acts) = Init F";
  19.477 +by (auto_tac (claset() addIs [impOfSubs Init_subset_States],
  19.478 +	      simpset() addsimps [Diff_def]));
  19.479 +qed "Init_Diff";
  19.480 +
  19.481 +Goal "Acts (Diff F acts) = insert (diag (States F)) (Acts F - acts)";
  19.482 +by (subgoal_tac "Acts F - acts <= Pow (States F Times States F)" 1);
  19.483 +by (blast_tac (claset() addEs [equalityE] 
  19.484 +                        addDs [impOfSubs Acts_subset_Pow_States]) 2);
  19.485 +by (auto_tac (claset(), simpset() addsimps [Diff_def]));
  19.486 +qed "Acts_Diff";
  19.487 +
  19.488 +Addsimps [States_Diff, Init_Diff, Acts_Diff];
  19.489 +
  19.490 +
  19.491 +Goalw [Join_def] "States F = States G ==> F Join (Diff G (Acts F)) = F Join G";
  19.492  by (rtac program_equalityI 1);
  19.493 -by Auto_tac;
  19.494 +by (auto_tac (claset(), simpset() addsimps [insert_absorb]));
  19.495  qed "Join_Diff2";
  19.496  
  19.497 -Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
  19.498 +Goalw [Disjoint_def] "States F = States G ==> Disjoint F (Diff G (Acts F))";
  19.499  by Auto_tac;
  19.500  qed "Diff_Disjoint";
  19.501  
  19.502 +Goalw [Disjoint_def] "Disjoint F G ==> States F = States G";
  19.503 +by Auto_tac;
  19.504 +qed "Disjoint_States_eq";
  19.505 +
  19.506  Goal "[| F Join G : v localTo F;  Disjoint F G |] \
  19.507  \     ==> G : (INT z. stable {s. v s = z})";
  19.508  by (asm_full_simp_tac 
  19.509 -    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
  19.510 +    (simpset() addsimps [localTo_def, Disjoint_def,
  19.511  			 Acts_Join, stable_def, constrains_def]) 1);
  19.512  by (Blast_tac 1);
  19.513  qed "localTo_imp_stable";
  19.514  
  19.515  Goal "[| F Join G : v localTo F;  (s,s') : act;  \
  19.516 -\        act : Acts G;  Disjoint F G |] ==> v s' = v s";
  19.517 +\        act : Acts G;  Disjoint F G  |] ==> v s' = v s";
  19.518  by (asm_full_simp_tac 
  19.519 -    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
  19.520 +    (simpset() addsimps [localTo_def, Disjoint_def,
  19.521  			 Acts_Join, stable_def, constrains_def]) 1);
  19.522  by (Blast_tac 1);
  19.523  qed "localTo_imp_equals";
  19.524 @@ -284,9 +433,15 @@
  19.525  \        F Join G : w localTo F;       \
  19.526  \        Disjoint F G |]               \
  19.527  \     ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
  19.528 -by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
  19.529 +by (auto_tac (claset(), 
  19.530 +	      simpset() addsimps [constrains_def, 
  19.531 +				  Disjoint_States_eq RS Acts_Join]));
  19.532  by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
  19.533 -by Auto_tac;
  19.534 +by (subgoal_tac "xa : States F" 1);
  19.535 +by (force_tac
  19.536 +    (claset() addSDs [Disjoint_States_eq,impOfSubs Acts_subset_Pow_States], 
  19.537 +     simpset()) 2);
  19.538 +by (Force_tac 1);
  19.539  qed "constrains_localTo_constrains2";
  19.540  
  19.541  Goalw [stable_def]
  19.542 @@ -316,7 +471,8 @@
  19.543  by (rtac ballI 1);
  19.544  by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
  19.545  \                                      ({s. v s = k} Un {s. v s <= w s})" 1);
  19.546 -by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
  19.547 +by (asm_simp_tac
  19.548 +    (simpset() addsimps [Disjoint_States_eq RS constrains_Join]) 2);
  19.549  by (blast_tac (claset() addIs [constrains_weaken]) 2);
  19.550  by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
  19.551  by (etac Constrains_weaken 2);
    20.1 --- a/src/HOL/UNITY/Union.thy	Wed Dec 02 16:14:09 1998 +0100
    20.2 +++ b/src/HOL/UNITY/Union.thy	Thu Dec 03 10:45:06 1998 +0100
    20.3 @@ -11,25 +11,33 @@
    20.4  Union = SubstAx + FP +
    20.5  
    20.6  constdefs
    20.7 +  eqStates :: ['a set, 'a => 'b program] => bool
    20.8 +    "eqStates I F == EX St. ALL i:I. States (F i) = St"
    20.9 +
   20.10    JOIN  :: ['a set, 'a => 'b program] => 'b program
   20.11 -    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
   20.12 +    "JOIN I F == mk_program (INT i:I. States (F i),
   20.13 +			     INT i:I. Init (F i),
   20.14 +			     UN i:I. Acts (F i))"
   20.15  
   20.16    Join :: ['a program, 'a program] => 'a program      (infixl 65)
   20.17 -    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
   20.18 +    "F Join G == mk_program (States F Int States G,
   20.19 +			     Init F Int Init G,
   20.20 +			     Acts F Un Acts G)"
   20.21  
   20.22 -  SKIP :: 'a program
   20.23 -    "SKIP == mk_program (UNIV, {})"
   20.24 +  SKIP :: 'a set => 'a program
   20.25 +    "SKIP states == mk_program (states, states, {})"
   20.26  
   20.27    Diff :: "['a program, ('a * 'a)set set] => 'a program"
   20.28 -    "Diff F acts == mk_program (Init F, Acts F - acts)"
   20.29 +    "Diff F acts == mk_program (States F, Init F, Acts F - acts)"
   20.30  
   20.31    (*The set of systems that regard "v" as local to F*)
   20.32    localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
   20.33      "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
   20.34  
   20.35 -  (*Two programs with disjoint actions, except for Id (idling)*)
   20.36 +  (*Two programs with disjoint actions, except for identity actions *)
   20.37    Disjoint :: ['a program, 'a program] => bool
   20.38 -    "Disjoint F G == Acts F Int Acts G <= {Id}"
   20.39 +    "Disjoint F G == States F = States G &
   20.40 +                     Acts F Int Acts G <= {diag (States G)}"
   20.41  
   20.42  syntax
   20.43    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
    21.1 --- a/src/HOL/UNITY/WFair.ML	Wed Dec 02 16:14:09 1998 +0100
    21.2 +++ b/src/HOL/UNITY/WFair.ML	Thu Dec 03 10:45:06 1998 +0100
    21.3 @@ -8,6 +8,10 @@
    21.4  From Misra, "A Logic for Concurrent Programming", 1994
    21.5  *)
    21.6  
    21.7 +    Goal "[| x:A;  P(x) |] ==> ? x:A. P(x)";
    21.8 +    by (Blast_tac 1);
    21.9 +    qed "rev_bexI";
   21.10 +
   21.11  
   21.12  overload_1st_set "WFair.transient";
   21.13  overload_1st_set "WFair.ensures";
   21.14 @@ -23,8 +27,7 @@
   21.15  Goalw [transient_def]
   21.16      "[| F : transient A; B<=A |] ==> F : transient B";
   21.17  by (Clarify_tac 1);
   21.18 -by (rtac bexI 1 THEN assume_tac 2);
   21.19 -by (Blast_tac 1);
   21.20 +by (blast_tac (claset() addSIs [rev_bexI]) 1);
   21.21  qed "transient_strengthen";
   21.22  
   21.23  Goalw [transient_def]