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