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