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