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