src/HOL/UNITY/UNITY_tactics.ML
author paulson
Wed Jan 29 11:02:08 2003 +0100 (2003-01-29)
changeset 13790 8d7e9fce8c50
parent 13786 ab8f39f48a6f
child 13792 d1811693899c
permissions -rw-r--r--
converting UNITY to new-style theories
     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 (*Extend*)
    10 val Restrict_iff = thm "Restrict_iff";
    11 val Restrict_UNIV = thm "Restrict_UNIV";
    12 val Restrict_empty = thm "Restrict_empty";
    13 val Restrict_Int = thm "Restrict_Int";
    14 val Restrict_triv = thm "Restrict_triv";
    15 val Restrict_subset = thm "Restrict_subset";
    16 val Restrict_eq_mono = thm "Restrict_eq_mono";
    17 val Restrict_imageI = thm "Restrict_imageI";
    18 val Domain_Restrict = thm "Domain_Restrict";
    19 val Image_Restrict = thm "Image_Restrict";
    20 val insert_Id_image_Acts = thm "insert_Id_image_Acts";
    21 val good_mapI = thm "good_mapI";
    22 val good_map_is_surj = thm "good_map_is_surj";
    23 val fst_inv_equalityI = thm "fst_inv_equalityI";
    24 val project_set_iff = thm "project_set_iff";
    25 val extend_set_mono = thm "extend_set_mono";
    26 val extend_set_empty = thm "extend_set_empty";
    27 val project_set_Int_subset = thm "project_set_Int_subset";
    28 val Init_extend = thm "Init_extend";
    29 val Init_project = thm "Init_project";
    30 val Acts_project = thm "Acts_project";
    31 val project_set_UNIV = thm "project_set_UNIV";
    32 val project_set_Union = thm "project_set_Union";
    33 val project_act_mono = thm "project_act_mono";
    34 val project_constrains_project_set = thm "project_constrains_project_set";
    35 val project_stable_project_set = thm "project_stable_project_set";
    36 
    37 
    38 (*Rename*)
    39 val good_map_bij = thm "good_map_bij";
    40 val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv";
    41 val mem_rename_set_iff = thm "mem_rename_set_iff";
    42 val extend_set_eq_image = thm "extend_set_eq_image";
    43 val Init_rename = thm "Init_rename";
    44 val extend_set_inv = thm "extend_set_inv";
    45 val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act";
    46 val bij_extend_act = thm "bij_extend_act";
    47 val bij_project_act = thm "bij_project_act";
    48 val bij_inv_project_act_eq = thm "bij_inv_project_act_eq";
    49 val Acts_project = thm "Acts_project";
    50 val extend_inv = thm "extend_inv";
    51 val rename_inv_rename = thm "rename_inv_rename";
    52 val rename_rename_inv = thm "rename_rename_inv";
    53 val rename_inv_eq = thm "rename_inv_eq";
    54 val bij_extend = thm "bij_extend";
    55 val bij_project = thm "bij_project";
    56 val inv_project_eq = thm "inv_project_eq";
    57 val Allowed_rename = thm "Allowed_rename";
    58 val bij_rename = thm "bij_rename";
    59 val surj_rename = thm "surj_rename";
    60 val inj_rename_imp_inj = thm "inj_rename_imp_inj";
    61 val surj_rename_imp_surj = thm "surj_rename_imp_surj";
    62 val bij_rename_imp_bij = thm "bij_rename_imp_bij";
    63 val bij_rename_iff = thm "bij_rename_iff";
    64 val rename_SKIP = thm "rename_SKIP";
    65 val rename_Join = thm "rename_Join";
    66 val rename_JN = thm "rename_JN";
    67 val rename_constrains = thm "rename_constrains";
    68 val rename_stable = thm "rename_stable";
    69 val rename_invariant = thm "rename_invariant";
    70 val rename_increasing = thm "rename_increasing";
    71 val reachable_rename_eq = thm "reachable_rename_eq";
    72 val rename_Constrains = thm "rename_Constrains";
    73 val rename_Stable = thm "rename_Stable";
    74 val rename_Always = thm "rename_Always";
    75 val rename_Increasing = thm "rename_Increasing";
    76 val rename_transient = thm "rename_transient";
    77 val rename_ensures = thm "rename_ensures";
    78 val rename_leadsTo = thm "rename_leadsTo";
    79 val rename_LeadsTo = thm "rename_LeadsTo";
    80 val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq";
    81 val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv";
    82 val rename_preserves = thm "rename_preserves";
    83 val ok_rename_iff = thm "ok_rename_iff";
    84 val OK_rename_iff = thm "OK_rename_iff";
    85 val bij_eq_rename = thm "bij_eq_rename";
    86 val rename_image_constrains = thm "rename_image_constrains";
    87 val rename_image_stable = thm "rename_image_stable";
    88 val rename_image_increasing = thm "rename_image_increasing";
    89 val rename_image_invariant = thm "rename_image_invariant";
    90 val rename_image_Constrains = thm "rename_image_Constrains";
    91 val rename_image_preserves = thm "rename_image_preserves";
    92 val rename_image_Stable = thm "rename_image_Stable";
    93 val rename_image_Increasing = thm "rename_image_Increasing";
    94 val rename_image_Always = thm "rename_image_Always";
    95 val rename_image_leadsTo = thm "rename_image_leadsTo";
    96 val rename_image_LeadsTo = thm "rename_image_LeadsTo";
    97 
    98 
    99 
   100 (*Lift_prog*)
   101 val sub_def = thm "sub_def";
   102 val lift_map_def = thm "lift_map_def";
   103 val drop_map_def = thm "drop_map_def";
   104 val insert_map_inverse = thm "insert_map_inverse";
   105 val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
   106 val insert_map_inject1 = thm "insert_map_inject1";
   107 val insert_map_inject2 = thm "insert_map_inject2";
   108 val insert_map_inject = thm "insert_map_inject";
   109 val insert_map_inject = thm "insert_map_inject";
   110 val lift_map_eq_iff = thm "lift_map_eq_iff";
   111 val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
   112 val inj_lift_map = thm "inj_lift_map";
   113 val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
   114 val drop_map_inject = thm "drop_map_inject";
   115 val surj_lift_map = thm "surj_lift_map";
   116 val bij_lift_map = thm "bij_lift_map";
   117 val inv_lift_map_eq = thm "inv_lift_map_eq";
   118 val inv_drop_map_eq = thm "inv_drop_map_eq";
   119 val bij_drop_map = thm "bij_drop_map";
   120 val sub_apply = thm "sub_apply";
   121 val lift_set_empty = thm "lift_set_empty";
   122 val lift_set_iff = thm "lift_set_iff";
   123 val lift_set_iff2 = thm "lift_set_iff2";
   124 val lift_set_mono = thm "lift_set_mono";
   125 val lift_set_Un_distrib = thm "lift_set_Un_distrib";
   126 val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
   127 val bij_lift = thm "bij_lift";
   128 val lift_SKIP = thm "lift_SKIP";
   129 val lift_Join = thm "lift_Join";
   130 val lift_JN = thm "lift_JN";
   131 val lift_constrains = thm "lift_constrains";
   132 val lift_stable = thm "lift_stable";
   133 val lift_invariant = thm "lift_invariant";
   134 val lift_Constrains = thm "lift_Constrains";
   135 val lift_Stable = thm "lift_Stable";
   136 val lift_Always = thm "lift_Always";
   137 val lift_transient = thm "lift_transient";
   138 val lift_ensures = thm "lift_ensures";
   139 val lift_leadsTo = thm "lift_leadsTo";
   140 val lift_LeadsTo = thm "lift_LeadsTo";
   141 val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
   142 val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
   143 val lift_preserves_snd_I = thm "lift_preserves_snd_I";
   144 val delete_map_eqE = thm "delete_map_eqE";
   145 val delete_map_eqE = thm "delete_map_eqE";
   146 val delete_map_neq_apply = thm "delete_map_neq_apply";
   147 val vimage_o_fst_eq = thm "vimage_o_fst_eq";
   148 val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
   149 val mem_lift_act_iff = thm "mem_lift_act_iff";
   150 val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
   151 val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
   152 val insert_map_upd_same = thm "insert_map_upd_same";
   153 val insert_map_upd = thm "insert_map_upd";
   154 val insert_map_eq_diff = thm "insert_map_eq_diff";
   155 val lift_map_eq_diff = thm "lift_map_eq_diff";
   156 val lift_transient_eq_disj = thm "lift_transient_eq_disj";
   157 val lift_map_image_Times = thm "lift_map_image_Times";
   158 val lift_preserves_eq = thm "lift_preserves_eq";
   159 val lift_preserves_sub = thm "lift_preserves_sub";
   160 val o_equiv_assoc = thm "o_equiv_assoc";
   161 val o_equiv_apply = thm "o_equiv_apply";
   162 val fst_o_lift_map = thm "fst_o_lift_map";
   163 val snd_o_lift_map = thm "snd_o_lift_map";
   164 val extend_act_extend_act = thm "extend_act_extend_act";
   165 val project_act_project_act = thm "project_act_project_act";
   166 val project_act_extend_act = thm "project_act_extend_act";
   167 val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
   168 val UNION_OK_lift_I = thm "UNION_OK_lift_I";
   169 val OK_lift_I = thm "OK_lift_I";
   170 val Allowed_lift = thm "Allowed_lift";
   171 val lift_image_preserves = thm "lift_image_preserves";
   172 
   173 
   174 (*PPROD*)
   175 val Init_PLam = thm "Init_PLam";
   176 val PLam_empty = thm "PLam_empty";
   177 val PLam_SKIP = thm "PLam_SKIP";
   178 val PLam_insert = thm "PLam_insert";
   179 val PLam_component_iff = thm "PLam_component_iff";
   180 val component_PLam = thm "component_PLam";
   181 val PLam_constrains = thm "PLam_constrains";
   182 val PLam_stable = thm "PLam_stable";
   183 val PLam_transient = thm "PLam_transient";
   184 val PLam_ensures = thm "PLam_ensures";
   185 val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
   186 val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
   187 val PLam_preserves_fst = thm "PLam_preserves_fst";
   188 val PLam_preserves_snd = thm "PLam_preserves_snd";
   189 val guarantees_PLam_I = thm "guarantees_PLam_I";
   190 val Allowed_PLam = thm "Allowed_PLam";
   191 val PLam_preserves = thm "PLam_preserves";
   192 
   193 
   194 (*proves "co" properties when the program is specified*)
   195 fun gen_constrains_tac(cs,ss) i = 
   196    SELECT_GOAL
   197       (EVERY [REPEAT (Always_Int_tac 1),
   198 	      REPEAT (etac Always_ConstrainsI 1
   199 		      ORELSE
   200 		      resolve_tac [StableI, stableI,
   201 				   constrains_imp_Constrains] 1),
   202 	      rtac constrainsI 1,
   203 	      full_simp_tac ss 1,
   204 	      REPEAT (FIRSTGOAL (etac disjE)),
   205 	      ALLGOALS (clarify_tac cs),
   206 	      ALLGOALS (asm_lr_simp_tac ss)]) i;
   207 
   208 (*proves "ensures/leadsTo" properties when the program is specified*)
   209 fun gen_ensures_tac(cs,ss) sact = 
   210     SELECT_GOAL
   211       (EVERY [REPEAT (Always_Int_tac 1),
   212 	      etac Always_LeadsTo_Basis 1 
   213 	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   214 		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
   215 				    EnsuresI, ensuresI] 1),
   216 	      (*now there are two subgoals: co & transient*)
   217 	      simp_tac ss 2,
   218 	      res_inst_tac [("act", sact)] transientI 2,
   219                  (*simplify the command's domain*)
   220 	      simp_tac (ss addsimps [Domain_def]) 3,
   221 	      gen_constrains_tac (cs,ss) 1,
   222 	      ALLGOALS (clarify_tac cs),
   223 	      ALLGOALS (asm_lr_simp_tac ss)]);
   224 
   225 
   226 (*Composition equivalences, from Lift_prog*)
   227 
   228 fun make_o_equivs th =
   229     [th,
   230      th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
   231      th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
   232 
   233 Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
   234 
   235 Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);