src/Pure/conjunction.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 67721 5348bea4accd
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
wenzelm@19416
     1
(*  Title:      Pure/conjunction.ML
wenzelm@19416
     2
    Author:     Makarius
wenzelm@19416
     3
wenzelm@19416
     4
Meta-level conjunction.
wenzelm@19416
     5
*)
wenzelm@19416
     6
wenzelm@19416
     7
signature CONJUNCTION =
wenzelm@19416
     8
sig
wenzelm@19416
     9
  val conjunction: cterm
wenzelm@19416
    10
  val mk_conjunction: cterm * cterm -> cterm
wenzelm@23422
    11
  val mk_conjunction_balanced: cterm list -> cterm
wenzelm@19416
    12
  val dest_conjunction: cterm -> cterm * cterm
wenzelm@30823
    13
  val dest_conjunctions: cterm -> cterm list
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@60623
    22
  val elim_conjunctions: thm -> thm list
wenzelm@23422
    23
  val elim_balanced: int -> thm -> thm list
wenzelm@23422
    24
  val curry_balanced: int -> thm -> thm
wenzelm@23422
    25
  val uncurry_balanced: int -> thm -> thm
wenzelm@19416
    26
end;
wenzelm@19416
    27
wenzelm@19416
    28
structure Conjunction: CONJUNCTION =
wenzelm@19416
    29
struct
wenzelm@19416
    30
wenzelm@19416
    31
(** abstract syntax **)
wenzelm@19416
    32
wenzelm@62876
    33
fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
wenzelm@33384
    34
val read_prop = certify o Simple_Syntax.read_prop;
wenzelm@19416
    35
wenzelm@26485
    36
val true_prop = certify Logic.true_prop;
wenzelm@26485
    37
val conjunction = certify Logic.conjunction;
wenzelm@23422
    38
wenzelm@46497
    39
fun mk_conjunction (A, B) = Thm.apply (Thm.apply conjunction A) B;
wenzelm@19416
    40
wenzelm@23422
    41
fun mk_conjunction_balanced [] = true_prop
wenzelm@32765
    42
  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
wenzelm@23422
    43
wenzelm@19416
    44
