Nominal-General/nominal_permeq.ML
changeset 2064 2725853f43b9
parent 1947 51f411b1197d
child 2069 2b6ba4d4e19a
equal deleted inserted replaced
2062:65bdcc42badd 2064:2725853f43b9
    95         val b = ctyp_of_term t;
    95         val b = ctyp_of_term t;
    96         val ty_insts = map SOME [b, a]
    96         val ty_insts = map SOME [b, a]
    97         val term_insts = map SOME [p, f, x]                        
    97         val term_insts = map SOME [p, f, x]                        
    98       in
    98       in
    99         if has_bad_head bad_hds trm
    99         if has_bad_head bad_hds trm
   100         then Conv.no_conv ctrm
   100         then Conv.all_conv ctrm
   101         else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
   101         else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
   102       end
   102       end
   103   | _ => Conv.no_conv ctrm
   103   | _ => Conv.no_conv ctrm
   104 
   104 
   105 (* conversion for lambdas *)
   105 (* conversion for lambdas *)
   113    if a permutation on a constant or application cannot be analysed *)
   113    if a permutation on a constant or application cannot be analysed *)
   114 fun progress_info_conv ctxt strict_flag bad_hds ctrm =
   114 fun progress_info_conv ctxt strict_flag bad_hds ctrm =
   115 let
   115 let
   116   fun msg trm =
   116   fun msg trm =
   117     let
   117     let
   118       val hd = head_of trm 
   118       val hd = head_of trm
   119     in 
   119     in 
   120     if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
   120       if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
   121     else (if strict_flag then error else warning) 
   121       else (if strict_flag then error else warning) 
   122            ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
   122              ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
   123     end
   123     end
   124 
   124 
   125   val _ = case (term_of ctrm) of
   125   val _ = case (term_of ctrm) of
   126       Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
   126       Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
   127     | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
   127     | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
   128     | _ => () 
   128     | _ => () 
   129 in
   129 in
   130   Conv.all_conv ctrm 
   130   Conv.all_conv ctrm 
   131 end
   131 end
   132 
   132 
   133 (* main conversion *)
   133 (* main conversion *) 
   134 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
   134 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
   135 let
   135 let
   136   val first_conv_wrapper = 
   136   val first_conv_wrapper = 
   137     if trace_enabled ctxt 
   137     if trace_enabled ctxt 
   138     then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
   138     then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
   148       More_Conv.rewrs_conv post_thms,
   148       More_Conv.rewrs_conv post_thms,
   149       progress_info_conv ctxt strict_flag bad_hds
   149       progress_info_conv ctxt strict_flag bad_hds
   150     ] ctrm
   150     ] ctrm
   151 end
   151 end
   152 
   152 
       
   153 (* the eqvt-tactics first eta-normalise goals in 
       
   154    order to avoid problems with inductions in the
       
   155    equivaraince command. *)
       
   156 
   153 (* raises an error if some permutations cannot be eliminated *)
   157 (* raises an error if some permutations cannot be eliminated *)
   154 fun eqvt_strict_tac ctxt user_thms bad_hds = 
   158 fun eqvt_strict_tac ctxt user_thms bad_hds = 
   155   CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt)
   159   CONVERSION (More_Conv.top_conv 
       
   160     (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt)
   156 
   161 
   157 (* prints a warning message if some permutations cannot be eliminated *)
   162 (* prints a warning message if some permutations cannot be eliminated *)
   158 fun eqvt_tac ctxt user_thms bad_hds = 
   163 fun eqvt_tac ctxt user_thms bad_hds = 
   159   CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt)
   164   CONVERSION (More_Conv.top_conv 
       
   165     (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt)
   160 
   166 
   161 (* setup of the configuration value *)
   167 (* setup of the configuration value *)
   162 val setup =
   168 val setup =
   163   trace_eqvt_setup
   169   trace_eqvt_setup
   164 
   170 
   167 
   173 
   168 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
   174 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
   169 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
   175 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
   170   (Scan.repeat (Args.const true))) []
   176   (Scan.repeat (Args.const true))) []
   171 
   177 
   172 val args_parser =  
   178 val args_parser =  add_thms_parser -- exclude_consts_parser 
   173   add_thms_parser -- exclude_consts_parser ||
       
   174   exclude_consts_parser -- add_thms_parser >> swap
       
   175 
   179 
   176 fun perm_simp_meth (thms, consts) ctxt = 
   180 fun perm_simp_meth (thms, consts) ctxt = 
   177   SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
   181   SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
   178 
   182 
   179 fun perm_strict_simp_meth (thms, consts) ctxt = 
   183 fun perm_strict_simp_meth (thms, consts) ctxt =