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