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