--- 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)
--- 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)))
--- 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
--- 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) *)
--- 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;
--- 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]));
--- 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 *)
--- 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 *)
--- 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 *)
--- 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
--- 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;
--- 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 =