# HG changeset patch # User wenzelm # Date 1303333049 -7200 # Node ID 9efdd0af15ac022eb0400d83e6563321dbbbce6e # Parent cf963c834435c7266f591f02641a73f6d0580481 eliminated Display.string_of_thm_without_context; tuned whitespace; diff -r cf963c834435 -r 9efdd0af15ac src/FOLP/classical.ML --- 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}; diff -r cf963c834435 -r 9efdd0af15ac src/HOL/Tools/inductive.ML --- 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])])); diff -r cf963c834435 -r 9efdd0af15ac src/HOL/Tools/lin_arith.ML --- 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; diff -r cf963c834435 -r 9efdd0af15ac src/Provers/classical.ML --- 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; diff -r cf963c834435 -r 9efdd0af15ac src/ZF/Tools/typechk.ML --- 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;