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