--- a/src/FOLP/classical.ML Wed Apr 20 17:17:01 2011 +0200
+++ b/src/FOLP/classical.ML Wed Apr 20 22:57:29 2011 +0200
@@ -39,7 +39,7 @@
val addSDs: claset * thm list -> claset
val addSEs: claset * thm list -> claset
val addSIs: claset * thm list -> claset
- val print_cs: claset -> unit
+ val print_cs: Proof.context -> claset -> unit
val rep_cs: claset ->
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list,
safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
@@ -122,12 +122,12 @@
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
-fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
+fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
writeln (cat_lines
- (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
- ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
- ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
- ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
+ (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @
+ ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @
+ ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @
+ ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs));
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
--- a/src/HOL/Tools/inductive.ML Wed Apr 20 17:17:01 2011 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Apr 20 22:57:29 2011 +0200
@@ -174,7 +174,7 @@
val get_monos = #2 o get_inductives;
val map_monos = InductiveData.map o apsnd;
-fun mk_mono thm =
+fun mk_mono ctxt thm =
let
fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
@@ -187,11 +187,15 @@
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
| _ => thm
- end handle THM _ =>
- error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
+ end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
-val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono);
-val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono);
+val mono_add =
+ Thm.declaration_attribute (fn thm => fn context =>
+ map_monos (Thm.add_thm (mk_mono (Context.proof_of context) thm)) context);
+
+val mono_del =
+ Thm.declaration_attribute (fn thm => fn context =>
+ map_monos (Thm.del_thm (mk_mono (Context.proof_of context) thm)) context);
@@ -350,7 +354,7 @@
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
REPEAT (FIRST
[atac 1,
- resolve_tac (map mk_mono monos @ get_monos ctxt) 1,
+ resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
--- a/src/HOL/Tools/lin_arith.ML Wed Apr 20 17:17:01 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Apr 20 22:57:29 2011 +0200
@@ -271,9 +271,9 @@
val {discrete, inj_consts, ...} = get_arith_data ctxt
in decomp_negation (thy, discrete, inj_consts) end;
-fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
+fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
| domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
- | domain_is_nat _ = false;
+ | domain_is_nat _ = false;
(*---------------------------------------------------------------------------*)
@@ -284,23 +284,25 @@
(* checks if splitting with 'thm' is implemented *)
-fun is_split_thm thm =
- case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
+fun is_split_thm ctxt thm =
+ (case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) =>
(* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
- case head_of lhs of
- Const (a, _) => member (op =) [@{const_name Orderings.max},
- @{const_name Orderings.min},
- @{const_name Groups.abs},
- @{const_name Groups.minus},
- "Int.nat" (*DYNAMIC BINDING!*),
- "Divides.div_class.mod" (*DYNAMIC BINDING!*),
- "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
- | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
- Display.string_of_thm_without_context thm);
- false))
- | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
- Display.string_of_thm_without_context thm);
- false);
+ (case head_of lhs of
+ Const (a, _) =>
+ member (op =)
+ [@{const_name Orderings.max},
+ @{const_name Orderings.min},
+ @{const_name Groups.abs},
+ @{const_name Groups.minus},
+ "Int.nat" (*DYNAMIC BINDING!*),
+ "Divides.div_class.mod" (*DYNAMIC BINDING!*),
+ "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
+ | _ =>
+ (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
+ false))
+ | _ =>
+ (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
+ false));
(* substitute new for occurrences of old in a term, incrementing bound *)
(* variables as needed when substituting inside an abstraction *)
@@ -343,7 +345,7 @@
fun REPEAT_DETERM_etac_rev_mp tms =
fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
HOLogic.false_const
- val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
+ val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
val cmap = Splitter.cmap_of_split_thms split_thms
val goal_tm = REPEAT_DETERM_etac_rev_mp terms
val splits = Splitter.split_posns cmap thy Ts goal_tm
@@ -645,13 +647,13 @@
(* terms in the same way as filter_prems_tac does *)
fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
-let
- fun filter_prems t (left, right) =
- if p t then (left, right @ [t]) else (left @ right, [])
- val (left, right) = fold filter_prems terms ([], [])
-in
- right @ left
-end;
+ let
+ fun filter_prems t (left, right) =
+ if p t then (left, right @ [t]) else (left @ right, [])
+ val (left, right) = fold filter_prems terms ([], [])
+ in
+ right @ left
+ end;
(* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *)
(* subgoal that has 'terms' as premises *)
@@ -664,29 +666,27 @@
terms;
fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list =
-let
- (* repeatedly split (including newly emerging subgoals) until no further *)
- (* splitting is possible *)
- fun split_loop ([] : (typ list * term list) list) =
- ([] : (typ list * term list) list)
- | split_loop (subgoal::subgoals) =
- (case split_once_items ctxt subgoal of
- SOME new_subgoals => split_loop (new_subgoals @ subgoals)
- | NONE => subgoal :: split_loop subgoals)
- fun is_relevant t = is_some (decomp ctxt t)
- (* filter_prems_tac is_relevant: *)
- val relevant_terms = filter_prems_tac_items is_relevant terms
- (* split_tac, NNF normalization: *)
- val split_goals = split_loop [(Ts, relevant_terms)]
- (* necessary because split_once_tac may normalize terms: *)
- val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
- split_goals
- (* TRY (etac notE) THEN eq_assume_tac: *)
- val result = filter_out (negated_term_occurs_positively o snd)
- beta_eta_norm
-in
- result
-end;
+ let
+ (* repeatedly split (including newly emerging subgoals) until no further *)
+ (* splitting is possible *)
+ fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
+ | split_loop (subgoal::subgoals) =
+ (case split_once_items ctxt subgoal of
+ SOME new_subgoals => split_loop (new_subgoals @ subgoals)
+ | NONE => subgoal :: split_loop subgoals)
+ fun is_relevant t = is_some (decomp ctxt t)
+ (* filter_prems_tac is_relevant: *)
+ val relevant_terms = filter_prems_tac_items is_relevant terms
+ (* split_tac, NNF normalization: *)
+ val split_goals = split_loop [(Ts, relevant_terms)]
+ (* necessary because split_once_tac may normalize terms: *)
+ val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
+ split_goals
+ (* TRY (etac notE) THEN eq_assume_tac: *)
+ val result = filter_out (negated_term_occurs_positively o snd) beta_eta_norm
+ in
+ result
+ end;
(* takes the i-th subgoal [| A1; ...; An |] ==> B to *)
(* An --> ... --> A1 --> B, performs splitting with the given 'split_thms' *)
@@ -744,22 +744,22 @@
(* contradiction (i.e., a term and its negation) in their premises. *)
fun pre_tac ss i =
-let
- val ctxt = Simplifier.the_context ss;
- val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
- fun is_relevant t = is_some (decomp ctxt t)
-in
- DETERM (
- TRY (filter_prems_tac is_relevant i)
- THEN (
- (TRY o REPEAT_ALL_NEW (split_once_tac ss split_thms))
- THEN_ALL_NEW
- (CONVERSION Drule.beta_eta_conversion
- THEN'
- (TRY o (etac notE THEN' eq_assume_tac)))
- ) i
- )
-end;
+ let
+ val ctxt = Simplifier.the_context ss;
+ val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
+ fun is_relevant t = is_some (decomp ctxt t)
+ in
+ DETERM (
+ TRY (filter_prems_tac is_relevant i)
+ THEN (
+ (TRY o REPEAT_ALL_NEW (split_once_tac ss split_thms))
+ THEN_ALL_NEW
+ (CONVERSION Drule.beta_eta_conversion
+ THEN'
+ (TRY o (etac notE THEN' eq_assume_tac)))
+ ) i
+ )
+ end;
end; (* LA_Data *)
@@ -783,7 +783,8 @@
val init_arith_data =
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} =>
- {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @ @{thms add_mono_thms_linordered_field} @ add_mono_thms,
+ {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @
+ @{thms add_mono_thms_linordered_field} @ add_mono_thms,
mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} ::
@{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms,
inj_thms = inj_thms,
@@ -840,6 +841,7 @@
fun prem_nnf_tac i st =
full_simp_tac (Simplifier.global_context (Thm.theory_of_thm st) nnf_simpset) i st;
in
+
fun refute_tac test prep_tac ref_tac =
let val refute_prems_tac =
REPEAT_DETERM
@@ -852,6 +854,7 @@
REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac,
SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
end;
+
end;
--- a/src/Provers/classical.ML Wed Apr 20 17:17:01 2011 +0200
+++ b/src/Provers/classical.ML Wed Apr 20 22:57:29 2011 +0200
@@ -37,7 +37,7 @@
sig
type claset
val empty_cs: claset
- val print_cs: claset -> unit
+ val print_cs: Proof.context -> claset -> unit
val rep_cs:
claset -> {safeIs: thm list, safeEs: thm list,
hazIs: thm list, hazEs: thm list,
@@ -258,8 +258,8 @@
dup_netpair = empty_netpair,
xtra_netpair = empty_netpair};
-fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
- let val pretty_thms = map Display.pretty_thm_without_context in
+fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
+ let val pretty_thms = map (Display.pretty_thm ctxt) in
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
@@ -1018,6 +1018,8 @@
Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
- Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
+ Toplevel.keep (fn state =>
+ let val ctxt = Toplevel.context_of state
+ in print_cs ctxt (claset_of ctxt) end)));
end;
--- a/src/ZF/Tools/typechk.ML Wed Apr 20 17:17:01 2011 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Apr 20 22:57:29 2011 +0200
@@ -25,20 +25,17 @@
{rules: thm list, (*the type-checking rules*)
net: thm Net.net}; (*discrimination net of the same rules*)
-fun add_rule th (tcs as TC {rules, net}) =
+fun add_rule ctxt th (tcs as TC {rules, net}) =
if member Thm.eq_thm_prop rules th then
- (warning ("Ignoring duplicate type-checking rule\n" ^
- Display.string_of_thm_without_context th); tcs)
+ (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs)
else
- TC {rules = th :: rules,
- net = Net.insert_term (K false) (Thm.concl_of th, th) net};
+ TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
-fun del_rule th (tcs as TC {rules, net}) =
+fun del_rule ctxt th (tcs as TC {rules, net}) =
if member Thm.eq_thm_prop rules th then
TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
- rules = remove Thm.eq_thm_prop th rules}
- else (warning ("No such type-checking rule\n" ^
- Display.string_of_thm_without_context th); tcs);
+ rules = remove Thm.eq_thm_prop th rules}
+ else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs);
(* generic data *)
@@ -52,8 +49,13 @@
TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
);
-val TC_add = Thm.declaration_attribute (Data.map o add_rule);
-val TC_del = Thm.declaration_attribute (Data.map o del_rule);
+val TC_add =
+ Thm.declaration_attribute (fn thm => fn context =>
+ Data.map (add_rule (Context.proof_of context) thm) context);
+
+val TC_del =
+ Thm.declaration_attribute (fn thm => fn context =>
+ Data.map (del_rule (Context.proof_of context) thm) context);
val tcset_of = Data.get o Context.Proof;