# HG changeset patch # User wenzelm # Date 1182287749 -7200 # Node ID 4a368c087f58ff671c2fe30499dab7869ece6710 # Parent c9007fc4a646d33ffbacc13ab7a0c423827bb3e1 balanced conjunctions; tuned interfaces; tuned; diff -r c9007fc4a646 -r 4a368c087f58 src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Tue Jun 19 23:15:47 2007 +0200 +++ b/src/Pure/conjunction.ML Tue Jun 19 23:15:49 2007 +0200 @@ -10,43 +10,46 @@ val conjunction: cterm val mk_conjunction: cterm * cterm -> cterm val mk_conjunction_list: cterm list -> cterm + val mk_conjunction_balanced: cterm list -> cterm val dest_conjunction: cterm -> cterm * cterm val cong: thm -> thm -> thm - val conv: int -> (int -> cterm -> thm) -> cterm -> thm + val convs: (cterm -> thm) -> cterm -> thm val conjunctionD1: thm val conjunctionD2: thm val conjunctionI: thm val intr: thm -> thm -> thm val intr_list: thm list -> thm + val intr_balanced: thm list -> thm val elim: thm -> thm * thm val elim_list: thm -> thm list - val elim_precise: int list -> thm -> thm list list - val curry: int -> thm -> thm - val uncurry: int -> thm -> thm - val split_defined: int -> thm -> thm * thm list + val elim_balanced: int -> thm -> thm list + val curry_balanced: int -> thm -> thm + val uncurry_balanced: int -> thm -> thm end; structure Conjunction: CONJUNCTION = struct - (** abstract syntax **) fun read s = Thm.read_cterm ProtoPure.thy (s, propT); val cert = Thm.cterm_of ProtoPure.thy; +val true_prop = cert Logic.true_prop; val conjunction = cert Logic.conjunction; + fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; -val true_prop = read "!!dummy. PROP dummy ==> PROP dummy"; - fun mk_conjunction_list [] = true_prop | mk_conjunction_list ts = foldr1 mk_conjunction ts; +fun mk_conjunction_balanced [] = true_prop + | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; + fun dest_conjunction ct = (case Thm.term_of ct of (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct - | _ => raise TERM ("dest_conjunction", [term_of ct])); + | _ => raise TERM ("dest_conjunction", [Thm.term_of ct])); @@ -54,20 +57,12 @@ (* conversion *) -(*rewrite the A's in A1 && ... && An*) - val cong = Thm.combination o Thm.combination (Thm.reflexive conjunction); -fun conv 0 _ = reflexive - | conv n cv = - let - fun cnv i ct = - if i = n then cv i ct - else - (case try dest_conjunction ct of - NONE => cv i ct - | SOME (A, B) => cong (cv i A) (cnv (i + 1) B)); - in cnv 1 end; +fun convs cv ct = + (case try dest_conjunction ct of + NONE => cv ct + | SOME (A, B) => cong (convs cv A) (convs cv B)); (* intro/elim *) @@ -98,6 +93,7 @@ (Thm.forall_intr C (Thm.implies_intr ABC (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))); + fun intr tha thb = Thm.implies_elim (Thm.implies_elim @@ -105,9 +101,6 @@ tha) thb; -fun intr_list [] = asm_rl - | intr_list ths = foldr1 (uncurry intr) ths; - fun elim th = let val (A, B) = dest_conjunction (Thm.cprop_of th) @@ -118,36 +111,34 @@ Thm.implies_elim (inst conjunctionD2) th) end; -(*((A && B) && C) && D && E -- flat*) -fun elim_list th = +end; + + +(* multiple conjuncts *) + +fun intr_list [] = asm_rl + | intr_list ths = foldr1 (uncurry intr) ths; + +fun intr_balanced [] = asm_rl + | intr_balanced ths = BalancedTree.make (uncurry intr) ths; + +fun elim_list th = (* FIXME improper!? rename to "elims" *) let val (th1, th2) = elim th in elim_list th1 @ elim_list th2 end handle THM _ => [th]; -(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*) -fun elim_precise spans = - let - fun elm 0 _ = [] - | elm 1 th = [th] - | elm n th = - let val (th1, th2) = elim th - in th1 :: elm (n - 1) th2 end; - fun elms (0 :: ns) ths = [] :: elms ns ths - | elms (n :: ns) (th :: ths) = elm n th :: elms ns ths - | elms _ _ = []; - in elms spans o elm (length (filter_out (equal 0) spans)) end; - -end; +fun elim_balanced 0 _ = [] + | elim_balanced n th = BalancedTree.dest elim n th; (* currying *) local -fun conjs m = - let val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m) - in (As, Logic.mk_conjunction_list As) end; +fun conjs n = + let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n) + in (As, mk_conjunction_balanced As) end; -val B = Free ("B", propT); +val B = cert (Free ("B", propT)); fun comp_rule th rule = Thm.adjust_maxidx_thm ~1 (th COMP @@ -160,64 +151,35 @@ ----------------------- A1 ==> ... ==> An ==> B *) -fun curry n th = - let - val k = - (case try Logic.dest_implies (Thm.prop_of th) of - NONE => 0 - | SOME (prem, _) => length (Logic.dest_conjunction_list prem)); - val m = if n = ~1 then k else Int.min (n, k); - in - if m < 2 then th - else - let - val (As, C) = conjs m; - val cAs = map cert As; - val D = Logic.mk_implies (Logic.mk_conjunction_list As, B) |> cert; - in - comp_rule th - (Thm.implies_elim (Thm.assume D) (intr_list (map Thm.assume cAs)) - |> Drule.implies_intr_list (D :: cAs)) - end - end; +fun curry_balanced n th = + if n < 2 then th + else + let + val (As, C) = conjs n; + val D = Drule.mk_implies (C, B); + in + comp_rule th + (Thm.implies_elim (Thm.assume D) (intr_balanced (map Thm.assume As)) + |> Drule.implies_intr_list (D :: As)) + end; (* A1 ==> ... ==> An ==> B ----------------------- - A1 && ... && An ==> B + A1 && ... && An ==> B *) -fun uncurry n th = - let - val k = Thm.nprems_of th; - val m = if n = ~1 then k else Int.min (n, k); - in - if m < 2 then th - else - let - val (As, C) = conjs m ||> cert; - val D = Logic.list_implies (As, B) |> cert; - in - comp_rule th - (Drule.implies_elim_list (Thm.assume D) (elim_list (Thm.assume C)) - |> Drule.implies_intr_list [D, C]) - end - end; +fun uncurry_balanced n th = + if n < 2 then th + else + let + val (As, C) = conjs n; + val D = Drule.list_implies (As, B); + in + comp_rule th + (Drule.implies_elim_list (Thm.assume D) (elim_balanced n (Thm.assume C)) + |> Drule.implies_intr_list [D, C]) + end; end; - -(* defined conjunctions *) - -fun project th 1 = (th RS conjunctionD1 handle THM _ => th) - | project th k = project (th RS conjunctionD2) (k - 1); - -fun split_defined n eq = - let - val intro = - (eq RS Drule.equal_elim_rule2) - |> curry n - |> n = 0 ? Thm.eq_assumption 1; - val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n); - in (intro, dests) end; - end;