--- a/src/Doc/IsarImplementation/Tactic.thy Thu Jun 27 12:34:58 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy Thu Jun 27 17:06:22 2013 +0200
@@ -484,14 +484,14 @@
Raw composition of two rules means resolving them without prior
lifting or renaming of unknowns. This low-level operation, which
underlies the resolution tactics, may occasionally be useful for
- special effects. Schematic variables are not renamed, so beware of
- clashes!
+ special effects. Schematic variables are not renamed by default, so
+ beware of clashes!
*}
text %mlref {*
\begin{mldecls}
@{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
- @{index_ML Drule.compose: "thm * int * thm -> thm list"} \\
+ @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
@{index_ML_op COMP: "thm * thm -> thm"} \\
\end{mldecls}
@@ -508,13 +508,13 @@
\item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
regarded as an atomic formula, to solve premise @{text "i"} of
@{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
- "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. For each @{text "s"} that unifies
- @{text "\<psi>"} and @{text "\<phi>"}, the result list contains the theorem
- @{text "(\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.
+ "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. The unique @{text "s"} that
+ unifies @{text "\<psi>"} and @{text "\<phi>"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
+ \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}. Multiple results are considered as
+ error (exception @{ML THM}).
- \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "Drule.compose (thm\<^sub>1, 1,
- thm\<^sub>2)"} and returns the result, if unique; otherwise, it raises
- exception @{ML THM}.
+ \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose
+ (thm\<^sub>1, 1, thm\<^sub>2)"}.
\end{description}
--- a/src/HOL/Tools/Function/function_core.ML Thu Jun 27 12:34:58 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Thu Jun 27 17:06:22 2013 +0200
@@ -420,7 +420,7 @@
|> Thm.implies_intr (ihyp)
|> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
|> Thm.forall_intr (cterm_of thy x)
- |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+ |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
|> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
val goalstate = Conjunction.intr graph_is_function complete
@@ -810,7 +810,7 @@
|> (fn it => it COMP accI)
|> Thm.implies_intr ihyp
|> Thm.forall_intr (cterm_of thy x)
- |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
+ |> (fn it => Drule.compose (it, 2, wf_induct_rule))
|> curry op RS (Thm.assume wfR')
|> forall_intr_vars
|> (fn it => it COMP allI)
--- a/src/HOL/Tools/Function/induction_schema.ML Thu Jun 27 12:34:58 2013 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Thu Jun 27 17:06:22 2013 +0200
@@ -328,7 +328,7 @@
|> split_list |> apsnd flat
val istep = sum_split_rule
- |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
+ |> fold (fn b => fn th => Drule.compose (b, 1, th)) branches
|> Thm.implies_intr ihyp
|> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
--- a/src/HOL/Tools/Function/pat_completeness.ML Thu Jun 27 12:34:58 2013 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML Thu Jun 27 17:06:22 2013 +0200
@@ -152,7 +152,7 @@
val complete_thm = prove_completeness ctxt xs thesis qss patss
|> fold_rev (Thm.forall_intr o cterm_of thy) vs
in
- PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
+ PRIMITIVE (fn st => Drule.compose (complete_thm, i, st))
end
handle COMPLETENESS => no_tac)
--- a/src/HOL/Tools/groebner.ML Thu Jun 27 12:34:58 2013 +0200
+++ b/src/HOL/Tools/groebner.ML Thu Jun 27 17:06:22 2013 +0200
@@ -388,9 +388,9 @@
fun refute_disj rfn tm =
case term_of tm of
Const(@{const_name HOL.disj},_)$l$r =>
- Drule.compose_single
+ Drule.compose
(refute_disj rfn (Thm.dest_arg tm), 2,
- Drule.compose_single (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
+ Drule.compose (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
| _ => rfn tm ;
val notnotD = @{thm notnotD};
--- a/src/Pure/drule.ML Thu Jun 27 12:34:58 2013 +0200
+++ b/src/Pure/drule.ML Thu Jun 27 17:06:22 2013 +0200
@@ -68,8 +68,7 @@
val store_standard_thm_open: binding -> thm -> thm
val multi_resolve: thm list -> thm -> thm Seq.seq
val multi_resolves: thm list -> thm list -> thm Seq.seq
- val compose: thm * int * thm -> thm list
- val compose_single: thm * int * thm -> thm
+ val compose: thm * int * thm -> thm
val equals_cong: thm
val imp_cong: thm
val swap_prems_eq: thm
@@ -358,15 +357,10 @@
(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
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 {flatten = true, match = false, incremented = false} (false, tha, 0) i thb));
-
-fun compose_single (tha,i,thb) =
- (case compose (tha,i,thb) of
- [th] => th
- | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
+fun compose (tha, i, thb) =
+ Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
+ |> Seq.list_of |> distinct Thm.eq_thm
+ |> (fn [th] => th | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
(** theorem equality **)
--- a/src/Tools/IsaPlanner/isand.ML Thu Jun 27 12:34:58 2013 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Thu Jun 27 17:06:22 2013 +0200
@@ -50,7 +50,7 @@
val solth' = solth
|> Drule.implies_intr_list hcprems
|> Drule.forall_intr_list cfvs;
- in Drule.compose_single (solth', i, gth) end;
+ in Drule.compose (solth', i, gth) end;
fun variant_names ctxt ts xs =
let