src/Pure/conjunction.ML
author wenzelm
Tue Jun 19 23:15:49 2007 +0200 (2007-06-19)
changeset 23422 4a368c087f58
parent 21565 bd28361f4c5b
child 23535 58147e5bd070
permissions -rw-r--r--
balanced conjunctions;
tuned interfaces;
tuned;
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@23422
    13
  val mk_conjunction_balanced: cterm list -> cterm
wenzelm@19416
    14
  val dest_conjunction: cterm -> cterm * cterm
wenzelm@19416
    15
  val cong: thm -> thm -> thm
wenzelm@23422
    16
  val convs: (cterm -> thm) -> cterm -> thm
wenzelm@19416
    17
  val conjunctionD1: thm
wenzelm@19416
    18
  val conjunctionD2: thm
wenzelm@19416
    19
  val conjunctionI: thm
wenzelm@19416
    20
  val intr: thm -> thm -> thm
wenzelm@19416
    21
  val intr_list: thm list -> thm
wenzelm@23422
    22
  val intr_balanced: thm list -> thm
wenzelm@19416
    23
  val elim: thm -> thm * thm
wenzelm@19416
    24
  val elim_list: thm -> thm list
wenzelm@23422
    25
  val elim_balanced: int -> thm -> thm list
wenzelm@23422
    26
  val curry_balanced: int -> thm -> thm
wenzelm@23422
    27
  val uncurry_balanced: int -> thm -> thm
wenzelm@19416
    28
end;
wenzelm@19416
    29
wenzelm@19416
    30
structure Conjunction: CONJUNCTION =
wenzelm@19416
    31
struct
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@23422
    38
val true_prop = cert Logic.true_prop;
wenzelm@19416
    39
val conjunction = cert Logic.conjunction;
wenzelm@23422
    40
wenzelm@19416
    41
fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
wenzelm@19416
    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@23422
    46
fun mk_conjunction_balanced [] = true_prop
wenzelm@23422
    47
  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
wenzelm@23422
    48
wenzelm@19416
    49
