src/Pure/conjunction.ML
author wenzelm
Sat Jul 29 00:51:31 2006 +0200 (2006-07-29)
changeset 20249 a13adb4f94dc
parent 20238 7e17d70a9303
child 20260 990dbc007ca6
permissions -rw-r--r--
added mk_conjunction_list;
     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 dest_conjunction: cterm -> cterm * cterm
    14   val cong: thm -> thm -> thm
    15   val conv: int -> (int -> 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_list: thm list -> thm
    21   val elim: thm -> thm * thm
    22   val elim_list: thm -> thm list
    23   val elim_precise: int list -> thm -> thm list list
    24   val curry: int -> thm -> thm
    25   val uncurry: int -> thm -> thm
    26   val split_defined: int -> thm -> thm * thm list
    27 end;
    28 
    29 structure Conjunction: CONJUNCTION =
    30 struct
    31 
    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 conjunction = cert Logic.conjunction;
    39 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    40 
    41 val true_prop = read "!!dummy. PROP dummy ==> PROP dummy";
    42 
    43 fun mk_conjunction_list [] = true_prop
    44   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    45 
    46 fun dest_conjunction ct =
    47   (case Thm.term_of ct of
    48     (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct
    49   | _ => raise TERM ("dest_conjunction", [term_of ct]));
    50 
    51 
    52 
    53 (** derived rules **)
    54 
    55 (* conversion *)
    56 
    57 (*rewrite the A's in A1 && ... && An*)
    58 
    59 val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
    60 
    61 fun conv 0 _ = reflexive
    62   | conv n cv =
    63       let
    64         fun cnv i ct =
    65           if i = n then cv i ct
    66           else
    67             (case try dest_conjunction ct of
    68               NONE => cv i ct
    69             | SOME (A, B) => cong (cv i A) (cnv (i + 1) B));
    70       in cnv 1 end;
    71 
    72 
    73 (* intro/elim *)
    74 
    75 local
    76 
    77 val A = read "PROP A";
    78 val B = read "PROP B";
    79 val C = read "PROP C";
    80 val ABC = read "PROP A ==> PROP B ==> PROP C";
    81 val A_B = read "PROP ProtoPure.conjunction(A, B)"
    82 
    83 val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
    84 
    85 fun conjunctionD which =
    86   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
    87   Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
    88 
    89 in
    90 
    91 val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1);
    92 val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2);
    93 
    94 val conjunctionI = Drule.store_standard_thm "conjunctionI"
    95   (Drule.implies_intr_list [A, B]
    96     (Thm.equal_elim
    97       (Thm.symmetric conjunction_def)
    98       (Thm.forall_intr C (Thm.implies_intr ABC
    99         (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
   100 
   101 fun intr tha thb = thb COMP (tha COMP Drule.incr_indexes2 tha thb conjunctionI);
   102 
   103 fun intr_list [] = asm_rl
   104   | intr_list ths = foldr1 (uncurry intr) ths;
   105 
   106 fun elim th =
   107  (th COMP Drule.incr_indexes th conjunctionD1,
   108   th COMP Drule.incr_indexes th conjunctionD2);
   109 
   110 (*((A && B) && C) && D && E -- flat*)
   111 fun elim_list th =
   112   let val (th1, th2) = elim th
   113   in elim_list th1 @ elim_list th2 end handle THM _ => [th];
   114 
   115 (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   116 fun elim_precise spans =
   117   let
   118     fun elm 0 _ = []
   119       | elm 1 th = [th]
   120       | elm n th =
   121           let val (th1, th2) = elim th
   122           in th1 :: elm (n - 1) th2 end;
   123     fun elms (0 :: ns) ths = [] :: elms ns ths
   124       | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths
   125       | elms _ _ = [];
   126   in elms spans o elm (length (filter_out (equal 0) spans)) end;
   127 
   128 end;
   129 
   130 
   131 (* currying *)
   132 
   133 local
   134 
   135 fun conjs m =
   136   let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m)
   137   in (As, Logic.mk_conjunction_list As) end;
   138 
   139 val B = Free ("B", propT);
   140 
   141 fun comp_rule th rule =
   142   Thm.adjust_maxidx_thm (th COMP
   143     (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
   144 
   145 in
   146 
   147 (*
   148    A1 && ... && An ==> B
   149   -----------------------
   150   A1 ==> ... ==> An ==> B
   151 *)
   152 fun curry n th =
   153   let
   154     val k =
   155       (case try Logic.dest_implies (Thm.prop_of th) of
   156         NONE => 0
   157       | SOME (prem, _) => length (Logic.dest_conjunction_list prem));
   158     val m = if n = ~1 then k else Int.min (n, k);
   159   in
   160     if m < 2 then th
   161     else
   162       let
   163         val (As, C) = conjs m;
   164         val cAs = map cert As;
   165         val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert;
   166       in
   167         comp_rule th
   168           (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs))
   169             |> Drule.implies_intr_list (D :: cAs))
   170       end
   171   end;
   172 
   173 (*
   174   A1 ==> ... ==> An ==> B
   175   -----------------------
   176    A1 && ... && An ==> B
   177 *)
   178 fun uncurry n th =
   179   let
   180     val k = Thm.nprems_of th;
   181     val m = if n = ~1 then k else Int.min (n, k);
   182   in
   183     if m < 2 then th
   184     else
   185       let
   186         val (As, C) = conjs m ||> cert;
   187         val D = Logic.list_implies (As, B) |> cert;
   188       in
   189         comp_rule th
   190           (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C))
   191             |> Drule.implies_intr_list [D, C])
   192       end
   193   end;
   194 
   195 end;
   196 
   197 
   198 (* defined conjunctions *)
   199 
   200 fun project th 1 = (th RS conjunctionD1 handle THM _ => th)
   201   | project th k = project (th RS conjunctionD2) (k - 1);
   202 
   203 fun split_defined n eq =
   204   let
   205     val intro =
   206       (eq RS Drule.equal_elim_rule2)
   207       |> curry n
   208       |> K (n = 0) ? Thm.eq_assumption 1;
   209     val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
   210   in (intro, dests) end;
   211 
   212 end;