src/Pure/conjunction.ML
author wenzelm
Tue Sep 12 12:12:39 2006 +0200 (2006-09-12)
changeset 20508 8182d961c7cc
parent 20260 990dbc007ca6
child 20666 82638257d372
permissions -rw-r--r--
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm@19416
     1
(*  Title:      Pure/conjunction.ML
wenzelm@19416
     2
    ID:         $Id$
wenzelm@19416
     3
    Author:     Makarius
wenzelm@19416
     4
wenzelm@19416
     5
Meta-level conjunction.
wenzelm@19416
     6
*)
wenzelm@19416
     7
wenzelm@19416
     8
signature CONJUNCTION =
wenzelm@19416
     9
sig
wenzelm@19416
    10
  val conjunction: cterm
wenzelm@19416
    11
  val mk_conjunction: cterm * cterm -> cterm
wenzelm@20249
    12
  val mk_conjunction_list: cterm list -> cterm
wenzelm@19416
    13
  val dest_conjunction: cterm -> cterm * cterm
wenzelm@19416
    14
  val cong: thm -> thm -> thm
wenzelm@19416
    15
  val conv: int -> (int -> cterm -> thm) -> cterm -> thm
wenzelm@19416
    16
  val conjunctionD1: thm
wenzelm@19416
    17
  val conjunctionD2: thm
wenzelm@19416
    18
  val conjunctionI: thm
wenzelm@19416
    19
  val intr: thm -> thm -> thm
wenzelm@19416
    20
  val intr_list: thm list -> thm
wenzelm@19416
    21
  val elim: thm -> thm * thm
wenzelm@19416
    22
  val elim_list: thm -> thm list
wenzelm@19416
    23
  val elim_precise: int list -> thm -> thm list list
wenzelm@19416
    24
  val curry: int -> thm -> thm
wenzelm@19416
    25
  val uncurry: int -> thm -> thm
wenzelm@19416
    26
  val split_defined: int -> thm -> thm * thm list
wenzelm@19416
    27
end;
wenzelm@19416
    28
wenzelm@19416
    29
structure Conjunction: CONJUNCTION =
wenzelm@19416
    30
struct
wenzelm@19416
    31
wenzelm@19416
    32
wenzelm@19416
    33
(** abstract syntax **)
wenzelm@19416
    34
wenzelm@19416
    35
fun read s = Thm.read_cterm ProtoPure.thy (s, propT);
wenzelm@19416
    36
val cert = Thm.cterm_of ProtoPure.thy;
wenzelm@19416
    37
wenzelm@19416
    38
val conjunction = cert Logic.conjunction;
wenzelm@19416
    39
fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
wenzelm@19416
    40
wenzelm@20249
    41
val true_prop = read "!!dummy. PROP dummy ==> PROP dummy";
wenzelm@20249
    42
wenzelm@20249
    43
fun mk_conjunction_list [] = true_prop
wenzelm@20249
    44
  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
wenzelm@20249
    45
wenzelm@19416
    46
fun dest_conjunction ct =
wenzelm@19416
    47
  (case Thm.term_of ct of
wenzelm@19416
    48
    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct
wenzelm@19416
    49
  | _ => raise TERM ("dest_conjunction", [term_of ct]));
wenzelm@19416
    50
wenzelm@19416
    51
wenzelm@19416
    52
wenzelm@19416
    53
(** derived rules **)
wenzelm@19416
    54
wenzelm@19416
    55
(* conversion *)
wenzelm@19416
    56
wenzelm@19416
    57
