src/Pure/conjunction.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20666 82638257d372
child 21565 bd28361f4c5b
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     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", _) $ _ $ _) => Thm.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" and vA = read "PROP ?A";
    78 val B = read "PROP B" and vB = 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 =
   102   Thm.implies_elim
   103     (Thm.implies_elim
   104       (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
   105     tha)
   106   thb;
   107 
   108 fun intr_list [] = asm_rl
   109   | intr_list ths = foldr1 (uncurry intr) ths;
   110 
   111 fun elim th =
   112   let
   113     val (A, B) = dest_conjunction (Thm.cprop_of th)
   114       handle TERM (msg, _) => raise THM (msg, 0, [th]);
   115     val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
   116   in
   117    (Thm.implies_elim (inst conjunctionD1) th,
   118     Thm.implies_elim (inst conjunctionD2) th)
   119   end;
   120 
   121 (*((A && B) && C) && D && E -- flat*)
   122 fun elim_list th =
   123   let val (th1, th2) = elim th
   124   in elim_list th1 @ elim_list th2 end handle THM _ => [th];
   125 
   126 (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   127 fun elim_precise spans =
   128   let
   129     fun elm 0 _ = []
   130       | elm 1 th = [th]
   131       | elm n th =
   132           let val (th1, th2) = elim th
   133           in th1 :: elm (n - 1) th2 end;
   134     fun elms (0 :: ns) ths = [] :: elms ns ths
   135       | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths
   136       | elms _ _ = [];
   137   in elms spans o elm (length (filter_out (equal 0) spans)) end;
   138 
   139 end;
   140 
   141 
   142 (* currying *)
   143 
   144 local
   145 
   146 fun conjs m =
   147   let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m)
   148   in (As, Logic.mk_conjunction_list As) end;
   149 
   150 val B = Free ("B", propT);
   151 
   152 fun comp_rule th rule =
   153   Thm.adjust_maxidx_thm ~1 (th COMP
   154     (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
   155 
   156 in
   157 
   158 (*
   159    A1 && ... && An ==> B
   160   -----------------------
   161   A1 ==> ... ==> An ==> B
   162 *)
   163 fun curry n th =
   164   let
   165     val k =
   166       (case try Logic.dest_implies (Thm.prop_of th) of
   167         NONE => 0
   168       | SOME (prem, _) => length (Logic.dest_conjunction_list prem));
   169     val m = if n = ~1 then k else Int.min (n, k);
   170   in
   171     if m < 2 then th
   172     else
   173       let
   174         val (As, C) = conjs m;
   175         val cAs = map cert As;
   176         val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert;
   177       in
   178         comp_rule th
   179           (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs))
   180             |> Drule.implies_intr_list (D :: cAs))
   181       end
   182   end;
   183 
   184 (*
   185   A1 ==> ... ==> An ==> B
   186   -----------------------
   187    A1 && ... && An ==> B
   188 *)
   189 fun uncurry n th =
   190   let
   191     val k = Thm.nprems_of th;
   192     val m = if n = ~1 then k else Int.min (n, k);
   193   in
   194     if m < 2 then th
   195     else
   196       let
   197         val (As, C) = conjs m ||> cert;
   198         val D = Logic.list_implies (As, B) |> cert;
   199       in
   200         comp_rule th
   201           (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C))
   202             |> Drule.implies_intr_list [D, C])
   203       end
   204   end;
   205 
   206 end;
   207 
   208 
   209 (* defined conjunctions *)
   210 
   211 fun project th 1 = (th RS conjunctionD1 handle THM _ => th)
   212   | project th k = project (th RS conjunctionD2) (k - 1);
   213 
   214 fun split_defined n eq =
   215   let
   216     val intro =
   217       (eq RS Drule.equal_elim_rule2)
   218       |> curry n
   219       |> K (n = 0) ? Thm.eq_assumption 1;
   220     val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
   221   in (intro, dests) end;
   222 
   223 end;