src/Pure/conjunction.ML
author wenzelm
Thu, 09 Jun 2011 20:22:22 +0200
changeset 43329 84472e198515
parent 35985 0bbf0d2348f9
child 46497 89ccf66aa73d
permissions -rw-r--r--
tuned signature: Name.invent and Name.invent_names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/conjunction.ML
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     3
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     4
Meta-level conjunction.
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     5
*)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     6
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     7
signature CONJUNCTION =
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     8
sig
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     9
  val conjunction: cterm
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    10
  val mk_conjunction: cterm * cterm -> cterm
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    11
  val mk_conjunction_balanced: cterm list -> cterm
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    12
  val dest_conjunction: cterm -> cterm * cterm
30823
eb99b9134f2e added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents: 29606
diff changeset
    13
  val dest_conjunctions: cterm -> cterm list
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    14
  val cong: thm -> thm -> thm
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    15
  val convs: (cterm -> thm) -> cterm -> thm
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    16
  val conjunctionD1: thm
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    17
  val conjunctionD2: thm
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    18
  val conjunctionI: thm
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    19
  val intr: thm -> thm -> thm
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    20
  val intr_balanced: thm list -> thm
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    21
  val elim: thm -> thm * thm
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    22
  val elim_balanced: int -> thm -> thm list
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    23
  val curry_balanced: int -> thm -> thm
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    24
  val uncurry_balanced: int -> thm -> thm
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    25
end;
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    26
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    27
structure Conjunction: CONJUNCTION =
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    28
struct
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    29
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    30
(** abstract syntax **)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    31
26485
b90d1fc201de certify wrt. dynamic context;
wenzelm
parents: 26424
diff changeset
    32
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
33384
1b5ba4e6a953 modernized structure Simple_Syntax;
wenzelm
parents: 33277
diff changeset
    33
val read_prop = certify o Simple_Syntax.read_prop;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    34
26485
b90d1fc201de certify wrt. dynamic context;
wenzelm
parents: 26424
diff changeset
    35
val true_prop = certify Logic.true_prop;
b90d1fc201de certify wrt. dynamic context;
wenzelm
parents: 26424
diff changeset
    36
