src/Pure/conv.ML
author wenzelm
Sun, 22 Jul 2012 12:26:41 +0200
changeset 48423 0ccf143a2a69
parent 43333 2bdec7f430d3
child 49974 791157a4179a
permissions -rw-r--r--
maintain set of source digests, including relevant parts of session entry;
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
32843
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
     2
    Author:     Amine Chaieb, TU Muenchen
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
     3
    Author:     Sascha Boehme, TU Muenchen
32843
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
     4
    Author:     Makarius
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     5
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     6
Conversions: primitive equality reasoning.
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     7
*)
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
     8
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
     9
infix 1 then_conv;
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    10
infix 0 else_conv;
23169
37091da05d8e moved aconvc to more_thm.ML;
wenzelm
parents: 23034
diff changeset
    11
30136
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
    12
signature BASIC_CONV =
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
    13
sig
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
    14
  val then_conv: conv * conv -> conv
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
    15
  val else_conv: conv * conv -> conv
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
    16
end;
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
    17
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    18
signature CONV =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    19
sig
30136
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
    20
  include BASIC_CONV
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    21
  val no_conv: conv
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    22
  val all_conv: conv
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    23
  val first_conv: conv list -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    24
  val every_conv: conv list -> conv
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    25
  val try_conv: conv -> conv
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    26
  val repeat_conv: conv -> conv
32843
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
    27
  val cache_conv: conv -> conv
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    28
  val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    29
  val combination_conv: conv -> conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    30
  val comb_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    31
  val arg_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    32
  val fun_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    33
  val arg1_conv: conv -> conv
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    34
  val fun2_conv: conv -> conv
23034
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
    35
  val binop_conv: conv -> conv
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
    36
  val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    37
  val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    38
  val implies_conv: conv -> conv -> conv
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    39
  val implies_concl_conv: conv -> conv
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    40
  val rewr_conv: thm -> conv
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
    41
  val rewrs_conv: thm list -> conv
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
    42
  val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
    43
  val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
    44
  val top_conv: (Proof.context -> conv) -> Proof.context -> conv
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
    45
  val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    46
  val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    47
  val prems_conv: int -> conv -> conv
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    48
  val concl_conv: int -> conv -> conv
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    49
  val fconv_rule: conv -> thm -> thm
23583
00751df1f98c else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents: 23534
diff changeset
    50
  val gconv_rule: conv -> int -> thm -> thm
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    51
end;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    52
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    53
structure Conv: CONV =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    54
struct
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    55
32843
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
    56
(* basic conversionals *)
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    57
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    58
fun no_conv _ = raise CTERM ("no conversion", []);
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    59
val all_conv = Thm.reflexive;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    60
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    61
fun (cv1 then_conv cv2) ct =
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    62
  let
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    63
    val eq1 = cv1 ct;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    64
    val eq2 = cv2 (Thm.rhs_of eq1);
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    65
  in
23596
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
    66
    if Thm.is_reflexive eq1 then eq2
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
    67
    else if Thm.is_reflexive eq2 then eq1
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    68
    else Thm.transitive eq1 eq2
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    69
  end;
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    70
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    71
fun (cv1 else_conv cv2) ct =
23583
00751df1f98c else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents: 23534
diff changeset
    72
  (cv1 ct
00751df1f98c else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents: 23534
diff changeset
    73
    handle THM _ => cv2 ct
00751df1f98c else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents: 23534
diff changeset
    74
      | CTERM _ => cv2 ct
00751df1f98c else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents: 23534
diff changeset
    75
      | TERM _ => cv2 ct
00751df1f98c else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents: 23534
diff changeset
    76
      | TYPE _ => cv2 ct);
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    77
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    78
fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    79
fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    80
22937
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    81
fun try_conv cv = cv else_conv all_conv;
08cf9aaf3aa1 unified names: foo_conv;
wenzelm
parents: 22926
diff changeset
    82
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    83
32843
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
    84
fun cache_conv (cv: conv) = Thm.cterm_cache cv;
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
    85
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    86
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
    87
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    88
(** Pure conversions **)
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    89
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    90
(* lambda terms *)
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    91
24834
5684cbf8c895 abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents: 23656
diff changeset
    92
