Revising the Client proof as suggested by Michel Charpentier. New lemmas
authorpaulson
Fri Nov 06 13:20:29 1998 +0100 (1998-11-06)
changeset 58048e0a4c4fd67b
parent 5803 06af82bec2f1
child 5805 e867bc95a47d
Revising the Client proof as suggested by Michel Charpentier. New lemmas
about composition (in Union.ML), etc. Also changed "length" to "size"
because it is displayed as "size" in any event.
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Client.thy
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Client.ML	Thu Nov 05 15:33:27 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Client.ML	Fri Nov 06 13:20:29 1998 +0100
     1.3 @@ -7,19 +7,7 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -(*Perhaps move to SubstAx.ML*)
     1.8 -Goal "[| F : Stable A;  F : transient C;  \
     1.9 -\        reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B";
    1.10 -by (etac reachable_LeadsTo_weaken 1);
    1.11 -by (rtac LeadsTo_Diff 1);
    1.12 -by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
    1.13 -by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
    1.14 -qed "Stable_transient_reachable_LeadsTo";
    1.15 -
    1.16 -
    1.17 -
    1.18 -(*split_all_tac causes a big blow-up*)
    1.19 -claset_ref() := claset() delSWrapper record_split_name;
    1.20 +claset_ref() := claset();
    1.21  
    1.22  Addsimps [Cli_prg_def RS def_prg_Init];
    1.23  program_defs_ref := [Cli_prg_def];
    1.24 @@ -29,17 +17,6 @@
    1.25  (*Simplification for records*)
    1.26  Addsimps (thms"state.update_defs");
    1.27  
    1.28 -(*CAN THIS be generalized?
    1.29 -  Importantly, the second case considers actions that are in G
    1.30 -  and NOT in Cli_prg (needed to use localTo_imp_equals) *)
    1.31 -Goal "(act : Acts (Cli_prg Join G)) = \
    1.32 -\      (act : {Id, rel_act, tok_act, ask_act} | \
    1.33 -\       act : Acts G & act ~: Acts Cli_prg)";
    1.34 -by (asm_full_simp_tac (simpset() addsimps [Cli_prg_def, Acts_Join]) 1);
    1.35 -(*don't unfold definitions of actions*)
    1.36 -by (blast_tac HOL_cs 1);
    1.37 -qed "Acts_Cli_Join_eq";
    1.38 -
    1.39  
    1.40  fun invariant_tac i = 
    1.41      rtac invariantI i  THEN
    1.42 @@ -73,92 +50,92 @@
    1.43  *)
    1.44  Goal "Cli_prg:                             \
    1.45  \       invariant ({s. tok s <= Max}  Int  \
    1.46 -\                  {s. ALL n: lessThan (length (ask s)). ask s!n <= Max})";
    1.47 +\                  {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})";
    1.48  by (invariant_tac 1);
    1.49  by (auto_tac (claset() addSEs [less_SucE], simpset()));
    1.50  qed "ask_bounded";
    1.51  
    1.52 +(** Several facts used to prove Lemma 1 **)
    1.53 +
    1.54 +Goal "Cli_prg: stable {s. rel s <= giv s}";
    1.55 +by (constrains_tac 1);
    1.56 +by Auto_tac;
    1.57 +qed "stable_rel_le_giv";
    1.58 +
    1.59 +Goal "Cli_prg: stable {s. size (rel s) <= size (giv s)}";
    1.60 +by (constrains_tac 1);
    1.61 +by Auto_tac;
    1.62 +qed "stable_size_rel_le_giv";
    1.63 +
    1.64 +Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}";
    1.65 +by (constrains_tac 1);
    1.66 +by Auto_tac;
    1.67 +qed "stable_size_ask_le_rel";
    1.68 +
    1.69  
    1.70  (*We no longer need constrains_tac to expand the program definition, and 
    1.71 -  expanding it is extremely expensive!  Instead, Acts_Cli_Join_eq expands
    1.72 -  the program.*)
    1.73 +  expanding it is extremely expensive!*)
    1.74  program_defs_ref := [];
    1.75  
    1.76  (*Safety property 2: clients return the right number of tokens*)
    1.77 -Goalw [increasing_def]
    1.78 -      "Cli_prg : (increasing giv Int (rel localTo Cli_prg))  \
    1.79 -\                guarantees invariant {s. rel s <= giv s}";
    1.80 +Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
    1.81 +\               guarantees Invariant {s. rel s <= giv s}";
    1.82  by (rtac guaranteesI 1);
    1.83 -by (invariant_tac 1);
    1.84 +by (rtac InvariantI 1);
    1.85  by (Force_tac 1);
    1.86 -by (subgoal_tac "rel s <= giv s'" 1);
    1.87 -by (force_tac (claset(),
    1.88 -	       simpset() addsimps [stable_def, constrains_def]) 2);
    1.89 -by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
    1.90 -(*we note that "rel" is local to Client*)
    1.91 -by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
    1.92 +by (blast_tac (claset() addIs [Increasing_localTo_Stable, 
    1.93 +			       stable_rel_le_giv]) 1);
    1.94  qed "ok_guar_rel_prefix_giv";
    1.95  
    1.96  
    1.97  (*** Towards proving the liveness property ***)
    1.98  
    1.99  Goal "Cli_prg Join G   \
   1.100 -\       : transient {s. length (giv s) = Suc k &  \
   1.101 -\                       length (rel s) = k & ask s ! k <= giv s ! k}";
   1.102 +\       : transient {s. size (giv s) = Suc k &  \
   1.103 +\                       size (rel s) = k & ask s ! k <= giv s ! k}";
   1.104  by (res_inst_tac [("act", "rel_act")] transient_mem 1);
   1.105  by (auto_tac (claset(),
   1.106  	      simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def]));
   1.107  qed "transient_lemma";
   1.108  
   1.109 +
   1.110 +
   1.111 +val rewrite_o = rewrite_rule [o_def];
   1.112 +
   1.113  Goal "Cli_prg : \
   1.114 -\      (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
   1.115 -\                 Int invariant giv_meets_ask) \
   1.116 -\      guarantees invariant {s. length (ask s) <= Suc (length (rel s)) & \
   1.117 -\                               length (rel s) <= length (giv s)}";
   1.118 +\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
   1.119 +\      guarantees Invariant ({s. size (ask s) <= Suc (size (rel s))} Int \
   1.120 +\                            {s. size (rel s) <= size (giv s)})";
   1.121  by (rtac guaranteesI 1);
   1.122  by (Clarify_tac 1);
   1.123 -by (dtac (impOfSubs increasing_length) 1);
   1.124 -by (invariant_tac 1);
   1.125 - by (Force_tac 1);
   1.126 -by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
   1.127 -by Auto_tac;
   1.128 - by (TRYALL (dtac localTo_imp_equals THEN' atac));
   1.129 -     by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
   1.130 -by (force_tac (claset() addD2 ("x",localTo_imp_equals),
   1.131 -	       simpset() addsimps [increasing_def, Acts_Join, stable_def, 
   1.132 -				   constrains_def]) 1);
   1.133 +by (dtac (impOfSubs (rewrite_o Increasing_size)) 1);
   1.134 +by (rtac InvariantI 1);
   1.135 +by (Force_tac 1);
   1.136 +by (rtac Stable_Int 1);
   1.137 +by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
   1.138 +	               addIs [Increasing_localTo_Stable, 
   1.139 +			      stable_size_rel_le_giv]) 2);
   1.140 +by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
   1.141 +	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
   1.142 +			      stable_size_ask_le_rel]) 1);
   1.143  val lemma1 = result();
   1.144  
   1.145  
   1.146  Goal "Cli_prg : \
   1.147 -\      (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
   1.148 -\                 Int invariant giv_meets_ask) \
   1.149 -\      guarantees (LeadsTo {s. k < length (giv s)}    \
   1.150 -\                          {s. k < length (rel s)})";
   1.151 +\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
   1.152 +\                 Int Invariant giv_meets_ask) \
   1.153 +\      guarantees (LeadsTo {s. k < size (giv s)}    \
   1.154 +\                          {s. k < size (rel s)})";
   1.155  by (rtac guaranteesI 1);
   1.156  by (Clarify_tac 1);
   1.157  by (rtac Stable_transient_reachable_LeadsTo 1);
   1.158 -  by (res_inst_tac [("k", "k")] transient_lemma 2);
   1.159 - by (rtac stable_imp_Stable 1);
   1.160 - by (dtac (impOfSubs increasing_length) 1);
   1.161 - by (force_tac (claset(),
   1.162 - 	        simpset() addsimps [increasing_def, 
   1.163 -				   stable_def, constrains_def]) 1);
   1.164 -(** LEVEL 7 **)
   1.165 -(*
   1.166 - 1. !!G. [| Cli_prg Join G : invariant giv_meets_ask;
   1.167 -            Cli_prg Join G : ask localTo Cli_prg;
   1.168 -            Cli_prg Join G : increasing giv;
   1.169 -            Cli_prg Join G : rel localTo Cli_prg |]
   1.170 -         ==> reachable (Cli_prg Join G)
   1.171 -             <= - {s. k < length (giv s)} Un {s. k < length (rel s)} Un
   1.172 -                {s. length (giv s) = Suc k &
   1.173 -                    length (rel s) = k & ask s ! k <= giv s ! k}
   1.174 -x
   1.175 -*)
   1.176 +by (res_inst_tac [("k", "k")] transient_lemma 2);
   1.177 +by (force_tac (claset() addDs [impOfSubs Increasing_size,
   1.178 +			       impOfSubs Increasing_Stable_less],
   1.179 +	       simpset()) 1);
   1.180  by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
   1.181   by (Blast_tac 1);
   1.182 -by (auto_tac (claset() addSDs [invariant_includes_reachable],
   1.183 -	      simpset() addsimps [giv_meets_ask_def]));
   1.184 +by (auto_tac (claset(),
   1.185 +	      simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
   1.186  by (ALLGOALS Force_tac);
   1.187  qed "client_correct";
     2.1 --- a/src/HOL/UNITY/Client.thy	Thu Nov 05 15:33:27 1998 +0100
     2.2 +++ b/src/HOL/UNITY/Client.thy	Fri Nov 06 13:20:29 1998 +0100
     2.3 @@ -29,9 +29,9 @@
     2.4    
     2.5    rel_act :: "(state*state) set"
     2.6      "rel_act == {(s,s').
     2.7 -		  EX nrel. nrel = length (rel s) &
     2.8 +		  EX nrel. nrel = size (rel s) &
     2.9  		           s' = s (| rel := rel s @ [giv s!nrel] |) &
    2.10 -		           nrel < length (giv s) &
    2.11 +		           nrel < size (giv s) &
    2.12  		           ask s!nrel <= giv s!nrel}"
    2.13  
    2.14    (** Choose a new token requirement **)
    2.15 @@ -45,7 +45,7 @@
    2.16    ask_act :: "(state*state) set"
    2.17      "ask_act == {(s,s'). s'=s |
    2.18  		         (s' = s (|ask := ask s @ [tok s]|) &
    2.19 -		          length (ask s) = length (rel s))}"
    2.20 +		          size (ask s) = size (rel s))}"
    2.21  
    2.22    Cli_prg :: state program
    2.23      "Cli_prg == mk_program ({s. tok s : atMost Max &
    2.24 @@ -56,7 +56,7 @@
    2.25  
    2.26    giv_meets_ask :: state set
    2.27      "giv_meets_ask ==
    2.28 -       {s. length (giv s) <= length (ask s) & 
    2.29 -           (ALL n: lessThan (length (giv s)). ask s!n <= giv s!n)}"
    2.30 +       {s. size (giv s) <= size (ask s) & 
    2.31 +           (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}"
    2.32  
    2.33  end
     3.1 --- a/src/HOL/UNITY/Comp.ML	Thu Nov 05 15:33:27 1998 +0100
     3.2 +++ b/src/HOL/UNITY/Comp.ML	Fri Nov 06 13:20:29 1998 +0100
     3.3 @@ -43,6 +43,10 @@
     3.4  				      component_Acts, component_Init]) 1);
     3.5  qed "component_anti_sym";
     3.6  
     3.7 +Goalw [component_def]
     3.8 +      "component F H = (EX G. F Join G = H & Disjoint F G)";
     3.9 +by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
    3.10 +qed "component_eq";
    3.11  
    3.12  (*** existential properties ***)
    3.13  
    3.14 @@ -101,8 +105,9 @@
    3.15  (*** guarantees ***)
    3.16  
    3.17  (*This equation is more intuitive than the official definition*)
    3.18 -Goalw [guarantees_def, component_def]
    3.19 -      "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
    3.20 +Goal "(F : A guarantees B) = \
    3.21 +\     (ALL G. F Join G : A & Disjoint F G --> F Join G : B)";
    3.22 +by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
    3.23  by (Blast_tac 1);
    3.24  qed "guarantees_eq";
    3.25  
    3.26 @@ -154,13 +159,16 @@
    3.27  by (Blast_tac 1);
    3.28  qed "ex_guarantees";
    3.29  
    3.30 -val prems = Goalw [guarantees_def, component_def]
    3.31 -      "(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
    3.32 +val prems = Goal
    3.33 +     "(!!G. [| F Join G : A;  Disjoint F G |] ==> F Join G : B) \
    3.34 +\     ==> F : A guarantees B";
    3.35 +by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
    3.36  by (blast_tac (claset() addIs prems) 1);
    3.37  qed "guaranteesI";
    3.38  
    3.39 -Goal "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
    3.40 -by (asm_full_simp_tac (simpset() addsimps [guarantees_eq]) 1);
    3.41 +Goalw [guarantees_def, component_def]
    3.42 +     "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
    3.43 +by (Blast_tac 1);
    3.44  qed "guaranteesD";
    3.45  
    3.46  
     4.1 --- a/src/HOL/UNITY/Constrains.ML	Thu Nov 05 15:33:27 1998 +0100
     4.2 +++ b/src/HOL/UNITY/Constrains.ML	Fri Nov 06 13:20:29 1998 +0100
     4.3 @@ -81,7 +81,7 @@
     4.4  by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
     4.5  qed "Constrains_Int";
     4.6  
     4.7 -Goal "[| ALL i:I. F : Constrains (A i) (A' i) |]   \
     4.8 +Goal "ALL i:I. F : Constrains (A i) (A' i)   \
     4.9  \     ==> F : Constrains (INT i:I. A i) (INT i:I. A' i)";
    4.10  by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
    4.11  by (dtac ball_constrains_INT 1);
    4.12 @@ -140,6 +140,11 @@
    4.13  qed "Stable_Constrains_Int";
    4.14  
    4.15  Goalw [Stable_def]
    4.16 +    "(ALL i:I. F : Stable (A i)) ==> F : Stable (UN i:I. A i)";
    4.17 +by (etac ball_Constrains_UN 1);
    4.18 +qed "ball_Stable_UN";
    4.19 +
    4.20 +Goalw [Stable_def]
    4.21      "(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
    4.22  by (etac ball_Constrains_INT 1);
    4.23  qed "ball_Stable_INT";
    4.24 @@ -156,13 +161,13 @@
    4.25       "Increasing f <= Increasing (length o f)";
    4.26  by Auto_tac;
    4.27  by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
    4.28 -qed "Increasing_length";
    4.29 +qed "Increasing_size";
    4.30  
    4.31  Goalw [Increasing_def]
    4.32       "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
    4.33  by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
    4.34  by (Blast_tac 1);
    4.35 -qed "Increasing_less";
    4.36 +qed "Increasing_Stable_less";
    4.37  
    4.38  Goalw [increasing_def, Increasing_def]
    4.39       "F : increasing f ==> F : Increasing f";
    4.40 @@ -211,13 +216,7 @@
    4.41  bind_thm ("InvariantE", InvariantD RS conjE);
    4.42  
    4.43  
    4.44 -(*The set of all reachable states is an Invariant...*)
    4.45 -Goal "F : Invariant (reachable F)";
    4.46 -by (simp_tac (simpset() addsimps [Invariant_def]) 1);
    4.47 -by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1);
    4.48 -qed "Invariant_reachable";
    4.49 -
    4.50 -(*...in fact the strongest Invariant!*)
    4.51 +(*The set of all reachable states is the strongest Invariant*)
    4.52  Goal "F : Invariant A ==> reachable F <= A";
    4.53  by (full_simp_tac 
    4.54      (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
    4.55 @@ -233,22 +232,33 @@
    4.56  qed "invariant_imp_Invariant";
    4.57  
    4.58  Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
    4.59 -     "(F : Invariant A) = (F : invariant (reachable F Int A))";
    4.60 +     "Invariant A = {F. F : invariant (reachable F Int A)}";
    4.61  by (blast_tac (claset() addIs reachable.intrs) 1);
    4.62  qed "Invariant_eq_invariant_reachable";
    4.63  
    4.64 +(*Invariant is the "always" notion*)
    4.65 +Goal "Invariant A = {F. reachable F <= A}";
    4.66 +by (auto_tac (claset() addDs [invariant_includes_reachable],
    4.67 +	      simpset() addsimps [Int_absorb2, invariant_reachable,
    4.68 +				  Invariant_eq_invariant_reachable]));
    4.69 +qed "Invariant_eq_always";
    4.70  
    4.71  
    4.72 -Goal "F : Invariant INV ==> reachable F Int INV = reachable F";
    4.73 -by (dtac Invariant_includes_reachable 1);
    4.74 -by (Blast_tac 1);
    4.75 -qed "reachable_Int_INV";
    4.76 +Goal "Invariant A = (UN I: Pow A. invariant I)";
    4.77 +by (simp_tac (simpset() addsimps [Invariant_eq_always]) 1);
    4.78 +by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
    4.79 +                               stable_reachable,
    4.80 +			       impOfSubs invariant_includes_reachable]) 1);
    4.81 +qed "Invariant_eq_UN_invariant";
    4.82 +
    4.83 +
    4.84 +(*** "Constrains" rules involving Invariant ***)
    4.85  
    4.86  Goal "[| F : Invariant INV;  F : Constrains (INV Int A) A' |]   \
    4.87  \     ==> F : Constrains A A'";
    4.88  by (asm_full_simp_tac
    4.89 -    (simpset() addsimps [Constrains_def, reachable_Int_INV,
    4.90 -			 Int_assoc RS sym]) 1);
    4.91 +    (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
    4.92 +			 Constrains_def, Int_assoc RS sym]) 1);
    4.93  qed "Invariant_ConstrainsI";
    4.94  
    4.95  (* [| F : Invariant INV; F : Constrains (INV Int A) A |]
    4.96 @@ -258,8 +268,8 @@
    4.97  Goal "[| F : Invariant INV;  F : Constrains A A' |]   \
    4.98  \     ==> F : Constrains A (INV Int A')";
    4.99  by (asm_full_simp_tac
   4.100 -    (simpset() addsimps [Constrains_def, reachable_Int_INV,
   4.101 -			 Int_assoc RS sym]) 1);
   4.102 +    (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
   4.103 +			 Constrains_def, Int_assoc RS sym]) 1);
   4.104  qed "Invariant_ConstrainsD";
   4.105  
   4.106  bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
   4.107 @@ -269,8 +279,7 @@
   4.108  (** Conjoining Invariants **)
   4.109  
   4.110  Goal "[| F : Invariant A;  F : Invariant B |] ==> F : Invariant (A Int B)";
   4.111 -by (auto_tac (claset(),
   4.112 -	      simpset() addsimps [Invariant_def, Stable_Int]));
   4.113 +by (auto_tac (claset(), simpset() addsimps [Invariant_eq_always]));
   4.114  qed "Invariant_Int";
   4.115  
   4.116  (*Delete the nearest invariance assumption (which will be the second one
     5.1 --- a/src/HOL/UNITY/SubstAx.ML	Thu Nov 05 15:33:27 1998 +0100
     5.2 +++ b/src/HOL/UNITY/SubstAx.ML	Fri Nov 06 13:20:29 1998 +0100
     5.3 @@ -294,6 +294,15 @@
     5.4  qed "PSP_Unless";
     5.5  
     5.6  
     5.7 +Goal "[| F : Stable A;  F : transient C;  \
     5.8 +\        reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B";
     5.9 +by (etac reachable_LeadsTo_weaken 1);
    5.10 +by (rtac LeadsTo_Diff 1);
    5.11 +by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
    5.12 +by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
    5.13 +qed "Stable_transient_reachable_LeadsTo";
    5.14 +
    5.15 +
    5.16  (*** Induction rules ***)
    5.17  
    5.18  (** Meta or object quantifier ????? **)
     6.1 --- a/src/HOL/UNITY/UNITY.ML	Thu Nov 05 15:33:27 1998 +0100
     6.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Nov 06 13:20:29 1998 +0100
     6.3 @@ -69,12 +69,6 @@
     6.4  by (Blast_tac 1);
     6.5  qed "ball_constrains_UN";
     6.6  
     6.7 -Goalw [constrains_def]
     6.8 -    "[| ALL i. F : constrains (A i) (A' i) |] \
     6.9 -\    ==> F : constrains (UN i. A i) (UN i. A' i)";
    6.10 -by (Blast_tac 1);
    6.11 -qed "all_constrains_UN";
    6.12 -
    6.13  (** Intersection **)
    6.14  
    6.15  Goalw [constrains_def]
    6.16 @@ -89,12 +83,6 @@
    6.17  by (Blast_tac 1);
    6.18  qed "ball_constrains_INT";
    6.19  
    6.20 -Goalw [constrains_def]
    6.21 -    "[| ALL i. F : constrains (A i) (A' i) |] \
    6.22 -\    ==> F : constrains (INT i. A i) (INT i. A' i)";
    6.23 -by (Blast_tac 1);
    6.24 -qed "all_constrains_INT";
    6.25 -
    6.26  Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'";
    6.27  by (Blast_tac 1);
    6.28  qed "constrains_imp_subset";
    6.29 @@ -116,16 +104,30 @@
    6.30  by (assume_tac 1);
    6.31  qed "stableD";
    6.32  
    6.33 +(** Union **)
    6.34 +
    6.35  Goalw [stable_def]
    6.36      "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
    6.37  by (blast_tac (claset() addIs [constrains_Un]) 1);
    6.38  qed "stable_Un";
    6.39  
    6.40  Goalw [stable_def]
    6.41 +    "ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)";
    6.42 +by (blast_tac (claset() addIs [ball_constrains_UN]) 1);
    6.43 +qed "ball_stable_UN";
    6.44 +
    6.45 +(** Intersection **)
    6.46 +
    6.47 +Goalw [stable_def]
    6.48      "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
    6.49  by (blast_tac (claset() addIs [constrains_Int]) 1);
    6.50  qed "stable_Int";
    6.51  
    6.52 +Goalw [stable_def]
    6.53 +    "ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)";
    6.54 +by (blast_tac (claset() addIs [ball_constrains_INT]) 1);
    6.55 +qed "ball_stable_INT";
    6.56 +
    6.57  Goalw [stable_def, constrains_def]
    6.58      "[| F : stable C; F : constrains A (C Un A') |]   \
    6.59  \    ==> F : constrains (C Un A) (C Un A')";
    6.60 @@ -150,7 +152,7 @@
    6.61  bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
    6.62  
    6.63  
    6.64 -(*** invariant & always ***)
    6.65 +(*** invariant ***)
    6.66  
    6.67  Goal "[| Init F<=A;  F: stable A |] ==> F : invariant A";
    6.68  by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
    6.69 @@ -176,17 +178,6 @@
    6.70  by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
    6.71  qed "invariant_includes_reachable";
    6.72  
    6.73 -Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
    6.74 -by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
    6.75 -                               stable_reachable,
    6.76 -			       impOfSubs invariant_includes_reachable]) 1);
    6.77 -qed "always_eq_UN_invariant";
    6.78 -
    6.79 -Goal "F : always A = (EX I. F: invariant I & I <= A)";
    6.80 -by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
    6.81 -by (Blast_tac 1);
    6.82 -qed "always_iff_ex_invariant";
    6.83 -
    6.84  
    6.85  (*** increasing ***)
    6.86  
    6.87 @@ -194,13 +185,13 @@
    6.88       "increasing f <= increasing (length o f)";
    6.89  by Auto_tac;
    6.90  by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
    6.91 -qed "increasing_length";
    6.92 +qed "increasing_size";
    6.93  
    6.94  Goalw [increasing_def]
    6.95       "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
    6.96  by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
    6.97  by (Blast_tac 1);
    6.98 -qed "increasing_less";
    6.99 +qed "increasing_stable_less";
   6.100  
   6.101  
   6.102  (** The Elimination Theorem.  The "free" m has become universally quantified!
     7.1 --- a/src/HOL/UNITY/UNITY.thy	Thu Nov 05 15:33:27 1998 +0100
     7.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Nov 06 13:20:29 1998 +0100
     7.3 @@ -24,15 +24,9 @@
     7.4    unless :: "['a set, 'a set] => 'a program set"
     7.5      "unless A B == constrains (A-B) (A Un B)"
     7.6  
     7.7 -  (*The traditional word for inductive properties.  Anyway, INDUCTIVE is
     7.8 -    reserved!*)
     7.9    invariant :: "'a set => 'a program set"
    7.10      "invariant A == {F. Init F <= A} Int stable A"
    7.11  
    7.12 -  (*Safety properties*)
    7.13 -  always :: "'a set => 'a program set"
    7.14 -    "always A == {F. reachable F <= A}"
    7.15 -
    7.16    (*Polymorphic in both states and the meaning of <= *)
    7.17    increasing :: "['a => 'b::{ord}] => 'a program set"
    7.18      "increasing f == INT z. stable {s. z <= f s}"
     8.1 --- a/src/HOL/UNITY/Union.ML	Thu Nov 05 15:33:27 1998 +0100
     8.2 +++ b/src/HOL/UNITY/Union.ML	Fri Nov 06 13:20:29 1998 +0100
     8.3 @@ -97,44 +97,6 @@
     8.4       simpset() addsimps [constrains_def, Join_def]));
     8.5  qed "constrains_Join";
     8.6  
     8.7 -
     8.8 -(**
     8.9 -Michel says...
    8.10 -
    8.11 -    p inductive-next q' in F
    8.12 -    p inductive-next q'' in G
    8.13 -    p noninductive-next q in FoG
    8.14 -    -------------------------------------------
    8.15 -    p noninductive-next q /\ (q' \/ q'') in FoG
    8.16 -
    8.17 -  From which you deduce:
    8.18 -
    8.19 -    inductive-stable A /\ B in F
    8.20 -    inductive-stable A      in G
    8.21 -    noninductive-stable B   in FoG
    8.22 -    ---------------------------------
    8.23 -    noninductive-stable A /\ B in FoG
    8.24 -**)
    8.25 -
    8.26 -Goal "[| F : constrains A B';  G : constrains A B'';  \
    8.27 -\        F Join G : Constrains A B |]                 \
    8.28 -\     ==> F Join G : Constrains A (B Int (B' Un B''))";
    8.29 -by (auto_tac
    8.30 -    (claset() addIs [constrains_Int RS constrains_weaken],
    8.31 -     simpset() addsimps [Constrains_def, constrains_Join]));
    8.32 -qed "constrains_imp_Join_Constrains";
    8.33 -
    8.34 -Goalw [Stable_def, stable_def]
    8.35 -     "[| F : stable (A Int B);  G : stable A;  \
    8.36 -\        F Join G : Stable B |]                 \
    8.37 -\     ==> F Join G : Stable (A Int B)";
    8.38 -by (auto_tac
    8.39 -    (claset() addIs [constrains_Int RS constrains_weaken],
    8.40 -     simpset() addsimps [Constrains_def, constrains_Join]));
    8.41 -qed "stable_imp_Join_Stable";
    8.42 -
    8.43 -
    8.44 -
    8.45  (**FAILS, I think; see 5.4.1, Substitution Axiom.
    8.46     The problem is to relate reachable (F Join G) with 
    8.47     reachable F and reachable G
    8.48 @@ -235,12 +197,82 @@
    8.49  qed "ensures_stable_Join2";
    8.50  
    8.51  
    8.52 -(** localTo **)
    8.53 +(** Diff and localTo **)
    8.54 +
    8.55 +Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G";
    8.56 +by (rtac program_equalityI 1);
    8.57 +by Auto_tac;
    8.58 +qed "Join_Diff2";
    8.59 +
    8.60 +Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
    8.61 +by Auto_tac;
    8.62 +qed "Diff_Disjoint";
    8.63  
    8.64 -Goal "[| F Join G : f localTo F;  (s,s') : act;  \
    8.65 -\        act : Acts G; act ~: Acts F |] ==> f s' = f s";
    8.66 +Goal "[| F Join G : v localTo F;  Disjoint F G |] \
    8.67 +\     ==> G : (INT z. stable {s. v s = z})";
    8.68  by (asm_full_simp_tac 
    8.69 -    (simpset() addsimps [localTo_def, Diff_def, Acts_Join, stable_def, 
    8.70 -			 constrains_def]) 1);
    8.71 +    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
    8.72 +			 Acts_Join, stable_def, constrains_def]) 1);
    8.73 +by (Blast_tac 1);
    8.74 +qed "localTo_imp_stable";
    8.75 +
    8.76 +Goal "[| F Join G : v localTo F;  (s,s') : act;  \
    8.77 +\        act : Acts G;  Disjoint F G |] ==> v s' = v s";
    8.78 +by (asm_full_simp_tac 
    8.79 +    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
    8.80 +			 Acts_Join, stable_def, constrains_def]) 1);
    8.81  by (Blast_tac 1);
    8.82  qed "localTo_imp_equals";
    8.83 +
    8.84 +Goalw [localTo_def, stable_def, constrains_def]
    8.85 +     "v localTo F <= (f o v) localTo F";
    8.86 +by (Clarify_tac 1);
    8.87 +by (auto_tac (claset() addSEs [allE, ballE], simpset()));
    8.88 +qed "localTo_imp_o_localTo";
    8.89 +
    8.90 +
    8.91 +(*** Higher-level rules involving localTo and Join ***)
    8.92 +
    8.93 +Goal "[| F : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)};   \
    8.94 +\        F Join G : v localTo F;       \
    8.95 +\        F Join G : w localTo F;       \
    8.96 +\        Disjoint F G |]               \
    8.97 +\     ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
    8.98 +by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
    8.99 +by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
   8.100 +by Auto_tac;
   8.101 +qed "constrains_localTo_constrains2";
   8.102 +
   8.103 +Goalw [stable_def]
   8.104 +     "[| F : stable {s. P (v s) (w s)};   \
   8.105 +\        F Join G : v localTo F;       \
   8.106 +\        F Join G : w localTo F;       \
   8.107 +\        Disjoint F G |]               \
   8.108 +\     ==> F Join G : stable {s. P (v s) (w s)}";
   8.109 +by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
   8.110 +qed "stable_localTo_stable2";
   8.111 +
   8.112 +
   8.113 +Goal "(UN k. {s. f s = k}) = UNIV";
   8.114 +by (Blast_tac 1);
   8.115 +qed "UN_eq_UNIV";
   8.116 +
   8.117 +Goal "[| F : stable {s. v s <= w s};   \
   8.118 +\        F Join G : v localTo F;       \
   8.119 +\        F Join G : Increasing w;      \
   8.120 +\        Disjoint F G |]               \
   8.121 +\     ==> F Join G : Stable {s. v s <= w s}";
   8.122 +by (safe_tac (claset() addSDs [localTo_imp_stable]));
   8.123 +by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
   8.124 +by (subgoal_tac "ALL k: UNIV. ?H : Constrains ({s. v s = k} Int ?AA) ?AA" 1);
   8.125 +by (dtac ball_Constrains_UN 1);
   8.126 +by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
   8.127 +by (rtac ballI 1);
   8.128 +by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
   8.129 +\                                      ({s. v s = k} Un {s. v s <= w s})" 1);
   8.130 +by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
   8.131 +by (blast_tac (claset() addIs [constrains_weaken]) 2);
   8.132 +by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
   8.133 +by (etac Constrains_weaken 2);
   8.134 +by Auto_tac;
   8.135 +qed "Increasing_localTo_Stable";
     9.1 --- a/src/HOL/UNITY/Union.thy	Thu Nov 05 15:33:27 1998 +0100
     9.2 +++ b/src/HOL/UNITY/Union.thy	Fri Nov 06 13:20:29 1998 +0100
     9.3 @@ -5,7 +5,7 @@
     9.4  
     9.5  Unions of programs
     9.6  
     9.7 -From Misra's Chapter 5: Asynchronous Compositions of Programs
     9.8 +Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
     9.9  *)
    9.10  
    9.11  Union = SubstAx + FP +
    9.12 @@ -23,9 +23,13 @@
    9.13    Diff :: "['a program, ('a * 'a)set set] => 'a program"
    9.14      "Diff F acts == mk_program (Init F, Acts F - acts)"
    9.15  
    9.16 -  (*The set of systems that regard "f" as local to F*)
    9.17 +  (*The set of systems that regard "v" as local to F*)
    9.18    localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
    9.19 -    "f localTo F == {G. ALL z. Diff G (Acts F) : stable {s. f s = z}}"
    9.20 +    "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
    9.21 +
    9.22 +  (*Two programs with disjoint actions, except for Id (idling)*)
    9.23 +  Disjoint :: ['a program, 'a program] => bool
    9.24 +    "Disjoint F G == Acts F Int Acts G <= {Id}"
    9.25  
    9.26  syntax
    9.27    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)