src/Tools/atomize_elim.ML
author wenzelm
Sat Aug 16 13:23:50 2014 +0200 (2014-08-16)
changeset 57948 75724d71013c
parent 54742 7a86358a3c0b
child 57949 b203a7644bf1
permissions -rw-r--r--
modernized module name and setup;
     1 (*  Title:      Tools/atomize_elim.ML
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     4 Turn elimination rules into atomic expressions in the object logic.
     5 *)
     6 
     7 signature ATOMIZE_ELIM =
     8 sig
     9   val declare_atomize_elim : attribute
    10   val atomize_elim_conv : Proof.context -> conv
    11   val full_atomize_elim_conv : Proof.context -> conv
    12   val atomize_elim_tac : Proof.context -> int -> tactic
    13 end
    14 
    15 structure Atomize_Elim : ATOMIZE_ELIM =
    16 struct
    17 
    18 (* theory data *)
    19 
    20 structure AtomizeElimData = Named_Thms
    21 (
    22   val name = @{binding atomize_elim};
    23   val description = "atomize_elim rewrite rule";
    24 );
    25 
    26 val _ = Theory.setup AtomizeElimData.setup;
    27 
    28 val declare_atomize_elim = AtomizeElimData.add
    29 
    30 (* More conversions: *)
    31 local open Conv in
    32 
    33 (* Compute inverse permutation *)
    34 fun invert_perm pi =
    35       (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0)))
    36            |> map_index I
    37            |> sort (int_ord o pairself snd)
    38            |> map fst
    39 
    40 (* rearrange_prems as a conversion *)
    41 fun rearrange_prems_conv pi ct =
    42     let
    43       val pi' = 0 :: map (Integer.add 1) pi
    44       val fwd  = Thm.trivial ct
    45                   |> Drule.rearrange_prems pi'
    46       val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
    47                   |> Drule.rearrange_prems (invert_perm pi')
    48     in Thm.equal_intr fwd back end
    49 
    50 
    51 (* convert !!thesis. (!!x y z. ... => thesis) ==> ...
    52                      ==> (!!a b c. ... => thesis)
    53                      ==> thesis
    54 
    55    to
    56 
    57    (EX x y z. ...) | ... | (EX a b c. ...)
    58 *)
    59 fun atomize_elim_conv ctxt ct =
    60     (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
    61     then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt)
    62     then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
    63                          then all_conv ct'
    64                          else raise CTERM ("atomize_elim", [ct', ct])))
    65     ct
    66 
    67 
    68 (* Move the thesis-quantifier inside over other quantifiers and unrelated prems *)
    69 fun thesis_miniscope_conv inner_cv ctxt =
    70     let
    71       (* check if the outermost quantifier binds the conclusion *)
    72       fun is_forall_thesis t =
    73           case Logic.strip_assums_concl t of
    74             (_ $ Bound i) => i = length (Logic.strip_params t) - 1
    75           | _ => false
    76 
    77       (* move unrelated assumptions out of the quantification *)
    78       fun movea_conv ctxt ct =
    79           let
    80             val _ $ Abs (_, _, b) = term_of ct
    81             val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i)
    82                        (Logic.strip_imp_prems b) []
    83                        |> rev
    84 
    85             fun skip_over_assm cv = rewr_conv (Thm.symmetric Drule.norm_hhf_eq)
    86                                     then_conv (implies_concl_conv cv)
    87           in
    88             (forall_conv (K (rearrange_prems_conv idxs)) ctxt
    89              then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt)))
    90             ct
    91           end
    92 
    93       (* move current quantifier to the right *)
    94       fun moveq_conv ctxt =
    95           (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
    96           else_conv (movea_conv ctxt)
    97 
    98       fun ms_conv ctxt ct =
    99           if is_forall_thesis (term_of ct)
   100           then moveq_conv ctxt ct
   101           else (implies_concl_conv (ms_conv ctxt)
   102             else_conv
   103             (forall_conv (ms_conv o snd) ctxt))
   104             ct
   105     in
   106       ms_conv ctxt
   107     end
   108 
   109 val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
   110 
   111 end
   112 
   113 
   114 fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) =>
   115     let
   116       val thy = Proof_Context.theory_of ctxt
   117       val _ $ thesis = Logic.strip_assums_concl subg
   118 
   119       (* Introduce a quantifier first if the thesis is not bound *)
   120       val quantify_thesis =
   121           if is_Bound thesis then all_tac
   122           else let
   123               val cthesis = cterm_of thy thesis
   124               val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
   125                          @{thm meta_spec}
   126             in
   127               compose_tac (false, rule, 1) i
   128             end
   129     in
   130       quantify_thesis
   131       THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
   132     end)
   133 
   134 val _ =
   135   Theory.setup
   136     (Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
   137       "convert obtains statement to atomic object logic goal")
   138 
   139 end