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