src/Pure/conv.ML
author wenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843 c8f5a7c8353f
parent 30136 6a874aedb964
child 36936 c52d1c130898
permissions -rw-r--r--
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
     1 (*  Title:      Pure/conv.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3     Author:     Makarius
     4 
     5 Conversions: primitive equality reasoning.
     6 *)
     7 
     8 infix 1 then_conv;
     9 infix 0 else_conv;
    10 
    11 signature BASIC_CONV =
    12 sig
    13   val then_conv: conv * conv -> conv
    14   val else_conv: conv * conv -> conv
    15 end;
    16 
    17 signature CONV =
    18 sig
    19   include BASIC_CONV
    20   val no_conv: conv
    21   val all_conv: conv
    22   val first_conv: conv list -> conv
    23   val every_conv: conv list -> conv
    24   val try_conv: conv -> conv
    25   val repeat_conv: conv -> conv
    26   val cache_conv: conv -> conv
    27   val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    28   val combination_conv: conv -> conv -> conv
    29   val comb_conv: conv -> conv
    30   val arg_conv: conv -> conv
    31   val fun_conv: conv -> conv
    32   val arg1_conv: conv -> conv
    33   val fun2_conv: conv -> conv
    34   val binop_conv: conv -> conv
    35   val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    36   val implies_conv: conv -> conv -> conv
    37   val implies_concl_conv: conv -> conv
    38   val rewr_conv: thm -> conv
    39   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    40   val prems_conv: int -> conv -> conv
    41   val concl_conv: int -> conv -> conv
    42   val fconv_rule: conv -> thm -> thm
    43   val gconv_rule: conv -> int -> thm -> thm
    44 end;
    45 
    46 structure Conv: CONV =
    47 struct
    48 
    49 (* basic conversionals *)
    50 
    51 fun no_conv _ = raise CTERM ("no conversion", []);
    52 val all_conv = Thm.reflexive;
    53 
    54 fun (cv1 then_conv cv2) ct =
    55   let
    56     val eq1 = cv1 ct;
    57     val eq2 = cv2 (Thm.rhs_of eq1);
    58   in
    59     if Thm.is_reflexive eq1 then eq2
    60     else if Thm.is_reflexive eq2 then eq1
    61     else Thm.transitive eq1 eq2
    62   end;
    63 
    64 fun (cv1 else_conv cv2) ct =
    65   (cv1 ct
    66     handle THM _ => cv2 ct
    67       | CTERM _ => cv2 ct
    68       | TERM _ => cv2 ct
    69       | TYPE _ => cv2 ct);
    70 
    71 fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
    72 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
    73 
    74 fun try_conv cv = cv else_conv all_conv;
    75 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    76 
    77 fun cache_conv (cv: conv) = Thm.cterm_cache cv;
    78 
    79 
    80 
    81 (** Pure conversions **)
    82 
    83 (* lambda terms *)
    84 
    85 fun abs_conv cv ctxt ct =
    86   (case Thm.term_of ct of
    87     Abs (x, _, _) =>
    88       let
    89         val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
    90         val (v, ct') = Thm.dest_abs (SOME u) ct;
    91         val eq = cv (v, ctxt') ct';
    92       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq 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 (* primitive logic *)
   110 
   111 fun forall_conv cv ctxt ct =
   112   (case Thm.term_of ct of
   113     Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
   114   | _ => raise CTERM ("forall_conv", [ct]));
   115 
   116 fun implies_conv cv1 cv2 ct =
   117   (case Thm.term_of ct of
   118     Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
   119   | _ => raise CTERM ("implies_conv", [ct]));
   120 
   121 fun implies_concl_conv cv ct =
   122   (case Thm.term_of ct of
   123     Const ("==>", _) $ _ $ _ => arg_conv cv ct
   124   | _ => raise CTERM ("implies_concl_conv", [ct]));
   125 
   126 
   127 (* single rewrite step, cf. REWR_CONV in HOL *)
   128 
   129 fun rewr_conv rule ct =
   130   let
   131     val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
   132     val lhs = Thm.lhs_of rule1;
   133     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   134   in
   135     Drule.instantiate (Thm.match (lhs, ct)) rule2
   136       handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   137   end;
   138 
   139 
   140 (* conversions on HHF rules *)
   141 
   142 (*rewrite B in !!x1 ... xn. B*)
   143 fun params_conv n cv ctxt ct =
   144   if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   145   then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
   146   else cv ctxt ct;
   147 
   148 (*rewrite the A's in A1 ==> ... ==> An ==> B*)
   149 fun prems_conv 0 _ ct = all_conv ct
   150   | prems_conv n cv ct =
   151       (case try Thm.dest_implies ct of
   152         NONE => all_conv ct
   153       | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
   154 
   155 (*rewrite B in A1 ==> ... ==> An ==> B*)
   156 fun concl_conv 0 cv ct = cv ct
   157   | concl_conv n cv ct =
   158       (case try Thm.dest_implies ct of
   159         NONE => cv ct
   160       | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
   161 
   162 
   163 (* conversions as inference rules *)
   164 
   165 (*forward conversion, cf. FCONV_RULE in LCF*)
   166 fun fconv_rule cv th =
   167   let val eq = cv (Thm.cprop_of th) in
   168     if Thm.is_reflexive eq then th
   169     else Thm.equal_elim eq th
   170   end;
   171 
   172 (*goal conversion*)
   173 fun gconv_rule cv i th =
   174   (case try (Thm.cprem_of th) i of
   175     SOME ct =>
   176       let val eq = cv ct in
   177         if Thm.is_reflexive eq then th
   178         else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
   179       end
   180   | NONE => raise THM ("gconv_rule", i, [th]));
   181 
   182 end;
   183 
   184 structure Basic_Conv: BASIC_CONV = Conv;
   185 open Basic_Conv;