# HG changeset patch # User wenzelm # Date 1372345582 -7200 # Node ID 24c6ddb48cb84086720b5f4c184c07d396903d09 # Parent a3b175675843fbfb039017b9dc1b2561f61de4d5 tuned signature; diff -r a3b175675843 -r 24c6ddb48cb8 src/Doc/IsarImplementation/Tactic.thy --- 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 - "\"} and @{text "\\<^sub>1 \ \ \\<^sub>n \ \"}. For each @{text "s"} that unifies - @{text "\"} and @{text "\"}, the result list contains the theorem - @{text "(\\<^sub>1 \ \ \\<^sub>i\<^sub>-\<^sub>1 \ \\<^sub>i\<^sub>+\<^sub>1 \ \ \\<^sub>n \ \)s"}. + "\"} and @{text "\\<^sub>1 \ \ \\<^sub>n \ \"}. The unique @{text "s"} that + unifies @{text "\"} and @{text "\"} yields the theorem @{text "(\\<^sub>1 \ + \ \\<^sub>i\<^sub>-\<^sub>1 \ \\<^sub>i\<^sub>+\<^sub>1 \ \ \\<^sub>n \ \)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} diff -r a3b175675843 -r 24c6ddb48cb8 src/HOL/Tools/Function/function_core.ML --- 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) diff -r a3b175675843 -r 24c6ddb48cb8 src/HOL/Tools/Function/induction_schema.ML --- 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 P x" *) diff -r a3b175675843 -r 24c6ddb48cb8 src/HOL/Tools/Function/pat_completeness.ML --- 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) diff -r a3b175675843 -r 24c6ddb48cb8 src/HOL/Tools/groebner.ML --- 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}; diff -r a3b175675843 -r 24c6ddb48cb8 src/Pure/drule.ML --- 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 **) diff -r a3b175675843 -r 24c6ddb48cb8 src/Tools/IsaPlanner/isand.ML --- 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