fun abs_conv cv ctxt ct =
23587
wenzelm
parents: 23583
diff changeset
    93
  (case Thm.term_of ct of
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
    94
    Abs (x, _, _) =>
23596
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
    95
      let
42485
wenzelm
parents: 41248
diff changeset
    96
        val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
24834
5684cbf8c895 abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents: 23656
diff changeset
    97
        val (v, ct') = Thm.dest_abs (SOME u) ct;
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
    98
        val eq = cv (v, ctxt') ct';
23596
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
    99
      in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   100
  | _ => raise CTERM ("abs_conv", [ct]));
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   101
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   102
fun combination_conv cv1 cv2 ct =
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   103
  let val (ct1, ct2) = Thm.dest_comb ct
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   104
  in Thm.combination (cv1 ct1) (cv2 ct2) end;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   105
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   106
fun comb_conv cv = combination_conv cv cv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   107
fun arg_conv cv = combination_conv all_conv cv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   108
fun fun_conv cv = combination_conv cv all_conv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   109
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   110
val arg1_conv = fun_conv o arg_conv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   111
val fun2_conv = fun_conv o fun_conv;
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   112
23034
b3a6815754d6 added binop_conv, aconvc
chaieb
parents: 22937
diff changeset
   113
fun binop_conv cv = combination_conv (arg_conv cv) cv;
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   114
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   115
fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt);
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   116
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   117
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   118
(* subterm structure *)
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   119
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   120
(*cf. SUB_CONV in HOL*)
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   121
fun sub_conv conv ctxt =
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   122
  comb_conv (conv ctxt) else_conv
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   123
  abs_conv (conv o snd) ctxt else_conv
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   124
  all_conv;
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   125
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   126
(*cf. BOTTOM_CONV in HOL*)
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   127
fun bottom_conv conv ctxt ct =
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   128
  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct;
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   129
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   130
(*cf. TOP_CONV in HOL*)
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   131
fun top_conv conv ctxt ct =
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   132
  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct;
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   133
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   134
(*cf. TOP_SWEEP_CONV in HOL*)
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   135
fun top_sweep_conv conv ctxt ct =
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   136
  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct;
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   137
23169
37091da05d8e moved aconvc to more_thm.ML;
wenzelm
parents: 23034
diff changeset
   138
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   139
(* primitive logic *)
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   140
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   141
fun forall_conv cv ctxt ct =
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   142
  (case Thm.term_of ct of
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   143
    Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   144
  | _ => raise CTERM ("forall_conv", [ct]));
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   145
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   146
fun implies_conv cv1 cv2 ct =
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   147
  (case Thm.term_of ct of
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   148
    Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   149
  | _ => raise CTERM ("implies_conv", [ct]));
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   150
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   151
fun implies_concl_conv cv ct =
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   152
  (case Thm.term_of ct of
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   153
    Const ("==>", _) $ _ $ _ => arg_conv cv ct
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   154
  | _ => raise CTERM ("implies_concl_conv", [ct]));
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   155
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   156
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   157
(* single rewrite step, cf. REWR_CONV in HOL *)
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   158
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   159
fun rewr_conv rule ct =
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   160
  let
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   161
    val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   162
    val lhs = Thm.lhs_of rule1;
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   163
    val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   164
  in
43333
2bdec7f430d3 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents: 42485
diff changeset
   165
    Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   166
      handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   167
  end;
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   168
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   169
fun rewrs_conv rules = first_conv (map rewr_conv rules);
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 32843
diff changeset
   170
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   171
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   172
(* conversions on HHF rules *)
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   173
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   174
(*rewrite B in !!x1 ... xn. B*)
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   175
fun params_conv n cv ctxt ct =
27332
94790a9620c3 Logic.is_all;
wenzelm
parents: 26571
diff changeset
   176
  if n <> 0 andalso Logic.is_all (Thm.term_of ct)
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   177
  then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
24834
5684cbf8c895 abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents: 23656
diff changeset
   178
  else cv ctxt ct;
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   179
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   180
(*rewrite the A's in A1 ==> ... ==> An ==> B*)
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   181
fun prems_conv 0 _ ct = all_conv ct
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   182
  | prems_conv n cv ct =
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   183
      (case try Thm.dest_implies ct of
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   184
        NONE => all_conv ct
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   185
      | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   186
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   187
(*rewrite B in A1 ==> ... ==> An ==> B*)
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   188
fun concl_conv 0 cv ct = cv ct
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   189
  | concl_conv n cv ct =
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   190
      (case try Thm.dest_implies ct of
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   191
        NONE => cv ct
22926
fb6917e426da more conversions;
wenzelm
parents: 22905
diff changeset
   192
      | 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
   193
23596
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   194
26571
114da911bc41 abs_conv: extra argument for bound variable;
wenzelm
parents: 26130
diff changeset
   195
(* conversions as inference rules *)
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   196
23596
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   197
(*forward conversion, cf. FCONV_RULE in LCF*)
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   198
fun fconv_rule cv th =
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   199
  let val eq = cv (Thm.cprop_of th) in
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   200
    if Thm.is_reflexive eq then th
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   201
    else Thm.equal_elim eq th
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   202
  end;
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   203
23596
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   204
(*goal conversion*)
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   205
fun gconv_rule cv i th =
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   206
  (case try (Thm.cprem_of th) i of
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   207
    SOME ct =>
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   208
      let val eq = cv ct in
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   209
        if Thm.is_reflexive eq then th
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   210
        else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   211
      end
f8381a95c49c moved type conv to thm.ML;
wenzelm
parents: 23587
diff changeset
   212
  | NONE => raise THM ("gconv_rule", i, [th]));
23411
c524900454f3 Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
chaieb
parents: 23169
diff changeset
   213
22905
dab6a898b47c Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff changeset
   214
end;
30136
6a874aedb964 Made then_conv and else_conv available as infix operations.
boehmes
parents: 29606
diff changeset
   215
32843
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
   216
structure Basic_Conv: BASIC_CONV = Conv;
c8f5a7c8353f moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm
parents: 30136
diff changeset
   217
open Basic_Conv;