src/Pure/conv.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 49974 791157a4179a
child 50639 f1c2f911ae33
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     1 (*  Title:      Pure/conv.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3     Author:     Sascha Boehme, TU Muenchen
     4     Author:     Makarius
     5 
     6 Conversions: primitive equality reasoning.
     7 *)
     8 
     9 infix 1 then_conv;
    10 infix 0 else_conv;
    11 
    12 signature BASIC_CONV =
    13 sig
    14   val then_conv: conv * conv -> conv
    15   val else_conv: conv * conv -> conv
    16 end;
    17 
    18 signature CONV =
    19 sig
    20   include BASIC_CONV
    21   val no_conv: conv
    22   val all_conv: conv
    23   val first_conv: conv list -> conv
    24   val every_conv: conv list -> conv
    25   val try_conv: conv -> conv
    26   val repeat_conv: conv -> conv
    27   val cache_conv: conv -> conv
    28   val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    29   val combination_conv: conv -> conv -> conv
    30   val comb_conv: conv -> conv
    31   val arg_conv: conv -> conv
    32   val fun_conv: conv -> conv
    33   val arg1_conv: conv -> conv
    34   val fun2_conv: conv -> conv
    35   val binop_conv: conv -> conv
    36   val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    37   val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    38   val implies_conv: conv -> conv -> conv
    39   val implies_concl_conv: conv -> conv
    40   val rewr_conv: thm -> conv
    41   val rewrs_conv: thm list -> conv
    42   val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
    43   val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
    44   val top_conv: (Proof.context -> conv) -> Proof.context -> conv
    45   val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
    46   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    47   val prems_conv: int -> conv -> conv
    48   val concl_conv: int -> conv -> conv
    49   val fconv_rule: conv -> thm -> thm
    50   val gconv_rule: conv -> int -> thm -> thm
    51 end;
    52 
    53 structure Conv: CONV =
    54 struct
    55 
    56 (* basic conversionals *)
    57 
    58 fun no_conv _ = raise CTERM ("no conversion", []);
    59 val all_conv = Thm.reflexive;
    60 
    61 fun (cv1 then_conv cv2) ct =
    62   let
    63     val eq1 = cv1 ct;
    64     val eq2 = cv2 (Thm.rhs_of eq1);
    65   in
    66     if Thm.is_reflexive eq1 then eq2
    67     else if Thm.is_reflexive eq2 then eq1
    68     else Thm.transitive eq1 eq2
    69   end;
    70 
    71 fun (cv1 else_conv cv2) ct =
    72   (cv1 ct
    73     handle THM _ => cv2 ct
    74       | CTERM _ => cv2 ct
    75       | TERM _ => cv2 ct
    76       | TYPE _ => cv2 ct);
    77 
    78 fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
    79 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
    80 
    81 fun try_conv cv = cv else_conv all_conv;
    82 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    83 
    84 fun cache_conv (cv: conv) = Thm.cterm_cache cv;
    85 
    86 
    87 
    88 (** Pure conversions **)
    89 
    90 (* lambda terms *)
    91 
    92 fun abs_conv cv ctxt ct =
    93   (case Thm.term_of ct of
    94     Abs (x, _, _) =>
    95       let
    96         val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
    97         val (v, ct') = Thm.dest_abs (SOME u) ct;
    98         val eq = cv (v, ctxt') ct';
    99       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
   100   | _ => raise CTERM ("abs_conv", [ct]));
   101 
   102 fun combination_conv cv1 cv2 ct =
   103   let val (ct1, ct2) = Thm.dest_comb ct
   104   in Thm.combination (cv1 ct1) (cv2 ct2) end;
   105 
   106 fun comb_conv cv = combination_conv cv cv;
   107 fun arg_conv cv = combination_conv all_conv cv;
   108 fun fun_conv cv = combination_conv cv all_conv;
   109 
   110 val arg1_conv = fun_conv o arg_conv;
   111 val fun2_conv = fun_conv o fun_conv;
   112 
   113 fun binop_conv cv = combination_conv (arg_conv cv) cv;
   114 
   115 fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt);
   116 
   117 
   118 (* subterm structure *)
   119 
   120 (*cf. SUB_CONV in HOL*)
   121 fun sub_conv conv ctxt =
   122   comb_conv (conv ctxt) else_conv
   123   abs_conv (conv o snd) ctxt else_conv
   124   all_conv;
   125 
   126 (*cf. BOTTOM_CONV in HOL*)
   127 fun bottom_conv conv ctxt ct =
   128   (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct;
   129 
   130 (*cf. TOP_CONV in HOL*)
   131 fun top_conv conv ctxt ct =
   132   (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct;
   133 
   134 (*cf. TOP_SWEEP_CONV in HOL*)
   135 fun top_sweep_conv conv ctxt ct =
   136   (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct;
   137 
   138 
   139 (* primitive logic *)
   140 
   141 fun forall_conv cv ctxt ct =
   142   (case Thm.term_of ct of
   143     Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
   144   | _ => raise CTERM ("forall_conv", [ct]));
   145 
   146 fun implies_conv cv1 cv2 ct =
   147   (case Thm.term_of ct of
   148     Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
   149   | _ => raise CTERM ("implies_conv", [ct]));
   150 
   151 fun implies_concl_conv cv ct =
   152   (case Thm.term_of ct of
   153     Const ("==>", _) $ _ $ _ => arg_conv cv ct
   154   | _ => raise CTERM ("implies_concl_conv", [ct]));
   155 
   156 
   157 (* single rewrite step
   158    beta-normalizes the rhs and takes care that lhs aconv ct *)
   159 fun rewr_conv rule ct =
   160   let
   161     val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
   162     val lhs = Thm.lhs_of rule1;
   163     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   164     val rule3 =
   165       Thm.instantiate (Thm.match (lhs, ct)) rule2
   166       handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   167     val rule4 =
   168       if term_of(Thm.lhs_of rule3) aconv term_of ct then rule3
   169       else
   170         let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
   171         in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (Thm.rhs_of rule3)) end
   172   in Thm.transitive rule4 (Thm.beta_conversion true (Thm.rhs_of rule4)) end
   173 
   174 fun rewrs_conv rules = first_conv (map rewr_conv rules);
   175 
   176 
   177 (* conversions on HHF rules *)
   178 
   179 (*rewrite B in !!x1 ... xn. B*)
   180 fun params_conv n cv ctxt ct =
   181   if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   182   then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
   183   else cv ctxt ct;
   184 
   185 (*rewrite the A's in A1 ==> ... ==> An ==> B*)
   186 fun prems_conv 0 _ ct = all_conv ct
   187   | prems_conv n cv ct =
   188       (case try Thm.dest_implies ct of
   189         NONE => all_conv ct
   190       | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
   191 
   192 (*rewrite B in A1 ==> ... ==> An ==> B*)
   193 fun concl_conv 0 cv ct = cv ct
   194   | concl_conv n cv ct =
   195       (case try Thm.dest_implies ct of
   196         NONE => cv ct
   197       | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
   198 
   199 
   200 (* conversions as inference rules *)
   201 
   202 (*forward conversion, cf. FCONV_RULE in LCF*)
   203 fun fconv_rule cv th =
   204   let val eq = cv (Thm.cprop_of th) in
   205     if Thm.is_reflexive eq then th
   206     else Thm.equal_elim eq th
   207   end;
   208 
   209 (*goal conversion*)
   210 fun gconv_rule cv i th =
   211   (case try (Thm.cprem_of th) i of
   212     SOME ct =>
   213       let val eq = cv ct in
   214         if Thm.is_reflexive eq then th
   215         else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
   216       end
   217   | NONE => raise THM ("gconv_rule", i, [th]));
   218 
   219 end;
   220 
   221 structure Basic_Conv: BASIC_CONV = Conv;
   222 open Basic_Conv;