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