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