src/Pure/conv.ML
author wenzelm
Thu May 10 00:39:51 2007 +0200 (2007-05-10)
changeset 22905 dab6a898b47c
child 22926 fb6917e426da
permissions -rw-r--r--
Conversions: primitive equality reasoning (from drule.ML);
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@22905
     8
infix 1 AND;
wenzelm@22905
     9
infix 0 OR;
wenzelm@22905
    10
wenzelm@22905
    11
signature CONV =
wenzelm@22905
    12
sig
wenzelm@22905
    13
  type conv = cterm -> thm
wenzelm@22905
    14
  val no_conv: conv
wenzelm@22905
    15
  val all_conv: conv
wenzelm@22905
    16
  val option_conv: conv -> cterm -> thm option
wenzelm@22905
    17
  val AND: conv * conv -> conv
wenzelm@22905
    18
  val OR: conv * conv -> conv
wenzelm@22905
    19
  val forall_conv: int -> conv -> conv
wenzelm@22905
    20
  val concl_conv: int -> conv -> conv
wenzelm@22905
    21
  val prems_conv: int -> (int -> conv) -> conv
wenzelm@22905
    22
  val goals_conv: (int -> bool) -> conv -> conv
wenzelm@22905
    23
  val fconv_rule: conv -> thm -> thm
wenzelm@22905
    24
end;
wenzelm@22905
    25
wenzelm@22905
    26
structure Conv: CONV =
wenzelm@22905
    27
struct
wenzelm@22905
    28
wenzelm@22905
    29
(* conversionals *)
wenzelm@22905
    30
wenzelm@22905
    31
type conv = cterm -> thm
wenzelm@22905
    32
wenzelm@22905
    33
fun no_conv _ = raise CTERM ("no conversion", []);
wenzelm@22905
    34
val all_conv = Thm.reflexive;
wenzelm@22905
    35
wenzelm@22905
    36
val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
wenzelm@22905
    37
wenzelm@22905
    38
fun option_conv conv ct =
wenzelm@22905
    39
  (case try conv ct of
wenzelm@22905
    40
    NONE => NONE
wenzelm@22905
    41
  | SOME eq => if is_refl eq then NONE else SOME eq);
wenzelm@22905
    42
wenzelm@22905
    43
fun (conv1 AND conv2) ct =
wenzelm@22905
    44
  let
wenzelm@22905
    45
    val eq1 = conv1 ct;
wenzelm@22905
    46
    val eq2 = conv2 (Thm.rhs_of eq1);
wenzelm@22905
    47
  in
wenzelm@22905
    48
    if is_refl eq1 then eq2
wenzelm@22905
    49
    else if is_refl eq2 then eq1
wenzelm@22905
    50
    else Thm.transitive eq1 eq2
wenzelm@22905
    51
  end;
wenzelm@22905
    52
wenzelm@22905
    53
fun (conv1 OR conv2) ct =
wenzelm@22905
    54
  (case try conv1 ct of SOME eq => eq | NONE => conv2 ct);
wenzelm@22905
    55
wenzelm@22905
    56
wenzelm@22905
    57
(* Pure conversions *)
wenzelm@22905
    58
wenzelm@22905
    59
(*rewrite B in !!x1 ... xn. B*)
wenzelm@22905
    60
fun forall_conv 0 cv ct = cv ct
wenzelm@22905
    61
  | forall_conv n cv ct =
wenzelm@22905
    62
      (case try Thm.dest_comb ct of
wenzelm@22905
    63
        NONE => cv ct
wenzelm@22905
    64
      | SOME (A, B) =>
wenzelm@22905
    65
          (case (term_of A, term_of B) of
wenzelm@22905
    66
            (Const ("all", _), Abs (x, _, _)) =>
wenzelm@22905
    67
              let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
wenzelm@22905
    68
                Thm.combination (Thm.reflexive A)
wenzelm@22905
    69
                  (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
wenzelm@22905
    70
              end
wenzelm@22905
    71
          | _ => cv ct));
wenzelm@22905
    72
wenzelm@22905
    73
(*rewrite B in A1 ==> ... ==> An ==> B*)
wenzelm@22905
    74
fun concl_conv 0 cv ct = cv ct
wenzelm@22905
    75
  | concl_conv n cv ct =
wenzelm@22905
    76
      (case try Thm.dest_implies ct of
wenzelm@22905
    77
        NONE => cv ct
wenzelm@22905
    78
      | SOME (A, B) => Drule.imp_cong_rule (reflexive A) (concl_conv (n - 1) cv B));
wenzelm@22905
    79
wenzelm@22905
    80
(*rewrite the A's in A1 ==> ... ==> An ==> B*)
wenzelm@22905
    81
fun prems_conv 0 _ = reflexive
wenzelm@22905
    82
  | prems_conv n cv =
wenzelm@22905
    83
      let
wenzelm@22905
    84
        fun conv i ct =
wenzelm@22905
    85
          if i = n + 1 then reflexive ct
wenzelm@22905
    86
          else
wenzelm@22905
    87
            (case try Thm.dest_implies ct of
wenzelm@22905
    88
              NONE => reflexive ct
wenzelm@22905
    89
            | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
wenzelm@22905
    90
  in conv 1 end;
wenzelm@22905
    91
wenzelm@22905
    92
fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
wenzelm@22905
    93
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
wenzelm@22905
    94
wenzelm@22905
    95
end;