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@19416: val dest_conjunction: cterm -> cterm * cterm wenzelm@19416: val cong: thm -> thm -> thm wenzelm@19416: val conv: int -> (int -> 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@19416: val intr_list: thm list -> thm wenzelm@19416: val elim: thm -> thm * thm wenzelm@19416: val elim_list: thm -> thm list wenzelm@19416: val elim_precise: int list -> thm -> thm list list wenzelm@19416: val curry: int -> thm -> thm wenzelm@19416: val uncurry: int -> thm -> thm wenzelm@19416: val split_defined: int -> thm -> thm * thm list wenzelm@19416: end; wenzelm@19416: wenzelm@19416: structure Conjunction: CONJUNCTION = wenzelm@19416: struct wenzelm@19416: wenzelm@19416: wenzelm@19416: (** abstract syntax **) wenzelm@19416: wenzelm@19416: fun read s = Thm.read_cterm ProtoPure.thy (s, propT); wenzelm@19416: val cert = Thm.cterm_of ProtoPure.thy; wenzelm@19416: wenzelm@19416: val conjunction = cert Logic.conjunction; wenzelm@19416: fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; wenzelm@19416: wenzelm@19416: fun dest_conjunction ct = wenzelm@19416: (case Thm.term_of ct of wenzelm@19416: (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct wenzelm@19416: | _ => raise TERM ("dest_conjunction", [term_of ct])); wenzelm@19416: wenzelm@19416: wenzelm@19416: wenzelm@19416: (** derived rules **) wenzelm@19416: wenzelm@19416: (* conversion *) wenzelm@19416: wenzelm@19416: (*rewrite the A's in A1 && ... && An*) wenzelm@19416: wenzelm@19416: val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction); wenzelm@19416: wenzelm@19416: fun conv 0 _ = reflexive wenzelm@19416: | conv n cv = wenzelm@19416: let wenzelm@19416: fun cnv i ct = wenzelm@19416: if i = n then cv i ct wenzelm@19416: else wenzelm@19416: (case try dest_conjunction ct of wenzelm@19416: NONE => cv i ct wenzelm@19416: | SOME (A, B) => cong (cv i A) (cnv (i + 1) B)); wenzelm@19416: in cnv 1 end; wenzelm@19416: wenzelm@19416: wenzelm@19416: (* intro/elim *) wenzelm@19416: wenzelm@19416: local wenzelm@19416: wenzelm@19416: val A = read "PROP A"; wenzelm@19416: val B = read "PROP B"; wenzelm@19416: val C = read "PROP C"; wenzelm@19416: val ABC = read "PROP A ==> PROP B ==> PROP C"; wenzelm@19416: val A_B = read "PROP ProtoPure.conjunction(A, B)" wenzelm@19416: wenzelm@19416: val conjunction_def = #1 (freeze_thaw 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@19416: fun intr tha thb = thb COMP (tha COMP Drule.incr_indexes2 tha thb conjunctionI); wenzelm@19416: wenzelm@19416: fun intr_list [] = asm_rl wenzelm@19416: | intr_list ths = foldr1 (uncurry intr) ths; wenzelm@19416: wenzelm@19416: fun elim th = wenzelm@19416: (th COMP Drule.incr_indexes th conjunctionD1, wenzelm@19416: th COMP Drule.incr_indexes th conjunctionD2); wenzelm@19416: wenzelm@19416: (*((A && B) && C) && D && E -- flat*) wenzelm@19416: fun elim_list th = wenzelm@19416: let val (th1, th2) = elim th wenzelm@19416: in elim_list th1 @ elim_list th2 end handle THM _ => [th]; wenzelm@19416: wenzelm@19416: (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*) wenzelm@19416: fun elim_precise spans = wenzelm@19416: let wenzelm@19416: fun elm 0 _ = [] wenzelm@19416: | elm 1 th = [th] wenzelm@19416: | elm n th = wenzelm@19416: let val (th1, th2) = elim th wenzelm@19416: in th1 :: elm (n - 1) th2 end; wenzelm@19416: fun elms (0 :: ns) ths = [] :: elms ns ths wenzelm@19416: | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths wenzelm@19416: | elms _ _ = []; wenzelm@19416: in elms spans o elm (length (filter_out (equal 0) spans)) end; wenzelm@19416: wenzelm@19416: end; wenzelm@19416: wenzelm@19416: wenzelm@19416: (* currying *) wenzelm@19416: wenzelm@19416: local wenzelm@19416: wenzelm@19416: fun conjs m = wenzelm@19416: let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m) wenzelm@19416: in (As, Logic.mk_conjunction_list As) end; wenzelm@19416: wenzelm@19416: val B = Free ("B", propT); wenzelm@19416: wenzelm@19416: fun comp_rule th rule = wenzelm@19416: Thm.adjust_maxidx_thm (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@19416: fun curry n th = wenzelm@19416: let wenzelm@19416: val k = wenzelm@19416: (case try Logic.dest_implies (Thm.prop_of th) of wenzelm@19416: NONE => 0 wenzelm@19416: | SOME (prem, _) => length (Logic.dest_conjunction_list prem)); wenzelm@19416: val m = if n = ~1 then k else Int.min (n, k); wenzelm@19416: in wenzelm@19416: if m < 2 then th wenzelm@19416: else wenzelm@19416: let wenzelm@19416: val (As, C) = conjs m; wenzelm@19416: val cAs = map cert As; wenzelm@19416: val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert; wenzelm@19416: in wenzelm@19416: comp_rule th wenzelm@19416: (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs)) wenzelm@19416: |> Drule.implies_intr_list (D :: cAs)) wenzelm@19416: end wenzelm@19416: end; wenzelm@19416: wenzelm@19416: (* wenzelm@19416: A1 ==> ... ==> An ==> B wenzelm@19416: ----------------------- wenzelm@19416: A1 && ... && An ==> B wenzelm@19416: *) wenzelm@19416: fun uncurry n th = wenzelm@19416: let wenzelm@19416: val k = Thm.nprems_of th; wenzelm@19416: val m = if n = ~1 then k else Int.min (n, k); wenzelm@19416: in wenzelm@19416: if m < 2 then th wenzelm@19416: else wenzelm@19416: let wenzelm@19416: val (As, C) = conjs m ||> cert; wenzelm@19416: val D = Logic.list_implies (As, B) |> cert; wenzelm@19416: in wenzelm@19416: comp_rule th wenzelm@19416: (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C)) wenzelm@19416: |> Drule.implies_intr_list [D, C]) wenzelm@19416: end wenzelm@19416: end; wenzelm@19416: wenzelm@19416: end; wenzelm@19416: wenzelm@19416: wenzelm@19416: (* defined conjunctions *) wenzelm@19416: wenzelm@19416: fun project th 1 = (th RS conjunctionD1 handle THM _ => th) wenzelm@19416: | project th k = project (th RS conjunctionD2) (k - 1); wenzelm@19416: wenzelm@19416: fun split_defined n eq = wenzelm@19416: let wenzelm@19416: val intro = wenzelm@19416: (eq RS Drule.equal_elim_rule2) wenzelm@19416: |> curry n wenzelm@19416: |> K (n = 0) ? Thm.eq_assumption 1; wenzelm@19416: val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n); wenzelm@19416: in (intro, dests) end; wenzelm@19416: wenzelm@19416: end;