src/HOL/Library/cconv.ML
author noschinl
Mon Apr 13 12:18:47 2015 +0200 (2015-04-13)
changeset 60050 dc6ac152d864
parent 60049 e4a5dfee0f9c
child 60054 ef4878146485
permissions -rw-r--r--
rewrite: propagate premises to new subgoals
wenzelm@59975
     1
(*  Title:      HOL/Library/cconv.ML
wenzelm@59975
     2
    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
wenzelm@59975
     3
wenzelm@59975
     4
FIXME!?
wenzelm@59975
     5
*)
wenzelm@59975
     6
noschinl@59739
     7
infix 1 then_cconv
noschinl@59739
     8
infix 0 else_cconv
noschinl@59739
     9
noschinl@59739
    10
type cconv = conv
noschinl@59739
    11
noschinl@59739
    12
signature BASIC_CCONV =
noschinl@59739
    13
sig
noschinl@59739
    14
  val then_cconv: cconv * cconv -> cconv
noschinl@59739
    15
  val else_cconv: cconv * cconv -> cconv
noschinl@59739
    16
  val CCONVERSION: cconv -> int -> tactic
noschinl@59739
    17
end
noschinl@59739
    18
noschinl@59739
    19
signature CCONV =
noschinl@59739
    20
sig
noschinl@59739
    21
  include BASIC_CCONV
noschinl@59739
    22
  val no_cconv: cconv
noschinl@59739
    23
  val all_cconv: cconv
noschinl@59739
    24
  val first_cconv: cconv list -> cconv
noschinl@59739
    25
  val abs_cconv: (cterm * Proof.context -> cconv) -> Proof.context -> cconv
noschinl@59739
    26
  val combination_cconv: cconv -> cconv -> cconv
noschinl@59739
    27
  val comb_cconv: cconv -> cconv
noschinl@59739
    28
  val arg_cconv: cconv -> cconv
noschinl@59739
    29
  val fun_cconv: cconv -> cconv
noschinl@59739
    30
  val arg1_cconv: cconv -> cconv
noschinl@59739
    31
  val fun2_cconv: cconv -> cconv
noschinl@59739
    32
  val rewr_cconv: thm -> cconv
noschinl@59739
    33
  val rewrs_cconv: thm list -> cconv
noschinl@59739
    34
  val params_cconv: int -> (Proof.context -> cconv) -> Proof.context -> cconv
noschinl@59739
    35
  val prems_cconv: int -> cconv -> cconv
noschinl@59739
    36
  val concl_cconv: int -> cconv -> cconv
noschinl@59739
    37
  val fconv_rule: cconv -> thm -> thm
noschinl@59739
    38
  val gconv_rule: cconv -> int -> thm -> thm
noschinl@59739
    39
end
noschinl@59739
    40
noschinl@59739
    41
structure CConv : CCONV =
noschinl@59739
    42
struct
noschinl@59739
    43
noschinl@59739
    44
val concl_lhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_lhs
noschinl@59739
    45
val concl_rhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_rhs
noschinl@59739
    46
noschinl@59739
    47
fun transitive th1 th2 = Drule.transitive_thm OF [th1, th2]
noschinl@59739
    48
noschinl@59739
    49
val combination_thm =
noschinl@59739
    50
  let
noschinl@59739
    51
    val fg = @{cprop "f :: 'a :: {} \<Rightarrow> 'b :: {} \<equiv> g"}
noschinl@59739
    52
    val st = @{cprop "s :: 'a :: {} \<equiv> t"}
noschinl@59739
    53
    val thm = Thm.combination (Thm.assume fg) (Thm.assume st)
noschinl@59739
    54
      |> Thm.implies_intr st
noschinl@59739
    55
      |> Thm.implies_intr fg
noschinl@59739
    56
  in Drule.export_without_context thm end
noschinl@59739
    57
noschinl@59739
    58
fun abstract_rule_thm n =
noschinl@59739
    59
  let
noschinl@59739
    60
    val eq = @{cprop "\<And>x :: 'a :: {}. (s :: 'a \<Rightarrow> 'b :: {}) x \<equiv> t x"}
noschinl@59739
    61
    val x = @{cterm "x :: 'a :: {}"}
noschinl@59739
    62
    val thm = eq
noschinl@59739
    63
      |> Thm.assume
noschinl@59739
    64
      |> Thm.forall_elim x
noschinl@59739
    65
      |> Thm.abstract_rule n x
noschinl@59739
    66
      |> Thm.implies_intr eq
noschinl@59739
    67
  in Drule.export_without_context thm end
noschinl@59739
    68
noschinl@59739
    69
val no_cconv = Conv.no_conv
noschinl@59739
    70
val all_cconv = Conv.all_conv
noschinl@59739
    71
noschinl@59739
    72
fun (cv1 else_cconv cv2) ct =
noschinl@59739
    73
  (cv1 ct
noschinl@59739
    74
    handle THM _ => cv2 ct
noschinl@59739
    75
      | CTERM _ => cv2 ct
noschinl@59739
    76
      | TERM _ => cv2 ct
noschinl@59739
    77
      | TYPE _ => cv2 ct)
