src/Pure/conv.ML
author chaieb
Sat, 19 May 2007 18:19:45 +0200
changeset 23034 b3a6815754d6
parent 22937 08cf9aaf3aa1
child 23169 37091da05d8e
permissions -rw-r--r--
added binop_conv, aconvc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/conv.ML
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     3
    Author:     Amine Chaieb and Makarius
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     4
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     5
Conversions: primitive equality reasoning.
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     6
*)
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     7
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
     8
infix 1 then_conv;
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
     9
infix 0 else_conv;
23034
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
    10
infix aconvc;
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    11
signature CONV =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    12
sig
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    13
  type conv = cterm -> thm
23034
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
    14
  val aconvc : cterm * cterm -> bool
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    15
  val no_conv: conv
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    16
  val all_conv: conv
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    17
  val then_conv: conv * conv -> conv
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    18
  val else_conv: conv * conv -> conv
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    19
  val first_conv: conv list -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    20
  val every_conv: conv list -> conv
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    21
  val try_conv: conv -> conv
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    22
  val repeat_conv: conv -> conv
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    23
  val cache_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    24
  val abs_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    25
  val combination_conv: conv -> conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    26
  val comb_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    27
  val arg_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    28
  val fun_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    29
  val arg1_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    30
  val fun2_conv: conv -> conv
23034
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
    31
  val binop_conv: conv -> conv
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    32
  val forall_conv: int -> conv -> conv
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    33
  val concl_conv: int -> conv -> conv
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    34
  val prems_conv: int -> (int -> conv) -> conv
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    35
  val goals_conv: (int -> bool) -> conv -> conv
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    36
  val fconv_rule: conv -> thm -> thm
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    37
end;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    38
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    39
structure Conv: CONV =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    40
struct
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    41
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    42
(* conversionals *)
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    43
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    44
type conv = cterm -> thm;
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    45
23034
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
    46
fun s aconvc t = term_of s aconv term_of t;
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
    47
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    48
fun no_conv _ = raise CTERM ("no conversion", []);
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    49
val all_conv = Thm.reflexive;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    50
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    51
val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    52
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    53
fun (cv1 then_conv cv2) ct =
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    54
  let
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    55
    val eq1 = cv1 ct;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    56
    val eq2 = cv2 (Thm.rhs_of eq1);
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    57
  in
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    58
    if is_refl eq1 then eq2
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    59
    else if is_refl eq2 then eq1
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    60
    else Thm.transitive eq1 eq2
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    61
  end;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    62
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    63
fun (cv1 else_conv cv2) ct =
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    64
  (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    65
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    66
fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    67
fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    68
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    69
fun try_conv cv = cv else_conv all_conv;
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    70
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    71
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    72
fun cache_conv cv =
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    73
  let
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    74
    val cache = ref Termtab.empty;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    75
    fun conv ct =
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    76
      (case Termtab.lookup (! cache) (term_of ct) of
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    77
        SOME th => th
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    78
      | NONE =>
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    79
          let val th = cv ct
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    80
          in change cache (Termtab.update (term_of ct, th)); th end);
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    81
 in conv end;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    82
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    83
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    84
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    85
(** Pure conversions **)
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    86
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    87
(* lambda terms *)
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    88
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    89
fun abs_conv cv ct =
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    90
  (case term_of ct of
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    91
    Abs (x, _, _) =>
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    92
      let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    93
      in Thm.abstract_rule x v (cv ct') end
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    94
  | _ => raise CTERM ("abs_conv", [ct]));
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    95
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    96
fun combination_conv cv1 cv2 ct =
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    97
  let val (ct1, ct2) = Thm.dest_comb ct
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    98
  in Thm.combination (cv1 ct1) (cv2 ct2) end;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    99
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   100
fun comb_conv cv = combination_conv cv cv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   101
fun arg_conv cv = combination_conv all_conv cv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   102
fun fun_conv cv = combination_conv cv all_conv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   103
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   104
val arg1_conv = fun_conv o arg_conv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   105
val fun2_conv = fun_conv o fun_conv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   106
23034
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
   107
fun binop_conv cv = combination_conv (arg_conv cv) cv;
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   108
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   109
(* logic *)
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   110
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   111
(*rewrite B in !!x1 ... xn. B*)
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   112
fun forall_conv 0 cv ct = cv ct
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   113
  | forall_conv n cv ct =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   114
      (case try Thm.dest_comb ct of
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   115
        NONE => cv ct
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   116
      | SOME (A, B) =>
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   117
          (case (term_of A, term_of B) of
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   118
            (Const ("all", _), Abs (x, _, _)) =>
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   119
              let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   120
                Thm.combination (all_conv A)
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   121
                  (Thm.abstract_rule x v (forall_conv (n - 1) cv B'))
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   122
              end
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   123
          | _ => cv ct));
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   124
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   125
(*rewrite B in A1 ==> ... ==> An ==> B*)
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   126
fun concl_conv 0 cv ct = cv ct
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   127
  | concl_conv n cv ct =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   128
      (case try Thm.dest_implies ct of
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   129
        NONE => cv ct
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   130
      | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   131
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   132
(*rewrite the A's in A1 ==> ... ==> An ==> B*)
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   133
fun prems_conv 0 _ = all_conv
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   134
  | prems_conv n cv =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   135
      let
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   136
        fun conv i ct =
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   137
          if i = n + 1 then all_conv ct
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   138
          else
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   139
            (case try Thm.dest_implies ct of
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   140
              NONE => all_conv ct
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   141
            | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   142
  in conv 1 end;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   143
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   144
fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   145
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   146
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   147
end;