src/Tools/atomize_elim.ML
author wenzelm
Sat, 02 Apr 2016 23:29:05 +0200
changeset 62826 eb94e570c1a4
parent 60801 7664e0916eec
child 67149 e61557884799
permissions -rw-r--r--
prefer infix operations;
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
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
     9
  val atomize_elim_conv : Proof.context -> conv
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    10
  val full_atomize_elim_conv : Proof.context -> conv
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    11
  val atomize_elim_tac : Proof.context -> int -> tactic
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    12
end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    13
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
    14
structure Atomize_Elim : ATOMIZE_ELIM =
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    15
struct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    16
57949
b203a7644bf1 updated to named_theorems;
wenzelm
parents: 57948
diff changeset
    17
(* atomize_elim rules *)
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30515
diff changeset
    18
57949
b203a7644bf1 updated to named_theorems;
wenzelm
parents: 57948
diff changeset
    19
val named_theorems =
b203a7644bf1 updated to named_theorems;
wenzelm
parents: 57948
diff changeset
    20
  Context.>>> (Context.map_theory_result
b203a7644bf1 updated to named_theorems;
wenzelm
parents: 57948
diff changeset
    21
   (Named_Target.theory_init #>
b203a7644bf1 updated to named_theorems;
wenzelm
parents: 57948
diff changeset
    22
    Named_Theorems.declare @{binding atomize_elim} "atomize_elim rewrite rule" ##>
b203a7644bf1 updated to named_theorems;
wenzelm
parents: 57948
diff changeset
    23
    Local_Theory.exit_global));
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    24
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    25
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    26
(* More conversions: *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    27
local open Conv in
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    28
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    29
(* Compute inverse permutation *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    30
fun invert_perm pi =
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33029
diff changeset
    31
      (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0)))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    32
           |> map_index I
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58956
diff changeset
    33
           |> sort (int_ord o apply2 snd)
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    34
           |> map fst
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    35
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    36
(* rearrange_prems as a conversion *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    37
fun rearrange_prems_conv pi ct =
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    38
    let
33002
f3f02f36a3e2 uniform use of Integer.add/mult/sum/prod;
wenzelm
parents: 31902
diff changeset
    39
      val pi' = 0 :: map (Integer.add 1) pi
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    40
      val fwd  = Thm.trivial ct
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    41
                  |> Drule.rearrange_prems pi'
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
    42
      val back = Thm.trivial (snd (Thm.dest_implies (Thm.cprop_of fwd)))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    43
                  |> Drule.rearrange_prems (invert_perm pi')
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    44
    in Thm.equal_intr fwd back end
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    45
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    46
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
    47
(* convert !!thesis. (!!x y z. ... => thesis) ==> ...
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    48
                     ==> (!!a b c. ... => thesis)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    49
                     ==> thesis
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    50
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    51
   to
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    52
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    53
   (EX x y z. ...) | ... | (EX a b c. ...)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    54
*)
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    55
fun atomize_elim_conv ctxt ct =
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 45294
diff changeset
    56
    (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
57949
b203a7644bf1 updated to named_theorems;
wenzelm
parents: 57948
diff changeset
    57
    then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems)
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59621
diff changeset
    58
    then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct'
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    59
                         then all_conv ct'
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    60
                         else raise CTERM ("atomize_elim", [ct', ct])))
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    61
    ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    62
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    63
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    64
(* Move the thesis-quantifier inside over other quantifiers and unrelated prems *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    65
fun thesis_miniscope_conv inner_cv ctxt =
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    66
    let
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    67
      (* check if the outermost quantifier binds the conclusion *)
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
    68
      fun is_forall_thesis t =
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    69
          case Logic.strip_assums_concl t of
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    70
            (_ $ Bound i) => i = length (Logic.strip_params t) - 1
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    71
          | _ => false
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    72
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    73
      (* move unrelated assumptions out of the quantification *)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    74
      fun movea_conv ctxt ct =
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    75
          let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
    76
            val _ $ Abs (_, _, b) = Thm.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
    77
            val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i)
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    78
                       (Logic.strip_imp_prems b) []
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    79
                       |> rev
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    80
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    81
            fun skip_over_assm cv = rewr_conv (Thm.symmetric Drule.norm_hhf_eq)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    82
                                    then_conv (implies_concl_conv cv)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    83
          in
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    84
            (forall_conv (K (rearrange_prems_conv idxs)) ctxt
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    85
             then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt)))
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    86
            ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    87
          end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    88
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    89
      (* move current quantifier to the right *)
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
    90
      fun moveq_conv ctxt =
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    91
          (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    92
          else_conv (movea_conv ctxt)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    93
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
    94
      fun ms_conv ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
    95
          if is_forall_thesis (Thm.term_of ct)
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    96
          then moveq_conv ctxt ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    97
          else (implies_concl_conv (ms_conv ctxt)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
    98
            else_conv
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
    99
            (forall_conv (ms_conv o snd) ctxt))
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   100
            ct
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   101
    in
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
   102
      ms_conv ctxt
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   103
    end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   104
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   105
val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   106
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   107
end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   108
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   109
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   110
fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) =>
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   111
    let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42083
diff changeset
   112
      val thy = Proof_Context.theory_of ctxt
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   113
      val _ $ thesis = Logic.strip_assums_concl subg
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
   114
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   115
      (* Introduce a quantifier first if the thesis is not bound *)
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
   116
      val quantify_thesis =
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   117
          if is_Bound thesis then all_tac
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   118
          else let
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59586
diff changeset
   119
              val cthesis = Thm.global_cterm_of thy thesis
60801
7664e0916eec tuned signature;
wenzelm
parents: 59970
diff changeset
   120
              val rule = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   121
                         @{thm meta_spec}
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   122
            in
58956
a816aa3ff391 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents: 57949
diff changeset
   123
              compose_tac ctxt (false, rule, 1) i
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   124
            end
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   125
    in
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   126
      quantify_thesis
27571
69f3981c8ed4 renamed conversions to _conv, tuned
krauss
parents: 26582
diff changeset
   127
      THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   128
    end)
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   129
57948
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
   130
val _ =
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
   131
  Theory.setup
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
   132
    (Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
75724d71013c modernized module name and setup;
wenzelm
parents: 54742
diff changeset
   133
      "convert obtains statement to atomic object logic goal")
26582
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   134
6f9c62d17baa added missing file
krauss
parents:
diff changeset
   135
end