--- a/src/HOL/Bali/AxCompl.thy Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Bali/AxCompl.thy Mon Jul 06 21:24:30 2009 +0200
@@ -1402,7 +1402,7 @@
apply -
apply (induct_tac "n")
apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
-apply (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
+apply (tactic {* dtac (Thm.permute_prems 0 1 (thm "card_seteq")) 1 *})
apply simp
apply (erule finite_imageI)
apply (simp add: MGF_asm ax_derivs_asm)
--- a/src/HOL/Import/import.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Import/import.ML Mon Jul 06 21:24:30 2009 +0200
@@ -55,7 +55,7 @@
then message "import: Terms match up"
else message "import: Terms DO NOT match up"
val thm' = equal_elim (symmetric prew) thm
- val res = bicompose true (false,thm',0) 1 th
+ val res = Thm.bicompose true (false,thm',0) 1 th
in
res
end
--- a/src/HOL/Import/proof_kernel.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Jul 06 21:24:30 2009 +0200
@@ -977,7 +977,7 @@
fun uniq_compose m th i st =
let
- val res = bicompose false (false,th,m) i st
+ val res = Thm.bicompose false (false,th,m) i st
in
case Seq.pull res of
SOME (th,rest) => (case Seq.pull rest of
@@ -1065,14 +1065,12 @@
res
end
-val permute_prems = Thm.permute_prems
-
fun rearrange sg tm th =
let
val tm' = Envir.beta_eta_contract tm
- fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
+ fun find [] n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
| find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
- then permute_prems n 1 th
+ then Thm.permute_prems n 1 th
else find ps (n+1)
in
find (prems_of th) 0
@@ -1193,7 +1191,7 @@
fun if_debug f x = if !debug then f x else ()
val message = if_debug writeln
-val conjE_helper = permute_prems 0 1 conjE
+val conjE_helper = Thm.permute_prems 0 1 conjE
fun get_hol4_thm thyname thmname thy =
case get_hol4_theorem thyname thmname thy of
--- a/src/HOL/Import/shuffler.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Mon Jul 06 21:24:30 2009 +0200
@@ -595,7 +595,7 @@
val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
val triv_th = trivial rhs
val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
- val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
+ val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
SOME(th,_) => SOME th
| NONE => NONE
in
--- a/src/HOL/Set.thy Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Set.thy Mon Jul 06 21:24:30 2009 +0200
@@ -449,7 +449,7 @@
lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
by (unfold Ball_def) blast
-ML {* bind_thm ("rev_ballE", permute_prems 1 1 @{thm ballE}) *}
+ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
text {*
\medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
--- a/src/HOL/TLA/Intensional.thy Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/TLA/Intensional.thy Mon Jul 06 21:24:30 2009 +0200
@@ -268,7 +268,7 @@
let
(* analogous to RS, but using matching instead of resolution *)
fun matchres tha i thb =
- case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
+ case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of
([th],_) => th
| ([],_) => raise THM("matchres: no match", i, [tha,thb])
| _ => raise THM("matchres: multiple unifiers", i, [tha,thb])
--- a/src/HOL/Tools/TFL/rules.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Mon Jul 06 21:24:30 2009 +0200
@@ -519,14 +519,14 @@
handle TERM _ => get (rst, n+1, L)
| U.ERR _ => get (rst, n+1, L);
-(* Note: rename_params_rule counts from 1, not 0 *)
+(* Note: Thm.rename_params_rule counts from 1, not 0 *)
fun rename thm =
let val thy = Thm.theory_of_thm thm
val tych = cterm_of thy
val ants = Logic.strip_imp_prems (Thm.prop_of thm)
val news = get (ants,1,[])
in
- fold rename_params_rule news thm
+ fold Thm.rename_params_rule news thm
end;
--- a/src/HOL/Tools/meson.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Tools/meson.ML Mon Jul 06 21:24:30 2009 +0200
@@ -470,7 +470,7 @@
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
fun TRYING_eq_assume_tac 0 st = Seq.single st
| TRYING_eq_assume_tac i st =
- TRYING_eq_assume_tac (i-1) (eq_assumption i st)
+ TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
handle THM _ => TRYING_eq_assume_tac (i-1) st;
fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
--- a/src/HOL/Tools/metis_tools.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Mon Jul 06 21:24:30 2009 +0200
@@ -339,7 +339,7 @@
could then fail. See comment on mk_var.*)
fun resolve_inc_tyvars(tha,i,thb) =
let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
- val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb)
+ val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
in
case distinct Thm.eq_thm ths of
[th] => th
--- a/src/Provers/blast.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Provers/blast.ML Mon Jul 06 21:24:30 2009 +0200
@@ -473,7 +473,7 @@
(*Like dup_elim, but puts the duplicated major premise FIRST*)
-fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd;
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
(*Rotate the assumptions in all new subgoals for the LIFO discipline*)
@@ -485,7 +485,7 @@
fun rot_tac [] i st = Seq.single st
| rot_tac (0::ks) i st = rot_tac ks (i+1) st
- | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
+ | rot_tac (k::ks) i st = rot_tac ks (i+1) (Thm.rotate_rule (~k) i st);
in
fun rot_subgoals_tac (rot, rl) =
rot_tac (if rot then map nNewHyps rl else [])
--- a/src/Provers/classical.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Provers/classical.ML Mon Jul 06 21:24:30 2009 +0200
@@ -209,7 +209,7 @@
fun dup_elim th =
rule_by_tactic (TRYALL (etac revcut_rl))
- ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
+ ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
(**** Classical rule sets ****)
--- a/src/Pure/Isar/rule_insts.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML Mon Jul 06 21:24:30 2009 +0200
@@ -354,7 +354,7 @@
instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
in
- (case Seq.list_of (bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
+ (case Seq.list_of (Thm.bicompose 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 Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Pure/drule.ML Mon Jul 06 21:24:30 2009 +0200
@@ -373,23 +373,25 @@
(*Rotates a rule's premises to the left by k*)
fun rotate_prems 0 = I
- | rotate_prems k = permute_prems 0 k;
+ | rotate_prems k = Thm.permute_prems 0 k;
fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i);
-(* permute prems, where the i-th position in the argument list (counting from 0)
- gives the position within the original thm to be transferred to position i.
- Any remaining trailing positions are left unchanged. *)
-val rearrange_prems = let
- fun rearr new [] thm = thm
- | rearr new (p::ps) thm = rearr (new+1)
- (map (fn q => if new<=q andalso q<p then q+1 else q) ps)
- (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
+(*Permute prems, where the i-th position in the argument list (counting from 0)
+ gives the position within the original thm to be transferred to position i.
+ Any remaining trailing positions are left unchanged.*)
+val rearrange_prems =
+ let
+ fun rearr new [] thm = thm
+ | rearr new (p :: ps) thm =
+ rearr (new + 1)
+ (map (fn q => if new <= q andalso q < p then q + 1 else q) ps)
+ (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm))
in rearr 0 end;
(*Resolution: exactly one resolvent must be produced.*)
fun tha RSN (i,thb) =
- case Seq.chop 2 (biresolution false [(false,tha)] i thb) of
+ case Seq.chop 2 (Thm.biresolution false [(false,tha)] i thb) of
([th],_) => th
| ([],_) => raise THM("RSN: no unifiers", i, [tha,thb])
| _ => raise THM("RSN: multiple unifiers", i, [tha,thb]);
@@ -399,7 +401,7 @@
(*For joining lists of rules*)
fun thas RLN (i,thbs) =
- let val resolve = biresolution false (map (pair false) thas) i
+ let val resolve = Thm.biresolution false (map (pair false) thas) i
fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
in maps resb thbs end;
@@ -425,7 +427,7 @@
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 (bicompose false (false,tha,0) i thb));
+ distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
fun compose_single (tha,i,thb) =
case compose (tha,i,thb) of
--- a/src/Pure/tactic.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Pure/tactic.ML Mon Jul 06 21:24:30 2009 +0200
@@ -105,24 +105,24 @@
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
(*Solve subgoal i by assumption*)
-fun assume_tac i = PRIMSEQ (assumption i);
+fun assume_tac i = PRIMSEQ (Thm.assumption i);
(*Solve subgoal i by assumption, using no unification*)
-fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
+fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
(** Resolution/matching tactics **)
(*The composition rule/state: no lifting or var renaming.
- The arg = (bires_flg, orule, m) ; see bicompose for explanation.*)
-fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
+ The arg = (bires_flg, orule, m); see Thm.bicompose for explanation.*)
+fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
like [| P&Q; P==>R |] ==> R *)
fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
(*Attack subgoal i by resolution, using flags to indicate elimination rules*)
-fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
+fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution false brules i);
(*Resolution: the simple case, works for introduction rules*)
fun resolve_tac rules = biresolve_tac (map (pair false) rules);
@@ -152,7 +152,7 @@
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
(*Matching tactics -- as above, but forbid updating of state*)
-fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
+fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution true brules i);
fun match_tac rules = bimatch_tac (map (pair false) rules);
fun ematch_tac rules = bimatch_tac (map (pair true) rules);
fun dmatch_tac rls = ematch_tac (map make_elim rls);
@@ -295,7 +295,7 @@
let val hyps = Logic.strip_assums_hyp prem
and concl = Logic.strip_assums_concl prem
val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
- in PRIMSEQ (biresolution match (order kbrls) i) end);
+ in PRIMSEQ (Thm.biresolution match (order kbrls) i) end);
(*versions taking pre-built nets. No filtering of brls*)
val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
@@ -326,7 +326,7 @@
in
if pred krls
then PRIMSEQ
- (biresolution match (map (pair false) (order_list krls)) i)
+ (Thm.biresolution match (map (pair false) (order_list krls)) i)
else no_tac
end);
@@ -359,15 +359,15 @@
fun rename_tac xs i =
case Library.find_first (not o Syntax.is_identifier) xs of
SOME x => error ("Not an identifier: " ^ x)
- | NONE => PRIMITIVE (rename_params_rule (xs, i));
+ | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
right to left if n is positive, and from left to right if n is negative.*)
fun rotate_tac 0 i = all_tac
- | rotate_tac k i = PRIMITIVE (rotate_rule k i);
+ | rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i);
(*Rotates the given subgoal to be the last.*)
-fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
+fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
(* remove premises that do not satisfy p; fails if all prems satisfy p *)
fun filter_prems_tac p =
--- a/src/Pure/tctical.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Pure/tctical.ML Mon Jul 06 21:24:30 2009 +0200
@@ -463,8 +463,7 @@
(forall_intr_list cparams (implies_intr_list chyps Cth)))
end
(*function to replace the current subgoal*)
- fun next st = bicompose false (false, relift st, nprems_of st)
- gno state
+ fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
end;
--- a/src/Pure/thm.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Pure/thm.ML Mon Jul 06 21:24:30 2009 +0200
@@ -97,14 +97,6 @@
val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
val incr_indexes: int -> thm -> thm
- val assumption: int -> thm -> thm Seq.seq
- val eq_assumption: int -> thm -> thm
- val rotate_rule: int -> int -> thm -> thm
- val permute_prems: int -> int -> thm -> thm
- val rename_params_rule: string list * int -> 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 biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
end;
signature THM =
@@ -117,37 +109,45 @@
val dest_fun2: cterm -> cterm
val dest_arg1: cterm -> cterm
val dest_abs: string option -> cterm -> cterm * cterm
- val adjust_maxidx_cterm: int -> cterm -> cterm
val capply: cterm -> cterm -> cterm
val cabs: cterm -> cterm -> cterm
- val major_prem_of: thm -> term
- val no_prems: thm -> bool
+ val adjust_maxidx_cterm: int -> cterm -> cterm
+ val incr_indexes_cterm: int -> cterm -> cterm
+ val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
+ val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
val terms_of_tpairs: (term * term) list -> term list
+ val full_prop_of: thm -> term
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
val hyps_of: thm -> term list
- val full_prop_of: thm -> term
+ val no_prems: thm -> bool
+ val major_prem_of: thm -> term
val axiom: theory -> string -> thm
val axioms_of: theory -> (string * thm) list
- val get_name: thm -> string
- val put_name: string -> thm -> thm
val get_tags: thm -> Properties.T
val map_tags: (Properties.T -> Properties.T) -> thm -> thm
val norm_proof: thm -> thm
val adjust_maxidx_thm: int -> thm -> thm
- val rename_boundvars: term -> term -> thm -> thm
- val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
- val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
- val incr_indexes_cterm: int -> cterm -> cterm
val varifyT: thm -> thm
val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val freezeT: thm -> thm
+ val assumption: int -> thm -> thm Seq.seq
+ val eq_assumption: int -> thm -> thm
+ val rotate_rule: int -> int -> thm -> thm
+ val permute_prems: int -> int -> thm -> thm
+ val rename_params_rule: string list * int -> 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 biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
+ val rename_boundvars: term -> term -> thm -> thm
val future: thm future -> cterm -> thm
val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val join_proof: thm -> unit
+ val get_name: thm -> string
+ val put_name: string -> thm -> thm
val extern_oracles: theory -> xstring list
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
--- a/src/Tools/IsaPlanner/isand.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Mon Jul 06 21:24:30 2009 +0200
@@ -110,7 +110,7 @@
fun solve_with sol th =
let fun solvei 0 = Seq.empty
| solvei i =
- Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
+ Seq.append (Thm.bicompose false (false,sol,0) i th) (solvei (i - 1))
in
solvei (Thm.nprems_of th)
end;
@@ -337,7 +337,7 @@
val newth' = Drule.implies_intr_list sgallcts allified_newth
in
- bicompose false (false, newth', (length sgallcts)) i gth
+ Thm.bicompose false (false, newth', (length sgallcts)) i gth
end;
(*