src/HOL/UNITY/UNITY_tactics.ML
author paulson
Wed Jan 29 16:34:51 2003 +0100 (2003-01-29)
changeset 13792 d1811693899c
parent 13790 8d7e9fce8c50
child 13796 19f50fa807ae
permissions -rw-r--r--
converted more UNITY theories to new-style
     1 (*  Title:      HOL/UNITY/UNITY_tactics.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2003  University of Cambridge
     5 
     6 Specialized UNITY tactics, and ML bindings of theorems
     7 *)
     8 
     9 (*Union*)
    10 val Init_SKIP = thm "Init_SKIP";
    11 val Acts_SKIP = thm "Acts_SKIP";
    12 val AllowedActs_SKIP = thm "AllowedActs_SKIP";
    13 val reachable_SKIP = thm "reachable_SKIP";
    14 val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff";
    15 val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff";
    16 val SKIP_in_stable = thm "SKIP_in_stable";
    17 val Init_Join = thm "Init_Join";
    18 val Acts_Join = thm "Acts_Join";
    19 val AllowedActs_Join = thm "AllowedActs_Join";
    20 val JN_empty = thm "JN_empty";
    21 val JN_insert = thm "JN_insert";
    22 val Init_JN = thm "Init_JN";
    23 val Acts_JN = thm "Acts_JN";
    24 val AllowedActs_JN = thm "AllowedActs_JN";
    25 val JN_cong = thm "JN_cong";
    26 val Join_commute = thm "Join_commute";
    27 val Join_assoc = thm "Join_assoc";
    28 val Join_left_commute = thm "Join_left_commute";
    29 val Join_SKIP_left = thm "Join_SKIP_left";
    30 val Join_SKIP_right = thm "Join_SKIP_right";
    31 val Join_absorb = thm "Join_absorb";
    32 val Join_left_absorb = thm "Join_left_absorb";
    33 val Join_ac = thms "Join_ac";
    34 val JN_absorb = thm "JN_absorb";
    35 val JN_Un = thm "JN_Un";
    36 val JN_constant = thm "JN_constant";
    37 val JN_Join_distrib = thm "JN_Join_distrib";
    38 val JN_Join_miniscope = thm "JN_Join_miniscope";
    39 val JN_Join_diff = thm "JN_Join_diff";
    40 val JN_constrains = thm "JN_constrains";
    41 val Join_constrains = thm "Join_constrains";
    42 val Join_unless = thm "Join_unless";
    43 val Join_constrains_weaken = thm "Join_constrains_weaken";
    44 val JN_constrains_weaken = thm "JN_constrains_weaken";
    45 val JN_stable = thm "JN_stable";
    46 val invariant_JN_I = thm "invariant_JN_I";
    47 val Join_stable = thm "Join_stable";
    48 val Join_increasing = thm "Join_increasing";
    49 val invariant_JoinI = thm "invariant_JoinI";
    50 val FP_JN = thm "FP_JN";
    51 val JN_transient = thm "JN_transient";
    52 val Join_transient = thm "Join_transient";
    53 val Join_transient_I1 = thm "Join_transient_I1";
    54 val Join_transient_I2 = thm "Join_transient_I2";
    55 val JN_ensures = thm "JN_ensures";
    56 val Join_ensures = thm "Join_ensures";
    57 val stable_Join_constrains = thm "stable_Join_constrains";
    58 val stable_Join_Always1 = thm "stable_Join_Always1";
    59 val stable_Join_Always2 = thm "stable_Join_Always2";
    60 val stable_Join_ensures1 = thm "stable_Join_ensures1";
    61 val stable_Join_ensures2 = thm "stable_Join_ensures2";
    62 val ok_SKIP1 = thm "ok_SKIP1";
    63 val ok_SKIP2 = thm "ok_SKIP2";
    64 val ok_Join_commute = thm "ok_Join_commute";
    65 val ok_commute = thm "ok_commute";
    66 val ok_sym = thm "ok_sym";
    67 val ok_iff_OK = thm "ok_iff_OK";
    68 val ok_Join_iff1 = thm "ok_Join_iff1";
    69 val ok_Join_iff2 = thm "ok_Join_iff2";
    70 val ok_Join_commute_I = thm "ok_Join_commute_I";
    71 val ok_JN_iff1 = thm "ok_JN_iff1";
    72 val ok_JN_iff2 = thm "ok_JN_iff2";
    73 val OK_iff_ok = thm "OK_iff_ok";
    74 val OK_imp_ok = thm "OK_imp_ok";
    75 val Allowed_SKIP = thm "Allowed_SKIP";
    76 val Allowed_Join = thm "Allowed_Join";
    77 val Allowed_JN = thm "Allowed_JN";
    78 val ok_iff_Allowed = thm "ok_iff_Allowed";
    79 val OK_iff_Allowed = thm "OK_iff_Allowed";
    80 val safety_prop_Acts_iff = thm "safety_prop_Acts_iff";
    81 val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
    82 val Allowed_eq = thm "Allowed_eq";
    83 val def_prg_Allowed = thm "def_prg_Allowed";
    84 val safety_prop_constrains = thm "safety_prop_constrains";
    85 val safety_prop_stable = thm "safety_prop_stable";
    86 val safety_prop_Int = thm "safety_prop_Int";
    87 val safety_prop_INTER1 = thm "safety_prop_INTER1";
    88 val safety_prop_INTER = thm "safety_prop_INTER";
    89 val def_UNION_ok_iff = thm "def_UNION_ok_iff";
    90 
    91 (*Comp*)
    92 val preserves_def = thm "preserves_def";
    93 val funPair_def = thm "funPair_def";
    94 val componentI = thm "componentI";
    95 val component_eq_subset = thm "component_eq_subset";
    96 val component_SKIP = thm "component_SKIP";
    97 val component_refl = thm "component_refl";
    98 val SKIP_minimal = thm "SKIP_minimal";
    99 val component_Join1 = thm "component_Join1";
   100 val component_Join2 = thm "component_Join2";
   101 val Join_absorb1 = thm "Join_absorb1";
   102 val Join_absorb2 = thm "Join_absorb2";
   103 val JN_component_iff = thm "JN_component_iff";
   104 val component_JN = thm "component_JN";
   105 val component_trans = thm "component_trans";
   106 val component_antisym = thm "component_antisym";
   107 val Join_component_iff = thm "Join_component_iff";
   108 val component_constrains = thm "component_constrains";
   109 val program_less_le = thm "program_less_le";
   110 val preservesI = thm "preservesI";
   111 val preserves_imp_eq = thm "preserves_imp_eq";
   112 val Join_preserves = thm "Join_preserves";
   113 val JN_preserves = thm "JN_preserves";
   114 val SKIP_preserves = thm "SKIP_preserves";
   115 val funPair_apply = thm "funPair_apply";
   116 val preserves_funPair = thm "preserves_funPair";
   117 val funPair_o_distrib = thm "funPair_o_distrib";
   118 val fst_o_funPair = thm "fst_o_funPair";
   119 val snd_o_funPair = thm "snd_o_funPair";
   120 val subset_preserves_o = thm "subset_preserves_o";
   121 val preserves_subset_stable = thm "preserves_subset_stable";
   122 val preserves_subset_increasing = thm "preserves_subset_increasing";
   123 val preserves_id_subset_stable = thm "preserves_id_subset_stable";
   124 val safety_prop_preserves = thm "safety_prop_preserves";
   125 val stable_localTo_stable2 = thm "stable_localTo_stable2";
   126 val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
   127 val component_of_imp_component = thm "component_of_imp_component";
   128 val component_of_refl = thm "component_of_refl";
   129 val component_of_SKIP = thm "component_of_SKIP";
   130 val component_of_trans = thm "component_of_trans";
   131 val strict_component_of_eq = thm "strict_component_of_eq";
   132 val localize_Init_eq = thm "localize_Init_eq";
   133 val localize_Acts_eq = thm "localize_Acts_eq";
   134 val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
   135 
   136 (*Guar*)
   137 val guar_def = thm "guar_def";
   138 val OK_insert_iff = thm "OK_insert_iff";
   139 val ex1 = thm "ex1";
   140 val ex2 = thm "ex2";
   141 val ex_prop_finite = thm "ex_prop_finite";
   142 val ex_prop_equiv = thm "ex_prop_equiv";
   143 val uv1 = thm "uv1";
   144 val uv2 = thm "uv2";
   145 val uv_prop_finite = thm "uv_prop_finite";
   146 val guaranteesI = thm "guaranteesI";
   147 val guaranteesD = thm "guaranteesD";
   148 val component_guaranteesD = thm "component_guaranteesD";
   149 val guarantees_weaken = thm "guarantees_weaken";
   150 val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV";
   151 val subset_imp_guarantees = thm "subset_imp_guarantees";
   152 val ex_prop_imp = thm "ex_prop_imp";
   153 val guarantees_imp = thm "guarantees_imp";
   154 val ex_prop_equiv2 = thm "ex_prop_equiv2";
   155 val guarantees_UN_left = thm "guarantees_UN_left";
   156 val guarantees_Un_left = thm "guarantees_Un_left";
   157 val guarantees_INT_right = thm "guarantees_INT_right";
   158 val guarantees_Int_right = thm "guarantees_Int_right";
   159 val guarantees_Int_right_I = thm "guarantees_Int_right_I";
   160 val guarantees_INT_right_iff = thm "guarantees_INT_right_iff";
   161 val shunting = thm "shunting";
   162 val contrapositive = thm "contrapositive";
   163 val combining1 = thm "combining1";
   164 val combining2 = thm "combining2";
   165 val all_guarantees = thm "all_guarantees";
   166 val ex_guarantees = thm "ex_guarantees";
   167 val guarantees_Join_Int = thm "guarantees_Join_Int";
   168 val guarantees_Join_Un = thm "guarantees_Join_Un";
   169 val guarantees_JN_INT = thm "guarantees_JN_INT";
   170 val guarantees_JN_UN = thm "guarantees_JN_UN";
   171 val guarantees_Join_I1 = thm "guarantees_Join_I1";
   172 val guarantees_Join_I2 = thm "guarantees_Join_I2";
   173 val guarantees_JN_I = thm "guarantees_JN_I";
   174 val Join_welldef_D1 = thm "Join_welldef_D1";
   175 val Join_welldef_D2 = thm "Join_welldef_D2";
   176 val refines_refl = thm "refines_refl";
   177 val ex_refinement_thm = thm "ex_refinement_thm";
   178 val uv_refinement_thm = thm "uv_refinement_thm";
   179 val guarantees_equiv = thm "guarantees_equiv";
   180 val wg_weakest = thm "wg_weakest";
   181 val wg_guarantees = thm "wg_guarantees";
   182 val wg_equiv = thm "wg_equiv";
   183 val component_of_wg = thm "component_of_wg";
   184 val wg_finite = thm "wg_finite";
   185 val wg_ex_prop = thm "wg_ex_prop";
   186 val wx_subset = thm "wx_subset";
   187 val wx_ex_prop = thm "wx_ex_prop";
   188 val wx_weakest = thm "wx_weakest";
   189 val wx'_ex_prop = thm "wx'_ex_prop";
   190 val wx_equiv = thm "wx_equiv";
   191 val guarantees_wx_eq = thm "guarantees_wx_eq";
   192 val stable_guarantees_Always = thm "stable_guarantees_Always";
   193 val leadsTo_Basis = thm "leadsTo_Basis";
   194 val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo";
   195 
   196 (*Extend*)
   197 val Restrict_iff = thm "Restrict_iff";
   198 val Restrict_UNIV = thm "Restrict_UNIV";
   199 val Restrict_empty = thm "Restrict_empty";
   200 val Restrict_Int = thm "Restrict_Int";
   201 val Restrict_triv = thm "Restrict_triv";
   202 val Restrict_subset = thm "Restrict_subset";
   203 val Restrict_eq_mono = thm "Restrict_eq_mono";
   204 val Restrict_imageI = thm "Restrict_imageI";
   205 val Domain_Restrict = thm "Domain_Restrict";
   206 val Image_Restrict = thm "Image_Restrict";
   207 val insert_Id_image_Acts = thm "insert_Id_image_Acts";
   208 val good_mapI = thm "good_mapI";
   209 val good_map_is_surj = thm "good_map_is_surj";
   210 val fst_inv_equalityI = thm "fst_inv_equalityI";
   211 val project_set_iff = thm "project_set_iff";
   212 val extend_set_mono = thm "extend_set_mono";
   213 val extend_set_empty = thm "extend_set_empty";
   214 val project_set_Int_subset = thm "project_set_Int_subset";
   215 val Init_extend = thm "Init_extend";
   216 val Init_project = thm "Init_project";
   217 val Acts_project = thm "Acts_project";
   218 val project_set_UNIV = thm "project_set_UNIV";
   219 val project_set_Union = thm "project_set_Union";
   220 val project_act_mono = thm "project_act_mono";
   221 val project_constrains_project_set = thm "project_constrains_project_set";
   222 val project_stable_project_set = thm "project_stable_project_set";
   223 
   224 
   225 (*Rename*)
   226 val good_map_bij = thm "good_map_bij";
   227 val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv";
   228 val mem_rename_set_iff = thm "mem_rename_set_iff";
   229 val extend_set_eq_image = thm "extend_set_eq_image";
   230 val Init_rename = thm "Init_rename";
   231 val extend_set_inv = thm "extend_set_inv";
   232 val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act";
   233 val bij_extend_act = thm "bij_extend_act";
   234 val bij_project_act = thm "bij_project_act";
   235 val bij_inv_project_act_eq = thm "bij_inv_project_act_eq";
   236 val Acts_project = thm "Acts_project";
   237 val extend_inv = thm "extend_inv";
   238 val rename_inv_rename = thm "rename_inv_rename";
   239 val rename_rename_inv = thm "rename_rename_inv";
   240 val rename_inv_eq = thm "rename_inv_eq";
   241 val bij_extend = thm "bij_extend";
   242 val bij_project = thm "bij_project";
   243 val inv_project_eq = thm "inv_project_eq";
   244 val Allowed_rename = thm "Allowed_rename";
   245 val bij_rename = thm "bij_rename";
   246 val surj_rename = thm "surj_rename";
   247 val inj_rename_imp_inj = thm "inj_rename_imp_inj";
   248 val surj_rename_imp_surj = thm "surj_rename_imp_surj";
   249 val bij_rename_imp_bij = thm "bij_rename_imp_bij";
   250 val bij_rename_iff = thm "bij_rename_iff";
   251 val rename_SKIP = thm "rename_SKIP";
   252 val rename_Join = thm "rename_Join";
   253 val rename_JN = thm "rename_JN";
   254 val rename_constrains = thm "rename_constrains";
   255 val rename_stable = thm "rename_stable";
   256 val rename_invariant = thm "rename_invariant";
   257 val rename_increasing = thm "rename_increasing";
   258 val reachable_rename_eq = thm "reachable_rename_eq";
   259 val rename_Constrains = thm "rename_Constrains";
   260 val rename_Stable = thm "rename_Stable";
   261 val rename_Always = thm "rename_Always";
   262 val rename_Increasing = thm "rename_Increasing";
   263 val rename_transient = thm "rename_transient";
   264 val rename_ensures = thm "rename_ensures";
   265 val rename_leadsTo = thm "rename_leadsTo";
   266 val rename_LeadsTo = thm "rename_LeadsTo";
   267 val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq";
   268 val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv";
   269 val rename_preserves = thm "rename_preserves";
   270 val ok_rename_iff = thm "ok_rename_iff";
   271 val OK_rename_iff = thm "OK_rename_iff";
   272 val bij_eq_rename = thm "bij_eq_rename";
   273 val rename_image_constrains = thm "rename_image_constrains";
   274 val rename_image_stable = thm "rename_image_stable";
   275 val rename_image_increasing = thm "rename_image_increasing";
   276 val rename_image_invariant = thm "rename_image_invariant";
   277 val rename_image_Constrains = thm "rename_image_Constrains";
   278 val rename_image_preserves = thm "rename_image_preserves";
   279 val rename_image_Stable = thm "rename_image_Stable";
   280 val rename_image_Increasing = thm "rename_image_Increasing";
   281 val rename_image_Always = thm "rename_image_Always";
   282 val rename_image_leadsTo = thm "rename_image_leadsTo";
   283 val rename_image_LeadsTo = thm "rename_image_LeadsTo";
   284 
   285 
   286 
   287 (*Lift_prog*)
   288 val sub_def = thm "sub_def";
   289 val lift_map_def = thm "lift_map_def";
   290 val drop_map_def = thm "drop_map_def";
   291 val insert_map_inverse = thm "insert_map_inverse";
   292 val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
   293 val insert_map_inject1 = thm "insert_map_inject1";
   294 val insert_map_inject2 = thm "insert_map_inject2";
   295 val insert_map_inject = thm "insert_map_inject";
   296 val insert_map_inject = thm "insert_map_inject";
   297 val lift_map_eq_iff = thm "lift_map_eq_iff";
   298 val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
   299 val inj_lift_map = thm "inj_lift_map";
   300 val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
   301 val drop_map_inject = thm "drop_map_inject";
   302 val surj_lift_map = thm "surj_lift_map";
   303 val bij_lift_map = thm "bij_lift_map";
   304 val inv_lift_map_eq = thm "inv_lift_map_eq";
   305 val inv_drop_map_eq = thm "inv_drop_map_eq";
   306 val bij_drop_map = thm "bij_drop_map";
   307 val sub_apply = thm "sub_apply";
   308 val lift_set_empty = thm "lift_set_empty";
   309 val lift_set_iff = thm "lift_set_iff";
   310 val lift_set_iff2 = thm "lift_set_iff2";
   311 val lift_set_mono = thm "lift_set_mono";
   312 val lift_set_Un_distrib = thm "lift_set_Un_distrib";
   313 val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
   314 val bij_lift = thm "bij_lift";
   315 val lift_SKIP = thm "lift_SKIP";
   316 val lift_Join = thm "lift_Join";
   317 val lift_JN = thm "lift_JN";
   318 val lift_constrains = thm "lift_constrains";
   319 val lift_stable = thm "lift_stable";
   320 val lift_invariant = thm "lift_invariant";
   321 val lift_Constrains = thm "lift_Constrains";
   322 val lift_Stable = thm "lift_Stable";
   323 val lift_Always = thm "lift_Always";
   324 val lift_transient = thm "lift_transient";
   325 val lift_ensures = thm "lift_ensures";
   326 val lift_leadsTo = thm "lift_leadsTo";
   327 val lift_LeadsTo = thm "lift_LeadsTo";
   328 val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
   329 val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
   330 val lift_preserves_snd_I = thm "lift_preserves_snd_I";
   331 val delete_map_eqE = thm "delete_map_eqE";
   332 val delete_map_eqE = thm "delete_map_eqE";
   333 val delete_map_neq_apply = thm "delete_map_neq_apply";
   334 val vimage_o_fst_eq = thm "vimage_o_fst_eq";
   335 val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
   336 val mem_lift_act_iff = thm "mem_lift_act_iff";
   337 val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
   338 val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
   339 val insert_map_upd_same = thm "insert_map_upd_same";
   340 val insert_map_upd = thm "insert_map_upd";
   341 val insert_map_eq_diff = thm "insert_map_eq_diff";
   342 val lift_map_eq_diff = thm "lift_map_eq_diff";
   343 val lift_transient_eq_disj = thm "lift_transient_eq_disj";
   344 val lift_map_image_Times = thm "lift_map_image_Times";
   345 val lift_preserves_eq = thm "lift_preserves_eq";
   346 val lift_preserves_sub = thm "lift_preserves_sub";
   347 val o_equiv_assoc = thm "o_equiv_assoc";
   348 val o_equiv_apply = thm "o_equiv_apply";
   349 val fst_o_lift_map = thm "fst_o_lift_map";
   350 val snd_o_lift_map = thm "snd_o_lift_map";
   351 val extend_act_extend_act = thm "extend_act_extend_act";
   352 val project_act_project_act = thm "project_act_project_act";
   353 val project_act_extend_act = thm "project_act_extend_act";
   354 val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
   355 val UNION_OK_lift_I = thm "UNION_OK_lift_I";
   356 val OK_lift_I = thm "OK_lift_I";
   357 val Allowed_lift = thm "Allowed_lift";
   358 val lift_image_preserves = thm "lift_image_preserves";
   359 
   360 
   361 (*PPROD*)
   362 val Init_PLam = thm "Init_PLam";
   363 val PLam_empty = thm "PLam_empty";
   364 val PLam_SKIP = thm "PLam_SKIP";
   365 val PLam_insert = thm "PLam_insert";
   366 val PLam_component_iff = thm "PLam_component_iff";
   367 val component_PLam = thm "component_PLam";
   368 val PLam_constrains = thm "PLam_constrains";
   369 val PLam_stable = thm "PLam_stable";
   370 val PLam_transient = thm "PLam_transient";
   371 val PLam_ensures = thm "PLam_ensures";
   372 val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
   373 val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
   374 val PLam_preserves_fst = thm "PLam_preserves_fst";
   375 val PLam_preserves_snd = thm "PLam_preserves_snd";
   376 val guarantees_PLam_I = thm "guarantees_PLam_I";
   377 val Allowed_PLam = thm "Allowed_PLam";
   378 val PLam_preserves = thm "PLam_preserves";
   379 
   380 
   381 (*proves "co" properties when the program is specified*)
   382 fun gen_constrains_tac(cs,ss) i = 
   383    SELECT_GOAL
   384       (EVERY [REPEAT (Always_Int_tac 1),
   385 	      REPEAT (etac Always_ConstrainsI 1
   386 		      ORELSE
   387 		      resolve_tac [StableI, stableI,
   388 				   constrains_imp_Constrains] 1),
   389 	      rtac constrainsI 1,
   390 	      full_simp_tac ss 1,
   391 	      REPEAT (FIRSTGOAL (etac disjE)),
   392 	      ALLGOALS (clarify_tac cs),
   393 	      ALLGOALS (asm_lr_simp_tac ss)]) i;
   394 
   395 (*proves "ensures/leadsTo" properties when the program is specified*)
   396 fun gen_ensures_tac(cs,ss) sact = 
   397     SELECT_GOAL
   398       (EVERY [REPEAT (Always_Int_tac 1),
   399 	      etac Always_LeadsTo_Basis 1 
   400 	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   401 		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
   402 				    EnsuresI, ensuresI] 1),
   403 	      (*now there are two subgoals: co & transient*)
   404 	      simp_tac ss 2,
   405 	      res_inst_tac [("act", sact)] transientI 2,
   406                  (*simplify the command's domain*)
   407 	      simp_tac (ss addsimps [Domain_def]) 3,
   408 	      gen_constrains_tac (cs,ss) 1,
   409 	      ALLGOALS (clarify_tac cs),
   410 	      ALLGOALS (asm_lr_simp_tac ss)]);
   411 
   412 
   413 (*Composition equivalences, from Lift_prog*)
   414 
   415 fun make_o_equivs th =
   416     [th,
   417      th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
   418      th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
   419 
   420 Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
   421 
   422 Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);