# HG changeset patch
# User wenzelm
# Date 1369844711 -7200
# Node ID 5bb6ae8acb87f67a89f7e606b9994348b4e42328
# Parent  0fa3b456a2679374457b212cff23471baa8267f8
tuned signature -- more explicit flags for low-level Thm.bicompose;

diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Wed May 29 18:25:11 2013 +0200
@@ -351,7 +351,8 @@
       map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
 
     fun elim_implies_eta A AB =
-      Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
+      Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
+      |> Seq.list_of |> the_single
 
     val uniqueness = G_cases
       |> Thm.forall_elim (cterm_of thy lhs)
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 18:25:11 2013 +0200
@@ -385,7 +385,8 @@
     val nbranches = length branches
     val npres = length pres
   in
-    Thm.compose_no_flatten false (res, length newgoals) i
+    Thm.bicompose {flatten = false, match = false, incremented = false}
+      (false, res, length newgoals) i
     THEN term_tac (i + nbranches + npres)
     THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
     THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 29 18:25:11 2013 +0200
@@ -185,14 +185,15 @@
   let
     val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
     fun aux (tha, thb) =
-      case Thm.bicompose false (false, tha, nprems_of tha) i thb
+      case Thm.bicompose {flatten = true, match = false, incremented = false}
+            (false, tha, nprems_of tha) i thb
            |> Seq.list_of |> distinct Thm.eq_thm of
         [th] => th
       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
                         [tha, thb])
   in
     aux (tha, thb)
