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