noschinl@59739
    78
noschinl@59739
    79
fun (cv1 then_cconv cv2) ct =
noschinl@59739
    80
  let
noschinl@59739
    81
    val eq1 = cv1 ct
noschinl@59739
    82
    val eq2 = cv2 (concl_rhs_of eq1)
noschinl@59739
    83
  in
noschinl@59739
    84
    if Thm.is_reflexive eq1 then eq2
noschinl@59739
    85
    else if Thm.is_reflexive eq2 then eq1
noschinl@59739
    86
    else transitive eq1 eq2
noschinl@59739
    87
  end
noschinl@59739
    88
noschinl@59739
    89
fun first_cconv cvs = fold_rev (curry op else_cconv) cvs no_cconv
noschinl@59739
    90
noschinl@59739
    91
fun rewr_cconv rule ct =
noschinl@59739
    92
  let
noschinl@59739
    93
    val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule
noschinl@59739
    94
    val lhs = concl_lhs_of rule1
noschinl@59739
    95
    val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1
noschinl@59739
    96
    val rule3 = Thm.instantiate (Thm.match (lhs, ct)) rule2
noschinl@59739
    97
                handle Pattern.MATCH => raise CTERM ("rewr_cconv", [lhs, ct])
noschinl@60048
    98
    val concl = rule3 |> Thm.cprop_of |> Drule.strip_imp_concl
noschinl@59739
    99
    val rule4 =
noschinl@60048
   100
      if Thm.dest_equals_lhs concl aconvc ct then rule3
noschinl@60048
   101
      else let val ceq = Thm.dest_fun2 concl
noschinl@60048
   102
           in rule3 RS Thm.trivial (Thm.mk_binop ceq ct (Thm.dest_equals_rhs concl)) end
noschinl@59739
   103
  in
noschinl@59739
   104
    transitive rule4 (Thm.beta_conversion true (concl_rhs_of rule4))
noschinl@59739
   105
  end
noschinl@59739
   106
noschinl@59739
   107
fun rewrs_cconv rules = first_cconv (map rewr_cconv rules)
noschinl@59739
   108
noschinl@59739
   109
fun combination_cconv cv1 cv2 cterm =
noschinl@59739
   110
  let val (l, r) = Thm.dest_comb cterm
noschinl@59739
   111
  in combination_thm OF [cv1 l, cv2 r] end
noschinl@59739
   112
noschinl@59739
   113
fun comb_cconv cv = combination_cconv cv cv
noschinl@59739
   114
noschinl@59739
   115
fun fun_cconv conversion =
noschinl@59739
   116
  combination_cconv conversion all_cconv
noschinl@59739
   117
noschinl@59739
   118
fun arg_cconv conversion =
noschinl@59739
   119
  combination_cconv all_cconv conversion
noschinl@59739
   120
noschinl@59739
   121
