src/Pure/conv.ML
author wenzelm
Thu Jul 05 00:06:22 2007 +0200 (2007-07-05)
changeset 23583 00751df1f98c
parent 23534 3f82d1798976
child 23587 46d01f5e1e5b
permissions -rw-r--r--
else_conv: only handle THM | CTERM | TERM | TYPE;
prems_conv: no index;
renamed goal_conv_rule to gconv_rule;
wenzelm@22905
     1
(*  Title:      Pure/conv.ML
wenzelm@22905
     2
    ID:         $Id$
wenzelm@22905
     3
    Author:     Amine Chaieb and Makarius
wenzelm@22905
     4
wenzelm@22905
     5
Conversions: primitive equality reasoning.
wenzelm@22905
     6
*)
wenzelm@22905
     7
wenzelm@22937
     8
infix 1 then_conv;
wenzelm@22937
     9
infix 0 else_conv;
wenzelm@23169
    10
wenzelm@23490
    11
type conv = cterm -> thm;
wenzelm@23490
    12
wenzelm@22905
    13
signature CONV =
wenzelm@22905
    14
sig
wenzelm@22905
    15
  val no_conv: conv
wenzelm@22905
    16
  val all_conv: conv
wenzelm@23490
    17
  val is_refl: thm -> bool
wenzelm@22937
    18
  val then_conv: conv * conv -> conv
wenzelm@22937
    19
  val else_conv: conv * conv -> conv
wenzelm@22926
    20
  val first_conv: conv list -> conv
wenzelm@22926
    21
  val every_conv: conv list -> conv
wenzelm@22937
    22
  val try_conv: conv -> conv
wenzelm@22937
    23
  val repeat_conv: conv -> conv
wenzelm@22926
    24
  val cache_conv: conv -> conv
wenzelm@22926
    25
  val abs_conv: conv -> conv
wenzelm@22926
    26
  val combination_conv: conv -> conv -> conv
wenzelm@22926
    27
  val comb_conv: conv -> conv
wenzelm@22926
    28
  val arg_conv: conv -> conv
wenzelm@22926
    29
  val fun_conv: conv -> conv
wenzelm@22926
    30
  val arg1_conv: conv -> conv
wenzelm@22926
    31
  val fun2_conv: conv -> conv
chaieb@23034
    32
  val binop_conv: conv -> conv
wenzelm@22905
    33
  val forall_conv: int -> conv -> conv
wenzelm@22905
    34
  val concl_conv: int -> conv -> conv
wenzelm@23583
    35
  val prems_conv: int -> conv -> conv
wenzelm@22905
    36
  val fconv_rule: conv -> thm -> thm
wenzelm@23583
    37
  val gconv_rule: conv -> int -> thm -> thm
wenzelm@22905
    38
end;
wenzelm@22905
    39
wenzelm@22905
    40
structure Conv: CONV =
wenzelm@22905
    41
struct
wenzelm@22905
    42
wenzelm@22905
    43
(* conversionals *)
wenzelm@22905
    44
wenzelm@22926
    45
type conv = cterm -> thm;
wenzelm@22905
    46
wenzelm@22905
    47
fun no_conv _ = raise CTERM ("no conversion", []);
wenzelm@22905
    48
val all_conv = Thm.reflexive;
wenzelm@22905
    49
wenzelm@22905
    50
val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
wenzelm@22905
    51
wenzelm@22937
    52
fun (cv1 then_conv cv2) ct =
wenzelm@22905
    53
  let
wenzelm@22926
    54
    val eq1 = cv1 ct;
wenzelm@22926
    55
    val eq2 = cv2 (Thm.rhs_of eq1);
wenzelm@22905
    56
  in
wenzelm@22905
    57
    if is_refl eq1 then eq2
wenzelm@22905
    58
    else if is_refl eq2 then eq1
wenzelm@22905
    59
    else Thm.transitive eq1 eq2
wenzelm@22905
    60
  end;
wenzelm@22905
    61
wenzelm@22937
    62
fun (cv1 else_conv cv2) ct =
wenzelm@23583
    63
  (cv1 ct
wenzelm@23583
    64
    handle THM _ => cv2 ct
wenzelm@23583
    65
      | CTERM _ => cv2 ct
wenzelm@23583
    66
      | TERM _ => cv2 ct
wenzelm@23583
    67
      | TYPE _ => cv2 ct);
wenzelm@22926
    68
wenzelm@22937
    69
fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
wenzelm@22937
    70
fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
wenzelm@22926
    71
wenzelm@22937
    72
fun try_conv cv = cv else_conv all_conv;
wenzelm@22937
    73
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
wenzelm@22926
    74
wenzelm@22926
    75
fun cache_conv cv =
wenzelm@22926
    76
  let
wenzelm@22926
    77
    val cache = ref Termtab.empty;