(*rewrite the A's in A1 && ... && An*)
wenzelm@19416
    58
wenzelm@19416
    59
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
wenzelm@19416
    60
wenzelm@19416
    61
fun conv 0 _ = reflexive
wenzelm@19416
    62
  | conv n cv =
wenzelm@19416
    63
      let
wenzelm@19416
    64
        fun cnv i ct =
wenzelm@19416
    65
          if i = n then cv i ct
wenzelm@19416
    66
          else
wenzelm@19416
    67
            (case try dest_conjunction ct of
wenzelm@19416
    68
              NONE => cv i ct
wenzelm@19416
    69
            | SOME (A, B) => cong (cv i A) (cnv (i + 1) B));
wenzelm@19416
    70
      in cnv 1 end;
wenzelm@19416
    71
wenzelm@19416
    72
wenzelm@19416
    73
(* intro/elim *)
wenzelm@19416
    74
wenzelm@19416
    75
local
wenzelm@19416
    76
wenzelm@20508
    77
val A = read "PROP A" and vA = read "PROP ?A";
wenzelm@20508
    78
val B = read "PROP B" and vB = read "PROP ?B";
wenzelm@19416
    79
val C = read "PROP C";
wenzelm@19416
    80
val ABC = read "PROP A ==> PROP B ==> PROP C";
wenzelm@19416
    81
val A_B = read "PROP ProtoPure.conjunction(A, B)"
wenzelm@19416
    82
wenzelm@20238
    83
val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
wenzelm@19416
    84
wenzelm@19416
    85
fun conjunctionD which =
wenzelm@19416
    86
  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
wenzelm@19416
    87
  Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
wenzelm@19416
    88
wenzelm@19416
    89
in
wenzelm@19416
    90
wenzelm@19416
    91
val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
wenzelm@19416
    92
val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
wenzelm@19416
    93
wenzelm@19416
    94
val conjunctionI = Drule.store_standard_thm "conjunctionI"
wenzelm@19416
    95
  (Drule.implies_intr_list [A, B]
wenzelm@19416
    96
    (Thm.equal_elim
wenzelm@19416
    97
      (Thm.symmetric conjunction_def)
wenzelm@19416
    98
      (Thm.forall_intr C (Thm.implies_intr ABC
wenzelm@19416
    99
        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
wenzelm@19416
   100
wenzelm@20508
   101
fun intr tha thb =
wenzelm@20508
   102
  Thm.implies_elim
wenzelm@20508
   103
    (Thm.implies_elim
wenzelm@20508
   104
      (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
wenzelm@20508
   105
    tha)
wenzelm@20508
   106
  thb;
wenzelm@19416
   107
wenzelm@19416
   108
fun intr_list [] = asm_rl
wenzelm@19416
   109
  | intr_list ths = foldr1 (uncurry intr) ths;
wenzelm@19416
   110
wenzelm@19416
   111
fun elim th =
wenzelm@20508
   112
  let
wenzelm@20508
   113
    val (A, B) = dest_conjunction (Thm.cprop_of th)
wenzelm@20508
   114
      handle TERM (msg, _) => raise THM (msg, 0, [th]);
wenzelm@20508
   115
    val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
wenzelm@20508
   116
  in
wenzelm@20508
   117
   (Thm.implies_elim (inst conjunctionD1) th,
wenzelm@20508
   118
    Thm.implies_elim (inst conjunctionD2) th)
wenzelm@20508
   119
  end;
wenzelm@19416
   120
wenzelm@19416
   121
(*((A && B) && C) && D && E -- flat*)
wenzelm@19416
   122
fun elim_list th =
wenzelm@19416
   123
  let val (th1, th2) = elim th
wenzelm@19416
   124
  in elim_list th1 @ elim_list th2 end handle THM _ => [th];
wenzelm@19416
   125
wenzelm@19416
   126
(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
wenzelm@19416
   127
fun elim_precise spans =
wenzelm@19416
   128
  let
wenzelm@19416
   129
    fun elm 0 _ = []
wenzelm@19416
   130
      | elm 1 th = [th]
wenzelm@19416
   131
      | elm n th =
wenzelm@19416
   132
          let val (th1, th2) = elim th
wenzelm@19416
   133
          in th1 :: elm (n - 1) th2 end;
wenzelm@19416
   134
    fun elms (0 :: ns) ths = [] :: elms ns ths
wenzelm@19416
   135
      | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths
wenzelm@19416
   136
      | elms _ _ = [];
wenzelm@19416
   137
  in elms spans o elm (length (filter_out (equal 0) spans)) end;
wenzelm@19416
   138
wenzelm@19416
   139
end;
wenzelm@19416
   140
wenzelm@19416
   141
wenzelm@19416
   142
(* currying *)
wenzelm@19416
   143
wenzelm@19416
   144
local
wenzelm@19416
   145
wenzelm@19416
   146
fun conjs m =
wenzelm@19416
   147
  let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m)
wenzelm@19416
   148
  in (As, Logic.mk_conjunction_list As) end;
wenzelm@19416
   149
wenzelm@19416
   150
val B = Free ("B", propT);
wenzelm@19416
   151
wenzelm@19416
   152
fun comp_rule th rule =
wenzelm@20260
   153
  Thm.adjust_maxidx_thm ~1 (th COMP
wenzelm@19416
   154
    (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
wenzelm@19416
   155
wenzelm@19416
   156
in
wenzelm@19416
   157
wenzelm@19416
   158
(*
wenzelm@19416
   159
   A1 && ... && An ==> B
wenzelm@19416
   160
  -----------------------
wenzelm@19416
   161
  A1 ==> ... ==> An ==> B
wenzelm@19416
   162
*)
wenzelm@19416
   163
fun curry n th =
wenzelm@19416
   164
  let
wenzelm@19416
   165
    val k =
wenzelm@19416
   166
      (case try Logic.dest_implies (Thm.prop_of th) of
wenzelm@19416
   167
        NONE => 0
wenzelm@19416
   168
      | SOME (prem, _) => length (Logic.dest_conjunction_list prem));
wenzelm@19416
   169
    val m = if n = ~1 then k else Int.min (n, k);
wenzelm@19416
   170
  in
wenzelm@19416
   171
    if m < 2 then th
wenzelm@19416
   172
    else
wenzelm@19416
   173
      let
wenzelm@19416
   174
        val (As, C) = conjs m;
wenzelm@19416
   175
        val cAs = map cert As;
wenzelm@19416
   176
        val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert;
wenzelm@19416
   177
      in
wenzelm@19416
   178
        comp_rule th
wenzelm@19416
   179
          (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs))
wenzelm@19416
   180
            |> Drule.implies_intr_list (D :: cAs))
wenzelm@19416
   181
      end
wenzelm@19416
   182
  end;
wenzelm@19416
   183
wenzelm@19416
   184
(*
wenzelm@19416
   185
  A1 ==> ... ==> An ==> B
wenzelm@19416
   186
  -----------------------
wenzelm@19416
   187
   A1 && ... && An ==> B
wenzelm@19416
   188
*)
wenzelm@19416
   189
fun uncurry n th =
wenzelm@19416
   190
  let
wenzelm@19416
   191
    val k = Thm.nprems_of th;
wenzelm@19416
   192
    val m = if n = ~1 then k else Int.min (n, k);
wenzelm@19416
   193
  in
wenzelm@19416
   194
    if m < 2 then th
wenzelm@19416
   195
    else
wenzelm@19416
   196
      let
wenzelm@19416
   197
        val (As, C) = conjs m ||> cert;
wenzelm@19416
   198
        val D = Logic.list_implies (As, B) |> cert;
wenzelm@19416
   199
      in
wenzelm@19416
   200
        comp_rule th
wenzelm@19416
   201
          (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C))
wenzelm@19416
   202
            |> Drule.implies_intr_list [D, C])
wenzelm@19416
   203
      end
wenzelm@19416
   204
  end;
wenzelm@19416
   205
wenzelm@19416
   206
end;
wenzelm@19416
   207
wenzelm@19416
   208
wenzelm@19416
   209
(* defined conjunctions *)
wenzelm@19416
   210
wenzelm@19416
   211
fun project th 1 = (th RS conjunctionD1 handle THM _ => th)
wenzelm@19416
   212
  | project th k = project (th RS conjunctionD2) (k - 1);
wenzelm@19416
   213
wenzelm@19416
   214
fun split_defined n eq =
wenzelm@19416
   215
  let
wenzelm@19416
   216
    val intro =
wenzelm@19416
   217
      (eq RS Drule.equal_elim_rule2)
wenzelm@19416
   218
      |> curry n
wenzelm@19416
   219
      |> K (n = 0) ? Thm.eq_assumption 1;
wenzelm@19416
   220
    val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
wenzelm@19416
   221
  in (intro, dests) end;
wenzelm@19416
   222
wenzelm@19416
   223
end;