fun abs_cconv cv ctxt ct =
noschinl@59739
   122
  (case Thm.term_of ct of
noschinl@59739
   123
     Abs (x, _, _) =>
noschinl@59739
   124
       let
noschinl@59739
   125
         (* Instantiate the rule properly and apply it to the eq theorem. *)
noschinl@59739
   126
         fun abstract_rule u v eq =
noschinl@59739
   127
           let
noschinl@59739
   128
             (* Take a variable v and an equality theorem of form:
noschinl@60049
   129
                  P1 \<Longrightarrow> ... \<Longrightarrow> Pn \<Longrightarrow> L v \<equiv> R v
noschinl@59739
   130
                And build a term of form:
noschinl@60049
   131
                  \<And>v. (\<lambda>x. L x) v \<equiv> (\<lambda>x. R x) v *)
noschinl@59739
   132
             fun mk_concl var eq =
noschinl@59739
   133
               let
noschinl@59739
   134
                 val certify = Thm.cterm_of ctxt
noschinl@59739
   135
                 fun abs term = (Term.lambda var term) $ var
noschinl@59739
   136
                 fun equals_cong f t =
noschinl@59739
   137
                   Logic.dest_equals t
noschinl@59739
   138
                   |> (fn (a, b) => (f a, f b))
noschinl@59739
   139
                   |> Logic.mk_equals
noschinl@59739
   140
               in
noschinl@59739
   141
                 Thm.concl_of eq
noschinl@59739
   142
                 |> equals_cong abs
noschinl@59739
   143
                 |> Logic.all var |> certify
noschinl@59739
   144
               end
noschinl@59739
   145
             val rule = abstract_rule_thm x
noschinl@59739
   146
             val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
noschinl@59739
   147
           in
noschinl@59739
   148
             (Drule.instantiate_normalize inst rule OF [Drule.generalize ([], [u]) eq])
noschinl@59739
   149
             |> Drule.zero_var_indexes
noschinl@59739
   150
           end
noschinl@59739
   151
noschinl@59739
   152
         (* Destruct the abstraction and apply the conversion. *)
noschinl@59739
   153
         val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
noschinl@59739
   154
         val (v, ct') = Thm.dest_abs (SOME u) ct
noschinl@59739
   155
         val eq = cv (v, ctxt') ct'
noschinl@59739
   156
       in
noschinl@59739
   157
         if Thm.is_reflexive eq
noschinl@59739
   158
         then all_cconv ct
noschinl@59739
   159
         else abstract_rule u v eq
noschinl@59739
   160
       end
noschinl@59739
   161
   | _ => raise CTERM ("abs_cconv", [ct]))
noschinl@59739
   162
noschinl@59739
   163
val arg1_cconv = fun_cconv o arg_cconv
noschinl@59739
   164
val fun2_cconv = fun_cconv o fun_cconv
noschinl@59739
   165
noschinl@59739
   166
(* conversions on HHF rules *)
noschinl@59739
   167
noschinl@60049
   168
(*rewrite B in \<And>x1 ... xn. B*)
noschinl@59739
   169
fun params_cconv n cv ctxt ct =
noschinl@59739
   170
  if n <> 0 andalso Logic.is_all (Thm.term_of ct)
noschinl@59739
   171
  then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
noschinl@59739
   172
  else cv ctxt ct
noschinl@59739
   173
noschinl@59739
   174
(* TODO: This code behaves not exactly like Conv.prems_cconv does.
noschinl@59739
   175
         Fix this! *)
noschinl@60049
   176
(*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
noschinl@59739
   177
fun prems_cconv 0 cv ct = cv ct
noschinl@59739
   178
  | prems_cconv n cv ct =
noschinl@59739
   179
      (case ct |> Thm.term_of of
wenzelm@59975
   180
        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ =>
wenzelm@59975
   181
          ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
noschinl@59739
   182
      | _ =>  cv ct)
noschinl@59739
   183
noschinl@60050
   184
fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong
noschinl@60050
   185
noschinl@60049
   186
(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
noschinl@59739
   187
fun concl_cconv 0 cv ct = cv ct
noschinl@59739
   188
  | concl_cconv n cv ct =
noschinl@60050
   189
      (case try Thm.dest_implies ct of
noschinl@60050
   190
        NONE => cv ct
noschinl@60050
   191
      | SOME (A,B) => (concl_cconv (n-1) cv B) RS inst_imp_cong A)
noschinl@59739
   192
noschinl@59739
   193
(*forward conversion, cf. FCONV_RULE in LCF*)
noschinl@59739
   194
fun fconv_rule cv th =
noschinl@59739
   195
  let
noschinl@59739
   196
    val eq = cv (Thm.cprop_of th)
noschinl@59739
   197
  in
noschinl@59739
   198
    if Thm.is_reflexive eq then th
noschinl@59739
   199
    else th COMP (Thm.permute_prems 0 (Thm.nprems_of eq) (eq RS Drule.equal_elim_rule1))
noschinl@59739
   200
  end
noschinl@59739
   201
noschinl@59739
   202
(*goal conversion*)
noschinl@59739
   203
fun gconv_rule cv i th =
noschinl@59739
   204
  (case try (Thm.cprem_of th) i of
noschinl@59739
   205
    SOME ct =>
noschinl@59739
   206
      let
noschinl@59739
   207
        val eq = cv ct
noschinl@59739
   208
noschinl@59739
   209
        (* Drule.with_subgoal assumes that there are no new premises generated
noschinl@59739
   210
           and thus rotates the premises wrongly. *)
noschinl@59739
   211
        fun with_subgoal i f thm =
noschinl@59739
   212
          let
noschinl@59739
   213
            val num_prems = Thm.nprems_of thm
noschinl@59739
   214
            val rotate_to_front = rotate_prems (i - 1)
noschinl@59739
   215
            fun rotate_back thm = rotate_prems (1 - i + num_prems - Thm.nprems_of thm) thm
noschinl@59739
   216
          in
noschinl@59739
   217
            thm |> rotate_to_front |> f |> rotate_back
noschinl@59739
   218
          end
noschinl@59739
   219
      in
noschinl@59739
   220
        if Thm.is_reflexive eq then th
noschinl@59739
   221
        else with_subgoal i (fconv_rule (arg1_cconv (K eq))) th
noschinl@59739
   222
      end
noschinl@59739
   223
  | NONE => raise THM ("gconv_rule", i, [th]))
noschinl@59739
   224
wenzelm@59975
   225
(* Conditional conversions as tactics. *)
noschinl@59739
   226
fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
noschinl@59739
   227
  handle THM _ => Seq.empty
noschinl@59739
   228
       | CTERM _ => Seq.empty
noschinl@59739
   229
       | TERM _ => Seq.empty
noschinl@59739
   230
       | TYPE _ => Seq.empty
noschinl@59739
   231
noschinl@59739
   232
end
noschinl@59739
   233
noschinl@59739
   234
structure Basic_CConv: BASIC_CCONV = CConv
noschinl@59739
   235
open Basic_CConv