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