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