src/Pure/conjunction.ML

renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;

(*  Title:      Pure/conjunction.ML
    Author:     Makarius

Meta-level conjunction.
*)

signature CONJUNCTION =
sig
  val conjunction: cterm
  val mk_conjunction: cterm * cterm -> cterm
  val mk_conjunction_balanced: cterm list -> cterm
  val dest_conjunction: cterm -> cterm * cterm
  val dest_conjunctions: cterm -> cterm list
  val cong: thm -> thm -> thm
  val convs: (cterm -> thm) -> cterm -> thm
  val conjunctionD1: thm
  val conjunctionD2: thm
  val conjunctionI: thm
  val intr: thm -> thm -> thm
  val intr_balanced: thm list -> thm
  val elim: thm -> thm * thm
  val elim_balanced: int -> thm -> thm list
  val curry_balanced: int -> thm -> thm
  val uncurry_balanced: int -> thm -> thm
end;

structure Conjunction: CONJUNCTION =
struct

(** abstract syntax **)

fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
val read_prop = certify o Simple_Syntax.read_prop;

val true_prop = certify Logic.true_prop;
val conjunction = certify Logic.conjunction;

fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;

fun mk_conjunction_balanced [] = true_prop
  | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;

fun dest_conjunction ct =
  (case Thm.term_of ct of
    (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
  | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));

fun dest_conjunctions ct =
  (case try dest_conjunction ct of
    NONE => [ct]
  | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);



(** derived rules **)

(* conversion *)

val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);

fun convs cv ct =
  (case try dest_conjunction ct of
    NONE => cv ct
  | SOME (A, B) => cong (convs cv A) (convs cv B));


(* intro/elim *)

local

val A = read_prop "A" and vA = read_prop "?A";
val B = read_prop "B" and vB = read_prop "?B";
val C = read_prop "C";
val ABC = read_prop "A ==> B ==> C";
val A_B = read_prop "A &&& B";

val conjunction_def =
  Thm.unvarify_global
    (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");

fun conjunctionD which =
  Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP