wenzelm@19416: (* Title: Pure/conjunction.ML wenzelm@19416: ID: $Id$ wenzelm@19416: Author: Makarius wenzelm@19416: wenzelm@19416: Meta-level conjunction. wenzelm@19416: *) wenzelm@19416: wenzelm@19416: signature CONJUNCTION = wenzelm@19416: sig wenzelm@19416: val conjunction: cterm wenzelm@19416: val mk_conjunction: cterm * cterm -> cterm wenzelm@23422: val mk_conjunction_balanced: cterm list -> cterm wenzelm@19416: val dest_conjunction: cterm -> cterm * cterm wenzelm@19416: val cong: thm -> thm -> thm wenzelm@23422: val convs: (cterm -> thm) -> cterm -> thm wenzelm@19416: val conjunctionD1: thm wenzelm@19416: val conjunctionD2: thm wenzelm@19416: val conjunctionI: thm wenzelm@19416: val intr: thm -> thm -> thm wenzelm@23422: val intr_balanced: thm list -> thm wenzelm@19416: val elim: thm -> thm * thm wenzelm@23422: val elim_balanced: int -> thm -> thm list wenzelm@23422: val curry_balanced: int -> thm -> thm wenzelm@23422: val uncurry_balanced: int -> thm -> thm wenzelm@19416: end; wenzelm@19416: wenzelm@19416: structure Conjunction: CONJUNCTION = wenzelm@19416: struct wenzelm@19416: wenzelm@19416: (** abstract syntax **) wenzelm@19416: wenzelm@19416: val cert = Thm.cterm_of ProtoPure.thy; wenzelm@24241: val read_prop = cert o SimpleSyntax.read_prop; wenzelm@19416: wenzelm@23422: val true_prop = cert Logic.true_prop; wenzelm@19416: val conjunction = cert Logic.conjunction; wenzelm@23422: wenzelm@19416: fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; wenzelm@19416: wenzelm@23422: fun mk_conjunction_balanced [] = true_prop wenzelm@23422: | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; wenzelm@23422: wenzelm@19416: fun dest_conjunction ct = wenzelm@19416: (case Thm.term_of ct of wenzelm@20666: (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct wenzelm@23422: | _ => raise TERM ("dest_conjunction", [Thm.term_of ct])); wenzelm@19416: wenzelm@19416: wenzelm@19416: wenzelm@19416: (** derived rules **) wenzelm@19416: wenzelm@19416: (* conversion *) wenzelm@19416: wenzelm@19416: val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction); wenzelm@19416: wenzelm@23422: fun convs cv ct = wenzelm@23422: (case try dest_conjunction ct of wenzelm@23422: NONE => cv ct wenzelm@23422: | SOME (A, B) => cong (convs cv A) (convs cv B)); wenzelm@19416: wenzelm@19416: wenzelm@19416: (* intro/elim *) wenzelm@19416: wenzelm@19416: local wenzelm@19416: wenzelm@24241: val A = read_prop "A" and vA = read_prop "?A"; wenzelm@24241: val B = read_prop "B" and vB = read_prop "?B"; wenzelm@24241: val C = read_prop "C"; wenzelm@24241: val ABC = read_prop "A ==> B ==> C"; wenzelm@24241: val A_B = read_prop "A && B"; wenzelm@19416: wenzelm@20238: val conjunction_def = Drule.unvarify ProtoPure.conjunction_def; wenzelm@19416: wenzelm@19416: fun conjunctionD which = wenzelm@19416: Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP wenzelm@19416: Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B)); wenzelm@19416: wenzelm@19416: in wenzelm@19416: wenzelm@19416: val conjunctionD1 = Drule.store_standard_thm "conjunctionD1" (conjunctionD #1); wenzelm@19416: val conjunctionD2 = Drule.store_standard_thm "conjunctionD2" (conjunctionD #2); wenzelm@19416: wenzelm@19416: val conjunctionI = Drule.store_standard_thm "conjunctionI" wenzelm@19416: (Drule.implies_intr_list [A, B] wenzelm@19416: (Thm.equal_elim wenzelm@19416: (Thm.symmetric conjunction_def) wenzelm@19416: (Thm.forall_intr C (Thm.implies_intr ABC wenzelm@19416: (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))); wenzelm@19416: wenzelm@23422: wenzelm@20508: fun intr tha thb = wenzelm@20508: Thm.implies_elim wenzelm@20508: (Thm.implies_elim wenzelm@20508: (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI) wenzelm@20508: tha) wenzelm@20508: thb; wenzelm@19416: wenzelm@19416: fun elim th = wenzelm@20508: let wenzelm@20508: val (A, B) = dest_conjunction (Thm.cprop_of th) wenzelm@20508: handle TERM (msg, _) => raise THM (msg, 0, [th]); wenzelm@20508: val inst = Thm.instantiate ([], [(vA, A), (vB, B)]); wenzelm@20508: in wenzelm@20508: (Thm.implies_elim (inst conjunctionD1) th, wenzelm@20508: Thm.implies_elim (inst conjunctionD2) th) wenzelm@20508: end; wenzelm@19416: wenzelm@23422: end; wenzelm@23422: wenzelm@23422: wenzelm@23535: (* balanced conjuncts *) wenzelm@23422: wenzelm@23422: fun intr_balanced [] = asm_rl wenzelm@23422: | intr_balanced ths = BalancedTree.make (uncurry intr) ths; wenzelm@23422: wenzelm@23422: fun elim_balanced 0 _ = [] wenzelm@23422: | elim_balanced n th = BalancedTree.dest elim n th; wenzelm@19416: wenzelm@19416: wenzelm@19416: (* currying *) wenzelm@19416: wenzelm@19416: local wenzelm@19416: wenzelm@23422: fun conjs n = wenzelm@23422: let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n) wenzelm@23422: in (As, mk_conjunction_balanced As) end; wenzelm@19416: wenzelm@24241: val B = read_prop "B"; wenzelm@19416: wenzelm@19416: fun comp_rule th rule = wenzelm@20260: Thm.adjust_maxidx_thm ~1 (th COMP wenzelm@19416: (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1))); wenzelm@19416: wenzelm@19416: in wenzelm@19416: wenzelm@19416: (* wenzelm@19416: A1 && ... && An ==> B wenzelm@19416: ----------------------- wenzelm@19416: A1 ==> ... ==> An ==> B wenzelm@19416: *) wenzelm@23422: fun curry_balanced n th = wenzelm@23422: if n < 2 then th wenzelm@23422: else wenzelm@23422: let wenzelm@23422: val (As, C) = conjs n; wenzelm@23422: val D = Drule.mk_implies (C, B); wenzelm@23422: in wenzelm@23422: comp_rule th wenzelm@23422: (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As)) wenzelm@23422: |> Drule.implies_intr_list (D :: As)) wenzelm@23422: end; wenzelm@19416: wenzelm@19416: (* wenzelm@19416: A1 ==> ... ==> An ==> B wenzelm@19416: ----------------------- wenzelm@23422: A1 && ... && An ==> B wenzelm@19416: *) wenzelm@23422: fun uncurry_balanced n th = wenzelm@23422: if n < 2 then th wenzelm@23422: else wenzelm@23422: let wenzelm@23422: val (As, C) = conjs n; wenzelm@23422: val D = Drule.list_implies (As, B); wenzelm@23422: in wenzelm@23422: comp_rule th wenzelm@23422: (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C)) wenzelm@23422: |> Drule.implies_intr_list [D, C]) wenzelm@23422: end; wenzelm@19416: wenzelm@19416: end; wenzelm@19416: wenzelm@19416: end;