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