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