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