src/Pure/conv.ML
author chaieb
Sun Jun 17 13:39:48 2007 +0200 (2007-06-17)
changeset 23411 c524900454f3
parent 23169 37091da05d8e
child 23490 1dfbfc92017a
permissions -rw-r--r--
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
     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 signature CONV =
    12 sig
    13   type conv = cterm -> thm
    14   val no_conv: conv
    15   val all_conv: conv
    16   val then_conv: conv * conv -> conv
    17   val else_conv: conv * conv -> conv
    18   val first_conv: conv list -> conv
    19   val every_conv: conv list -> conv
    20   val try_conv: conv -> conv
    21   val repeat_conv: conv -> conv
    22   val cache_conv: conv -> conv
    23   val abs_conv: conv -> conv
    24   val combination_conv: conv -> conv -> conv
    25   val comb_conv: conv -> conv
    26   val arg_conv: conv -> conv
    27   val fun_conv: conv -> conv
    28   val arg1_conv: conv -> conv
    29   val fun2_conv: conv -> conv
    30   val binop_conv: conv -> conv
    31   val forall_conv: int -> conv -> conv
    32   val concl_conv: int -> conv -> conv
    33   val prems_conv: int -> (int -> conv) -> conv
    34   val goals_conv: (int -> bool) -> conv -> conv
    35   val eta_conv: theory -> conv 
    36   val fconv_rule: conv -> thm -> thm
    37   val is_refl: thm -> bool
    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   (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
    64 
    65 fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
    66 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
    67 
    68 fun try_conv cv = cv else_conv all_conv;
    69 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    70 
    71 fun cache_conv cv =
    72   let
    73     val cache = ref Termtab.empty;
    74     fun conv ct =
    75       (case Termtab.lookup (! cache) (term_of ct) of
    76         SOME th => th
    77       | NONE =>
    78           let val th = cv ct
    79           in change cache (Termtab.update (term_of ct, th)); th end);
    80  in conv end;
    81 
    82 
    83 
    84 (** Pure conversions **)
    85 
    86 (* lambda terms *)
    87 
    88 fun abs_conv cv ct =
    89   (case term_of ct of
    90     Abs (x, _, _) =>
    91       let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct
    92       in Thm.abstract_rule x v (cv ct') end
    93   | _ => raise CTERM ("abs_conv", [ct]));
    94 
    95 fun combination_conv cv1 cv2 ct =
    96   let val (ct1, ct2) = Thm.dest_comb ct
    97   in Thm.combination (cv1 ct1) (cv2 ct2) end;
    98 
    99 fun comb_conv cv = combination_conv cv cv;
   100 fun arg_conv cv = combination_conv all_conv cv;
   101 fun fun_conv cv = combination_conv cv all_conv;
   102 
   103 val arg1_conv = fun_conv o arg_conv;
   104 val fun2_conv = fun_conv o fun_conv;
   105 
   106 fun binop_conv cv = combination_conv (arg_conv cv) cv;
   107 
   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 
   146 fun eta_conv thy ct = 
   147   let val {t, ...} = rep_cterm ct
   148       val ct' = cterm_of thy (Pattern.eta_long [] t)
   149   in (symmetric o eta_conversion) ct'
   150   end;
   151 
   152 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   153 end;