val conjunction = certify Logic.conjunction;
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    37
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    38
fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    39
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    40
fun mk_conjunction_balanced [] = true_prop
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 30823
diff changeset
    41
  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    42
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    43
fun dest_conjunction ct =
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    44
  (case Thm.term_of ct of
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 24976
diff changeset
    45
    (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    46
  | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    47
30823
eb99b9134f2e added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents: 29606
diff changeset
    48
fun dest_conjunctions ct =
eb99b9134f2e added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents: 29606
diff changeset
    49
  (case try dest_conjunction ct of
eb99b9134f2e added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents: 29606
diff changeset
    50
    NONE => [ct]
eb99b9134f2e added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents: 29606
diff changeset
    51
  | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
eb99b9134f2e added dest_conjunctions (cf. Logic.dest_conjunctions);
wenzelm
parents: 29606
diff changeset
    52
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    53
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    54
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    55
(** derived rules **)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    56
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    57
(* conversion *)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    58
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    59
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    60
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    61
fun convs cv ct =
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    62
  (case try dest_conjunction ct of
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    63
    NONE => cv ct
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    64
  | SOME (A, B) => cong (convs cv A) (convs cv B));
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    65
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    66
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    67
(* intro/elim *)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    68
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    69
local
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    70
24241
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    71
val A = read_prop "A" and vA = read_prop "?A";
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    72
val B = read_prop "B" and vB = read_prop "?B";
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    73
val C = read_prop "C";
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    74
val ABC = read_prop "A ==> B ==> C";
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28674
diff changeset
    75
val A_B = read_prop "A &&& B";
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    76
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 24976
diff changeset
    77
val conjunction_def =
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 33384
diff changeset
    78
  Thm.unvarify_global
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 33384
diff changeset
    79
    (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    80
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    81
fun conjunctionD which =
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    82
  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
26653
60e0cf6bef89 Thm.forall_elim_var(s);
wenzelm
parents: 26485
diff changeset
    83
  Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    84
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    85
in
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    86
33277
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    87
val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    88
val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    89
33277
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    90
val conjunctionI =
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    91
  Drule.store_standard_thm (Binding.name "conjunctionI")
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    92
    (Drule.implies_intr_list [A, B]
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    93
      (Thm.equal_elim
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    94
        (Thm.symmetric conjunction_def)
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    95
        (Thm.forall_intr C (Thm.implies_intr ABC
1bdc3c732fdd Drule.store: proper binding;
wenzelm
parents: 32765
diff changeset
    96
          (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    97
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    98
20508
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
    99
fun intr tha thb =
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   100
  Thm.implies_elim
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   101
    (Thm.implies_elim
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   102
      (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   103
    tha)
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   104
  thb;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   105
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   106
fun elim th =
20508
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   107
  let
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   108
    val (A, B) = dest_conjunction (Thm.cprop_of th)
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   109
      handle TERM (msg, _) => raise THM (msg, 0, [th]);
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   110
    val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   111
  in
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   112
   (Thm.implies_elim (inst conjunctionD1) th,
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   113
    Thm.implies_elim (inst conjunctionD2) th)
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   114
  end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   115
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   116
end;
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   117
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   118
23535
58147e5bd070 removed obsolete mk_conjunction_list, intr/elim_list;
wenzelm
parents: 23422
diff changeset
   119
(* balanced conjuncts *)
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   120
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   121
fun intr_balanced [] = asm_rl
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 30823
diff changeset
   122
  | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   123
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   124
fun elim_balanced 0 _ = []
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 30823
diff changeset
   125
  | elim_balanced n th = Balanced_Tree.dest elim n th;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   126
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   127
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   128
(* currying *)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   129
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   130
local
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   131
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 24976
diff changeset
   132
fun conjs thy n =
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 35985
diff changeset
   133
  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   134
  in (As, mk_conjunction_balanced As) end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   135
24241
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
   136
val B = read_prop "B";
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   137
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   138
fun comp_rule th rule =
20260
990dbc007ca6 Thm.adjust_maxidx;
wenzelm
parents: 20249
diff changeset
   139
  Thm.adjust_maxidx_thm ~1 (th COMP
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35845
diff changeset
   140
    (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   141
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   142
in
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   143
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   144
(*
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28674
diff changeset
   145
  A1 &&& ... &&& An ==> B
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   146
  -----------------------
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   147
  A1 ==> ... ==> An ==> B
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   148
*)
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   149
fun curry_balanced n th =
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   150
  if n < 2 then th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   151
  else
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   152
    let
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 24976
diff changeset
   153
      val thy = Thm.theory_of_thm th;
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 24976
diff changeset
   154
      val (As, C) = conjs thy n;
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   155
      val D = Drule.mk_implies (C, B);
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   156
    in
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   157
      comp_rule th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   158
        (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   159
          |> Drule.implies_intr_list (D :: As))
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   160
    end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   161
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   162
(*
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   163
  A1 ==> ... ==> An ==> B
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   164
  -----------------------
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28674
diff changeset
   165
  A1 &&& ... &&& An ==> B
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   166
*)
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   167
fun uncurry_balanced n th =
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   168
  if n < 2 then th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   169
  else
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   170
    let
26424
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 24976
diff changeset
   171
      val thy = Thm.theory_of_thm th;
a6cad32a27b0 eliminated theory ProtoPure;
wenzelm
parents: 24976
diff changeset
   172
      val (As, C) = conjs thy n;
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   173
      val D = Drule.list_implies (As, B);
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   174
    in
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   175
      comp_rule th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   176
        (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   177
          |> Drule.implies_intr_list [D, C])
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   178
    end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   179
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   180
end;
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   181
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   182
end;