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