src/Pure/conjunction.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 35985 0bbf0d2348f9
child 43329 84472e198515
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      Pure/conjunction.ML
     2     Author:     Makarius
     3 
     4 Meta-level conjunction.
     5 *)
     6 
     7 signature CONJUNCTION =
     8 sig
     9   val conjunction: cterm
    10   val mk_conjunction: cterm * cterm -> cterm
    11   val mk_conjunction_balanced: cterm list -> cterm
    12   val dest_conjunction: cterm -> cterm * cterm
    13   val dest_conjunctions: cterm -> cterm list
    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 fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
    33 val read_prop = certify o Simple_Syntax.read_prop;
    34 
    35 val true_prop = certify Logic.true_prop;
    36 val conjunction = certify 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 = Balanced_Tree.make mk_conjunction ts;
    42 
    43 fun dest_conjunction ct =
    44   (case Thm.term_of ct of
    45     (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    46   | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
    47 
    48 fun dest_conjunctions ct =
    49   (case try dest_conjunction ct of
    50     NONE => [ct]
    51   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
    52 
    53 
    54 
    55 (** derived rules **)
    56 
    57 (* conversion *)
    58 
    59 val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction);
    60 
    61 fun convs cv ct =
    62   (case try dest_conjunction ct of
    63     NONE => cv ct
    64   | SOME (A, B) => cong (convs cv A) (convs cv B));
    65 
    66 
    67 (* intro/elim *)
    68 
    69 local
    70 
    71 val A = read_prop "A" and vA = read_prop "?A";
    72 val B = read_prop "B" and vB = read_prop "?B";
    73 val C = read_prop "C";
    74 val ABC = read_prop "A ==> B ==> C";
    75 val A_B = read_prop "A &&& B";
    76 
    77 val conjunction_def =
    78   Thm.unvarify_global
    79     (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
    80 
    81 fun conjunctionD which =
    82   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
    83   Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
    84 
    85 in
    86 
    87 val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
    88 val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
    89 
    90 val conjunctionI =
    91   Drule.store_standard_thm (Binding.name "conjunctionI")
    92     (Drule.implies_intr_list [A, B]
    93       (Thm.equal_elim
    94         (Thm.symmetric conjunction_def)
    95         (Thm.forall_intr C (Thm.implies_intr ABC
    96           (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    97 
    98 
    99 fun intr tha thb =
   100   Thm.implies_elim
   101     (Thm.implies_elim
   102       (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
   103     tha)
   104   thb;
   105 
   106 fun elim th =
   107   let
   108     val (A, B) = dest_conjunction (Thm.cprop_of th)
   109       handle TERM (msg, _) => raise THM (msg, 0, [th]);
   110     val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
   111   in
   112    (Thm.implies_elim (inst conjunctionD1) th,
   113     Thm.implies_elim (inst conjunctionD2) th)
   114   end;
   115 
   116 end;
   117 
   118 
   119 (* balanced conjuncts *)
   120 
   121 fun intr_balanced [] = asm_rl
   122   | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
   123 
   124 fun elim_balanced 0 _ = []
   125   | elim_balanced n th = Balanced_Tree.dest elim n th;
   126 
   127 
   128 (* currying *)
   129 
   130 local
   131 
   132 fun conjs thy n =
   133   let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
   134   in (As, mk_conjunction_balanced As) end;
   135 
   136 val B = read_prop "B";
   137 
   138 fun comp_rule th rule =
   139   Thm.adjust_maxidx_thm ~1 (th COMP
   140     (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
   141 
   142 in
   143 
   144 (*
   145   A1 &&& ... &&& An ==> B
   146   -----------------------
   147   A1 ==> ... ==> An ==> B
   148 *)
   149 fun curry_balanced n th =
   150   if n < 2 then th
   151   else
   152     let
   153       val thy = Thm.theory_of_thm th;
   154       val (As, C) = conjs thy n;
   155       val D = Drule.mk_implies (C, B);
   156     in
   157       comp_rule th
   158         (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
   159           |> Drule.implies_intr_list (D :: As))
   160     end;
   161 
   162 (*
   163   A1 ==> ... ==> An ==> B
   164   -----------------------
   165   A1 &&& ... &&& An ==> B
   166 *)
   167 fun uncurry_balanced n th =
   168   if n < 2 then th
   169   else
   170     let
   171       val thy = Thm.theory_of_thm th;
   172       val (As, C) = conjs thy n;
   173       val D = Drule.list_implies (As, B);
   174     in
   175       comp_rule th
   176         (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
   177           |> Drule.implies_intr_list [D, C])
   178     end;
   179 
   180 end;
   181 
   182 end;