src/Pure/conjunction.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24241 424cb8b5e5b4
child 24976 821628d16552
permissions -rw-r--r--
filtering out some package theorems
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
    ID:         $Id$
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     4
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     5
Meta-level conjunction.
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     6
*)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     7
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     8
signature CONJUNCTION =
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
     9
sig
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    10
  val conjunction: cterm
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    11
  val mk_conjunction: cterm * cterm -> cterm
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    12
  val mk_conjunction_balanced: cterm list -> cterm
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    13
  val dest_conjunction: cterm -> cterm * cterm
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
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    32
val cert = Thm.cterm_of ProtoPure.thy;
24241
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    33
val read_prop = cert o SimpleSyntax.read_prop;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    34
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    35
val true_prop = cert Logic.true_prop;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    36
val conjunction = cert 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
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    41
  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
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
20666
82638257d372 Thm.dest_binop;
wenzelm
parents: 20508
diff changeset
    45
    (Const ("ProtoPure.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
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    48
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    49
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    50
(** derived rules **)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    51
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    52
(* conversion *)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    53
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    54
val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    55
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    56
fun convs cv ct =
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    57
  (case try dest_conjunction ct of
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    58
    NONE => cv ct
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    59
  | SOME (A, B) => cong (convs cv A) (convs cv B));
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    60
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    61
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    62
(* intro/elim *)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    63
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    64
local
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    65
24241
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    66
val A = read_prop "A" and vA = read_prop "?A";
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    67
val B = read_prop "B" and vB = read_prop "?B";
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    68
val C = read_prop "C";
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    69
val ABC = read_prop "A ==> B ==> C";
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
    70
val A_B = read_prop "A && B";
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    71
20238
7e17d70a9303 eliminated obsolete freeze_thaw;
wenzelm
parents: 19416
diff changeset
    72
val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    73
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    74
fun conjunctionD which =
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    75
  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    76
  Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    77
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    78
in
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    79
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    80
val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    81
val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    82
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    83
val conjunctionI = Drule.store_standard_thm "conjunctionI"
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    84
  (Drule.implies_intr_list [A, B]
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    85
    (Thm.equal_elim
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    86
      (Thm.symmetric conjunction_def)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    87
      (Thm.forall_intr C (Thm.implies_intr ABC
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    88
        (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    89
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
    90
20508
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
    91
fun intr tha thb =
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
    92
  Thm.implies_elim
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
    93
    (Thm.implies_elim
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
    94
      (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
    95
    tha)
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
    96
  thb;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    97
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
    98
fun elim th =
20508
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
    99
  let
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   100
    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
   101
      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
   102
    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
   103
  in
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   104
   (Thm.implies_elim (inst conjunctionD1) th,
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   105
    Thm.implies_elim (inst conjunctionD2) th)
8182d961c7cc intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
wenzelm
parents: 20260
diff changeset
   106
  end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   107
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   108
end;
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   109
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   110
23535
58147e5bd070 removed obsolete mk_conjunction_list, intr/elim_list;
wenzelm
parents: 23422
diff changeset
   111
(* balanced conjuncts *)
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   112
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   113
fun intr_balanced [] = asm_rl
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   114
  | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   115
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   116
fun elim_balanced 0 _ = []
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   117
  | elim_balanced n th = BalancedTree.dest elim n th;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   118
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   119
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   120
(* currying *)
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   121
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   122
local
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   123
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   124
fun conjs n =
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   125
  let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   126
  in (As, mk_conjunction_balanced As) end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   127
24241
424cb8b5e5b4 SimpleSyntax.read_prop;
wenzelm
parents: 23535
diff changeset
   128
val B = read_prop "B";
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   129
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   130
fun comp_rule th rule =
20260
990dbc007ca6 Thm.adjust_maxidx;
wenzelm
parents: 20249
diff changeset
   131
  Thm.adjust_maxidx_thm ~1 (th COMP
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   132
    (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   133
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   134
in
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   135
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   136
(*
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   137
   A1 && ... && An ==> B
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   138
  -----------------------
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   139
  A1 ==> ... ==> An ==> B
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   140
*)
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   141
fun curry_balanced n th =
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   142
  if n < 2 then th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   143
  else
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   144
    let
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   145
      val (As, C) = conjs n;
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   146
      val D = Drule.mk_implies (C, B);
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   147
    in
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   148
      comp_rule th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   149
        (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   150
          |> Drule.implies_intr_list (D :: As))
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   151
    end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   152
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   153
(*
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   154
  A1 ==> ... ==> An ==> B
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   155
  -----------------------
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   156
  A1 && ... && An ==> B
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   157
*)
23422
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   158
fun uncurry_balanced n th =
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   159
  if n < 2 then th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   160
  else
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   161
    let
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   162
      val (As, C) = conjs n;
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   163
      val D = Drule.list_implies (As, B);
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   164
    in
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   165
      comp_rule th
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   166
        (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   167
          |> Drule.implies_intr_list [D, C])
4a368c087f58 balanced conjunctions;
wenzelm
parents: 21565
diff changeset
   168
    end;
19416
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   169
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   170
end;
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   171
4198e7698f6a Meta-level conjunction.
wenzelm
parents:
diff changeset
   172
end;