# HG changeset patch # User wenzelm # Date 1246908270 -7200 # Node ID d5f186aa0beda31177f79b4fb064158567da98d3 # Parent c8a35979a5bce44c84555d0790401429fceb6730 structure Thm: less pervasive names; diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Bali/AxCompl.thy --- 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) diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Import/import.ML --- 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 diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Import/proof_kernel.ML --- 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 diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Import/shuffler.ML --- 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 diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Set.thy --- 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 diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/TLA/Intensional.thy --- 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]) diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Tools/TFL/rules.ML --- 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; diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Tools/meson.ML --- 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; diff -r c8a35979a5bc -r d5f186aa0bed src/HOL/Tools/metis_tools.ML --- 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 diff -r c8a35979a5bc -r d5f186aa0bed src/Provers/blast.ML --- 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 []) diff -r c8a35979a5bc -r d5f186aa0bed src/Provers/classical.ML --- 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 ****) diff -r c8a35979a5bc -r d5f186aa0bed src/Pure/Isar/rule_insts.ML --- 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; diff -r c8a35979a5bc -r d5f186aa0bed src/Pure/drule.ML --- 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

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 diff -r c8a35979a5bc -r d5f186aa0bed src/Pure/tactic.ML --- 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 = diff -r c8a35979a5bc -r d5f186aa0bed src/Pure/tctical.ML --- 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; diff -r c8a35979a5bc -r d5f186aa0bed src/Pure/thm.ML --- 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; diff -r c8a35979a5bc -r d5f186aa0bed src/Tools/IsaPlanner/isand.ML --- 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; (*