src/HOL/UNITY/Comp/Alloc.thy
changeset 56199 8e8d28ed7529
parent 52089 6ce832f71bdd
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 18 10:00:23 2014 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Mar 18 11:07:47 2014 +0100
     1.3 @@ -425,7 +425,7 @@
     1.4    apply (rule fst_o_funPair)
     1.5    done
     1.6  
     1.7 -ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
     1.8 +ML {* ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
     1.9  declare fst_o_client_map' [simp]
    1.10  
    1.11  lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
    1.12 @@ -433,7 +433,7 @@
    1.13    apply (rule snd_o_funPair)
    1.14    done
    1.15  
    1.16 -ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
    1.17 +ML {* ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
    1.18  declare snd_o_client_map' [simp]
    1.19  
    1.20  
    1.21 @@ -443,28 +443,28 @@
    1.22    apply record_auto
    1.23    done
    1.24  
    1.25 -ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
    1.26 +ML {* ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
    1.27  declare client_o_sysOfAlloc' [simp]
    1.28  
    1.29  lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
    1.30    apply record_auto
    1.31    done
    1.32  
    1.33 -ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
    1.34 +ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
    1.35  declare allocGiv_o_sysOfAlloc_eq' [simp]
    1.36  
    1.37  lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
    1.38    apply record_auto
    1.39    done
    1.40  
    1.41 -ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
    1.42 +ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
    1.43  declare allocAsk_o_sysOfAlloc_eq' [simp]
    1.44  
    1.45  lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
    1.46    apply record_auto
    1.47    done
    1.48  
    1.49 -ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
    1.50 +ML {* ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
    1.51  declare allocRel_o_sysOfAlloc_eq' [simp]
    1.52  
    1.53  
    1.54 @@ -474,49 +474,49 @@
    1.55    apply record_auto
    1.56    done
    1.57  
    1.58 -ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
    1.59 +ML {* ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
    1.60  declare client_o_sysOfClient' [simp]
    1.61  
    1.62  lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
    1.63    apply record_auto
    1.64    done
    1.65  
    1.66 -ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
    1.67 +ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
    1.68  declare allocGiv_o_sysOfClient_eq' [simp]
    1.69  
    1.70  lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
    1.71    apply record_auto
    1.72    done
    1.73  
    1.74 -ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
    1.75 +ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
    1.76  declare allocAsk_o_sysOfClient_eq' [simp]
    1.77  
    1.78  lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
    1.79    apply record_auto
    1.80    done
    1.81  
    1.82 -ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
    1.83 +ML {* ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
    1.84  declare allocRel_o_sysOfClient_eq' [simp]
    1.85  
    1.86  lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
    1.87    apply (simp add: o_def)
    1.88    done
    1.89  
    1.90 -ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
    1.91 +ML {* ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
    1.92  declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
    1.93  
    1.94  lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
    1.95    apply (simp add: o_def)
    1.96    done
    1.97  
    1.98 -ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
    1.99 +ML {* ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
   1.100  declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
   1.101  
   1.102  lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
   1.103    apply (simp add: o_def)
   1.104    done
   1.105  
   1.106 -ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
   1.107 +ML {* ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
   1.108  declare allocRel_o_inv_sysOfAlloc_eq' [simp]
   1.109  
   1.110  lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
   1.111 @@ -524,7 +524,7 @@
   1.112    apply (simp add: o_def drop_map_def)
   1.113    done
   1.114  
   1.115 -ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
   1.116 +ML {* ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
   1.117  declare rel_inv_client_map_drop_map [simp]
   1.118  
   1.119  lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
   1.120 @@ -532,7 +532,7 @@
   1.121    apply (simp add: o_def drop_map_def)
   1.122    done
   1.123  
   1.124 -ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
   1.125 +ML {* ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
   1.126  declare ask_inv_client_map_drop_map [simp]
   1.127  
   1.128  
   1.129 @@ -549,13 +549,13 @@
   1.130          @{thm Client} |> simplify (@{context} addsimps @{thms client_spec_simps})
   1.131                 |> list_of_Int;
   1.132  
   1.133 -bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
   1.134 -bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
   1.135 -bind_thm ("Client_Bounded", Client_Bounded);
   1.136 -bind_thm ("Client_Progress", Client_Progress);
   1.137 -bind_thm ("Client_AllowedActs", Client_AllowedActs);
   1.138 -bind_thm ("Client_preserves_giv", Client_preserves_giv);
   1.139 -bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
   1.140 +ML_Thms.bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
   1.141 +ML_Thms.bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
   1.142 +ML_Thms.bind_thm ("Client_Bounded", Client_Bounded);
   1.143 +ML_Thms.bind_thm ("Client_Progress", Client_Progress);
   1.144 +ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs);
   1.145 +ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv);
   1.146 +ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
   1.147  *}
   1.148  
   1.149  declare
   1.150 @@ -579,13 +579,13 @@
   1.151          @{thm Network} |> simplify (@{context} addsimps @{thms network_spec_simps})
   1.152                  |> list_of_Int;
   1.153  
   1.154 -bind_thm ("Network_Ask", Network_Ask);
   1.155 -bind_thm ("Network_Giv", Network_Giv);
   1.156 -bind_thm ("Network_Rel", Network_Rel);
   1.157 -bind_thm ("Network_AllowedActs", Network_AllowedActs);
   1.158 -bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
   1.159 -bind_thm ("Network_preserves_rel", Network_preserves_rel);
   1.160 -bind_thm ("Network_preserves_ask", Network_preserves_ask);
   1.161 +ML_Thms.bind_thm ("Network_Ask", Network_Ask);
   1.162 +ML_Thms.bind_thm ("Network_Giv", Network_Giv);
   1.163 +ML_Thms.bind_thm ("Network_Rel", Network_Rel);
   1.164 +ML_Thms.bind_thm ("Network_AllowedActs", Network_AllowedActs);
   1.165 +ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
   1.166 +ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel);
   1.167 +ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask);
   1.168  *}
   1.169  
   1.170  declare Network_preserves_allocGiv [iff]
   1.171 @@ -610,13 +610,13 @@
   1.172          @{thm Alloc} |> simplify (@{context} addsimps @{thms alloc_spec_simps})
   1.173                |> list_of_Int;
   1.174  
   1.175 -bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
   1.176 -bind_thm ("Alloc_Safety", Alloc_Safety);
   1.177 -bind_thm ("Alloc_Progress", Alloc_Progress);
   1.178 -bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
   1.179 -bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
   1.180 -bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
   1.181 -bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
   1.182 +ML_Thms.bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
   1.183 +ML_Thms.bind_thm ("Alloc_Safety", Alloc_Safety);
   1.184 +ML_Thms.bind_thm ("Alloc_Progress", Alloc_Progress);
   1.185 +ML_Thms.bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
   1.186 +ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
   1.187 +ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
   1.188 +ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
   1.189  *}
   1.190  
   1.191  text{*Strip off the INT in the guarantees postcondition*}
   1.192 @@ -808,7 +808,7 @@
   1.193  
   1.194  
   1.195  ML {*
   1.196 -bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
   1.197 +ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
   1.198  *}
   1.199  
   1.200  declare System_Increasing' [intro!]