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