src/Pure/conjunction.ML
author wenzelm
Thu Nov 20 00:03:47 2008 +0100 (2008-11-20)
changeset 28856 5e009a80fe6d
parent 28674 08a77c495dc1
child 29606 fedb8be05f24
permissions -rw-r--r--
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
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@23422
    12
  val mk_conjunction_balanced: cterm list -> cterm
wenzelm@19416
    13
  val dest_conjunction: cterm -> cterm * cterm
wenzelm@19416
    14
  val cong: thm -> thm -> thm
wenzelm@23422
    15
  val convs: (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@23422
    20
  val intr_balanced: thm list -> thm
wenzelm@19416
    21
  val elim: thm -> thm * thm
wenzelm@23422
    22
  val elim_balanced: int -> thm -> thm list
wenzelm@23422
    23
  val curry_balanced: int -> thm -> thm
wenzelm@23422
    24
  val uncurry_balanced: int -> thm -> thm
wenzelm@19416
    25
end;
wenzelm@19416
    26
wenzelm@19416
    27
structure Conjunction: CONJUNCTION =
wenzelm@19416
    28
struct
wenzelm@19416
    29
wenzelm@19416
    30
(** abstract syntax **)
wenzelm@19416
    31
wenzelm@26485
    32
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
wenzelm@26485
    33
val read_prop = certify o SimpleSyntax.read_prop;
wenzelm@19416
    34
wenzelm@26485
    35
val true_prop = certify Logic.true_prop;
wenzelm@26485
    36
val conjunction = certify Logic.conjunction;
wenzelm@23422
    37
wenzelm@19416
    38
fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
wenzelm@19416
    39
wenzelm@23422
    40
fun mk_conjunction_balanced [] = true_prop
wenzelm@23422
    41
  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
wenzelm@23422
    42
wenzelm@19416
    43
fun dest_conjunction ct =
wenzelm@19416
    44
  (case Thm.term_of ct of
wenzelm@26424
    45
    (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
wenzelm@23422
    46
  | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
wenzelm@19416
    47
wenzelm@19416
    48
wenzelm@19416
    49
wenzelm@19416
    50
(** derived rules **)
wenzelm@19416
    51
wenzelm@19416
    52
(* conversion *)
wenzelm@19416
    53
wenzelm@19416
    54
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
wenzelm@19416
    55
wenzelm@23422
    56
fun convs cv ct =
wenzelm@23422
    57
  (case try dest_conjunction ct of
wenzelm@23422
    58
    NONE => cv ct
wenzelm@23422
    59
  | SOME (A, B) => cong (convs cv A) (convs cv B));
wenzelm@19416
    60
wenzelm@19416
    61
wenzelm@19416
    62
(* intro/elim *)
wenzelm@19416
    63
wenzelm@19416
    64
local
wenzelm@19416
    65
wenzelm@24241
    66
val A = read_prop "A" and vA = read_prop "?A";
wenzelm@24241
    67
val B = read_prop "B" and vB = read_prop "?B";
wenzelm@24241
    68
val C = read_prop "C";
wenzelm@24241
    69
val ABC = read_prop "A ==> B ==> C";
wenzelm@28856
    70
val A_B = read_prop "A &&& B";
wenzelm@19416
    71
wenzelm@26424
    72
val conjunction_def =
wenzelm@28674
    73
  Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
wenzelm@19416
    74
wenzelm@19416
    75
fun conjunctionD which =
wenzelm@19416
    76
  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
wenzelm@26653
    77
  Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
wenzelm@19416
    78
wenzelm@19416
    79
in
wenzelm@19416
    80
wenzelm@19416
    81
val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
wenzelm@19416
    82
val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
wenzelm@19416
    83
wenzelm@19416
    84
val conjunctionI = Drule.store_standard_thm "conjunctionI"
wenzelm@19416
    85
  (Drule.implies_intr_list [A, B]
wenzelm@19416
    86
    (Thm.equal_elim
wenzelm@19416
    87
      (Thm.symmetric conjunction_def)
wenzelm@19416
    88
      (Thm.forall_intr C (Thm.implies_intr ABC
wenzelm@19416
    89
        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
wenzelm@19416
    90
wenzelm@23422
    91
wenzelm@20508
    92
fun intr tha thb =
wenzelm@20508
    93
  Thm.implies_elim
wenzelm@20508
    94
    (Thm.implies_elim
wenzelm@20508
    95
      (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
wenzelm@20508
    96
    tha)
wenzelm@20508
    97
  thb;
wenzelm@19416
    98
wenzelm@19416
    99
fun elim th =
wenzelm@20508
   100
  let
wenzelm@20508
   101
    val (A, B) = dest_conjunction (Thm.cprop_of th)
wenzelm@20508
   102
      handle TERM (msg, _) => raise THM (msg, 0, [th]);
wenzelm@20508
   103
    val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
wenzelm@20508
   104
  in
wenzelm@20508
   105
   (Thm.implies_elim (inst conjunctionD1) th,
wenzelm@20508
   106
    Thm.implies_elim (inst conjunctionD2) th)
wenzelm@20508
   107
  end;
wenzelm@19416
   108
wenzelm@23422
   109
end;
wenzelm@23422
   110
wenzelm@23422
   111
wenzelm@23535
   112
(* balanced conjuncts *)
wenzelm@23422
   113
wenzelm@23422
   114
fun intr_balanced [] = asm_rl
wenzelm@23422
   115
  | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
wenzelm@23422
   116
wenzelm@23422
   117
fun elim_balanced 0 _ = []
wenzelm@23422
   118
  | elim_balanced n th = BalancedTree.dest elim n th;
wenzelm@19416
   119
wenzelm@19416
   120
wenzelm@19416
   121
(* currying *)
wenzelm@19416
   122
wenzelm@19416
   123
local
wenzelm@19416
   124
wenzelm@26424
   125
fun conjs thy n =
wenzelm@26424
   126
  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
wenzelm@23422
   127
  in (As, mk_conjunction_balanced As) end;
wenzelm@19416
   128
wenzelm@24241
   129
val B = read_prop "B";
wenzelm@19416
   130
wenzelm@19416
   131
fun comp_rule th rule =
wenzelm@20260
   132
  Thm.adjust_maxidx_thm ~1 (th COMP
wenzelm@26653
   133
    (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
wenzelm@19416
   134
wenzelm@19416
   135
in
wenzelm@19416
   136
wenzelm@19416
   137
(*
wenzelm@28856
   138
  A1 &&& ... &&& An ==> B
wenzelm@19416
   139
  -----------------------
wenzelm@19416
   140
  A1 ==> ... ==> An ==> B
wenzelm@19416
   141
*)
wenzelm@23422
   142
fun curry_balanced n th =
wenzelm@23422
   143
  if n < 2 then th
wenzelm@23422
   144
  else
wenzelm@23422
   145
    let
wenzelm@26424
   146
      val thy = Thm.theory_of_thm th;
wenzelm@26424
   147
      val (As, C) = conjs thy n;
wenzelm@23422
   148
      val D = Drule.mk_implies (C, B);
wenzelm@23422
   149
    in
wenzelm@23422
   150
      comp_rule th
wenzelm@23422
   151
        (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
wenzelm@23422
   152
          |> Drule.implies_intr_list (D :: As))
wenzelm@23422
   153
    end;
wenzelm@19416
   154
wenzelm@19416
   155
(*
wenzelm@19416
   156
  A1 ==> ... ==> An ==> B
wenzelm@19416
   157
  -----------------------
wenzelm@28856
   158
  A1 &&& ... &&& An ==> B
wenzelm@19416
   159
*)
wenzelm@23422
   160
fun uncurry_balanced n th =
wenzelm@23422
   161
  if n < 2 then th
wenzelm@23422
   162
  else
wenzelm@23422
   163
    let
wenzelm@26424
   164
      val thy = Thm.theory_of_thm th;
wenzelm@26424
   165
      val (As, C) = conjs thy n;
wenzelm@23422
   166
      val D = Drule.list_implies (As, B);
wenzelm@23422
   167
    in
wenzelm@23422
   168
      comp_rule th
wenzelm@23422
   169
        (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
wenzelm@23422
   170
          |> Drule.implies_intr_list [D, C])
wenzelm@23422
   171
    end;
wenzelm@19416
   172
wenzelm@19416
   173
end;
wenzelm@19416
   174
wenzelm@19416
   175
end;