fun dest_conjunction ct =
wenzelm@19416
    50
  (case Thm.term_of ct of
wenzelm@20666
    51
    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
wenzelm@23422
    52
  | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
wenzelm@19416
    53
wenzelm@19416
    54
wenzelm@19416
    55
wenzelm@19416
    56
(** derived rules **)
wenzelm@19416
    57
wenzelm@19416
    58
(* conversion *)
wenzelm@19416
    59
wenzelm@19416
    60
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
wenzelm@19416
    61
wenzelm@23422
    62
fun convs cv ct =
wenzelm@23422
    63
  (case try dest_conjunction ct of
wenzelm@23422
    64
    NONE => cv ct
wenzelm@23422
    65
  | SOME (A, B) => cong (convs cv A) (convs cv B));
wenzelm@19416
    66
wenzelm@19416
    67
wenzelm@19416
    68
(* intro/elim *)
wenzelm@19416
    69
wenzelm@19416
    70
local
wenzelm@19416
    71
wenzelm@20508
    72
val A = read "PROP A" and vA = read "PROP ?A";
wenzelm@20508
    73
val B = read "PROP B" and vB = read "PROP ?B";
wenzelm@19416
    74
val C = read "PROP C";
wenzelm@19416
    75
val ABC = read "PROP A ==> PROP B ==> PROP C";
wenzelm@19416
    76
val A_B = read "PROP ProtoPure.conjunction(A, B)"
wenzelm@19416
    77
wenzelm@20238
    78
val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
wenzelm@19416
    79
wenzelm@19416
    80
fun conjunctionD which =
wenzelm@19416
    81
  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
wenzelm@19416
    82
  Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
wenzelm@19416
    83
wenzelm@19416
    84
in
wenzelm@19416
    85
wenzelm@19416
    86
val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
wenzelm@19416
    87
val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
wenzelm@19416
    88
wenzelm@19416
    89
val conjunctionI = Drule.store_standard_thm "conjunctionI"
wenzelm@19416
    90
  (Drule.implies_intr_list [A, B]
wenzelm@19416
    91
    (Thm.equal_elim
wenzelm@19416
    92
      (Thm.symmetric conjunction_def)
wenzelm@19416
    93
      (Thm.forall_intr C (Thm.implies_intr ABC
wenzelm@19416
    94
        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
wenzelm@19416
    95
wenzelm@23422
    96
wenzelm@20508
    97
fun intr tha thb =
wenzelm@20508
    98
  Thm.implies_elim
wenzelm@20508
    99
    (Thm.implies_elim
wenzelm@20508
   100
      (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
wenzelm@20508
   101
    tha)
wenzelm@20508
   102
  thb;
wenzelm@19416
   103
wenzelm@19416
   104
fun elim th =
wenzelm@20508
   105
  let
wenzelm@20508
   106
    val (A, B) = dest_conjunction (Thm.cprop_of th)
wenzelm@20508
   107
      handle TERM (msg, _) => raise THM (msg, 0, [th]);
wenzelm@20508
   108
    val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
wenzelm@20508
   109
  in
wenzelm@20508
   110
   (Thm.implies_elim (inst conjunctionD1) th,
wenzelm@20508
   111
    Thm.implies_elim (inst conjunctionD2) th)
wenzelm@20508
   112
  end;
wenzelm@19416
   113
wenzelm@23422
   114
end;
wenzelm@23422
   115
wenzelm@23422
   116
wenzelm@23422
   117
(* multiple conjuncts *)
wenzelm@23422
   118
wenzelm@23422
   119
fun intr_list [] = asm_rl
wenzelm@23422
   120
  | intr_list ths = foldr1 (uncurry intr) ths;
wenzelm@23422
   121
wenzelm@23422
   122
fun intr_balanced [] = asm_rl
wenzelm@23422
   123
  | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
wenzelm@23422
   124
wenzelm@23422
   125
fun elim_list th =   (* FIXME improper!? rename to "elims" *)
wenzelm@19416
   126
  let val (th1, th2) = elim th
wenzelm@19416
   127
  in elim_list th1 @ elim_list th2 end handle THM _ => [th];
wenzelm@19416
   128
wenzelm@23422
   129
fun elim_balanced 0 _ = []
wenzelm@23422
   130
  | elim_balanced n th = BalancedTree.dest elim n th;
wenzelm@19416
   131
wenzelm@19416
   132
wenzelm@19416
   133
(* currying *)
wenzelm@19416
   134
wenzelm@19416
   135
local
wenzelm@19416
   136
wenzelm@23422
   137
fun conjs n =
wenzelm@23422
   138
  let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
wenzelm@23422
   139
  in (As, mk_conjunction_balanced As) end;
wenzelm@19416
   140
wenzelm@23422
   141
val B = cert (Free ("B", propT));
wenzelm@19416
   142
wenzelm@19416
   143
fun comp_rule th rule =
wenzelm@20260
   144
  Thm.adjust_maxidx_thm ~1 (th COMP
wenzelm@19416
   145
    (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
wenzelm@19416
   146
wenzelm@19416
   147
in
wenzelm@19416
   148
wenzelm@19416
   149
(*
wenzelm@19416
   150
   A1 && ... && An ==> B
wenzelm@19416
   151
  -----------------------
wenzelm@19416
   152
  A1 ==> ... ==> An ==> B
wenzelm@19416
   153
*)
wenzelm@23422
   154
fun curry_balanced n th =
wenzelm@23422
   155
  if n < 2 then th
wenzelm@23422
   156
  else
wenzelm@23422
   157
    let
wenzelm@23422
   158
      val (As, C) = conjs n;
wenzelm@23422
   159
      val D = Drule.mk_implies (C, B);
wenzelm@23422
   160
    in
wenzelm@23422
   161
      comp_rule th
wenzelm@23422
   162
        (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
wenzelm@23422
   163
          |> Drule.implies_intr_list (D :: As))
wenzelm@23422
   164
    end;
wenzelm@19416
   165
wenzelm@19416
   166
(*
wenzelm@19416
   167
  A1 ==> ... ==> An ==> B
wenzelm@19416
   168
  -----------------------
wenzelm@23422
   169
  A1 && ... && An ==> B
wenzelm@19416
   170
*)
wenzelm@23422
   171
fun uncurry_balanced n th =
wenzelm@23422
   172
  if n < 2 then th
wenzelm@23422
   173
  else
wenzelm@23422
   174
    let
wenzelm@23422
   175
      val (As, C) = conjs n;
wenzelm@23422
   176
      val D = Drule.list_implies (As, B);
wenzelm@23422
   177
    in
wenzelm@23422
   178
      comp_rule th
wenzelm@23422
   179
        (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
wenzelm@23422
   180
          |> Drule.implies_intr_list [D, C])
wenzelm@23422
   181
    end;
wenzelm@19416
   182
wenzelm@19416
   183
end;
wenzelm@19416
   184
wenzelm@19416
   185
end;