--- 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.
--- 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.
--- 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
--- 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;
--- 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*)
--- 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;
--- 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
--- 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";
-
-
--- 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);
--- 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;
--- 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
--- 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";
--- 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
--- /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;
--- 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 **)
--- 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 *)
--- 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;
--- 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 **)
--- 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 ***)
--- 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;
--- 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);
--- 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;
--- 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
--- 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;