src/Pure/conv.ML
author wenzelm
Wed Jan 21 22:26:49 2009 +0100 (2009-01-21)
changeset 29605 f2924219125e
parent 27332 94790a9620c3
child 29606 fedb8be05f24
permissions -rw-r--r--
eliminated obsolete var morphism;
     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: (cterm * 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: (cterm * Proof.context -> conv) -> Proof.context -> conv
    30   val implies_conv: conv -> conv -> conv
    31   val implies_concl_conv: conv -> conv
    32   val rewr_conv: thm -> conv
    33   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    34   val prems_conv: int -> conv -> conv
    35   val concl_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 fun no_conv _ = raise CTERM ("no conversion", []);
    46 val all_conv = Thm.reflexive;
    47 
    48 fun (cv1 then_conv cv2) ct =
    49   let
    50     val eq1 = cv1 ct;
    51     val eq2 = cv2 (Thm.rhs_of eq1);
    52   in
    53     if Thm.is_reflexive eq1 then eq2
    54     else if Thm.is_reflexive eq2 then eq1
    55     else Thm.transitive eq1 eq2
    56   end;
    57 
    58 fun (cv1 else_conv cv2) ct =
    59   (cv1 ct
    60     handle THM _ => cv2 ct
    61       | CTERM _ => cv2 ct
    62       | TERM _ => cv2 ct
    63       | TYPE _ => 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 
    72 
    73 (** Pure conversions **)
    74 
    75 (* lambda terms *)
    76 
    77 fun abs_conv cv ctxt ct =
    78   (case Thm.term_of ct of
    79     Abs (x, _, _) =>
    80       let
    81         val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
    82         val (v, ct') = Thm.dest_abs (SOME u) ct;
    83         val eq = cv (v, ctxt') ct';
    84       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
    85   | _ => raise CTERM ("abs_conv", [ct]));
    86 
    87 fun combination_conv cv1 cv2 ct =
    88   let val (ct1, ct2) = Thm.dest_comb ct
    89   in Thm.combination (cv1 ct1) (cv2 ct2) end;
    90 
    91 fun comb_conv cv = combination_conv cv cv;
    92 fun arg_conv cv = combination_conv all_conv cv;
    93 fun fun_conv cv = combination_conv cv all_conv;
    94 
    95 val arg1_conv = fun_conv o arg_conv;
    96 val fun2_conv = fun_conv o fun_conv;
    97 
    98 fun binop_conv cv = combination_conv (arg_conv cv) cv;
    99 
   100 
   101 (* primitive logic *)
   102 
   103 fun forall_conv cv ctxt ct =
   104   (case Thm.term_of ct of
   105     Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
   106   | _ => raise CTERM ("forall_conv", [ct]));
   107 
   108 fun implies_conv cv1 cv2 ct =
   109   (case Thm.term_of ct of
   110     Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
   111   | _ => raise CTERM ("implies_conv", [ct]));
   112 
   113 fun implies_concl_conv cv ct =
   114   (case Thm.term_of ct of
   115     Const ("==>", _) $ _ $ _ => arg_conv cv ct
   116   | _ => raise CTERM ("implies_concl_conv", [ct]));
   117 
   118 
   119 (* single rewrite step, cf. REWR_CONV in HOL *)
   120 
   121 fun rewr_conv rule ct =
   122   let
   123     val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
   124     val lhs = Thm.lhs_of rule1;
   125     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   126   in
   127     Drule.instantiate (Thm.match (lhs, ct)) rule2
   128       handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   129   end;
   130 
   131 
   132 (* conversions on HHF rules *)
   133 
   134 (*rewrite B in !!x1 ... xn. B*)
   135 fun params_conv n cv ctxt ct =
   136   if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   137   then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
   138   else cv ctxt ct;
   139 
   140 (*rewrite the A's in A1 ==> ... ==> An ==> B*)
   141 fun prems_conv 0 _ ct = all_conv ct
   142   | prems_conv n cv ct =
   143       (case try Thm.dest_implies ct of
   144         NONE => all_conv ct
   145       | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
   146 
   147 (*rewrite B in A1 ==> ... ==> An ==> B*)
   148 fun concl_conv 0 cv ct = cv ct
   149   | concl_conv n cv ct =
   150       (case try Thm.dest_implies ct of
   151         NONE => cv ct
   152       | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
   153 
   154 
   155 (* conversions as inference rules *)
   156 
   157 (*forward conversion, cf. FCONV_RULE in LCF*)
   158 fun fconv_rule cv th =
   159   let val eq = cv (Thm.cprop_of th) in
   160     if Thm.is_reflexive eq then th
   161     else Thm.equal_elim eq th
   162   end;
   163 
   164 (*goal conversion*)
   165 fun gconv_rule cv i th =
   166   (case try (Thm.cprem_of th) i of
   167     SOME ct =>
   168       let val eq = cv ct in
   169         if Thm.is_reflexive eq then th
   170         else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
   171       end
   172   | NONE => raise THM ("gconv_rule", i, [th]));
   173 
   174 end;