converting HOL/UNITY to use unconditional fairness
authorpaulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 1381291713a1915ee
parent 13811 f39f67982854
child 13813 722593f2f068
converting HOL/UNITY to use unconditional fairness
src/HOL/Relation.thy
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Comp/Client.ML
src/HOL/UNITY/Comp/Client.thy
src/HOL/UNITY/Comp/Counter.ML
src/HOL/UNITY/Comp/Counter.thy
src/HOL/UNITY/Comp/Counterc.ML
src/HOL/UNITY/Comp/Counterc.thy
src/HOL/UNITY/Comp/Handshake.thy
src/HOL/UNITY/Comp/Priority.ML
src/HOL/UNITY/Comp/Priority.thy
src/HOL/UNITY/Comp/TimerArray.thy
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/Detects.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/FP.thy
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/Project.thy
src/HOL/UNITY/Simple/Common.thy
src/HOL/UNITY/Simple/Lift.thy
src/HOL/UNITY/Simple/Mutex.thy
src/HOL/UNITY/Simple/NSP_Bad.ML
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/Relation.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -86,6 +86,9 @@
     1.4  
     1.5  subsection {* Diagonal: identity over a set *}
     1.6  
     1.7 +lemma diag_empty [simp]: "diag {} = {}"
     1.8 +  by (simp add: diag_def) 
     1.9 +
    1.10  lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
    1.11    by (simp add: diag_def)
    1.12  
    1.13 @@ -318,6 +321,9 @@
    1.14  lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B"
    1.15    by blast
    1.16  
    1.17 +lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
    1.18 +  by blast
    1.19 +
    1.20  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
    1.21    by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
    1.22  
     2.1 --- a/src/HOL/UNITY/Comp.thy	Sat Feb 08 14:46:22 2003 +0100
     2.2 +++ b/src/HOL/UNITY/Comp.thy	Sat Feb 08 16:05:33 2003 +0100
     2.3 @@ -185,7 +185,7 @@
     2.4       "[| F \<in> stable {s. P (v s) (w s)};    
     2.5           G \<in> preserves v;  G \<in> preserves w |]                
     2.6        ==> F Join G \<in> stable {s. P (v s) (w s)}"
     2.7 -apply (simp)
     2.8 +apply simp
     2.9  apply (subgoal_tac "G \<in> preserves (funPair v w) ")
    2.10   prefer 2 apply simp 
    2.11  apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
     3.1 --- a/src/HOL/UNITY/Comp/Client.ML	Sat Feb 08 14:46:22 2003 +0100
     3.2 +++ b/src/HOL/UNITY/Comp/Client.ML	Sat Feb 08 16:05:33 2003 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4  \     (G : preserves rel & G : preserves ask & G : preserves tok &\
     3.5  \      Client : Allowed G)";
     3.6  by (auto_tac (claset(), 
     3.7 -      simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));  
     3.8 +    simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed]));
     3.9  qed "Client_ok_iff";
    3.10  AddIffs [Client_ok_iff];
    3.11  
    3.12 @@ -79,7 +79,8 @@
    3.13  qed "Join_Always_rel_le_giv";
    3.14  
    3.15  Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
    3.16 -by (res_inst_tac [("act", "rel_act")] transientI 1);
    3.17 +by (simp_tac (simpset() addsimps [Client_def, mk_total_program_def]) 1);
    3.18 +by (res_inst_tac [("act", "rel_act")] totalize_transientI 1);
    3.19  by (auto_tac (claset(),
    3.20  	      simpset() addsimps [Domain_def, Client_def]));
    3.21  by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
     4.1 --- a/src/HOL/UNITY/Comp/Client.thy	Sat Feb 08 14:46:22 2003 +0100
     4.2 +++ b/src/HOL/UNITY/Comp/Client.thy	Sat Feb 08 16:05:33 2003 +0100
     4.3 @@ -30,10 +30,10 @@
     4.4    
     4.5    rel_act :: "('a state_d * 'a state_d) set"
     4.6      "rel_act == {(s,s').
     4.7 -		  EX nrel. nrel = size (rel s) &
     4.8 -		           s' = s (| rel := rel s @ [giv s!nrel] |) &
     4.9 -		           nrel < size (giv s) &
    4.10 -		           ask s!nrel <= giv s!nrel}"
    4.11 +		  \\<exists>nrel. nrel = size (rel s) &
    4.12 +		         s' = s (| rel := rel s @ [giv s!nrel] |) &
    4.13 +		         nrel < size (giv s) &
    4.14 +		         ask s!nrel <= giv s!nrel}"
    4.15  
    4.16    (** Choose a new token requirement **)
    4.17  
    4.18 @@ -49,10 +49,11 @@
    4.19  
    4.20    Client :: 'a state_d program
    4.21      "Client ==
    4.22 -       mk_program ({s. tok s : atMost NbT &
    4.23 -		    giv s = [] & ask s = [] & rel s = []},
    4.24 -		   {rel_act, tok_act, ask_act},
    4.25 -		   UN G: preserves rel Int preserves ask Int preserves tok.
    4.26 +       mk_total_program
    4.27 +            ({s. tok s : atMost NbT &
    4.28 +		 giv s = [] & ask s = [] & rel s = []},
    4.29 +	     {rel_act, tok_act, ask_act},
    4.30 +	     \\<Union>G \\<in> preserves rel Int preserves ask Int preserves tok.
    4.31  		   Acts G)"
    4.32  
    4.33    (*Maybe want a special theory section to declare such maps*)
     5.1 --- a/src/HOL/UNITY/Comp/Counter.ML	Sat Feb 08 14:46:22 2003 +0100
     5.2 +++ b/src/HOL/UNITY/Comp/Counter.ML	Sat Feb 08 16:05:33 2003 +0100
     5.3 @@ -11,11 +11,10 @@
     5.4     Spriner LNCS 1586 (1999), pages 1215-1227.
     5.5  *)
     5.6  
     5.7 -Addsimps [Component_def RS def_prg_Init];
     5.8 -Addsimps (map simp_of_act  [a_def]);
     5.9 +Addsimps [Component_def RS def_prg_Init, simp_of_act a_def];
    5.10  
    5.11  (* Theorems about sum and sumj *)
    5.12 -Goal "ALL n. I<n --> sum I (s(c n := x)) = sum I s";
    5.13 +Goal "\\<forall>n. I<n --> sum I (s(c n := x)) = sum I s";
    5.14  by (induct_tac "I" 1);
    5.15  by Auto_tac;
    5.16  qed_spec_mp "sum_upd_gt";
    5.17 @@ -47,7 +46,7 @@
    5.18      addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
    5.19  qed "sumj_upd_C";
    5.20  
    5.21 -Goal "ALL i. I<i--> (sumj I i s = sum I s)";
    5.22 +Goal "\\<forall>i. I<i--> (sumj I i s = sum I s)";
    5.23  by (induct_tac "I" 1);
    5.24  by Auto_tac;
    5.25  qed_spec_mp  "sumj_sum_gt";
    5.26 @@ -58,49 +57,49 @@
    5.27  by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
    5.28  qed "sumj_sum_eq";
    5.29  
    5.30 -Goal "ALL i. i<I-->(sum I s = s (c i) +  sumj I i s)";
    5.31 +Goal "\\<forall>i. i<I-->(sum I s = s (c i) +  sumj I i s)";
    5.32  by (induct_tac "I" 1);
    5.33  by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq]));  
    5.34  qed_spec_mp "sum_sumj";
    5.35  
    5.36  (* Correctness proofs for Components *)
    5.37  (* p2 and p3 proofs *)
    5.38 -Goal "Component i : stable {s. s C = s (c i) + k}";
    5.39 +Goal "Component i \\<in> stable {s. s C = s (c i) + k}";
    5.40  by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    5.41  by (constrains_tac 1);
    5.42  qed "p2";
    5.43  
    5.44 -Goal "Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
    5.45 +Goal "Component i \\<in> stable {s. \\<forall>v. v~=c i & v~=C --> s v = k v}";
    5.46  by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    5.47  by (constrains_tac 1);
    5.48  qed "p3";
    5.49  
    5.50  
    5.51  Goal 
    5.52 -"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \
    5.53 -\                  Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \
    5.54 -\  = (Component i: stable {s. s C = s (c i) + sumj I i s})";
    5.55 +"(\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} \
    5.56 +\                  \\<inter> {s. \\<forall>v. v~=c i & v~=C --> s v = k v})) \
    5.57 +\  = (Component i \\<in> stable {s. s C = s (c i) + sumj I i s})";
    5.58 +by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1);
    5.59  by (auto_tac (claset(), simpset() 
    5.60 -     addsimps [constrains_def, stable_def,Component_def,
    5.61 -               sumj_upd_C, sumj_upd_ci]));
    5.62 +     addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci]));
    5.63  qed "p2_p3_lemma1";
    5.64  
    5.65  Goal 
    5.66 -"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \
    5.67 -\                             {s. ALL v. v~=c i & v~=C --> s v = k v})";
    5.68 +"\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} Int \
    5.69 +\                             {s. \\<forall>v. v~=c i & v~=C --> s v = k v})";
    5.70  by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
    5.71  qed "p2_p3_lemma2";
    5.72  
    5.73  
    5.74  Goal 
    5.75 -"Component i: stable {s.  s C = s (c i) + sumj I i s}";
    5.76 +"Component i \\<in> stable {s.  s C = s (c i) + sumj I i s}";
    5.77  by (auto_tac (claset() addSIs [p2_p3_lemma2],
    5.78                simpset() addsimps [p2_p3_lemma1 RS sym]));
    5.79  qed "p2_p3";
    5.80  
    5.81  (* Compositional Proof *)
    5.82  
    5.83 -Goal "(ALL i. i < I --> s (c i) = 0) --> sum I s = 0";
    5.84 +Goal "(\\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0";
    5.85  by (induct_tac "I" 1);
    5.86  by Auto_tac;
    5.87  qed "sum_0'";
    5.88 @@ -108,33 +107,7 @@
    5.89  
    5.90  (* I could'nt be empty *)
    5.91  Goalw [invariant_def] 
    5.92 -"!!I. 0<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
    5.93 -by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
    5.94 +"!!I. 0<I ==> (\\<Squnion>i \\<in> {i. i<I}. Component i) \\<in> invariant {s. s C = sum I s}";
    5.95 +by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1);
    5.96  by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
    5.97  qed "safety";
    5.98 -
    5.99 -
   5.100 -
   5.101 -
   5.102 -
   5.103 -
   5.104 -
   5.105 -
   5.106 -
   5.107 -
   5.108 -
   5.109 -
   5.110 -
   5.111 -
   5.112 -
   5.113 -
   5.114 -
   5.115 -
   5.116 -
   5.117 -
   5.118 -
   5.119 - 
   5.120 -
   5.121 -
   5.122 -
   5.123 -
     6.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Sat Feb 08 14:46:22 2003 +0100
     6.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Sat Feb 08 16:05:33 2003 +0100
     6.3 @@ -37,6 +37,7 @@
     6.4  
     6.5    Component :: "nat => state program"
     6.6    "Component i ==
     6.7 -    mk_program({s. s C = 0 & s (c i) = 0}, {a i},
     6.8 -	       UN G: preserves (%s. s (c i)). Acts G)"
     6.9 +    mk_total_program({s. s C = 0 & s (c i) = 0}, {a i},
    6.10 +	             \\<Union>G \\<in> preserves (%s. s (c i)). Acts G)"
    6.11 +
    6.12  end  
     7.1 --- a/src/HOL/UNITY/Comp/Counterc.ML	Sat Feb 08 14:46:22 2003 +0100
     7.2 +++ b/src/HOL/UNITY/Comp/Counterc.ML	Sat Feb 08 16:05:33 2003 +0100
     7.3 @@ -12,11 +12,11 @@
     7.4  *)
     7.5  
     7.6  Addsimps [Component_def RS def_prg_Init, 
     7.7 -Component_def RS def_prg_AllowedActs];
     7.8 -Addsimps (map simp_of_act  [a_def]);
     7.9 +          Component_def RS def_prg_AllowedActs,
    7.10 +          simp_of_act a_def];
    7.11  
    7.12  (* Theorems about sum and sumj *)
    7.13 -Goal "ALL i. I<i--> (sum I s = sumj I i s)";
    7.14 +Goal "\\<forall>i. I<i--> (sum I s = sumj I i s)";
    7.15  by (induct_tac "I" 1);
    7.16  by Auto_tac;
    7.17  qed_spec_mp  "sum_sumj_eq1";
    7.18 @@ -26,18 +26,18 @@
    7.19  by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1]));
    7.20  qed_spec_mp "sum_sumj_eq2";
    7.21  
    7.22 -Goal "(ALL i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
    7.23 +Goal "(\\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
    7.24  by (induct_tac "I" 1 THEN Auto_tac);
    7.25  qed_spec_mp "sum_ext";
    7.26  
    7.27 -Goal "(ALL j. j<I & j~=i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)";
    7.28 +Goal "(\\<forall>j. j<I & j~=i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)";
    7.29  by (induct_tac "I" 1);
    7.30  by Safe_tac;
    7.31  by (auto_tac (claset() addSIs [sum_ext], simpset()));
    7.32  qed_spec_mp "sumj_ext";
    7.33  
    7.34  
    7.35 -Goal "(ALL i. i<I --> c s i = 0) -->  sum I s = 0";
    7.36 +Goal "(\\<forall>i. i<I --> c s i = 0) -->  sum I s = 0";
    7.37  by (induct_tac "I" 1);
    7.38  by Auto_tac;
    7.39  qed "sum0";
    7.40 @@ -46,22 +46,24 @@
    7.41  (* Safety properties for Components *)
    7.42  
    7.43  Goal "(Component i ok G) = \
    7.44 -\     (G: preserves (%s. c s i) & Component i:Allowed G)";
    7.45 +\     (G \\<in> preserves (%s. c s i) & Component i \\<in> Allowed G)";
    7.46  by (auto_tac (claset(), 
    7.47 -      simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed]));
    7.48 +      simpset() addsimps [ok_iff_Allowed, Component_def RS def_total_prg_Allowed]));
    7.49  qed "Component_ok_iff";
    7.50  AddIffs [Component_ok_iff];
    7.51  AddIffs [OK_iff_ok];
    7.52  Addsimps [preserves_def];
    7.53  
    7.54  
    7.55 -Goal "Component i: stable {s. C s = (c s) i + k}";
    7.56 +Goal "Component i \\<in> stable {s. C s = (c s) i + k}";
    7.57  by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
    7.58  by (constrains_tac 1);
    7.59  qed "p2";
    7.60  
    7.61 -Goal "[| OK I Component; i:I |]  \
    7.62 -\      ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}";
    7.63 +Goal "[| OK I Component; i\\<in>I |]  \
    7.64 +\     ==> Component i \\<in> stable {s. \\<forall>j\\<in>I. j~=i --> c s j = c k j}";
    7.65 +by (asm_full_simp_tac (simpset() addsimps []) 1); 
    7.66 +by (rewrite_goals_tac [Component_def, mk_total_program_def]);
    7.67  by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1);
    7.68  by (Blast_tac 1);
    7.69  qed "p3";
    7.70 @@ -69,22 +71,22 @@
    7.71  
    7.72  Goal 
    7.73  "[| OK {i. i<I} Component; i<I |] ==> \
    7.74 -\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \
    7.75 -\                             {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})";
    7.76 +\ \\<forall>k. Component i \\<in> stable ({s. C s = c s i + sumj I i k} Int \
    7.77 +\                             {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j})";
    7.78  by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
    7.79  qed "p2_p3_lemma1";
    7.80  
    7.81  
    7.82 -Goal "(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \
    7.83 -\                       {s. ALL j:{i. i<I}. j~=i --> c s j = c k j}))  \
    7.84 -\     ==> (F:stable {s. C s = c s i + sumj I i s})";
    7.85 +Goal "(\\<forall>k. F\\<in>stable ({s. C s = (c s) i + sumj I i k} Int \
    7.86 +\                       {s. \\<forall>j\\<in>{i. i<I}. j~=i --> c s j = c k j}))  \
    7.87 +\     ==> (F\\<in>stable {s. C s = c s i + sumj I i s})";
    7.88  by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1);
    7.89  by (force_tac (claset() addSIs [sumj_ext], simpset()) 1);
    7.90  qed "p2_p3_lemma2";
    7.91  
    7.92  
    7.93  Goal "[| OK {i. i<I} Component; i<I |] \
    7.94 -\     ==> Component i: stable {s. C s = c s i + sumj I i s}";
    7.95 +\     ==> Component i \\<in> stable {s. C s = c s i + sumj I i s}";
    7.96  by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1);
    7.97  qed "p2_p3";
    7.98  
    7.99 @@ -92,7 +94,7 @@
   7.100  (* Compositional correctness *)
   7.101  Goalw [invariant_def]
   7.102       "[| 0<I; OK {i. i<I} Component |]  \
   7.103 -\     ==> (JN i:{i. i<I}. (Component i)) : invariant {s. C s = sum I s}";
   7.104 +\     ==> (\\<Squnion>i\\<in>{i. i<I}. (Component i)) \\<in> invariant {s. C s = sum I s}";
   7.105  by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
   7.106  by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3], 
   7.107                simpset()));
     8.1 --- a/src/HOL/UNITY/Comp/Counterc.thy	Sat Feb 08 14:46:22 2003 +0100
     8.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy	Sat Feb 08 16:05:33 2003 +0100
     8.3 @@ -39,6 +39,7 @@
     8.4   "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
     8.5   
     8.6    Component :: "nat => state program"
     8.7 -  "Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i},
     8.8 -	       UN G: preserves (%s. (c s) i). Acts G)"
     8.9 +  "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
    8.10 +				   {a i},
    8.11 + 	                           \\<Union>G \\<in> preserves (%s. (c s) i). Acts G)"
    8.12  end  
     9.1 --- a/src/HOL/UNITY/Comp/Handshake.thy	Sat Feb 08 14:46:22 2003 +0100
     9.2 +++ b/src/HOL/UNITY/Comp/Handshake.thy	Sat Feb 08 16:05:33 2003 +0100
     9.3 @@ -21,14 +21,14 @@
     9.4      "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
     9.5  
     9.6    F :: "state program"
     9.7 -    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
     9.8 +    "F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
     9.9  
    9.10    (*G's program*)
    9.11    cmdG :: "(state*state) set"
    9.12      "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
    9.13  
    9.14    G :: "state program"
    9.15 -    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
    9.16 +    "G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
    9.17  
    9.18    (*the joint invariant*)
    9.19    invFG :: "state set"
    10.1 --- a/src/HOL/UNITY/Comp/Priority.ML	Sat Feb 08 14:46:22 2003 +0100
    10.2 +++ b/src/HOL/UNITY/Comp/Priority.ML	Sat Feb 08 16:05:33 2003 +0100
    10.3 @@ -77,7 +77,7 @@
    10.4  
    10.5  (* property 13: universal *)
    10.6  Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
    10.7 -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); 
    10.8 +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
    10.9  by (constrains_tac 1);
   10.10  by (Blast_tac 1);
   10.11  qed "p13";
   10.12 @@ -88,16 +88,15 @@
   10.13  "ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
   10.14  by (Clarify_tac 1);
   10.15  by (cut_inst_tac [("i", "j")] reach_lemma 1);
   10.16 -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); 
   10.17 +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
   10.18  by (constrains_tac 1);
   10.19  by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
   10.20  qed "above_not_increase";  
   10.21  
   10.22 -Goal 
   10.23 -"system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
   10.24 +Goal "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
   10.25  by (cut_inst_tac [("i", "i")] above_not_increase 1);
   10.26 -by (asm_full_simp_tac (simpset() addsimps 
   10.27 -                 [trancl_converse, constrains_def]) 1); 
   10.28 +by (asm_full_simp_tac
   10.29 +    (simpset() addsimps [trancl_converse, constrains_def]) 1); 
   10.30  by (Blast_tac 1);
   10.31  qed "above_not_increase'";  
   10.32  
   10.33 @@ -106,7 +105,7 @@
   10.34  (* p15: universal property: all Components well behave  *)
   10.35  Goal "ALL i. system: Highest i co Highest i Un Lowest i";
   10.36  by (Clarify_tac 1);
   10.37 -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); 
   10.38 +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
   10.39  by (constrains_tac 1);
   10.40  by Auto_tac;
   10.41  qed "system_well_behaves";  
   10.42 @@ -147,9 +146,9 @@
   10.43  (* propert 5: existential property *)
   10.44  
   10.45  Goal "system: Highest i leadsTo Lowest i";
   10.46 -by (asm_full_simp_tac (simpset() addsimps [system_def]) 1); 
   10.47 +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
   10.48  by (ensures_tac "act i" 1);
   10.49 -by (auto_tac (claset(), simpset() addsimps [Component_def]));
   10.50 +by Auto_tac;
   10.51  qed "Highest_leadsTo_Lowest";
   10.52  
   10.53  (* a lowest i can never be in any abover set *) 
    11.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Sat Feb 08 14:46:22 2003 +0100
    11.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Sat Feb 08 16:05:33 2003 +0100
    11.3 @@ -35,7 +35,7 @@
    11.4  
    11.5    (* All components start with the same initial state *)
    11.6    Component :: "vertex=>state program"
    11.7 -  "Component i == mk_program({init}, {act i}, UNIV)"
    11.8 +  "Component i == mk_total_program({init}, {act i}, UNIV)"
    11.9  
   11.10    (* Abbreviations *)
   11.11    Highest :: "vertex=>state set"
    12.1 --- a/src/HOL/UNITY/Comp/TimerArray.thy	Sat Feb 08 14:46:22 2003 +0100
    12.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sat Feb 08 16:05:33 2003 +0100
    12.3 @@ -18,7 +18,7 @@
    12.4      "decr == UN n uu. {((Suc n, uu), (n,uu))}"
    12.5    
    12.6    Timer :: "'a state program"
    12.7 -    "Timer == mk_program (UNIV, {decr}, UNIV)"
    12.8 +    "Timer == mk_total_program (UNIV, {decr}, UNIV)"
    12.9  
   12.10  
   12.11  declare Timer_def [THEN def_prg_Init, simp]
   12.12 @@ -61,8 +61,8 @@
   12.13  apply (rename_tac "n")
   12.14  apply (rule PLam_leadsTo_Basis)
   12.15  apply (auto simp add: lessThan_Suc [symmetric])
   12.16 -apply (unfold Timer_def, constrains) 
   12.17 -apply (rule_tac act = decr in transientI, auto)
   12.18 +apply (unfold Timer_def mk_total_program_def, constrains) 
   12.19 +apply (rule_tac act = decr in totalize_transientI, auto)
   12.20  done
   12.21  
   12.22  end
    13.1 --- a/src/HOL/UNITY/Constrains.thy	Sat Feb 08 14:46:22 2003 +0100
    13.2 +++ b/src/HOL/UNITY/Constrains.thy	Sat Feb 08 16:05:33 2003 +0100
    13.3 @@ -55,7 +55,7 @@
    13.4  subsection{*traces and reachable*}
    13.5  
    13.6  lemma reachable_equiv_traces:
    13.7 -     "reachable F = {s. \<exists>evs. (s,evs): traces (Init F) (Acts F)}"
    13.8 +     "reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}"
    13.9  apply safe
   13.10  apply (erule_tac [2] traces.induct)
   13.11  apply (erule reachable.induct)
   13.12 @@ -392,4 +392,35 @@
   13.13    used by Always_Int_I) *)
   13.14  lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
   13.15  
   13.16 +
   13.17 +subsection{*Totalize*}
   13.18 +
   13.19 +lemma reachable_imp_reachable_tot:
   13.20 +      "s \<in> reachable F ==> s \<in> reachable (totalize F)"
   13.21 +apply (erule reachable.induct)
   13.22 + apply (rule reachable.Init) 
   13.23 + apply simp 
   13.24 +apply (rule_tac act = "totalize_act act" in reachable.Acts) 
   13.25 +apply (auto simp add: totalize_act_def) 
   13.26 +done
   13.27 +
   13.28 +lemma reachable_tot_imp_reachable:
   13.29 +      "s \<in> reachable (totalize F) ==> s \<in> reachable F"
   13.30 +apply (erule reachable.induct)
   13.31 + apply (rule reachable.Init, simp) 
   13.32 +apply (force simp add: totalize_act_def intro: reachable.Acts) 
   13.33 +done
   13.34 +
   13.35 +lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F"
   13.36 +by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable) 
   13.37 +
   13.38 +lemma totalize_Constrains_iff [simp]: "(totalize F \<in> A Co B) = (F \<in> A Co B)"
   13.39 +by (simp add: Constrains_def) 
   13.40 +
   13.41 +lemma totalize_Stable_iff [simp]: "(totalize F \<in> Stable A) = (F \<in> Stable A)"
   13.42 +by (simp add: Stable_def)
   13.43 +
   13.44 +lemma totalize_Always_iff [simp]: "(totalize F \<in> Always A) = (F \<in> Always A)"
   13.45 +by (simp add: Always_def)
   13.46 +
   13.47  end
    14.1 --- a/src/HOL/UNITY/Detects.thy	Sat Feb 08 14:46:22 2003 +0100
    14.2 +++ b/src/HOL/UNITY/Detects.thy	Sat Feb 08 16:05:33 2003 +0100
    14.3 @@ -21,7 +21,8 @@
    14.4  
    14.5  (* Corollary from Sectiom 3.6.4 *)
    14.6  
    14.7 -lemma Always_at_FP: "F \<in> A LeadsTo B ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
    14.8 +lemma Always_at_FP:
    14.9 +     "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
   14.10  apply (rule LeadsTo_empty)
   14.11  apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
   14.12  apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
   14.13 @@ -36,8 +37,7 @@
   14.14  apply (unfold Detects_def Int_def)
   14.15  apply (simp (no_asm))
   14.16  apply safe
   14.17 -apply (rule_tac [2] LeadsTo_Trans)
   14.18 -apply auto
   14.19 +apply (rule_tac [2] LeadsTo_Trans, auto)
   14.20  apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
   14.21   apply (blast intro: Always_weaken)
   14.22  apply (simp add: Always_Int_distrib)
   14.23 @@ -49,9 +49,7 @@
   14.24  done
   14.25  
   14.26  lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
   14.27 -apply (unfold Equality_def)
   14.28 -apply blast
   14.29 -done
   14.30 +by (unfold Equality_def, blast)
   14.31  
   14.32  (*Not quite antisymmetry: sets A and B agree in all reachable states *)
   14.33  lemma Detects_antisym: 
   14.34 @@ -64,9 +62,9 @@
   14.35  (* Theorem from Section 3.8 *)
   14.36  
   14.37  lemma Detects_Always: 
   14.38 -     "F \<in> A Detects B ==> F \<in> Always ((-(FP F)) \<union> (A <==> B))"
   14.39 +     "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
   14.40  apply (unfold Detects_def Equality_def)
   14.41 -apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
   14.42 +apply (simp add: Un_Int_distrib Always_Int_distrib)
   14.43  apply (blast dest: Always_at_FP intro: Always_weaken)
   14.44  done
   14.45  
   14.46 @@ -75,7 +73,7 @@
   14.47  lemma Detects_Imp_LeadstoEQ: 
   14.48       "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
   14.49  apply (unfold Detects_def Equality_def)
   14.50 -apply (rule_tac B = "B" in LeadsTo_Diff)
   14.51 +apply (rule_tac B = B in LeadsTo_Diff)
   14.52   apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
   14.53  apply (blast intro: Always_LeadsTo_weaken)
   14.54  done
    15.1 --- a/src/HOL/UNITY/ELT.thy	Sat Feb 08 14:46:22 2003 +0100
    15.2 +++ b/src/HOL/UNITY/ELT.thy	Sat Feb 08 16:05:33 2003 +0100
    15.3 @@ -281,22 +281,11 @@
    15.4       "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |]  
    15.5      ==> F : A leadsTo[CC] (B' Un A')"
    15.6  apply (rule leadsETo_cancel1)
    15.7 -prefer 2 apply assumption
    15.8 -apply (simp_all (no_asm_simp))
    15.9 + prefer 2 apply assumption
   15.10 +apply simp_all
   15.11  done
   15.12  
   15.13  
   15.14 -(** The impossibility law **)
   15.15 -
   15.16 -lemma leadsETo_empty_lemma: "F : A leadsTo[CC] B ==> B={} --> A={}"
   15.17 -apply (erule leadsETo_induct)
   15.18 -apply (simp_all (no_asm_simp))
   15.19 -apply (unfold ensures_def constrains_def transient_def, blast)
   15.20 -done
   15.21 -
   15.22 -lemma leadsETo_empty: "F : A leadsTo[CC] {} ==> A={}"
   15.23 -by (blast intro!: leadsETo_empty_lemma [THEN mp])
   15.24 -
   15.25  
   15.26  (** PSP: Progress-Safety-Progress **)
   15.27  
   15.28 @@ -367,23 +356,6 @@
   15.29  apply (blast intro: constrains_Int [THEN constrains_weaken])+
   15.30  done
   15.31  
   15.32 -(*useful??*)
   15.33 -lemma Join_leadsETo_stable_imp_leadsETo:
   15.34 -     "[| F Join G : (A leadsTo[CC] B);  ALL C:CC. G : stable C |]  
   15.35 -      ==> F: (A leadsTo[CC] B)"
   15.36 -apply (erule leadsETo_induct)
   15.37 -prefer 3 apply (blast intro: leadsETo_Union)
   15.38 -prefer 2 apply (blast intro: leadsETo_Trans)
   15.39 -apply (rule leadsETo_Basis)
   15.40 -apply (case_tac "A <= B")
   15.41 -apply (erule subset_imp_ensures)
   15.42 -apply (auto intro: constrains_weaken simp add: stable_def ensures_def Join_transient)
   15.43 -apply (erule_tac V = "?F : ?A co ?B" in thin_rl)+
   15.44 -apply (erule transientE)
   15.45 -apply (unfold constrains_def)
   15.46 -apply (blast dest!: bspec)
   15.47 -done
   15.48 -
   15.49  (**** Relationship with traditional "leadsTo", strong & weak ****)
   15.50  
   15.51  (** strong **)
   15.52 @@ -538,18 +510,6 @@
   15.53  done
   15.54  
   15.55  
   15.56 -
   15.57 -(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
   15.58 -lemma (in Extend) 
   15.59 -     "[| G : preserves (v o f);  project h C G : transient D;   
   15.60 -         D : givenBy v |] ==> D={}"
   15.61 -apply (rule stable_transient_empty)
   15.62 - prefer 2 apply assumption
   15.63 -(*If addIs then PROOF FAILED at depth 2*)
   15.64 -apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)
   15.65 -done
   15.66 -
   15.67 -
   15.68  (*This version's stronger in the "ensures" precondition
   15.69    BUT there's no ensures_weaken_L*)
   15.70  lemma (in Extend) Join_project_ensures_strong:
   15.71 @@ -563,20 +523,7 @@
   15.72  apply (auto simp add: Int_Diff)
   15.73  done
   15.74  
   15.75 -(*Generalizes preserves_project_transient_empty*)
   15.76 -lemma (in Extend) preserves_o_project_transient_empty:
   15.77 -     "[| G : preserves (v o f);   
   15.78 -         project h C G : transient (C' Int D);   
   15.79 -         project h C G : stable C';  D : givenBy v |]     
   15.80 -      ==> C' Int D = {}"
   15.81 -apply (rule stable_transient_empty)
   15.82 -prefer 2 apply assumption
   15.83 -(*Fragile proof.  Was just a single blast call.
   15.84 -  If just "intro" then PROOF FAILED at depth 3*)
   15.85 -apply (rule stable_Int) 
   15.86 - apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)+
   15.87 -done
   15.88 -
   15.89 +(*NOT WORKING.  MODIFY AS IN Project.thy
   15.90  lemma (in Extend) pld_lemma:
   15.91       "[| extend h F Join G : stable C;   
   15.92           F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
   15.93 @@ -596,7 +543,7 @@
   15.94   prefer 2
   15.95   apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric])
   15.96  apply (rule Join_project_ensures_strong)
   15.97 -apply (auto dest: preserves_o_project_transient_empty intro: project_stable_project_set simp add: Int_left_absorb)
   15.98 +apply (auto intro: project_stable_project_set simp add: Int_left_absorb)
   15.99  apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
  15.100  done
  15.101  
  15.102 @@ -652,6 +599,7 @@
  15.103  apply (unfold extending_def)
  15.104  apply (blast intro: project_LeadsETo_D)
  15.105  done
  15.106 +*)
  15.107  
  15.108  
  15.109  (*** leadsETo in the precondition ***)
    16.1 --- a/src/HOL/UNITY/Extend.thy	Sat Feb 08 14:46:22 2003 +0100
    16.2 +++ b/src/HOL/UNITY/Extend.thy	Sat Feb 08 16:05:33 2003 +0100
    16.3 @@ -101,9 +101,6 @@
    16.4  lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> B)"
    16.5  by blast
    16.6  
    16.7 -lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
    16.8 -by (blast intro: sym [THEN image_eqI])
    16.9 -
   16.10  (*Possibly easier than reasoning about "inv h"*)
   16.11  lemma good_mapI: 
   16.12       assumes surj_h: "surj h"
   16.13 @@ -338,9 +335,9 @@
   16.14  
   16.15  
   16.16  
   16.17 -subsection{*extend ****)
   16.18 +subsection{*extend*}
   16.19  
   16.20 -(*** Basic properties*}
   16.21 +text{*Basic properties*}
   16.22  
   16.23  lemma Init_extend [simp]:
   16.24       "Init (extend h F) = extend_set h (Init F)"
   16.25 @@ -453,6 +450,8 @@
   16.26  lemma (in Extend) project_mono: "F \<le> G ==> project h C F \<le> project h C G"
   16.27  by (simp add: component_eq_subset, blast)
   16.28  
   16.29 +lemma (in Extend) all_total_extend: "all_total F ==> all_total (extend h F)"
   16.30 +by (simp add: all_total_def Domain_extend_act)
   16.31  
   16.32  subsection{*Safety: co, stable*}
   16.33  
   16.34 @@ -611,10 +610,7 @@
   16.35  
   16.36  lemma (in Extend) extend_transient_slice:
   16.37       "extend h F \<in> transient A ==> F \<in> transient (slice A y)"
   16.38 -apply (unfold transient_def, auto)
   16.39 -apply (rule bexI, auto)
   16.40 -apply (force simp add: extend_act_def)
   16.41 -done
   16.42 +by (unfold transient_def, auto)
   16.43  
   16.44  (*Converse?*)
   16.45  lemma (in Extend) extend_constrains_slice:
    17.1 --- a/src/HOL/UNITY/FP.thy	Sat Feb 08 14:46:22 2003 +0100
    17.2 +++ b/src/HOL/UNITY/FP.thy	Sat Feb 08 16:05:33 2003 +0100
    17.3 @@ -56,4 +56,7 @@
    17.4  lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
    17.5  by (simp add: Diff_eq Compl_FP)
    17.6  
    17.7 +lemma totalize_FP [simp]: "FP (totalize F) = FP F"
    17.8 +by (simp add: FP_def)
    17.9 +
   17.10  end
    18.1 --- a/src/HOL/UNITY/Follows.thy	Sat Feb 08 14:46:22 2003 +0100
    18.2 +++ b/src/HOL/UNITY/Follows.thy	Sat Feb 08 16:05:33 2003 +0100
    18.3 @@ -62,16 +62,13 @@
    18.4  subsection{*Destruction rules*}
    18.5  
    18.6  lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
    18.7 -apply (unfold Follows_def, blast)
    18.8 -done
    18.9 +by (unfold Follows_def, blast)
   18.10  
   18.11  lemma Follows_Increasing2: "F \<in> f Fols g ==> F \<in> Increasing g"
   18.12 -apply (unfold Follows_def, blast)
   18.13 -done
   18.14 +by (unfold Follows_def, blast)
   18.15  
   18.16  lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<subseteq> g s}"
   18.17 -apply (unfold Follows_def, blast)
   18.18 -done
   18.19 +by (unfold Follows_def, blast)
   18.20  
   18.21  lemma Follows_LeadsTo: 
   18.22       "F \<in> f Fols g ==> F \<in> {s. k \<le> g s} LeadsTo {s. k \<le> f s}"
   18.23 @@ -159,8 +156,7 @@
   18.24  apply (rule LeadsTo_weaken)
   18.25  apply (rule PSP_Stable)
   18.26  apply (erule_tac x = "f s" in spec)
   18.27 -apply (erule Stable_Int, assumption)
   18.28 -apply blast+
   18.29 +apply (erule Stable_Int, assumption, blast+)
   18.30  done
   18.31  
   18.32  lemma Follows_Un: 
   18.33 @@ -218,8 +214,7 @@
   18.34  apply (rule LeadsTo_weaken)
   18.35  apply (rule PSP_Stable)
   18.36  apply (erule_tac x = "f s" in spec)
   18.37 -apply (erule Stable_Int, assumption)
   18.38 -apply blast
   18.39 +apply (erule Stable_Int, assumption, blast)
   18.40  apply (blast intro: union_le_mono order_trans)
   18.41  done
   18.42  
    19.1 --- a/src/HOL/UNITY/Guar.thy	Sat Feb 08 14:46:22 2003 +0100
    19.2 +++ b/src/HOL/UNITY/Guar.thy	Sat Feb 08 16:05:33 2003 +0100
    19.3 @@ -109,8 +109,7 @@
    19.4  lemma ex_prop_equiv: 
    19.5       "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
    19.6  apply auto
    19.7 -apply (unfold ex_prop_def component_of_def, safe)
    19.8 -apply blast 
    19.9 +apply (unfold ex_prop_def component_of_def, safe, blast) 
   19.10  apply blast 
   19.11  apply (subst Join_commute) 
   19.12  apply (drule ok_sym, blast) 
    20.1 --- a/src/HOL/UNITY/Lift_prog.thy	Sat Feb 08 14:46:22 2003 +0100
    20.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Sat Feb 08 16:05:33 2003 +0100
    20.3 @@ -47,7 +47,7 @@
    20.4  apply (auto split add: nat_diff_split)
    20.5  done
    20.6  
    20.7 -(*** Injectiveness proof ***)
    20.8 +subsection{*Injectiveness proof*}
    20.9  
   20.10  lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
   20.11  by (drule_tac x = i in fun_cong, simp)
   20.12 @@ -80,7 +80,7 @@
   20.13  apply (rule inj_onI, auto)
   20.14  done
   20.15  
   20.16 -(*** Surjectiveness proof ***)
   20.17 +subsection{*Surjectiveness proof*}
   20.18  
   20.19  lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
   20.20  apply (unfold lift_map_def drop_map_def)
   20.21 @@ -111,7 +111,11 @@
   20.22  lemma sub_apply [simp]: "sub i f = f i"
   20.23  by (simp add: sub_def)
   20.24  
   20.25 -(*** lift_set ***)
   20.26 +lemma all_total_lift: "all_total F ==> all_total (lift i F)"
   20.27 +by (simp add: lift_def rename_def Extend.all_total_extend)
   20.28 +
   20.29 +
   20.30 +subsection{*The Operator @{term lift_set}*}
   20.31  
   20.32  lemma lift_set_empty [simp]: "lift_set i {} = {}"
   20.33  by (unfold lift_set_def, auto)
   20.34 @@ -133,9 +137,7 @@
   20.35  done
   20.36  
   20.37  lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
   20.38 -apply (unfold lift_set_def)
   20.39 -apply (simp add: image_Un)
   20.40 -done
   20.41 +by (simp add: lift_set_def image_Un)
   20.42  
   20.43  lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
   20.44  apply (unfold lift_set_def)
   20.45 @@ -143,7 +145,7 @@
   20.46  done
   20.47  
   20.48  
   20.49 -(*** the lattice operations ***)
   20.50 +subsection{*The Lattice Operations*}
   20.51  
   20.52  lemma bij_lift [iff]: "bij (lift i)"
   20.53  by (simp add: lift_def)
   20.54 @@ -157,7 +159,7 @@
   20.55  lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
   20.56  by (simp add: lift_def)
   20.57  
   20.58 -(*** Safety: co, stable, invariant ***)
   20.59 +subsection{*Safety: constrains, stable, invariant*}
   20.60  
   20.61  lemma lift_constrains: 
   20.62       "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
   20.63 @@ -169,29 +171,21 @@
   20.64  
   20.65  lemma lift_invariant: 
   20.66       "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
   20.67 -apply (unfold lift_def lift_set_def)
   20.68 -apply (simp add: rename_invariant)
   20.69 -done
   20.70 +by (simp add: lift_def lift_set_def rename_invariant)
   20.71  
   20.72  lemma lift_Constrains: 
   20.73       "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
   20.74 -apply (unfold lift_def lift_set_def)
   20.75 -apply (simp add: rename_Constrains)
   20.76 -done
   20.77 +by (simp add: lift_def lift_set_def rename_Constrains)
   20.78  
   20.79  lemma lift_Stable: 
   20.80       "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
   20.81 -apply (unfold lift_def lift_set_def)
   20.82 -apply (simp add: rename_Stable)
   20.83 -done
   20.84 +by (simp add: lift_def lift_set_def rename_Stable)
   20.85  
   20.86  lemma lift_Always: 
   20.87       "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
   20.88 -apply (unfold lift_def lift_set_def)
   20.89 -apply (simp add: rename_Always)
   20.90 -done
   20.91 +by (simp add: lift_def lift_set_def rename_Always)
   20.92  
   20.93 -(*** Progress: transient, ensures ***)
   20.94 +subsection{*Progress: transient, ensures*}
   20.95  
   20.96  lemma lift_transient: 
   20.97       "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
   20.98 @@ -223,16 +217,12 @@
   20.99  apply (simp add: o_def)
  20.100  done
  20.101  
  20.102 -lemma lift_guarantees_eq_lift_inv: "(lift i F \<in> X guarantees Y) =  
  20.103 +lemma lift_guarantees_eq_lift_inv:
  20.104 +     "(lift i F \<in> X guarantees Y) =  
  20.105        (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
  20.106  by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
  20.107  
  20.108  
  20.109 -(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj, 
  20.110 -     which is used only in TimerArray and perhaps isn't even essential
  20.111 -     there!
  20.112 -***)
  20.113 -
  20.114  (*To preserve snd means that the second component is there just to allow
  20.115    guarantees properties to be stated.  Converse fails, for lift i F can 
  20.116    change function components other than i*)
  20.117 @@ -293,59 +283,9 @@
  20.118  apply (erule constrains_imp_subset [THEN lift_set_mono])
  20.119  done
  20.120  
  20.121 -(** Lemmas for the transient theorem **)
  20.122 -
  20.123 -lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f"
  20.124 -by (rule ext, auto)
  20.125 -
  20.126 -lemma insert_map_upd:
  20.127 -     "(insert_map j t f)(i := s) =  
  20.128 -      (if i=j then insert_map i s f  
  20.129 -       else if i<j then insert_map j t (f(i:=s))  
  20.130 -       else insert_map j t (f(i - Suc 0 := s)))"
  20.131 -apply (rule ext) 
  20.132 -apply (simp split add: nat_diff_split) 
  20.133 - txt{*This simplification is VERY slow*}
  20.134 -done
  20.135 -
  20.136 -lemma insert_map_eq_diff:
  20.137 -     "[| insert_map i s f = insert_map j t g;  i\<noteq>j |]  
  20.138 -      ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
  20.139 -apply (subst insert_map_upd_same [symmetric])
  20.140 -apply (erule ssubst)
  20.141 -apply (simp only: insert_map_upd if_False split: split_if, blast)
  20.142 -done
  20.143 -
  20.144 -lemma lift_map_eq_diff: 
  20.145 -     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i\<noteq>j |]  
  20.146 -      ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
  20.147 -apply (unfold lift_map_def, auto)
  20.148 -apply (blast dest: insert_map_eq_diff)
  20.149 -done
  20.150 -
  20.151 -lemma lift_transient_eq_disj:
  20.152 -     "F \<in> preserves snd  
  20.153 -      ==> (lift i F \<in> transient (lift_set j (A <*> UNIV))) =  
  20.154 -          (i=j & F \<in> transient (A <*> UNIV) | A={})"
  20.155 -apply (case_tac "i=j")
  20.156 -apply (auto simp add: lift_transient)
  20.157 -apply (auto simp add: lift_set_def lift_def transient_def rename_def 
  20.158 -                      extend_def Domain_extend_act)
  20.159 -apply (drule subsetD, blast, auto)
  20.160 -apply (rename_tac s f uu s' f' uu')
  20.161 -apply (subgoal_tac "f'=f & uu'=uu")
  20.162 - prefer 2 apply (force dest!: preserves_imp_eq, auto)
  20.163 -apply (drule sym)
  20.164 -apply (drule subsetD)
  20.165 -apply (rule ImageI)
  20.166 -apply (erule bij_lift_map [THEN good_map_bij, 
  20.167 -                           THEN Extend.intro, 
  20.168 -                           THEN Extend.mem_extend_act_iff [THEN iffD2]], force)
  20.169 -apply (erule lift_map_eq_diff [THEN exE], auto)
  20.170 -done
  20.171 -
  20.172  (*USELESS??*)
  20.173 -lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) =  
  20.174 +lemma lift_map_image_Times:
  20.175 +     "lift_map i ` (A <*> UNIV) =  
  20.176        (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
  20.177  apply (auto intro!: bexI image_eqI simp add: lift_map_def)
  20.178  apply (rule split_conv [symmetric])
  20.179 @@ -368,7 +308,7 @@
  20.180  done
  20.181  
  20.182  
  20.183 -(*** Lemmas to handle function composition (o) more consistently ***)
  20.184 +subsection{*Lemmas to Handle Function Composition (o) More Consistently*}
  20.185  
  20.186  (*Lets us prove one version of a theorem and store others*)
  20.187  lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
  20.188 @@ -388,15 +328,18 @@
  20.189  done
  20.190  
  20.191  
  20.192 -(*** More lemmas about extend and project 
  20.193 -     They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
  20.194 +subsection{*More lemmas about extend and project*}
  20.195  
  20.196 -lemma extend_act_extend_act: "extend_act h' (extend_act h act) =  
  20.197 +text{*They could be moved to theory Extend or Project*}
  20.198 +
  20.199 +lemma extend_act_extend_act:
  20.200 +     "extend_act h' (extend_act h act) =  
  20.201        extend_act (%(x,(y,y')). h'(h(x,y),y')) act"
  20.202  apply (auto elim!: rev_bexI simp add: extend_act_def, blast) 
  20.203  done
  20.204  
  20.205 -lemma project_act_project_act: "project_act h (project_act h' act) =  
  20.206 +lemma project_act_project_act:
  20.207 +     "project_act h (project_act h' act) =  
  20.208        project_act (%(x,(y,y')). h'(h(x,y),y')) act"
  20.209  by (auto elim!: rev_bexI simp add: project_act_def)
  20.210  
  20.211 @@ -407,7 +350,7 @@
  20.212  by (simp add: extend_act_def project_act_def, blast)
  20.213  
  20.214  
  20.215 -(*** OK and "lift" ***)
  20.216 +subsection{*OK and "lift"*}
  20.217  
  20.218  lemma act_in_UNION_preserves_fst:
  20.219       "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
    21.1 --- a/src/HOL/UNITY/PPROD.thy	Sat Feb 08 14:46:22 2003 +0100
    21.2 +++ b/src/HOL/UNITY/PPROD.thy	Sat Feb 08 16:05:33 2003 +0100
    21.3 @@ -27,28 +27,20 @@
    21.4  
    21.5  (*** Basic properties ***)
    21.6  
    21.7 -lemma Init_PLam: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
    21.8 -apply (simp (no_asm) add: PLam_def lift_def lift_set_def)
    21.9 -done
   21.10 -
   21.11 -declare Init_PLam [simp]
   21.12 +lemma Init_PLam [simp]: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
   21.13 +by (simp add: PLam_def lift_def lift_set_def)
   21.14  
   21.15 -lemma PLam_empty: "PLam {} F = SKIP"
   21.16 -apply (simp (no_asm) add: PLam_def)
   21.17 -done
   21.18 +lemma PLam_empty [simp]: "PLam {} F = SKIP"
   21.19 +by (simp add: PLam_def)
   21.20  
   21.21 -lemma PLam_SKIP: "(plam i : I. SKIP) = SKIP"
   21.22 -apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant)
   21.23 -done
   21.24 -
   21.25 -declare PLam_SKIP [simp] PLam_empty [simp]
   21.26 +lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
   21.27 +by (simp add: PLam_def lift_SKIP JN_constant)
   21.28  
   21.29  lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
   21.30  by (unfold PLam_def, auto)
   21.31  
   21.32  lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
   21.33 -apply (simp (no_asm) add: PLam_def JN_component_iff)
   21.34 -done
   21.35 +by (simp add: PLam_def JN_component_iff)
   21.36  
   21.37  lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
   21.38  apply (unfold PLam_def)
   21.39 @@ -59,87 +51,89 @@
   21.40  
   21.41  (** Safety & Progress: but are they used anywhere? **)
   21.42  
   21.43 -lemma PLam_constrains: 
   21.44 -     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |] ==>   
   21.45 -      (PLam I F \<in> (lift_set i (A <*> UNIV)) co  
   21.46 -                  (lift_set i (B <*> UNIV)))  =   
   21.47 -      (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
   21.48 -apply (simp (no_asm_simp) add: PLam_def JN_constrains)
   21.49 +lemma PLam_constrains:
   21.50 +     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
   21.51 +      ==> (PLam I F \<in> (lift_set i (A <*> UNIV)) co
   21.52 +                      (lift_set i (B <*> UNIV)))  =
   21.53 +          (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
   21.54 +apply (simp add: PLam_def JN_constrains)
   21.55  apply (subst insert_Diff [symmetric], assumption)
   21.56 -apply (simp (no_asm_simp) add: lift_constrains)
   21.57 +apply (simp add: lift_constrains)
   21.58  apply (blast intro: constrains_imp_lift_constrains)
   21.59  done
   21.60  
   21.61 -lemma PLam_stable: 
   21.62 -     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]   
   21.63 -      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =  
   21.64 +lemma PLam_stable:
   21.65 +     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
   21.66 +      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
   21.67            (F i \<in> stable (A <*> UNIV))"
   21.68 -apply (simp (no_asm_simp) add: stable_def PLam_constrains)
   21.69 -done
   21.70 +by (simp add: stable_def PLam_constrains)
   21.71 +
   21.72 +lemma PLam_transient:
   21.73 +     "i \<in> I ==>
   21.74 +    PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
   21.75 +by (simp add: JN_transient PLam_def)
   21.76  
   21.77 -lemma PLam_transient: 
   21.78 -     "i \<in> I ==>  
   21.79 -    PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
   21.80 -apply (simp (no_asm_simp) add: JN_transient PLam_def)
   21.81 +text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
   21.82 +lemma PLam_ensures:
   21.83 +     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
   21.84 +         \<forall>j. F j \<in> preserves snd |]
   21.85 +      ==> PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
   21.86 +apply (simp add: ensures_def PLam_constrains PLam_transient
   21.87 +              lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
   21.88 +              Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
   21.89 +apply (rule rev_bexI, assumption)
   21.90 +apply (simp add: lift_transient)
   21.91  done
   21.92  
   21.93 -(*This holds because the F j cannot change (lift_set i)*)
   21.94 -lemma PLam_ensures: 
   21.95 -     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);   
   21.96 -         \<forall>j. F j \<in> preserves snd |] ==>   
   21.97 -      PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
   21.98 -apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
   21.99 -done
  21.100 -
  21.101 -lemma PLam_leadsTo_Basis: 
  21.102 -     "[| i \<in> I;   
  21.103 -         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co  
  21.104 -               ((A <*> UNIV) \<union> (B <*> UNIV));   
  21.105 -         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));   
  21.106 -         \<forall>j. F j \<in> preserves snd |] ==>   
  21.107 -      PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
  21.108 +lemma PLam_leadsTo_Basis:
  21.109 +     "[| i \<in> I;
  21.110 +         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
  21.111 +               ((A <*> UNIV) \<union> (B <*> UNIV));
  21.112 +         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
  21.113 +         \<forall>j. F j \<in> preserves snd |]
  21.114 +      ==> PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
  21.115  by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
  21.116  
  21.117  
  21.118  
  21.119  (** invariant **)
  21.120  
  21.121 -lemma invariant_imp_PLam_invariant: 
  21.122 -     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;   
  21.123 -         \<forall>j. F j \<in> preserves snd |]  
  21.124 +lemma invariant_imp_PLam_invariant:
  21.125 +     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;
  21.126 +         \<forall>j. F j \<in> preserves snd |]
  21.127        ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
  21.128  by (auto simp add: PLam_stable invariant_def)
  21.129  
  21.130  
  21.131  lemma PLam_preserves_fst [simp]:
  21.132 -     "\<forall>j. F j \<in> preserves snd  
  21.133 -      ==> (PLam I F \<in> preserves (v o sub j o fst)) =  
  21.134 +     "\<forall>j. F j \<in> preserves snd
  21.135 +      ==> (PLam I F \<in> preserves (v o sub j o fst)) =
  21.136            (if j \<in> I then F j \<in> preserves (v o fst) else True)"
  21.137 -by (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
  21.138 +by (simp add: PLam_def lift_preserves_sub)
  21.139  
  21.140  lemma PLam_preserves_snd [simp,intro]:
  21.141       "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
  21.142 -by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
  21.143 +by (simp add: PLam_def lift_preserves_snd_I)
  21.144  
  21.145  
  21.146  
  21.147  (*** guarantees properties ***)
  21.148  
  21.149 -(*This rule looks unsatisfactory because it refers to "lift".  One must use
  21.150 +text{*This rule looks unsatisfactory because it refers to "lift".  One must use
  21.151    lift_guarantees_eq_lift_inv to rewrite the first subgoal and
  21.152    something like lift_preserves_sub to rewrite the third.  However there's
  21.153 -  no obvious way to alternative for the third premise.*)
  21.154 -lemma guarantees_PLam_I: 
  21.155 -    "[| lift i (F i): X guarantees Y;  i \<in> I;   
  21.156 -        OK I (%i. lift i (F i)) |]   
  21.157 +  no obvious way to alternative for the third premise.*}
  21.158 +lemma guarantees_PLam_I:
  21.159 +    "[| lift i (F i): X guarantees Y;  i \<in> I;
  21.160 +        OK I (%i. lift i (F i)) |]
  21.161       ==> (PLam I F) \<in> X guarantees Y"
  21.162  apply (unfold PLam_def)
  21.163 -apply (simp (no_asm_simp) add: guarantees_JN_I)
  21.164 +apply (simp add: guarantees_JN_I)
  21.165  done
  21.166  
  21.167  lemma Allowed_PLam [simp]:
  21.168       "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
  21.169 -by (simp (no_asm) add: PLam_def)
  21.170 +by (simp add: PLam_def)
  21.171  
  21.172  
  21.173  lemma PLam_preserves [simp]:
  21.174 @@ -149,24 +143,24 @@
  21.175  
  21.176  (**UNUSED
  21.177      (*The f0 premise ensures that the product is well-defined.*)
  21.178 -    lemma PLam_invariant_imp_invariant: 
  21.179 -     "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;   
  21.180 +    lemma PLam_invariant_imp_invariant:
  21.181 +     "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;
  21.182               f0: Init (PLam I F) |] ==> F i \<in> invariant A"
  21.183      apply (auto simp add: invariant_def)
  21.184      apply (drule_tac c = "f0 (i:=x) " in subsetD)
  21.185      apply auto
  21.186      done
  21.187  
  21.188 -    lemma PLam_invariant: 
  21.189 -     "[| i \<in> I;  f0: Init (PLam I F) |]  
  21.190 +    lemma PLam_invariant:
  21.191 +     "[| i \<in> I;  f0: Init (PLam I F) |]
  21.192            ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
  21.193      apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
  21.194      done
  21.195  
  21.196      (*The f0 premise isn't needed if F is a constant program because then
  21.197        we get an initial state by replicating that of F*)
  21.198 -    lemma reachable_PLam: 
  21.199 -     "i \<in> I  
  21.200 +    lemma reachable_PLam:
  21.201 +     "i \<in> I
  21.202            ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
  21.203      apply (auto simp add: invariant_def)
  21.204      done
  21.205 @@ -185,15 +179,15 @@
  21.206      lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
  21.207      by auto
  21.208  
  21.209 -    lemma reachable_PLam_subset1: 
  21.210 +    lemma reachable_PLam_subset1:
  21.211       "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
  21.212      apply (force dest!: reachable_PLam)
  21.213      done
  21.214  
  21.215      (*simplify using reachable_lift??*)
  21.216      lemma reachable_lift_Join_PLam [rule_format]:
  21.217 -      "[| i \<notin> I;  A \<in> reachable (F i) |]      
  21.218 -       ==> \<forall>f. f \<in> reachable (PLam I F)       
  21.219 +      "[| i \<notin> I;  A \<in> reachable (F i) |]
  21.220 +       ==> \<forall>f. f \<in> reachable (PLam I F)
  21.221                    --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
  21.222      apply (erule reachable.induct)
  21.223      apply (ALLGOALS Clarify_tac)
  21.224 @@ -222,16 +216,16 @@
  21.225  
  21.226      (*The index set must be finite: otherwise infinitely many copies of F can
  21.227        perform actions, and PLam can never catch up in finite time.*)
  21.228 -    lemma reachable_PLam_subset2: 
  21.229 -     "finite I  
  21.230 +    lemma reachable_PLam_subset2:
  21.231 +     "finite I
  21.232            ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
  21.233      apply (erule finite_induct)
  21.234      apply (simp (no_asm))
  21.235      apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
  21.236      done
  21.237  
  21.238 -    lemma reachable_PLam_eq: 
  21.239 -     "finite I ==>  
  21.240 +    lemma reachable_PLam_eq:
  21.241 +     "finite I ==>
  21.242            reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
  21.243      apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
  21.244      done
  21.245 @@ -239,8 +233,8 @@
  21.246  
  21.247      (** Co **)
  21.248  
  21.249 -    lemma Constrains_imp_PLam_Constrains: 
  21.250 -     "[| F i \<in> A Co B;  i \<in> I;  finite I |]   
  21.251 +    lemma Constrains_imp_PLam_Constrains:
  21.252 +     "[| F i \<in> A Co B;  i \<in> I;  finite I |]
  21.253            ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
  21.254      apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
  21.255      apply (auto simp add: constrains_def PLam_def)
  21.256 @@ -249,37 +243,37 @@
  21.257  
  21.258  
  21.259  
  21.260 -    lemma PLam_Constrains: 
  21.261 -     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
  21.262 -          ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =   
  21.263 +    lemma PLam_Constrains:
  21.264 +     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
  21.265 +          ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =
  21.266                (F i \<in> A Co B)"
  21.267      apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
  21.268      done
  21.269  
  21.270 -    lemma PLam_Stable: 
  21.271 -     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
  21.272 +    lemma PLam_Stable:
  21.273 +     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
  21.274            ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
  21.275 -    apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
  21.276 +    apply (simp del: Init_PLam add: Stable_def PLam_Constrains)
  21.277      done
  21.278  
  21.279  
  21.280      (** const_PLam (no dependence on i) doesn't require the f0 premise **)
  21.281  
  21.282 -    lemma const_PLam_Constrains: 
  21.283 -     "[| i \<in> I;  finite I |]   
  21.284 -          ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =   
  21.285 +    lemma const_PLam_Constrains:
  21.286 +     "[| i \<in> I;  finite I |]
  21.287 +          ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =
  21.288                (F \<in> A Co B)"
  21.289      apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
  21.290      done
  21.291  
  21.292 -    lemma const_PLam_Stable: 
  21.293 -     "[| i \<in> I;  finite I |]   
  21.294 +    lemma const_PLam_Stable:
  21.295 +     "[| i \<in> I;  finite I |]
  21.296            ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
  21.297 -    apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
  21.298 +    apply (simp add: Stable_def const_PLam_Constrains)
  21.299      done
  21.300  
  21.301 -    lemma const_PLam_Increasing: 
  21.302 -	 "[| i \<in> I;  finite I |]   
  21.303 +    lemma const_PLam_Increasing:
  21.304 +	 "[| i \<in> I;  finite I |]
  21.305            ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
  21.306      apply (unfold Increasing_def)
  21.307      apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
    22.1 --- a/src/HOL/UNITY/Project.thy	Sat Feb 08 14:46:22 2003 +0100
    22.2 +++ b/src/HOL/UNITY/Project.thy	Sat Feb 08 16:05:33 2003 +0100
    22.3 @@ -16,20 +16,20 @@
    22.4    projecting :: "['c program => 'c set, 'a*'b => 'c, 
    22.5  		  'a program, 'c program set, 'a program set] => bool"
    22.6      "projecting C h F X' X ==
    22.7 -       ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
    22.8 +       \<forall>G. extend h F Join G \<in> X' --> F Join project h (C G) G \<in> X"
    22.9  
   22.10    extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
   22.11  		 'c program set, 'a program set] => bool"
   22.12      "extending C h F Y' Y ==
   22.13 -       ALL G. extend h F  ok G --> F Join project h (C G) G : Y
   22.14 -	      --> extend h F Join G : Y'"
   22.15 +       \<forall>G. extend h F  ok G --> F Join project h (C G) G \<in> Y
   22.16 +	      --> extend h F Join G \<in> Y'"
   22.17  
   22.18    subset_closed :: "'a set set => bool"
   22.19 -    "subset_closed U == ALL A: U. Pow A <= U"  
   22.20 +    "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"  
   22.21  
   22.22  
   22.23  lemma (in Extend) project_extend_constrains_I:
   22.24 -     "F : A co B ==> project h C (extend h F) : A co B"
   22.25 +     "F \<in> A co B ==> project h C (extend h F) \<in> A co B"
   22.26  apply (auto simp add: extend_act_def project_act_def constrains_def)
   22.27  done
   22.28  
   22.29 @@ -38,8 +38,8 @@
   22.30  
   22.31  (*used below to prove Join_project_ensures*)
   22.32  lemma (in Extend) project_unless [rule_format]:
   22.33 -     "[| G : stable C;  project h C G : A unless B |]  
   22.34 -      ==> G : (C Int extend_set h A) unless (extend_set h B)"
   22.35 +     "[| G \<in> stable C;  project h C G \<in> A unless B |]  
   22.36 +      ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
   22.37  apply (simp add: unless_def project_constrains)
   22.38  apply (blast dest: stable_constrains_Int intro: constrains_weaken)
   22.39  done
   22.40 @@ -47,21 +47,21 @@
   22.41  (*Generalizes project_constrains to the program F Join project h C G
   22.42    useful with guarantees reasoning*)
   22.43  lemma (in Extend) Join_project_constrains:
   22.44 -     "(F Join project h C G : A co B)  =   
   22.45 -        (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &   
   22.46 -         F : A co B)"
   22.47 +     "(F Join project h C G \<in> A co B)  =   
   22.48 +        (extend h F Join G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
   22.49 +         F \<in> A co B)"
   22.50  apply (simp (no_asm) add: project_constrains)
   22.51  apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 
   22.52               dest: constrains_imp_subset)
   22.53  done
   22.54  
   22.55  (*The condition is required to prove the left-to-right direction
   22.56 -  could weaken it to G : (C Int extend_set h A) co C*)
   22.57 +  could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
   22.58  lemma (in Extend) Join_project_stable: 
   22.59 -     "extend h F Join G : stable C  
   22.60 -      ==> (F Join project h C G : stable A)  =   
   22.61 -          (extend h F Join G : stable (C Int extend_set h A) &   
   22.62 -           F : stable A)"
   22.63 +     "extend h F Join G \<in> stable C  
   22.64 +      ==> (F Join project h C G \<in> stable A)  =   
   22.65 +          (extend h F Join G \<in> stable (C \<inter> extend_set h A) &   
   22.66 +           F \<in> stable A)"
   22.67  apply (unfold stable_def)
   22.68  apply (simp only: Join_project_constrains)
   22.69  apply (blast intro: constrains_weaken dest: constrains_Int)
   22.70 @@ -69,23 +69,23 @@
   22.71  
   22.72  (*For using project_guarantees in particular cases*)
   22.73  lemma (in Extend) project_constrains_I:
   22.74 -     "extend h F Join G : extend_set h A co extend_set h B  
   22.75 -      ==> F Join project h C G : A co B"
   22.76 +     "extend h F Join G \<in> extend_set h A co extend_set h B  
   22.77 +      ==> F Join project h C G \<in> A co B"
   22.78  apply (simp add: project_constrains extend_constrains)
   22.79  apply (blast intro: constrains_weaken dest: constrains_imp_subset)
   22.80  done
   22.81  
   22.82  lemma (in Extend) project_increasing_I: 
   22.83 -     "extend h F Join G : increasing (func o f)  
   22.84 -      ==> F Join project h C G : increasing func"
   22.85 +     "extend h F Join G \<in> increasing (func o f)  
   22.86 +      ==> F Join project h C G \<in> increasing func"
   22.87  apply (unfold increasing_def stable_def)
   22.88  apply (simp del: Join_constrains
   22.89              add: project_constrains_I extend_set_eq_Collect)
   22.90  done
   22.91  
   22.92  lemma (in Extend) Join_project_increasing:
   22.93 -     "(F Join project h UNIV G : increasing func)  =   
   22.94 -      (extend h F Join G : increasing (func o f))"
   22.95 +     "(F Join project h UNIV G \<in> increasing func)  =   
   22.96 +      (extend h F Join G \<in> increasing (func o f))"
   22.97  apply (rule iffI)
   22.98  apply (erule_tac [2] project_increasing_I)
   22.99  apply (simp del: Join_stable
  22.100 @@ -95,8 +95,8 @@
  22.101  
  22.102  (*The UNIV argument is essential*)
  22.103  lemma (in Extend) project_constrains_D:
  22.104 -     "F Join project h UNIV G : A co B  
  22.105 -      ==> extend h F Join G : extend_set h A co extend_set h B"
  22.106 +     "F Join project h UNIV G \<in> A co B  
  22.107 +      ==> extend h F Join G \<in> extend_set h A co extend_set h B"
  22.108  by (simp add: project_constrains extend_constrains)
  22.109  
  22.110  
  22.111 @@ -104,26 +104,26 @@
  22.112  
  22.113  lemma projecting_Int: 
  22.114       "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
  22.115 -      ==> projecting C h F (XA' Int XB') (XA Int XB)"
  22.116 +      ==> projecting C h F (XA' \<inter> XB') (XA \<inter> XB)"
  22.117  by (unfold projecting_def, blast)
  22.118  
  22.119  lemma projecting_Un: 
  22.120       "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
  22.121 -      ==> projecting C h F (XA' Un XB') (XA Un XB)"
  22.122 +      ==> projecting C h F (XA' \<union> XB') (XA \<union> XB)"
  22.123  by (unfold projecting_def, blast)
  22.124  
  22.125  lemma projecting_INT: 
  22.126 -     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]  
  22.127 -      ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"
  22.128 +     "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
  22.129 +      ==> projecting C h F (\<Inter>i \<in> I. X' i) (\<Inter>i \<in> I. X i)"
  22.130  by (unfold projecting_def, blast)
  22.131  
  22.132  lemma projecting_UN: 
  22.133 -     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]  
  22.134 -      ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"
  22.135 +     "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |]  
  22.136 +      ==> projecting C h F (\<Union>i \<in> I. X' i) (\<Union>i \<in> I. X i)"
  22.137  by (unfold projecting_def, blast)
  22.138  
  22.139  lemma projecting_weaken: 
  22.140 -     "[| projecting C h F X' X;  U'<=X';  X<=U |] ==> projecting C h F U' U"
  22.141 +     "[| projecting C h F X' X;  U'<=X';  X \<subseteq> U |] ==> projecting C h F U' U"
  22.142  by (unfold projecting_def, auto)
  22.143  
  22.144  lemma projecting_weaken_L: 
  22.145 @@ -132,26 +132,26 @@
  22.146  
  22.147  lemma extending_Int: 
  22.148       "[| extending C h F YA' YA;  extending C h F YB' YB |]  
  22.149 -      ==> extending C h F (YA' Int YB') (YA Int YB)"
  22.150 +      ==> extending C h F (YA' \<inter> YB') (YA \<inter> YB)"
  22.151  by (unfold extending_def, blast)
  22.152  
  22.153  lemma extending_Un: 
  22.154       "[| extending C h F YA' YA;  extending C h F YB' YB |]  
  22.155 -      ==> extending C h F (YA' Un YB') (YA Un YB)"
  22.156 +      ==> extending C h F (YA' \<union> YB') (YA \<union> YB)"
  22.157  by (unfold extending_def, blast)
  22.158  
  22.159  lemma extending_INT: 
  22.160 -     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]  
  22.161 -      ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)"
  22.162 +     "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
  22.163 +      ==> extending C h F (\<Inter>i \<in> I. Y' i) (\<Inter>i \<in> I. Y i)"
  22.164  by (unfold extending_def, blast)
  22.165  
  22.166  lemma extending_UN: 
  22.167 -     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]  
  22.168 -      ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)"
  22.169 +     "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |]  
  22.170 +      ==> extending C h F (\<Union>i \<in> I. Y' i) (\<Union>i \<in> I. Y i)"
  22.171  by (unfold extending_def, blast)
  22.172  
  22.173  lemma extending_weaken: 
  22.174 -     "[| extending C h F Y' Y;  Y'<=V';  V<=Y |] ==> extending C h F V' V"
  22.175 +     "[| extending C h F Y' Y;  Y'<=V';  V \<subseteq> Y |] ==> extending C h F V' V"
  22.176  by (unfold extending_def, auto)
  22.177  
  22.178  lemma extending_weaken_L: 
  22.179 @@ -204,9 +204,9 @@
  22.180  
  22.181  (*In practice, C = reachable(...): the inclusion is equality*)
  22.182  lemma (in Extend) reachable_imp_reachable_project:
  22.183 -     "[| reachable (extend h F Join G) <= C;   
  22.184 -         z : reachable (extend h F Join G) |]  
  22.185 -      ==> f z : reachable (F Join project h C G)"
  22.186 +     "[| reachable (extend h F Join G) \<subseteq> C;   
  22.187 +         z \<in> reachable (extend h F Join G) |]  
  22.188 +      ==> f z \<in> reachable (F Join project h C G)"
  22.189  apply (erule reachable.induct)
  22.190  apply (force intro!: reachable.Init simp add: split_extended_all, auto)
  22.191   apply (rule_tac act = x in reachable.Acts)
  22.192 @@ -217,8 +217,8 @@
  22.193  done
  22.194  
  22.195  lemma (in Extend) project_Constrains_D: 
  22.196 -     "F Join project h (reachable (extend h F Join G)) G : A Co B   
  22.197 -      ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"
  22.198 +     "F Join project h (reachable (extend h F Join G)) G \<in> A Co B   
  22.199 +      ==> extend h F Join G \<in> (extend_set h A) Co (extend_set h B)"
  22.200  apply (unfold Constrains_def)
  22.201  apply (simp del: Join_constrains
  22.202              add: Join_project_constrains, clarify)
  22.203 @@ -227,22 +227,22 @@
  22.204  done
  22.205  
  22.206  lemma (in Extend) project_Stable_D: 
  22.207 -     "F Join project h (reachable (extend h F Join G)) G : Stable A   
  22.208 -      ==> extend h F Join G : Stable (extend_set h A)"
  22.209 +     "F Join project h (reachable (extend h F Join G)) G \<in> Stable A   
  22.210 +      ==> extend h F Join G \<in> Stable (extend_set h A)"
  22.211  apply (unfold Stable_def)
  22.212  apply (simp (no_asm_simp) add: project_Constrains_D)
  22.213  done
  22.214  
  22.215  lemma (in Extend) project_Always_D: 
  22.216 -     "F Join project h (reachable (extend h F Join G)) G : Always A   
  22.217 -      ==> extend h F Join G : Always (extend_set h A)"
  22.218 +     "F Join project h (reachable (extend h F Join G)) G \<in> Always A   
  22.219 +      ==> extend h F Join G \<in> Always (extend_set h A)"
  22.220  apply (unfold Always_def)
  22.221  apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
  22.222  done
  22.223  
  22.224  lemma (in Extend) project_Increasing_D: 
  22.225 -     "F Join project h (reachable (extend h F Join G)) G : Increasing func   
  22.226 -      ==> extend h F Join G : Increasing (func o f)"
  22.227 +     "F Join project h (reachable (extend h F Join G)) G \<in> Increasing func   
  22.228 +      ==> extend h F Join G \<in> Increasing (func o f)"
  22.229  apply (unfold Increasing_def, auto)
  22.230  apply (subst extend_set_eq_Collect [symmetric])
  22.231  apply (simp (no_asm_simp) add: project_Stable_D)
  22.232 @@ -253,9 +253,9 @@
  22.233  
  22.234  (*In practice, C = reachable(...): the inclusion is equality*)
  22.235  lemma (in Extend) reachable_project_imp_reachable:
  22.236 -     "[| C <= reachable(extend h F Join G);    
  22.237 -         x : reachable (F Join project h C G) |]  
  22.238 -      ==> EX y. h(x,y) : reachable (extend h F Join G)"
  22.239 +     "[| C \<subseteq> reachable(extend h F Join G);    
  22.240 +         x \<in> reachable (F Join project h C G) |]  
  22.241 +      ==> \<exists>y. h(x,y) \<in> reachable (extend h F Join G)"
  22.242  apply (erule reachable.induct)
  22.243  apply  (force intro: reachable.Init)
  22.244  apply (auto simp add: project_act_def)
  22.245 @@ -270,15 +270,15 @@
  22.246  
  22.247  (*UNUSED*)
  22.248  lemma (in Extend) reachable_extend_Join_subset:
  22.249 -     "reachable (extend h F Join G) <= C   
  22.250 -      ==> reachable (extend h F Join G) <=  
  22.251 +     "reachable (extend h F Join G) \<subseteq> C   
  22.252 +      ==> reachable (extend h F Join G) \<subseteq>  
  22.253            extend_set h (reachable (F Join project h C G))"
  22.254  apply (auto dest: reachable_imp_reachable_project)
  22.255  done
  22.256  
  22.257  lemma (in Extend) project_Constrains_I: 
  22.258 -     "extend h F Join G : (extend_set h A) Co (extend_set h B)   
  22.259 -      ==> F Join project h (reachable (extend h F Join G)) G : A Co B"
  22.260 +     "extend h F Join G \<in> (extend_set h A) Co (extend_set h B)   
  22.261 +      ==> F Join project h (reachable (extend h F Join G)) G \<in> A Co B"
  22.262  apply (unfold Constrains_def)
  22.263  apply (simp del: Join_constrains
  22.264              add: Join_project_constrains extend_set_Int_distrib)
  22.265 @@ -291,43 +291,43 @@
  22.266  done
  22.267  
  22.268  lemma (in Extend) project_Stable_I: 
  22.269 -     "extend h F Join G : Stable (extend_set h A)   
  22.270 -      ==> F Join project h (reachable (extend h F Join G)) G : Stable A"
  22.271 +     "extend h F Join G \<in> Stable (extend_set h A)   
  22.272 +      ==> F Join project h (reachable (extend h F Join G)) G \<in> Stable A"
  22.273  apply (unfold Stable_def)
  22.274  apply (simp (no_asm_simp) add: project_Constrains_I)
  22.275  done
  22.276  
  22.277  lemma (in Extend) project_Always_I: 
  22.278 -     "extend h F Join G : Always (extend_set h A)   
  22.279 -      ==> F Join project h (reachable (extend h F Join G)) G : Always A"
  22.280 +     "extend h F Join G \<in> Always (extend_set h A)   
  22.281 +      ==> F Join project h (reachable (extend h F Join G)) G \<in> Always A"
  22.282  apply (unfold Always_def)
  22.283  apply (auto simp add: project_Stable_I)
  22.284  apply (unfold extend_set_def, blast)
  22.285  done
  22.286  
  22.287  lemma (in Extend) project_Increasing_I: 
  22.288 -    "extend h F Join G : Increasing (func o f)   
  22.289 -     ==> F Join project h (reachable (extend h F Join G)) G : Increasing func"
  22.290 +    "extend h F Join G \<in> Increasing (func o f)   
  22.291 +     ==> F Join project h (reachable (extend h F Join G)) G \<in> Increasing func"
  22.292  apply (unfold Increasing_def, auto)
  22.293  apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
  22.294  done
  22.295  
  22.296  lemma (in Extend) project_Constrains:
  22.297 -     "(F Join project h (reachable (extend h F Join G)) G : A Co B)  =   
  22.298 -      (extend h F Join G : (extend_set h A) Co (extend_set h B))"
  22.299 +     "(F Join project h (reachable (extend h F Join G)) G \<in> A Co B)  =   
  22.300 +      (extend h F Join G \<in> (extend_set h A) Co (extend_set h B))"
  22.301  apply (blast intro: project_Constrains_I project_Constrains_D)
  22.302  done
  22.303  
  22.304  lemma (in Extend) project_Stable: 
  22.305 -     "(F Join project h (reachable (extend h F Join G)) G : Stable A)  =   
  22.306 -      (extend h F Join G : Stable (extend_set h A))"
  22.307 +     "(F Join project h (reachable (extend h F Join G)) G \<in> Stable A)  =   
  22.308 +      (extend h F Join G \<in> Stable (extend_set h A))"
  22.309  apply (unfold Stable_def)
  22.310  apply (rule project_Constrains)
  22.311  done
  22.312  
  22.313  lemma (in Extend) project_Increasing: 
  22.314 -   "(F Join project h (reachable (extend h F Join G)) G : Increasing func)  =  
  22.315 -    (extend h F Join G : Increasing (func o f))"
  22.316 +   "(F Join project h (reachable (extend h F Join G)) G \<in> Increasing func)  =  
  22.317 +    (extend h F Join G \<in> Increasing (func o f))"
  22.318  apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
  22.319  done
  22.320  
  22.321 @@ -397,30 +397,24 @@
  22.322  subsubsection{*transient*}
  22.323  
  22.324  lemma (in Extend) transient_extend_set_imp_project_transient: 
  22.325 -     "[| G : transient (C Int extend_set h A);  G : stable C |]   
  22.326 -      ==> project h C G : transient (project_set h C Int A)"
  22.327 -
  22.328 -apply (unfold transient_def)
  22.329 -apply (auto simp add: Domain_project_act)
  22.330 -apply (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A")
  22.331 -prefer 2
  22.332 +     "[| G \<in> transient (C \<inter> extend_set h A);  G \<in> stable C |]   
  22.333 +      ==> project h C G \<in> transient (project_set h C \<inter> A)"
  22.334 +apply (auto simp add: transient_def Domain_project_act)
  22.335 +apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A")
  22.336 + prefer 2
  22.337   apply (simp add: stable_def constrains_def, blast) 
  22.338  (*back to main goal*)
  22.339 -apply (erule_tac V = "?AA <= -C Un ?BB" in thin_rl)
  22.340 +apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl)
  22.341  apply (drule bspec, assumption) 
  22.342  apply (simp add: extend_set_def project_act_def, blast)
  22.343  done
  22.344  
  22.345  (*converse might hold too?*)
  22.346  lemma (in Extend) project_extend_transient_D: 
  22.347 -     "project h C (extend h F) : transient (project_set h C Int D)  
  22.348 -      ==> F : transient (project_set h C Int D)"
  22.349 -apply (unfold transient_def)
  22.350 -apply (auto simp add: Domain_project_act)
  22.351 -apply (rule bexI)
  22.352 -prefer 2 apply assumption
  22.353 -apply auto
  22.354 -apply (unfold extend_act_def, blast)
  22.355 +     "project h C (extend h F) \<in> transient (project_set h C \<inter> D)  
  22.356 +      ==> F \<in> transient (project_set h C \<inter> D)"
  22.357 +apply (simp add: transient_def Domain_project_act, safe)
  22.358 +apply blast+
  22.359  done
  22.360  
  22.361  
  22.362 @@ -428,11 +422,12 @@
  22.363  
  22.364  (*Used to prove project_leadsETo_I*)
  22.365  lemma (in Extend) ensures_extend_set_imp_project_ensures:
  22.366 -     "[| extend h F : stable C;  G : stable C;   
  22.367 -         extend h F Join G : A ensures B;  A-B = C Int extend_set h D |]   
  22.368 +     "[| extend h F \<in> stable C;  G \<in> stable C;   
  22.369 +         extend h F Join G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
  22.370        ==> F Join project h C G   
  22.371 -            : (project_set h C Int project_set h A) ensures (project_set h B)"
  22.372 -apply (simp add: ensures_def project_constrains Join_transient extend_transient, clarify)
  22.373 +            \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
  22.374 +apply (simp add: ensures_def project_constrains Join_transient extend_transient,
  22.375 +       clarify)
  22.376  apply (intro conjI) 
  22.377  (*first subgoal*)
  22.378  apply (blast intro: extend_stable_project_set 
  22.379 @@ -457,19 +452,42 @@
  22.380                 [THEN project_extend_transient_D, THEN transient_strengthen])
  22.381  done
  22.382  
  22.383 +text{*Transferring a transient property upwards*}
  22.384 +lemma (in Extend) project_transient_extend_set:
  22.385 +     "project h C G \<in> transient (project_set h C \<inter> A - B)
  22.386 +      ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
  22.387 +apply (simp add: transient_def project_set_def extend_set_def project_act_def)
  22.388 +apply (elim disjE bexE)
  22.389 + apply (rule_tac x=Id in bexI)  
  22.390 +  apply (blast intro!: rev_bexI )+
  22.391 +done
  22.392 +
  22.393 +lemma (in Extend) project_unless2 [rule_format]:
  22.394 +     "[| G \<in> stable C;  project h C G \<in> (project_set h C \<inter> A) unless B |]  
  22.395 +      ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
  22.396 +by (auto dest: stable_constrains_Int intro: constrains_weaken
  22.397 +         simp add: unless_def project_constrains Diff_eq Int_assoc 
  22.398 +                   Int_extend_set_lemma)
  22.399 +
  22.400 +
  22.401 +lemma (in Extend) extend_unless:
  22.402 +   "[|extend h F \<in> stable C; F \<in> A unless B|]
  22.403 +    ==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B"
  22.404 +apply (simp add: unless_def stable_def)
  22.405 +apply (drule constrains_Int) 
  22.406 +apply (erule extend_constrains [THEN iffD2]) 
  22.407 +apply (erule constrains_weaken, blast) 
  22.408 +apply blast 
  22.409 +done
  22.410 +
  22.411  (*Used to prove project_leadsETo_D*)
  22.412  lemma (in Extend) Join_project_ensures [rule_format]:
  22.413 -     "[| project h C G ~: transient (A-B) | A<=B;   
  22.414 -         extend h F Join G : stable C;   
  22.415 -         F Join project h C G : A ensures B |]  
  22.416 -      ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
  22.417 -apply (erule disjE)
  22.418 -prefer 2 apply (blast intro: subset_imp_ensures)
  22.419 -apply (auto dest: extend_transient [THEN iffD2]
  22.420 -            intro: transient_strengthen project_set_I
  22.421 -                   project_unless [THEN unlessD] unlessI 
  22.422 -                   project_extend_constrains_I 
  22.423 -            simp add: ensures_def Join_transient)
  22.424 +     "[| extend h F Join G \<in> stable C;   
  22.425 +         F Join project h C G \<in> A ensures B |]  
  22.426 +      ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
  22.427 +apply (auto simp add: ensures_eq extend_unless project_unless)
  22.428 +apply (blast intro:  extend_transient [THEN iffD2] transient_strengthen)  
  22.429 +apply (blast intro: project_transient_extend_set transient_strengthen)  
  22.430  done
  22.431  
  22.432  text{*Lemma useful for both STRONG and WEAK progress, but the transient
  22.433 @@ -478,11 +496,10 @@
  22.434  (*The strange induction formula allows induction over the leadsTo
  22.435    assumption's non-atomic precondition*)
  22.436  lemma (in Extend) PLD_lemma:
  22.437 -     "[| ALL D. project h C G : transient D --> D={};   
  22.438 -         extend h F Join G : stable C;   
  22.439 -         F Join project h C G : (project_set h C Int A) leadsTo B |]  
  22.440 -      ==> extend h F Join G :  
  22.441 -          C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"
  22.442 +     "[| extend h F Join G \<in> stable C;   
  22.443 +         F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
  22.444 +      ==> extend h F Join G \<in>  
  22.445 +          C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
  22.446  apply (erule leadsTo_induct)
  22.447    apply (blast intro: leadsTo_Basis Join_project_ensures)
  22.448   apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
  22.449 @@ -490,74 +507,28 @@
  22.450  done
  22.451  
  22.452  lemma (in Extend) project_leadsTo_D_lemma:
  22.453 -     "[| ALL D. project h C G : transient D --> D={};   
  22.454 -         extend h F Join G : stable C;   
  22.455 -         F Join project h C G : (project_set h C Int A) leadsTo B |]  
  22.456 -      ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"
  22.457 +     "[| extend h F Join G \<in> stable C;   
  22.458 +         F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
  22.459 +      ==> extend h F Join G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
  22.460  apply (rule PLD_lemma [THEN leadsTo_weaken])
  22.461  apply (auto simp add: split_extended_all)
  22.462  done
  22.463  
  22.464  lemma (in Extend) Join_project_LeadsTo:
  22.465       "[| C = (reachable (extend h F Join G));  
  22.466 -         ALL D. project h C G : transient D --> D={};   
  22.467 -         F Join project h C G : A LeadsTo B |]  
  22.468 -      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
  22.469 +         F Join project h C G \<in> A LeadsTo B |]  
  22.470 +      ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
  22.471  by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
  22.472                                    project_set_reachable_extend_eq)
  22.473  
  22.474  
  22.475  subsection{*Towards the theorem @{text project_Ensures_D}*}
  22.476  
  22.477 -
  22.478 -lemma (in Extend) act_subset_imp_project_act_subset: 
  22.479 -     "act `` (C Int extend_set h A) <= B  
  22.480 -      ==> project_act h (Restrict C act) `` (project_set h C Int A)  
  22.481 -          <= project_set h B"
  22.482 -apply (unfold project_set_def extend_set_def project_act_def, blast)
  22.483 -done
  22.484 -
  22.485 -(*This trivial proof is the complementation part of transferring a transient
  22.486 -  property upwards.  The hard part would be to 
  22.487 -  show that G's action has a big enough domain.*)
  22.488 -lemma (in Extend) 
  22.489 -     "[| act: Acts G;        
  22.490 -         (project_act h (Restrict C act))``  
  22.491 -              (project_set h C Int A - B) <= -(project_set h C Int A - B) |]  
  22.492 -      ==> act``(C Int extend_set h A - extend_set h B)  
  22.493 -            <= -(C Int extend_set h A - extend_set h B)"
  22.494 -by (auto simp add: project_set_def extend_set_def project_act_def)
  22.495 -
  22.496 -lemma (in Extend) stable_project_transient:
  22.497 -     "[| G : stable ((C Int extend_set h A) - (extend_set h B));   
  22.498 -         project h C G : transient (project_set h C Int A - B) |]   
  22.499 -      ==> (C Int extend_set h A) - extend_set h B = {}"
  22.500 -apply (auto simp add: transient_def subset_Compl_self_eq Domain_project_act split_extended_all, blast)
  22.501 -apply (auto simp add: stable_def constrains_def)
  22.502 -apply (drule bspec, assumption) 
  22.503 -apply (auto simp add: Int_Diff extend_set_Diff_distrib [symmetric])
  22.504 -apply (drule act_subset_imp_project_act_subset)
  22.505 -apply (subgoal_tac "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}")
  22.506 -apply (erule_tac V = "?r``?A <= ?B" in thin_rl)+
  22.507 -apply (unfold project_set_def extend_set_def project_act_def)
  22.508 -prefer 2 apply blast
  22.509 -apply (rule ccontr)
  22.510 -apply (drule subsetD, blast)
  22.511 -apply (force simp add: split_extended_all)
  22.512 -done
  22.513 -
  22.514 -lemma (in Extend) project_unless2 [rule_format]:
  22.515 -     "[| G : stable C;  project h C G : (project_set h C Int A) unless B |]  
  22.516 -      ==> G : (C Int extend_set h A) unless (extend_set h B)"
  22.517 -by (auto dest: stable_constrains_Int intro: constrains_weaken
  22.518 -         simp add: unless_def project_constrains Diff_eq Int_assoc 
  22.519 -                   Int_extend_set_lemma)
  22.520 -
  22.521  lemma (in Extend) project_ensures_D_lemma:
  22.522 -     "[| G : stable ((C Int extend_set h A) - (extend_set h B));   
  22.523 -         F Join project h C G : (project_set h C Int A) ensures B;   
  22.524 -         extend h F Join G : stable C |]  
  22.525 -      ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
  22.526 +     "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
  22.527 +         F Join project h C G \<in> (project_set h C \<inter> A) ensures B;   
  22.528 +         extend h F Join G \<in> stable C |]  
  22.529 +      ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
  22.530  (*unless*)
  22.531  apply (auto intro!: project_unless2 [unfolded unless_def] 
  22.532              intro: project_extend_constrains_I 
  22.533 @@ -565,26 +536,24 @@
  22.534  (*transient*)
  22.535  (*A G-action cannot occur*)
  22.536   prefer 2
  22.537 - apply (force dest: stable_project_transient 
  22.538 -              simp del: Diff_eq_empty_iff
  22.539 -              simp add: Diff_eq_empty_iff [symmetric])
  22.540 + apply (blast intro: project_transient_extend_set) 
  22.541  (*An F-action*)
  22.542  apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
  22.543               simp add: split_extended_all)
  22.544  done
  22.545  
  22.546  lemma (in Extend) project_ensures_D:
  22.547 -     "[| F Join project h UNIV G : A ensures B;   
  22.548 -         G : stable (extend_set h A - extend_set h B) |]  
  22.549 -      ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"
  22.550 +     "[| F Join project h UNIV G \<in> A ensures B;   
  22.551 +         G \<in> stable (extend_set h A - extend_set h B) |]  
  22.552 +      ==> extend h F Join G \<in> (extend_set h A) ensures (extend_set h B)"
  22.553  apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
  22.554  done
  22.555  
  22.556  lemma (in Extend) project_Ensures_D: 
  22.557 -     "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B;   
  22.558 -         G : stable (reachable (extend h F Join G) Int extend_set h A -  
  22.559 +     "[| F Join project h (reachable (extend h F Join G)) G \<in> A Ensures B;   
  22.560 +         G \<in> stable (reachable (extend h F Join G) \<inter> extend_set h A -  
  22.561                       extend_set h B) |]  
  22.562 -      ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)"
  22.563 +      ==> extend h F Join G \<in> (extend_set h A) Ensures (extend_set h B)"
  22.564  apply (unfold Ensures_def)
  22.565  apply (rule project_ensures_D_lemma [THEN revcut_rl])
  22.566  apply (auto simp add: project_set_reachable_extend_eq [symmetric])
  22.567 @@ -594,7 +563,7 @@
  22.568  subsection{*Guarantees*}
  22.569  
  22.570  lemma (in Extend) project_act_Restrict_subset_project_act:
  22.571 -     "project_act h (Restrict C act) <= project_act h act"
  22.572 +     "project_act h (Restrict C act) \<subseteq> project_act h act"
  22.573  apply (auto simp add: project_act_def)
  22.574  done
  22.575  					   
  22.576 @@ -616,24 +585,24 @@
  22.577    Not clear that it has a converse [or that we want one!]*)
  22.578  
  22.579  (*The raw version; 3rd premise could be weakened by adding the
  22.580 -  precondition extend h F Join G : X' *)
  22.581 +  precondition extend h F Join G \<in> X' *)
  22.582  lemma (in Extend) project_guarantees_raw:
  22.583 - assumes xguary:  "F : X guarantees Y"
  22.584 + assumes xguary:  "F \<in> X guarantees Y"
  22.585       and closed:  "subset_closed (AllowedActs F)"
  22.586 -     and project: "!!G. extend h F Join G : X' 
  22.587 -                        ==> F Join project h (C G) G : X"
  22.588 -     and extend:  "!!G. [| F Join project h (C G) G : Y |]  
  22.589 -                        ==> extend h F Join G : Y'"
  22.590 - shows "extend h F : X' guarantees Y'"
  22.591 +     and project: "!!G. extend h F Join G \<in> X' 
  22.592 +                        ==> F Join project h (C G) G \<in> X"
  22.593 +     and extend:  "!!G. [| F Join project h (C G) G \<in> Y |]  
  22.594 +                        ==> extend h F Join G \<in> Y'"
  22.595 + shows "extend h F \<in> X' guarantees Y'"
  22.596  apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
  22.597  apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
  22.598  apply (erule project)
  22.599  done
  22.600  
  22.601  lemma (in Extend) project_guarantees:
  22.602 -     "[| F : X guarantees Y;  subset_closed (AllowedActs F);  
  22.603 +     "[| F \<in> X guarantees Y;  subset_closed (AllowedActs F);  
  22.604           projecting C h F X' X;  extending C h F Y' Y |]  
  22.605 -      ==> extend h F : X' guarantees Y'"
  22.606 +      ==> extend h F \<in> X' guarantees Y'"
  22.607  apply (rule guaranteesI)
  22.608  apply (auto simp add: guaranteesD projecting_def extending_def
  22.609                        subset_closed_ok_extend_imp_ok_project)
  22.610 @@ -648,73 +617,58 @@
  22.611  subsubsection{*Some could be deleted: the required versions are easy to prove*}
  22.612  
  22.613  lemma (in Extend) extend_guar_increasing:
  22.614 -     "[| F : UNIV guarantees increasing func;   
  22.615 +     "[| F \<in> UNIV guarantees increasing func;   
  22.616           subset_closed (AllowedActs F) |]  
  22.617 -      ==> extend h F : X' guarantees increasing (func o f)"
  22.618 +      ==> extend h F \<in> X' guarantees increasing (func o f)"
  22.619  apply (erule project_guarantees)
  22.620  apply (rule_tac [3] extending_increasing)
  22.621  apply (rule_tac [2] projecting_UNIV, auto)
  22.622  done
  22.623  
  22.624  lemma (in Extend) extend_guar_Increasing:
  22.625 -     "[| F : UNIV guarantees Increasing func;   
  22.626 +     "[| F \<in> UNIV guarantees Increasing func;   
  22.627           subset_closed (AllowedActs F) |]  
  22.628 -      ==> extend h F : X' guarantees Increasing (func o f)"
  22.629 +      ==> extend h F \<in> X' guarantees Increasing (func o f)"
  22.630  apply (erule project_guarantees)
  22.631  apply (rule_tac [3] extending_Increasing)
  22.632  apply (rule_tac [2] projecting_UNIV, auto)
  22.633  done
  22.634  
  22.635  lemma (in Extend) extend_guar_Always:
  22.636 -     "[| F : Always A guarantees Always B;   
  22.637 +     "[| F \<in> Always A guarantees Always B;   
  22.638           subset_closed (AllowedActs F) |]  
  22.639        ==> extend h F                    
  22.640 -            : Always(extend_set h A) guarantees Always(extend_set h B)"
  22.641 +            \<in> Always(extend_set h A) guarantees Always(extend_set h B)"
  22.642  apply (erule project_guarantees)
  22.643  apply (rule_tac [3] extending_Always)
  22.644  apply (rule_tac [2] projecting_Always, auto)
  22.645  done
  22.646  
  22.647 -lemma (in Extend) preserves_project_transient_empty:
  22.648 -     "[| G : preserves f;  project h C G : transient D |] ==> D={}"
  22.649 -apply (rule stable_transient_empty)
  22.650 - prefer 2 apply assumption
  22.651 -apply (blast intro: project_preserves_id_I 
  22.652 -                    preserves_id_subset_stable [THEN subsetD])
  22.653 -done
  22.654  
  22.655 -
  22.656 -subsubsection{*Guarantees with a leadsTo postcondition 
  22.657 -     ALL TOO WEAK because G can't affect F's variables at all**)
  22.658 +subsubsection{*Guarantees with a leadsTo postcondition*}
  22.659  
  22.660  lemma (in Extend) project_leadsTo_D:
  22.661 -     "[| F Join project h UNIV G : A leadsTo B;     
  22.662 -         G : preserves f |]   
  22.663 -      ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"
  22.664 -apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken])
  22.665 -apply (auto dest: preserves_project_transient_empty)
  22.666 +     "F Join project h UNIV G \<in> A leadsTo B
  22.667 +      ==> extend h F Join G \<in> (extend_set h A) leadsTo (extend_set h B)"
  22.668 +apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
  22.669  done
  22.670  
  22.671  lemma (in Extend) project_LeadsTo_D:
  22.672 -     "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B;
  22.673 -         G : preserves f |]   
  22.674 -       ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
  22.675 -apply (rule refl [THEN Join_project_LeadsTo])
  22.676 -apply (auto dest: preserves_project_transient_empty)
  22.677 +     "F Join project h (reachable (extend h F Join G)) G \<in> A LeadsTo B   
  22.678 +       ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
  22.679 +apply (rule refl [THEN Join_project_LeadsTo], auto)
  22.680  done
  22.681  
  22.682  lemma (in Extend) extending_leadsTo: 
  22.683 -     "(ALL G. extend h F ok G --> G : preserves f)  
  22.684 -      ==> extending (%G. UNIV) h F  
  22.685 -                  (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
  22.686 +     "extending (%G. UNIV) h F  
  22.687 +                (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
  22.688  apply (unfold extending_def)
  22.689  apply (blast intro: project_leadsTo_D)
  22.690  done
  22.691  
  22.692  lemma (in Extend) extending_LeadsTo: 
  22.693 -     "(ALL G. extend h F ok G --> G : preserves f)  
  22.694 -      ==> extending (%G. reachable (extend h F Join G)) h F  
  22.695 -                  (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
  22.696 +     "extending (%G. reachable (extend h F Join G)) h F  
  22.697 +                (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
  22.698  apply (unfold extending_def)
  22.699  apply (blast intro: project_LeadsTo_D)
  22.700  done
    23.1 --- a/src/HOL/UNITY/Simple/Common.thy	Sat Feb 08 14:46:22 2003 +0100
    23.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Sat Feb 08 16:05:33 2003 +0100
    23.3 @@ -54,20 +54,27 @@
    23.4  by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
    23.5  
    23.6  (*This one is  t := ftime t || t := gtime t*)
    23.7 -lemma "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
    23.8 +lemma "mk_total_program
    23.9 +         (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
   23.10         \<in> {m} co (maxfg m)"
   23.11 -by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
   23.12 +apply (simp add: mk_total_program_def) 
   23.13 +apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
   23.14 +done
   23.15  
   23.16  (*This one is  t := max (ftime t) (gtime t)*)
   23.17 -lemma  "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)  
   23.18 +lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
   23.19         \<in> {m} co (maxfg m)"
   23.20 -by (simp add: constrains_def maxfg_def max_def gasc)
   23.21 +apply (simp add: mk_total_program_def) 
   23.22 +apply (simp add: constrains_def maxfg_def max_def gasc)
   23.23 +done
   23.24  
   23.25  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
   23.26 -lemma  "mk_program   
   23.27 +lemma  "mk_total_program
   23.28            (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
   23.29         \<in> {m} co (maxfg m)"
   23.30 -by (simp add: constrains_def maxfg_def max_def gasc)
   23.31 +apply (simp add: mk_total_program_def) 
   23.32 +apply (simp add: constrains_def maxfg_def max_def gasc)
   23.33 +done
   23.34  
   23.35  
   23.36  (*It remans to prove that they satisfy CMT3': t does not decrease,
    24.1 --- a/src/HOL/UNITY/Simple/Lift.thy	Sat Feb 08 14:46:22 2003 +0100
    24.2 +++ b/src/HOL/UNITY/Simple/Lift.thy	Sat Feb 08 16:05:33 2003 +0100
    24.3 @@ -120,11 +120,12 @@
    24.4  
    24.5    Lift :: "state program"
    24.6      (*for the moment, we OMIT button_press*)
    24.7 -    "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
    24.8 +    "Lift == mk_total_program
    24.9 +                ({s. floor s = Min & ~ up s & move s & stop s &
   24.10  		          ~ open s & req s = {}},
   24.11 -			 {request_act, open_act, close_act,
   24.12 -			  req_up, req_down, move_up, move_down},
   24.13 -			 UNIV)"
   24.14 +		 {request_act, open_act, close_act,
   24.15 + 		  req_up, req_down, move_up, move_down},
   24.16 +		 UNIV)"
   24.17  
   24.18  
   24.19    (** Invariants **)
   24.20 @@ -196,7 +197,7 @@
   24.21  
   24.22  lemma open_stop: "Lift \<in> Always open_stop"
   24.23  apply (rule AlwaysI, force) 
   24.24 -apply (unfold Lift_def, constrains) 
   24.25 +apply (unfold Lift_def, constrains)
   24.26  done
   24.27  
   24.28  lemma stop_floor: "Lift \<in> Always stop_floor"
   24.29 @@ -249,19 +250,22 @@
   24.30  apply (unfold Lift_def, ensures_tac "open_act")
   24.31  done  (*lem_lift_1_5*)
   24.32  
   24.33 +
   24.34 +
   24.35 +
   24.36  lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
   24.37 -                     (Req n \<inter> opened - atFloor n)"
   24.38 +                       (Req n \<inter> opened - atFloor n)"
   24.39  apply (cut_tac stop_floor)
   24.40  apply (unfold Lift_def, ensures_tac "open_act")
   24.41  done  (*lem_lift_1_1*)
   24.42  
   24.43  lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
   24.44 -                     (Req n \<inter> closed - (atFloor n - queueing))"
   24.45 +                       (Req n \<inter> closed - (atFloor n - queueing))"
   24.46  apply (unfold Lift_def, ensures_tac "close_act")
   24.47  done  (*lem_lift_1_2*)
   24.48  
   24.49  lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
   24.50 -             LeadsTo (opened \<inter> atFloor n)"
   24.51 +                       LeadsTo (opened \<inter> atFloor n)"
   24.52  apply (unfold Lift_def, ensures_tac "open_act")
   24.53  done  (*lem_lift_1_7*)
   24.54  
    25.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Sat Feb 08 14:46:22 2003 +0100
    25.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Sat Feb 08 16:05:33 2003 +0100
    25.3 @@ -54,9 +54,10 @@
    25.4      "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
    25.5  
    25.6    Mutex :: "state program"
    25.7 -    "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
    25.8 -		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
    25.9 -			  UNIV)"
   25.10 +    "Mutex == mk_total_program
   25.11 +                 ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
   25.12 +		  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
   25.13 +                  UNIV)"
   25.14  
   25.15  
   25.16    (** The correct invariants **)
    26.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.ML	Sat Feb 08 14:46:22 2003 +0100
    26.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.ML	Sat Feb 08 16:05:33 2003 +0100
    26.3 @@ -22,8 +22,7 @@
    26.4    Here, it facilitates re-use of the Auth proofs.*)
    26.5  
    26.6  AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]);
    26.7 -
    26.8 -Addsimps [Nprg_def RS def_prg_simps];
    26.9 +Addsimps [Nprg_def RS def_prg_Init];
   26.10  
   26.11  
   26.12  (*A "possibility property": there are traces that reach the end.
   26.13 @@ -31,12 +30,13 @@
   26.14  Goal "A ~= B ==> EX NB. EX s: reachable Nprg.                \
   26.15  \                  Says A B (Crypt (pubK B) (Nonce NB)) : set s";
   26.16  by (REPEAT (resolve_tac [exI,bexI] 1));
   26.17 -by (res_inst_tac [("act", "NS3")] reachable_Acts 2);
   26.18 -by (res_inst_tac [("act", "NS2")] reachable_Acts 3);
   26.19 -by (res_inst_tac [("act", "NS1")] reachable_Acts 4);
   26.20 +by (res_inst_tac [("act", "totalize_act NS3")] reachable_Acts 2);
   26.21 +by (res_inst_tac [("act", "totalize_act NS2")] reachable_Acts 3);
   26.22 +by (res_inst_tac [("act", "totalize_act NS1")] reachable_Acts 4);
   26.23  by (rtac reachable_Init 5);
   26.24 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
   26.25 -by (REPEAT_FIRST (rtac exI ));
   26.26 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def, totalize_act_def])));
   26.27 +  (*Now ignore the possibility of identity transitions*)
   26.28 +by (REPEAT_FIRST (resolve_tac [disjI1, exI]));
   26.29  by possibility_tac;
   26.30  result();
   26.31  
   26.32 @@ -54,12 +54,23 @@
   26.33  by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset()));
   26.34  *)
   26.35  
   26.36 +val [prem] = 
   26.37 +Goal "(!!act s s'. [| act: {Id, Fake, NS1, NS2, NS3};  \
   26.38 +\                     (s,s') \\<in> act;  s \\<in> A |] ==> s': A')  \
   26.39 +\     ==> Nprg \\<in> A co A'";
   26.40 +by (asm_full_simp_tac (simpset() addsimps [Nprg_def, mk_total_program_def]) 1);
   26.41 +by (rtac constrainsI 1); 
   26.42 +by (rtac prem 1); 
   26.43 +by Auto_tac; 
   26.44 +qed "ns_constrainsI";
   26.45 +
   26.46 +
   26.47  fun ns_constrains_tac i = 
   26.48     SELECT_GOAL
   26.49        (EVERY [REPEAT (etac Always_ConstrainsI 1),
   26.50  	      REPEAT (resolve_tac [StableI, stableI,
   26.51  				   constrains_imp_Constrains] 1),
   26.52 -	      rtac constrainsI 1,
   26.53 +	      rtac ns_constrainsI 1,
   26.54  	      Full_simp_tac 1,
   26.55  	      REPEAT (FIRSTGOAL (etac disjE)),
   26.56  	      ALLGOALS (clarify_tac (claset() delrules [impI,impCE])),
    27.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Feb 08 14:46:22 2003 +0100
    27.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Feb 08 16:05:33 2003 +0100
    27.3 @@ -54,6 +54,6 @@
    27.4  constdefs
    27.5    Nprg :: state program
    27.6      (*Initial trace is empty*)
    27.7 -    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
    27.8 +    "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
    27.9  
   27.10  end
    28.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Sat Feb 08 14:46:22 2003 +0100
    28.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Sat Feb 08 16:05:33 2003 +0100
    28.3 @@ -24,7 +24,7 @@
    28.4      "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
    28.5  
    28.6    Rprg :: "state program"
    28.7 -    "Rprg == mk_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
    28.8 +    "Rprg == mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
    28.9  
   28.10    reach_invariant :: "state set"
   28.11      "reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
   28.12 @@ -81,7 +81,8 @@
   28.13  
   28.14  lemma lemma1: 
   28.15       "FP Rprg \<subseteq> fixedpoint"
   28.16 -apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def, auto)
   28.17 +apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
   28.18 +apply (auto simp add: stable_def constrains_def)
   28.19  apply (drule bspec, assumption)
   28.20  apply (simp add: Image_singleton image_iff)
   28.21  apply (drule fun_cong, auto)
   28.22 @@ -89,8 +90,8 @@
   28.23  
   28.24  lemma lemma2: 
   28.25       "fixedpoint \<subseteq> FP Rprg"
   28.26 -apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def)
   28.27 -apply (auto intro!: ext)
   28.28 +apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def)
   28.29 +apply (auto intro!: ext simp add: stable_def constrains_def)
   28.30  done
   28.31  
   28.32  lemma FP_fixedpoint: "FP Rprg = fixedpoint"
   28.33 @@ -104,7 +105,8 @@
   28.34    *)
   28.35  
   28.36  lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
   28.37 -apply (auto simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def)
   28.38 +apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
   28.39 +apply (auto simp add: Compl_FP UN_UN_flatten)
   28.40   apply (rule fun_upd_idem, force)
   28.41  apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
   28.42  done
    29.1 --- a/src/HOL/UNITY/SubstAx.thy	Sat Feb 08 14:46:22 2003 +0100
    29.2 +++ b/src/HOL/UNITY/SubstAx.thy	Sat Feb 08 16:05:33 2003 +0100
    29.3 @@ -21,7 +21,7 @@
    29.4    "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
    29.5  
    29.6  
    29.7 -(*Resembles the previous definition of LeadsTo*)
    29.8 +text{*Resembles the previous definition of LeadsTo*}
    29.9  lemma LeadsTo_eq_leadsTo: 
   29.10       "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
   29.11  apply (unfold LeadsTo_def)
   29.12 @@ -76,7 +76,7 @@
   29.13  lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
   29.14  by (simp add: LeadsTo_def)
   29.15  
   29.16 -(*Useful with cancellation, disjunction*)
   29.17 +text{*Useful with cancellation, disjunction*}
   29.18  lemma LeadsTo_Un_duplicate:
   29.19       "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
   29.20  by (simp add: Un_ac)
   29.21 @@ -91,14 +91,14 @@
   29.22  apply (blast intro: LeadsTo_Union)
   29.23  done
   29.24  
   29.25 -(*Binary union introduction rule*)
   29.26 +text{*Binary union introduction rule*}
   29.27  lemma LeadsTo_Un:
   29.28       "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
   29.29  apply (subst Un_eq_Union)
   29.30  apply (blast intro: LeadsTo_Union)
   29.31  done
   29.32  
   29.33 -(*Lets us look at the starting state*)
   29.34 +text{*Lets us look at the starting state*}
   29.35  lemma single_LeadsTo_I:
   29.36       "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
   29.37  by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
   29.38 @@ -182,8 +182,8 @@
   29.39  apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
   29.40  done
   29.41  
   29.42 -(*Set difference: maybe combine with leadsTo_weaken_L??
   29.43 -  This is the most useful form of the "disjunction" rule*)
   29.44 +text{*Set difference: maybe combine with leadsTo_weaken_L??
   29.45 +  This is the most useful form of the "disjunction" rule*}
   29.46  lemma LeadsTo_Diff:
   29.47       "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
   29.48        ==> F \<in> A LeadsTo C"
   29.49 @@ -198,18 +198,18 @@
   29.50  done
   29.51  
   29.52  
   29.53 -(*Version with no index set*)
   29.54 +text{*Version with no index set*}
   29.55  lemma LeadsTo_UN_UN_noindex: 
   29.56       "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
   29.57  by (blast intro: LeadsTo_UN_UN)
   29.58  
   29.59 -(*Version with no index set*)
   29.60 +text{*Version with no index set*}
   29.61  lemma all_LeadsTo_UN_UN:
   29.62       "\<forall>i. F \<in> (A i) LeadsTo (A' i)  
   29.63        ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
   29.64  by (blast intro: LeadsTo_UN_UN)
   29.65  
   29.66 -(*Binary union version*)
   29.67 +text{*Binary union version*}
   29.68  lemma LeadsTo_Un_Un:
   29.69       "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]  
   29.70              ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
   29.71 @@ -247,18 +247,18 @@
   29.72  done
   29.73  
   29.74  
   29.75 -(** The impossibility law **)
   29.76 +text{*The impossibility law*}
   29.77  
   29.78 -(*The set "A" may be non-empty, but it contains no reachable states*)
   29.79 -lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)"
   29.80 +text{*The set "A" may be non-empty, but it contains no reachable states*}
   29.81 +lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)"
   29.82  apply (simp add: LeadsTo_def Always_eq_includes_reachable)
   29.83  apply (drule leadsTo_empty, auto)
   29.84  done
   29.85  
   29.86  
   29.87 -(** PSP: Progress-Safety-Progress **)
   29.88 +subsection{*PSP: Progress-Safety-Progress*}
   29.89  
   29.90 -(*Special case of PSP: Misra's "stable conjunction"*)
   29.91 +text{*Special case of PSP: Misra's "stable conjunction"*}
   29.92  lemma PSP_Stable:
   29.93       "[| F \<in> A LeadsTo A';  F \<in> Stable B |]  
   29.94        ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
   29.95 @@ -336,7 +336,7 @@
   29.96        ==> F \<in> A LeadsTo B"
   29.97  by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
   29.98  
   29.99 -(*Integer version.  Could generalize from 0 to any lower bound*)
  29.100 +text{*Integer version.  Could generalize from 0 to any lower bound*}
  29.101  lemma integ_0_le_induct:
  29.102       "[| F \<in> Always {s. (0::int) \<le> f s};   
  29.103           !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo                      
    30.1 --- a/src/HOL/UNITY/UNITY.thy	Sat Feb 08 14:46:22 2003 +0100
    30.2 +++ b/src/HOL/UNITY/UNITY.thy	Sat Feb 08 16:05:33 2003 +0100
    30.3 @@ -50,12 +50,12 @@
    30.4    invariant :: "'a set => 'a program set"
    30.5      "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
    30.6  
    30.7 -  (*Polymorphic in both states and the meaning of \<le> *)
    30.8    increasing :: "['a => 'b::{order}] => 'a program set"
    30.9 +    --{*Polymorphic in both states and the meaning of @{text "\<le>"}*}
   30.10      "increasing f == \<Inter>z. stable {s. z \<le> f s}"
   30.11  
   30.12  
   30.13 -(*Perhaps equalities.ML shouldn't add this in the first place!*)
   30.14 +text{*Perhaps equalities.ML shouldn't add this in the first place!*}
   30.15  declare image_Collect [simp del]
   30.16  
   30.17  (*** The abstract type of programs ***)
   30.18 @@ -83,14 +83,14 @@
   30.19  (** Inspectors for type "program" **)
   30.20  
   30.21  lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
   30.22 -by (auto simp add: program_typedef)
   30.23 +by (simp add: program_typedef)
   30.24  
   30.25  lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
   30.26 -by (auto simp add: program_typedef)
   30.27 +by (simp add: program_typedef)
   30.28  
   30.29  lemma AllowedActs_eq [simp]:
   30.30       "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
   30.31 -by (auto simp add: program_typedef)
   30.32 +by (simp add: program_typedef)
   30.33  
   30.34  (** Equality for UNITY programs **)
   30.35  
   30.36 @@ -121,38 +121,6 @@
   30.37  by (blast intro: program_equalityI program_equalityE)
   30.38  
   30.39  
   30.40 -(*** These rules allow "lazy" definition expansion 
   30.41 -     They avoid expanding the full program, which is a large expression
   30.42 -***)
   30.43 -
   30.44 -lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init"
   30.45 -by auto
   30.46 -
   30.47 -lemma def_prg_Acts:
   30.48 -     "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"
   30.49 -by auto
   30.50 -
   30.51 -lemma def_prg_AllowedActs:
   30.52 -     "F == mk_program (init,acts,allowed)  
   30.53 -      ==> AllowedActs F = insert Id allowed"
   30.54 -by auto
   30.55 -
   30.56 -(*The program is not expanded, but its Init and Acts are*)
   30.57 -lemma def_prg_simps:
   30.58 -    "[| F == mk_program (init,acts,allowed) |]  
   30.59 -     ==> Init F = init & Acts F = insert Id acts"
   30.60 -by simp
   30.61 -
   30.62 -(*An action is expanded only if a pair of states is being tested against it*)
   30.63 -lemma def_act_simp:
   30.64 -     "[| act == {(s,s'). P s s'} |] ==> ((s,s') \<in> act) = P s s'"
   30.65 -by auto
   30.66 -
   30.67 -(*A set is expanded only if an element is being tested against it*)
   30.68 -lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
   30.69 -by auto
   30.70 -
   30.71 -
   30.72  (*** co ***)
   30.73  
   30.74  lemma constrainsI: 
   30.75 @@ -176,12 +144,12 @@
   30.76  lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
   30.77  by (unfold constrains_def, blast)
   30.78  
   30.79 -(*monotonic in 2nd argument*)
   30.80 +text{*monotonic in 2nd argument*}
   30.81  lemma constrains_weaken_R: 
   30.82      "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
   30.83  by (unfold constrains_def, blast)
   30.84  
   30.85 -(*anti-monotonic in 1st argument*)
   30.86 +text{*anti-monotonic in 1st argument*}
   30.87  lemma constrains_weaken_L: 
   30.88      "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
   30.89  by (unfold constrains_def, blast)
   30.90 @@ -227,8 +195,8 @@
   30.91  lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
   30.92  by (unfold constrains_def, auto)
   30.93  
   30.94 -(*The reasoning is by subsets since "co" refers to single actions
   30.95 -  only.  So this rule isn't that useful.*)
   30.96 +text{*The reasoning is by subsets since "co" refers to single actions
   30.97 +  only.  So this rule isn't that useful.*}
   30.98  lemma constrains_trans: 
   30.99      "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
  30.100  by (unfold constrains_def, blast)
  30.101 @@ -304,7 +272,7 @@
  30.102  lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
  30.103  by (simp add: invariant_def)
  30.104  
  30.105 -(*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*)
  30.106 +text{*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*}
  30.107  lemma invariant_Int:
  30.108       "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
  30.109  by (auto simp add: invariant_def stable_Int)
  30.110 @@ -314,7 +282,6 @@
  30.111  
  30.112  lemma increasingD: 
  30.113       "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
  30.114 -
  30.115  by (unfold increasing_def, blast)
  30.116  
  30.117  lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
  30.118 @@ -341,8 +308,8 @@
  30.119       ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
  30.120  by (unfold constrains_def, blast)
  30.121  
  30.122 -(*As above, but for the trivial case of a one-variable state, in which the
  30.123 -  state is identified with its one variable.*)
  30.124 +text{*As above, but for the trivial case of a one-variable state, in which the
  30.125 +  state is identified with its one variable.*}
  30.126  lemma elimination_sing: 
  30.127      "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
  30.128  by (unfold constrains_def, blast)
  30.129 @@ -376,4 +343,119 @@
  30.130  lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
  30.131  by blast
  30.132  
  30.133 +
  30.134 +subsection{*Partial versus Total Transitions*}
  30.135 +
  30.136 +constdefs
  30.137 +  totalize_act :: "('a * 'a)set => ('a * 'a)set"
  30.138 +    "totalize_act act == act \<union> diag (-(Domain act))"
  30.139 +
  30.140 +  totalize :: "'a program => 'a program"
  30.141 +    "totalize F == mk_program (Init F,
  30.142 +			       totalize_act ` Acts F,
  30.143 +			       AllowedActs F)"
  30.144 +
  30.145 +  mk_total_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
  30.146 +		   => 'a program"
  30.147 +    "mk_total_program args == totalize (mk_program args)"
  30.148 +
  30.149 +  all_total :: "'a program => bool"
  30.150 +    "all_total F == \<forall>act \<in> Acts F. Domain act = UNIV"
  30.151 +  
  30.152 +lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
  30.153 +by (blast intro: sym [THEN image_eqI])
  30.154 +
  30.155 +
  30.156 +text{*Basic properties*}
  30.157 +
  30.158 +lemma totalize_act_Id [simp]: "totalize_act Id = Id"
  30.159 +by (simp add: totalize_act_def) 
  30.160 +
  30.161 +lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"
  30.162 +by (auto simp add: totalize_act_def)
  30.163 +
  30.164 +lemma Init_totalize [simp]: "Init (totalize F) = Init F"
  30.165 +by (unfold totalize_def, auto)
  30.166 +
  30.167 +lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)"
  30.168 +by (simp add: totalize_def insert_Id_image_Acts) 
  30.169 +
  30.170 +lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"
  30.171 +by (simp add: totalize_def)
  30.172 +
  30.173 +lemma totalize_constrains_iff [simp]: "(totalize F \<in> A co B) = (F \<in> A co B)"
  30.174 +by (simp add: totalize_def totalize_act_def constrains_def, blast)
  30.175 +
  30.176 +lemma totalize_stable_iff [simp]: "(totalize F \<in> stable A) = (F \<in> stable A)"
  30.177 +by (simp add: stable_def)
  30.178 +
  30.179 +lemma totalize_invariant_iff [simp]:
  30.180 +     "(totalize F \<in> invariant A) = (F \<in> invariant A)"
  30.181 +by (simp add: invariant_def)
  30.182 +
  30.183 +lemma all_total_totalize: "all_total (totalize F)"
  30.184 +by (simp add: totalize_def all_total_def)
  30.185 +
  30.186 +lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"
  30.187 +by (force simp add: totalize_act_def)
  30.188 +
  30.189 +lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)"
  30.190 +apply (simp add: all_total_def totalize_def) 
  30.191 +apply (rule program_equalityI)
  30.192 +  apply (simp_all add: Domain_iff_totalize_act image_def)
  30.193 +done
  30.194 +
  30.195 +lemma all_total_iff_totalize: "all_total F = (totalize F = F)"
  30.196 +apply (rule iffI) 
  30.197 + apply (erule all_total_imp_totalize) 
  30.198 +apply (erule subst) 
  30.199 +apply (rule all_total_totalize) 
  30.200 +done
  30.201 +
  30.202 +lemma mk_total_program_constrains_iff [simp]:
  30.203 +     "(mk_total_program args \<in> A co B) = (mk_program args \<in> A co B)"
  30.204 +by (simp add: mk_total_program_def)
  30.205 +
  30.206 +
  30.207 +subsection{*Rules for Lazy Definition Expansion*}
  30.208 +
  30.209 +text{*They avoid expanding the full program, which is a large expression*}
  30.210 +
  30.211 +lemma def_prg_Init:
  30.212 +     "F == mk_total_program (init,acts,allowed) ==> Init F = init"
  30.213 +by (simp add: mk_total_program_def)
  30.214 +
  30.215 +lemma def_prg_Acts:
  30.216 +     "F == mk_total_program (init,acts,allowed) 
  30.217 +      ==> Acts F = insert Id (totalize_act ` acts)"
  30.218 +by (simp add: mk_total_program_def)
  30.219 +
  30.220 +lemma def_prg_AllowedActs:
  30.221 +     "F == mk_total_program (init,acts,allowed)  
  30.222 +      ==> AllowedActs F = insert Id allowed"
  30.223 +by (simp add: mk_total_program_def)
  30.224 +
  30.225 +text{*An action is expanded if a pair of states is being tested against it*}
  30.226 +lemma def_act_simp:
  30.227 +     "act == {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
  30.228 +by (simp add: mk_total_program_def)
  30.229 +
  30.230 +text{*A set is expanded only if an element is being tested against it*}
  30.231 +lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
  30.232 +by (simp add: mk_total_program_def)
  30.233 +
  30.234 +(** Inspectors for type "program" **)
  30.235 +
  30.236 +lemma Init_total_eq [simp]:
  30.237 +     "Init (mk_total_program (init,acts,allowed)) = init"
  30.238 +by (simp add: mk_total_program_def)
  30.239 +
  30.240 +lemma Acts_total_eq [simp]:
  30.241 +    "Acts(mk_total_program(init,acts,allowed)) = insert Id (totalize_act`acts)"
  30.242 +by (simp add: mk_total_program_def)
  30.243 +
  30.244 +lemma AllowedActs_total_eq [simp]:
  30.245 +     "AllowedActs (mk_total_program (init,acts,allowed)) = insert Id allowed"
  30.246 +by (auto simp add: mk_total_program_def)
  30.247 +
  30.248  end
    31.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Sat Feb 08 14:46:22 2003 +0100
    31.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Sat Feb 08 16:05:33 2003 +0100
    31.3 @@ -72,6 +72,8 @@
    31.4  
    31.5  
    31.6  (*UNITY*)
    31.7 +val mk_total_program_def = thm "mk_total_program_def";
    31.8 +val totalize_act_def = thm "totalize_act_def";
    31.9  val constrains_def = thm "constrains_def";
   31.10  val stable_def = thm "stable_def";
   31.11  val invariant_def = thm "invariant_def";
   31.12 @@ -91,7 +93,6 @@
   31.13  val def_prg_Init = thm "def_prg_Init";
   31.14  val def_prg_Acts = thm "def_prg_Acts";
   31.15  val def_prg_AllowedActs = thm "def_prg_AllowedActs";
   31.16 -val def_prg_simps = thm "def_prg_simps";
   31.17  val def_act_simp = thm "def_act_simp";
   31.18  val def_set_simp = thm "def_set_simp";
   31.19  val constrainsI = thm "constrainsI";
   31.20 @@ -140,13 +141,14 @@
   31.21  val Int_Union_Union = thm "Int_Union_Union";
   31.22  val Image_less_than = thm "Image_less_than";
   31.23  val Image_inverse_less_than = thm "Image_inverse_less_than";
   31.24 +val totalize_constrains_iff = thm "totalize_constrains_iff";
   31.25  
   31.26  (*WFair*)
   31.27  val stable_transient_empty = thm "stable_transient_empty";
   31.28  val transient_strengthen = thm "transient_strengthen";
   31.29  val transientI = thm "transientI";
   31.30 +val totalize_transientI = thm "totalize_transientI";
   31.31  val transientE = thm "transientE";
   31.32 -val transient_UNIV = thm "transient_UNIV";
   31.33  val transient_empty = thm "transient_empty";
   31.34  val ensuresI = thm "ensuresI";
   31.35  val ensuresD = thm "ensuresD";
   31.36 @@ -415,12 +417,14 @@
   31.37  val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
   31.38  val Allowed_eq = thm "Allowed_eq";
   31.39  val def_prg_Allowed = thm "def_prg_Allowed";
   31.40 +val def_total_prg_Allowed = thm "def_total_prg_Allowed";
   31.41  val safety_prop_constrains = thm "safety_prop_constrains";
   31.42  val safety_prop_stable = thm "safety_prop_stable";
   31.43  val safety_prop_Int = thm "safety_prop_Int";
   31.44  val safety_prop_INTER1 = thm "safety_prop_INTER1";
   31.45  val safety_prop_INTER = thm "safety_prop_INTER";
   31.46  val def_UNION_ok_iff = thm "def_UNION_ok_iff";
   31.47 +val totalize_JN = thm "totalize_JN";
   31.48  
   31.49  (*Comp*)
   31.50  val preserves_def = thm "preserves_def";
   31.51 @@ -670,11 +674,6 @@
   31.52  val mem_lift_act_iff = thm "mem_lift_act_iff";
   31.53  val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
   31.54  val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
   31.55 -val insert_map_upd_same = thm "insert_map_upd_same";
   31.56 -val insert_map_upd = thm "insert_map_upd";
   31.57 -val insert_map_eq_diff = thm "insert_map_eq_diff";
   31.58 -val lift_map_eq_diff = thm "lift_map_eq_diff";
   31.59 -val lift_transient_eq_disj = thm "lift_transient_eq_disj";
   31.60  val lift_map_image_Times = thm "lift_map_image_Times";
   31.61  val lift_preserves_eq = thm "lift_preserves_eq";
   31.62  val lift_preserves_sub = thm "lift_preserves_sub";
   31.63 @@ -751,14 +750,19 @@
   31.64  (*Combines a list of invariance THEOREMS into one.*)
   31.65  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I)
   31.66  
   31.67 -(*proves "co" properties when the program is specified*)
   31.68 +(*Proves "co" properties when the program is specified.  Any use of invariants
   31.69 +  (from weak constrains) must have been done already.*)
   31.70  fun gen_constrains_tac(cs,ss) i = 
   31.71     SELECT_GOAL
   31.72        (EVERY [REPEAT (Always_Int_tac 1),
   31.73 +              (*reduce the fancy safety properties to "constrains"*)
   31.74  	      REPEAT (etac Always_ConstrainsI 1
   31.75  		      ORELSE
   31.76  		      resolve_tac [StableI, stableI,
   31.77  				   constrains_imp_Constrains] 1),
   31.78 +              (*for safety, the totalize operator can be ignored*)
   31.79 +	      simp_tac (HOL_ss addsimps
   31.80 +                         [mk_total_program_def, totalize_constrains_iff]) 1,
   31.81  	      rtac constrainsI 1,
   31.82  	      full_simp_tac ss 1,
   31.83  	      REPEAT (FIRSTGOAL (etac disjE)),
   31.84 @@ -774,8 +778,9 @@
   31.85  		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
   31.86  				    EnsuresI, ensuresI] 1),
   31.87  	      (*now there are two subgoals: co & transient*)
   31.88 -	      simp_tac ss 2,
   31.89 -	      res_inst_tac [("act", sact)] transientI 2,
   31.90 +	      simp_tac (ss addsimps [mk_total_program_def]) 2,
   31.91 +	      res_inst_tac [("act", sact)] totalize_transientI 2 
   31.92 + 	      ORELSE res_inst_tac [("act", sact)] transientI 2,
   31.93                   (*simplify the command's domain*)
   31.94  	      simp_tac (ss addsimps [Domain_def]) 3,
   31.95  	      gen_constrains_tac (cs,ss) 1,
    32.1 --- a/src/HOL/UNITY/Union.thy	Sat Feb 08 14:46:22 2003 +0100
    32.2 +++ b/src/HOL/UNITY/Union.thy	Sat Feb 08 16:05:33 2003 +0100
    32.3 @@ -32,7 +32,7 @@
    32.4    SKIP :: "'a program"
    32.5      "SKIP == mk_program (UNIV, {}, UNIV)"
    32.6  
    32.7 -  (*Characterizes safety properties.  Used with specifying AllowedActs*)
    32.8 +  (*Characterizes safety properties.  Used with specifying Allowed*)
    32.9    safety_prop :: "'a program set => bool"
   32.10      "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
   32.11  
   32.12 @@ -316,10 +316,10 @@
   32.13  subsection{*the ok and OK relations*}
   32.14  
   32.15  lemma ok_SKIP1 [iff]: "SKIP ok F"
   32.16 -by (auto simp add: ok_def)
   32.17 +by (simp add: ok_def)
   32.18  
   32.19  lemma ok_SKIP2 [iff]: "F ok SKIP"
   32.20 -by (auto simp add: ok_def)
   32.21 +by (simp add: ok_def)
   32.22  
   32.23  lemma ok_Join_commute:
   32.24       "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
   32.25 @@ -332,7 +332,8 @@
   32.26  
   32.27  lemma ok_iff_OK:
   32.28       "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"
   32.29 -by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast)
   32.30 +by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
   32.31 +              all_conj_distrib eq_commute,   blast)
   32.32  
   32.33  lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)"
   32.34  by (auto simp add: ok_def)
   32.35 @@ -374,7 +375,7 @@
   32.36  lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
   32.37  by (auto simp add: OK_iff_ok ok_iff_Allowed)
   32.38  
   32.39 -subsection{*@{text safety_prop}, for reasoning about
   32.40 +subsection{*@{term safety_prop}, for reasoning about
   32.41   given instances of "ok"*}
   32.42  
   32.43  lemma safety_prop_Acts_iff:
   32.44 @@ -389,11 +390,6 @@
   32.45       "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
   32.46  by (simp add: Allowed_def safety_prop_Acts_iff)
   32.47  
   32.48 -lemma def_prg_Allowed:
   32.49 -     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
   32.50 -      ==> Allowed F = X"
   32.51 -by (simp add: Allowed_eq)
   32.52 -
   32.53  (*For safety_prop to hold, the property must be satisfiable!*)
   32.54  lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)"
   32.55  by (simp add: safety_prop_def constrains_def, blast)
   32.56 @@ -413,9 +409,35 @@
   32.57       "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
   32.58  by (auto simp add: safety_prop_def, blast)
   32.59  
   32.60 +lemma def_prg_Allowed:
   32.61 +     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
   32.62 +      ==> Allowed F = X"
   32.63 +by (simp add: Allowed_eq)
   32.64 +
   32.65 +lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F"
   32.66 +by (simp add: Allowed_def) 
   32.67 +
   32.68 +lemma def_total_prg_Allowed:
   32.69 +     "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
   32.70 +      ==> Allowed F = X"
   32.71 +by (simp add: mk_total_program_def def_prg_Allowed) 
   32.72 +
   32.73  lemma def_UNION_ok_iff:
   32.74       "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
   32.75        ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
   32.76  by (auto simp add: ok_def safety_prop_Acts_iff)
   32.77  
   32.78 +text{*The union of two total programs is total.*}
   32.79 +lemma totalize_Join: "totalize F Join totalize G = totalize (F Join G)"
   32.80 +by (simp add: program_equalityI totalize_def Join_def image_Un)
   32.81 +
   32.82 +lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F Join G)"
   32.83 +by (simp add: all_total_def, blast)
   32.84 +
   32.85 +lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)"
   32.86 +by (simp add: program_equalityI totalize_def JOIN_def image_UN)
   32.87 +
   32.88 +lemma all_total_JN: "(!!i. i\<in>I ==> all_total (F i)) ==> all_total(\<Squnion>i\<in>I. F i)"
   32.89 +by (simp add: all_total_iff_totalize totalize_JN [symmetric])
   32.90 +
   32.91  end
    33.1 --- a/src/HOL/UNITY/WFair.thy	Sat Feb 08 14:46:22 2003 +0100
    33.2 +++ b/src/HOL/UNITY/WFair.thy	Sat Feb 08 16:05:33 2003 +0100
    33.3 @@ -3,21 +3,44 @@
    33.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    33.5      Copyright   1998  University of Cambridge
    33.6  
    33.7 -Weak Fairness versions of transient, ensures, leadsTo.
    33.8 +Conditional Fairness versions of transient, ensures, leadsTo.
    33.9  
   33.10  From Misra, "A Logic for Concurrent Programming", 1994
   33.11  *)
   33.12  
   33.13 -header{*Progress under Weak Fairness*}
   33.14 +header{*Progress*}
   33.15  
   33.16  theory WFair = UNITY:
   33.17  
   33.18 +text{*The original version of this theory was based on weak fairness.  (Thus,
   33.19 +the entire UNITY development embodied this assumption, until February 2003.)
   33.20 +Weak fairness states that if a command is enabled continuously, then it is
   33.21 +eventually executed.  Ernie Cohen suggested that I instead adopt unconditional
   33.22 +fairness: every command is executed infinitely often.  
   33.23 +
   33.24 +In fact, Misra's paper on "Progress" seems to be ambiguous about the correct
   33.25 +interpretation, and says that the two forms of fairness are equivalent.  They
   33.26 +differ only on their treatment of partial transitions, which under
   33.27 +unconditional fairness behave magically.  That is because if there are partial
   33.28 +transitions then there may be no fair executions, making all leads-to
   33.29 +properties hold vacuously.
   33.30 +
   33.31 +Unconditional fairness has some great advantages.  By distinguishing partial
   33.32 +transitions from total ones that are the identity on part of their domain, it
   33.33 +is more expressive.  Also, by simplifying the definition of the transient
   33.34 +property, it simplifies many proofs.  A drawback is that some laws only hold
   33.35 +under the assumption that all transitions are total.  The best-known of these
   33.36 +is the impossibility law for leads-to.
   33.37 +*}
   33.38 +
   33.39  constdefs
   33.40  
   33.41 -  (*This definition specifies weak fairness.  The rest of the theory
   33.42 -    is generic to all forms of fairness.*)
   33.43 +  --{*This definition specifies conditional fairness.  The rest of the theory
   33.44 +      is generic to all forms of fairness.  To get weak fairness, conjoin
   33.45 +      the inclusion below with @{term "A \<subseteq> Domain act"}, which specifies 
   33.46 +      that the action is enabled over all of @{term A}.*}
   33.47    transient :: "'a set => 'a program set"
   33.48 -    "transient A == {F. \<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A}"
   33.49 +    "transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}"
   33.50  
   33.51    ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60)
   33.52      "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
   33.53 @@ -25,8 +48,8 @@
   33.54  
   33.55  consts
   33.56  
   33.57 -  (*LEADS-TO constant for the inductive definition*)
   33.58    leads :: "'a program => ('a set * 'a set) set"
   33.59 +    --{*LEADS-TO constant for the inductive definition*}
   33.60  
   33.61  
   33.62  inductive "leads F"
   33.63 @@ -41,12 +64,12 @@
   33.64  
   33.65  constdefs
   33.66  
   33.67 -  (*visible version of the LEADS-TO relation*)
   33.68    leadsTo :: "['a set, 'a set] => 'a program set"    (infixl "leadsTo" 60)
   33.69 +     --{*visible version of the LEADS-TO relation*}
   33.70      "A leadsTo B == {F. (A,B) \<in> leads F}"
   33.71    
   33.72 -  (*wlt F B is the largest set that leads to B*)
   33.73    wlt :: "['a program, 'a set] => 'a set"
   33.74 +     --{*predicate transformer: the largest set that leads to @{term B}*}
   33.75      "wlt F B == Union {A. F \<in> A leadsTo B}"
   33.76  
   33.77  syntax (xsymbols)
   33.78 @@ -55,9 +78,17 @@
   33.79  
   33.80  subsection{*transient*}
   33.81  
   33.82 +lemma stable_transient: 
   33.83 +    "[| F \<in> stable A; F \<in> transient A |] ==> \<exists>act\<in>Acts F. A \<subseteq> - (Domain act)"
   33.84 +apply (simp add: stable_def constrains_def transient_def, clarify)
   33.85 +apply (rule rev_bexI, auto)  
   33.86 +done
   33.87 +
   33.88  lemma stable_transient_empty: 
   33.89 -    "[| F \<in> stable A; F \<in> transient A |] ==> A = {}"
   33.90 -by (unfold stable_def constrains_def transient_def, blast)
   33.91 +    "[| F \<in> stable A; F \<in> transient A; all_total F |] ==> A = {}"
   33.92 +apply (drule stable_transient, assumption)
   33.93 +apply (simp add: all_total_def)
   33.94 +done
   33.95  
   33.96  lemma transient_strengthen: 
   33.97      "[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B"
   33.98 @@ -66,22 +97,34 @@
   33.99  done
  33.100  
  33.101  lemma transientI: 
  33.102 -    "[| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] ==> F \<in> transient A"
  33.103 +    "[| act: Acts F;  act``A \<subseteq> -A |] ==> F \<in> transient A"
  33.104  by (unfold transient_def, blast)
  33.105  
  33.106  lemma transientE: 
  33.107      "[| F \<in> transient A;   
  33.108 -        !!act. [| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] ==> P |]  
  33.109 +        !!act. [| act: Acts F;  act``A \<subseteq> -A |] ==> P |]  
  33.110       ==> P"
  33.111  by (unfold transient_def, blast)
  33.112  
  33.113 -lemma transient_UNIV [simp]: "transient UNIV = {}"
  33.114 -by (unfold transient_def, blast)
  33.115 -
  33.116  lemma transient_empty [simp]: "transient {} = UNIV"
  33.117  by (unfold transient_def, auto)
  33.118  
  33.119  
  33.120 +text{*This equation recovers the notion of weak fairness.  A totalized
  33.121 +      program satisfies a transient assertion just if the original program
  33.122 +      contains a suitable action that is also enabled.*}
  33.123 +lemma totalize_transient_iff:
  33.124 +   "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
  33.125 +apply (simp add: totalize_def totalize_act_def transient_def 
  33.126 +                 Un_Image Un_subset_iff, safe)
  33.127 +apply (blast intro!: rev_bexI)+
  33.128 +done
  33.129 +
  33.130 +lemma totalize_transientI: 
  33.131 +    "[| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] 
  33.132 +     ==> totalize F \<in> transient A"
  33.133 +by (simp add: totalize_transient_iff, blast)
  33.134 +
  33.135  subsection{*ensures*}
  33.136  
  33.137  lemma ensuresI: 
  33.138 @@ -98,7 +141,7 @@
  33.139  apply (blast intro: constrains_weaken transient_strengthen)
  33.140  done
  33.141  
  33.142 -(*The L-version (precondition strengthening) fails, but we have this*)
  33.143 +text{*The L-version (precondition strengthening) fails, but we have this*}
  33.144  lemma stable_ensures_Int: 
  33.145      "[| F \<in> stable C;  F \<in> A ensures B |]    
  33.146      ==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
  33.147 @@ -134,7 +177,7 @@
  33.148  lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
  33.149  by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
  33.150  
  33.151 -(*Useful with cancellation, disjunction*)
  33.152 +text{*Useful with cancellation, disjunction*}
  33.153  lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
  33.154  by (simp add: Un_ac)
  33.155  
  33.156 @@ -142,7 +185,7 @@
  33.157       "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
  33.158  by (simp add: Un_ac)
  33.159  
  33.160 -(*The Union introduction rule as we should have liked to state it*)
  33.161 +text{*The Union introduction rule as we should have liked to state it*}
  33.162  lemma leadsTo_Union: 
  33.163      "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
  33.164  apply (unfold leadsTo_def)
  33.165 @@ -162,7 +205,7 @@
  33.166  apply (blast intro: leadsTo_Union)
  33.167  done
  33.168  
  33.169 -(*Binary union introduction rule*)
  33.170 +text{*Binary union introduction rule*}
  33.171  lemma leadsTo_Un:
  33.172       "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
  33.173  apply (subst Un_eq_Union)
  33.174 @@ -174,7 +217,7 @@
  33.175  by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
  33.176  
  33.177  
  33.178 -(*The INDUCTION rule as we should have liked to state it*)
  33.179 +text{*The INDUCTION rule as we should have liked to state it*}
  33.180  lemma leadsTo_induct: 
  33.181    "[| F \<in> za leadsTo zb;   
  33.182        !!A B. F \<in> A ensures B ==> P A B;  
  33.183 @@ -203,16 +246,16 @@
  33.184  
  33.185  (** Variant induction rule: on the preconditions for B **)
  33.186  
  33.187 -(*Lemma is the weak version: can't see how to do it in one step*)
  33.188 +text{*Lemma is the weak version: can't see how to do it in one step*}
  33.189  lemma leadsTo_induct_pre_lemma: 
  33.190    "[| F \<in> za leadsTo zb;   
  33.191        P zb;  
  33.192        !!A B. [| F \<in> A ensures B;  P B |] ==> P A;  
  33.193        !!S. \<forall>A \<in> S. P A ==> P (Union S)  
  33.194     |] ==> P za"
  33.195 -(*by induction on this formula*)
  33.196 +txt{*by induction on this formula*}
  33.197  apply (subgoal_tac "P zb --> P za")
  33.198 -(*now solve first subgoal: this formula is sufficient*)
  33.199 +txt{*now solve first subgoal: this formula is sufficient*}
  33.200  apply (blast intro: leadsTo_refl)
  33.201  apply (erule leadsTo_induct)
  33.202  apply (blast+)
  33.203 @@ -240,7 +283,7 @@
  33.204       "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
  33.205  by (blast intro: leadsTo_Trans subset_imp_leadsTo)
  33.206  
  33.207 -(*Distributes over binary unions*)
  33.208 +text{*Distributes over binary unions*}
  33.209  lemma leadsTo_Un_distrib:
  33.210       "F \<in> (A \<union> B) leadsTo C  =  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
  33.211  by (blast intro: leadsTo_Un leadsTo_weaken_L)
  33.212 @@ -271,7 +314,7 @@
  33.213  apply (blast intro: leadsTo_Union leadsTo_weaken_R)
  33.214  done
  33.215  
  33.216 -(*Binary union version*)
  33.217 +text{*Binary union version*}
  33.218  lemma leadsTo_Un_Un:
  33.219       "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]  
  33.220        ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
  33.221 @@ -309,18 +352,17 @@
  33.222  done
  33.223  
  33.224  
  33.225 -
  33.226 -(** The impossibility law **)
  33.227 -
  33.228 -lemma leadsTo_empty: "F \<in> A leadsTo {} ==> A={}"
  33.229 +text{*The impossibility law*}
  33.230 +lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
  33.231  apply (erule leadsTo_induct_pre)
  33.232 -apply (simp_all add: ensures_def constrains_def transient_def, blast)
  33.233 +apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
  33.234 +apply (drule bspec, assumption)+
  33.235 +apply blast
  33.236  done
  33.237  
  33.238 +subsection{*PSP: Progress-Safety-Progress*}
  33.239  
  33.240 -(** PSP: Progress-Safety-Progress **)
  33.241 -
  33.242 -(*Special case of PSP: Misra's "stable conjunction"*)
  33.243 +text{*Special case of PSP: Misra's "stable conjunction"*}
  33.244  lemma psp_stable: 
  33.245     "[| F \<in> A leadsTo A'; F \<in> stable B |]  
  33.246      ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
  33.247 @@ -452,7 +494,7 @@
  33.248  
  33.249  subsection{*wlt*}
  33.250  
  33.251 -(*Misra's property W3*)
  33.252 +text{*Misra's property W3*}
  33.253  lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
  33.254  apply (unfold wlt_def)
  33.255  apply (blast intro!: leadsTo_Union)
  33.256 @@ -463,17 +505,17 @@
  33.257  apply (blast intro!: leadsTo_Union)
  33.258  done
  33.259  
  33.260 -(*Misra's property W2*)
  33.261 +text{*Misra's property W2*}
  33.262  lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
  33.263  by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
  33.264  
  33.265 -(*Misra's property W4*)
  33.266 +text{*Misra's property W4*}
  33.267  lemma wlt_increasing: "B \<subseteq> wlt F B"
  33.268  apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
  33.269  done
  33.270  
  33.271  
  33.272 -(*Used in the Trans case below*)
  33.273 +text{*Used in the Trans case below*}
  33.274  lemma lemma1: 
  33.275     "[| B \<subseteq> A2;   
  33.276         F \<in> (A1 - B) co (A1 \<union> B);  
  33.277 @@ -481,18 +523,18 @@
  33.278      ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
  33.279  by (unfold constrains_def, clarify,  blast)
  33.280  
  33.281 -(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
  33.282 +text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
  33.283  lemma leadsTo_123:
  33.284       "F \<in> A leadsTo A'  
  33.285        ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
  33.286  apply (erule leadsTo_induct)
  33.287 -(*Basis*)
  33.288 -apply (blast dest: ensuresD)
  33.289 -(*Trans*)
  33.290 -apply clarify
  33.291 -apply (rule_tac x = "Ba \<union> Bb" in exI)
  33.292 -apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
  33.293 -(*Union*)
  33.294 +  txt{*Basis*}
  33.295 +  apply (blast dest: ensuresD)
  33.296 + txt{*Trans*}
  33.297 + apply clarify
  33.298 + apply (rule_tac x = "Ba \<union> Bb" in exI)
  33.299 + apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
  33.300 +txt{*Union*}
  33.301  apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
  33.302  apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
  33.303  apply (auto intro: leadsTo_UN)
  33.304 @@ -502,7 +544,7 @@
  33.305  done
  33.306  
  33.307  
  33.308 -(*Misra's property W5*)
  33.309 +text{*Misra's property W5*}
  33.310  lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
  33.311  proof -
  33.312    from wlt_leadsTo [of F B, THEN leadsTo_123]