src/Pure/conjunction.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 67721 5348bea4accd
permissions -rw-r--r--
more robust sorted_entries;
     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_conjunctions: thm -> thm list
    23   val elim_balanced: int -> thm -> thm list
    24   val curry_balanced: int -> thm -> thm
    25   val uncurry_balanced: int -> thm -> thm
    26 end;
    27 
    28 structure Conjunction: CONJUNCTION =
    29 struct
    30 
    31 (** abstract syntax **)
    32 
    33 fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
    34 val read_prop = certify o Simple_Syntax.read_prop;
    35 
    36 val true_prop = certify Logic.true_prop;
    37 val conjunction = certify Logic.conjunction;
    38 
    39 fun mk_conjunction (A, B) = Thm.apply (Thm.apply conjunction A) B;
    40 
    41 fun mk_conjunction_balanced [] = true_prop
    42   | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
    43 
    44 fun dest_conjunction ct =
    45   (case Thm.term_of ct of
    46     (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    47   | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
    48 
    49 fun dest_conjunctions ct =
    50   (case try dest_conjunction ct of
    51     NONE => [ct]
    52   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
    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 = (("A", 0), propT);
    73 val B = read_prop "B" and vB = (("B", 0), propT);
    74 val C = read_prop "C";
    75 val ABC = read_prop "A ==> B ==> C";
    76 val A_B = read_prop "A &&& B";
    77 
    78 val conjunction_def =
    79   Thm.unvarify_axiom (Context.the_global_context ()) "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 =
    88   Drule.store_standard_thm (Binding.make ("conjunctionD1", \<^here>)) (conjunctionD #1);
    89 
    90 val conjunctionD2 =
    91   Drule.store_standard_thm (Binding.make ("conjunctionD2", \<^here>)) (conjunctionD #2);
    92 
    93 val conjunctionI =
    94   Drule.store_standard_thm (Binding.make ("conjunctionI", \<^here>))
    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 
   102 fun intr tha thb =
   103   Thm.implies_elim
   104     (Thm.implies_elim
   105       (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
   106     tha)
   107   thb;
   108 
   109 fun elim th =
   110   let
   111     val (A, B) = dest_conjunction (Thm.cprop_of th)
   112       handle TERM (msg, _) => raise THM (msg, 0, [th]);
   113     val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
   114   in
   115    (Thm.implies_elim (inst conjunctionD1) th,
   116     Thm.implies_elim (inst conjunctionD2) th)
   117   end;
   118 
   119 end;
   120 
   121 fun elim_conjunctions th =
   122   (case try elim th of
   123     NONE => [th]
   124   | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2);
   125 
   126 
   127 (* balanced conjuncts *)
   128 
   129 fun intr_balanced [] = asm_rl
   130   | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;
   131 
   132 fun elim_balanced 0 _ = []
   133   | elim_balanced n th = Balanced_Tree.dest elim n th;
   134 
   135 
   136 (* currying *)
   137 
   138 local
   139 
   140 val bootstrap_thy = Context.the_global_context ();
   141 
   142 fun conjs n =
   143   let
   144     val As =
   145       map (fn A => Thm.global_cterm_of bootstrap_thy (Free (A, propT)))
   146         (Name.invent Name.context "A" n);
   147   in (As, mk_conjunction_balanced As) end;
   148 
   149 val B = read_prop "B";
   150 
   151 fun comp_rule th rule =
   152   Thm.adjust_maxidx_thm ~1 (th COMP
   153     (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
   154 
   155 in
   156 
   157 (*
   158   A1 &&& ... &&& An ==> B
   159   -----------------------
   160   A1 ==> ... ==> An ==> B
   161 *)
   162 fun curry_balanced n th =
   163   if n < 2 then th
   164   else
   165     let
   166       val (As, C) = conjs n;
   167       val D = Drule.mk_implies (C, B);
   168     in
   169       comp_rule th
   170         (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As))
   171           |> Drule.implies_intr_list (D :: As))
   172     end;
   173 
   174 (*
   175   A1 ==> ... ==> An ==> B
   176   -----------------------
   177   A1 &&& ... &&& An ==> B
   178 *)
   179 fun uncurry_balanced n th =
   180   if n < 2 then th
   181   else
   182     let
   183       val (As, C) = conjs n;
   184       val D = Drule.list_implies (As, B);
   185     in
   186       comp_rule th
   187         (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C))
   188           |> Drule.implies_intr_list [D, C])
   189     end;
   190 
   191 end;
   192 
   193 end;