misc cleanup of ML bindings (for multihreading);
authorwenzelm
Fri Aug 03 20:19:41 2007 +0200 (2007-08-03)
changeset 24147edc90be09ac1
parent 24146 e4fbf438376d
child 24148 2d4ee876c215
misc cleanup of ML bindings (for multihreading);
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/UNITY/Project.thy
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/UNITY/UNITY_tactics.ML
     1.1 --- a/src/HOL/UNITY/Comp.thy	Fri Aug 03 16:28:25 2007 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Fri Aug 03 20:19:41 2007 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4  by (auto intro: safety_prop_INTER1 simp add: preserves_def)
     1.5  
     1.6  
     1.7 -(** Some lemmas used only in Client.ML **)
     1.8 +(** Some lemmas used only in Client.thy **)
     1.9  
    1.10  lemma stable_localTo_stable2:
    1.11       "[| F \<in> stable {s. P (v s) (w s)};
     2.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Fri Aug 03 16:28:25 2007 +0200
     2.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri Aug 03 20:19:41 2007 +0200
     2.3 @@ -30,7 +30,7 @@
     2.4    client_map :: "'a clientState_d => clientState*'a"
     2.5      "client_map == funPair non_dummy dummy"
     2.6  
     2.7 -  
     2.8 +
     2.9  record allocState =
    2.10    allocGiv :: "nat => nat list"   --{*OUTPUT history: source of "giv" for i*}
    2.11    allocAsk :: "nat => nat list"   --{*INPUT: allocator's copy of "ask" for i*}
    2.12 @@ -59,9 +59,9 @@
    2.13    --{*spec (2)*}
    2.14    system_progress :: "'a systemState program set"
    2.15      "system_progress == INT i : lessThan Nclients.
    2.16 -			INT h. 
    2.17 -			  {s. h \<le> (ask o sub i o client)s} LeadsTo
    2.18 -			  {s. h pfixLe (giv o sub i o client) s}"
    2.19 +                        INT h.
    2.20 +                          {s. h \<le> (ask o sub i o client)s} LeadsTo
    2.21 +                          {s. h pfixLe (giv o sub i o client) s}"
    2.22  
    2.23    system_spec :: "'a systemState program set"
    2.24      "system_spec == system_safety Int system_progress"
    2.25 @@ -81,9 +81,9 @@
    2.26    --{*spec (5)*}
    2.27    client_progress :: "'a clientState_d program set"
    2.28      "client_progress ==
    2.29 -	 Increasing giv  guarantees
    2.30 -	 (INT h. {s. h \<le> giv s & h pfixGe ask s}
    2.31 -		 LeadsTo {s. tokens h \<le> (tokens o rel) s})"
    2.32 +         Increasing giv  guarantees
    2.33 +         (INT h. {s. h \<le> giv s & h pfixGe ask s}
    2.34 +                 LeadsTo {s. tokens h \<le> (tokens o rel) s})"
    2.35  
    2.36    --{*spec: preserves part*}
    2.37    client_preserves :: "'a clientState_d program set"
    2.38 @@ -93,7 +93,7 @@
    2.39    client_allowed_acts :: "'a clientState_d program set"
    2.40      "client_allowed_acts ==
    2.41         {F. AllowedActs F =
    2.42 -	    insert Id (UNION (preserves (funPair rel ask)) Acts)}"
    2.43 +            insert Id (UNION (preserves (funPair rel ask)) Acts)}"
    2.44  
    2.45    client_spec :: "'a clientState_d program set"
    2.46      "client_spec == client_increasing Int client_bounded Int client_progress
    2.47 @@ -104,40 +104,40 @@
    2.48    --{*spec (6)*}
    2.49    alloc_increasing :: "'a allocState_d program set"
    2.50      "alloc_increasing ==
    2.51 -	 UNIV  guarantees
    2.52 -	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
    2.53 +         UNIV  guarantees
    2.54 +         (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
    2.55  
    2.56    --{*spec (7)*}
    2.57    alloc_safety :: "'a allocState_d program set"
    2.58      "alloc_safety ==
    2.59 -	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    2.60 +         (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    2.61           guarantees
    2.62 -	 Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
    2.63 +         Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
    2.64           \<le> NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
    2.65  
    2.66    --{*spec (8)*}
    2.67    alloc_progress :: "'a allocState_d program set"
    2.68      "alloc_progress ==
    2.69 -	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
    2.70 -	                             Increasing (sub i o allocRel))
    2.71 +         (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
    2.72 +                                     Increasing (sub i o allocRel))
    2.73           Int
    2.74           Always {s. ALL i<Nclients.
    2.75 -		     ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}
    2.76 +                     ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}
    2.77           Int
    2.78 -         (INT i : lessThan Nclients. 
    2.79 -	  INT h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
    2.80 -		 LeadsTo
    2.81 -	         {s. tokens h \<le> (tokens o sub i o allocRel)s})
    2.82 +         (INT i : lessThan Nclients.
    2.83 +          INT h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
    2.84 +                 LeadsTo
    2.85 +                 {s. tokens h \<le> (tokens o sub i o allocRel)s})
    2.86           guarantees
    2.87 -	     (INT i : lessThan Nclients.
    2.88 -	      INT h. {s. h \<le> (sub i o allocAsk) s}
    2.89 -	             LeadsTo
    2.90 -	             {s. h pfixLe (sub i o allocGiv) s})"
    2.91 +             (INT i : lessThan Nclients.
    2.92 +              INT h. {s. h \<le> (sub i o allocAsk) s}
    2.93 +                     LeadsTo
    2.94 +                     {s. h pfixLe (sub i o allocGiv) s})"
    2.95  
    2.96    (*NOTE: to follow the original paper, the formula above should have had
    2.97 -	INT h. {s. h i \<le> (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
    2.98 -	       LeadsTo
    2.99 -	       {s. tokens h i \<le> (tokens o sub i o allocRel)s})
   2.100 +        INT h. {s. h i \<le> (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
   2.101 +               LeadsTo
   2.102 +               {s. tokens h i \<le> (tokens o sub i o allocRel)s})
   2.103      thus h should have been a function variable.  However, only h i is ever
   2.104      looked at.*)
   2.105  
   2.106 @@ -145,12 +145,12 @@
   2.107    alloc_preserves :: "'a allocState_d program set"
   2.108      "alloc_preserves == preserves allocRel Int preserves allocAsk Int
   2.109                          preserves allocState_d.dummy"
   2.110 -  
   2.111 +
   2.112    --{*environmental constraints*}
   2.113    alloc_allowed_acts :: "'a allocState_d program set"
   2.114      "alloc_allowed_acts ==
   2.115         {F. AllowedActs F =
   2.116 -	    insert Id (UNION (preserves allocGiv) Acts)}"
   2.117 +            insert Id (UNION (preserves allocGiv) Acts)}"
   2.118  
   2.119    alloc_spec :: "'a allocState_d program set"
   2.120      "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
   2.121 @@ -161,22 +161,22 @@
   2.122    --{*spec (9.1)*}
   2.123    network_ask :: "'a systemState program set"
   2.124      "network_ask == INT i : lessThan Nclients.
   2.125 -			Increasing (ask o sub i o client)  guarantees
   2.126 -			((sub i o allocAsk) Fols (ask o sub i o client))"
   2.127 +                        Increasing (ask o sub i o client)  guarantees
   2.128 +                        ((sub i o allocAsk) Fols (ask o sub i o client))"
   2.129  
   2.130    --{*spec (9.2)*}
   2.131    network_giv :: "'a systemState program set"
   2.132      "network_giv == INT i : lessThan Nclients.
   2.133 -			Increasing (sub i o allocGiv)
   2.134 -			guarantees
   2.135 -			((giv o sub i o client) Fols (sub i o allocGiv))"
   2.136 +                        Increasing (sub i o allocGiv)
   2.137 +                        guarantees
   2.138 +                        ((giv o sub i o client) Fols (sub i o allocGiv))"
   2.139  
   2.140    --{*spec (9.3)*}
   2.141    network_rel :: "'a systemState program set"
   2.142      "network_rel == INT i : lessThan Nclients.
   2.143 -			Increasing (rel o sub i o client)
   2.144 -			guarantees
   2.145 -			((sub i o allocRel) Fols (rel o sub i o client))"
   2.146 +                        Increasing (rel o sub i o client)
   2.147 +                        guarantees
   2.148 +                        ((sub i o allocRel) Fols (rel o sub i o client))"
   2.149  
   2.150    --{*spec: preserves part*}
   2.151    network_preserves :: "'a systemState program set"
   2.152 @@ -184,15 +184,15 @@
   2.153         preserves allocGiv  Int
   2.154         (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
   2.155                                     preserves (ask o sub i o client))"
   2.156 -  
   2.157 +
   2.158    --{*environmental constraints*}
   2.159    network_allowed_acts :: "'a systemState program set"
   2.160      "network_allowed_acts ==
   2.161         {F. AllowedActs F =
   2.162             insert Id
   2.163 -	    (UNION (preserves allocRel Int
   2.164 -		    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
   2.165 -		  Acts)}"
   2.166 +            (UNION (preserves allocRel Int
   2.167 +                    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
   2.168 +                  Acts)}"
   2.169  
   2.170    network_spec :: "'a systemState program set"
   2.171      "network_spec == network_ask Int network_giv Int
   2.172 @@ -204,25 +204,25 @@
   2.173    sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
   2.174      "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
   2.175                         in (| allocGiv = allocGiv s,
   2.176 -			     allocAsk = allocAsk s,
   2.177 -			     allocRel = allocRel s,
   2.178 -			     client   = cl,
   2.179 -			     dummy    = xtr|)"
   2.180 +                             allocAsk = allocAsk s,
   2.181 +                             allocRel = allocRel s,
   2.182 +                             client   = cl,
   2.183 +                             dummy    = xtr|)"
   2.184  
   2.185  
   2.186    sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
   2.187      "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
   2.188 -			         allocAsk = allocAsk al,
   2.189 -			         allocRel = allocRel al,
   2.190 -			         client   = cl,
   2.191 -			         systemState.dummy = allocState_d.dummy al|)"
   2.192 +                                 allocAsk = allocAsk al,
   2.193 +                                 allocRel = allocRel al,
   2.194 +                                 client   = cl,
   2.195 +                                 systemState.dummy = allocState_d.dummy al|)"
   2.196  
   2.197 -consts 
   2.198 +consts
   2.199      Alloc   :: "'a allocState_d program"
   2.200      Client  :: "'a clientState_d program"
   2.201      Network :: "'a systemState program"
   2.202      System  :: "'a systemState program"
   2.203 -  
   2.204 +
   2.205  axioms
   2.206      Alloc:   "Alloc   : alloc_spec"
   2.207      Client:  "Client  : client_spec"
   2.208 @@ -232,12 +232,12 @@
   2.209      System_def:
   2.210        "System == rename sysOfAlloc Alloc Join Network Join
   2.211                   (rename sysOfClient
   2.212 -		  (plam x: lessThan Nclients. rename client_map Client))"
   2.213 +                  (plam x: lessThan Nclients. rename client_map Client))"
   2.214  
   2.215  
   2.216  (**
   2.217  locale System =
   2.218 -  fixes 
   2.219 +  fixes
   2.220      Alloc   :: 'a allocState_d program
   2.221      Client  :: 'a clientState_d program
   2.222      Network :: 'a systemState program
   2.223 @@ -255,7 +255,7 @@
   2.224                   Network
   2.225                   Join
   2.226                   (rename sysOfClient
   2.227 -		  (plam x: lessThan Nclients. rename client_map Client))"
   2.228 +                  (plam x: lessThan Nclients. rename client_map Client))"
   2.229  **)
   2.230  
   2.231  (*Perhaps equalities.ML shouldn't add this in the first place!*)
   2.232 @@ -287,62 +287,62 @@
   2.233    bij_image_Collect_eq
   2.234  
   2.235  ML {*
   2.236 -local
   2.237 -  val INT_D = thm "INT_D";
   2.238 -in
   2.239  (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
   2.240 -fun list_of_Int th = 
   2.241 +fun list_of_Int th =
   2.242      (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
   2.243      handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
   2.244 -    handle THM _ => (list_of_Int (th RS INT_D))
   2.245 +    handle THM _ => (list_of_Int (th RS @{thm INT_D}))
   2.246      handle THM _ => (list_of_Int (th RS bspec))
   2.247      handle THM _ => [th];
   2.248 -end;
   2.249  *}
   2.250  
   2.251  lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
   2.252  
   2.253 -ML {*
   2.254 -local
   2.255 -  val lessThanBspec = thm "lessThanBspec"
   2.256 +setup {*
   2.257 +let
   2.258 +  fun normalized th =
   2.259 +    normalized (th RS spec
   2.260 +      handle THM _ => th RS @{thm lessThanBspec}
   2.261 +      handle THM _ => th RS bspec
   2.262 +      handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
   2.263 +    handle THM _ => th;
   2.264  in
   2.265 -fun normalize th = 
   2.266 -     normalize (th RS spec
   2.267 -		handle THM _ => th RS lessThanBspec
   2.268 -		handle THM _ => th RS bspec
   2.269 -		handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
   2.270 -     handle THM _ => th
   2.271 +  Attrib.add_attributes [("normalized", Attrib.no_args (Thm.rule_attribute (K normalized)), "")]
   2.272  end
   2.273  *}
   2.274  
   2.275  (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
   2.276  ML {*
   2.277 -val record_auto_tac =
   2.278 -  auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper, 
   2.279 -    simpset() addsimps [thm "sysOfAlloc_def", thm "sysOfClient_def",
   2.280 -      thm "client_map_def", thm "non_dummy_def", thm "funPair_def", thm "o_apply", thm "Let_def"])
   2.281 +fun record_auto_tac (cs, ss) =
   2.282 +  auto_tac (cs addIs [ext] addSWrapper record_split_wrapper,
   2.283 +    ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
   2.284 +      @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
   2.285 +      @{thm o_apply}, @{thm Let_def}])
   2.286  *}
   2.287  
   2.288 +method_setup record_auto = {*
   2.289 +  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
   2.290 +*} ""
   2.291  
   2.292  lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   2.293    apply (unfold sysOfAlloc_def Let_def)
   2.294    apply (rule inj_onI)
   2.295 -  apply (tactic record_auto_tac)
   2.296 +  apply record_auto
   2.297    done
   2.298  
   2.299  text{*We need the inverse; also having it simplifies the proof of surjectivity*}
   2.300 -lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s =  
   2.301 -             (| allocGiv = allocGiv s,    
   2.302 -                allocAsk = allocAsk s,    
   2.303 -                allocRel = allocRel s,    
   2.304 +lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s =
   2.305 +             (| allocGiv = allocGiv s,
   2.306 +                allocAsk = allocAsk s,
   2.307 +                allocRel = allocRel s,
   2.308                  allocState_d.dummy = (client s, dummy s) |)"
   2.309    apply (rule inj_sysOfAlloc [THEN inv_f_eq])
   2.310 -  apply (tactic record_auto_tac)
   2.311 +  apply record_auto
   2.312    done
   2.313  
   2.314  lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
   2.315    apply (simp add: surj_iff expand_fun_eq o_apply)
   2.316 -  apply (tactic record_auto_tac)
   2.317 +  apply record_auto
   2.318    done
   2.319  
   2.320  lemma bij_sysOfAlloc [iff]: "bij sysOfAlloc"
   2.321 @@ -355,22 +355,22 @@
   2.322  lemma inj_sysOfClient [iff]: "inj sysOfClient"
   2.323    apply (unfold sysOfClient_def)
   2.324    apply (rule inj_onI)
   2.325 -  apply (tactic record_auto_tac)
   2.326 +  apply record_auto
   2.327    done
   2.328  
   2.329 -lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s =  
   2.330 -             (client s,  
   2.331 -              (| allocGiv = allocGiv s,  
   2.332 -                 allocAsk = allocAsk s,  
   2.333 -                 allocRel = allocRel s,  
   2.334 +lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s =
   2.335 +             (client s,
   2.336 +              (| allocGiv = allocGiv s,
   2.337 +                 allocAsk = allocAsk s,
   2.338 +                 allocRel = allocRel s,
   2.339                   allocState_d.dummy = systemState.dummy s|) )"
   2.340    apply (rule inj_sysOfClient [THEN inv_f_eq])
   2.341 -  apply (tactic record_auto_tac)
   2.342 +  apply record_auto
   2.343    done
   2.344  
   2.345  lemma surj_sysOfClient [iff]: "surj sysOfClient"
   2.346    apply (simp add: surj_iff expand_fun_eq o_apply)
   2.347 -  apply (tactic record_auto_tac)
   2.348 +  apply record_auto
   2.349    done
   2.350  
   2.351  lemma bij_sysOfClient [iff]: "bij sysOfClient"
   2.352 @@ -382,19 +382,19 @@
   2.353  
   2.354  lemma inj_client_map [iff]: "inj client_map"
   2.355    apply (unfold inj_on_def)
   2.356 -  apply (tactic record_auto_tac)
   2.357 +  apply record_auto
   2.358    done
   2.359  
   2.360 -lemma inv_client_map_eq [simp]: "!!s. inv client_map s =  
   2.361 -             (%(x,y).(|giv = giv x, ask = ask x, rel = rel x,  
   2.362 +lemma inv_client_map_eq [simp]: "!!s. inv client_map s =
   2.363 +             (%(x,y).(|giv = giv x, ask = ask x, rel = rel x,
   2.364                         clientState_d.dummy = y|)) s"
   2.365    apply (rule inj_client_map [THEN inv_f_eq])
   2.366 -  apply (tactic record_auto_tac)
   2.367 +  apply record_auto
   2.368    done
   2.369  
   2.370  lemma surj_client_map [iff]: "surj client_map"
   2.371    apply (simp add: surj_iff expand_fun_eq o_apply)
   2.372 -  apply (tactic record_auto_tac)
   2.373 +  apply record_auto
   2.374    done
   2.375  
   2.376  lemma bij_client_map [iff]: "bij client_map"
   2.377 @@ -424,28 +424,28 @@
   2.378  subsection{*o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]*}
   2.379  
   2.380  lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy "
   2.381 -  apply (tactic record_auto_tac)
   2.382 +  apply record_auto
   2.383    done
   2.384  
   2.385  ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs (thm "client_o_sysOfAlloc")) *}
   2.386  declare client_o_sysOfAlloc' [simp]
   2.387  
   2.388  lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
   2.389 -  apply (tactic record_auto_tac)
   2.390 +  apply record_auto
   2.391    done
   2.392  
   2.393  ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_sysOfAlloc_eq")) *}
   2.394  declare allocGiv_o_sysOfAlloc_eq' [simp]
   2.395  
   2.396  lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
   2.397 -  apply (tactic record_auto_tac)
   2.398 +  apply record_auto
   2.399    done
   2.400  
   2.401  ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_sysOfAlloc_eq")) *}
   2.402  declare allocAsk_o_sysOfAlloc_eq' [simp]
   2.403  
   2.404  lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
   2.405 -  apply (tactic record_auto_tac)
   2.406 +  apply record_auto
   2.407    done
   2.408  
   2.409  ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *}
   2.410 @@ -455,28 +455,28 @@
   2.411  subsection{* o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]*}
   2.412  
   2.413  lemma client_o_sysOfClient: "client o sysOfClient = fst"
   2.414 -  apply (tactic record_auto_tac)
   2.415 +  apply record_auto
   2.416    done
   2.417  
   2.418  ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs (thm "client_o_sysOfClient")) *}
   2.419  declare client_o_sysOfClient' [simp]
   2.420  
   2.421  lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
   2.422 -  apply (tactic record_auto_tac)
   2.423 +  apply record_auto
   2.424    done
   2.425  
   2.426  ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs (thm "allocGiv_o_sysOfClient_eq")) *}
   2.427  declare allocGiv_o_sysOfClient_eq' [simp]
   2.428  
   2.429  lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
   2.430 -  apply (tactic record_auto_tac)
   2.431 +  apply record_auto
   2.432    done
   2.433  
   2.434  ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs (thm "allocAsk_o_sysOfClient_eq")) *}
   2.435  declare allocAsk_o_sysOfClient_eq' [simp]
   2.436  
   2.437  lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
   2.438 -  apply (tactic record_auto_tac)
   2.439 +  apply record_auto
   2.440    done
   2.441  
   2.442  ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs (thm "allocRel_o_sysOfClient_eq")) *}
   2.443 @@ -503,7 +503,7 @@
   2.444  ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_inv_sysOfAlloc_eq")) *}
   2.445  declare allocRel_o_inv_sysOfAlloc_eq' [simp]
   2.446  
   2.447 -lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =  
   2.448 +lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
   2.449        rel o sub i o client"
   2.450    apply (simp add: o_def drop_map_def)
   2.451    done
   2.452 @@ -511,7 +511,7 @@
   2.453  ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs (thm "rel_inv_client_map_drop_map")) *}
   2.454  declare rel_inv_client_map_drop_map [simp]
   2.455  
   2.456 -lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =  
   2.457 +lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
   2.458        ask o sub i o client"
   2.459    apply (simp add: o_def drop_map_def)
   2.460    done
   2.461 @@ -519,17 +519,6 @@
   2.462  ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs (thm "ask_inv_client_map_drop_map")) *}
   2.463  declare ask_inv_client_map_drop_map [simp]
   2.464  
   2.465 -(**
   2.466 -Open_locale "System"
   2.467 -
   2.468 -val Alloc = thm "Alloc";
   2.469 -val Client = thm "Client";
   2.470 -val Network = thm "Network";
   2.471 -val System_def = thm "System_def";
   2.472 -
   2.473 -CANNOT use bind_thm: it puts the theorem into standard form, in effect
   2.474 -  exporting it from the locale
   2.475 -**)
   2.476  
   2.477  declare finite_lessThan [iff]
   2.478  
   2.479 @@ -541,9 +530,9 @@
   2.480  
   2.481  ML {*
   2.482  val [Client_Increasing_ask, Client_Increasing_rel,
   2.483 -     Client_Bounded, Client_Progress, Client_AllowedActs, 
   2.484 +     Client_Bounded, Client_Progress, Client_AllowedActs,
   2.485       Client_preserves_giv, Client_preserves_dummy] =
   2.486 -        thm "Client" |> simplify (simpset() addsimps (thms "client_spec_simps") )
   2.487 +        @{thm Client} |> simplify (@{simpset} addsimps @{thms client_spec_simps})
   2.488                 |> list_of_Int;
   2.489  
   2.490  bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
   2.491 @@ -571,9 +560,9 @@
   2.492  
   2.493  ML {*
   2.494  val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
   2.495 -     Network_preserves_allocGiv, Network_preserves_rel, 
   2.496 -     Network_preserves_ask]  =  
   2.497 -        thm "Network" |> simplify (simpset() addsimps (thms "network_spec_simps"))
   2.498 +     Network_preserves_allocGiv, Network_preserves_rel,
   2.499 +     Network_preserves_ask]  =
   2.500 +        @{thm Network} |> simplify (@{simpset} addsimps @{thms network_spec_simps})
   2.501                  |> list_of_Int;
   2.502  
   2.503  bind_thm ("Network_Ask", Network_Ask);
   2.504 @@ -602,9 +591,9 @@
   2.505  
   2.506  ML {*
   2.507  val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
   2.508 -     Alloc_preserves_allocRel, Alloc_preserves_allocAsk, 
   2.509 -     Alloc_preserves_dummy] = 
   2.510 -        thm "Alloc" |> simplify (simpset() addsimps (thms "alloc_spec_simps")) 
   2.511 +     Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
   2.512 +     Alloc_preserves_dummy] =
   2.513 +        @{thm Alloc} |> simplify (@{simpset} addsimps @{thms alloc_spec_simps})
   2.514                |> list_of_Int;
   2.515  
   2.516  bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
   2.517 @@ -617,10 +606,8 @@
   2.518  *}
   2.519  
   2.520  text{*Strip off the INT in the guarantees postcondition*}
   2.521 -ML
   2.522 -{*
   2.523 -bind_thm ("Alloc_Increasing", normalize Alloc_Increasing_0)
   2.524 -*}
   2.525 +
   2.526 +lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized]
   2.527  
   2.528  declare
   2.529    Alloc_preserves_allocRel [iff]
   2.530 @@ -630,20 +617,20 @@
   2.531  
   2.532  subsection{*Components Lemmas [MUST BE AUTOMATED]*}
   2.533  
   2.534 -lemma Network_component_System: "Network Join  
   2.535 -      ((rename sysOfClient  
   2.536 -        (plam x: (lessThan Nclients). rename client_map Client)) Join  
   2.537 -       rename sysOfAlloc Alloc)  
   2.538 +lemma Network_component_System: "Network Join
   2.539 +      ((rename sysOfClient
   2.540 +        (plam x: (lessThan Nclients). rename client_map Client)) Join
   2.541 +       rename sysOfAlloc Alloc)
   2.542        = System"
   2.543    by (simp add: System_def Join_ac)
   2.544  
   2.545 -lemma Client_component_System: "(rename sysOfClient  
   2.546 -       (plam x: (lessThan Nclients). rename client_map Client)) Join  
   2.547 +lemma Client_component_System: "(rename sysOfClient
   2.548 +       (plam x: (lessThan Nclients). rename client_map Client)) Join
   2.549        (Network Join rename sysOfAlloc Alloc)  =  System"
   2.550    by (simp add: System_def Join_ac)
   2.551  
   2.552 -lemma Alloc_component_System: "rename sysOfAlloc Alloc Join  
   2.553 -       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join  
   2.554 +lemma Alloc_component_System: "rename sysOfAlloc Alloc Join
   2.555 +       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join
   2.556          Network)  =  System"
   2.557    by (simp add: System_def Join_ac)
   2.558  
   2.559 @@ -658,8 +645,8 @@
   2.560  lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask"
   2.561    by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff)
   2.562  
   2.563 -lemma Network_Allowed [simp]: "Allowed Network =         
   2.564 -        preserves allocRel Int  
   2.565 +lemma Network_Allowed [simp]: "Allowed Network =
   2.566 +        preserves allocRel Int
   2.567          (INT i: lessThan Nclients. preserves(giv o sub i o client))"
   2.568    by (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff)
   2.569  
   2.570 @@ -677,14 +664,14 @@
   2.571  
   2.572  lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
   2.573  apply (insert fst_o_lift_map [of i])
   2.574 -apply (drule fun_cong [where x=x])  
   2.575 +apply (drule fun_cong [where x=x])
   2.576  apply (simp add: o_def);
   2.577  done
   2.578  
   2.579  lemma fst_o_lift_map' [simp]:
   2.580       "(f \<circ> sub i \<circ> fst \<circ> lift_map i \<circ> g) = f o fst o g"
   2.581 -apply (subst fst_o_lift_map [symmetric]) 
   2.582 -apply (simp only: o_assoc) 
   2.583 +apply (subst fst_o_lift_map [symmetric])
   2.584 +apply (simp only: o_assoc)
   2.585  done
   2.586  
   2.587  
   2.588 @@ -697,8 +684,8 @@
   2.589    RS (lift_lift_guarantees_eq RS iffD2)
   2.590    RS guarantees_PLam_I
   2.591    RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
   2.592 -  |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def, 
   2.593 -				   surj_rename RS surj_range])
   2.594 +  |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
   2.595 +                                   surj_rename RS surj_range])
   2.596  
   2.597  However, the "preserves" property remains to be discharged, and the unfolding
   2.598  of "o" and "sub" complicates subsequent reasoning.
   2.599 @@ -708,41 +695,46 @@
   2.600  *)
   2.601  ML
   2.602  {*
   2.603 -val rename_client_map_tac =
   2.604 +fun rename_client_map_tac ss =
   2.605    EVERY [
   2.606 -    simp_tac (simpset() addsimps [thm "rename_guarantees_eq_rename_inv"]) 1,
   2.607 -    rtac (thm "guarantees_PLam_I") 1,
   2.608 +    simp_tac (ss addsimps [thm "rename_guarantees_eq_rename_inv"]) 1,
   2.609 +    rtac @{thm guarantees_PLam_I} 1,
   2.610      assume_tac 2,
   2.611 -	 (*preserves: routine reasoning*)
   2.612 -    asm_simp_tac (simpset() addsimps [thm "lift_preserves_sub"]) 2,
   2.613 -	 (*the guarantee for  "lift i (rename client_map Client)" *)
   2.614 +         (*preserves: routine reasoning*)
   2.615 +    asm_simp_tac (ss addsimps [@{thm lift_preserves_sub}]) 2,
   2.616 +         (*the guarantee for  "lift i (rename client_map Client)" *)
   2.617      asm_simp_tac
   2.618 -	(simpset() addsimps [thm "lift_guarantees_eq_lift_inv",
   2.619 -			     thm "rename_guarantees_eq_rename_inv",
   2.620 -			     thm "bij_imp_bij_inv", thm "surj_rename" RS thm "surj_range",
   2.621 -			     thm "inv_inv_eq"]) 1,
   2.622 +        (ss addsimps [@{thm lift_guarantees_eq_lift_inv},
   2.623 +                      @{thm rename_guarantees_eq_rename_inv},
   2.624 +                      @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
   2.625 +                      @{thm inv_inv_eq}]) 1,
   2.626      asm_simp_tac
   2.627 -        (simpset() addsimps [thm "o_def", thm "non_dummy_def", thm "guarantees_Int_right"]) 1]
   2.628 +        (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
   2.629  *}
   2.630  
   2.631 +method_setup rename_client_map = {*
   2.632 +  Method.ctxt_args (fn ctxt =>
   2.633 +    Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
   2.634 +*} ""
   2.635 +
   2.636  text{*Lifting @{text Client_Increasing} to @{term systemState}*}
   2.637 -lemma rename_Client_Increasing: "i : I  
   2.638 -      ==> rename sysOfClient (plam x: I. rename client_map Client) :  
   2.639 -            UNIV  guarantees   
   2.640 -            Increasing (ask o sub i o client) Int  
   2.641 +lemma rename_Client_Increasing: "i : I
   2.642 +      ==> rename sysOfClient (plam x: I. rename client_map Client) :
   2.643 +            UNIV  guarantees
   2.644 +            Increasing (ask o sub i o client) Int
   2.645              Increasing (rel o sub i o client)"
   2.646 -  by (tactic rename_client_map_tac)
   2.647 +  by rename_client_map
   2.648  
   2.649 -lemma preserves_sub_fst_lift_map: "[| F : preserves w; i ~= j |]  
   2.650 +lemma preserves_sub_fst_lift_map: "[| F : preserves w; i ~= j |]
   2.651        ==> F : preserves (sub i o fst o lift_map j o funPair v w)"
   2.652    apply (auto simp add: lift_map_def split_def linorder_neq_iff o_def)
   2.653    apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
   2.654    apply (auto simp add: o_def)
   2.655    done
   2.656  
   2.657 -lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |]  
   2.658 +lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |]
   2.659        ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)"
   2.660 -  apply (case_tac "i=j") 
   2.661 +  apply (case_tac "i=j")
   2.662    apply (simp, simp add: o_def non_dummy_def)
   2.663    apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map])
   2.664    apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
   2.665 @@ -750,12 +742,12 @@
   2.666    done
   2.667  
   2.668  lemma rename_sysOfClient_ok_Network:
   2.669 -  "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) 
   2.670 +  "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)
   2.671      ok Network"
   2.672    by (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map)
   2.673  
   2.674  lemma rename_sysOfClient_ok_Alloc:
   2.675 -  "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) 
   2.676 +  "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)
   2.677      ok rename sysOfAlloc Alloc"
   2.678    by (simp add: ok_iff_Allowed)
   2.679  
   2.680 @@ -767,7 +759,7 @@
   2.681    rename_sysOfClient_ok_Alloc [iff]
   2.682    rename_sysOfAlloc_ok_Network [iff]
   2.683  
   2.684 -text{*The "ok" laws, re-oriented. 
   2.685 +text{*The "ok" laws, re-oriented.
   2.686    But not sure this works: theorem @{text ok_commute} is needed below*}
   2.687  declare
   2.688    rename_sysOfClient_ok_Network [THEN ok_sym, iff]
   2.689 @@ -775,7 +767,7 @@
   2.690    rename_sysOfAlloc_ok_Network [THEN ok_sym]
   2.691  
   2.692  lemma System_Increasing: "i < Nclients
   2.693 -      ==> System : Increasing (ask o sub i o client) Int  
   2.694 +      ==> System : Increasing (ask o sub i o client) Int
   2.695                     Increasing (rel o sub i o client)"
   2.696    apply (rule component_guaranteesD [OF rename_Client_Increasing Client_component_System])
   2.697    apply auto
   2.698 @@ -788,12 +780,12 @@
   2.699  (*Lifting Alloc_Increasing up to the level of systemState*)
   2.700  lemmas rename_Alloc_Increasing =
   2.701    Alloc_Increasing
   2.702 -    [THEN rename_guarantees_sysOfAlloc_I, 
   2.703 -     simplified surj_rename [THEN surj_range] o_def sub_apply 
   2.704 -                rename_image_Increasing bij_sysOfAlloc 
   2.705 +    [THEN rename_guarantees_sysOfAlloc_I,
   2.706 +     simplified surj_rename [THEN surj_range] o_def sub_apply
   2.707 +                rename_image_Increasing bij_sysOfAlloc
   2.708                  allocGiv_o_inv_sysOfAlloc_eq'];
   2.709  
   2.710 -lemma System_Increasing_allocGiv: 
   2.711 +lemma System_Increasing_allocGiv:
   2.712       "i < Nclients ==> System : Increasing (sub i o allocGiv)"
   2.713    apply (unfold System_def)
   2.714    apply (simp add: o_def)
   2.715 @@ -812,19 +804,19 @@
   2.716      The "Always (INT ...) formulation expresses the general safety property
   2.717      and allows it to be combined using @{text Always_Int_rule} below. *}
   2.718  
   2.719 -lemma System_Follows_rel: 
   2.720 +lemma System_Follows_rel:
   2.721    "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))"
   2.722    apply (auto intro!: Network_Rel [THEN component_guaranteesD])
   2.723 -  apply (simp add: ok_commute [of Network]) 
   2.724 +  apply (simp add: ok_commute [of Network])
   2.725    done
   2.726  
   2.727 -lemma System_Follows_ask: 
   2.728 +lemma System_Follows_ask:
   2.729    "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))"
   2.730    apply (auto intro!: Network_Ask [THEN component_guaranteesD])
   2.731 -  apply (simp add: ok_commute [of Network]) 
   2.732 +  apply (simp add: ok_commute [of Network])
   2.733    done
   2.734  
   2.735 -lemma System_Follows_allocGiv: 
   2.736 +lemma System_Follows_allocGiv:
   2.737    "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)"
   2.738    apply (auto intro!: Network_Giv [THEN component_guaranteesD]
   2.739      rename_Alloc_Increasing [THEN component_guaranteesD])
   2.740 @@ -833,21 +825,21 @@
   2.741    done
   2.742  
   2.743  
   2.744 -lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.  
   2.745 +lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
   2.746                         {s. (giv o sub i o client) s \<le> (sub i o allocGiv) s})"
   2.747    apply auto
   2.748    apply (erule System_Follows_allocGiv [THEN Follows_Bounded])
   2.749    done
   2.750  
   2.751  
   2.752 -lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients.  
   2.753 +lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients.
   2.754                         {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s})"
   2.755    apply auto
   2.756    apply (erule System_Follows_ask [THEN Follows_Bounded])
   2.757    done
   2.758  
   2.759  
   2.760 -lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.  
   2.761 +lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.
   2.762                         {s. (sub i o allocRel) s \<le> (rel o sub i o client) s})"
   2.763    by (auto intro!: Follows_Bounded System_Follows_rel)
   2.764  
   2.765 @@ -865,27 +857,27 @@
   2.766    gets rid of the other "o"s too.*)
   2.767  
   2.768  text{*safety (1), step 3*}
   2.769 -lemma System_sum_bounded: 
   2.770 +lemma System_sum_bounded:
   2.771      "System : Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s)
   2.772              \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
   2.773    apply (simp add: o_apply)
   2.774 -  apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])   
   2.775 -  apply (simp add: o_def); 
   2.776 -  apply (erule component_guaranteesD) 
   2.777 +  apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
   2.778 +  apply (simp add: o_def);
   2.779 +  apply (erule component_guaranteesD)
   2.780    apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
   2.781    done
   2.782  
   2.783  text{* Follows reasoning*}
   2.784  
   2.785 -lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.  
   2.786 -                          {s. (tokens o giv o sub i o client) s  
   2.787 +lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
   2.788 +                          {s. (tokens o giv o sub i o client) s
   2.789                             \<le> (tokens o sub i o allocGiv) s})"
   2.790    apply (rule Always_giv_le_allocGiv [THEN Always_weaken])
   2.791    apply (auto intro: tokens_mono_prefix simp add: o_apply)
   2.792    done
   2.793  
   2.794 -lemma Always_tokens_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.  
   2.795 -                          {s. (tokens o sub i o allocRel) s  
   2.796 +lemma Always_tokens_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.
   2.797 +                          {s. (tokens o sub i o allocRel) s
   2.798                             \<le> (tokens o rel o sub i o client) s})"
   2.799    apply (rule Always_allocRel_le_rel [THEN Always_weaken])
   2.800    apply (auto intro: tokens_mono_prefix simp add: o_apply)
   2.801 @@ -915,15 +907,15 @@
   2.802  lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1, standard]
   2.803  
   2.804  text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
   2.805 -lemma rename_Client_Bounded: "i : I  
   2.806 -    ==> rename sysOfClient (plam x: I. rename client_map Client) :  
   2.807 -          UNIV  guarantees   
   2.808 +lemma rename_Client_Bounded: "i : I
   2.809 +    ==> rename sysOfClient (plam x: I. rename client_map Client) :
   2.810 +          UNIV  guarantees
   2.811            Always {s. ALL elt : set ((ask o sub i o client) s). elt \<le> NbT}"
   2.812 -  by (tactic rename_client_map_tac)
   2.813 +  by rename_client_map
   2.814  
   2.815  
   2.816 -lemma System_Bounded_ask: "i < Nclients  
   2.817 -      ==> System : Always  
   2.818 +lemma System_Bounded_ask: "i < Nclients
   2.819 +      ==> System : Always
   2.820                      {s. ALL elt : set ((ask o sub i o client) s). elt \<le> NbT}"
   2.821    apply (rule component_guaranteesD [OF rename_Client_Bounded Client_component_System])
   2.822    apply auto
   2.823 @@ -934,7 +926,7 @@
   2.824    done
   2.825  
   2.826  text{*progress (2), step 4*}
   2.827 -lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.  
   2.828 +lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
   2.829                            ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}"
   2.830    apply (auto simp add: Collect_all_imp_eq)
   2.831    apply (tactic {* rtac (Always_Int_rule [thm "Always_allocAsk_le_ask",
   2.832 @@ -949,23 +941,23 @@
   2.833  lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1, standard]
   2.834  
   2.835  
   2.836 -lemma rename_Client_Progress: "i: I  
   2.837 -   ==> rename sysOfClient (plam x: I. rename client_map Client)  
   2.838 -        : Increasing (giv o sub i o client)   
   2.839 -          guarantees  
   2.840 -          (INT h. {s. h \<le> (giv o sub i o client) s &  
   2.841 -                            h pfixGe (ask o sub i o client) s}   
   2.842 +lemma rename_Client_Progress: "i: I
   2.843 +   ==> rename sysOfClient (plam x: I. rename client_map Client)
   2.844 +        : Increasing (giv o sub i o client)
   2.845 +          guarantees
   2.846 +          (INT h. {s. h \<le> (giv o sub i o client) s &
   2.847 +                            h pfixGe (ask o sub i o client) s}
   2.848                    LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
   2.849 -  apply (tactic rename_client_map_tac)
   2.850 +  apply rename_client_map
   2.851    apply (simp add: Client_Progress [simplified o_def])
   2.852    done
   2.853  
   2.854  
   2.855  text{*progress (2), step 7*}
   2.856 -lemma System_Client_Progress: 
   2.857 -  "System : (INT i : (lessThan Nclients).  
   2.858 -            INT h. {s. h \<le> (giv o sub i o client) s &  
   2.859 -                       h pfixGe (ask o sub i o client) s}   
   2.860 +lemma System_Client_Progress:
   2.861 +  "System : (INT i : (lessThan Nclients).
   2.862 +            INT h. {s. h \<le> (giv o sub i o client) s &
   2.863 +                       h pfixGe (ask o sub i o client) s}
   2.864                  LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
   2.865    apply (rule INT_I)
   2.866  (*Couldn't have just used Auto_tac since the "INT h" must be kept*)
   2.867 @@ -974,7 +966,7 @@
   2.868    done
   2.869  
   2.870  (*Concludes
   2.871 - System : {s. k \<le> (sub i o allocGiv) s} 
   2.872 + System : {s. k \<le> (sub i o allocGiv) s}
   2.873            LeadsTo
   2.874            {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s} Int
   2.875            {s. k \<le> (giv o sub i o client) s} *)
   2.876 @@ -985,17 +977,17 @@
   2.877  
   2.878  lemmas System_lemma2 =
   2.879    PSP_Stable [OF System_lemma1
   2.880 -	      System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]]
   2.881 +              System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]]
   2.882  
   2.883  
   2.884 -lemma System_lemma3: "i < Nclients  
   2.885 -      ==> System : {s. h \<le> (sub i o allocGiv) s &       
   2.886 -                       h pfixGe (sub i o allocAsk) s}    
   2.887 -                   LeadsTo   
   2.888 -                   {s. h \<le> (giv o sub i o client) s &   
   2.889 +lemma System_lemma3: "i < Nclients
   2.890 +      ==> System : {s. h \<le> (sub i o allocGiv) s &
   2.891 +                       h pfixGe (sub i o allocAsk) s}
   2.892 +                   LeadsTo
   2.893 +                   {s. h \<le> (giv o sub i o client) s &
   2.894                         h pfixGe (ask o sub i o client) s}"
   2.895    apply (rule single_LeadsTo_I)
   2.896 -  apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s" 
   2.897 +  apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s"
   2.898           in System_lemma2 [THEN LeadsTo_weaken])
   2.899    apply auto
   2.900    apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe)
   2.901 @@ -1003,9 +995,9 @@
   2.902  
   2.903  
   2.904  text{*progress (2), step 8: Client i's "release" action is visible system-wide*}
   2.905 -lemma System_Alloc_Client_Progress: "i < Nclients   
   2.906 -      ==> System : {s. h \<le> (sub i o allocGiv) s &  
   2.907 -                       h pfixGe (sub i o allocAsk) s}   
   2.908 +lemma System_Alloc_Client_Progress: "i < Nclients
   2.909 +      ==> System : {s. h \<le> (sub i o allocGiv) s &
   2.910 +                       h pfixGe (sub i o allocAsk) s}
   2.911                     LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel) s}"
   2.912    apply (rule LeadsTo_Trans)
   2.913     prefer 2
   2.914 @@ -1023,15 +1015,15 @@
   2.915  text{*Lifting @{text Alloc_Progress} up to the level of systemState*}
   2.916  
   2.917  text{*progress (2), step 9*}
   2.918 -lemma System_Alloc_Progress: 
   2.919 - "System : (INT i : (lessThan Nclients).  
   2.920 -            INT h. {s. h \<le> (sub i o allocAsk) s}   
   2.921 +lemma System_Alloc_Progress:
   2.922 + "System : (INT i : (lessThan Nclients).
   2.923 +            INT h. {s. h \<le> (sub i o allocAsk) s}
   2.924                     LeadsTo {s. h pfixLe (sub i o allocGiv) s})"
   2.925    apply (simp only: o_apply sub_def)
   2.926 -  apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I]) 
   2.927 -  apply (simp add: o_def del: Set.INT_iff); 
   2.928 +  apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I])
   2.929 +  apply (simp add: o_def del: Set.INT_iff);
   2.930    apply (erule component_guaranteesD)
   2.931 -  apply (auto simp add: 
   2.932 +  apply (auto simp add:
   2.933      System_Increasing_allocRel [simplified sub_apply o_def]
   2.934      System_Increasing_allocAsk [simplified sub_apply o_def]
   2.935      System_Bounded_allocAsk [simplified sub_apply o_def]
   2.936 @@ -1056,13 +1048,13 @@
   2.937  
   2.938  text{* Some obsolete lemmas *}
   2.939  
   2.940 -lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o  
   2.941 +lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o
   2.942                                (funPair giv (funPair ask rel))"
   2.943    apply (rule ext)
   2.944    apply (auto simp add: o_def non_dummy_def)
   2.945    done
   2.946  
   2.947 -lemma preserves_non_dummy_eq: "(preserves non_dummy) =  
   2.948 +lemma preserves_non_dummy_eq: "(preserves non_dummy) =
   2.949        (preserves rel Int preserves ask Int preserves giv)"
   2.950    apply (simp add: non_dummy_eq_o_funPair)
   2.951    apply auto
     3.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Fri Aug 03 16:28:25 2007 +0200
     3.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Aug 03 20:19:41 2007 +0200
     3.3 @@ -106,19 +106,4 @@
     3.4  apply (subst setsum_UN_disjoint, auto)
     3.5  done
     3.6  
     3.7 -ML
     3.8 -{*
     3.9 -val NbT_pos = thm "NbT_pos";
    3.10 -val setsum_fun_mono = thm "setsum_fun_mono";
    3.11 -val tokens_mono_prefix = thm "tokens_mono_prefix";
    3.12 -val mono_tokens = thm "mono_tokens";
    3.13 -val bag_of_append = thm "bag_of_append";
    3.14 -val mono_bag_of = thm "mono_bag_of";
    3.15 -val bag_of_sublist_lemma = thm "bag_of_sublist_lemma";
    3.16 -val bag_of_sublist = thm "bag_of_sublist";
    3.17 -val bag_of_sublist_Un_Int = thm "bag_of_sublist_Un_Int";
    3.18 -val bag_of_sublist_Un_disjoint = thm "bag_of_sublist_Un_disjoint";
    3.19 -val bag_of_sublist_UN_disjoint = thm "bag_of_sublist_UN_disjoint";
    3.20 -*}
    3.21 -
    3.22  end
     4.1 --- a/src/HOL/UNITY/Project.thy	Fri Aug 03 16:28:25 2007 +0200
     4.2 +++ b/src/HOL/UNITY/Project.thy	Fri Aug 03 20:19:41 2007 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/UNITY/Project.ML
     4.5 +(*  Title:      HOL/UNITY/Project.thy
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1999  University of Cambridge
     4.9 @@ -673,21 +673,4 @@
    4.10  apply (blast intro: project_LeadsTo_D)
    4.11  done
    4.12  
    4.13 -ML
    4.14 -{*
    4.15 -val projecting_Int = thm "projecting_Int";
    4.16 -val projecting_Un = thm "projecting_Un";
    4.17 -val projecting_INT = thm "projecting_INT";
    4.18 -val projecting_UN = thm "projecting_UN";
    4.19 -val projecting_weaken = thm "projecting_weaken";
    4.20 -val projecting_weaken_L = thm "projecting_weaken_L";
    4.21 -val extending_Int = thm "extending_Int";
    4.22 -val extending_Un = thm "extending_Un";
    4.23 -val extending_INT = thm "extending_INT";
    4.24 -val extending_UN = thm "extending_UN";
    4.25 -val extending_weaken = thm "extending_weaken";
    4.26 -val extending_weaken_L = thm "extending_weaken_L";
    4.27 -val projecting_UNIV = thm "projecting_UNIV";
    4.28 -*}
    4.29 -
    4.30  end
     5.1 --- a/src/HOL/UNITY/ROOT.ML	Fri Aug 03 16:28:25 2007 +0200
     5.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Aug 03 20:19:41 2007 +0200
     5.3 @@ -6,39 +6,44 @@
     5.4  Root file for UNITY proofs.
     5.5  *)
     5.6  
     5.7 -(*Basic meta-theory*)
     5.8 -time_use_thy "UNITY_Main";
     5.9 +(*Verifying security protocols using UNITY*)
    5.10 +no_document use_thy "../Auth/Public";
    5.11  
    5.12 -(*Simple examples: no composition*)
    5.13 -time_use_thy "Simple/Deadlock";
    5.14 -time_use_thy "Simple/Common";
    5.15 -time_use_thy "Simple/Network";
    5.16 -time_use_thy "Simple/Token";
    5.17 -time_use_thy "Simple/Channel";
    5.18 -time_use_thy "Simple/Lift";
    5.19 -time_use_thy "Simple/Mutex";
    5.20 -time_use_thy "Simple/Reach";
    5.21 -time_use_thy "Simple/Reachability";
    5.22 +use_thys [
    5.23 +  (*Basic meta-theory*)
    5.24 +  "UNITY_Main",
    5.25  
    5.26 -(*Verifying security protocols using UNITY*)
    5.27 -with_path "../Auth" (no_document use_thy) "Public";
    5.28 -with_path "../Auth" time_use_thy "Simple/NSP_Bad";
    5.29 +  (*Simple examples: no composition*)
    5.30 +  "Simple/Deadlock",
    5.31 +  "Simple/Common",
    5.32 +  "Simple/Network",
    5.33 +  "Simple/Token",
    5.34 +  "Simple/Channel",
    5.35 +  "Simple/Lift",
    5.36 +  "Simple/Mutex",
    5.37 +  "Simple/Reach",
    5.38 +  "Simple/Reachability",
    5.39  
    5.40 -(*Example of composition*)
    5.41 -time_use_thy "Comp/Handshake";
    5.42 +  (*Verifying security protocols using UNITY*)
    5.43 +  "Simple/NSP_Bad",
    5.44  
    5.45 -(*Universal properties examples*)
    5.46 -time_use_thy "Comp/Counter";
    5.47 -time_use_thy "Comp/Counterc";
    5.48 -time_use_thy "Comp/Priority";
    5.49 +  (*Example of composition*)
    5.50 +  "Comp/Handshake",
    5.51  
    5.52 -time_use_thy "Comp/TimerArray";
    5.53 +  (*Universal properties examples*)
    5.54 +  "Comp/Counter",
    5.55 +  "Comp/Counterc",
    5.56 +  "Comp/Priority",
    5.57 +
    5.58 +  "Comp/TimerArray",
    5.59 +
    5.60 +  (*obsolete*)
    5.61 +  "ELT"
    5.62 +];
    5.63  
    5.64  (*Allocator example*)
    5.65  (* FIXME some parts no longer work -- had been commented out for a long time *)
    5.66  setmp quick_and_dirty true
    5.67 -  time_use_thy "Comp/Alloc";
    5.68 -time_use_thy "Comp/AllocImpl";
    5.69 -time_use_thy "Comp/Client";
    5.70 +  use_thy "Comp/Alloc";
    5.71  
    5.72 -time_use_thy "ELT";  (*obsolete*)
    5.73 +use_thys ["Comp/AllocImpl", "Comp/Client"];
     6.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Aug 03 16:28:25 2007 +0200
     6.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Aug 03 20:19:41 2007 +0200
     6.3 @@ -3,8 +3,6 @@
     6.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.5      Copyright   1996  University of Cambridge
     6.6  
     6.7 -ML{*add_path "$ISABELLE_HOME/src/HOL/Auth"*}
     6.8 -
     6.9  Original file is ../Auth/NS_Public_Bad
    6.10  *)
    6.11  
    6.12 @@ -103,28 +101,25 @@
    6.13  
    6.14  text{*This ML code does the inductions directly.*}
    6.15  ML{*
    6.16 -val ns_constrainsI = thm "ns_constrainsI";
    6.17 -val impCE = thm "impCE";
    6.18 -
    6.19  fun ns_constrains_tac(cs,ss) i =
    6.20     SELECT_GOAL
    6.21 -      (EVERY [REPEAT (etac Always_ConstrainsI 1),
    6.22 -	      REPEAT (resolve_tac [StableI, stableI,
    6.23 -				   constrains_imp_Constrains] 1),
    6.24 -	      rtac ns_constrainsI 1,
    6.25 +      (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1),
    6.26 +	      REPEAT (resolve_tac [@{thm StableI}, @{thm stableI},
    6.27 +				   @{thm constrains_imp_Constrains}] 1),
    6.28 +	      rtac @{thm ns_constrainsI} 1,
    6.29  	      full_simp_tac ss 1,
    6.30  	      REPEAT (FIRSTGOAL (etac disjE)),
    6.31 -	      ALLGOALS (clarify_tac (cs delrules [impI,impCE])),
    6.32 +	      ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])),
    6.33  	      REPEAT (FIRSTGOAL analz_mono_contra_tac),
    6.34  	      ALLGOALS (asm_simp_tac ss)]) i;
    6.35  
    6.36  (*Tactic for proving secrecy theorems*)
    6.37  fun ns_induct_tac(cs,ss) =
    6.38    (SELECT_GOAL o EVERY)
    6.39 -     [rtac AlwaysI 1,
    6.40 +     [rtac @{thm AlwaysI} 1,
    6.41        force_tac (cs,ss) 1,
    6.42        (*"reachable" gets in here*)
    6.43 -      rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
    6.44 +      rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
    6.45        ns_constrains_tac(cs,ss) 1];
    6.46  *}
    6.47  
     7.1 --- a/src/HOL/UNITY/UNITY.thy	Fri Aug 03 16:28:25 2007 +0200
     7.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Aug 03 20:19:41 2007 +0200
     7.3 @@ -55,7 +55,7 @@
     7.4      "increasing f == \<Inter>z. stable {s. z \<le> f s}"
     7.5  
     7.6  
     7.7 -text{*Perhaps equalities.ML shouldn't add this in the first place!*}
     7.8 +text{*Perhaps HOL shouldn't add this in the first place!*}
     7.9  declare image_Collect [simp del]
    7.10  
    7.11  subsubsection{*The abstract type of programs*}
    7.12 @@ -346,7 +346,7 @@
    7.13  lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
    7.14  by blast
    7.15  
    7.16 -text{*Needed for WF reasoning in WFair.ML*}
    7.17 +text{*Needed for WF reasoning in WFair.thy*}
    7.18  
    7.19  lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
    7.20  by blast
     8.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Fri Aug 03 16:28:25 2007 +0200
     8.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Fri Aug 03 20:19:41 2007 +0200
     8.3 @@ -11,13 +11,13 @@
     8.4  
     8.5  method_setup safety = {*
     8.6      Method.ctxt_args (fn ctxt =>
     8.7 -        Method.SIMPLE_METHOD' (gen_constrains_tac (local_clasimpset_of ctxt))) *}
     8.8 +        Method.SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
     8.9      "for proving safety properties"
    8.10  
    8.11  method_setup ensures_tac = {*
    8.12      fn args => fn ctxt =>
    8.13          Method.goal_args' (Scan.lift Args.name)
    8.14 -           (gen_ensures_tac (local_clasimpset_of ctxt))
    8.15 +           (ensures_tac (local_clasimpset_of ctxt))
    8.16             args ctxt *}
    8.17      "for proving progress properties"
    8.18  
     9.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Fri Aug 03 16:28:25 2007 +0200
     9.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri Aug 03 20:19:41 2007 +0200
     9.3 @@ -3,803 +3,60 @@
     9.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.5      Copyright   2003  University of Cambridge
     9.6  
     9.7 -Specialized UNITY tactics, and ML bindings of theorems
     9.8 +Specialized UNITY tactics.
     9.9  *)
    9.10  
    9.11 -(*ListOrder*)
    9.12 -val Domain_def = thm "Domain_def";
    9.13 -val Le_def = thm "Le_def";
    9.14 -val Ge_def = thm "Ge_def";
    9.15 -val prefix_def = thm "prefix_def";
    9.16 -val Nil_genPrefix = thm "Nil_genPrefix";
    9.17 -val genPrefix_length_le = thm "genPrefix_length_le";
    9.18 -val cons_genPrefixE = thm "cons_genPrefixE";
    9.19 -val Cons_genPrefix_Cons = thm "Cons_genPrefix_Cons";
    9.20 -val refl_genPrefix = thm "refl_genPrefix";
    9.21 -val genPrefix_refl = thm "genPrefix_refl";
    9.22 -val genPrefix_mono = thm "genPrefix_mono";
    9.23 -val append_genPrefix = thm "append_genPrefix";
    9.24 -val genPrefix_trans_O = thm "genPrefix_trans_O";
    9.25 -val genPrefix_trans = thm "genPrefix_trans";
    9.26 -val prefix_genPrefix_trans = thm "prefix_genPrefix_trans";
    9.27 -val genPrefix_prefix_trans = thm "genPrefix_prefix_trans";
    9.28 -val trans_genPrefix = thm "trans_genPrefix";
    9.29 -val genPrefix_antisym = thm "genPrefix_antisym";
    9.30 -val antisym_genPrefix = thm "antisym_genPrefix";
    9.31 -val genPrefix_Nil = thm "genPrefix_Nil";
    9.32 -val same_genPrefix_genPrefix = thm "same_genPrefix_genPrefix";
    9.33 -val genPrefix_Cons = thm "genPrefix_Cons";
    9.34 -val genPrefix_take_append = thm "genPrefix_take_append";
    9.35 -val genPrefix_append_both = thm "genPrefix_append_both";
    9.36 -val append_cons_eq = thm "append_cons_eq";
    9.37 -val append_one_genPrefix = thm "append_one_genPrefix";
    9.38 -val genPrefix_imp_nth = thm "genPrefix_imp_nth";
    9.39 -val nth_imp_genPrefix = thm "nth_imp_genPrefix";
    9.40 -val genPrefix_iff_nth = thm "genPrefix_iff_nth";
    9.41 -val prefix_refl = thm "prefix_refl";
    9.42 -val prefix_trans = thm "prefix_trans";
    9.43 -val prefix_antisym = thm "prefix_antisym";
    9.44 -val prefix_less_le = thm "prefix_less_le";
    9.45 -val set_mono = thm "set_mono";
    9.46 -val Nil_prefix = thm "Nil_prefix";
    9.47 -val prefix_Nil = thm "prefix_Nil";
    9.48 -val Cons_prefix_Cons = thm "Cons_prefix_Cons";
    9.49 -val same_prefix_prefix = thm "same_prefix_prefix";
    9.50 -val append_prefix = thm "append_prefix";
    9.51 -val prefix_appendI = thm "prefix_appendI";
    9.52 -val prefix_Cons = thm "prefix_Cons";
    9.53 -val append_one_prefix = thm "append_one_prefix";
    9.54 -val prefix_length_le = thm "prefix_length_le";
    9.55 -val strict_prefix_length_less = thm "strict_prefix_length_less";
    9.56 -val mono_length = thm "mono_length";
    9.57 -val prefix_iff = thm "prefix_iff";
    9.58 -val prefix_snoc = thm "prefix_snoc";
    9.59 -val prefix_append_iff = thm "prefix_append_iff";
    9.60 -val common_prefix_linear = thm "common_prefix_linear";
    9.61 -val reflexive_Le = thm "reflexive_Le";
    9.62 -val antisym_Le = thm "antisym_Le";
    9.63 -val trans_Le = thm "trans_Le";
    9.64 -val pfixLe_refl = thm "pfixLe_refl";
    9.65 -val pfixLe_trans = thm "pfixLe_trans";
    9.66 -val pfixLe_antisym = thm "pfixLe_antisym";
    9.67 -val prefix_imp_pfixLe = thm "prefix_imp_pfixLe";
    9.68 -val reflexive_Ge = thm "reflexive_Ge";
    9.69 -val antisym_Ge = thm "antisym_Ge";
    9.70 -val trans_Ge = thm "trans_Ge";
    9.71 -val pfixGe_refl = thm "pfixGe_refl";
    9.72 -val pfixGe_trans = thm "pfixGe_trans";
    9.73 -val pfixGe_antisym = thm "pfixGe_antisym";
    9.74 -val prefix_imp_pfixGe = thm "prefix_imp_pfixGe";
    9.75 -
    9.76 -
    9.77 -(*UNITY*)
    9.78 -val mk_total_program_def = thm "mk_total_program_def";
    9.79 -val totalize_act_def = thm "totalize_act_def";
    9.80 -val constrains_def = thm "constrains_def";
    9.81 -val stable_def = thm "stable_def";
    9.82 -val invariant_def = thm "invariant_def";
    9.83 -val increasing_def = thm "increasing_def";
    9.84 -val Allowed_def = thm "Allowed_def";
    9.85 -val Id_in_Acts = thm "Id_in_Acts";
    9.86 -val insert_Id_Acts = thm "insert_Id_Acts";
    9.87 -val Id_in_AllowedActs = thm "Id_in_AllowedActs";
    9.88 -val insert_Id_AllowedActs = thm "insert_Id_AllowedActs";
    9.89 -val Init_eq = thm "Init_eq";
    9.90 -val Acts_eq = thm "Acts_eq";
    9.91 -val AllowedActs_eq = thm "AllowedActs_eq";
    9.92 -val surjective_mk_program = thm "surjective_mk_program";
    9.93 -val program_equalityI = thm "program_equalityI";
    9.94 -val program_equalityE = thm "program_equalityE";
    9.95 -val program_equality_iff = thm "program_equality_iff";
    9.96 -val def_prg_Init = thm "def_prg_Init";
    9.97 -val def_prg_Acts = thm "def_prg_Acts";
    9.98 -val def_prg_AllowedActs = thm "def_prg_AllowedActs";
    9.99 -val def_act_simp = thm "def_act_simp";
   9.100 -val def_set_simp = thm "def_set_simp";
   9.101 -val constrainsI = thm "constrainsI";
   9.102 -val constrainsD = thm "constrainsD";
   9.103 -val constrains_empty = thm "constrains_empty";
   9.104 -val constrains_empty2 = thm "constrains_empty2";
   9.105 -val constrains_UNIV = thm "constrains_UNIV";
   9.106 -val constrains_UNIV2 = thm "constrains_UNIV2";
   9.107 -val constrains_weaken_R = thm "constrains_weaken_R";
   9.108 -val constrains_weaken_L = thm "constrains_weaken_L";
   9.109 -val constrains_weaken = thm "constrains_weaken";
   9.110 -val constrains_Un = thm "constrains_Un";
   9.111 -val constrains_UN = thm "constrains_UN";
   9.112 -val constrains_Un_distrib = thm "constrains_Un_distrib";
   9.113 -val constrains_UN_distrib = thm "constrains_UN_distrib";
   9.114 -val constrains_Int_distrib = thm "constrains_Int_distrib";
   9.115 -val constrains_INT_distrib = thm "constrains_INT_distrib";
   9.116 -val constrains_Int = thm "constrains_Int";
   9.117 -val constrains_INT = thm "constrains_INT";
   9.118 -val constrains_imp_subset = thm "constrains_imp_subset";
   9.119 -val constrains_trans = thm "constrains_trans";
   9.120 -val constrains_cancel = thm "constrains_cancel";
   9.121 -val unlessI = thm "unlessI";
   9.122 -val unlessD = thm "unlessD";
   9.123 -val stableI = thm "stableI";
   9.124 -val stableD = thm "stableD";
   9.125 -val stable_UNIV = thm "stable_UNIV";
   9.126 -val stable_Un = thm "stable_Un";
   9.127 -val stable_UN = thm "stable_UN";
   9.128 -val stable_Int = thm "stable_Int";
   9.129 -val stable_INT = thm "stable_INT";
   9.130 -val stable_constrains_Un = thm "stable_constrains_Un";
   9.131 -val stable_constrains_Int = thm "stable_constrains_Int";
   9.132 -val stable_constrains_stable = thm "stable_constrains_stable";
   9.133 -val invariantI = thm "invariantI";
   9.134 -val invariant_Int = thm "invariant_Int";
   9.135 -val increasingD = thm "increasingD";
   9.136 -val increasing_constant = thm "increasing_constant";
   9.137 -val mono_increasing_o = thm "mono_increasing_o";
   9.138 -val strict_increasingD = thm "strict_increasingD";
   9.139 -val elimination = thm "elimination";
   9.140 -val elimination_sing = thm "elimination_sing";
   9.141 -val constrains_strongest_rhs = thm "constrains_strongest_rhs";
   9.142 -val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest";
   9.143 -val Un_Diff_Diff = thm "Un_Diff_Diff";
   9.144 -val Int_Union_Union = thm "Int_Union_Union";
   9.145 -val Image_less_than = thm "Image_less_than";
   9.146 -val Image_inverse_less_than = thm "Image_inverse_less_than";
   9.147 -val totalize_constrains_iff = thm "totalize_constrains_iff";
   9.148 -
   9.149 -(*WFair*)
   9.150 -val stable_transient_empty = thm "stable_transient_empty";
   9.151 -val transient_strengthen = thm "transient_strengthen";
   9.152 -val transientI = thm "transientI";
   9.153 -val totalize_transientI = thm "totalize_transientI";
   9.154 -val transientE = thm "transientE";
   9.155 -val transient_empty = thm "transient_empty";
   9.156 -val ensuresI = thm "ensuresI";
   9.157 -val ensuresD = thm "ensuresD";
   9.158 -val ensures_weaken_R = thm "ensures_weaken_R";
   9.159 -val stable_ensures_Int = thm "stable_ensures_Int";
   9.160 -val stable_transient_ensures = thm "stable_transient_ensures";
   9.161 -val ensures_eq = thm "ensures_eq";
   9.162 -val leadsTo_Basis = thm "leadsTo_Basis";
   9.163 -val leadsTo_Trans = thm "leadsTo_Trans";
   9.164 -val transient_imp_leadsTo = thm "transient_imp_leadsTo";
   9.165 -val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate";
   9.166 -val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2";
   9.167 -val leadsTo_Union = thm "leadsTo_Union";
   9.168 -val leadsTo_Union_Int = thm "leadsTo_Union_Int";
   9.169 -val leadsTo_UN = thm "leadsTo_UN";
   9.170 -val leadsTo_Un = thm "leadsTo_Un";
   9.171 -val single_leadsTo_I = thm "single_leadsTo_I";
   9.172 -val leadsTo_induct = thm "leadsTo_induct";
   9.173 -val subset_imp_ensures = thm "subset_imp_ensures";
   9.174 -val subset_imp_leadsTo = thm "subset_imp_leadsTo";
   9.175 -val leadsTo_refl = thm "leadsTo_refl";
   9.176 -val empty_leadsTo = thm "empty_leadsTo";
   9.177 -val leadsTo_UNIV = thm "leadsTo_UNIV";
   9.178 -val leadsTo_induct_pre = thm "leadsTo_induct_pre";
   9.179 -val leadsTo_weaken_R = thm "leadsTo_weaken_R";
   9.180 -val leadsTo_weaken_L = thm "leadsTo_weaken_L";
   9.181 -val leadsTo_Un_distrib = thm "leadsTo_Un_distrib";
   9.182 -val leadsTo_UN_distrib = thm "leadsTo_UN_distrib";
   9.183 -val leadsTo_Union_distrib = thm "leadsTo_Union_distrib";
   9.184 -val leadsTo_weaken = thm "leadsTo_weaken";
   9.185 -val leadsTo_Diff = thm "leadsTo_Diff";
   9.186 -val leadsTo_UN_UN = thm "leadsTo_UN_UN";
   9.187 -val leadsTo_Un_Un = thm "leadsTo_Un_Un";
   9.188 -val leadsTo_cancel2 = thm "leadsTo_cancel2";
   9.189 -val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2";
   9.190 -val leadsTo_cancel1 = thm "leadsTo_cancel1";
   9.191 -val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1";
   9.192 -val leadsTo_empty = thm "leadsTo_empty";
   9.193 -val psp_stable = thm "psp_stable";
   9.194 -val psp_stable2 = thm "psp_stable2";
   9.195 -val psp_ensures = thm "psp_ensures";
   9.196 -val psp = thm "psp";
   9.197 -val psp2 = thm "psp2";
   9.198 -val psp_unless = thm "psp_unless";
   9.199 -val leadsTo_wf_induct = thm "leadsTo_wf_induct";
   9.200 -val bounded_induct = thm "bounded_induct";
   9.201 -val lessThan_induct = thm "lessThan_induct";
   9.202 -val lessThan_bounded_induct = thm "lessThan_bounded_induct";
   9.203 -val greaterThan_bounded_induct = thm "greaterThan_bounded_induct";
   9.204 -val wlt_leadsTo = thm "wlt_leadsTo";
   9.205 -val leadsTo_subset = thm "leadsTo_subset";
   9.206 -val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt";
   9.207 -val wlt_increasing = thm "wlt_increasing";
   9.208 -val leadsTo_123 = thm "leadsTo_123";
   9.209 -val wlt_constrains_wlt = thm "wlt_constrains_wlt";
   9.210 -val completion = thm "completion";
   9.211 -val finite_completion = thm "finite_completion";
   9.212 -val stable_completion = thm "stable_completion";
   9.213 -val finite_stable_completion = thm "finite_stable_completion";
   9.214 -
   9.215 -(*Constrains*)
   9.216 -val Increasing_def = thm "Increasing_def";
   9.217 -val reachable_Init = thm "reachable.Init";
   9.218 -val reachable_Acts = thm "reachable.Acts";
   9.219 -val reachable_equiv_traces = thm "reachable_equiv_traces";
   9.220 -val Init_subset_reachable = thm "Init_subset_reachable";
   9.221 -val stable_reachable = thm "stable_reachable";
   9.222 -val invariant_reachable = thm "invariant_reachable";
   9.223 -val invariant_includes_reachable = thm "invariant_includes_reachable";
   9.224 -val constrains_reachable_Int = thm "constrains_reachable_Int";
   9.225 -val Constrains_eq_constrains = thm "Constrains_eq_constrains";
   9.226 -val constrains_imp_Constrains = thm "constrains_imp_Constrains";
   9.227 -val stable_imp_Stable = thm "stable_imp_Stable";
   9.228 -val ConstrainsI = thm "ConstrainsI";
   9.229 -val Constrains_empty = thm "Constrains_empty";
   9.230 -val Constrains_UNIV = thm "Constrains_UNIV";
   9.231 -val Constrains_weaken_R = thm "Constrains_weaken_R";
   9.232 -val Constrains_weaken_L = thm "Constrains_weaken_L";
   9.233 -val Constrains_weaken = thm "Constrains_weaken";
   9.234 -val Constrains_Un = thm "Constrains_Un";
   9.235 -val Constrains_UN = thm "Constrains_UN";
   9.236 -val Constrains_Int = thm "Constrains_Int";
   9.237 -val Constrains_INT = thm "Constrains_INT";
   9.238 -val Constrains_imp_subset = thm "Constrains_imp_subset";
   9.239 -val Constrains_trans = thm "Constrains_trans";
   9.240 -val Constrains_cancel = thm "Constrains_cancel";
   9.241 -val Stable_eq = thm "Stable_eq";
   9.242 -val Stable_eq_stable = thm "Stable_eq_stable";
   9.243 -val StableI = thm "StableI";
   9.244 -val StableD = thm "StableD";
   9.245 -val Stable_Un = thm "Stable_Un";
   9.246 -val Stable_Int = thm "Stable_Int";
   9.247 -val Stable_Constrains_Un = thm "Stable_Constrains_Un";
   9.248 -val Stable_Constrains_Int = thm "Stable_Constrains_Int";
   9.249 -val Stable_UN = thm "Stable_UN";
   9.250 -val Stable_INT = thm "Stable_INT";
   9.251 -val Stable_reachable = thm "Stable_reachable";
   9.252 -val IncreasingD = thm "IncreasingD";
   9.253 -val mono_Increasing_o = thm "mono_Increasing_o";
   9.254 -val strict_IncreasingD = thm "strict_IncreasingD";
   9.255 -val increasing_imp_Increasing = thm "increasing_imp_Increasing";
   9.256 -val Increasing_constant = thm "Increasing_constant";
   9.257 -val Elimination = thm "Elimination";
   9.258 -val Elimination_sing = thm "Elimination_sing";
   9.259 -val AlwaysI = thm "AlwaysI";
   9.260 -val AlwaysD = thm "AlwaysD";
   9.261 -val AlwaysE = thm "AlwaysE";
   9.262 -val Always_imp_Stable = thm "Always_imp_Stable";
   9.263 -val Always_includes_reachable = thm "Always_includes_reachable";
   9.264 -val invariant_imp_Always = thm "invariant_imp_Always";
   9.265 -val Always_reachable = thm "Always_reachable";
   9.266 -val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable";
   9.267 -val Always_eq_includes_reachable = thm "Always_eq_includes_reachable";
   9.268 -val Always_UNIV_eq = thm "Always_UNIV_eq";
   9.269 -val UNIV_AlwaysI = thm "UNIV_AlwaysI";
   9.270 -val Always_eq_UN_invariant = thm "Always_eq_UN_invariant";
   9.271 -val Always_weaken = thm "Always_weaken";
   9.272 -val Always_Constrains_pre = thm "Always_Constrains_pre";
   9.273 -val Always_Constrains_post = thm "Always_Constrains_post";
   9.274 -val Always_ConstrainsI = thm "Always_ConstrainsI";
   9.275 -val Always_ConstrainsD = thm "Always_ConstrainsD";
   9.276 -val Always_Constrains_weaken = thm "Always_Constrains_weaken";
   9.277 -val Always_Int_distrib = thm "Always_Int_distrib";
   9.278 -val Always_INT_distrib = thm "Always_INT_distrib";
   9.279 -val Always_Int_I = thm "Always_Int_I";
   9.280 -val Always_Compl_Un_eq = thm "Always_Compl_Un_eq";
   9.281 -val Always_thin = thm "Always_thin";
   9.282 -
   9.283 -(*FP*)
   9.284 -val stable_FP_Orig_Int = thm "stable_FP_Orig_Int";
   9.285 -val FP_Orig_weakest = thm "FP_Orig_weakest";
   9.286 -val stable_FP_Int = thm "stable_FP_Int";
   9.287 -val FP_equivalence = thm "FP_equivalence";
   9.288 -val FP_weakest = thm "FP_weakest";
   9.289 -val Compl_FP = thm "Compl_FP";
   9.290 -val Diff_FP = thm "Diff_FP";
   9.291 -
   9.292 -(*SubstAx*)
   9.293 -val LeadsTo_eq_leadsTo = thm "LeadsTo_eq_leadsTo";
   9.294 -val Always_LeadsTo_pre = thm "Always_LeadsTo_pre";
   9.295 -val Always_LeadsTo_post = thm "Always_LeadsTo_post";
   9.296 -val Always_LeadsToI = thm "Always_LeadsToI";
   9.297 -val Always_LeadsToD = thm "Always_LeadsToD";
   9.298 -val leadsTo_imp_LeadsTo = thm "leadsTo_imp_LeadsTo";
   9.299 -val LeadsTo_Trans = thm "LeadsTo_Trans";
   9.300 -val LeadsTo_Union = thm "LeadsTo_Union";
   9.301 -val LeadsTo_UNIV = thm "LeadsTo_UNIV";
   9.302 -val LeadsTo_Un_duplicate = thm "LeadsTo_Un_duplicate";
   9.303 -val LeadsTo_Un_duplicate2 = thm "LeadsTo_Un_duplicate2";
   9.304 -val LeadsTo_UN = thm "LeadsTo_UN";
   9.305 -val LeadsTo_Un = thm "LeadsTo_Un";
   9.306 -val single_LeadsTo_I = thm "single_LeadsTo_I";
   9.307 -val subset_imp_LeadsTo = thm "subset_imp_LeadsTo";
   9.308 -val empty_LeadsTo = thm "empty_LeadsTo";
   9.309 -val LeadsTo_weaken_R = thm "LeadsTo_weaken_R";
   9.310 -val LeadsTo_weaken_L = thm "LeadsTo_weaken_L";
   9.311 -val LeadsTo_weaken = thm "LeadsTo_weaken";
   9.312 -val Always_LeadsTo_weaken = thm "Always_LeadsTo_weaken";
   9.313 -val LeadsTo_Un_post = thm "LeadsTo_Un_post";
   9.314 -val LeadsTo_Trans_Un = thm "LeadsTo_Trans_Un";
   9.315 -val LeadsTo_Un_distrib = thm "LeadsTo_Un_distrib";
   9.316 -val LeadsTo_UN_distrib = thm "LeadsTo_UN_distrib";
   9.317 -val LeadsTo_Union_distrib = thm "LeadsTo_Union_distrib";
   9.318 -val LeadsTo_Basis = thm "LeadsTo_Basis";
   9.319 -val EnsuresI = thm "EnsuresI";
   9.320 -val Always_LeadsTo_Basis = thm "Always_LeadsTo_Basis";
   9.321 -val LeadsTo_Diff = thm "LeadsTo_Diff";
   9.322 -val LeadsTo_UN_UN = thm "LeadsTo_UN_UN";
   9.323 -val LeadsTo_UN_UN_noindex = thm "LeadsTo_UN_UN_noindex";
   9.324 -val all_LeadsTo_UN_UN = thm "all_LeadsTo_UN_UN";
   9.325 -val LeadsTo_Un_Un = thm "LeadsTo_Un_Un";
   9.326 -val LeadsTo_cancel2 = thm "LeadsTo_cancel2";
   9.327 -val LeadsTo_cancel_Diff2 = thm "LeadsTo_cancel_Diff2";
   9.328 -val LeadsTo_cancel1 = thm "LeadsTo_cancel1";
   9.329 -val LeadsTo_cancel_Diff1 = thm "LeadsTo_cancel_Diff1";
   9.330 -val LeadsTo_empty = thm "LeadsTo_empty";
   9.331 -val PSP_Stable = thm "PSP_Stable";
   9.332 -val PSP_Stable2 = thm "PSP_Stable2";
   9.333 -val PSP = thm "PSP";
   9.334 -val PSP2 = thm "PSP2";
   9.335 -val PSP_Unless = thm "PSP_Unless";
   9.336 -val Stable_transient_Always_LeadsTo = thm "Stable_transient_Always_LeadsTo";
   9.337 -val LeadsTo_wf_induct = thm "LeadsTo_wf_induct";
   9.338 -val Bounded_induct = thm "Bounded_induct";
   9.339 -val LessThan_induct = thm "LessThan_induct";
   9.340 -val integ_0_le_induct = thm "integ_0_le_induct";
   9.341 -val LessThan_bounded_induct = thm "LessThan_bounded_induct";
   9.342 -val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct";
   9.343 -val Completion = thm "Completion";
   9.344 -val Finite_completion = thm "Finite_completion";
   9.345 -val Stable_completion = thm "Stable_completion";
   9.346 -val Finite_stable_completion = thm "Finite_stable_completion";
   9.347 -
   9.348 -(*Union*)
   9.349 -val Init_SKIP = thm "Init_SKIP";
   9.350 -val Acts_SKIP = thm "Acts_SKIP";
   9.351 -val AllowedActs_SKIP = thm "AllowedActs_SKIP";
   9.352 -val reachable_SKIP = thm "reachable_SKIP";
   9.353 -val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff";
   9.354 -val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff";
   9.355 -val SKIP_in_stable = thm "SKIP_in_stable";
   9.356 -val Init_Join = thm "Init_Join";
   9.357 -val Acts_Join = thm "Acts_Join";
   9.358 -val AllowedActs_Join = thm "AllowedActs_Join";
   9.359 -val JN_empty = thm "JN_empty";
   9.360 -val JN_insert = thm "JN_insert";
   9.361 -val Init_JN = thm "Init_JN";
   9.362 -val Acts_JN = thm "Acts_JN";
   9.363 -val AllowedActs_JN = thm "AllowedActs_JN";
   9.364 -val JN_cong = thm "JN_cong";
   9.365 -val Join_commute = thm "Join_commute";
   9.366 -val Join_assoc = thm "Join_assoc";
   9.367 -val Join_left_commute = thm "Join_left_commute";
   9.368 -val Join_SKIP_left = thm "Join_SKIP_left";
   9.369 -val Join_SKIP_right = thm "Join_SKIP_right";
   9.370 -val Join_absorb = thm "Join_absorb";
   9.371 -val Join_left_absorb = thm "Join_left_absorb";
   9.372 -val Join_ac = thms "Join_ac";
   9.373 -val JN_absorb = thm "JN_absorb";
   9.374 -val JN_Un = thm "JN_Un";
   9.375 -val JN_constant = thm "JN_constant";
   9.376 -val JN_Join_distrib = thm "JN_Join_distrib";
   9.377 -val JN_Join_miniscope = thm "JN_Join_miniscope";
   9.378 -val JN_Join_diff = thm "JN_Join_diff";
   9.379 -val JN_constrains = thm "JN_constrains";
   9.380 -val Join_constrains = thm "Join_constrains";
   9.381 -val Join_unless = thm "Join_unless";
   9.382 -val Join_constrains_weaken = thm "Join_constrains_weaken";
   9.383 -val JN_constrains_weaken = thm "JN_constrains_weaken";
   9.384 -val JN_stable = thm "JN_stable";
   9.385 -val invariant_JN_I = thm "invariant_JN_I";
   9.386 -val Join_stable = thm "Join_stable";
   9.387 -val Join_increasing = thm "Join_increasing";
   9.388 -val invariant_JoinI = thm "invariant_JoinI";
   9.389 -val FP_JN = thm "FP_JN";
   9.390 -val JN_transient = thm "JN_transient";
   9.391 -val Join_transient = thm "Join_transient";
   9.392 -val Join_transient_I1 = thm "Join_transient_I1";
   9.393 -val Join_transient_I2 = thm "Join_transient_I2";
   9.394 -val JN_ensures = thm "JN_ensures";
   9.395 -val Join_ensures = thm "Join_ensures";
   9.396 -val stable_Join_constrains = thm "stable_Join_constrains";
   9.397 -val stable_Join_Always1 = thm "stable_Join_Always1";
   9.398 -val stable_Join_Always2 = thm "stable_Join_Always2";
   9.399 -val stable_Join_ensures1 = thm "stable_Join_ensures1";
   9.400 -val stable_Join_ensures2 = thm "stable_Join_ensures2";
   9.401 -val ok_SKIP1 = thm "ok_SKIP1";
   9.402 -val ok_SKIP2 = thm "ok_SKIP2";
   9.403 -val ok_Join_commute = thm "ok_Join_commute";
   9.404 -val ok_commute = thm "ok_commute";
   9.405 -val ok_sym = thm "ok_sym";
   9.406 -val ok_iff_OK = thm "ok_iff_OK";
   9.407 -val ok_Join_iff1 = thm "ok_Join_iff1";
   9.408 -val ok_Join_iff2 = thm "ok_Join_iff2";
   9.409 -val ok_Join_commute_I = thm "ok_Join_commute_I";
   9.410 -val ok_JN_iff1 = thm "ok_JN_iff1";
   9.411 -val ok_JN_iff2 = thm "ok_JN_iff2";
   9.412 -val OK_iff_ok = thm "OK_iff_ok";
   9.413 -val OK_imp_ok = thm "OK_imp_ok";
   9.414 -val Allowed_SKIP = thm "Allowed_SKIP";
   9.415 -val Allowed_Join = thm "Allowed_Join";
   9.416 -val Allowed_JN = thm "Allowed_JN";
   9.417 -val ok_iff_Allowed = thm "ok_iff_Allowed";
   9.418 -val OK_iff_Allowed = thm "OK_iff_Allowed";
   9.419 -val safety_prop_Acts_iff = thm "safety_prop_Acts_iff";
   9.420 -val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
   9.421 -val Allowed_eq = thm "Allowed_eq";
   9.422 -val def_prg_Allowed = thm "def_prg_Allowed";
   9.423 -val def_total_prg_Allowed = thm "def_total_prg_Allowed";
   9.424 -val safety_prop_constrains = thm "safety_prop_constrains";
   9.425 -val safety_prop_stable = thm "safety_prop_stable";
   9.426 -val safety_prop_Int = thm "safety_prop_Int";
   9.427 -val safety_prop_INTER1 = thm "safety_prop_INTER1";
   9.428 -val safety_prop_INTER = thm "safety_prop_INTER";
   9.429 -val def_UNION_ok_iff = thm "def_UNION_ok_iff";
   9.430 -val totalize_JN = thm "totalize_JN";
   9.431 -
   9.432 -(*Comp*)
   9.433 -val preserves_def = thm "preserves_def";
   9.434 -val funPair_def = thm "funPair_def";
   9.435 -val componentI = thm "componentI";
   9.436 -val component_eq_subset = thm "component_eq_subset";
   9.437 -val component_SKIP = thm "component_SKIP";
   9.438 -val component_refl = thm "component_refl";
   9.439 -val SKIP_minimal = thm "SKIP_minimal";
   9.440 -val component_Join1 = thm "component_Join1";
   9.441 -val component_Join2 = thm "component_Join2";
   9.442 -val Join_absorb1 = thm "Join_absorb1";
   9.443 -val Join_absorb2 = thm "Join_absorb2";
   9.444 -val JN_component_iff = thm "JN_component_iff";
   9.445 -val component_JN = thm "component_JN";
   9.446 -val component_trans = thm "component_trans";
   9.447 -val component_antisym = thm "component_antisym";
   9.448 -val Join_component_iff = thm "Join_component_iff";
   9.449 -val component_constrains = thm "component_constrains";
   9.450 -val program_less_le = thm "program_less_le";
   9.451 -val preservesI = thm "preservesI";
   9.452 -val preserves_imp_eq = thm "preserves_imp_eq";
   9.453 -val Join_preserves = thm "Join_preserves";
   9.454 -val JN_preserves = thm "JN_preserves";
   9.455 -val SKIP_preserves = thm "SKIP_preserves";
   9.456 -val funPair_apply = thm "funPair_apply";
   9.457 -val preserves_funPair = thm "preserves_funPair";
   9.458 -val funPair_o_distrib = thm "funPair_o_distrib";
   9.459 -val fst_o_funPair = thm "fst_o_funPair";
   9.460 -val snd_o_funPair = thm "snd_o_funPair";
   9.461 -val subset_preserves_o = thm "subset_preserves_o";
   9.462 -val preserves_subset_stable = thm "preserves_subset_stable";
   9.463 -val preserves_subset_increasing = thm "preserves_subset_increasing";
   9.464 -val preserves_id_subset_stable = thm "preserves_id_subset_stable";
   9.465 -val safety_prop_preserves = thm "safety_prop_preserves";
   9.466 -val stable_localTo_stable2 = thm "stable_localTo_stable2";
   9.467 -val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
   9.468 -val component_of_imp_component = thm "component_of_imp_component";
   9.469 -val component_of_refl = thm "component_of_refl";
   9.470 -val component_of_SKIP = thm "component_of_SKIP";
   9.471 -val component_of_trans = thm "component_of_trans";
   9.472 -val strict_component_of_eq = thm "strict_component_of_eq";
   9.473 -val localize_Init_eq = thm "localize_Init_eq";
   9.474 -val localize_Acts_eq = thm "localize_Acts_eq";
   9.475 -val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
   9.476 -
   9.477 -(*Guar*)
   9.478 -val guar_def = thm "guar_def";
   9.479 -val OK_insert_iff = thm "OK_insert_iff";
   9.480 -val ex1 = thm "ex1";
   9.481 -val ex2 = thm "ex2";
   9.482 -val ex_prop_finite = thm "ex_prop_finite";
   9.483 -val ex_prop_equiv = thm "ex_prop_equiv";
   9.484 -val uv1 = thm "uv1";
   9.485 -val uv2 = thm "uv2";
   9.486 -val uv_prop_finite = thm "uv_prop_finite";
   9.487 -val guaranteesI = thm "guaranteesI";
   9.488 -val guaranteesD = thm "guaranteesD";
   9.489 -val component_guaranteesD = thm "component_guaranteesD";
   9.490 -val guarantees_weaken = thm "guarantees_weaken";
   9.491 -val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV";
   9.492 -val subset_imp_guarantees = thm "subset_imp_guarantees";
   9.493 -val ex_prop_imp = thm "ex_prop_imp";
   9.494 -val guarantees_imp = thm "guarantees_imp";
   9.495 -val ex_prop_equiv2 = thm "ex_prop_equiv2";
   9.496 -val guarantees_UN_left = thm "guarantees_UN_left";
   9.497 -val guarantees_Un_left = thm "guarantees_Un_left";
   9.498 -val guarantees_INT_right = thm "guarantees_INT_right";
   9.499 -val guarantees_Int_right = thm "guarantees_Int_right";
   9.500 -val guarantees_Int_right_I = thm "guarantees_Int_right_I";
   9.501 -val guarantees_INT_right_iff = thm "guarantees_INT_right_iff";
   9.502 -val shunting = thm "shunting";
   9.503 -val contrapositive = thm "contrapositive";
   9.504 -val combining1 = thm "combining1";
   9.505 -val combining2 = thm "combining2";
   9.506 -val all_guarantees = thm "all_guarantees";
   9.507 -val ex_guarantees = thm "ex_guarantees";
   9.508 -val guarantees_Join_Int = thm "guarantees_Join_Int";
   9.509 -val guarantees_Join_Un = thm "guarantees_Join_Un";
   9.510 -val guarantees_JN_INT = thm "guarantees_JN_INT";
   9.511 -val guarantees_JN_UN = thm "guarantees_JN_UN";
   9.512 -val guarantees_Join_I1 = thm "guarantees_Join_I1";
   9.513 -val guarantees_Join_I2 = thm "guarantees_Join_I2";
   9.514 -val guarantees_JN_I = thm "guarantees_JN_I";
   9.515 -val Join_welldef_D1 = thm "Join_welldef_D1";
   9.516 -val Join_welldef_D2 = thm "Join_welldef_D2";
   9.517 -val refines_refl = thm "refines_refl";
   9.518 -val ex_refinement_thm = thm "ex_refinement_thm";
   9.519 -val uv_refinement_thm = thm "uv_refinement_thm";
   9.520 -val guarantees_equiv = thm "guarantees_equiv";
   9.521 -val wg_weakest = thm "wg_weakest";
   9.522 -val wg_guarantees = thm "wg_guarantees";
   9.523 -val wg_equiv = thm "wg_equiv";
   9.524 -val component_of_wg = thm "component_of_wg";
   9.525 -val wg_finite = thm "wg_finite";
   9.526 -val wg_ex_prop = thm "wg_ex_prop";
   9.527 -val wx_subset = thm "wx_subset";
   9.528 -val wx_ex_prop = thm "wx_ex_prop";
   9.529 -val wx_weakest = thm "wx_weakest";
   9.530 -val wx'_ex_prop = thm "wx'_ex_prop";
   9.531 -val wx_equiv = thm "wx_equiv";
   9.532 -val guarantees_wx_eq = thm "guarantees_wx_eq";
   9.533 -val stable_guarantees_Always = thm "stable_guarantees_Always";
   9.534 -val leadsTo_Basis = thm "leadsTo_Basis";
   9.535 -val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo";
   9.536 -
   9.537 -(*Extend*)
   9.538 -val Restrict_iff = thm "Restrict_iff";
   9.539 -val Restrict_UNIV = thm "Restrict_UNIV";
   9.540 -val Restrict_empty = thm "Restrict_empty";
   9.541 -val Restrict_Int = thm "Restrict_Int";
   9.542 -val Restrict_triv = thm "Restrict_triv";
   9.543 -val Restrict_subset = thm "Restrict_subset";
   9.544 -val Restrict_eq_mono = thm "Restrict_eq_mono";
   9.545 -val Restrict_imageI = thm "Restrict_imageI";
   9.546 -val Domain_Restrict = thm "Domain_Restrict";
   9.547 -val Image_Restrict = thm "Image_Restrict";
   9.548 -val insert_Id_image_Acts = thm "insert_Id_image_Acts";
   9.549 -val good_mapI = thm "good_mapI";
   9.550 -val good_map_is_surj = thm "good_map_is_surj";
   9.551 -val fst_inv_equalityI = thm "fst_inv_equalityI";
   9.552 -val project_set_iff = thm "project_set_iff";
   9.553 -val extend_set_mono = thm "extend_set_mono";
   9.554 -val extend_set_empty = thm "extend_set_empty";
   9.555 -val project_set_Int_subset = thm "project_set_Int_subset";
   9.556 -val Init_extend = thm "Init_extend";
   9.557 -val Init_project = thm "Init_project";
   9.558 -val Acts_project = thm "Acts_project";
   9.559 -val project_set_UNIV = thm "project_set_UNIV";
   9.560 -val project_set_Union = thm "project_set_Union";
   9.561 -val project_act_mono = thm "project_act_mono";
   9.562 -val project_constrains_project_set = thm "project_constrains_project_set";
   9.563 -val project_stable_project_set = thm "project_stable_project_set";
   9.564 -
   9.565 -
   9.566 -(*Rename*)
   9.567 -val good_map_bij = thm "good_map_bij";
   9.568 -val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv";
   9.569 -val mem_rename_set_iff = thm "mem_rename_set_iff";
   9.570 -val extend_set_eq_image = thm "extend_set_eq_image";
   9.571 -val Init_rename = thm "Init_rename";
   9.572 -val extend_set_inv = thm "extend_set_inv";
   9.573 -val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act";
   9.574 -val bij_extend_act = thm "bij_extend_act";
   9.575 -val bij_project_act = thm "bij_project_act";
   9.576 -val bij_inv_project_act_eq = thm "bij_inv_project_act_eq";
   9.577 -val Acts_project = thm "Acts_project";
   9.578 -val extend_inv = thm "extend_inv";
   9.579 -val rename_inv_rename = thm "rename_inv_rename";
   9.580 -val rename_rename_inv = thm "rename_rename_inv";
   9.581 -val rename_inv_eq = thm "rename_inv_eq";
   9.582 -val bij_extend = thm "bij_extend";
   9.583 -val bij_project = thm "bij_project";
   9.584 -val inv_project_eq = thm "inv_project_eq";
   9.585 -val Allowed_rename = thm "Allowed_rename";
   9.586 -val bij_rename = thm "bij_rename";
   9.587 -val surj_rename = thm "surj_rename";
   9.588 -val inj_rename_imp_inj = thm "inj_rename_imp_inj";
   9.589 -val surj_rename_imp_surj = thm "surj_rename_imp_surj";
   9.590 -val bij_rename_imp_bij = thm "bij_rename_imp_bij";
   9.591 -val bij_rename_iff = thm "bij_rename_iff";
   9.592 -val rename_SKIP = thm "rename_SKIP";
   9.593 -val rename_Join = thm "rename_Join";
   9.594 -val rename_JN = thm "rename_JN";
   9.595 -val rename_constrains = thm "rename_constrains";
   9.596 -val rename_stable = thm "rename_stable";
   9.597 -val rename_invariant = thm "rename_invariant";
   9.598 -val rename_increasing = thm "rename_increasing";
   9.599 -val reachable_rename_eq = thm "reachable_rename_eq";
   9.600 -val rename_Constrains = thm "rename_Constrains";
   9.601 -val rename_Stable = thm "rename_Stable";
   9.602 -val rename_Always = thm "rename_Always";
   9.603 -val rename_Increasing = thm "rename_Increasing";
   9.604 -val rename_transient = thm "rename_transient";
   9.605 -val rename_ensures = thm "rename_ensures";
   9.606 -val rename_leadsTo = thm "rename_leadsTo";
   9.607 -val rename_LeadsTo = thm "rename_LeadsTo";
   9.608 -val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq";
   9.609 -val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv";
   9.610 -val rename_preserves = thm "rename_preserves";
   9.611 -val ok_rename_iff = thm "ok_rename_iff";
   9.612 -val OK_rename_iff = thm "OK_rename_iff";
   9.613 -val bij_eq_rename = thm "bij_eq_rename";
   9.614 -val rename_image_constrains = thm "rename_image_constrains";
   9.615 -val rename_image_stable = thm "rename_image_stable";
   9.616 -val rename_image_increasing = thm "rename_image_increasing";
   9.617 -val rename_image_invariant = thm "rename_image_invariant";
   9.618 -val rename_image_Constrains = thm "rename_image_Constrains";
   9.619 -val rename_image_preserves = thm "rename_image_preserves";
   9.620 -val rename_image_Stable = thm "rename_image_Stable";
   9.621 -val rename_image_Increasing = thm "rename_image_Increasing";
   9.622 -val rename_image_Always = thm "rename_image_Always";
   9.623 -val rename_image_leadsTo = thm "rename_image_leadsTo";
   9.624 -val rename_image_LeadsTo = thm "rename_image_LeadsTo";
   9.625 -
   9.626 -
   9.627 -
   9.628 -(*Lift_prog*)
   9.629 -val sub_def = thm "sub_def";
   9.630 -val lift_map_def = thm "lift_map_def";
   9.631 -val drop_map_def = thm "drop_map_def";
   9.632 -val insert_map_inverse = thm "insert_map_inverse";
   9.633 -val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
   9.634 -val insert_map_inject1 = thm "insert_map_inject1";
   9.635 -val insert_map_inject2 = thm "insert_map_inject2";
   9.636 -val insert_map_inject = thm "insert_map_inject";
   9.637 -val insert_map_inject = thm "insert_map_inject";
   9.638 -val lift_map_eq_iff = thm "lift_map_eq_iff";
   9.639 -val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
   9.640 -val inj_lift_map = thm "inj_lift_map";
   9.641 -val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
   9.642 -val drop_map_inject = thm "drop_map_inject";
   9.643 -val surj_lift_map = thm "surj_lift_map";
   9.644 -val bij_lift_map = thm "bij_lift_map";
   9.645 -val inv_lift_map_eq = thm "inv_lift_map_eq";
   9.646 -val inv_drop_map_eq = thm "inv_drop_map_eq";
   9.647 -val bij_drop_map = thm "bij_drop_map";
   9.648 -val sub_apply = thm "sub_apply";
   9.649 -val lift_set_empty = thm "lift_set_empty";
   9.650 -val lift_set_iff = thm "lift_set_iff";
   9.651 -val lift_set_iff2 = thm "lift_set_iff2";
   9.652 -val lift_set_mono = thm "lift_set_mono";
   9.653 -val lift_set_Un_distrib = thm "lift_set_Un_distrib";
   9.654 -val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
   9.655 -val bij_lift = thm "bij_lift";
   9.656 -val lift_SKIP = thm "lift_SKIP";
   9.657 -val lift_Join = thm "lift_Join";
   9.658 -val lift_JN = thm "lift_JN";
   9.659 -val lift_constrains = thm "lift_constrains";
   9.660 -val lift_stable = thm "lift_stable";
   9.661 -val lift_invariant = thm "lift_invariant";
   9.662 -val lift_Constrains = thm "lift_Constrains";
   9.663 -val lift_Stable = thm "lift_Stable";
   9.664 -val lift_Always = thm "lift_Always";
   9.665 -val lift_transient = thm "lift_transient";
   9.666 -val lift_ensures = thm "lift_ensures";
   9.667 -val lift_leadsTo = thm "lift_leadsTo";
   9.668 -val lift_LeadsTo = thm "lift_LeadsTo";
   9.669 -val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
   9.670 -val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
   9.671 -val lift_preserves_snd_I = thm "lift_preserves_snd_I";
   9.672 -val delete_map_eqE = thm "delete_map_eqE";
   9.673 -val delete_map_eqE = thm "delete_map_eqE";
   9.674 -val delete_map_neq_apply = thm "delete_map_neq_apply";
   9.675 -val vimage_o_fst_eq = thm "vimage_o_fst_eq";
   9.676 -val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
   9.677 -val mem_lift_act_iff = thm "mem_lift_act_iff";
   9.678 -val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
   9.679 -val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
   9.680 -val lift_map_image_Times = thm "lift_map_image_Times";
   9.681 -val lift_preserves_eq = thm "lift_preserves_eq";
   9.682 -val lift_preserves_sub = thm "lift_preserves_sub";
   9.683 -val o_equiv_assoc = thm "o_equiv_assoc";
   9.684 -val o_equiv_apply = thm "o_equiv_apply";
   9.685 -val fst_o_lift_map = thm "fst_o_lift_map";
   9.686 -val snd_o_lift_map = thm "snd_o_lift_map";
   9.687 -val extend_act_extend_act = thm "extend_act_extend_act";
   9.688 -val project_act_project_act = thm "project_act_project_act";
   9.689 -val project_act_extend_act = thm "project_act_extend_act";
   9.690 -val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
   9.691 -val UNION_OK_lift_I = thm "UNION_OK_lift_I";
   9.692 -val OK_lift_I = thm "OK_lift_I";
   9.693 -val Allowed_lift = thm "Allowed_lift";
   9.694 -val lift_image_preserves = thm "lift_image_preserves";
   9.695 -
   9.696 -
   9.697 -(*PPROD*)
   9.698 -val Init_PLam = thm "Init_PLam";
   9.699 -val PLam_empty = thm "PLam_empty";
   9.700 -val PLam_SKIP = thm "PLam_SKIP";
   9.701 -val PLam_insert = thm "PLam_insert";
   9.702 -val PLam_component_iff = thm "PLam_component_iff";
   9.703 -val component_PLam = thm "component_PLam";
   9.704 -val PLam_constrains = thm "PLam_constrains";
   9.705 -val PLam_stable = thm "PLam_stable";
   9.706 -val PLam_transient = thm "PLam_transient";
   9.707 -val PLam_ensures = thm "PLam_ensures";
   9.708 -val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
   9.709 -val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
   9.710 -val PLam_preserves_fst = thm "PLam_preserves_fst";
   9.711 -val PLam_preserves_snd = thm "PLam_preserves_snd";
   9.712 -val guarantees_PLam_I = thm "guarantees_PLam_I";
   9.713 -val Allowed_PLam = thm "Allowed_PLam";
   9.714 -val PLam_preserves = thm "PLam_preserves";
   9.715 -
   9.716 -(*Follows*)
   9.717 -val mono_Always_o = thm "mono_Always_o";
   9.718 -val mono_LeadsTo_o = thm "mono_LeadsTo_o";
   9.719 -val Follows_constant = thm "Follows_constant";
   9.720 -val mono_Follows_o = thm "mono_Follows_o";
   9.721 -val mono_Follows_apply = thm "mono_Follows_apply";
   9.722 -val Follows_trans = thm "Follows_trans";
   9.723 -val Follows_Increasing1 = thm "Follows_Increasing1";
   9.724 -val Follows_Increasing2 = thm "Follows_Increasing2";
   9.725 -val Follows_Bounded = thm "Follows_Bounded";
   9.726 -val Follows_LeadsTo = thm "Follows_LeadsTo";
   9.727 -val Follows_LeadsTo_pfixLe = thm "Follows_LeadsTo_pfixLe";
   9.728 -val Follows_LeadsTo_pfixGe = thm "Follows_LeadsTo_pfixGe";
   9.729 -val Always_Follows1 = thm "Always_Follows1";
   9.730 -val Always_Follows2 = thm "Always_Follows2";
   9.731 -val increasing_Un = thm "increasing_Un";
   9.732 -val Increasing_Un = thm "Increasing_Un";
   9.733 -val Always_Un = thm "Always_Un";
   9.734 -val Follows_Un = thm "Follows_Un";
   9.735 -val increasing_union = thm "increasing_union";
   9.736 -val Increasing_union = thm "Increasing_union";
   9.737 -val Always_union = thm "Always_union";
   9.738 -val Follows_union = thm "Follows_union";
   9.739 -val Follows_setsum = thm "Follows_setsum";
   9.740 -val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe";
   9.741 -val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe";
   9.742 -
   9.743 -
   9.744 -(*Lazy unfolding of actions or of sets*)
   9.745 -fun simp_of_act def = def RS def_act_simp;
   9.746 -
   9.747 -fun simp_of_set def = def RS def_set_simp;
   9.748 -
   9.749 -
   9.750  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   9.751 -val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin
   9.752 +val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
   9.753  
   9.754  (*Combines a list of invariance THEOREMS into one.*)
   9.755 -val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I)
   9.756 +val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
   9.757  
   9.758  (*Proves "co" properties when the program is specified.  Any use of invariants
   9.759    (from weak constrains) must have been done already.*)
   9.760 -fun gen_constrains_tac(cs,ss) i = 
   9.761 +fun constrains_tac(cs,ss) i =
   9.762     SELECT_GOAL
   9.763        (EVERY [REPEAT (Always_Int_tac 1),
   9.764                (*reduce the fancy safety properties to "constrains"*)
   9.765 -	      REPEAT (etac Always_ConstrainsI 1
   9.766 -		      ORELSE
   9.767 -		      resolve_tac [StableI, stableI,
   9.768 -				   constrains_imp_Constrains] 1),
   9.769 +              REPEAT (etac @{thm Always_ConstrainsI} 1
   9.770 +                      ORELSE
   9.771 +                      resolve_tac [@{thm StableI}, @{thm stableI},
   9.772 +                                   @{thm constrains_imp_Constrains}] 1),
   9.773                (*for safety, the totalize operator can be ignored*)
   9.774 -	      simp_tac (HOL_ss addsimps
   9.775 -                         [mk_total_program_def, totalize_constrains_iff]) 1,
   9.776 -	      rtac constrainsI 1,
   9.777 -	      full_simp_tac ss 1,
   9.778 -	      REPEAT (FIRSTGOAL (etac disjE)),
   9.779 -	      ALLGOALS (clarify_tac cs),
   9.780 -	      ALLGOALS (asm_lr_simp_tac ss)]) i;
   9.781 +              simp_tac (HOL_ss addsimps
   9.782 +                         [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
   9.783 +              rtac @{thm constrainsI} 1,
   9.784 +              full_simp_tac ss 1,
   9.785 +              REPEAT (FIRSTGOAL (etac disjE)),
   9.786 +              ALLGOALS (clarify_tac cs),
   9.787 +              ALLGOALS (asm_lr_simp_tac ss)]) i;
   9.788  
   9.789  (*proves "ensures/leadsTo" properties when the program is specified*)
   9.790 -fun gen_ensures_tac(cs,ss) sact = 
   9.791 +fun ensures_tac(cs,ss) sact =
   9.792      SELECT_GOAL
   9.793        (EVERY [REPEAT (Always_Int_tac 1),
   9.794 -	      etac Always_LeadsTo_Basis 1 
   9.795 -	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   9.796 -		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
   9.797 -				    EnsuresI, ensuresI] 1),
   9.798 -	      (*now there are two subgoals: co & transient*)
   9.799 -	      simp_tac (ss addsimps [mk_total_program_def]) 2,
   9.800 -	      res_inst_tac [("act", sact)] totalize_transientI 2 
   9.801 - 	      ORELSE res_inst_tac [("act", sact)] transientI 2,
   9.802 +              etac @{thm Always_LeadsTo_Basis} 1
   9.803 +                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   9.804 +                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
   9.805 +                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
   9.806 +              (*now there are two subgoals: co & transient*)
   9.807 +              simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
   9.808 +              res_inst_tac [("act", sact)] @{thm totalize_transientI} 2
   9.809 +              ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2,
   9.810                   (*simplify the command's domain*)
   9.811 -	      simp_tac (ss addsimps [Domain_def]) 3,
   9.812 -	      gen_constrains_tac (cs,ss) 1,
   9.813 -	      ALLGOALS (clarify_tac cs),
   9.814 -	      ALLGOALS (asm_lr_simp_tac ss)]);
   9.815 -
   9.816 -fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
   9.817 -
   9.818 -fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
   9.819 +              simp_tac (ss addsimps [@{thm Domain_def}]) 3,
   9.820 +              constrains_tac (cs,ss) 1,
   9.821 +              ALLGOALS (clarify_tac cs),
   9.822 +              ALLGOALS (asm_lr_simp_tac ss)]);
   9.823  
   9.824  
   9.825  (*Composition equivalences, from Lift_prog*)
   9.826  
   9.827  fun make_o_equivs th =
   9.828      [th,
   9.829 -     th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
   9.830 -     th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
   9.831 +     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
   9.832 +     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
   9.833  
   9.834 -Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
   9.835 +Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair});
   9.836  
   9.837 -Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
   9.838 +Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map});