-    handle TERM z =>
+    handle TERM z =>  (* FIXME obsolete!? *)
            (* The unifier, which is invoked from "Thm.bicompose", will sometimes
               refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
               "TERM" exception (with "add_ffpair" as first argument). We then
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed May 29 18:25:11 2013 +0200
@@ -869,9 +869,17 @@
 
 (* fact_tac *)
 
+local
+
+fun comp_hhf_tac th i st =
+  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true}
+    (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
+
 fun comp_incr_tac [] _ = no_tac
   | comp_incr_tac (th :: ths) i =
-      (fn st => Goal.compose_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
+      (fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
+
+in
 
 fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
 
@@ -880,6 +888,8 @@
 
 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
 
+end;
+
 
 (* get_thm(s) *)
 
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Wed May 29 18:25:11 2013 +0200
@@ -287,7 +287,10 @@
       Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   in
-    (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
+    (case Seq.list_of
+      (Thm.bicompose {flatten = true, match = false, incremented = false}
+        (false, rl, Thm.nprems_of rl) 1 revcut_rl')
+     of
       [th] => th
     | _ => raise THM ("make_elim_preserve", 1, [rl]))
   end;
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/drule.ML	Wed May 29 18:25:11 2013 +0200
@@ -359,7 +359,9 @@
   with no lifting or renaming!  Q may contain ==> or meta-quants
   ALWAYS deletes premise i *)
 fun compose(tha,i,thb) =
-  distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
+  distinct Thm.eq_thm
+    (Seq.list_of
+      (Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb));
 
 fun compose_single (tha,i,thb) =
   (case compose (tha,i,thb) of
@@ -743,7 +745,8 @@
 
 fun comp_no_flatten (th, n) i rule =
   (case distinct Thm.eq_thm (Seq.list_of
-      (Thm.compose_no_flatten false (th, n) i (incr_indexes th rule))) of
+      (Thm.bicompose {flatten = false, match = false, incremented = true}
+        (false, th, n) i (incr_indexes th rule))) of
     [th'] => th'
   | [] => raise THM ("comp_no_flatten", i, [th, rule])
   | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule]));
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/goal.ML	Wed May 29 18:25:11 2013 +0200
@@ -56,7 +56,6 @@
   val precise_conjunction_tac: int -> int -> tactic
   val recover_conjunction_tac: tactic
   val norm_hhf_tac: int -> tactic
-  val compose_hhf_tac: thm -> int -> tactic
   val assume_rule_tac: Proof.context -> int -> tactic
 end;
 
@@ -359,7 +358,8 @@
 fun retrofit i n st' st =
   (if n = 1 then st
    else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
-  |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
+  |> Thm.bicompose {flatten = false, match = false, incremented = false}
+      (false, conclude st', Thm.nprems_of st') i;
 
 fun SELECT_GOAL tac i st =
   if Thm.nprems_of st = 1 andalso i = 1 then tac st
@@ -403,9 +403,6 @@
     if Drule.is_norm_hhf t then all_tac
     else rewrite_goal_tac Drule.norm_hhf_eqs i);
 
-fun compose_hhf_tac th i st =
-  PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
-
 
 (* non-atomic goal assumptions *)
 
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/subgoal.ML	Wed May 29 18:25:11 2013 +0200
@@ -125,7 +125,10 @@
       |> fold (Thm.forall_elim o #2) subgoal_inst
       |> Thm.adjust_maxidx_thm idx
       |> singleton (Variable.export ctxt2 ctxt0);
-  in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
+  in
+    Thm.bicompose {flatten = true, match = false, incremented = false}
+      (false, result, Thm.nprems_of st1) i st0
+  end;
 
 
 (* tacticals *)
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/tactic.ML	Wed May 29 18:25:11 2013 +0200
@@ -111,7 +111,8 @@
 
 (*The composition rule/state: no lifting or var renaming.
   The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
-fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
+fun compose_tac arg i =
+  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = false} arg i);
 
 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   like [| P&Q; P==>R |] ==> R *)
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/thm.ML	Wed May 29 18:25:11 2013 +0200
@@ -144,8 +144,8 @@
   val permute_prems: int -> int -> thm -> thm
   val rename_params_rule: string list * int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
-  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
-  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
+  val bicompose: {flatten: bool, match: bool, incremented: bool} ->
+    bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   val extern_oracles: Proof.context -> (Markup.T * xstring) list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
@@ -1615,7 +1615,7 @@
 *)
 local exception COMPOSE
 in
-fun bicompose_aux flatten match (state, (stpairs, Bs, Bi, C), lifted)
+fun bicompose_aux {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
                         (eres_flg, orule, nsubgoal) =
  let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
      and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
@@ -1705,17 +1705,14 @@
 
      val env0 = Envir.empty (Int.max (rmax, smax));
  in
-   (case if lifted then SOME env0 else unify_var_types thy (state, orule) env0 of
+   (case if incremented then SOME env0 else unify_var_types thy (state, orule) env0 of
      NONE => Seq.empty
    | SOME env => if eres_flg then eres env (rev rAs) else res env)
  end;
 end;
 
-fun compose_no_flatten match (orule, nsubgoal) i state =
-  bicompose_aux false match (state, dest_state (state, i), false) (false, orule, nsubgoal);
-
-fun bicompose match arg i state =
-  bicompose_aux true match (state, dest_state (state,i), false) arg;
+fun bicompose flags arg i state =
+  bicompose_aux flags (state, dest_state (state,i), false) arg;
 
 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
@@ -1733,7 +1730,9 @@
         val lift = lift_rule (cprem_of state i);
         val B = Logic.strip_assums_concl Bi;
         val Hs = Logic.strip_assums_hyp Bi;
-        val compose = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true);
+        val compose =
+          bicompose_aux {flatten = true, match = match, incremented = true}
+            (state, (stpairs, Bs, Bi, C), true);
         fun res [] = Seq.empty
           | res ((eres_flg, rule)::brules) =
               if !Pattern.trace_unify_fail orelse
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Tools/eqsubst.ML	Wed May 29 18:25:11 2013 +0200
@@ -365,12 +365,6 @@
       (* ~j because new asm starts at back, thus we subtract 1 *)
       Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
       (Tactic.dtac preelimrule i th2)
-
-      (* (Thm.bicompose
-                 false (* use unification *)
-                 (true, (* elim resolution *)
-                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
-                 i th2) *)
     end;
 
 
diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Tools/misc_legacy.ML	Wed May 29 18:25:11 2013 +0200
@@ -203,7 +203,9 @@
                   (forall_intr_list cparams (implies_intr_list chyps Cth)))
         end
       (*function to replace the current subgoal*)
-      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
+      fun next st =
+        Thm.bicompose {flatten = true, match = false, incremented = false}
+          (false, relift st, nprems_of st) gno state
   in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
 
 fun print_vars_terms n thm =