fun dest_conjunction ct =
wenzelm@19416
    45
  (case Thm.term_of ct of
wenzelm@26424
    46
    (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
wenzelm@23422
    47
  | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
wenzelm@19416
    48
wenzelm@30823
    49
fun dest_conjunctions ct =
wenzelm@30823
    50
  (case try dest_conjunction ct of
wenzelm@30823
    51
    NONE => [ct]
wenzelm@30823
    52
  | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
wenzelm@30823
    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@60642
    72
val A = read_prop "A" and vA = (("A", 0), propT);
wenzelm@60642
    73
val B = read_prop "B" and vB = (("B", 0), propT);
wenzelm@24241
    74
val C = read_prop "C";
wenzelm@67721
    75
val ABC = read_prop "A \<Longrightarrow> B \<Longrightarrow> C";
wenzelm@28856
    76
val A_B = read_prop "A &&& B";
wenzelm@19416
    77
wenzelm@26424
    78
val conjunction_def =
wenzelm@62876
    79
  Thm.unvarify_axiom (Context.the_global_context ()) "Pure.conjunction_def";
wenzelm@19416
    80
wenzelm@19416
    81
fun conjunctionD which =
wenzelm@19416
    82
  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
wenzelm@26653
    83
  Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
wenzelm@19416
    84
wenzelm@19416
    85
in
wenzelm@19416
    86
wenzelm@56436
    87
val conjunctionD1 =
wenzelm@64556
    88
  Drule.store_standard_thm (Binding.make ("conjunctionD1", \<^here>)) (conjunctionD #1);
wenzelm@56436
    89
wenzelm@56436
    90
val conjunctionD2 =
wenzelm@64556
    91
  Drule.store_standard_thm (Binding.make ("conjunctionD2", \<^here>)) (conjunctionD #2);
wenzelm@19416
    92
wenzelm@33277
    93
val conjunctionI =
wenzelm@64556
    94
  Drule.store_standard_thm (Binding.make ("conjunctionI", \<^here>))
wenzelm@33277
    95
    (Drule.implies_intr_list [A, B]
wenzelm@33277
    96
      (Thm.equal_elim
wenzelm@33277
    97
        (Thm.symmetric conjunction_def)
wenzelm@33277
    98
        (Thm.forall_intr C (Thm.implies_intr ABC
wenzelm@33277
    99
          (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
wenzelm@19416
   100
wenzelm@23422
   101
wenzelm@20508
   102
fun intr tha thb =
wenzelm@20508
   103
  Thm.implies_elim
wenzelm@20508
   104
    (Thm.implies_elim
wenzelm@20508
   105
      (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
wenzelm@20508
   106
    tha)
wenzelm@20508
   107
  thb;
wenzelm@19416
   108
wenzelm@19416
   109
fun elim th =
wenzelm@20508
   110
  let
wenzelm@20508
   111
    val (A, B) = dest_conjunction (Thm.cprop_of th)
wenzelm@20508
   112
      handle TERM (msg, _) => raise THM (msg, 0, [th]);
wenzelm@20508
   113
    val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
wenzelm@20508
   114
  in
wenzelm@20508
   115
   (Thm.implies_elim (inst conjunctionD1) th,
wenzelm@20508
   116
    Thm.implies_elim (inst conjunctionD2) th)
wenzelm@20508
   117
  end;
wenzelm@19416
   118
wenzelm@23422
   119
end;
wenzelm@23422
   120
wenzelm@60623
   121
fun elim_conjunctions th =
wenzelm@60623
   122
  (case try elim th of
wenzelm@60623
   123
    NONE => [th]
wenzelm@60623
   124
  | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2);
wenzelm@60623
   125
wenzelm@23422
   126
wenzelm@23535
   127
(* balanced conjuncts *)
wenzelm@23422
   128
wenzelm@23422
   129
fun intr_balanced [] = asm_rl
wenzelm@32765
   130
  | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
wenzelm@23422
   131
wenzelm@23422
   132
fun elim_balanced 0 _ = []
wenzelm@32765
   133
  | elim_balanced n th = Balanced_Tree.dest elim n th;
wenzelm@19416
   134
wenzelm@19416
   135
wenzelm@19416
   136
(* currying *)
wenzelm@19416
   137
wenzelm@19416
   138
local
wenzelm@19416
   139
wenzelm@62876
   140
val bootstrap_thy = Context.the_global_context ();
wenzelm@60815
   141
wenzelm@60815
   142
fun conjs n =
wenzelm@60815
   143
  let
wenzelm@60815
   144
    val As =
wenzelm@60815
   145
      map (fn A => Thm.global_cterm_of bootstrap_thy (Free (A, propT)))
wenzelm@60815
   146
        (Name.invent Name.context "A" n);
wenzelm@23422
   147
  in (As, mk_conjunction_balanced As) end;
wenzelm@19416
   148
wenzelm@24241
   149
val B = read_prop "B";
wenzelm@19416
   150
wenzelm@19416
   151
fun comp_rule th rule =
wenzelm@20260
   152
  Thm.adjust_maxidx_thm ~1 (th COMP
wenzelm@35985
   153
    (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
wenzelm@19416
   154
wenzelm@19416
   155
in
wenzelm@19416
   156
wenzelm@19416
   157
(*
wenzelm@67721
   158
  A1 &&& ... &&& An \<Longrightarrow> B
wenzelm@19416
   159
  -----------------------
wenzelm@67721
   160
  A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B
wenzelm@19416
   161
*)
wenzelm@23422
   162
fun curry_balanced n th =
wenzelm@23422
   163
  if n < 2 then th
wenzelm@23422
   164
  else
wenzelm@23422
   165
    let
wenzelm@60815
   166
      val (As, C) = conjs n;
wenzelm@23422
   167
      val D = Drule.mk_implies (C, B);
wenzelm@23422
   168
    in
wenzelm@23422
   169
      comp_rule th
wenzelm@23422
   170
        (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
wenzelm@23422
   171
          |> Drule.implies_intr_list (D :: As))
wenzelm@23422
   172
    end;
wenzelm@19416
   173
wenzelm@19416
   174
(*
wenzelm@67721
   175
  A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B
wenzelm@19416
   176
  -----------------------
wenzelm@67721
   177
  A1 &&& ... &&& An \<Longrightarrow> B
wenzelm@19416
   178
*)
wenzelm@23422
   179
fun uncurry_balanced n th =
wenzelm@23422
   180
  if n < 2 then th
wenzelm@23422
   181
  else
wenzelm@23422
   182
    let
wenzelm@60815
   183
      val (As, C) = conjs n;
wenzelm@23422
   184
      val D = Drule.list_implies (As, B);
wenzelm@23422
   185
    in
wenzelm@23422
   186
      comp_rule th
wenzelm@23422
   187
        (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
wenzelm@23422
   188
          |> Drule.implies_intr_list [D, C])
wenzelm@23422
   189
    end;
wenzelm@19416
   190
wenzelm@19416
   191
end;
wenzelm@19416
   192
wenzelm@19416
   193
end;