wenzelm@22926
    78
    fun conv ct =
wenzelm@22926
    79
      (case Termtab.lookup (! cache) (term_of ct) of
wenzelm@22926
    80
        SOME th => th
wenzelm@22926
    81
      | NONE =>
wenzelm@22926
    82
          let val th = cv ct
wenzelm@22926
    83
          in change cache (Termtab.update (term_of ct, th)); th end);
wenzelm@22926
    84
 in conv end;
wenzelm@22926
    85
wenzelm@22905
    86
wenzelm@22905
    87
wenzelm@22926
    88
(** Pure conversions **)
wenzelm@22926
    89
wenzelm@22926
    90
(* lambda terms *)
wenzelm@22926
    91
wenzelm@22926
    92
fun abs_conv cv ct =
wenzelm@22926
    93
  (case term_of ct of
wenzelm@22926
    94
    Abs (x, _, _) =>
wenzelm@22926
    95
      let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct
wenzelm@22926
    96
      in Thm.abstract_rule x v (cv ct') end
wenzelm@22926
    97
  | _ => raise CTERM ("abs_conv", [ct]));
wenzelm@22926
    98
wenzelm@22926
    99
fun combination_conv cv1 cv2 ct =
wenzelm@22926
   100
  let val (ct1, ct2) = Thm.dest_comb ct
wenzelm@22926
   101
  in Thm.combination (cv1 ct1) (cv2 ct2) end;
wenzelm@22926
   102
wenzelm@22926
   103
fun comb_conv cv = combination_conv cv cv;
wenzelm@22926
   104
fun arg_conv cv = combination_conv all_conv cv;
wenzelm@22926
   105
fun fun_conv cv = combination_conv cv all_conv;
wenzelm@22926
   106
wenzelm@22926
   107
val arg1_conv = fun_conv o arg_conv;
wenzelm@22926
   108
val fun2_conv = fun_conv o fun_conv;
wenzelm@22926
   109
chaieb@23034
   110
fun binop_conv cv = combination_conv (arg_conv cv) cv;
wenzelm@22926
   111
wenzelm@23169
   112
wenzelm@22926
   113
(* logic *)
wenzelm@22905
   114
wenzelm@22905
   115
(*rewrite B in !!x1 ... xn. B*)
wenzelm@22905
   116
fun forall_conv 0 cv ct = cv ct
wenzelm@22905
   117
  | forall_conv n cv ct =
wenzelm@22905
   118
      (case try Thm.dest_comb ct of
wenzelm@22905
   119
        NONE => cv ct
wenzelm@22905
   120
      | SOME (A, B) =>
wenzelm@22905
   121
          (case (term_of A, term_of B) of
wenzelm@22905
   122
            (Const ("all", _), Abs (x, _, _)) =>
wenzelm@22905
   123
              let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
wenzelm@22926
   124
                Thm.combination (all_conv A)
wenzelm@22905
   125
                  (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
wenzelm@22905
   126
              end
wenzelm@22905
   127
          | _ => cv ct));
wenzelm@22905
   128
wenzelm@22905
   129
(*rewrite B in A1 ==> ... ==> An ==> B*)
wenzelm@22905
   130
fun concl_conv 0 cv ct = cv ct
wenzelm@22905
   131
  | concl_conv n cv ct =
wenzelm@22905
   132
      (case try Thm.dest_implies ct of
wenzelm@22905
   133
        NONE => cv ct
wenzelm@22926
   134
      | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
wenzelm@22905
   135
wenzelm@22905
   136
(*rewrite the A's in A1 ==> ... ==> An ==> B*)
wenzelm@22926
   137
fun prems_conv 0 _ = all_conv
wenzelm@22905
   138
  | prems_conv n cv =
wenzelm@22905
   139
      let
wenzelm@22905
   140
        fun conv i ct =
wenzelm@22926
   141
          if i = n + 1 then all_conv ct
wenzelm@22905
   142
          else
wenzelm@22905
   143
            (case try Thm.dest_implies ct of
wenzelm@22926
   144
              NONE => all_conv ct
wenzelm@23583
   145
            | SOME (A, B) => Drule.imp_cong_rule (cv A) (conv (i + 1) B));
wenzelm@22905
   146
  in conv 1 end;
wenzelm@22905
   147
wenzelm@23534
   148
fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th;  (*FCONV_RULE in LCF*)
wenzelm@22905
   149
wenzelm@23583
   150
fun gconv_rule cv i = Drule.with_subgoal i (fn th =>
wenzelm@23534
   151
  (case try (Thm.dest_implies o Thm.cprop_of) th of
wenzelm@23583
   152
    SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th
wenzelm@23583
   153
  | NONE => raise THM ("gconv_rule", i, [th])));
chaieb@23411
   154
wenzelm@22905
   155
end;