# HG changeset patch
# User wenzelm
# Date 1182287727 -7200
# Node ID c195f6f1376993f2d7a97672f6c91ecb709d9255
# Parent  42c1a89b45c1283ce6a4d1c4a4da833adbfd8635
balanced conjunctions;

diff -r 42c1a89b45c1 -r c195f6f13769 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -350,7 +350,7 @@
 
     val rule_prems = cprems @ flat cpremss;
     val rule = implies_intr_list rule_prems
-      (foldr1 (uncurry Conjunction.intr) (map mk_eqn (rec_rewrites' ~~ asmss)));
+      (Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
 
     val goals = map (fn ((cargs, _, _), (_, eqn)) =>
       (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns);
diff -r 42c1a89b45c1 -r c195f6f13769 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -214,7 +214,7 @@
   (* A registration is indexed by parameter instantiation.  Its components are:
      - parameters and prefix
        (if the Boolean flag is set, only accesses containing the prefix are generated,
-        otherwise the prefix may be omitted when accessing theorems etc.) 
+        otherwise the prefix may be omitted when accessing theorems etc.)
      - theorems (actually witnesses) instantiating locale assumptions
      - theorems (equations, actually witnesses) interpreting derived concepts
        and indexed by lhs
@@ -656,10 +656,10 @@
 
     fun unify T U envir = Sign.typ_unify thy (U, T) envir
       handle Type.TUNIFY =>
-        let 
+        let
           val T' = Envir.norm_type (fst envir) T;
           val U' = Envir.norm_type (fst envir) U;
-          val prt = Sign.string_of_typ thy; 
+          val prt = Sign.string_of_typ thy;
         in
           raise TYPE ("unify_parms: failed to unify types " ^
             prt U' ^ " and " ^ prt T', [U', T'], [])
@@ -1660,7 +1660,7 @@
       (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
   add_thmss loc Thm.internalK [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
 
-in  
+in
 
 val add_type_syntax = add_decls (apfst o cons);
 val add_term_syntax = add_decls (apsnd o cons);
@@ -1687,7 +1687,7 @@
 
 fun atomize_spec thy ts =
   let
-    val t = Logic.mk_conjunction_list ts;
+    val t = Logic.mk_conjunction_balanced ts;
     val body = ObjectLogic.atomize_term thy t;
     val bodyT = Term.fastype_of body;
   in
@@ -1737,12 +1737,13 @@
     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
       MetaSimplifier.rewrite_goals_tac [pred_def] THEN
       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
-      Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
+      Tactic.compose_tac (false,
+        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq,
         MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
-      |> Conjunction.elim_precise [length ts] |> hd;
+      |> Conjunction.elim_balanced (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness defs_ctxt t
        (MetaSimplifier.rewrite_goals_tac defs THEN
@@ -2353,7 +2354,7 @@
       #> after_qed;
   in
     thy
-    |> ProofContext.init 
+    |> ProofContext.init
     |> Proof.theorem_i NONE after_qed' (prep_propp propss)
     |> Element.refine_witness
     |> Seq.hd
diff -r 42c1a89b45c1 -r c195f6f13769 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -468,11 +468,22 @@
     val _ = null extra_hyps orelse
       error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
 
-    val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
-      handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
-    val _ = Unify.matches_list thy (flat propss) (map Thm.prop_of (flat results)) orelse
+    fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
+
+    val th = Goal.conclude goal handle THM _ => lost_structure ();
+    val goal_propss = filter_out null propss;
+    val results =
+      Conjunction.elim_balanced (length goal_propss) th
+      |> map2 Conjunction.elim_balanced (map length goal_propss)
+      handle THM _ => lost_structure ();
+    val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
       error ("Proved a different theorem:\n" ^ string_of_thm th);
-  in results end;
+
+    fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
+      | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
+      | recover_result [] [] = []
+      | recover_result _ _ = lost_structure ();
+  in recover_result propss results end;
 
 
 
@@ -758,6 +769,7 @@
 fun generic_goal prepp kind before_qed after_qed raw_propp state =
   let
     val thy = theory_of state;
+    val cert = Thm.cterm_of thy;
     val chaining = can assert_chain state;
 
     val ((propss, after_ctxt), goal_state) =
@@ -773,7 +785,9 @@
     val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
 
     val propss' = map (Logic.mk_term o Var) vars :: propss;
-    val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss'));
+    val goal_propss = filter_out null propss';
+    val goal = Goal.init (cert
+      (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)));
     val after_qed' = after_qed |>> (fn after_local =>
       fn results => map_context after_ctxt #> after_local results);
   in
@@ -787,7 +801,7 @@
     |> open_block
     |> put_goal NONE
     |> enter_backward
-    |> not (null vars) ? refine_terms (length propss')
+    |> not (null vars) ? refine_terms (length goal_propss)
     |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
   end;
 
diff -r 42c1a89b45c1 -r c195f6f13769 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -195,8 +195,8 @@
   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   else
     Conv.fconv_rule
-      (Conv.concl_conv ~1 (Conjunction.conv ~1
-        (K (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
+      (Conv.concl_conv ~1 (Conjunction.convs
+        (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs))))) th;
 
 in
 
@@ -338,7 +338,7 @@
         else
           SOME (ns,
             rls
-            |> foldr1 (uncurry Conjunction.intr)
+            |> Conjunction.intr_balanced
             |> Drule.implies_intr_list prems
             |> singleton (Variable.export ctxt' ctxt)
             |> save th
diff -r 42c1a89b45c1 -r c195f6f13769 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -238,9 +238,9 @@
     fun burrow_thms f [] = []
       | burrow_thms f thms =
           thms
-          |> Conjunction.intr_list
+          |> Conjunction.intr_balanced
           |> f
-          |> Conjunction.elim_list;
+          |> Conjunction.elim_balanced (length thms)
   in
     thms
     |> burrow_thms (canonical_tvars purify_tvar)
diff -r 42c1a89b45c1 -r c195f6f13769 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/goal.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -8,8 +8,8 @@
 signature BASIC_GOAL =
 sig
   val SELECT_GOAL: tactic -> int -> tactic
+  val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
-  val CONJUNCTS: tactic -> int -> tactic
 end;
 
 signature GOAL =
@@ -29,8 +29,9 @@
   val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val extract: int -> int -> thm -> thm Seq.seq
   val retrofit: int -> int -> thm -> thm -> thm Seq.seq
+  val conjunction_tac: int -> tactic
   val precise_conjunction_tac: int -> int -> tactic
-  val conjunction_tac: int -> tactic
+  val recover_conjunction_tac: tactic
   val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
   val rewrite_goal_tac: thm list -> int -> tactic
   val norm_hhf_tac: int -> tactic
@@ -132,12 +133,12 @@
       |> fold Variable.declare_internal (asms @ props)
       |> Assumption.add_assumes casms;
 
-    val goal = init (Conjunction.mk_conjunction_list cprops);
+    val goal = init (Conjunction.mk_conjunction_balanced cprops);
     val res =
       (case SINGLE (tac {prems = prems, context = ctxt'}) goal of
         NONE => err "Tactic failed."
       | SOME res => res);
-    val [results] = Conjunction.elim_precise [length props] (finish res)
+    val results = Conjunction.elim_balanced (length props) (finish res)
       handle THM (msg, _, _) => err msg;
     val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results)
       orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
@@ -165,12 +166,13 @@
 fun extract i n st =
   (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    else if n = 1 then Seq.single (Thm.cprem_of st i)
-   else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
+   else
+     Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
   |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
 
 fun retrofit i n st' st =
   (if n = 1 then st
-   else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
+   else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
   |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
 
 fun SELECT_GOAL tac i st =
@@ -180,48 +182,31 @@
 
 (* multiple goals *)
 
-local
-
-fun conj_intrs n =
-  let
-    val cert = Thm.cterm_of ProtoPure.thy;
-    val names = Name.invents Name.context "A" n;
-    val As = map (fn name => cert (Free (name, propT))) names;
-  in
-    Thm.generalize ([], names) 0
-      (Drule.implies_intr_list As (Conjunction.intr_list (map Thm.assume As)))
-  end;
+fun precise_conjunction_tac 0 i = eq_assume_tac i
+  | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
+  | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n));
 
-fun count_conjs A =
-  (case try Logic.dest_conjunction A of
-    NONE => 1
-  | SOME (_, B) => count_conjs B + 1);
-
-in
+val adhoc_conjunction_tac = REPEAT_ALL_NEW
+  (SUBGOAL (fn (goal, i) =>
+    if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
+    else no_tac));
 
-val precise_conjunction_tac =
-  let
-    fun tac 0 i = eq_assume_tac i
-      | tac 1 i = SUBGOAL (K all_tac) i
-      | tac 2 i = rtac Conjunction.conjunctionI i
-      | tac n i = rtac (conj_intrs n) i;
-  in TRY oo tac end;
+val conjunction_tac = SUBGOAL (fn (goal, i) =>
+  precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
+  TRY (adhoc_conjunction_tac i));
 
-val conjunction_tac = TRY o REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) =>
-  let val n = count_conjs goal
-  in if n < 2 then no_tac else precise_conjunction_tac n i end));
+val recover_conjunction_tac = PRIMITIVE (fn th =>
+  Conjunction.uncurry_balanced (Thm.nprems_of th) th);
 
 fun PRECISE_CONJUNCTS n tac =
   SELECT_GOAL (precise_conjunction_tac n 1
     THEN tac
-    THEN PRIMITIVE (Conjunction.uncurry ~1));
+    THEN recover_conjunction_tac);
 
 fun CONJUNCTS tac =
   SELECT_GOAL (conjunction_tac 1
     THEN tac
-    THEN PRIMITIVE (Conjunction.uncurry ~1));
-
-end;
+    THEN recover_conjunction_tac);
 
 
 (* rewriting *)
diff -r 42c1a89b45c1 -r c195f6f13769 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/logic.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -19,12 +19,14 @@
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
   val nth_prem: int * term -> term
+  val true_prop: term
   val conjunction: term
   val mk_conjunction: term * term -> term
   val mk_conjunction_list: term list -> term
-  val mk_conjunction_list2: term list list -> term
+  val mk_conjunction_balanced: term list -> term
   val dest_conjunction: term -> term * term
   val dest_conjunction_list: term -> term list
+  val dest_conjunction_balanced: int -> term -> term list
   val dest_conjunctions: term -> term list
   val strip_horn: term -> term list * term
   val mk_type: typ -> term
@@ -145,20 +147,24 @@
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
 
 
+
 (** conjunction **)
 
+val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
 val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
 
+
 (*A && B*)
 fun mk_conjunction (A, B) = conjunction $ A $ B;
 
 (*A && B && C -- improper*)
-fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
+fun mk_conjunction_list [] = true_prop
   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
 
-(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
-fun mk_conjunction_list2 tss =
-  mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
+(*(A && B) && (C && D) -- balanced*)
+fun mk_conjunction_balanced [] = true_prop
+  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
+
 
 (*A && B*)
 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
@@ -170,6 +176,10 @@
     NONE => [t]
   | SOME (A, B) => A :: dest_conjunction_list B);
 
+(*(A && B) && (C && D) -- balanced*)
+fun dest_conjunction_balanced 0 _ = []
+  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
+
 (*((A && B) && C) && D && E -- flat*)
 fun dest_conjunctions t =
   (case try dest_conjunction t of