# HG changeset patch # User wenzelm # Date 1237295665 -3600 # Node ID e99c5466af9294a7d2cb819ff7b6934120505b1a # Parent 7b0017587e7d6417a38fca58fa90fea8f144d307# Parent 0cc3b7f03ade4d757e79e3456d79ba4c3d7cde51 merged diff -r 7b0017587e7d -r e99c5466af92 doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Mar 16 15:58:41 2009 -0700 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Tue Mar 17 14:14:25 2009 +0100 @@ -807,12 +807,12 @@ text %mlref {* \begin{mldecls} - @{index_ML MetaSimplifier.norm_hhf: "thm -> thm"} \\ + @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\ \end{mldecls} \begin{description} - \item @{ML MetaSimplifier.norm_hhf}~@{text thm} normalizes the given + \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given theorem according to the canonical form specified above. This is occasionally helpful to repair some low-level tools that do not handle Hereditary Harrop Formulae properly. diff -r 7b0017587e7d -r e99c5466af92 doc-src/IsarImplementation/Thy/document/Logic.tex --- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Mar 16 15:58:41 2009 -0700 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Tue Mar 17 14:14:25 2009 +0100 @@ -821,12 +821,12 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\ + \indexdef{}{ML}{Simplifier.norm\_hhf}\verb|Simplifier.norm_hhf: thm -> thm| \\ \end{mldecls} \begin{description} - \item \verb|MetaSimplifier.norm_hhf|~\isa{thm} normalizes the given + \item \verb|Simplifier.norm_hhf|~\isa{thm} normalizes the given theorem according to the canonical form specified above. This is occasionally helpful to repair some low-level tools that do not handle Hereditary Harrop Formulae properly. diff -r 7b0017587e7d -r e99c5466af92 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Mar 17 14:14:25 2009 +0100 @@ -91,13 +91,13 @@ structure FundefData = GenericDataFun ( - type T = (term * fundef_context_data) NetRules.T; - val empty = NetRules.init + type T = (term * fundef_context_data) Item_Net.T; + val empty = Item_Net.init (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool) fst; val copy = I; val extend = I; - fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) + fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2) ); val get_fundef = FundefData.get o Context.Proof; @@ -122,11 +122,11 @@ SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) handle Pattern.MATCH => NONE in - get_first match (NetRules.retrieve (get_fundef ctxt) t) + get_first match (Item_Net.retrieve (get_fundef ctxt) t) end fun import_last_fundef ctxt = - case NetRules.rules (get_fundef ctxt) of + case Item_Net.content (get_fundef ctxt) of [] => NONE | (t, data) :: _ => let @@ -135,10 +135,10 @@ import_fundef_data t' ctxt' end -val all_fundef_data = NetRules.rules o get_fundef +val all_fundef_data = Item_Net.content o get_fundef fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = - FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) + FundefData.map (fold (fn f => Item_Net.insert (f, data)) fs) #> store_termination_rule termination diff -r 7b0017587e7d -r e99c5466af92 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/HOL/Tools/inductive_package.ML Tue Mar 17 14:14:25 2009 +0100 @@ -302,7 +302,7 @@ hol_simplify inductive_conj #> hol_simplify inductive_rulify #> hol_simplify inductive_rulify_fallback - #> MetaSimplifier.norm_hhf; + #> Simplifier.norm_hhf; end; diff -r 7b0017587e7d -r e99c5466af92 src/Provers/blast.ML --- a/src/Provers/blast.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Provers/blast.ML Tue Mar 17 14:14:25 2009 +0100 @@ -564,11 +564,11 @@ (Const ("*Goal*", _) $ G) => let val pG = mk_Trueprop (toTerm 2 G) val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps - in map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs) end + in map (fromIntrRule thy vars o #2) (order_list intrs) end | _ => let val pP = mk_Trueprop (toTerm 3 P) val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps - in map_filter (fromRule thy vars o #2) (Tactic.orderlist elims) end; + in map_filter (fromRule thy vars o #2) (order_list elims) end; (*Normalize a branch--for tracing*) diff -r 7b0017587e7d -r e99c5466af92 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Provers/classical.ML Tue Mar 17 14:14:25 2009 +0100 @@ -688,7 +688,7 @@ (*version of bimatch_from_nets_tac that only applies rules that create precisely n subgoals.*) fun n_bimatch_from_nets_tac n = - biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true; + biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true; fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; diff -r 7b0017587e7d -r e99c5466af92 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/IsaMakefile Tue Mar 17 14:14:25 2009 +0100 @@ -61,7 +61,7 @@ Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \ Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \ Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ - Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ + Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ @@ -89,12 +89,12 @@ Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \ conjunction.ML consts.ML context.ML context_position.ML conv.ML \ defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \ - interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \ - morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \ - primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \ - sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \ - term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \ - type_infer.ML unify.ML variable.ML + interpretation.ML item_net.ML library.ML logic.ML meta_simplifier.ML \ + more_thm.ML morphism.ML name.ML net.ML old_goals.ML old_term.ML \ + pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML \ + search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML \ + tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML \ + type.ML type_infer.ML unify.ML variable.ML @./mk diff -r 7b0017587e7d -r e99c5466af92 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/Isar/ROOT.ML Tue Mar 17 14:14:25 2009 +0100 @@ -44,7 +44,6 @@ use "proof.ML"; use "../ML/ml_thms.ML"; use "element.ML"; -use "net_rules.ML"; (*derived theory and proof elements*) use "calculation.ML"; @@ -89,5 +88,3 @@ use "../Thy/thm_deps.ML"; use "isar_cmd.ML"; use "isar_syn.ML"; - - diff -r 7b0017587e7d -r e99c5466af92 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/Isar/calculation.ML Tue Mar 17 14:14:25 2009 +0100 @@ -29,18 +29,18 @@ structure CalculationData = GenericDataFun ( - type T = (thm NetRules.T * thm list) * (thm list * int) option; - val empty = ((NetRules.elim, []), NONE); + type T = (thm Item_Net.T * thm list) * (thm list * int) option; + val empty = ((Thm.elim_rules, []), NONE); val extend = I; fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = - ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); + ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); ); fun print_rules ctxt = let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in [Pretty.big_list "transitivity rules:" - (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)), + (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)), Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |> Pretty.chunks |> Pretty.writeln end; @@ -66,8 +66,8 @@ (* add/del rules *) -val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert); -val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete); +val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert); +val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete); val sym_add = Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) @@ -130,8 +130,8 @@ fun combine ths = (case opt_rules of SOME rules => rules | NONE => - (case ths of [] => NetRules.rules (#1 (get_rules state)) - | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th))) + (case ths of [] => Item_Net.content (#1 (get_rules state)) + | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th))) |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) |> Seq.filter (not o projection ths); diff -r 7b0017587e7d -r e99c5466af92 src/Pure/Isar/net_rules.ML --- a/src/Pure/Isar/net_rules.ML Mon Mar 16 15:58:41 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,69 +0,0 @@ -(* Title: Pure/Isar/net_rules.ML - Author: Markus Wenzel, TU Muenchen - -Efficient storage of rules: preserves order, prefers later entries. -*) - -signature NET_RULES = -sig - type 'a T - val rules: 'a T -> 'a list - val retrieve: 'a T -> term -> 'a list - val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T - val merge: 'a T * 'a T -> 'a T - val delete: 'a -> 'a T -> 'a T - val insert: 'a -> 'a T -> 'a T - val intro: thm T - val elim: thm T -end; - -structure NetRules: NET_RULES = -struct - -(* datatype rules *) - -datatype 'a T = - Rules of { - eq: 'a * 'a -> bool, - index: 'a -> term, - rules: 'a list, - next: int, - net: (int * 'a) Net.net}; - -fun mk_rules eq index rules next net = - Rules {eq = eq, index = index, rules = rules, next = next, net = net}; - -fun rules (Rules {rules = rs, ...}) = rs; - -fun retrieve (Rules {rules, net, ...}) tm = - Tactic.untaglist - ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm))); - - -(* build rules *) - -fun init eq index = mk_rules eq index [] ~1 Net.empty; - -fun add rule (Rules {eq, index, rules, next, net}) = - mk_rules eq index (rule :: rules) (next - 1) - (Net.insert_term (K false) (index rule, (next, rule)) net); - -fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) = - let val rules = Library.merge eq (rules1, rules2) - in fold_rev add rules (init eq index) end; - -fun delete rule (rs as Rules {eq, index, rules, next, net}) = - if not (member eq rules rule) then rs - else mk_rules eq index (remove eq rule rules) next - (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net); - -fun insert rule rs = add rule (delete rule rs); (*ensure that new rule gets precedence*) - - -(* intro/elim rules *) - -val intro = init Thm.eq_thm_prop Thm.concl_of; -val elim = init Thm.eq_thm_prop Thm.major_prem_of; - - -end; diff -r 7b0017587e7d -r e99c5466af92 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/Isar/proof.ML Tue Mar 17 14:14:25 2009 +0100 @@ -440,12 +440,18 @@ (* refine via sub-proof *) +fun finish_tac 0 = K all_tac + | finish_tac n = + Goal.norm_hhf_tac THEN' + SUBGOAL (fn (goal, i) => + if can Logic.unprotect (Logic.strip_assums_concl goal) then + Tactic.etac Drule.protectI i THEN finish_tac (n - 1) i + else finish_tac (n - 1) (i + 1)); + fun goal_tac rule = - Goal.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW - (Goal.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) => - if can Logic.unprotect (Logic.strip_assums_concl goal) then - Tactic.etac Drule.protectI i - else all_tac))); + Goal.norm_hhf_tac THEN' + Tactic.rtac rule THEN' + finish_tac (Thm.nprems_of rule); fun refine_goals print_rule inner raw_rules state = let diff -r 7b0017587e7d -r e99c5466af92 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/ROOT.ML Tue Mar 17 14:14:25 2009 +0100 @@ -52,11 +52,12 @@ use "ML/ml_syntax.ML"; (*core of tactical proof system*) +use "net.ML"; +use "item_net.ML"; use "envir.ML"; use "consts.ML"; use "primitive_defs.ML"; use "defs.ML"; -use "net.ML"; use "sign.ML"; use "pattern.ML"; use "unify.ML"; diff -r 7b0017587e7d -r e99c5466af92 src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/drule.ML Tue Mar 17 14:14:25 2009 +0100 @@ -787,14 +787,12 @@ val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq); val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq]; -fun is_norm_hhf tm = - let - fun is_norm (Const ("Pure.sort_constraint", _)) = false - | is_norm (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false - | is_norm (t $ u) = is_norm t andalso is_norm u - | is_norm (Abs (_, _, t)) = is_norm t - | is_norm _ = true; - in is_norm (Envir.beta_eta_contract tm) end; +fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false + | is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false + | is_norm_hhf (Abs _ $ _) = false + | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u + | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t + | is_norm_hhf _ = true; fun norm_hhf thy t = if is_norm_hhf t then t diff -r 7b0017587e7d -r e99c5466af92 src/Pure/item_net.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/item_net.ML Tue Mar 17 14:14:25 2009 +0100 @@ -0,0 +1,58 @@ +(* Title: Pure/item_net.ML + Author: Markus Wenzel, TU Muenchen + +Efficient storage of items indexed by terms; preserves order and +prefers later entries. +*) + +signature ITEM_NET = +sig + type 'a T + val content: 'a T -> 'a list + val retrieve: 'a T -> term -> 'a list + val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T + val merge: 'a T * 'a T -> 'a T + val delete: 'a -> 'a T -> 'a T + val insert: 'a -> 'a T -> 'a T +end; + +structure Item_Net: ITEM_NET = +struct + +(* datatype *) + +datatype 'a T = + Items of { + eq: 'a * 'a -> bool, + index: 'a -> term, + content: 'a list, + next: int, + net: (int * 'a) Net.net}; + +fun mk_items eq index content next net = + Items {eq = eq, index = index, content = content, next = next, net = net}; + +fun content (Items {content, ...}) = content; +fun retrieve (Items {net, ...}) = order_list o Net.unify_term net; + + +(* build net *) + +fun init eq index = mk_items eq index [] ~1 Net.empty; + +fun add x (Items {eq, index, content, next, net}) = + mk_items eq index (x :: content) (next - 1) + (Net.insert_term (K false) (index x, (next, x)) net); + +fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) = + let val content = Library.merge eq (content1, content2) + in fold_rev add content (init eq index) end; + +fun delete x (items as Items {eq, index, content, next, net}) = + if not (member eq content x) then items + else mk_items eq index (remove eq x content) next + (Net.delete_term (eq o pairself #2) (index x, (0, x)) net); + +fun insert x items = add x (delete x items); (*ensure that added entry gets precedence*) + +end; diff -r 7b0017587e7d -r e99c5466af92 src/Pure/library.ML --- a/src/Pure/library.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/library.ML Tue Mar 17 14:14:25 2009 +0100 @@ -211,6 +211,9 @@ val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list val sort_strings: string list -> string list val sort_wrt: ('a -> string) -> 'a list -> 'a list + val tag_list: int -> 'a list -> (int * 'a) list + val untag_list: (int * 'a) list -> 'a list + val order_list: (int * 'a) list -> 'a list (*random numbers*) exception RANDOM @@ -1015,6 +1018,23 @@ fun sort_wrt sel xs = sort (string_ord o pairself sel) xs; +(* items tagged by integer index *) + +(*insert tags*) +fun tag_list k [] = [] + | tag_list k (x :: xs) = (k, x) :: tag_list (k + 1) xs; + +(*remove tags and suppress duplicates -- list is assumed sorted!*) +fun untag_list [] = [] + | untag_list [(k: int, x)] = [x] + | untag_list ((k, x) :: (rest as (k', x') :: _)) = + if k = k' then untag_list rest + else x :: untag_list rest; + +(*return list elements in original order*) +fun order_list list = untag_list (sort (int_ord o pairself fst) list); + + (** random numbers **) diff -r 7b0017587e7d -r e99c5466af92 src/Pure/logic.ML --- a/src/Pure/logic.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/logic.ML Tue Mar 17 14:14:25 2009 +0100 @@ -65,6 +65,7 @@ val flatten_params: int -> term -> term val list_rename_params: string list * term -> term val assum_pairs: int * term -> (term*term)list + val assum_problems: int * term -> (term -> term) * term list * term val varifyT: typ -> typ val unvarifyT: typ -> typ val varify: term -> term @@ -462,6 +463,13 @@ in pairrev (Hs,[]) end; +fun assum_problems (nasms, A) = + let + val (params, A') = strip_assums_all ([], A) + val (Hs, B) = strip_assums_imp (nasms, [], A') + fun abspar t = rlist_abs (params, t) + in (abspar, rev Hs, B) end; + (* global schematic variables *) diff -r 7b0017587e7d -r e99c5466af92 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/meta_simplifier.ML Tue Mar 17 14:14:25 2009 +0100 @@ -73,6 +73,8 @@ val prune_params_tac: tactic val fold_rule: thm list -> thm -> thm val fold_goals_tac: thm list -> tactic + val norm_hhf: thm -> thm + val norm_hhf_protect: thm -> thm end; signature META_SIMPLIFIER = @@ -122,8 +124,6 @@ (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic - val norm_hhf: thm -> thm - val norm_hhf_protect: thm -> thm val rewrite: bool -> thm list -> conv val simplify: bool -> thm list -> thm -> thm end; diff -r 7b0017587e7d -r e99c5466af92 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/more_thm.ML Tue Mar 17 14:14:25 2009 +0100 @@ -33,6 +33,8 @@ val add_thm: thm -> thm list -> thm list val del_thm: thm -> thm list -> thm list val merge_thms: thm list * thm list -> thm list + val intro_rules: thm Item_Net.T + val elim_rules: thm Item_Net.T val elim_implies: thm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm @@ -213,6 +215,12 @@ val merge_thms = merge eq_thm_prop; +(* indexed collections *) + +val intro_rules = Item_Net.init eq_thm_prop Thm.concl_of; +val elim_rules = Item_Net.init eq_thm_prop Thm.major_prem_of; + + (** basic derived rules **) diff -r 7b0017587e7d -r e99c5466af92 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/pattern.ML Tue Mar 17 14:14:25 2009 +0100 @@ -290,7 +290,8 @@ (*Tests whether 2 terms are alpha/eta-convertible and have same type. Note that Consts and Vars may have more than one type.*) -fun t aeconv u = Envir.eta_contract t aconv Envir.eta_contract u; +fun t aeconv u = t aconv u orelse + Envir.eta_contract t aconv Envir.eta_contract u; (*** Matching ***) diff -r 7b0017587e7d -r e99c5466af92 src/Pure/subgoal.ML --- a/src/Pure/subgoal.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/subgoal.ML Tue Mar 17 14:14:25 2009 +0100 @@ -29,7 +29,7 @@ fun focus ctxt i st = let val ((schematics, [st']), ctxt') = - Variable.import_thms true [MetaSimplifier.norm_hhf_protect st] ctxt; + Variable.import_thms true [Simplifier.norm_hhf_protect st] ctxt; val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt'; val asms = Drule.strip_imp_prems goal; val concl = Drule.strip_imp_concl goal; diff -r 7b0017587e7d -r e99c5466af92 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/tactic.ML Tue Mar 17 14:14:25 2009 +0100 @@ -66,8 +66,6 @@ val innermost_params: int -> thm -> (string * typ) list val term_lift_inst_rule: thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm - val untaglist: (int * 'a) list -> 'a list - val orderlist: (int * 'a) list -> 'a list val insert_tagged_brl: 'a * (bool * thm) -> ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net @@ -264,20 +262,6 @@ (** To preserve the order of the rules, tag them with increasing integers **) -(*insert tags*) -fun taglist k [] = [] - | taglist k (x::xs) = (k,x) :: taglist (k+1) xs; - -(*remove tags and suppress duplicates -- list is assumed sorted!*) -fun untaglist [] = [] - | untaglist [(k:int,x)] = [x] - | untaglist ((k,x) :: (rest as (k',x')::_)) = - if k=k' then untaglist rest - else x :: untaglist rest; - -(*return list elements in original order*) -fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); - (*insert one tagged brl into the pair of nets*) fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) = if eres then @@ -288,7 +272,7 @@ (*build a pair of nets for biresolution*) fun build_netpair netpair brls = - fold_rev insert_tagged_brl (taglist 1 brls) netpair; + fold_rev insert_tagged_brl (tag_list 1 brls) netpair; (*delete one kbrl from the pair of nets*) fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th') @@ -314,8 +298,8 @@ in PRIMSEQ (biresolution match (order kbrls) i) end); (*versions taking pre-built nets. No filtering of brls*) -val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false; -val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist true; +val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false; +val bimatch_from_nets_tac = biresolution_from_nets_tac order_list true; (*fast versions using nets internally*) val net_biresolve_tac = @@ -332,7 +316,7 @@ (*build a net of rules for resolution*) fun build_net rls = - fold_rev insert_krl (taglist 1 rls) Net.empty; + fold_rev insert_krl (tag_list 1 rls) Net.empty; (*resolution using a net rather than rules; pred supports filt_resolve_tac*) fun filt_resolution_from_net_tac match pred net = @@ -342,7 +326,7 @@ in if pred krls then PRIMSEQ - (biresolution match (map (pair false) (orderlist krls)) i) + (biresolution match (map (pair false) (order_list krls)) i) else no_tac end); diff -r 7b0017587e7d -r e99c5466af92 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Pure/thm.ML Tue Mar 17 14:14:25 2009 +0100 @@ -1247,12 +1247,17 @@ else (*normalize the new rule fully*) Envir.norm_term env (Logic.list_implies (Bs, C)), thy_ref = Theory.check_thy thy}); + + val (close, asms, concl) = Logic.assum_problems (~1, Bi); + val concl' = close concl; fun addprfs [] _ = Seq.empty - | addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull + | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull (Seq.mapp (newth n) - (Unify.unifiers (thy, Envir.empty maxidx, (t, u) :: tpairs)) - (addprfs apairs (n + 1)))) - in addprfs (Logic.assum_pairs (~1, Bi)) 1 end; + (if Term.could_unify (asm, concl) then + (Unify.unifiers (thy, Envir.empty maxidx, (close asm, concl') :: tpairs)) + else Seq.empty) + (addprfs rest (n + 1)))) + in addprfs asms 1 end; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) @@ -1260,8 +1265,9 @@ let val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); + val (_, asms, concl) = Logic.assum_problems (~1, Bi); in - (case find_index Pattern.aeconv (Logic.assum_pairs (~1, Bi)) of + (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of ~1 => raise THM ("eq_assumption", 0, [state]) | n => Thm (deriv_rule1 (Pt.assumption_proof Bs Bi (n + 1)) der, @@ -1520,24 +1526,37 @@ val env = Envir.empty(Int.max(rmax,smax)); val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); val dpairs = BBi :: (rtpairs@stpairs); - (*elim-resolution: try each assumption in turn. Initially n=1*) - fun tryasms (_, _, _, []) = Seq.empty - | tryasms (A, As, n, (t,u)::apairs) = - (case Seq.pull(Unify.unifiers(thy, env, (t,u)::dpairs)) of - NONE => tryasms (A, As, n+1, apairs) - | cell as SOME((_,tpairs),_) => - Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs))) - (Seq.make(fn()=> cell), - Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs))))) - fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) - | eres (A1::As) = tryasms(SOME A1, As, 1, Logic.assum_pairs(nlift+1,A1)) + + (*elim-resolution: try each assumption in turn*) + fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state]) + | eres (A1 :: As) = + let + val A = SOME A1; + val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1); + val concl' = close concl; + fun tryasms [] _ = Seq.empty + | tryasms (asm :: rest) n = + if Term.could_unify (asm, concl) then + let val asm' = close asm in + (case Seq.pull (Unify.unifiers (thy, env, (asm', concl') :: dpairs)) of + NONE => tryasms rest (n + 1) + | cell as SOME ((_, tpairs), _) => + Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs))) + (Seq.make (fn () => cell), + Seq.make (fn () => Seq.pull (tryasms rest (n + 1))))) + end + else tryasms rest (n + 1); + in tryasms asms 1 end; + (*ordinary resolution*) - fun res(NONE) = Seq.empty - | res(cell as SOME((_,tpairs),_)) = - Seq.it_right (addth NONE (newAs(rev rAs, 0, [BBi], tpairs))) - (Seq.make (fn()=> cell), Seq.empty) - in if eres_flg then eres(rev rAs) - else res(Seq.pull(Unify.unifiers(thy, env, dpairs))) + fun res () = + (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of + NONE => Seq.empty + | cell as SOME ((_, tpairs), _) => + Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs))) + (Seq.make (fn () => cell), Seq.empty)); + in + if eres_flg then eres (rev rAs) else res () end; end; diff -r 7b0017587e7d -r e99c5466af92 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Tools/coherent.ML Tue Mar 17 14:14:25 2009 +0100 @@ -51,7 +51,7 @@ end; -fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); +fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); (* Decompose elimination rule of the form A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P diff -r 7b0017587e7d -r e99c5466af92 src/Tools/induct.ML --- a/src/Tools/induct.ML Mon Mar 16 15:58:41 2009 -0700 +++ b/src/Tools/induct.ML Tue Mar 17 14:14:25 2009 +0100 @@ -111,19 +111,19 @@ (* rules *) -type rules = (string * thm) NetRules.T; +type rules = (string * thm) Item_Net.T; val init_rules = - NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso + Item_Net.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2)); fun filter_rules (rs: rules) th = - filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (NetRules.rules rs); + filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs); -fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs); +fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs); fun pretty_rules ctxt kind rs = - let val thms = map snd (NetRules.rules rs) + let val thms = map snd (Item_Net.content rs) in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end; @@ -139,21 +139,21 @@ val extend = I; fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)), ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) = - ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)), - (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)), - (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2))); + ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)), + (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)), + (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2))); ); val get_local = InductData.get o Context.Proof; fun dest_rules ctxt = let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in - {type_cases = NetRules.rules casesT, - pred_cases = NetRules.rules casesP, - type_induct = NetRules.rules inductT, - pred_induct = NetRules.rules inductP, - type_coinduct = NetRules.rules coinductT, - pred_coinduct = NetRules.rules coinductP} + {type_cases = Item_Net.content casesT, + pred_cases = Item_Net.content casesP, + type_induct = Item_Net.content inductT, + pred_induct = Item_Net.content inductP, + type_coinduct = Item_Net.content coinductT, + pred_coinduct = Item_Net.content coinductP} end; fun print_rules ctxt = @@ -184,7 +184,7 @@ fun find_rules which how ctxt x = - map snd (NetRules.retrieve (which (get_local ctxt)) (how x)); + map snd (Item_Net.retrieve (which (get_local ctxt)) (how x)); val find_casesT = find_rules (#1 o #1) encode_type; val find_casesP = find_rules (#2 o #1) I; @@ -203,18 +203,18 @@ let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end; fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs => - fold NetRules.delete (filter_rules rs th) rs)))); + fold Item_Net.delete (filter_rules rs th) rs)))); fun map1 f (x, y, z) = (f x, y, z); fun map2 f (x, y, z) = (x, f y, z); fun map3 f (x, y, z) = (x, y, f z); -fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x; -fun add_casesP rule x = map1 (apsnd (NetRules.insert rule)) x; -fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x; -fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x; -fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x; -fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x; +fun add_casesT rule x = map1 (apfst (Item_Net.insert rule)) x; +fun add_casesP rule x = map1 (apsnd (Item_Net.insert rule)) x; +fun add_inductT rule x = map2 (apfst (Item_Net.insert rule)) x; +fun add_inductP rule x = map2 (apsnd (Item_Net.insert rule)) x; +fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x; +fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x; val consumes0 = RuleCases.consumes_default 0; val consumes1 = RuleCases.consumes_default 1;