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