src/Tools/atomize_elim.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45294 3c5d3d286055
child 54742 7a86358a3c0b
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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 *)
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30515
diff changeset
    23
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30515
diff changeset
    24
structure AtomizeElimData = Named_Thms
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30515
diff changeset
    25
(
45294
3c5d3d286055 tuned Named_Thms: proper binding;
wenzelm
parents: 42361
diff changeset
    26
  val name = @{binding atomize_elim};
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    27
  val description = "atomize_elim rewrite rule";
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    28
);
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    29
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    30
val declare_atomize_elim = AtomizeElimData.add
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    31
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    32
(* More conversions: *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    33
local open Conv in
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    34
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    35
(* Compute inverse permutation *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    36
fun invert_perm pi =
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33029
diff changeset
    37
      (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0)))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    38
           |> map_index I
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    39
           |> sort (int_ord o pairself snd)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    40
           |> map fst
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    41
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    42
(* rearrange_prems as a conversion *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    43
fun rearrange_prems_conv pi ct =
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    44
    let
33002
f3f02f36a3e2 uniform use of Integer.add/mult/sum/prod;
wenzelm
parents: 31902
diff changeset
    45
      val pi' = 0 :: map (Integer.add 1) pi
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    46
      val fwd  = Thm.trivial ct
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    47
                  |> Drule.rearrange_prems pi'
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    48
      val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    49
                  |> Drule.rearrange_prems (invert_perm pi')
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    50
    in Thm.equal_intr fwd back end
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    51
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    52
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    53
(* convert !!thesis. (!!x y z. ... => thesis) ==> ... 
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    54
                     ==> (!!a b c. ... => thesis)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    55
                     ==> thesis
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    56
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    57
   to
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    58
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    59
   (EX x y z. ...) | ... | (EX a b c. ...)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    60
*)
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    61
fun atomize_elim_conv ctxt ct =
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 33040
diff changeset
    62
    (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 35625
diff changeset
    63
    then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 33040
diff changeset
    64
    then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    65
                         then all_conv ct'
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    66
                         else raise CTERM ("atomize_elim", [ct', ct])))
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    67
    ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    68
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    69
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    70
(* Move the thesis-quantifier inside over other quantifiers and unrelated prems *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    71
fun thesis_miniscope_conv inner_cv ctxt =
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    72
    let
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    73
      (* check if the outermost quantifier binds the conclusion *)
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    74
      fun is_forall_thesis t = 
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    75
          case Logic.strip_assums_concl t of
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    76
            (_ $ Bound i) => i = length (Logic.strip_params t) - 1
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    77
          | _ => false
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    78
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    79
      (* move unrelated assumptions out of the quantification *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    80
      fun movea_conv ctxt ct =
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    81
          let
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    82
            val _ $ Abs (_, _, b) = term_of ct
42083
e1209fc7ecdc added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents: 41228
diff changeset
    83
            val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i)
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    84
                       (Logic.strip_imp_prems b) []
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    85
                       |> rev
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    86
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    87
            fun skip_over_assm cv = rewr_conv (Thm.symmetric Drule.norm_hhf_eq)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    88
                                    then_conv (implies_concl_conv cv)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    89
          in
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    90
            (forall_conv (K (rearrange_prems_conv idxs)) ctxt
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    91
             then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt)))
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    92
            ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    93
          end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    94
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    95
      (* move current quantifier to the right *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    96
      fun moveq_conv ctxt = 
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    97
          (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    98
          else_conv (movea_conv ctxt)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    99
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   100
      fun ms_conv ctxt ct = 
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   101
          if is_forall_thesis (term_of ct)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   102
          then moveq_conv ctxt ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   103
          else (implies_concl_conv (ms_conv ctxt)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   104
            else_conv
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   105
            (forall_conv (ms_conv o snd) ctxt))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   106
            ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   107
    in
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   108
      ms_conv ctxt 
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   109
    end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   110
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   111
val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   112
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   113
end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   114
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   115
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   116
fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) =>
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   117
    let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42083
diff changeset
   118
      val thy = Proof_Context.theory_of ctxt
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   119
      val _ $ thesis = Logic.strip_assums_concl subg
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   120
                       
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   121
      (* Introduce a quantifier first if the thesis is not bound *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   122
      val quantify_thesis = 
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   123
          if is_Bound thesis then all_tac
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   124
          else let
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   125
              val cthesis = cterm_of thy thesis
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   126
              val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] 
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   127
                         @{thm meta_spec}
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   128
            in
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   129
              compose_tac (false, rule, 1) i
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   130
            end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   131
    in
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   132
      quantify_thesis
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   133
      THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   134
    end)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   135
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30510
diff changeset
   136
val setup =
bca05b17b618 simplified method setup;
wenzelm
parents: 30510
diff changeset
   137
  Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
bca05b17b618 simplified method setup;
wenzelm
parents: 30510
diff changeset
   138
    "convert obtains statement to atomic object logic goal"
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   139
  #> AtomizeElimData.setup
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   140
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   141
end